Mercurial > hg > Members > kono > Proof > automaton

comparison agda/derive.agda @ 45:e9edc777dc03

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix derive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Dec 2018 15:48:05 +0900
parents aa15eff1aeb3
children 7a0634a7c25a
comparison
equal deleted inserted replaced
44:aa15eff1aeb3 45:e9edc777dc03
33 finiso←' zero = refl 33 finiso←' zero = refl
34 finiso←' (suc zero) = refl 34 finiso←' (suc zero) = refl
35 finiso←' (suc (suc ())) 35 finiso←' (suc (suc ()))
36 36
37 37
38 test-r1 = < i0 > & < i1 > 38 tr1 = < i0 > & < i1 >
39 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] ) 39 tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] )
40 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] ) 40 tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] )
41 tr4 = (< i0 > * ) & < i1 >
42 tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) *
41 43
42 issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool 44 sb : { Σ : Set } → Regex Σ → List ( Regex Σ )
43 issub (r *) s f = issub r s f 45 sb (x *) = map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x )
44 issub (r & r₁) s f = issub r s f ∨ issub r₁ s f 46 sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y )
45 issub (r || r₁) s f = issub r s f ∨ issub r₁ s f 47 sb (x || y) = sb x ++ sb y
46 issub < x > < s > f with cmpi f x s 48 sb < x > = < x > ∷ []
47 issub < x > < s > f | yes p = true
48 issub < x > < s > f | no ¬p = false
49 issub < x > s f = false
50
51 record RegexSub {Σ : Set} (R : Regex Σ) {n : ℕ } (fin : FiniteSet Σ {n} ): Set where
52 field
53 Subterm : Regex Σ
54 sub : issub R Subterm fin ≡ true
55
56 open import Data.Product
57 49
58 50
59 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 51 nth : { S : Set } → (x : List S ) → Fin ( length x ) → S
60 regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where 52 nth [] ()
61 nr0 = proj₁ (regex2nfa r fin) 53 nth (s ∷ t) zero = s
62 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool 54 nth (_ ∷ t) (suc f) = nth t f
63 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
64 Nstart : (Regex Σ) → Bool
65 Nstart s0 = NAutomaton.Nstart nr0 s0
66 Nend : (Regex Σ) → Bool
67 Nend s0 = NAutomaton.Nend nr0 s0
68 regex2nfa {Σ} (r0 & r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where
69 nr0 = proj₁ (regex2nfa r0 fin)
70 nr1 = proj₁ (regex2nfa r1 fin)
71 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
72 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr1 s0 i s1 )
73 Nstart : (Regex Σ) → Bool
74 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
75 Nend : (Regex Σ) → Bool
76 Nend s0 = NAutomaton.Nend nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
77 regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where
78 nr0 = proj₁ (regex2nfa r0 fin)
79 nr1 = proj₁ (regex2nfa r1 fin)
80 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
81 Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
82 Nstart : (Regex Σ) → Bool
83 Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ NAutomaton.Nstart nr1 s0
84 Nend : (Regex Σ) → Bool
85 Nend s0 = NAutomaton.Nend nr0 s0 ∨ NAutomaton.Nend nr1 s0
86 regex2nfa {Σ} < x > fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } , {!!} where
87 Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
88 Nδ r1 s r2 with cmpi fin s x
89 Nδ r1 s r2 | yes _ = true
90 Nδ r1 s r2 | no _ = false
91 Nstart : (Regex Σ) → Bool
92 Nstart = {!!}
93 Nstart < s > with cmpi fin s x
94 ... | yes _ = true
95 ... | no _ = false
96 Nstart _ = false
97 Nend : (Regex Σ) → Bool
98 Nend _ = false
99
100 test-r4 = regex2nfa (< i0 > & < i1 >) finIn2
101
102 testr5 = Naccept ( proj₁ test-r4) {!!} ( i0 ∷ i1 ∷ [] )
103
104 rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s }
105 rfin {Σ} s = record {
106 Q←F = Q←F'
107 ; F←Q = F←Q'
108 ; finiso→ = finiso→'
109 ; finiso← = finiso←'
110 } where
111 Q←F' : Fin (length s) → Regex Σ
112 Q←F' = {!!}
113 F←Q' : Regex Σ → Fin (length s)
114 F←Q' = {!!}
115 finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
116 finiso→' = {!!}
117 finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
118 finiso←' = {!!}
119
120 reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n})
121 → ( regex : Regex Σ )
122 → ( In : List Σ )
123 → regular-language regex fin In ≡ Naccept {Regex Σ} {_} ( proj₁ ( regex2nfa {Σ} regex fin ))
124 (rfin (proj₂ ( regex2nfa {Σ} regex fin ) )) In
125 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
126 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
127 reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
128 reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}
129
130
131 derivatives : {Σ : Set} → Σ → Regex Σ → Regex Σ
132 derivatives x (r *) = {!!}
133 derivatives x (r & r₁) = {!!}
134 derivatives x (r || r₁) = {!!}
135 derivatives x < x₁ > = {!!}
136
137 daccept : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ ) → Bool
138 daccept r fin [] = {!!}
139 daccept r fin (h ∷ t) = regular-language ( derivatives h r ) fin t
140
141 lemma1 : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ )
142 → regular-language r fin s ≡ true → daccept r fin s ≡ true
143 lemma1 = {!!}
144
145 lemma2 : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ )
146 → daccept r fin s ≡ true → regular-language r fin s ≡ true
147 lemma2 = {!!}
148
149
150