AgdaTuringMachine2.agda

module Scratch where

postulate
  Inf  : ∀ {a} (A : Set a) → Set a
  delay : ∀ {a} {A : Set a} → A → Inf A
  force  : ∀ {a} {A : Set a} → Inf A → A

{-# BUILTIN INFINITY Inf  #-}
{-# BUILTIN SHARP    delay #-}
{-# BUILTIN FLAT     force  #-}

record _*_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A → Maybe A

data CoList (A : Set) : Set where
  [] : CoList A
  _::_ : A → Inf (CoList A) → CoList A

unfold : ∀ {A : Set} → A → (A → Maybe A) → CoList A
unfold x f with f x
... | Nothing = []
... | Just x' = x :: delay (unfold x' f)


data LList (A : Set) : Set where
  [] : LList A
  _<:_ : LList A → A → LList A

data RList (A : Set) : Set where
  [] : RList A
  _:>_ : A → RList A → RList A

data Tape (A : Set) : Set where
  _[_]_ : LList (Maybe A) → Maybe A → RList (Maybe A) → Tape A

data Machine (A Q : Set) : Set where
  Done : Tape A → Machine A Q
  Running : Tape A → Q → Machine A Q

data Move (A Q : Set) : Set where
  Halt : Move A Q
  Left Right : Q → Move A Q
  Write : Maybe A → Q → Move A Q

Transition : Set → Set → Set
Transition A Q = Maybe A → Q → Move A Q

left : ∀ {A} → Tape A → Tape A
left ([] [ r ] rs) = [] [ Nothing ] (r :> rs)
left ((ls <: l) [ r ] rs) = ls [ l ] (r :> rs)

right : ∀ {A} → Tape A → Tape A
right (ls [ l ] []) = (ls <: l) [ Nothing ] []
right (ls [ l ] (r :> rs)) = (ls <: l) [ r ] rs

write : ∀ {A} → Maybe A → Tape A → Tape A
write x (ls [ _ ] rs) = ls [ x ] rs

step : ∀ {A Q} → Transition A Q → Machine A Q → Maybe (Machine A Q)
step _ (Done t) = Nothing
step f (Running (ls [ x ] rs) q) with f x q
... | Halt = Just (Done (ls [ x ] rs))
... | Left q' = Just (Running (left (ls [ x ] rs)) q')
... | Right q' = Just (Running (right (ls [ x ] rs)) q')
... | Write y q' = Just (Running (write y (ls [ x ] rs)) q')

run : ∀ {A Q} → Transition A Q → Tape A → Q → CoList (Machine A Q)
run f t0 q0 = unfold (Running t0 q0) (step f)