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

diff -r 5e066b730d73 -r f60c1041ae8e automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Fri Nov 26 22:33:25 2021 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Nov 27 02:50:06 2021 +0900
@@ -84,71 +84,79 @@
 
 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 : (x y : Regex Σ) → Dec ( x ≡ y )
+cmp-regex ε ε = yes refl
+cmp-regex ε φ = no (λ ())
+cmp-regex ε (y *) = no (λ ())
+cmp-regex ε (y & y₁) = no (λ ())
+cmp-regex ε (y || y₁) = no (λ ())
+cmp-regex ε < x > = no (λ ())
+cmp-regex φ ε = no (λ ())
+cmp-regex φ φ = yes refl
+cmp-regex φ (y *) =  no (λ ())
+cmp-regex φ (y & y₁) =  no (λ ())
+cmp-regex φ (y || y₁) =  no (λ ())
+cmp-regex φ < x > =  no (λ ())
+cmp-regex (x *) ε =  no (λ ())
+cmp-regex (x *) φ =  no (λ ())
+cmp-regex (x *) (y *) with cmp-regex x y
+... | yes refl = yes refl
+... | no ne = no (λ x → ne (cmp1 x)) where
+   cmp1 : (x *) ≡ (y *) → x ≡ y
+   cmp1 refl = refl
+cmp-regex (x *) (y & y₁) = no (λ ())
+cmp-regex (x *) (y || y₁) = no (λ ())
+cmp-regex (x *) < x₁ > = no (λ ())
+cmp-regex (x & x₁) ε = no (λ ())
+cmp-regex (x & x₁) φ = no (λ ())
+cmp-regex (x & x₁) (y *) = no (λ ())
+cmp-regex (x & x₁) (y & y₁) with cmp-regex x y | cmp-regex x₁ y₁ 
+... | yes refl | yes refl = yes refl
+... | no ne | _ = no (λ x → ne (cmp1 x)) where
+   cmp1 :  x & x₁ ≡ y & y₁ → x ≡ y
+   cmp1 refl = refl
+... | _ | no ne  = no (λ x → ne (cmp1 x)) where
+   cmp1 :  x & x₁ ≡ y & y₁ → x₁ ≡ y₁
+   cmp1 refl = refl
+cmp-regex (x & x₁) (y || y₁) = no (λ ())
+cmp-regex (x & x₁) < x₂ > = no (λ ())
+cmp-regex (x || x₁) ε = no (λ ())
+cmp-regex (x || x₁) φ = no (λ ())
+cmp-regex (x || x₁) (y *) = no (λ ())
+cmp-regex (x || x₁) (y & y₁) = no (λ ())
+cmp-regex (x || x₁) (y || y₁) with cmp-regex x y | cmp-regex x₁ y₁ 
+... | yes refl | yes refl = yes refl
+... | no ne | _ = no (λ x → ne (cmp1 x)) where
+   cmp1 :  x || x₁ ≡ y || y₁ → x ≡ y
+   cmp1 refl = refl
+... | _ | no ne  = no (λ x → ne (cmp1 x)) where
+   cmp1 :  x || x₁ ≡ y || y₁ → x₁ ≡ y₁
+   cmp1 refl = refl
+cmp-regex (x || x₁) < x₂ > = no (λ ())
+cmp-regex < x > ε = no (λ ())
+cmp-regex < x > φ = no (λ ())
+cmp-regex < x > (y *) = no (λ ())
+cmp-regex < x > (y & y₁) = no (λ ())
+cmp-regex < x > (y || y₁) = no (λ ())
+cmp-regex < x > < x₁ > with equal? fin x x₁ | inspect ( equal? fin x ) x₁
+... | false | record { eq = eq } = no (λ x → ¬-bool eq (cmp1 x)) where
+   cmp1 :  < x > ≡ < x₁ > →  equal? fin x x₁ ≡ true 
+   cmp1 refl = equal?-refl fin
+... | true | record { eq = eq } with equal→refl fin eq
+... | refl = yes refl
 
-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 = {!!}
+insert : List (Regex Σ) → (Regex Σ) → List (Regex Σ) 
+insert [] k = k ∷ []
+insert (x ∷ t) k with cmp-regex k x
+... | no n = x ∷ (insert t k) 
+... | yes y = x ∷ t
 
-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 : List (Regex Σ) → List (Regex Σ)
 regex-derive t = regex-derive0 t t where
-   regex-derive1 : Regex Σ → List Σ → Tree (Regex Σ) → Tree (Regex Σ)
+   regex-derive1 : Regex Σ → List Σ → List (Regex Σ) → List (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))  
+   regex-derive0 :  List (Regex Σ)  → List (Regex Σ) → List (Regex Σ)
+   regex-derive0 [] t = t
+   regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) 
 
