# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637933605 -32400
# Node ID 5e066b730d7368f3bdc85e4bec3b37c7f16d1e14
# Parent  dd98e7e5d4a5cde74bd41c2e92cbf6bb583d6234
regex cmp

diff -r dd98e7e5d4a5 -r 5e066b730d73 automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Fri Nov 26 20:02:06 2021 +0900
+++ b/automaton-in-agda/src/derive.agda	Fri Nov 26 22:33:25 2021 +0900
@@ -3,19 +3,19 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.List hiding ( [_] )
+open import finiteSet
 
-module derive ( Σ : Set) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
+module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
 
 -- open import nfa
 open import Data.Nat
 -- open import Data.Nat hiding ( _<_ ; _>_ )
 -- open import Data.Fin hiding ( _<_ )
-
-open import finiteSet
 open import finiteSetUtil
 open import automaton
 open import logic
 open import regex
+open FiniteSet
 
 empty? : Regex  Σ → Bool
 empty?  ε       = true
@@ -81,3 +81,74 @@
 
 regex-match : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
+
+open import Relation.Binary.Definitions
+
+
+data _r<_  : (x y : Regex Σ)  → Set  where
+   ε<φ : ε r< φ  
+   ε<* : {y : Regex Σ} → ε r< (y *) 
+   ε<|| : {y y₁ : Regex Σ} → ε r< (y || y₁) 
+   ε<& : {y y₁ : Regex Σ} → ε r< (y & y₁) 
+   ε<<> : {x : Σ} → ε r< < x > 
+   φ<* : {y : Regex Σ} → φ r< (y *) 
+   φ<|| : {y y₁ : Regex Σ} → φ r< (y || y₁) 
+   φ<& : {y y₁ : Regex Σ} → φ r< (y & y₁) 
+   φ<<> : {x : Σ} → φ r< < x > 
+   *<* : {x y : Regex Σ} → x r< y → (x *) r< (y *) 
+   *<& : {x y y₁ : Regex Σ} → (x *) r< (y & y₁) 
+   *<|| : {x y y₁ : Regex Σ} → (x *) r< (y || y₁) 
+   <><* : {x₁ : Σ} {x : Regex Σ} → < x₁ > r< (x *)  
+   &<&0 : {x x₁ y y₁ : Regex Σ} → x r<  y  → (x & x₁) r< (y & y₁) 
+   &<&1 : {x x₁ y₁ : Regex Σ} → x₁ r< y₁  → (x & x₁) r< (x & y₁) 
+   &<|| : (x x₁ y y₁ : Regex Σ) → (x & x₁) r< (y || y₁) 
+   ||<||0 : {x x₁ y y₁ : Regex Σ} → x r< y  → (x || x₁) r< (y || y₁) 
+   ||<||1 : {x x₁ y₁ : Regex Σ} → x₁ r< y₁  → (x || x₁) r< (x || y₁) 
+   <><<> : {x x₁ : Σ} → F←Q fin x Data.Fin.< F←Q fin x₁  → < x > r< < x₁ > 
+
+cmp-regex : Trichotomous  _≡_  _r<_  
+cmp-regex ε ε = tri≈ (λ ()) refl (λ ())
+cmp-regex ε φ = tri< ε<φ (λ ()) (λ ())
+cmp-regex ε (y *) = tri< ε<* (λ ()) (λ ())
+cmp-regex ε (y & y₁) = tri< ε<& (λ ()) (λ ())
+cmp-regex ε (y || y₁) = tri< ε<|| (λ ()) (λ ())
+cmp-regex ε < x > = tri< ε<<> (λ ()) (λ ())
+cmp-regex φ ε = tri> (λ ()) (λ ()) ε<φ 
+cmp-regex φ φ = tri≈ (λ ()) refl (λ ())
+cmp-regex φ (y *) = tri< φ<*   (λ ()) (λ ())
+cmp-regex φ (y & y₁) = tri< φ<&   (λ ()) (λ ())
+cmp-regex φ (y || y₁) = tri< φ<||   (λ ()) (λ ())
+cmp-regex φ < x > = tri< φ<<>   (λ ()) (λ ())
+cmp-regex (x *) ε =  tri> (λ ()) (λ ()) ε<*
+cmp-regex (x *) φ = tri> (λ ()) (λ ()) φ<*
+cmp-regex (x *) (y *) with cmp-regex x y
+... | tri< a ¬b ¬c = tri< ( *<* a ) {!!} {!!}
+... | tri≈ ¬a refl ¬c = tri≈ {!!} refl {!!}
+... | tri> ¬a ¬b c = {!!}
+cmp-regex (x *) (y & y₁) = tri< *<& (λ ()) (λ ()) 
+cmp-regex (x *) (y || y₁) = tri< *<|| (λ ()) (λ ()) 
+cmp-regex (x *) < x₁ > =  tri> (λ ()) (λ ()) <><*
+cmp-regex (x & x₁) y = {!!}
+cmp-regex (x || x₁) y = {!!}
+cmp-regex < x > y = {!!}
+
+data Tree ( Key : Set ) : Set where
+    leaf : Tree Key 
+    node : Key → Tree Key → Tree Key → Tree Key 
+
+insert : Tree (Regex Σ) → (Regex Σ) → Tree (Regex Σ) 
+insert leaf k = node k leaf leaf
+insert (node x t t₁) k with cmp-regex k x
+... | tri< a ¬b ¬c = node x (insert t k) t₁
+... | tri≈ ¬a b ¬c = node x t t₁
+... | tri> ¬a ¬b c = node x t (insert t₁ k) 
+
+regex-derive : Tree (Regex Σ) → Tree (Regex Σ)
+regex-derive t = regex-derive0 t t where
+   regex-derive1 : Regex Σ → List Σ → Tree (Regex Σ) → Tree (Regex Σ)
+   regex-derive1 x [] t = t
+   regex-derive1 x (i ∷ t) r =  regex-derive1 x t (insert r (derivative x i))
+   regex-derive0 :  Tree (Regex Σ)  → Tree (Regex Σ) → Tree (Regex Σ)
+   regex-derive0 leaf t = t
+   regex-derive0 (node x r r₁) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true))  (regex-derive0 r₁ t))  
+
diff -r dd98e7e5d4a5 -r 5e066b730d73 automaton-in-agda/src/deriveUtil.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/automaton-in-agda/src/deriveUtil.agda	Fri Nov 26 22:33:25 2021 +0900
@@ -0,0 +1,38 @@
+module deriveUtil where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.Fin
+open import Data.List
+
+open import regex
+open import automaton
+open import nfa
+open import logic
+open NAutomaton
+open Automaton
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary
+
+
+open Bool
+
+data alpha2 : Set where
+   a : alpha2
+   b : alpha2
+
+a-eq? : (x y : alpha2) → Dec (x ≡ y)
+a-eq? a a = yes refl
+a-eq? b b = yes refl
+a-eq? a b = no (λ ())
+a-eq? b a = no (λ ())
+
+open Regex
+
+open import derive alpha2 a-eq?
+test11 = regex→automaton ( < a > & < b > )
+
+test12 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ b ∷ [] )
+test13 = accept test11 record { state =  < a > & < b > ; is-derived = unit } ( a ∷ a ∷ [] )
+
+test14 = regex-match ( (  < a > & < b > ) * ) ( a ∷ b ∷ a ∷ a ∷ [] )