Mercurial > hg > Members > kono > Proof > automaton
annotate agda/nfa-list.agda @ 24:9406c2571fe7
naccept1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Nov 2018 07:53:48 +0900 |
| parents | agda/automaton.agda@02b4ecc9972c |
| children | aa15eff1aeb3 |
| rev | line source |
|---|---|
| 24 | 1 module nfa-list where |
| 0 | 2 |
| 3 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 2 | 4 open import Data.Nat |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
5 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
6 open import Data.Maybe |
| 0 | 7 open import Data.Bool using ( Bool ; true ; false ) |
| 3 | 8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 9 | 9 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 0 | 10 |
| 11 | |
| 12 data States1 : Set where | |
| 1 | 13 sr : States1 |
| 14 ss : States1 | |
| 15 st : States1 | |
| 0 | 16 |
| 17 data In2 : Set where | |
| 18 i0 : In2 | |
| 19 i1 : In2 | |
| 20 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
21 transition1 : States1 → In2 → States1 |
| 1 | 22 transition1 sr i0 = sr |
| 23 transition1 sr i1 = ss | |
| 24 transition1 ss i0 = sr | |
| 25 transition1 ss i1 = st | |
| 26 transition1 st i0 = sr | |
| 27 transition1 st i1 = st | |
| 0 | 28 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
29 fin1 : States1 → Bool |
| 1 | 30 fin1 st = true |
| 0 | 31 fin1 _ = false |
| 32 | |
| 2 | 33 s1id : States1 → ℕ |
| 34 s1id sr = 0 | |
| 35 s1id ss = 1 | |
| 36 s1id st = 2 | |
| 0 | 37 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
38 record NAutomaton ( Q : Set ) ( Σ : Set ) |
| 0 | 39 : Set where |
| 1 | 40 field |
| 41 nδ : Q → Σ → List Q | |
| 2 | 42 sid : Q → ℕ |
| 1 | 43 nstart : Q |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
44 nend : Q → Bool |
| 1 | 45 |
| 46 open NAutomaton | |
| 0 | 47 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
48 insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q |
| 2 | 49 insert M [] q = q ∷ [] |
| 50 insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') | |
| 51 ... | yes _ = insert M T q' | |
| 52 ... | no _ = q ∷ (insert M T q' ) | |
| 0 | 53 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
54 merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q |
| 2 | 55 merge M L1 [] = L1 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
56 merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H |
| 0 | 57 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
58 Nmoves : { Q : Set } { Σ : Set } |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
59 → NAutomaton Q Σ |
| 0 | 60 → List Q → List Σ → List Q |
| 1 | 61 Nmoves {Q} { Σ} M q L = Nmoves1 q L [] |
| 0 | 62 where |
| 63 Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q | |
| 64 Nmoves1 q [] _ = q | |
| 65 Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] | |
| 2 | 66 Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) |
| 0 | 67 |
| 68 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
69 Naccept : { Q : Set } { Σ : Set } |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
70 → NAutomaton Q Σ |
| 0 | 71 → List Σ → Bool |
| 1 | 72 Naccept {Q} { Σ} M L = |
| 73 checkAccept ( Nmoves M ((nstart M) ∷ [] ) L ) | |
| 0 | 74 where |
| 75 checkAccept : (q : List Q ) → Bool | |
| 76 checkAccept [] = false | |
| 1 | 77 checkAccept ( H ∷ L ) with (nend M) H |
| 0 | 78 ... | true = true |
| 79 ... | false = checkAccept L | |
| 80 | |
| 81 | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
82 transition2 : States1 → In2 → List States1 |
| 1 | 83 transition2 sr i0 = (sr ∷ []) |
| 84 transition2 sr i1 = (ss ∷ sr ∷ [] ) | |
| 85 transition2 ss i0 = (sr ∷ []) | |
| 86 transition2 ss i1 = (st ∷ []) | |
| 87 transition2 st i0 = (sr ∷ []) | |
| 88 transition2 st i1 = (st ∷ []) | |
| 0 | 89 |
| 1 | 90 am2 : NAutomaton States1 In2 |
| 2 | 91 am2 = record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1} |
| 0 | 92 |
| 93 | |
| 94 example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] ) | |
| 95 example2-2 = Naccept am2 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 96 |