Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/regex2.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 a5c874396cc4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
405
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 384
diff changeset
3 -- {-# OPTIONS --allow-unsolved-metas #-}
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
4
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
5 open import Relation.Binary.PropositionalEquality hiding ( [_] )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
6 open import Relation.Nullary using (¬_; Dec; yes; no)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
7 open import Data.List hiding ( [_] )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
8 open import Data.Empty
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
9 open import finiteSet
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
10 open import finiteSetUtil
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
11 open import fin
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
12
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
13 module regex2 ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Level renaming ( suc to succ ; zero to Zero )
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
16 open import Data.Fin hiding ( pred )
34
a904b6bc76af add regular language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
17 open import Data.Nat hiding ( _≟_ )
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
18 open import Data.List hiding ( any ; [_] )
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
19 -- import Data.Bool using ( Bool ; true ; false ; _∧_ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
20 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
34
a904b6bc76af add regular language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
21 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] )
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
22 open import Relation.Nullary using (¬_; Dec; yes; no)
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
23 open import regex
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
24 open import regular-language
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
25 open import automaton
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
26 open import logic
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
27
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
28 open import regular-star
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
29 open import regular-concat
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
30
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
31 open Automaton
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
32 open FiniteSet
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
33
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
34 open RegularLanguage
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
35
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
36 regex→RegularLanguage : Regex Σ → RegularLanguage Σ
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
37 regex→RegularLanguage ε = record { states = One ∨ One ; astart = case1 one ; afin = fin-∨1 finOne
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
38 ; automaton = record { δ = λ _ _ → case2 one ; aend = rg00 } } where
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
39 rg00 : One ∨ One → Bool
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
40 rg00 (case1 one) = true
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
41 rg00 (case2 one) = false
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
42 regex→RegularLanguage φ = record { states = One ; astart = one ; afin = finOne ; automaton = record { δ = λ _ _ → one ; aend = λ _ → false } }
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
43 regex→RegularLanguage (r *) = M-Star ( regex→RegularLanguage r )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
44 regex→RegularLanguage (r & r₁) = M-Concat ( regex→RegularLanguage r ) (regex→RegularLanguage r₁ )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
45 regex→RegularLanguage (r || r₁) = M-Union ( regex→RegularLanguage r ) (regex→RegularLanguage r₁ )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
46 regex→RegularLanguage < x > = record { states = One ∨ One ∨ One ; astart = case1 one ; afin = fin-∨1 (fin-∨1 finOne)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
47 ; automaton = record { δ = rg01 ; aend = rg00 } } where
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
48 rg00 : One ∨ One ∨ One → Bool
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
49 rg00 (case1 one) = false -- empty case failure
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
50 rg00 (case2 (case1 one)) = true -- may true on this phase
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
51 rg00 (case2 (case2 one)) = false -- no success never after
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
52 rg01 : One ∨ One ∨ One → Σ → One ∨ One ∨ One
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
53 rg01 (case1 one) s with eq? s x
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
54 ... | yes _ = case2 (case1 one)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
55 ... | no _ = case2 (case2 one)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
56 rg01 (case2 (case1 one)) s = case2 (case2 one)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
57 rg01 (case2 (case2 one)) s = case2 (case2 one)
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
58
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
59
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
60 open Split
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
61
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
62 open _∧_
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
63
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
64 open import Data.List.Properties
330
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
65
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
66 regex-concat : {a b : Regex Σ} → (x : List Σ) → regex-language (a & b) eq? x ≡ Concat (regex-language a eq?) (regex-language b eq?) x
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
67 regex-concat {_} {_} x = refl
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
68
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
69 open import sbconst2
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
70
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
71 regex-is-regular : (r : Regex Σ ) → ( x : List Σ ) → isRegular (regex-language r eq?) x ( regex→RegularLanguage r )
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
72 regex-is-regular r x = rg00 r x where
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
73 rg00 : (r : Regex Σ) → (x : List Σ) → regex-language r eq? x ≡ accept (automaton (regex→RegularLanguage r)) (astart (regex→RegularLanguage r)) x
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
74 rg00 ε x = ?
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
75 rg00 φ x = ?
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
76 rg00 (r *) x = ?
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
77 rg00 (r & r₁) x = begin
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
78 split (regex-language r eq?) (regex-language r₁ eq?) x ≡⟨ cong₂ (λ j k → Concat j k x)
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
79 (f-extensionality (rg00 r)) (f-extensionality (rg00 r₁)) ⟩
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
80 Concat (contain (regex→RegularLanguage r)) (contain (regex→RegularLanguage r₁)) x
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
81 ≡⟨ closed-in-concat (regex→RegularLanguage r) (regex→RegularLanguage r₁) x ⟩
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
82 contain (M-Concat (regex→RegularLanguage r) (regex→RegularLanguage r₁)) x ∎
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
83 where open ≡-Reasoning
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
84 rg00 (r || r₁) x = ?
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
85 rg00 < s > x = ?
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
86
383
708570e55a91 add regex2 (we need source reorganization)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 382
diff changeset
87 -- end