module pushdown 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 PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
       : Set  where
    field
        pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
        pstart : Q
        pok : Q → Bool
        pempty : Γ
    pmoves :  Q → List  Γ  → Σ → ( Q × List  Γ )
    pmoves q [] i with pδ q i pempty
    pmoves q [] i | qn , pop = ( qn , [] )
    pmoves q [] i | qn , push x = ( qn , ( x ∷  [] ) )
    pmoves q (  H  ∷ T  ) i with pδ q i H
    pmoves q (H ∷ T) i | qn , pop =  ( qn , T )
    pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )

    paccept : List  Σ → Bool
    paccept L = move pstart L []
           where
              move : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
              move q [] [] = pok q
              move q ( H  ∷ T) [] with pδ q H pempty
              move q (H ∷ T) [] | qn , pop = move qn T []
              move q (H ∷ T) [] | qn , push x = move qn T (x  ∷ [] )
              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 )


--  0011
--  00000111111
inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
inputnn {zero} {_} _ _ s = s
inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )       

data  States0   : Set  where
   sr : States0

data  In2   : Set  where
   i0 : In2
   i1 : In2
 
pnn : PushDownAutomaton States0 In2 States0
pnn = record {
         pδ  = pδ
      ;  pstart = sr
      ;  pempty = sr
      ;  pok = λ q → true
   } where
        pδ  : States0 → In2 → States0 → States0 × PushDown States0
        pδ sr i0 _ = (sr , push sr) 
        pδ sr i1 _ = (sr , pop ) 

test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
test3 = PushDownAutomaton.pmoves pnn sr [] i0