1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Copied from HOL Light jordan directory *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 module Lib_ext = struct
13 match (i,list) with (_,[]) -> failwith "drop null"
15 | (i,a::b) -> a::(drop (i-1) b);;
20 a::b -> match (i,j) with
22 (0,j) -> a::(take 0 (j-1) b) |
23 _ -> take (i-1) (j-1) b;;
25 let cannot f x = try (f x; false) with Failure _ -> true;;
27 (* ------------------------------------------------------------------ *)
29 (* ------------------------------------------------------------------ *)
31 let new_test_suite() =
32 let t = ref ([]:(string*bool) list) in
33 let add_test (s,f) = (t:= ((s,f)::!t)) in
34 let eval (s,f) = if f then () else failwith ("test suite: "^s) in
35 let test() = (ignore (List.map eval (!t));()) in
38 let add_test,test = new_test_suite();;
41 (* ------------------------------------------------------------------ *)
42 (* LOCAL DEFINITIONS *)
43 (* ------------------------------------------------------------------ *)
45 let local_defs = ref ([]:(string * (string * term)) list);;
47 let add_interface (sym,tm) =
48 if (can (assoc sym) (!the_overload_skeletons)) then
49 (overload_interface (sym,tm))
50 else (override_interface(sym,tm));;
52 let local_definition package_name tm =
53 let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
54 let avs,bod = strip_forall tm in
55 let l,r = try dest_eq bod
56 with Failure _ -> failwith "new_local_definition: Not an equation" in
57 let lv,largs = strip_comb l in
58 let cname,ty = dest_var lv in
59 let cname' = package_name^"'"^cname in
60 let lv' = mk_var(cname',ty) in
61 let l' = list_mk_comb(lv',largs) in
62 let bod' = mk_eq(l',r) in
63 let tm'= list_mk_forall(avs,bod') in
64 let thm = new_definition tm' in
65 let _ = (local_defs := (package_name,(cname,lv'))::(!local_defs)) in
66 let _ = add_interface(cname,lv') in
69 let reduce_local_interface(package_name) =
70 map (reduce_interface o snd)
71 (filter (fun x -> ((fst x) = package_name)) !local_defs);;
73 let mk_local_interface(package_name) =
74 map (add_interface o snd)
75 (filter (fun x -> ((fst x) = package_name)) !local_defs);;