--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/regex.agda	Mon Nov 16 13:11:26 2020 +0900
@@ -0,0 +1,150 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module regex where
+
+open import Level renaming ( suc to Suc ; zero to Zero )
+open import Data.List hiding ( any ;  [_] ; concat )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] ) 
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Empty
+open import Data.Unit
+open import Data.Maybe
+open import logic
+
+
+data Regex   ( Σ : Set  ) : Set  where
+   _*    : Regex  Σ → Regex  Σ
+   _&_   : Regex  Σ → Regex  Σ → Regex Σ
+   _||_  : Regex  Σ → Regex  Σ → Regex Σ
+   <_>   : Σ → Regex  Σ
+
+-- postulate a b c d : Set
+
+data char : Set where
+   a : char
+   b : char
+   c : char
+   d : char
+
+infixr 40 _&_ _||_
+
+r1' =    (< a > & < b >) & < c >
+r1 =    < a > & < b > & < c >
+any = < a > || < b >  || < c > || < d >
+r2 =    ( any * ) & ( < a > & < b > & < c > )
+r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
+data regular-expr  {Σ : Set} : Regex Σ → List Σ → Set where
+   atom : (x :  Σ ) →  regular-expr < x > ( x ∷ [] )
+   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
+
+test-regex : Set
+test-regex = ¬ (regular-expr r1 ( a ∷ [] ) )
+
+test-regex1 : regular-expr r1 ( a ∷ b ∷ c ∷ [] ) 
+test-regex1 = concat (atom a) (concat (atom b) (atom c)) 
+
+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? (r & s) with empty? r
+... | nothing = nothing
+... | just _ = empty? s
+empty? (r || s) with empty? r | empty? s
+... | nothing | nothing = nothing
+... | just r1 | _ = just r1
+... | _ | just s1 = just s1
+empty? < x > = nothing
+
+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 *))
+... | 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 (just r1) | just (just s1)  | just _  = just (just (s1 || (r1 & s)))
+... | just (just r1) | _ | _ = 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
+... | _ | just nothing = just nothing
+... | just (just r1) | _ = just (just r1)
+... | _ | just (just s1) = just (just s1)
+... | nothing | nothing = nothing
+derivative < i > x dec  with dec i x
+... | yes y = just nothing
+... | no _ = nothing
+
+open import automaton
+
+regex→automaton :  {Σ : Set} →  Regex Σ → ((i j : Σ ) → Dec ( i ≡ j )) → Automaton (Maybe (Maybe (Regex Σ))) Σ
+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) = ⊤
+      F _ = ⊥
+
+char-dec : (i j : char) → Dec (i ≡ j)
+char-dec a a = yes refl
+char-dec b b = yes refl
+char-dec c c = yes refl
+char-dec d d = yes refl
+char-dec a b = no (λ ())
+char-dec a c = no (λ ())
+char-dec a d = no (λ ())
+char-dec b a = no (λ ())
+char-dec b c = no (λ ())
+char-dec b d = no (λ ())
+char-dec c a = no (λ ())
+char-dec c b = no (λ ())
+char-dec c d = no (λ ())
+char-dec d a = no (λ ())
+char-dec d b = no (λ ())
+char-dec d c = no (λ ())
+
+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
+
+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 ∷ [] )
+
+
+
+
+
+
+
+
+