Mercurial > hg > Members > kono > Proof > automaton
annotate agda/epautomaton.agda @ 139:3be1afb87f82
add utm
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Mar 2020 17:34:54 +0900 |
| parents | a904b6bc76af |
| children |
| rev | line source |
|---|---|
| 9 | 1 module epautomaton where |
| 2 | |
| 3 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 4 open import Data.Nat | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
5 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
6 open import Data.Maybe |
| 9 | 7 open import Data.Bool using ( Bool ; true ; false ) |
| 8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 9 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 10 | |
| 11 open import automaton | |
| 34 | 12 open import nfa-list |
| 9 | 13 |
| 14 nth : {S : Set } → ℕ → List S → Maybe S | |
| 15 nth _ [] = nothing | |
| 16 nth 0 ( x ∷ _ ) = just x | |
| 17 nth (suc n) ( _ ∷ t ) = nth n t | |
| 18 | |
| 19 member : ℕ → List ℕ → Bool | |
| 20 member _ [] = false | |
| 21 member n ( x ∷ t ) with n ≟ x | |
| 22 ... | yes _ = true | |
| 23 ... | no _ = member n t | |
| 24 | |
| 25 | |
| 26 data STree (S E : Set ) : Set where | |
| 27 empty : STree S E | |
| 28 leaf : S → E → STree S E | |
| 29 node : S → E → STree S E → STree S E → STree S E | |
| 30 | |
| 31 Tree : Set → Set | |
| 32 Tree E = STree ℕ E | |
| 33 | |
| 34 insertT : {E : Set} → ℕ → E → Tree E → Tree E | |
| 35 insertT {E} n e empty = leaf n e | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
36 insertT {E} n e (leaf n1 e1 ) with n ≟ n1 | n ≤? n1 |
| 9 | 37 ... | yes _ | _ = leaf n e |
| 38 ... | no _ | yes _ = node n e ( leaf n1 e1 ) empty | |
| 39 ... | no _ | no _ = node n e empty ( leaf n1 e1 ) | |
| 40 insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1 | |
| 41 ... | yes _ | _ = node n e left right | |
| 42 ... | no _ | yes _ = node n1 e1 ( insertT n e left ) right | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
43 ... | no _ | no _ = node n1 e1 left ( insertT n e right ) |
| 9 | 44 |
| 45 memberT : {E : Set } → ℕ → Tree E → Maybe E | |
| 46 memberT _ empty = nothing | |
| 47 memberT n (leaf n1 e) with n ≟ n1 | |
| 48 ... | yes _ = just e | |
| 49 ... | no _ = nothing | |
| 50 memberT n (node n1 e1 left right) with n ≟ n1 | n ≤? n1 | |
| 51 ... | yes _ | _ = just e1 | |
| 52 memberT n (node n1 e1 left right) | no ¬p | (yes p) = memberT n left | |
| 53 memberT n (node n1 e1 left right) | no ¬p | (no ¬p₁) = memberT n right | |
| 54 | |
| 55 open import Data.Product | |
| 56 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
57 record εAutomaton ( Q : Set ) ( Σ : Set ) |
| 9 | 58 : Set where |
| 59 field | |
| 60 εδ : Q → Maybe Σ → Tree Q | |
| 61 all-εδ : Q → Tree ( Maybe Σ × Tree Q ) | |
| 62 εid : Q → ℕ | |
| 10 | 63 Σid : Σ → ℕ |
| 9 | 64 allState : Tree Q |
| 65 εstart : Q | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
66 εend : Q → Bool |
| 9 | 67 |
| 68 open εAutomaton | |
| 69 | |
| 70 -- | |
| 71 -- find ε connected state by following ε transition | |
| 72 -- keep track state list in C | |
| 73 -- if already tracked, skip it | |
| 74 εclosure : { Q : Set } { Σ : Set } | |
| 75 → ( allState : Tree Q ) | |
| 76 → ( εδ : Q → Maybe Σ → Tree Q ) | |
| 77 → Tree ( Tree Q ) | |
| 78 εclosure {Q} { Σ} allState εδ = closure ( allState ) | |
| 79 where | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
80 closure2 : Tree Q → Tree Q → Tree Q |
| 9 | 81 closure2 empty C = C |
| 82 closure2 ( leaf n1 q ) C with memberT n1 C | |
| 83 ... | just _ = C | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
84 ... | nothing = insertT n1 q C |
| 9 | 85 closure2 ( node n1 q left right ) C with memberT n1 C |
| 86 ... | just _ = closure2 left ( closure2 right C ) | |
| 87 ... | nothing = insertT n1 q (closure2 left ( closure2 right C )) | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
88 closure1 : ℕ → Tree Q |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
89 closure1 n with memberT n (allState ) |
| 9 | 90 ... | nothing = empty |
| 91 ... | just q = closure2 (εδ q nothing) ( leaf n q ) | |
| 92 closure : Tree Q → Tree ( Tree Q ) | |
| 93 closure empty = empty | |
| 94 closure (leaf n e) = (leaf n (closure1 n) ) | |
| 95 closure (node n e left right) = | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
10
diff
changeset
|
96 node n (closure1 n) ( closure left ) ( closure right ) |
| 9 | 97 |
| 10 | 98 |
| 9 | 99 εAutomaton2U : { Q : Set } { Σ : Set } |
| 100 → εAutomaton Q Σ → NAutomaton Q Σ | |
| 101 εAutomaton2U {Q} { Σ} M = record { | |
| 102 nδ = nδ' ; | |
| 103 sid = εid M ; | |
| 104 nstart = εstart M ; | |
| 105 nend = εend M | |
| 106 } where | |
| 107 MTree : Tree ( Tree Q ) | |
| 108 MTree = εclosure (allState M ) ( εδ M ) | |
| 10 | 109 flatten : Tree Q → List Q |
| 110 flatten empty = [] | |
| 111 flatten (leaf x q) = [ q ] | |
| 112 flatten (node x q left right) = flatten left ++ [ q ] ++ flatten right | |
| 9 | 113 nδ1 : Tree Q → Σ → List Q |
| 114 nδ1 empty i = [] | |
| 10 | 115 nδ1 (leaf n q) i = flatten (εδ M q (just i)) |
| 116 nδ1 (node n q left right) i = nδ1 left i ++ ( flatten (εδ M q (just i) )) ++ nδ1 right i | |
| 9 | 117 nδ' : Q → Σ → List Q |
| 118 nδ' q i with memberT ( εid M q ) MTree | |
| 119 ... | nothing = [] | |
| 120 ... | just x = nδ1 x i | |
| 121 |