(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Jordan *) (* Copied from HOL Light jordan directory *) (* Author: Thomas C. Hales *) (* Date: 2010-07-08 *) (* ========================================================================== *) module Lib_ext = struct 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);; end;;