--- a/regex.agda	Mon Nov 16 18:51:57 2020 +0900
+++ b/regex.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -53,6 +53,79 @@
 test-regex1 = concat (atom a) (concat (atom b) (atom c)) 
 
 open import regular-language
+open import Data.Empty 
+open import  Relation.Nullary
+
+regex-language : {Σ : Set} → (r : Regex Σ) →  ((i j : Σ) → Dec ( i ≡ j)) →  (t : List Σ ) → Set
+regex-language φ dec  _ = ⊥
+regex-language ε dec [] = ⊤
+regex-language ε dec (_ ∷ _) = ⊥
+regex-language (x *) dec f = Star ( regex-language x dec )  f
+regex-language (x & y) dec f = split ( regex-language x dec ) ( regex-language y dec ) f
+regex-language (x || y) dec f = ( regex-language x dec f )  ∨  ( regex-language y dec f )
+regex-language < h > dec [] = ⊥
+regex-language < h > dec (h1  ∷ [] ) with dec h h1
+... | yes _ = ⊤
+... | no _  = ⊥
+regex-language < h > 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 ∷ []
+
+test-regex2 : ¬ (regex-language r1 char-dec ( a ∷ [] ) )
+test-regex2 (case1 ())
+test-regex2 (case2 ())
+
+test-regex3 : regex-language r1 char-dec  ( a ∷ b ∷ c ∷ [] ) 
+test-regex3 = case2 (case1 [ tt , case2 (case1 [ tt , tt ]) ] )
+
+splitb : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → List Σ → Bool
+splitb x y  [] = x [] /\ y []
+splitb x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
+  splitb (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
+
+{-# TERMINATING #-}
+repeatb : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+repeatb x [] = true
+repeatb {Σ} x ( h  ∷ t ) = splitb x (repeatb {Σ} x) ( h  ∷ t )
+
+regular-language : {Σ : Set} → Regex Σ → ((i j : Σ) → Dec ( i ≡ j)) →  List Σ → Bool
+regular-language ε dec _ = false
+regular-language φ dec [] = true
+regular-language φ dec (_ ∷ _ ) = false
+regular-language (x *) dec = repeatb ( regular-language x dec )
+regular-language (x & y) dec = splitb ( regular-language x dec ) ( regular-language y dec )
+regular-language (x || y) dec = λ s → ( regular-language x dec s )  \/ ( regular-language y dec s)
+regular-language < h > dec [] = false
+regular-language < h > dec (h1  ∷ [] ) with dec h h1
+... | yes _ = true
+... | no _  = false
+regular-language < h > dec _ = false
+
+test-regex4 : Bool
+test-regex4 = regular-language  r1 char-dec ( a ∷ [] ) 
+
+test-regex5 : Bool
+test-regex5 = regular-language  r1 char-dec  ( a ∷ b ∷ c ∷ [] )
 
 -- open import Data.Nat.DivMod
 
@@ -118,27 +191,6 @@
       F finish = ⊤
       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 ∷ []
-
 open Automaton 
 
 a2 : accept (regex→automaton r2 char-dec ) (continue r2) ( a ∷ a ∷ b ∷ c ∷ [] )