Mercurial > hg > Members > kono > Proof > automaton1
view dfa2regex.agda @ 20:bdca72fe271e default tip
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 03 Dec 2020 06:44:49 +0900 (2020-12-02) |
parents | 5f97e5606e7e |
children |
line wrap: on
line source
{-# 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₁