4 match (i,list) with (_,[]) -> failwith "drop null"
6 | (i,a::b) -> a::(drop (i-1) b);;
11 a::b -> match (i,j) with
13 (0,j) -> a::(take 0 (j-1) b) |
14 _ -> take (i-1) (j-1) b;;
16 let cannot f x = try (f x; false) with Failure _ -> true;;
18 (* ------------------------------------------------------------------ *)
20 (* ------------------------------------------------------------------ *)
22 let new_test_suite() =
23 let t = ref ([]:(string*bool) list) in
24 let add_test (s,f) = (t:= ((s,f)::!t)) in
25 let eval (s,f) = if f then () else failwith ("test suite: "^s) in
26 let test() = (ignore (List.map eval (!t));()) in
29 let add_test,test = new_test_suite();;
32 (* ------------------------------------------------------------------ *)
33 (* LOCAL DEFINITIONS *)
34 (* ------------------------------------------------------------------ *)
36 let local_defs = ref ([]:(string * (string * term)) list);;
38 let add_interface (sym,tm) =
39 if (can (assoc sym) (!the_overload_skeletons)) then
40 (overload_interface (sym,tm))
41 else (override_interface(sym,tm));;
43 let local_definition package_name tm =
44 let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
45 let avs,bod = strip_forall tm in
46 let l,r = try dest_eq bod
47 with Failure _ -> failwith "new_local_definition: Not an equation" in
48 let lv,largs = strip_comb l in
49 let cname,ty = dest_var lv in
50 let cname' = package_name^"'"^cname in
51 let lv' = mk_var(cname',ty) in
52 let l' = list_mk_comb(lv',largs) in
53 let bod' = mk_eq(l',r) in
54 let tm'= list_mk_forall(avs,bod') in
55 let thm = new_definition tm' in
56 let _ = (local_defs := (package_name,(cname,lv'))::(!local_defs)) in
57 let _ = add_interface(cname,lv') in
60 let reduce_local_interface(package_name) =
61 map (reduce_interface o snd)
62 (filter (fun x -> ((fst x) = package_name)) !local_defs);;
64 let mk_local_interface(package_name) =
65 map (add_interface o snd)
66 (filter (fun x -> ((fst x) = package_name)) !local_defs);;
70 (* ------------------------------------------------------------------ *)
72 (* ------------------------------------------------------------------ *)
74 (****** Removed for now by JRH
76 let (save_state,get_state) =
77 let state_array = ref [] in
78 let save_state (key:string) =
80 (key,(!EVERY_STEP_TAC,!local_defs,!the_interface,
81 !the_term_constants,!the_type_constants,
82 !the_overload_skeletons,
83 !the_axioms,!the_definitions))::!state_array in
85 let (et,ld,i,tc,tyc,os,ax,def) = assoc key !state_array in
90 the_term_constants:= tc;
91 the_type_constants:= tyc;
92 the_overload_skeletons:= os;
94 the_definitions:= def)
95 in (save_state,get_state);;
97 save_state "lib_ext";;