Mercurial > hg > Members > kono > Proof > automaton

annotate agda/nfa-list.agda @ 63:abfeed0c61b5

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