--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/dfa2regex.agda	Mon Nov 16 18:51:57 2020 +0900
@@ -0,0 +1,48 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module dfa2regex 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
+open import automaton
+open import regex
+
+open Automaton 
+
+initail : {n  : Level} {Q : Set n} {Σ : Set } → (atm : Automaton Q Σ) → ((q : Q ) → Dec (F atm q))  → (Q → Regex Σ)
+initail atm decF q with decF q
+... | yes _ = ε
+... | no _ = φ
+
+add1 : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → List Σ → (Q → Regex Σ) → (Q → Regex Σ)
+add1 atm [] qs q = qs q
+add1 atm (x ∷ L) qs q with add1 atm L qs q | δ atm q x
+... | rx | nq = ( < x > & qs nq ) || rx
+
+{-# TERMINATING #-}
+sumup : {n  : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → ((s t : Σ) → Dec (s ≡ t))  → List Σ → (Q → Regex Σ) → Q → Regex Σ
+sumup atm dec L f q with RE-dec dec (f q) (add1 atm L f q) 
+... | yes _ = f q
+... | no _ = sumup atm dec L (add1 atm L f) q
+
+L2 : List Σ2
+L2 = s0 ∷  s1 ∷ []
+
+dec2 : (s t : Σ2) → Dec (s ≡ t)
+dec2 s0 s0 = yes refl
+dec2 s0 s1 = no (λ ())
+dec2 s1 s0 = no (λ ())
+dec2 s1 s1 = yes refl
+
+a16Fdec : (q : Q3) → Dec (F a16 q)
+a16Fdec q₁ = no (λ ())
+a16Fdec q₂ = yes a16q2
+a16Fdec q₃ = no (λ ())
+
+sm1 : Regex Σ2 
+sm1 = sumup a16 dec2 L2 (initail a16 a16Fdec) q₁