diff -r 5e066b730d73 -r f60c1041ae8e automaton-in-agda/src/deriveUtil.agda
--- a/automaton-in-agda/src/deriveUtil.agda	Fri Nov 26 22:33:25 2021 +0900
+++ b/automaton-in-agda/src/deriveUtil.agda	Sat Nov 27 02:50:06 2021 +0900
@@ -29,10 +29,41 @@
 
 open Regex
 
-open import derive alpha2 a-eq?
+open import finiteSet
+
+fin-a : FiniteSet alpha2
+fin-a  = record {
+     finite = finite0
+   ; Q←F = Q←F0 
+   ; F←Q = F←Q0 
+   ; finiso→ = finiso→0
+   ; finiso← = finiso←0
+ } where
+     finite0 : ℕ
+     finite0 = 2
+     Q←F0 : Fin finite0 → alpha2
+     Q←F0 zero = a
+     Q←F0 (suc zero) = b
+     F←Q0 : alpha2 → Fin finite0
+     F←Q0 a = # 0
+     F←Q0 b = # 1
+     finiso→0 : (q : alpha2) → Q←F0 ( F←Q0 q ) ≡ q
+     finiso→0 a = refl
+     finiso→0 b = refl
+     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
+     finiso←0 zero = refl
+     finiso←0 (suc zero) = refl
+
+
+open import derive alpha2 fin-a 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 ∷ [] )
+
+test15 = regex-derive ( (  < a > & < b > ) * ∷ [] )
+test16 = regex-derive test15
+test17 : regex-derive test16 ≡ test16
+test17 = refl
diff -r 5e066b730d73 -r f60c1041ae8e automaton-in-agda/src/nfa.agda
--- a/automaton-in-agda/src/nfa.agda	Fri Nov 26 22:33:25 2021 +0900
+++ b/automaton-in-agda/src/nfa.agda	Sat Nov 27 02:50:06 2021 +0900
@@ -83,24 +83,6 @@
 data-fin-01 (suc (suc zero)) lt = {!!}
 data-fin-01 (suc (suc (suc x))) (s≤s (s≤s (s≤s ())))
 
-{-# TERMINATING #-}
-NtraceDepth : { Q : Set } { Σ : Set  } 
-    → NAutomaton Q  Σ
-    → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
-NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] where
-    ndepth : List Q → (q : Q → Bool ) → List Σ  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
-    ndepth1 : Q → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
-    ndepth1 q [] is t t1 = t ∷ t1
-    ndepth1 q _ [] t t1 = t1
-    ndepth1 q (x ∷ qns) (i ∷ []) t t1 with Nend M x
-    ... | true = ndepth1 q qns (i ∷ []) (⟪ i , x ⟫ ∷ t) t1
-    ... | false = t1
-    ndepth1 q (x ∷ qns) (i ∷ is) t t1 =  ndepth all (Nδ M x i) is (ndepth1 q qns (i ∷ is) (⟪ i , q ⟫ ∷ t) t1 )
-    ndepth [] sb is t = t
-    ndepth (q ∷ qs) sb is t with sb q 
-    ... | true  = ndepth qs sb is (ndepth1 q all is [] t )
-    ... | false = ndepth qs sb is t
-    
 transition3 : States1  → In2  → States1 → Bool
 transition3 sr i0 sr = true
 transition3 sr i1 ss = true
@@ -129,12 +111,30 @@
 example2-1 = Naccept am2 existsS1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
 example2-2 = Naccept am2 existsS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 
+{-# TERMINATING #-}
+NtraceDepth : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ
+    → (Nstart : Q → Bool) → List Q  → List  Σ → List (Bool ∧ List ( Σ ∧ Q ))
+NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
+    ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (Bool ∧ List ( Σ ∧ Q )  ) →  List (Bool ∧ List ( Σ ∧ Q )  )
+    ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( Bool ∧ List ( Σ ∧ Q )) →  List ( Bool ∧ List ( Σ ∧ Q ))
+    ndepth1 q i [] is t t1 = t1
+    ndepth1 q i _ [] t t1 with Nend M q
+    ... | true =  ⟪ true , (⟪ i , q ⟫ ∷ t ) ⟫ ∷ t1
+    ... | false = ⟪ false , (⟪ i , q ⟫ ∷ t )  ⟫ ∷ t1
+    ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
+    ndepth [] sb is t t1 =  t1
+    ndepth (q ∷ qs) sb [] t t1 =  t1
+    ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
+    ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
+    ... | false = ndepth qs sb (i ∷ is) t t1
+    
 t-1 : List ( List States1 )
 t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
 t-3 = NtraceDepth am2 start1 LStates1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 t-4 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
-t-5 = NtraceDepth am2 start1 LStates1 ( i0  ∷ [] ) 
+t-5 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1 ∷ [] ) 
 
 transition4 : States1  → In2  → States1 → Bool
 transition4 sr i0 sr = true