text_formalization/general/package_constant.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* General Utility                                                            *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-02-11                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* ------------------------------------------------------------------ *)
  11 (* LOCAL DEFINITIONS , from Jordan curve lib_ext.ml *)
  12 (* ------------------------------------------------------------------ *)
  13
  14
  15
  16 module type Local_definition_type = sig
  17
  18
  19 end;;
  20
  21
  22 module Local_definition  : Local_definition_type = struct
  23
  24 let local_defs = ref ([]:(string * (string * term)) list);;
  25
  26 let add_interface (sym,tm) =
  27   if (can (assoc sym) (!the_overload_skeletons)) then
  28     (overload_interface (sym,tm))
  29   else (override_interface(sym,tm));;
  30
  31 let local_definition package_name tm =
  32   let list_mk_forall(vars,bod) = itlist (curry mk_forall) vars bod in
  33   let avs,bod = strip_forall tm in
  34   let l,r = try dest_eq bod
  35     with Failure _ -> failwith "new_local_definition: Not an equation" in
  36   let lv,largs = strip_comb l in
  37   let cname,ty = dest_var lv in
  38   let cname' = package_name^"'"^cname in
  39   let lv' = mk_var(cname',ty) in
  40   let l' = list_mk_comb(lv',largs) in
  41   let bod' = mk_eq(l',r) in
  42   let tm'= list_mk_forall(avs,bod') in
  43   let thm = new_definition tm' in
  44   let _ = (local_defs := (package_name,(cname,lv'))::(!local_defs)) in
  45   let _ = add_interface(cname,lv') in
  46   thm;;
  47
  48 let reduce_local_interface(package_name) =
  49   map (reduce_interface o snd)
  50     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  51
  52 let mk_local_interface(package_name) =
  53   map (add_interface o snd)
  54     (filter (fun x -> ((fst x) = package_name)) !local_defs);;
  55
  56
  57 (* adapted from HOL Light code, true if it is a local def. *)
  58
  59 let is_benign =
  60   fun tm ->
  61     let tm' = snd(strip_forall tm) in
  62     try let th,th' = tryfind (fun th -> th,PART_MATCH I th tm')
  63                              (!the_definitions) in
  64         (can (PART_MATCH I th') (concl th))
  65     with Failure _ -> false;;
  66
  67 end;;