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