Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/derive.agda @ 271:5e066b730d73
regex cmp
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 26 Nov 2021 22:33:25 +0900 |
parents | dd98e7e5d4a5 |
children | f60c1041ae8e |
line wrap: on
line diff
--- 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)) +