# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1605502471 -32400
# Node ID 6f1fb2fa9a31db82e8da19c456e3a418a378af52
# Parent  c3fa431262fa152efd735e7a56415609d7976abe
derivative

diff -r c3fa431262fa -r 6f1fb2fa9a31 regex.agda
--- a/regex.agda	Mon Nov 16 13:11:26 2020 +0900
+++ b/regex.agda	Mon Nov 16 13:54:31 2020 +0900
@@ -40,7 +40,7 @@
    concat : {x y : Regex Σ} {t s : List Σ} →  regular-expr x t →  regular-expr y s →  regular-expr (x & y) (t ++ s )
    select : {x y : Regex Σ} {t : List Σ} →  regular-expr x t ∨  regular-expr y t →  regular-expr (x || y) t
    star-nil : {x : Regex Σ}  →  regular-expr (x *) []
-   star : {x : Regex Σ}  → {lx next : List Σ} →  regular-expr x lx → regular-expr (x *) next →  regular-expr (x *) next
+   star : {x : Regex Σ}  → {lx next : List Σ} →  regular-expr x lx → regular-expr (x *) next →  regular-expr (x *) (lx ++ next)
 
 test-regex : Set
 test-regex = ¬ (regular-expr r1 ( a ∷ [] ) )
@@ -71,16 +71,17 @@
 derivative : {Σ : Set} →  Regex Σ → Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Maybe (Maybe (Regex Σ))
 derivative (r *) x dec  with derivative r x dec 
 ... | just (just r1) = just (just (r1 & (r *)))
-... | just (nothing) = just (just (r *))
+... | just nothing = just (just (r *))
 ... | nothing = nothing
 derivative (r & s) x dec  with derivative r x dec | derivative s x dec | empty? r
 ... | nothing | _ | _ = nothing
-... | just nothing | nothing | _ = nothing
-... | just nothing | just nothing  | _ = just nothing
-... | just nothing | just (just s1)  | _ = just (just s1)
-... | just (just r1) | just (just s1)  | nothing = just (just (r1 & s))
+... | 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 (r1 & s))
+... | just (just r1) | _ | just _  = just (just (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
@@ -129,16 +130,25 @@
 char-list : List char
 char-list = a ∷ b ∷ c ∷ d ∷ []
 
-a2 = accept (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] )
-
-tr2 = trace (regex→automaton r2 char-dec ) (just (just r2)) char-list
+a2 : accept (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] )
+a2 = tt
+tr2 = trace (regex→automaton r2 char-dec ) (just (just r2)) ( a ∷ a ∷ b ∷ c ∷ [] ) a2
 
 a1  : accept (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] )
 a1  = tt
 tr1 = trace (regex→automaton < a > char-dec ) (just (just < a > )) ( a ∷ [] ) a1
 
 a3  = accept (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
-t3  = trace (regex→automaton < a > char-dec ) (just (just (< a > & < b > ))) ( a ∷ b ∷ [] )
+tr3  = trace (regex→automaton < a > char-dec ) (just (just (< 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
+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 
+regex←accept r x dec re = {!!} 
 
 
 
@@ -146,5 +156,3 @@
 
 
 
-
-