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
|
(** {1 Theory of regular expressions} *)
module Regexp
type char
(** {2 Syntax} *)
type regexp =
| Empty
| Epsilon
| Char char
| Alt regexp regexp
| Concat regexp regexp
| Star regexp
(** {2 Semantics} *)
(** Words are sequences of characters. *)
use seq.Seq
use seq.FreeMonoid
use int.Int
type word = seq char
(** Inductive predicate `mem w r` means
"word `w` belongs to the language of `r`". *)
inductive mem (w: word) (r: regexp) =
| mem_eps:
mem empty Epsilon
| mem_char:
forall c: char. mem (singleton c) (Char c)
| mem_altl:
forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
| mem_altr:
forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
| mem_concat:
forall w1 w2: word, r1 r2: regexp.
mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
| mems1:
forall r: regexp. mem empty (Star r)
| mems2:
forall w1 w2: word, r: regexp.
mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)
(** Optimizing constructors for Alt and Concat *)
let alt (r1 r2: regexp) : regexp
ensures { forall w: word. mem w result <-> mem w (Alt r1 r2) }
= match r1, r2 with
| Empty, _ -> r2
| _, Empty -> r1
| _ -> Alt r1 r2
end
let concat (r1 r2: regexp) : regexp
ensures { forall w: word. mem w result <-> mem w (Concat r1 r2) }
= match r1, r2 with
| Empty, _ -> Empty
| _, Empty -> Empty
| Epsilon, _ -> r2
| _, Epsilon -> r1
| _ -> Concat r1 r2
end
end
|
