Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/derive.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents c298981108c1
children b85402051cdb
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
3 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 3 open import Relation.Binary.PropositionalEquality hiding ( [_] )
4 open import Relation.Nullary using (¬_; Dec; yes; no) 4 open import Relation.Nullary using (¬_; Dec; yes; no)
5 open import Data.List hiding ( [_] ) 5 open import Data.List hiding ( [_] )
6 open import Data.Empty 6 open import Data.Empty
7 open import finiteSet 7 open import finiteSet
8 open import finiteFunc
8 open import fin 9 open import fin
9 10
10 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where 11 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
11 12
12 open import automaton 13 open import automaton
72 regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit refl } is 73 regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit refl } is
73 74
74 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 75 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
75 76
76 -- open import nfa 77 -- open import nfa
77 open import Data.Nat 78 open import Data.Nat hiding (eq?)
78 open import Data.Nat.Properties hiding ( eq? ) 79 open import Data.Nat.Properties hiding ( eq? )
79 open import nat 80 open import nat
80 open import finiteSetUtil 81 open import finiteSetUtil
81 open FiniteSet 82 open FiniteSet
82 open import Data.Fin hiding (_<_ ; _≤_ ; pred ) 83 open import Data.Fin hiding (_<_ ; _≤_ ; pred )
259 sbempty? (r *) f = true 260 sbempty? (r *) f = true
260 sbempty? (r & r₁) f = ? where 261 sbempty? (r & r₁) f = ? where
261 sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? ) 262 sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? )
262 ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? ) 263 ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? )
263 ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? )) 264 ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? ))
264 sb01 isb with ISB.is-sub isb | inspect ISB.is-sub isb 265 sb01 isb with ISB.is-sub isb in eq
265 ... | sub&1 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case1 refl 266 ... | sub&1 .r .r₁ .(ISB.s isb) t = case1 ?
266 ... | sub&2 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case2 (case1 refl) 267 ... | sub&2 .r .r₁ .(ISB.s isb) t = case2 (case1 ?)
267 ... | sub&& .r .r₁ z x t | record { eq = refl } = case2 (case2 refl) 268 ... | sub&& .r .r₁ z x t = case2 (case2 ?)
268 sb00 : ISB r → Bool 269 sb00 : ISB r → Bool
269 sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub } 270 sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub }
270 sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? } 271 sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }
271 ... | false | t = true 272 ... | false | t = true
272 ... | true | t = empty? r \/ empty? r₁ 273 ... | true | t = empty? r \/ empty? r₁