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
|
let rec drop i list =
match (i,list) with (_,[]) -> failwith "drop null"
| (0,a::b) -> b
| (i,a::b) -> a::(drop (i-1) b);;
let rec take i j =
function
[] -> [] |
a::b -> match (i,j) with
(0,0) -> [] |
(0,j) -> a::(take 0 (j-1) b) |
_ -> take (i-1) (j-1) b;;
let cannot f x = try (f x; false) with Failure _ -> true;;
(* ------------------------------------------------------------------ *)
(* UNIT TESTS *)
(* ------------------------------------------------------------------ *)
let new_test_suite() =
let t = ref ([]:(string*bool) list) in
let add_test (s,f) = (t:= ((s,f)::!t)) in
let eval (s,f) = if f then () else failwith ("test suite: "^s) in
let test() = (ignore (List.map eval (!t));()) in
add_test,test;;
let add_test,test = new_test_suite();;
(* ------------------------------------------------------------------ *)
(* LOCAL DEFINITIONS *)
(* ------------------------------------------------------------------ *)
let local_defs = ref ([]:(string * (string * term)) list);;
let add_interface (sym,tm) =
if (can (assoc sym) (!the_overload_skeletons)) then
(overload_interface (sym,tm))
else (override_interface(sym,tm));;
let local_definition package_name tm =
let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
let avs,bod = strip_forall tm in
let l,r = try dest_eq bod
with Failure _ -> failwith "new_local_definition: Not an equation" in
let lv,largs = strip_comb l in
let cname,ty = dest_var lv in
let cname' = package_name^"'"^cname in
let lv' = mk_var(cname',ty) in
let l' = list_mk_comb(lv',largs) in
let bod' = mk_eq(l',r) in
let tm'= list_mk_forall(avs,bod') in
let thm = new_definition tm' in
let _ = (local_defs := (package_name,(cname,lv'))::(!local_defs)) in
let _ = add_interface(cname,lv') in
thm;;
let reduce_local_interface(package_name) =
map (reduce_interface o snd)
(filter (fun x -> ((fst x) = package_name)) !local_defs);;
let mk_local_interface(package_name) =
map (add_interface o snd)
(filter (fun x -> ((fst x) = package_name)) !local_defs);;
(* ------------------------------------------------------------------ *)
(* SAVING STATE *)
(* ------------------------------------------------------------------ *)
(****** Removed for now by JRH
let (save_state,get_state) =
let state_array = ref [] in
let save_state (key:string) =
state_array :=
(key,(!EVERY_STEP_TAC,!local_defs,!the_interface,
!the_term_constants,!the_type_constants,
!the_overload_skeletons,
!the_axioms,!the_definitions))::!state_array in
let get_state key =
let (et,ld,i,tc,tyc,os,ax,def) = assoc key !state_array in
(
EVERY_STEP_TAC := et;
local_defs := ld;
the_interface := i;
the_term_constants:= tc;
the_type_constants:= tyc;
the_overload_skeletons:= os;
the_axioms:= ax;
the_definitions:= def)
in (save_state,get_state);;
save_state "lib_ext";;
*****)
|
