diff agda/regex.agda @ 2:e4d298d26820

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 00:18:38 +0900 (2018-08-14)
parents 3c6de7cf2a95
children 3ac6311293ec
line wrap: on
line diff
--- a/agda/regex.agda	Tue Aug 14 21:44:12 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 00:18:38 2018 +0900
@@ -5,7 +5,7 @@
 open import Data.Nat
 open import Data.List 
 open import Data.Bool using ( Bool ; true ; false )
-open import  Relation.Binary.PropositionalEquality
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 
@@ -28,7 +28,7 @@
    inductive
    field
       state :  ℕ
-      move  :  Σ → List (RST Σ)
+      move  :  Σ → List ℕ
       RSTend : Bool
 
 open RST
@@ -36,24 +36,54 @@
 record RNFA ( Σ : Set )
      : Set where
    field
-      eqRST? :  (q q' : RST Σ) → Dec (q ≡ q')
-      start :  RST Σ
-      end   :  RST Σ → Bool
+      states : List ( RST Σ )
+   map1  : ( List ( RST Σ ) ) → ℕ →  RST Σ 
+   map1 [] _ ()
+   map1 ( h ∷ t ) 0 = h
+   map1 ( h ∷ t ) (suc n) = map1 t n
+   map   :  ℕ →  RST Σ 
+   map n =  map1 n states
+   start :  RST Σ
+   start = map 3
 
 open RNFA
 
-generateRNFA :  { Σ : Set  } →  ( Regex  Σ ) →  RNFA  Σ
-generateRNFA  {Σ} regex = record {
-          eqRST? = eqRST
-       ;  start = {!!}
+generateRNFA :  { Σ : Set  } → ( (q q' : Σ) → Dec ( q ≡  q' ))  →  ( Regex  Σ ) →  RNFA  Σ
+generateRNFA  {Σ} _≟_ regex = record {
+          start = generate regex true 2
+              [ record { state = 0 ; move = λ q → [] ; RSTend = true } ]
+              [ record { state = 1 ; move = λ q → [] ; RSTend = false } ]
        ;  end = λ s → RSTend s
     } where
-       eqRST :  (q q' : RST Σ) → Dec (q ≡ q')
-       eqRST q q' with  (state q)  ≟  (state q')
-       ... | yes eq = {!!}
-       ... | no neq = {!!}
+  listcase :  Σ →  List Σ → List ( RST  Σ ) → List ( RST  Σ ) → List ( RST  Σ )
+  listcase q [] ok else = else
+  listcase q ( q'  ∷ t )  ok else with q ≟  q'
+  ... | yes _ = ok
+  ... | no _ = listcase q t ok else
+  generate : ( Regex  Σ ) → Bool → ℕ  → List ( RST  Σ ) → List ( RST  Σ ) → ( RST  Σ )
+  generate (x *) end n next else = loop
+     where 
+       loop : RST  Σ
+       repeat : RST  Σ
+       loop = generate x end (n + 1) [ repeat ] else
+       repeat = record {
+               state = n
+             ; move = {!!}
+             ; RSTend = end
+            } 
+  generate (x & y) end n next else = {!!}
+  generate (x || y) end n next else = {!!}
+  generate < x > end n next else = record {
+       state = n
+     ; move = λ q → listcase q x end else
+     ; RSTend = false
+    }  
 
 
 regex2nfa :  (regex : Regex In2 ) → NAutomaton (RST In2) In2 
-regex2nfa regex = record {  nδ = λ s i → move s i ; n≟ = {!!} ; nstart = {!!} ;  nend = {!!} }
+regex2nfa regex = record {
+      nδ = λ s i → move s i
+    ; sid = λ s → state s
+    ; nstart =  start ( generateRNFA ieq regex )
+    ; nend = λ s → RSTend s }