-
Notifications
You must be signed in to change notification settings - Fork 129
/
Interactive.tests
136 lines (104 loc) · 4.81 KB
/
Interactive.tests
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
(*---------------------------------------------------------------------------*)
(* Examples to test ML execution *)
(*---------------------------------------------------------------------------*)
use "Interactive";
Datatype `foo = One | Two`;
Datatype `bar = Alpha
| Beta of 'a
| Delta of ('a # 'b)list
| Elephant of bool list
| Zebra of 'a -> 'b -> bool`;
Datatype `tree = Node of 'a => tree list`;
Function `(mem x [] = F) /\ (mem x (h::t) = (x=h) \/ mem x t)`;
Function `insert x l = if mem x l then l else x::l`;
Weak_Function "tree_els"
`tree_els els (Node x tlist) =
FOLDL (\acc t. tree_els acc t) (insert x els) tlist`;
Weak_Function "occurs"
`occurs x (Node y tlist) = (x=y) \/ EXISTS (occurs x) tlist`;
Datatype `enum = OneA | TwoA | Three | Four of blef list
;
blef = E | G`;
Datatype `Enum = A1 | A2 | A3 | A4 | A5 | A6 | A7 | A8 | A9 | A10
| A11 | A12 | A13 | A14 | A15 | A16 of 'a list list
| A17 | A18 of 'b -> num -> bool | A19 | A20`;
Datatype `prods = P of 'a # 'b # bool # bool # bool # bool # bool
# bool # bool # bool # bool # bool # bool`;
Datatype `funs = Q of 'a => 'b => bool => bool => bool => bool => bool
=> bool => bool => bool => bool => bool => bool`;
load "stringLib";
Datatype `regexp =
Any (* Any character *)
| Epsilon (* Empty string *)
| Atom of char (* Specific character *)
| Or of regexp => regexp (* Union *)
| Then of regexp => regexp (* Concatenation *)
| Repeat of regexp`; (* Iterated concat, >= 0 *)
val _ = remove_termtok{term_name = "COND",tok="=>"};
val _ = overload_on ("|", Term`$Or`);
val _ = overload_on ("#", Term`$Then`);
val _ = set_fixity "|" (Infixr 501);
val _ = set_fixity "#" (Infixr 601);
Weak_Function
"match"
`(match [] [] _ = T)
/\ (match [] _ _ = F)
/\ (match (Epsilon::t) w s = match t w s)
/\ (match (Any::t) [] s = F)
/\ (match (Any::t) (_::w) s = match t w NONE)
/\ (match (Atom c::t) [] s = F)
/\ (match (Atom c::t) (d::w) s = (c=d) /\ match t w NONE)
/\ (match (r1|r2::t) w s = match (r1::t) w s \/ match (r2::t) w s)
/\ (match (r1#r2::t) w s = match (r1::r2::t) w s)
/\ (match (Repeat r::t) w s = let stop = Repeat r::t in
if s = SOME stop then
F
else
match t w s \/
match (r::Repeat r::t) w (SOME stop))`;
try Function `check r s = match [r] (EXPLODE s) NONE`;
val Zero_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "0"))`)));
val One_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "1"))`)));
val Two_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "2"))`)));
val Three_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "3"))`)));
val a_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "a"))`)));
val b_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "b"))`)));
val c_tm = rhs(concl(EVAL(Term`Atom(HD(EXPLODE "c"))`)));
val r0 = Term `^One_tm # ^Two_tm`;
val r1 = Term `Repeat ^r0`
val r2 = Term `Repeat Any # ^One_tm`;
val r3 = Term `^r2 # ^r1`;
termEval (Term `check ^r0 "12"`);
termEval (Term `check ^r1 "12"`);
termEval (Term `check ^r1 "12121212121212121212121212121212"`);
termEval (Term `check ^r1 "12123"`);
(*---------------------------------------------------------------------------*)
(* Testing theory generation. *)
(*---------------------------------------------------------------------------*)
open Drop;
fun EQN defn = DEFN (LIST_CONJ (Defn.eqns_of defn));
fun DATA q = (Hol_datatype q; ParseDatatype.parse q);
val list =
[DATATYPE (ParseDatatype.parse`foo = One | Two`),
DATATYPE (ParseDatatype.parse `tree = Node of 'a => tree list`),
DATATYPE (ParseDatatype.parse `bar = Alpha
| Beta of 'a
| Delta of ('a # 'b)list
| Elephant of bool list
| Zebra of 'a -> 'b -> bool`),
DEFN (Function `(mem x [] = F) /\ (mem x (h::t) = (x=h) \/ mem x t)`),
DEFN (Function `insert x l = if mem x l then l else x::l`),
EQN (Weak_Function "tree_els"
`tree_els els (Node x tlist) =
FOLDL (\acc t. tree_els acc t) (insert x els) tlist`),
EQN (Weak_Function "occurs"
`occurs x (Node y tlist) = (x=y) \/ EXISTS (occurs x) tlist`)];
fun pp_theory (s,elist) =
let open Portable
in pprint pp_sig (s,elist);
pprint pp_struct (s,elist)
end;
pp_theory ("foo",list);
(* Useful for seeing what is going on.
fun printML tm = try (Drop.pp_term_as_ML (Portable.stdOut_ppstream())) tm;
*)