module turing where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat
open import Data.List
open import Data.Maybe
open import Data.Bool using ( Bool ; true ; false )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Product


data PushDown   (  Σ : Set  ) : Set  where
   pop    : PushDown  Σ
   push   :  Σ → PushDown  Σ


record Turing ( Q : Set ) ( Σ : Set  ) 
       : Set  where
    field
        tδ : Q →  Σ → Q × ( PushDown  Σ ) × ( PushDown  Σ )
        tstart : Q
        tend : Q → Bool
        tz0 :  Σ
    tmoves :  Q → List  Σ → ( Q × List  Σ × List  Σ )
    tmoves q L = move q L [ pz0 ]
           where
              move : Q → ( List  Σ ) → ( List  Σ ) → ( Q × List  Σ × List  Σ )
              move q _ [] = ( q , [] )
              move q [] S = ( q , S )
              move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
              ... | (nq , pop )     = move nq T ST
              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
    taccept : List  Σ → Bool
    taccept L = move pstart L [ pz0 ]
           where
              move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → Bool
              move q [] [] = true
              move q _ [] = false
              move q [] (_ ∷ _ ) = false
              move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
              ... | (nq , pop )     = move nq T ST
              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )