1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
embed
{{ coq
Import ListNotations.
Section RegExp.
Variable char : Type.
}}
metavar c ::=
{{ lex alphanum }}
{{ com character }}
{{ coq char }}
{{ hol char }}
{{ coq-universe Type }}
grammar
s :: s_ ::=
{{ com string }}
{{ coq list char }}
{{ hol char list }}
{{ coq-universe Type }}
| e :: M :: empty
{{ coq [] }}
{{ hol [] }}
{{ tex \epsilon }}
| c :: M :: char
{{ coq ([[c]] :: []) }}
{{ hol ([[c]] :: []) }}
| s s' :: M :: concat
{{ coq ([[s]] ++ [[s']]) }}
{{ hol ([[s]] ++ [[s']]) }}
r :: r_ ::=
{{ com regexp }}
{{ coq-universe Type }}
| 0 :: :: zero
| 1 :: :: unit
| c :: :: char
| r + r' :: :: plus
| r r' :: :: times
| r * :: :: star
{{ tex [[r]]^* }}
terminals :: terminals_ ::=
| in :: :: in {{ tex \in }}
| L :: :: L {{ tex \mathit{L} }}
formula :: formula_ ::=
| judgement :: :: judgement
defns
regexp_ins :: '' ::=
defn
s in L ( r ) :: :: s_in_regexp_lang :: s_in_regexp_lang_
{{ com string in regexp language }} by
--------- :: unit
e in L(1)
---------- :: char
c in L(c)
s in L(r1)
------------- :: plus_1
s in L(r1+r2)
s in L(r2)
------------- :: plus_2
s in L(r1+r2)
s in L(r1)
s' in L(r2)
---------------- :: times
s s' in L(r1 r2)
---------- :: star_1
e in L(r*)
s in L(r)
s' in L(r*)
------------- :: star_2
s s' in L(r*)
defns
regexp_ins_c :: '' ::=
defn
s in L ( r ; c ) :: :: s_in_regexp_c_lang :: s_in_regexp_c_lang_
{{ com string in regexp c language }} by
c s in L(r)
----------- :: cs
s in L(r;c)
embed
{{ coq
End RegExp.
}}
|
