module turing where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat hiding ( erase )
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 Write   (  Σ : Set  ) : Set  where
   write   : Σ → Write  Σ
   wnone   : Write  Σ
   --   erase write tnone

data Move   (  Σ : Set  ) : Set  where
   left   : Move  Σ
   right  : Move  Σ
   mnone  : Move  Σ

-- at tδ both stack is poped

-- write S      push S  , push SR
-- erase        push SL , push tone 
-- none         push SL , push SR 
-- left         push SR , pop      
-- right        pop     , push SL      


record Turing ( Q : Set ) ( Σ : Set  ) 
       : Set  where
    field
        tδ : Q →  Σ → Q × ( Write  Σ ) × ( Move  Σ )
        tstart : Q
        tend : Q → Bool
        tnone :  Σ
    {-# TERMINATING #-}
    move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
    move q L [] = move q  L  ( tnone  ∷ [] ) 
    move q [] R = move q  ( tnone  ∷ [] )  R 
    move q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
    ... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
    ... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
    ... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
    ... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
    ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
    ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
    {-# TERMINATING #-}
    move-loop : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
    move-loop  q L R with tend q
    ... | true = ( q , L , R )
    ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
      where
        next = move  q  L  R 
    taccept : List  Σ → ( Q × List  Σ × List  Σ )
    taccept L = move-loop tstart L []

data CopyStates : Set where
   s1 : CopyStates
   s2 : CopyStates
   s3 : CopyStates
   s4 : CopyStates
   s5 : CopyStates
   H  : CopyStates


Copyδ :  CopyStates →  Bool → CopyStates × ( Write  Bool ) × ( Move  Bool )
Copyδ s1 false  = (H    , wnone       , mnone )
Copyδ s1 true   = (s2   , write false , right )
Copyδ s2 false  = (s3   , write false , right )
Copyδ s2 true   = (s2   , write true  , right )
Copyδ s3 false  = (s4   , write true  , left )
Copyδ s3 true   = (s3   , write true  , right )
Copyδ s4 false  = (s5   , write false , left )
Copyδ s4 true   = (s4   , write true  , left )
Copyδ s5 false  = (s1   , write true  , right )
Copyδ s5 true   = (s5   , write true  , left )
Copyδ H  _      = (H    , wnone       , mnone )

copyMachine : Turing CopyStates Bool
copyMachine = record {
        tδ = Copyδ
     ;  tstart = s1
     ;  tend = tend
     ;  tnone =  false
  } where
      tend : CopyStates →  Bool
      tend H = true
      tend _ = false

test1 : CopyStates × ( List  Bool ) × ( List  Bool )
test1 = Turing.taccept copyMachine  ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  )

test2 : ℕ  → CopyStates × ( List  Bool ) × ( List  Bool )
test2 n  = loop n (Turing.tstart copyMachine) ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  ) []
  where
        loop :  ℕ → CopyStates → ( List  Bool ) → ( List  Bool ) → CopyStates × ( List  Bool ) × ( List  Bool )
        loop zero q L R = ( q , L , R )
        loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) )  ( proj₂  ( proj₂ t1 ) )
          where
              t1 = Turing.move copyMachine q L R