# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1605505156 -32400
# Node ID 2e589115f7c956262c8baa790b60c85d1766360c
# Parent  6f1fb2fa9a31db82e8da19c456e3a418a378af52
RexResult

diff -r 6f1fb2fa9a31 -r 2e589115f7c9 regex.agda
--- a/regex.agda	Mon Nov 16 13:54:31 2020 +0900
+++ b/regex.agda	Mon Nov 16 14:39:16 2020 +0900
@@ -50,63 +50,64 @@
 
 open import regular-language
 
--- match : {Σ : Set} → (r : Regex Σ ) → Automaton (Regex Σ) Σ
-
 -- open import Data.Nat.DivMod
 
 -- test-regex-even : Set
 -- test-regex-even = (s : List char ) → regular-expr ( ( any & any ) * )  s  → (length s) mod 2 ≡ zero
 
-empty? : {Σ : Set} →  Regex Σ → Maybe (Regex Σ)
-empty? (r *) = just (r *)
+empty? : {Σ : Set} →  Regex Σ → Bool
+empty? (r *) = true
 empty? (r & s) with empty? r
-... | nothing = nothing
-... | just _ = empty? s
+... | false = false
+... | true  = empty? s
 empty? (r || s) with empty? r | empty? s
-... | nothing | nothing = nothing
-... | just r1 | _ = just r1
-... | _ | just s1 = just s1
-empty? < x > = nothing
+... | false | false = false
+... | true | _ = true
+... | _ | true = true
+empty? < x > = false
 
-derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Maybe (Maybe (Regex Σ))
+data RexResult {Σ : Set}  : Set where
+   fail     : RexResult
+   finish   : RexResult
+   continue : (Regex Σ) → RexResult
+
+derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → RexResult
 derivative (r *) x dec  with derivative r x dec 
-... | just (just r1) = just (just (r1 & (r *)))
-... | just nothing = just (just (r *))
-... | nothing = nothing
+... | continue r1 = continue (r1 & (r *))
+... | finish = continue (r *)
+... | fail = fail
 derivative (r & s) x dec  with derivative r x dec | derivative s x dec | empty? r
-... | nothing | _ | _ = nothing
-... | just nothing | nothing | _ = just (just s)
-... | just nothing | just nothing  | _ = just (just s)
-... | just nothing | just (just s1)  | nothing = just (just s)
-... | just nothing | just (just s1)  | just _ = just (just (s1 || s))
-... | just (just r1) | _ | nothing = just (just (r1 & s))
-... | just (just r1) | just (just s1)  | just _  = just (just (s1 || (r1 & s)))
-... | just (just r1) | _ | just _  = just (just (r1 & s))
+... | fail        | _            | _     = fail
+... | finish      | continue s1  | true  = continue (s1 || s)
+... | finish      | _            | _     = continue s
+... | continue r1 | continue s1  | true  = continue (s1 || (r1 & s))
+... | continue r1 | _            | _     = continue (r1 & s)
 derivative (r || s) x dec  with derivative r x dec  | derivative s x dec 
-... | just (just r1) | just (just s1) = just (just ( r1 || s1 ) )
-... | just nothing | _ = just nothing
-... | _ | just nothing = just nothing
-... | just (just r1) | _ = just (just r1)
-... | _ | just (just s1) = just (just s1)
-... | nothing | nothing = nothing
+... | continue r1 | continue s1 = continue ( r1 || s1 ) 
+... | fail        | p           = p
+... | p           | fail        = p
+... | finish      | _           = finish
+... | _           | finish      = finish
 derivative < i > x dec  with dec i x
-... | yes y = just nothing
-... | no _ = nothing
+... | yes y = finish
+... | no _  = fail
 
 open import automaton
 
-regex→automaton :  {Σ : Set} →  Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton (Maybe (Maybe (Regex Σ))) Σ
+regex→automaton :  {Σ : Set} →  Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton RexResult Σ
 regex→automaton {Σ} r dec = record {
       δ = δ
     ; F = F
    } where
