author | Chengsong |
Fri, 26 May 2023 08:09:30 +0100 | |
changeset 646 | 56057198e4f5 |
parent 156 | 6a43ea9305ba |
permissions | -rw-r--r-- |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
type rexp = |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
3 |
ZERO |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
4 |
| ONE |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
| CHAR of char |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
| ALT of rexp * rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
| SEQ of rexp * rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
| STAR of rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
| RECD of string * rexp;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
type value = |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
12 |
Empty |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
| Chr of char |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
| Sequ of value * value |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
| Left of value |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
| Right of value |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
| Stars of value list |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
| Rec of string * value;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
let rec string_of_val v = match v with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
21 |
Empty -> "Empty" |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
| Chr(c) -> String.make 1 c |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
| Sequ(v1, v2) -> "Seq(" ^ string_of_val v1 ^ "," ^ string_of_val v2 ^ ")" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
| Left(v1) -> "Left(" ^ string_of_val v1 ^ ")" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
| Right(v1) -> "Right(" ^ string_of_val v1 ^ ")" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
| Stars(vs) -> "[" ^ String.concat "," (List.map string_of_val vs) ^ "]" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
| Rec(x, v1) -> x ^ " $ " ^ string_of_val v1;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
(* some helper functions for strings *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
let explode s = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
let rec exp i l = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
if i < 0 then l else exp (i - 1) (s.[i] :: l) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
exp (String.length s - 1) [];; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
let string_repeat s n = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
Array.fold_left (^) "" (Array.make n s);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
(* some helper functions for rexps *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
let rec seq s = match s with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
41 |
[] -> ONE |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
| [c] -> CHAR(c) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
| c::cs -> SEQ(CHAR(c), seq cs);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
let chr c = CHAR(c) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
let str s = seq(explode s);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
let plus r = SEQ(r, STAR(r));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
let (++) r1 r2 = ALT(r1, r2);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
let (--) r1 r2 = SEQ(r1, r2);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
let ($) x r = RECD(x, r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
let alts rs = match rs with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
58 |
[] -> ZERO |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
| [r] -> r |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
| r::rs -> List.fold_left (++) r rs;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
(* size of a regular expressions - for testing purposes *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
let rec size r = match r with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
65 |
ZERO -> 1 |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
66 |
| ONE -> 1 |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
| CHAR(_) -> 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
| ALT(r1, r2) -> 1 + (size r1) + (size r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
| SEQ(r1, r2) -> 1 + (size r1) + (size r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
| STAR(r) -> 1 + (size r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
| RECD(_, r) -> 1 + (size r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
73 |
(* nullable function: tests whether the regular |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
expression can recognise the empty string *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
let rec nullable r = match r with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
76 |
ZERO -> false |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
77 |
| ONE -> true |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
78 |
| CHAR(_) -> false |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
| ALT(r1, r2) -> nullable(r1) || nullable(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
| SEQ(r1, r2) -> nullable(r1) && nullable(r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
81 |
| STAR(_) -> true |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
82 |
| RECD(_, r) -> nullable(r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
83 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
84 |
(* derivative of a regular expression r w.r.t. a character c *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
85 |
let rec der c r = match r with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
86 |
ZERO -> ZERO |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
87 |
| ONE -> ZERO |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
88 |
| CHAR(d) -> if c = d then ONE else ZERO |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
| ALT(r1, r2) -> ALT(der c r1, der c r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
| SEQ(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
91 |
if nullable r1 then ALT(SEQ(der c r1, r2), der c r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
else SEQ(der c r1, r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
| STAR(r) -> SEQ(der c r, STAR(r)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
| RECD(_, r) -> der c r;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
95 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
(* derivative w.r.t. a list of chars (iterates der) *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
97 |
let rec ders s r = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
98 |
[] -> r |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
99 |
| c::s -> ders s (der c r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
(* extracts a string from value *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
let rec flatten v = match v with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
103 |
Empty -> "" |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
| Chr(c) -> String.make 1 c |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
| Left(v) -> flatten v |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
| Right(v) -> flatten v |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
| Sequ(v1, v2) -> flatten v1 ^ flatten v2 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
| Stars(vs) -> String.concat "" (List.map flatten vs) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
| Rec(_, v) -> flatten v;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
(* extracts an environment from a value *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
113 |
let rec env v = match v with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
114 |
Empty -> [] |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
| Chr(c) -> [] |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
| Left(v) -> env v |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
| Right(v) -> env v |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
| Sequ(v1, v2) -> env v1 @ env v2 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
| Stars(vs) -> List.flatten (List.map env vs) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
| Rec(x, v) -> (x, flatten v) :: env v;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
let string_of_pair (x, s) = "(" ^ x ^ "," ^ s ^ ")";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
let string_of_env xs = String.concat "," (List.map string_of_pair xs);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
124 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
125 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
(* the value for a nullable rexp *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
let rec mkeps r = match r with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
128 |
ONE -> Empty |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
| ALT(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
if nullable r1 then Left(mkeps r1) else Right(mkeps r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
| SEQ(r1, r2) -> Sequ(mkeps r1, mkeps r2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
| STAR(r) -> Stars([]) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
| RECD(x, r) -> Rec(x, mkeps r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
(* injection of a char into a value *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
let rec inj r c v = match r, v with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
STAR(r), Sequ(v1, Stars(vs)) -> Stars(inj r c v1 :: vs) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
| SEQ(r1, r2), Sequ(v1, v2) -> Sequ(inj r1 c v1, v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
| SEQ(r1, r2), Left(Sequ(v1, v2)) -> Sequ(inj r1 c v1, v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
| SEQ(r1, r2), Right(v2) -> Sequ(mkeps r1, inj r2 c v2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
| ALT(r1, r2), Left(v1) -> Left(inj r1 c v1) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
| ALT(r1, r2), Right(v2) -> Right(inj r2 c v2) |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
144 |
| CHAR(d), Empty -> Chr(d) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
| RECD(x, r1), _ -> Rec(x, inj r1 c v);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
147 |
(* some "rectification" functions for simplification *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
let f_id v = v;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
let f_right f = fun v -> Right(f v);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
let f_left f = fun v -> Left(f v);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
let f_alt f1 f2 = fun v -> match v with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
152 |
Right(v) -> Right(f2 v) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
153 |
| Left(v) -> Left(f1 v);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
154 |
let f_seq f1 f2 = fun v -> match v with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
Sequ(v1, v2) -> Sequ(f1 v1, f2 v2);; |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
156 |
let f_seq_Empty1 f1 f2 = fun v -> Sequ(f1 Empty, f2 v);; |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
157 |
let f_seq_Empty2 f1 f2 = fun v -> Sequ(f1 v, f2 Empty);; |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
let f_rec f = fun v -> match v with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
159 |
Rec(x, v) -> Rec(x, f v);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
160 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
exception ShouldNotHappen |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
let f_error v = raise ShouldNotHappen |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
(* simplification of regular expressions returning also an |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
rectification function; no simplification under STARs *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
let rec simp r = match r with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
ALT(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
168 |
let (r1s, f1s) = simp r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
169 |
let (r2s, f2s) = simp r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
170 |
(match r1s, r2s with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
171 |
ZERO, _ -> (r2s, f_right f2s) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
172 |
| _, ZERO -> (r1s, f_left f1s) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
| _, _ -> if r1s = r2s then (r1s, f_left f1s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
else (ALT (r1s, r2s), f_alt f1s f2s)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
| SEQ(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
let (r1s, f1s) = simp r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
let (r2s, f2s) = simp r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
(match r1s, r2s with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
179 |
ZERO, _ -> (ZERO, f_error) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
180 |
| _, ZERO -> (ZERO, f_error) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
181 |
| ONE, _ -> (r2s, f_seq_Empty1 f1s f2s) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
182 |
| _, ONE -> (r1s, f_seq_Empty2 f1s f2s) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
| _, _ -> (SEQ(r1s, r2s), f_seq f1s f2s)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
| RECD(x, r1) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
let (r1s, f1s) = simp r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
(RECD(x, r1s), f_rec f1s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
| r -> (r, f_id) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
188 |
;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
let rec der_simp c r = match r with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
191 |
ZERO -> (ZERO, f_id) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
192 |
| ONE -> (ZERO, f_id) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
193 |
| CHAR(d) -> ((if c = d then ONE else ZERO), f_id) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
194 |
| ALT(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
195 |
let (r1d, f1d) = der_simp c r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
196 |
let (r2d, f2d) = der_simp c r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
197 |
(match r1d, r2d with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
198 |
ZERO, _ -> (r2d, f_right f2d) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
199 |
| _, ZERO -> (r1d, f_left f1d) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
200 |
| _, _ -> if r1d = r2d then (r1d, f_left f1d) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
201 |
else (ALT (r1d, r2d), f_alt f1d f2d)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
202 |
| SEQ(r1, r2) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
203 |
if nullable r1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
204 |
then |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
let (r1d, f1d) = der_simp c r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
206 |
let (r2d, f2d) = der_simp c r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
207 |
let (r2s, f2s) = simp r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
(match r1d, r2s, r2d with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
209 |
ZERO, _, _ -> (r2d, f_right f2d) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
210 |
| _, ZERO, _ -> (r2d, f_right f2d) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
211 |
| _, _, ZERO -> (SEQ(r1d, r2s), f_left (f_seq f1d f2s)) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
212 |
| ONE, _, _ -> (ALT(r2s, r2d), f_alt (f_seq_Empty1 f1d f2s) f2d) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
213 |
| _, ONE, _ -> (ALT(r1d, r2d), f_alt (f_seq_Empty2 f1d f2s) f2d) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
214 |
| _, _, _ -> (ALT(SEQ(r1d, r2s), r2d), f_alt (f_seq f1d f2s) f2d)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
215 |
else |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
216 |
let (r1d, f1d) = der_simp c r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
217 |
let (r2s, f2s) = simp r2 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
218 |
(match r1d, r2s with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
219 |
ZERO, _ -> (ZERO, f_error) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
220 |
| _, ZERO -> (ZERO, f_error) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
221 |
| ONE, _ -> (r2s, f_seq_Empty1 f1d f2s) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
222 |
| _, ONE -> (r1d, f_seq_Empty2 f1d f2s) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
223 |
| _, _ -> (SEQ(r1d, r2s), f_seq f1d f2s)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
224 |
| STAR(r1) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
225 |
let (r1d, f1d) = der_simp c r1 in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
226 |
(match r1d with |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
227 |
ZERO -> (ZERO, f_error) |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
228 |
| ONE -> (STAR r1, f_seq_Empty1 f1d f_id) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
229 |
| _ -> (SEQ(r1d, STAR(r1)), f_seq f1d f_id)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
230 |
| RECD(x, r1) -> der_simp c r1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
231 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
232 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
233 |
(* matcher function *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
234 |
let matcher r s = nullable(ders (explode s) r);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
235 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
236 |
(* lexing function (produces a value) *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
237 |
exception LexError;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
238 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
239 |
let rec lex r s = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
240 |
[] -> if (nullable r) then mkeps r else raise LexError |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
241 |
| c::cs -> inj r c (lex (der c r) cs);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
242 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
243 |
let lexing r s = lex r (explode s);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
244 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
245 |
(* lexing with simplification *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
246 |
let rec lex_simp r s = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
247 |
[] -> if (nullable r) then mkeps r else raise LexError |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
248 |
| c::cs -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
249 |
let (r_simp, f_simp) = simp (der c r) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
250 |
inj r c (f_simp (lex_simp r_simp cs));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
251 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
252 |
let lexing_simp r s = lex_simp r (explode s);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
253 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
254 |
let rec lex_simp2 r s = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
255 |
[] -> if (nullable r) then mkeps r else raise LexError |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
256 |
| c::cs -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
257 |
let (r_simp, f_simp) = der_simp c r in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
258 |
inj r c (f_simp (lex_simp2 r_simp cs));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
259 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
260 |
let lexing_simp2 r s = lex_simp2 r (explode s);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
261 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
262 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
263 |
(* lexing with accumulation *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
264 |
let rec lex_acc r s f = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
265 |
[] -> if (nullable r) then f (mkeps r) else raise LexError |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
266 |
| c::cs -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
267 |
let (r_simp, f_simp) = simp (der c r) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
268 |
lex_acc r_simp cs (fun v -> f (inj r c (f_simp v)));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
269 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
270 |
let lexing_acc r s = lex_acc r (explode s) (f_id);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
271 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
272 |
let rec lex_acc2 r s f = match s with |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
273 |
[] -> if (nullable r) then f (mkeps r) else raise LexError |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
274 |
| c::cs -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
275 |
let (r_simp, f_simp) = der_simp c r in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
276 |
lex_acc2 r_simp cs (fun v -> f (inj r c (f_simp v)));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
277 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
278 |
let lexing_acc2 r s = lex_acc2 r (explode s) (f_id);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
279 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
(* Lexing rules for a small WHILE language *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
282 |
let sym = alts (List.map chr (explode "abcdefghijklmnopqrstuvwxyz"));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
let digit = alts (List.map chr (explode "0123456789"));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
let idents = sym -- STAR(sym ++ digit);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
let nums = plus(digit);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
let keywords = alts |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
(List.map str ["skip"; "while"; "do"; "if"; "then"; "else"; "read"; "write"; "true"; "false"]);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
288 |
let semicolon = str ";" |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
289 |
let ops = alts |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
290 |
(List.map str [":="; "=="; "-"; "+"; "*"; "!="; "<"; ">"; "<="; ">="; "%"; "/"]);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
291 |
let whitespace = plus(str " " ++ str "\n" ++ str "\t");; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
292 |
let rparen = str ")";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
293 |
let lparen = str "(";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
let begin_paren = str "{";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
295 |
let end_paren = str "}";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
296 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
297 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
298 |
let while_regs = STAR(("k" $ keywords) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
299 |
("i" $ idents) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
300 |
("o" $ ops) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
301 |
("n" $ nums) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
302 |
("s" $ semicolon) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
303 |
("p" $ (lparen ++ rparen)) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
304 |
("b" $ (begin_paren ++ end_paren)) ++ |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
305 |
("w" $ whitespace));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
306 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
307 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
308 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
309 |
(* Some Tests |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
310 |
============ *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
311 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
let time f x = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
313 |
let t = Sys.time() in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
let f_x = (f x; f x; f x) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
315 |
(print_float ((Sys.time() -. t) /. 3.0); f_x);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
316 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
317 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
318 |
let prog0 = "read n";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
319 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
320 |
let prog1 = "read n; write (n)";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
321 |
string_of_env (env (lexing_simp while_regs prog1));; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
322 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
323 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
324 |
let prog2 = " |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
325 |
i := 2; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
326 |
max := 100; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
327 |
while i < max do { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
328 |
isprime := 1; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
329 |
j := 2; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
330 |
while (j * j) <= i + 1 do { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
331 |
if i % j == 0 then isprime := 0 else skip; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
332 |
j := j + 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
333 |
}; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
334 |
if isprime == 1 then write i else skip; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
335 |
i := i + 1 |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
336 |
}";; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
337 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
338 |
let tst1 = (lexing_simp while_regs prog2 = lexing_simp2 while_regs prog2) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
339 |
let tst2 = (lexing_simp while_regs prog2 = lexing_acc while_regs prog2) in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
340 |
let tst3 = (lexing_simp while_regs prog2 = lexing_acc2 while_regs prog2) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
341 |
in |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
342 |
print_string ("Sanity test simp vs simp2: >>" ^ (string_of_bool tst1) ^ "<<\n") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
343 |
print_string ("Sanity test simp vs acc: >>" ^ (string_of_bool tst2) ^ "<<\n") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
344 |
print_string ("Sanity test simp vs acc2: >>" ^ (string_of_bool tst3) ^ "<<") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
345 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
346 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
347 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
348 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
349 |
type range = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
350 |
To of int * int;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
351 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
352 |
let (---) i j = To(i, j);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
353 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
354 |
let forby n = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
355 |
fun range -> match range with To(lo, up) -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
356 |
(fun f -> |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
357 |
let rec loop lo = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
358 |
if lo > up then () else (f lo; loop (lo + n)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
359 |
in loop lo);; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
360 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
361 |
let step_simp i = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
362 |
(print_string ((string_of_int i) ^ ": ") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
363 |
time (lexing_simp while_regs) (string_repeat prog2 i) ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
364 |
print_newline ());; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
365 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
366 |
let step_simp2 i = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
367 |
(print_string ((string_of_int i) ^ ": ") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
368 |
time (lexing_simp2 while_regs) (string_repeat prog2 i) ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
369 |
print_newline ());; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
370 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
371 |
let step_acc i = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
372 |
(print_string ((string_of_int i) ^ ": ") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
373 |
time (lexing_acc while_regs) (string_repeat prog2 i) ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
374 |
print_newline ());; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
375 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
376 |
let step_acc2 i = |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
377 |
(print_string ((string_of_int i) ^ ": ") ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
378 |
time (lexing_acc2 while_regs) (string_repeat prog2 i) ; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
379 |
print_newline ());; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
380 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
381 |
forby 100 (100 --- 700) step_simp;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
382 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
383 |
forby 100 (100 --- 700) step_simp2;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
384 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
385 |
forby 100 (100 --- 700) step_acc;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
386 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
387 |
forby 100 (100 --- 700) step_acc2;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
388 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
389 |
forby 1000 (1000 --- 5000) step_acc;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
390 |
print_newline ();; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
391 |
forby 1000 (1000 --- 5000) step_acc2;; |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
392 |
(*print_newline ();;*) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
393 |
(* forby 500 (100 --- 5000) step_simp;; *) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
394 |