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

-- |
  -- Module      :  Lift
  -- Copyright   :  (c) Reed Mullanix 2019
  -- License     :  BSD-style
  -- Maintainer  :  [email protected]
  --
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}

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

{-
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

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

:- 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).