Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/pushdown.agda @ 318:91781b7c65a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jan 2022 07:27:52 +0900
parents 7828beb7d849
children 6f3636fbc481
comparison
equal deleted inserted replaced
317:16e47a3c4eda 318:91781b7c65a8
8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Nullary using (¬_; Dec; yes; no) 9 open import Relation.Nullary using (¬_; Dec; yes; no)
10 open import Level renaming ( suc to succ ; zero to Zero ) 10 open import Level renaming ( suc to succ ; zero to Zero )
11 -- open import Data.Product 11 -- open import Data.Product
12 open import logic 12 open import logic
13 open import automaton
13 14
14 15
15 data PushDown ( Γ : Set ) : Set where 16 data PushDown ( Γ : Set ) : Set where
16 pop : PushDown Γ 17 pop : PushDown Γ
17 push : Γ → PushDown Γ 18 push : Γ → PushDown Γ
44 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH 45 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
45 ... | ⟪ nq , pop ⟫ = paccept nq T ST 46 ... | ⟪ nq , pop ⟫ = paccept nq T ST
46 ... | ⟪ nq , none ⟫ = paccept nq T (SH ∷ ST) 47 ... | ⟪ nq , none ⟫ = paccept nq T (SH ∷ ST)
47 ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns ∷ SH ∷ ST ) 48 ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns ∷ SH ∷ ST )
48 49
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 )
49 67
50 data States0 : Set where 68 data States0 : Set where
51 sr : States0 69 sr : States0
52 70
53 data In2 : Set where 71 data In2 : Set where
62 } where 80 } where
63 pδ : States0 → In2 → States0 → States0 ∧ PushDown States0 81 pδ : States0 → In2 → States0 → States0 ∧ PushDown States0
64 pδ sr i0 _ = ⟪ sr , push sr ⟫ 82 pδ sr i0 _ = ⟪ sr , push sr ⟫
65 pδ sr i1 _ = ⟪ sr , pop ⟫ 83 pδ sr i1 _ = ⟪ sr , pop ⟫
66 84
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
67 data States1 : Set where 108 data States1 : Set where
68 ss : States1 109 ss : States1
69 st : States1 110 st : States1
70
71 pn1 : PushDownAutomaton States1 In2 States1 111 pn1 : PushDownAutomaton States1 In2 States1
72 pn1 = record { 112 pn1 = record {
73 pδ = pδ 113 pδ = pδ
74 ; pempty = ss 114 ; pempty = ss
75 ; pok = pok1 115 ; pok = pok1