Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/pushdown.agda @ 289:c9802aa2a8c9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 28 Dec 2021 15:25:22 +0900 |
| parents | 7828beb7d849 |
| children | 91781b7c65a8 |
| 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 | |
| 17 | 13 |
| 14 | |
| 15 data PushDown ( Γ : Set ) : Set where | |
| 16 pop : PushDown Γ | |
| 17 push : Γ → PushDown Γ | |
| 275 | 18 none : PushDown Γ |
| 17 | 19 |
| 20 | |
| 21 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set ) | |
| 22 : Set where | |
| 23 field | |
| 275 | 24 pδ : Q → Σ → Γ → Q ∧ ( PushDown Γ ) |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
25 pok : Q → Bool |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
26 pempty : Γ |
| 275 | 27 pmoves : Q → List Γ → Σ → ( Q ∧ List Γ ) |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
28 pmoves q [] i with pδ q i pempty |
| 275 | 29 pmoves q [] i | ⟪ qn , pop ⟫ = ⟪ qn , [] ⟫ |
| 30 pmoves q [] i | ⟪ qn , push x ⟫ = ⟪ qn , ( x ∷ [] ) ⟫ | |
| 31 pmoves q [] i | ⟪ qn , none ⟫ = ⟪ qn , [] ⟫ | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
32 pmoves q ( H ∷ T ) i with pδ q i H |
| 275 | 33 pmoves q (H ∷ T) i | ⟪ qn , pop ⟫ = ⟪ qn , T ⟫ |
| 34 pmoves q (H ∷ T) i | ⟪ qn , none ⟫ = ⟪ qn , (H ∷ T) ⟫ | |
| 35 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
|
36 |
| 138 | 37 paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool |
| 38 paccept q [] [] = pok q | |
| 39 paccept q ( H ∷ T) [] with pδ q H pempty | |
| 275 | 40 paccept q (H ∷ T) [] | ⟪ qn , pop ⟫ = paccept qn T [] |
| 41 paccept q (H ∷ T) [] | ⟪ qn , none ⟫ = paccept qn T [] | |
| 42 paccept q (H ∷ T) [] | ⟪ qn , push x ⟫ = paccept qn T (x ∷ [] ) | |
| 138 | 43 paccept q [] (_ ∷ _ ) = false |
| 44 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH | |
| 275 | 45 ... | ⟪ nq , pop ⟫ = paccept nq T ST |
| 46 ... | ⟪ nq , none ⟫ = paccept nq T (SH ∷ ST) | |
| 47 ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns ∷ SH ∷ ST ) | |
| 138 | 48 |
| 17 | 49 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
50 data States0 : Set where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
51 sr : States0 |
| 17 | 52 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
53 data In2 : Set where |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
54 i0 : In2 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
55 i1 : In2 |
| 138 | 56 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
57 pnn : PushDownAutomaton States0 In2 States0 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
58 pnn = record { |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
59 pδ = pδ |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
60 ; pempty = sr |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
61 ; pok = λ q → true |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
62 } where |
| 275 | 63 pδ : States0 → In2 → States0 → States0 ∧ PushDown States0 |
| 64 pδ sr i0 _ = ⟪ sr , push sr ⟫ | |
| 65 pδ sr i1 _ = ⟪ sr , pop ⟫ | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
66 |
| 138 | 67 data States1 : Set where |
| 68 ss : States1 | |
| 69 st : States1 | |
| 70 | |
| 71 pn1 : PushDownAutomaton States1 In2 States1 | |
| 72 pn1 = record { | |
| 73 pδ = pδ | |
| 74 ; pempty = ss | |
| 75 ; pok = pok1 | |
| 76 } where | |
| 77 pok1 : States1 → Bool | |
| 78 pok1 ss = false | |
| 79 pok1 st = true | |
| 275 | 80 pδ : States1 → In2 → States1 → States1 ∧ PushDown States1 |
| 81 pδ ss i0 _ = ⟪ ss , push ss ⟫ | |
| 82 pδ ss i1 _ = ⟪ st , pop ⟫ | |
| 83 pδ st i0 _ = ⟪ st , push ss ⟫ | |
| 84 pδ st i1 _ = ⟪ st , pop ⟫ | |
| 138 | 85 |
| 86 test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] | |
| 87 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
|
88 test3 = PushDownAutomaton.pmoves pnn sr [] i0 |
| 138 | 89 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
|
90 |
| 138 | 91 test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] |
| 92 test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) [] | |
| 141 | 93 |