-      δ : Maybe (Maybe (Regex Σ)) → Σ → Maybe (Maybe (Regex Σ))
-      δ nothing i = nothing
-      δ (just nothing) i = nothing
-      δ (just (just r)) i = derivative r i dec 
-      F : Maybe (Maybe (Regex Σ)) → Set
-      F (just (just (r *))) = ⊤
-      F (just nothing) = ⊤
+      δ : RexResult → Σ → RexResult
+      δ fail i = fail
+      δ finish i = fail
+      δ (continue r) i = derivative r i dec 
+      F : RexResult  → Set
+      F (continue r) with empty? r
+      ... | true  = ⊤
+      ... | false = ⊥
+      F finish = ⊤
       F _ = ⊥
 
 char-dec : (i j : char) → Dec (i ≡ j)
@@ -130,29 +131,49 @@
 char-list : List char
 char-list = a ∷ b ∷ c ∷ d ∷ []
 
-a2 : accept (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] )
+open Automaton 
+
+a2 : accept (regex→automaton r2 char-dec ) (continue r2) ( a ∷ a ∷ b ∷ c ∷ [] )
 a2 = tt
-tr2 = trace (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] ) a2
+tr2 = trace (regex→automaton r2 char-dec ) (continue r2) ( a ∷ a ∷ b ∷ c ∷ [] ) a2
 
-a1  : accept (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] )
+a1  : accept (regex→automaton < a > char-dec ) (continue < a > ) ( a ∷ [] )
 a1  = tt
-tr1 = trace (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] ) a1
+tr1 = trace (regex→automaton < a > char-dec ) (continue < a > ) ( a ∷ [] ) a1
 
-a3  = accept (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
-tr3  = trace (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
+a3  : accept (regex→automaton < a > char-dec ) (continue (< a > & < b > )) ( a ∷ b ∷ [] )
+a3  = tt
+tr3  = trace (regex→automaton < a > char-dec ) (continue (< a > & < b > )) ( a ∷ b ∷ [] )
 
 
 regex→accept :  {Σ : Set} →  (r : Regex Σ ) → (x : List Σ)  → (dec : (i j : Σ ) → Dec ( i ≡ j ))
-   → accept (regex→automaton r dec) (just (just r)) x → regular-expr r x
+   → accept (regex→automaton r dec) (continue r) x → regular-expr r x
 regex→accept r x dec ac = {!!}
 
 regex←accept :  {Σ : Set} →  (r : Regex Σ ) → (x : List Σ)  → (dec : (i j : Σ ) → Dec ( i ≡ j ))
-   → regular-expr r x → accept (regex→automaton r dec) (just (just r)) x 
+   → regular-expr r x → accept (regex→automaton r dec) (continue r) x 
 regex←accept r x dec re = {!!} 
 
 
 
+-- charRE-dec : (x y : Regex char) → Dec (x ≡ y)
+-- charRE-dec (x *) (y *) with charRE-dec x y
+-- ... | yes refl = yes refl
+-- ... | no n = no {!!}
+-- charRE-dec (x *) (_ & _) = no (λ ())
+-- charRE-dec (x *) (_ || _) = no (λ ())
+-- charRE-dec (x *) < _ > = no (λ ())
+-- charRE-dec (x & x1) (y & y1) with charRE-dec x y | charRE-dec x1 y1
+-- ... | yes refl | yes refl = yes refl
+-- ... | no n | _ = no {!!}
+-- ... |  _ | no n = no {!!}
+-- charRE-dec (x & x1) (y *) = no (λ ())
+-- charRE-dec (x & x1) (_ || _) = no (λ ())
+-- charRE-dec (x & x1) < _ > = no (λ ())
+-- charRE-dec (x || x₁) y = {!!}
+-- charRE-dec < x > y = {!!}
+
+
+
 
 
-
-