Mercurial > hg > Members > kono > Proof > automaton

changeset 35:95f2e129cf9e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 07 Nov 2018 14:46:54 +0900
parents a904b6bc76af
children 9558d870e8ae
files agda/nfa.agda agda/regex1.agda
diffstat 2 files changed, 47 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/agda/nfa.agda	Tue Nov 06 12:50:11 2018 +0900
+++ b/agda/nfa.agda	Wed Nov 07 14:46:54 2018 +0900
@@ -140,3 +140,7 @@
 
 test2 = Nmoves am2 finState1 start1 
 
+test4 : Fin 2 → Bool
+test4 zero = {!!}
+test4 (suc zero) = {!!}
+test4 (suc (suc ()))
--- a/agda/regex1.agda	Tue Nov 06 12:50:11 2018 +0900
+++ b/agda/regex1.agda	Wed Nov 07 14:46:54 2018 +0900
@@ -77,16 +77,50 @@
 test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
 test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
 
-regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } {fin : FiniteSet Σ {n}} → NAutomaton (Regex Σ) Σ
-regex2nfa {Σ} r {n} {fin} = record {
-          Nδ     = Nδ
-      ;   Nstart = Nstart
-      ;   Nend   = Nend
-  } where
+regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ
+regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
+          nr0 = regex2nfa r fin
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0
+          Nend : (Regex Σ) → Bool
+          Nend s0 =  NAutomaton.Nend nr0 s0
+regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
+          nr0 = regex2nfa r0 fin
+          nr1 = regex2nfa r1 fin
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
+          Nend : (Regex Σ) → Bool
+          Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
+regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
+          nr0 = regex2nfa r0 fin 
+          nr1 = regex2nfa r1 fin
           Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ = {!!}
+          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
+          Nstart : (Regex Σ) → Bool
+          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
+          Nend : (Regex Σ) → Bool
+          Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
+regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
+          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
+          Nδ r1 s r2 with cmpi fin s x
+          Nδ r1 s r2 | yes _ = true
+          Nδ r1 s r2 | no _ = false
           Nstart : (Regex Σ) → Bool
-          Nstart = {!!}
+          Nstart < s > with cmpi fin s x
+          ... | yes _ = true
+          ... | no  _ = false
+          Nstart _ = false
           Nend  :  (Regex Σ) → Bool
-          Nend  = {!!}
+          Nend  _ = false
+
+test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 
 
+testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )
+
+
+
+