Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regex.agda @ 411:207e6c4e155c

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 Wed, 29 Nov 2023 17:40:55 +0900
parents af8f630b7e60
children
comparison
equal deleted inserted replaced
410:db02b6938e04 411:207e6c4e155c
12 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 12 open import Relation.Binary.PropositionalEquality as RBF hiding ( [_] )
13 open import Relation.Nullary using (¬_; Dec; yes; no) 13 open import Relation.Nullary using (¬_; Dec; yes; no)
14 open import logic 14 open import logic
15 open import regular-language 15 open import regular-language
16 16
17 -- (abc|d.*)
18 -- any = < a > || < b > || < c > || < d >
19 -- ( < a > & < b > & < c > ) || ( <d > & ( any * ) )
20
17 data Regex ( Σ : Set) : Set where 21 data Regex ( Σ : Set) : Set where
18 ε : Regex Σ -- empty 22 ε : Regex Σ -- empty
19 φ : Regex Σ -- fail 23 φ : Regex Σ -- fail
20 _* : Regex Σ → Regex Σ 24 _* : Regex Σ → Regex Σ
21 _&_ : Regex Σ → Regex Σ → Regex Σ 25 _&_ : Regex Σ → Regex Σ → Regex Σ
22 _||_ : Regex Σ → Regex Σ → Regex Σ 26 _||_ : Regex Σ → Regex Σ → Regex Σ
23 <_> : Σ → Regex Σ 27 <_> : Σ → Regex Σ
24 28
25 infixr 40 _&_ _||_ 29 infixr 40 _&_ _||_
26 30
27 -- Meaning of regular expression 31 -- Meaning of regular expression
28 32
29 regex-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y)) → List Σ → Bool 33 regex-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y)) → List Σ → Bool
30 regex-language φ cmp _ = false 34 regex-language φ cmp _ = false
31 regex-language ε cmp [] = true 35 regex-language ε cmp [] = true
32 regex-language ε cmp (_ ∷ _) = false 36 regex-language ε cmp (_ ∷ _) = false
33 regex-language (x *) cmp = repeat ( regex-language x cmp ) 37 regex-language (x *) cmp = repeat ( regex-language x cmp ) []
34 regex-language (x & y) cmp = split ( λ z → regex-language x cmp z ) (λ z → regex-language y cmp z ) 38 regex-language (x & y) cmp = split ( λ z → regex-language x cmp z ) (regex-language y cmp )
35 regex-language (x || y) cmp = λ s → ( regex-language x cmp s ) \/ ( regex-language y cmp s) 39 regex-language (x || y) cmp = λ s → ( regex-language x cmp s ) \/ ( regex-language y cmp s)
36 regex-language < h > cmp [] = false 40 regex-language < h > cmp [] = false
37 regex-language < h > cmp (h1 ∷ [] ) with cmp h h1 41 regex-language < h > cmp (h1 ∷ [] ) with cmp h h1
38 ... | yes _ = true 42 ... | yes _ = true
39 ... | no _ = false 43 ... | no _ = false
40 regex-language < h > _ (_ ∷ _ ∷ _) = false 44 regex-language < h > _ (_ ∷ _ ∷ _) = false