Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/pushdown.agda @ 330:407684f806e4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Nov 2022 17:43:10 +0900 |
| parents | 91781b7c65a8 |
| children | 6f3636fbc481 |
| rev | line source |
|---|---|
| 17 | 1 module pushdown where |
| 2 | |
| 3 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 4 open import Data.Nat | |
| 5 open import Data.List | |
| 6 open import Data.Maybe | |
| 275 | 7 -- open import Data.Bool using ( Bool ; true ; false ) |
| 17 | 8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 9 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 10 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 275 | 11 -- open import Data.Product |
| 12 open import logic | |
| 318 | 13 open import automaton |
| 17 | 14 |
| 15 | |
| 16 data PushDown ( Γ : Set ) : Set where | |
| 17 pop : PushDown Γ | |
| 18 push : Γ → PushDown Γ | |
| 275 | 19 none : PushDown Γ |
| 17 | 20 |
| 21 | |
| 22 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set ) | |
| 23 : Set where | |
| 24 field | |
| 275 | 25 pδ : Q → Σ → Γ → Q ∧ ( PushDown Γ ) |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
26 pok : Q → Bool |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
27 pempty : Γ |
| 275 | 28 pmoves : Q → List Γ → Σ → ( Q ∧ List Γ ) |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
29 pmoves q [] i with pδ q i pempty |
| 275 | 30 pmoves q [] i | ⟪ qn , pop ⟫ = ⟪ qn , [] ⟫ |
| 31 pmoves q [] i | ⟪ qn , push x ⟫ = ⟪ qn , ( x ∷ [] ) ⟫ | |
| 32 pmoves q [] i | ⟪ qn , none ⟫ = ⟪ qn , [] ⟫ | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
33 pmoves q ( H ∷ T ) i with pδ q i H |
| 275 | 34 pmoves q (H ∷ T) i | ⟪ qn , pop ⟫ = ⟪ qn , T ⟫ |
| 35 pmoves q (H ∷ T) i | ⟪ qn , none ⟫ = ⟪ qn , (H ∷ T) ⟫ | |
| 36 pmoves q (H ∷ T) i | ⟪ qn , push x ⟫ = ⟪ qn , x ∷ H ∷ T ⟫ | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
37 |
| 138 | 38 paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool |
| 39 paccept q [] [] = pok q | |
| 40 paccept q ( H ∷ T) [] with pδ q H pempty | |
| 275 | 41 paccept q (H ∷ T) [] | ⟪ qn , pop ⟫ = paccept qn T [] |
| 42 paccept q (H ∷ T) [] | ⟪ qn , none ⟫ = paccept qn T [] | |
| 43 paccept q (H ∷ T) [] | ⟪ qn , push x ⟫ = paccept qn T (x ∷ [] ) | |
| 138 | 44 paccept q [] (_ ∷ _ ) = false |
| 45 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH | |
| 275 | 46 ... | ⟪ nq , pop ⟫ = paccept nq T ST |
| 47 ... | ⟪ nq , none ⟫ = paccept nq T (SH ∷ ST) | |
| 48 ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns ∷ SH ∷ ST ) | |
| 138 | 49 |
| 318 | 50 record PDA ( Q : Set ) ( Σ : Set ) ( Γ : Set ) |
| 51 : Set where | |
| 52 field | |
| 53 automaton : Automaton Q Σ | |
| 54 pδ : Q → PushDown Γ | |
| 55 open Automaton | |
| 56 paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool | |
| 57 paccept q [] [] = aend automaton q | |
| 58 paccept q (H ∷ T) [] with pδ (δ automaton q H) | |
| 59 paccept q (H ∷ T) [] | pop = paccept (δ automaton q H) T [] | |
| 60 paccept q (H ∷ T) [] | none = paccept (δ automaton q H) T [] | |
| 61 paccept q (H ∷ T) [] | push x = paccept (δ automaton q H) T (x ∷ [] ) | |
| 62 paccept q [] (_ ∷ _ ) = false | |
| 63 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ (δ automaton q H) | |
| 64 ... | pop = paccept (δ automaton q H) T ST | |
| 65 ... | none = paccept (δ automaton q H) T (SH ∷ ST) | |
| 66 ... | push ns = paccept (δ automaton q H) T ( ns ∷ SH ∷ ST ) | |
| 17 | 67 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
68 data States0 : Set where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
69 sr : States0 |
| 17 | 70 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
71 data In2 : Set where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
72 i0 : In2 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
73 i1 : In2 |
| 138 | 74 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
75 pnn : PushDownAutomaton States0 In2 States0 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
76 pnn = record { |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
77 pδ = pδ |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
78 ; pempty = sr |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
79 ; pok = λ q → true |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
80 } where |
| 275 | 81 pδ : States0 → In2 → States0 → States0 ∧ PushDown States0 |
| 82 pδ sr i0 _ = ⟪ sr , push sr ⟫ | |
| 83 pδ sr i1 _ = ⟪ sr , pop ⟫ | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
84 |
| 318 | 85 data States2 : Set where |
| 86 ph1 : States2 | |
| 87 ph2 : States2 | |
| 88 phf : States2 | |
| 89 | |
| 90 pnnp : PDA States2 In2 States2 | |
| 91 pnnp = record { | |
| 92 automaton = record { aend = aend ; δ = δ } | |
| 93 ; pδ = pδ | |
| 94 } where | |
| 95 δ : States2 → In2 → States2 | |
| 96 δ ph1 i0 = ph1 | |
| 97 δ ph1 i1 = ph2 | |
| 98 δ ph2 i1 = ph2 | |
| 99 δ _ _ = phf | |
| 100 aend : States2 → Bool | |
| 101 aend ph2 = true | |
| 102 aend _ = false | |
| 103 pδ : States2 → PushDown States2 | |
| 104 pδ ph1 = push ph1 | |
| 105 pδ ph2 = pop | |
| 106 pδ phf = none | |
| 107 | |
| 138 | 108 data States1 : Set where |
| 109 ss : States1 | |
| 110 st : States1 | |
| 111 pn1 : PushDownAutomaton States1 In2 States1 | |
| 112 pn1 = record { | |
| 113 pδ = pδ | |
| 114 ; pempty = ss | |
| 115 ; pok = pok1 | |
| 116 } where | |
| 117 pok1 : States1 → Bool | |
| 118 pok1 ss = false | |
| 119 pok1 st = true | |
| 275 | 120 pδ : States1 → In2 → States1 → States1 ∧ PushDown States1 |
| 121 pδ ss i0 _ = ⟪ ss , push ss ⟫ | |
| 122 pδ ss i1 _ = ⟪ st , pop ⟫ | |
| 123 pδ st i0 _ = ⟪ st , push ss ⟫ | |
| 124 pδ st i1 _ = ⟪ st , pop ⟫ | |
| 138 | 125 |
| 126 test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] | |
| 127 test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) [] | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
128 test3 = PushDownAutomaton.pmoves pnn sr [] i0 |
| 138 | 129 test4 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) [] |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
130 |
| 138 | 131 test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] |
| 132 test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) [] | |
| 141 | 133 |