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
        pz0 :  Γ
    pmoves :  Q → List  Σ → ( Q × List  Γ )
    pmoves q L = move q L [ pz0 ]
           where
              move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × 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 )
    paccept : List  Σ → Bool
    paccept 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 )