TOTBWF

:- set_prolog_flag(double_quotes, chars).

tape(N, List) :- length(List, N), zeros(List).

zeros([]).
zeros([0|T]) :- zeros(T).

interpret(_, [], _, _, _, Acc) --> { reverse(Acc, RAcc) }, RAcc. 
interpret(Seen, [+|Next], Left, [Data], Right, Acc) --> { NData is Data + 1}, interpret([+|Seen], Next, Left, [NData], Right, Acc).
interpret(Seen, [-|Next], Left, [Data], Right, Acc) --> { NData is Data - 1}, interpret([-|Seen], Next, Left, [NData], Right, Acc).

TOTBWF

newtype StateLT s m a = StateLT { runStateLT :: s -> m (s,a) }

instance (Functor m) => Functor (StateLT s m) where
  fmap f (StateLT k) = StateLT $ \s -> fmap (\(s',a) -> (s', f a)) $ k s

instance Monad m => Applicative (StateLT s m) where
  pure a = StateLT $ \s -> return (s, a)
  StateLT kf <*> StateLT kv = StateLT $ \s -> do
    (s', f) <- kf s
    (s'', v) <- kv s'

TOTBWF

{-
Requires (from Stack lts-12.11)
- arithmoi >= 0 && < 1
- containers >= 0.5 && < 0.6
- parallel >= 3 && < 4
- split >= 0.2 && < 0.3
-}
import qualified Math.NumberTheory.Primes.Sieve as Math

import Data.IntSet (IntSet)

TOTBWF

import Control.Monad (zipWithM)
import Data.Foldable (foldlM)

data Command = Up | Down

parseChar :: Char -> Int -> Either String Command
parseChar '(' _ = Right Up
parseChar ')' _ = Right Down
parseChar c i = Left $ "Parse Error: unexpected token " ++ [c] ++ " at index " ++ (show i)

TOTBWF

-- |
  -- Module      :  Lift
  -- Copyright   :  (c) Reed Mullanix 2019
  -- License     :  BSD-style
  -- Maintainer  :  reedmullanix@gmail.com
  --
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}

TOTBWF

{-# OPTIONS --without-K --safe #-}

open import Algebra
module Cayley {a ℓ} {S : Semigroup a ℓ} where

open Semigroup S renaming (Carrier to A; assoc to ∙-assoc; setoid to S-Setoid )

open import Algebra.Structures
open import Algebra.Morphism; open Definitions

TOTBWF

type (~>) f g = forall x. f x -> g x

class HProfunctor (p :: (* -> *) -> (* -> *) -> * -> *) where
  hdimap :: (f ~> g) -> (h ~> i) -> p g h ~> p f i

instance HProfunctor Ran where
  hdimap fg hi r = Ran $ \k -> hi $ runRan r (fg . k)

instance HProfunctor Lan where
  hdimap fg hi (Lan gbx h) = Lan (gbx . fg) (hi h)

TOTBWF

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE GADTs #-}
module Pullbacks where

TOTBWF

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Lib where

import Data.Functor.Const

type family NonInjective env a = result | result -> env where
    NonInjective env (a -> r) = [env] -> NonInjective env r
    NonInjective env a        = [env]

TOTBWF

{-# OPTIONS --without-K --safe #-}
-- Some stuff from "Higher Operads, Higher Categories"
-- https://arxiv.org/abs/math/0305049
module MultiCategory where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

open import Categories.Category
open import Categories.Bicategory