Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/regex.agda @ 366:19410aadd636

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 Sat, 22 Jul 2023 10:04:39 +0900
parents 3fa72793620b
children a5c874396cc4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module regex where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
3 data Regex ( Σ : Set) : Set where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
4 ε : Regex Σ -- empty
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
5 φ : Regex Σ -- fail
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
6 _* : Regex Σ → Regex Σ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
7 _&_ : Regex Σ → Regex Σ → Regex Σ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
8 _||_ : Regex Σ → Regex Σ → Regex Σ
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
9 <_> : Σ → Regex Σ
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
10
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
11 infixr 40 _&_ _||_
7
f1fbe6603066 εAutomaton using Tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
12
f1fbe6603066 εAutomaton using Tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
13
f1fbe6603066 εAutomaton using Tree
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
14