Jordan/lib_ext.ml

   1
   2
   3 let rec drop i list =
   4         match (i,list) with (_,[]) -> failwith "drop null"
   5                 | (0,a::b) -> b
   6                 | (i,a::b) -> a::(drop (i-1) b);;
   7
   8 let rec take i j =
   9   function
  10   [] -> [] |
  11   a::b -> match (i,j) with
  12       (0,0) -> [] |
  13       (0,j) -> a::(take 0 (j-1) b) |
  14       _ -> take (i-1) (j-1) b;;
  15
  16 let cannot f x = try (f x; false) with Failure _ -> true;;
  17
  18 (* ------------------------------------------------------------------ *)
  19 (* UNIT TESTS *)
  20 (* ------------------------------------------------------------------ *)
  21
  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
  27   add_test,test;;
  28
  29 let add_test,test = new_test_suite();;
  30
  31
  32 (* ------------------------------------------------------------------ *)
  33 (* LOCAL DEFINITIONS *)
  34 (* ------------------------------------------------------------------ *)
  35
  36 let local_defs = ref ([]:(string * (string * term)) list);;
  37
  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));;
  42
  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
  58   thm;;
  59
  60 let reduce_local_interface(package_name) =
  61   map (reduce_interface o snd)
  62     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  63
  64 let mk_local_interface(package_name) =
  65   map (add_interface o snd)
  66     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  67
  68
  69
  70 (* ------------------------------------------------------------------ *)
  71 (* SAVING STATE *)
  72 (* ------------------------------------------------------------------ *)
  73
  74 (****** Removed for now by JRH
  75
  76 let (save_state,get_state) =
  77   let state_array = ref [] in
  78   let save_state (key:string) =
  79     state_array :=
  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
  84   let get_state key =
  85     let (et,ld,i,tc,tyc,os,ax,def) = assoc key !state_array in
  86       (
  87         EVERY_STEP_TAC := et;
  88         local_defs := ld;
  89         the_interface := i;
  90         the_term_constants:= tc;
  91         the_type_constants:= tyc;
  92         the_overload_skeletons:= os;
  93         the_axioms:= ax;
  94         the_definitions:= def)
  95   in (save_state,get_state);;
  96
  97 save_state "lib_ext";;
  98
  99 *****)