Mercurial > hg > Members > kono > Proof > automaton

comparison agda/pushdown.agda @ 38:ab265470c2d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
push down automaton example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Dec 2018 17:50:42 +0900
parents 08b589172493
children 7a0634a7c25a
comparison
equal deleted inserted replaced
37:a7f09c9a2c7a 38:ab265470c2d0
19 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set ) 19 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set )
20 : Set where 20 : Set where
21 field 21 field
22 pδ : Q → Σ → Γ → Q × ( PushDown Γ ) 22 pδ : Q → Σ → Γ → Q × ( PushDown Γ )
23 pstart : Q 23 pstart : Q
24 pz0 : Γ 24 pok : Q → Bool
25 pmoves : Q → List Σ → ( Q × List Γ ) 25 pempty : Γ
26 pmoves q L = move q L [ pz0 ] 26 pmoves : Q → List Γ → Σ → ( Q × List Γ )
27 pmoves q [] i with pδ q i pempty
28 pmoves q [] i | qn , pop = ( qn , [] )
29 pmoves q [] i | qn , push x = ( qn , ( x ∷ [] ) )
30 pmoves q ( H ∷ T ) i with pδ q i H
31 pmoves q (H ∷ T) i | qn , pop = ( qn , T )
32 pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )
33
34 paccept : List Σ → Bool
35 paccept L = move pstart L []
27 where 36 where
28 move : Q → ( List Σ ) → ( List Γ ) → ( Q × List Γ ) 37 move : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool
29 move q _ [] = ( q , [] ) 38 move q [] [] = pok q
30 move q [] S = ( q , S ) 39 move q ( H ∷ T) [] with pδ q H pempty
31 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH 40 move q (H ∷ T) [] | qn , pop = move qn T []
32 ... | (nq , pop ) = move nq T ST 41 move q (H ∷ T) [] | qn , push x = move qn T (x ∷ [] )
33 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
34 paccept : List Σ → Bool
35 paccept L = move pstart L [ pz0 ]
36 where
37 move : (q : Q ) ( L : List Σ ) ( L : List Γ ) → Bool
38 move q [] [] = true
39 move q _ [] = false
40 move q [] (_ ∷ _ ) = false 42 move q [] (_ ∷ _ ) = false
41 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH 43 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
42 ... | (nq , pop ) = move nq T ST 44 ... | (nq , pop ) = move nq T ST
43 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST ) 45 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
44 46
45 47
48 -- 0011
49 -- 00000111111
50 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
51 inputnn {zero} {_} _ _ s = s
52 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) )
46 53
54 data States0 : Set where
55 sr : States0
47 56
57 data In2 : Set where
58 i0 : In2
59 i1 : In2
60
61 pnn : PushDownAutomaton States0 In2 States0
62 pnn = record {
63 pδ = pδ
64 ; pstart = sr
65 ; pempty = sr
66 ; pok = λ q → true
67 } where
68 pδ : States0 → In2 → States0 → States0 × PushDown States0
69 pδ sr i0 _ = (sr , push sr)
70 pδ sr i1 _ = (sr , pop )
71
72 test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
73 test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
74 test3 = PushDownAutomaton.pmoves pnn sr [] i0
75