Mercurial > hg > Members > kono > Proof > automaton
annotate agda/sbconst.agda @ 99:aca3f1349913
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Nov 2019 21:30:04 +0900 |
| parents | 02b4ecc9972c |
| children |
| rev | line source |
|---|---|
| 8 | 1 module sbconst 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:
12
diff
changeset
|
5 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
6 open import Data.Maybe |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
7 open import Data.Product |
| 8 | 8 open import Data.Bool using ( Bool ; true ; false ; _∨_ ) |
| 9 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 10 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 11 | |
| 12 open import automaton | |
| 9 | 13 open import epautomaton |
| 8 | 14 |
| 10 | 15 |
| 16 -- all primitive state has id | |
| 17 -- Tree Q is sorted by id and is contents are unique | |
| 18 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
19 flatten : { Q : Set} → Tree Q → List ℕ |
| 8 | 20 flatten empty = [] |
| 21 flatten (leaf x x₁) = [ x ] | |
| 22 flatten (node x x₁ x₂ x₃) = flatten x₂ ++ [ x ] ++ flatten x₃ | |
| 23 | |
| 24 listEq : List ℕ → List ℕ → Bool | |
| 25 listEq [] [] = true | |
| 26 listEq [] ( _ ∷ _ ) = false | |
| 27 listEq ( _ ∷ _ ) [] = false | |
| 28 listEq ( h1 ∷ t1 ) ( h2 ∷ t2 ) with h1 ≟ h2 | |
| 29 ... | yes _ = listEq t1 t2 | |
| 30 ... | no _ = false | |
| 31 | |
| 32 infixr 7 _==_ | |
| 33 _==_ : { Q : Set} → Tree Q → Tree Q → Bool | |
| 34 x == y = listEq ( flatten x ) ( flatten y ) | |
| 35 | |
| 10 | 36 memberTT : { Q : Set} → Tree Q → Tree ( Tree Q ) → Bool |
| 8 | 37 memberTT t empty = false |
| 38 memberTT t (leaf x x₁) = t == x₁ | |
| 39 memberTT t (node x x₁ x₂ x₃) with t == x₁ | |
| 40 ... | true = true | |
| 41 ... | false = memberTT t x₂ ∨ memberTT t x₃ | |
| 42 | |
| 43 lengthT : { Q : Set} → Tree Q → ℕ | |
| 44 lengthT t = length ( flatten t ) | |
| 45 | |
| 9 | 46 findT : { Q : Set} → Tree Q → Tree ( Tree Q ) → Maybe ( Tree Q ) |
| 47 findT t empty = nothing | |
| 48 findT t (leaf x x₁) = just x₁ | |
| 49 findT t (node x x₁ x₂ x₃) with t == x₁ | |
| 50 ... | true = just x₁ | |
| 51 ... | false with findT t x₂ | |
| 52 ... | (just y) = just y | |
| 53 ... | nothing = findT t x₃ | |
| 54 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
55 mergeT : { Q : Set} → Tree Q → Tree Q → Tree Q |
| 10 | 56 mergeT empty t = t |
| 57 mergeT (leaf x t0) t = insertT x t0 t | |
| 58 mergeT (node x t0 left right ) t = | |
| 59 mergeT left ( insertT x t0 (mergeT right t )) | |
| 60 | |
| 8 | 61 open εAutomaton |
| 62 | |
| 10 | 63 -- all inputs are exclusive each other ( only one input can happen ) |
| 9 | 64 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
65 -- merge Tree ( Maybe Σ × Tree Q ) |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
66 merge-itεδ : { Σ Q : Set } → εAutomaton Q Σ → Σ → Tree Q → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q ) |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
67 merge-itεδ NFA i t empty = leaf (Σid NFA i) ( just i , t ) |
| 10 | 68 merge-itεδ NFA i t (leaf x (i' , t1 )) with (Σid NFA i) ≟ x |
| 69 ... | no _ = leaf x (i' , t1) | |
| 70 ... | yes _ = leaf x (just i , mergeT t t1 ) | |
| 71 merge-itεδ NFA i t (node x (i' , t1) left right ) with (Σid NFA i) ≟ x | |
| 72 ... | no _ = node x (i' , t1) ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right ) | |
| 73 ... | yes _ = node x (just i , mergeT t t1 ) | |
| 74 ( merge-itεδ NFA i t left ) ( merge-itεδ NFA i t right ) | |
| 75 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
76 merge-iεδ : { Σ Q : Set } → εAutomaton Q Σ → Maybe Σ → Tree Q → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q ) |
| 10 | 77 merge-iεδ NFA nothing _ t = t |
| 78 merge-iεδ NFA (just i) q t = merge-itεδ NFA i q t | |
| 79 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
80 merge-εδ : { Σ Q : Set } → εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q ) |
| 10 | 81 merge-εδ NFA empty t = t |
| 82 merge-εδ NFA (leaf x (i , t1) ) t = merge-iεδ NFA i t1 t | |
| 83 merge-εδ NFA (node x (i , t1) left right) t = | |
| 84 merge-εδ NFA left ( merge-iεδ NFA i t1 ( merge-εδ NFA right t ) ) | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
85 |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
86 -- merge and find new state from newly created Tree ( Maybe Σ × Tree Q ) |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
87 sbconst13 : { Σ Q : Set } → εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Tree Q ) → Tree ( Tree Q ) → ℕ → ( Tree ( Tree Q ) × Tree ( Tree Q ) × ℕ ) |
| 11 | 88 sbconst13 NFA empty nt t n = (nt , t , n) |
| 89 sbconst13 NFA (leaf x (p , q)) nt t n with memberTT q t | |
| 90 ... | true = ( nt , t , n) | |
| 12 | 91 ... | false = ( insertT n q nt , insertT n q t , n + 1 ) |
| 11 | 92 sbconst13 NFA (node x (_ , q) left right) nt t n with memberTT q t |
| 12 | 93 sbconst13 NFA (node x (_ , q) left right) nt t n | true = ( nt , t , n ) |
| 11 | 94 sbconst13 NFA (node x (_ , q) left right) nt t n | false = p2 |
| 9 | 95 where |
| 11 | 96 p1 = sbconst13 NFA left nt t n |
| 12 | 97 n1 = proj₂ ( proj₂ p1 ) |
| 98 p2 = sbconst13 NFA right (insertT n1 q ( proj₁ p1 )) (insertT n1 q ( proj₁ (proj₂ p1))) (n1 + 1 ) | |
| 11 | 99 -- expand state to Tree ( Maybe Σ × Tree Q ) |
| 100 sbconst12 : { Σ Q : Set } → εAutomaton Q Σ → Tree Q → Tree ( Maybe Σ × Tree Q ) → Tree ( Maybe Σ × Tree Q ) | |
| 101 sbconst12 NFA empty s = s | |
| 102 sbconst12 NFA (leaf x q) s = merge-εδ NFA s (all-εδ NFA q) | |
| 103 sbconst12 NFA (node x q left right) s = sbconst12 NFA right (merge-εδ NFA (all-εδ NFA q) (sbconst12 NFA left s)) | |
| 104 -- loop on state tree | |
| 12 | 105 sbconst11 : { Σ Q : Set } → εAutomaton Q Σ → Tree ( Tree Q ) → Tree ( Tree Q ) → Tree ( Tree Q ) → ℕ → ( Tree ( Tree Q ) × Tree ( Tree Q ) × ℕ ) |
| 106 sbconst11 NFA empty nt t n = (nt , t , n ) | |
| 107 sbconst11 NFA (leaf x q) nt t n = sbconst13 NFA (sbconst12 NFA q empty ) nt t n | |
| 108 sbconst11 NFA (node x q left right ) nt t n = p3 | |
| 9 | 109 where |
| 12 | 110 p1 = sbconst11 NFA left nt t n |
| 111 p2 = sbconst13 NFA (sbconst12 NFA q empty ) ( proj₁ p1 ) ( proj₁ ( proj₂ p1 ) ) ( proj₂ ( proj₂ p1 ) ) | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
112 p3 = sbconst11 NFA right ( proj₁ p2 ) ( proj₁ ( proj₂ p2 )) ( proj₂ ( proj₂ p2 )) |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
113 |
| 9 | 114 {-# TERMINATING #-} |
| 11 | 115 sbconst0 : { Σ Q : Set } → εAutomaton Q Σ → Tree ( Tree Q ) → Tree ( Tree Q ) → ℕ → ( Tree ( Tree Q ) × ℕ ) |
| 12 | 116 sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 empty n0 |
| 11 | 117 ... | t2 , empty , n = (t2 , n ) |
| 12 | 118 ... | t2 , leaf x y , n = sbconst0 NFA ( proj₁ ( proj₂ p1 )) (leaf x y) ( proj₂ ( proj₂ p1 ) ) |
| 9 | 119 where |
| 12 | 120 p1 = sbconst11 NFA (leaf x y) t1 empty n |
| 121 ... | t2 , node x y left right , n = p4 | |
| 9 | 122 where |
| 123 p1 = sbconst0 NFA left t2 n | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
124 p2 = sbconst11 NFA (leaf x y) ( proj₁ p1 ) empty ( proj₂ p1 ) |
| 12 | 125 p3 = sbconst0 NFA right ( proj₁ p2 ) ( proj₂ ( proj₂ p2 )) |
| 126 p4 = sbconst0 NFA ( proj₁ ( proj₂ p2 )) ( proj₁ p3) ( proj₂ p3 ) | |
| 9 | 127 |
| 128 nfa2dfa : { Σ Q : Set } → εAutomaton Q Σ → Automaton (Tree Q) Σ | |
| 8 | 129 nfa2dfa {Σ} {Q} NFA = record { |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
130 δ = δ' |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
131 ; astart = astart' |
| 8 | 132 ; aend = aend' |
| 133 } | |
| 134 where | |
| 9 | 135 MTree : { Σ Q : Set } → (x : εAutomaton Q Σ) → Tree ( Tree Q ) |
| 136 MTree {Σ} {Q} NFA = εclosure (allState NFA ) ( εδ NFA ) | |
| 137 sbconst : { Σ Q : Set } → εAutomaton Q Σ → Tree ( Tree Q ) | |
| 11 | 138 sbconst NFA = proj₁ (sbconst0 NFA ( MTree NFA ) (MTree NFA) zero) |
| 12 | 139 δ0 : Σ → Tree ( Maybe Σ × Tree Q ) → Tree Q |
| 140 δ0 x empty = empty | |
| 141 δ0 x (leaf x₁ q) with Σid NFA x ≟ x₁ | |
| 142 ... | no ¬p = empty | |
| 143 ... | yes p with proj₁ q | |
| 144 ... | nothing = empty | |
| 145 ... | just _ = proj₂ q | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
146 δ0 x (node x₁ q left right) with Σid NFA x ≟ x₁ |
| 12 | 147 ... | no ¬p with δ0 x left |
| 148 ... | empty = δ0 x right | |
| 149 ... | q1 = q1 | |
| 150 δ0 x (node x₁ q left right) | yes p with proj₁ q | |
| 151 ... | nothing = empty | |
| 152 ... | just _ = proj₂ q | |
| 9 | 153 δ' : Tree Q → Σ → Tree Q |
| 154 δ' t x with findT t ( MTree NFA ) | |
| 155 ... | nothing = leaf zero ( εstart NFA ) -- can't happen | |
| 12 | 156 ... | just q = δ0 x (sbconst12 NFA q empty) |
| 9 | 157 astart' : Tree Q |
| 158 astart' = leaf zero ( εstart NFA ) | |
| 159 aend' : Tree Q → Bool | |
| 160 aend' empty = false | |
| 161 aend' (leaf _ x) = εend NFA x | |
| 162 aend' (node _ x left right ) = | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
12
diff
changeset
|
163 aend' left ∨ εend NFA x ∨ aend' right |
| 8 | 164 |