Mercurial > hg > Members > kono > Proof > automaton
view agda/regex1.agda @ 37:a7f09c9a2c7a
fix
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 05 Dec 2018 16:17:28 +0900 |
parents | 9558d870e8ae |
children | ab265470c2d0 |
line wrap: on
line source
module regex1 where open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Fin open import Data.Nat hiding ( _≟_ ) open import Data.List hiding ( any ) import Data.Bool using ( Bool ; true ; false ; _∧_ ) open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) data Regex ( Σ : Set ) : Set where _* : Regex Σ → Regex Σ _&_ : Regex Σ → Regex Σ → Regex Σ _||_ : Regex Σ → Regex Σ → Regex Σ <_> : Σ → Regex Σ -- postulate a b c d : Set data hoge : Set where a : hoge b : hoge c : hoge d : hoge infixr 40 _&_ _||_ r1' = (< a > & < b >) & < c > r1 = < a > & < b > & < c > any = < a > || < b > || < c > r2 = ( any * ) & ( < a > & < b > & < c > ) r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > ) r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > ) r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > ) open import nfa _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool x ‖ y = λ s → x s ∨ y s split : {Σ : Set} → (List Σ → Bool) → ( List Σ → Bool) → List Σ → Bool split x y [] = x [] ∧ y [] split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) t _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool x ・ y = λ z → split x y z {-# TERMINATING #-} repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool repeat x [] = true repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t ) open FiniteSet cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y) cmpi fin x y = F←Q fin x ≟ F←Q fin y regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → List Σ → Bool regular-language (x *) f = repeat ( regular-language x f ) regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f ) regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f ) regular-language < h > f [] = false regular-language < h > f (h1 ∷ [] ) with cmpi f h h1 ... | yes _ = true ... | no _ = false regular-language < h > f _ = false finIn2 : FiniteSet In2 finIn2 = record { Q←F = Q←F' ; F←Q = F←Q' ; finiso→ = finiso→' ; finiso← = finiso←' } where Q←F' : Fin 2 → In2 Q←F' zero = i0 Q←F' (suc zero) = i1 Q←F' (suc (suc ())) F←Q' : In2 → Fin 2 F←Q' i0 = zero F←Q' i1 = suc (zero) finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q finiso→' i0 = refl finiso→' i1 = refl finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f finiso←' zero = refl finiso←' (suc zero) = refl finiso←' (suc (suc ())) test-r1 = < i0 > & < i1 > test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] ) test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] ) issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool issub (r *) s f = issub r s f issub (r & r₁) s f = issub r s f ∨ issub r₁ s f issub (r || r₁) s f = issub r s f ∨ issub r₁ s f issub < x > < s > f with cmpi f x s issub < x > < s > f | yes p = true issub < x > < s > f | no ¬p = false issub < x > s f = false record RegexSub {Σ : Set} (R : Regex Σ) {n : ℕ } (fin : FiniteSet Σ {n} ): Set where field Subterm : Regex Σ sub : issub R Subterm fin ≡ true open import Data.Product regex2nfa' : {Σ : Set} → Regex Σ → {n m : ℕ } (fin : FiniteSet Σ {n}) → ( NAutomaton (Regex Σ) Σ × FiniteSet (Regex Σ) {m} ) regex2nfa' = {!!} regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where nr0 = regex2nfa r fin Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1) Nstart : (Regex Σ) → Bool Nstart s0 = NAutomaton.Nstart nr0 s0 Nend : (Regex Σ) → Bool Nend s0 = NAutomaton.Nend nr0 s0 regex2nfa {Σ} (r0 & r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where nr0 = regex2nfa r0 fin nr1 = regex2nfa r1 fin Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr1 s0 i s1 ) Nstart : (Regex Σ) → Bool Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 ) Nend : (Regex Σ) → Bool Nend s0 = NAutomaton.Nend nr0 s0 ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 ) regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where nr0 = regex2nfa r0 fin nr1 = regex2nfa r1 fin Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1 Nstart : (Regex Σ) → Bool Nstart s0 = NAutomaton.Nstart nr0 s0 ∨ NAutomaton.Nstart nr1 s0 Nend : (Regex Σ) → Bool Nend s0 = NAutomaton.Nend nr0 s0 ∨ NAutomaton.Nend nr1 s0 regex2nfa {Σ} < x > fin = record { Nδ = Nδ ; Nstart = Nstart ; Nend = Nend } where Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool Nδ r1 s r2 with cmpi fin s x Nδ r1 s r2 | yes _ = true Nδ r1 s r2 | no _ = false Nstart : (Regex Σ) → Bool Nstart < s > with cmpi fin s x ... | yes _ = true ... | no _ = false Nstart _ = false Nend : (Regex Σ) → Bool Nend _ = false test-r4 = regex2nfa (< i0 > & < i1 >) finIn2 -- testr5 = Naccept test-r4 {!!} ( i0 ∷ i1 ∷ [] ) reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) → ( regex : Regex Σ ) → ( rfin : FiniteSet (Regex Σ) {m} ) → ( In : List Σ ) → regular-language regex fin In ≡ Naccept {Regex Σ} {_} ( regex2nfa {Σ} regex fin ) rfin In reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) rfin In = {!!} reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) rfin In = {!!} reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) rfin In = {!!} reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > rfin In = {!!}