text_formalization/jordan/lib_ext.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10 module Lib_ext = struct
  11
  12 let rec drop i list =
  13         match (i,list) with (_,[]) -> failwith "drop null"
  14                 | (0,a::b) -> b
  15                 | (i,a::b) -> a::(drop (i-1) b);;
  16
  17 let rec take i j =
  18   function
  19   [] -> [] |
  20   a::b -> match (i,j) with
  21       (0,0) -> [] |
  22       (0,j) -> a::(take 0 (j-1) b) |
  23       _ -> take (i-1) (j-1) b;;
  24
  25 let cannot f x = try (f x; false) with Failure _ -> true;;
  26
  27 (* ------------------------------------------------------------------ *)
  28 (* UNIT TESTS *)
  29 (* ------------------------------------------------------------------ *)
  30
  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
  36   add_test,test;;
  37
  38 let add_test,test = new_test_suite();;
  39
  40
  41 (* ------------------------------------------------------------------ *)
  42 (* LOCAL DEFINITIONS *)
  43 (* ------------------------------------------------------------------ *)
  44
  45 let local_defs = ref ([]:(string * (string * term)) list);;
  46
  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));;
  51
  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
  67   thm;;
  68
  69 let reduce_local_interface(package_name) =
  70   map (reduce_interface o snd)
  71     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  72
  73 let mk_local_interface(package_name) =
  74   map (add_interface o snd)
  75     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  76
  77
  78
  79 end;;