Jordan/tactics_refine.ml

   1
   2 (* ------------------------------------------------------------------ *)
   3 (* This bundles an interactive session into a proof. *)
   4 (* ------------------------------------------------------------------ *)
   5
   6 let labels_flag = ref false;;
   7
   8
   9 let LABEL_ALL_TAC:tactic =
  10  let mk_label avoid =
  11   let rec mk_one_label i avoid  =
  12     let label = "Z-"^(string_of_int i) in
  13       if not(mem label avoid) then label else mk_one_label (i+1) avoid in
  14     mk_one_label 0 avoid in
  15  let update_label i asl =
  16   let rec f_at_i f j =
  17     function [] -> []
  18       | a::b -> if (j=0) then (f a)::b else a::(f_at_i f (j-1) b) in
  19   let avoid = map fst asl in
  20   let current = el i avoid in
  21   let new_label = mk_label avoid in
  22   if (String.length current > 0) then asl else
  23     f_at_i (fun (_,y) -> (new_label,y) ) i asl in
  24   fun (asl,w) ->
  25     let aslp = ref asl in
  26     (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
  27     (ALL_TAC (!aslp,w)));;
  28
  29 (* global_var *)
  30 let (EVERY_STEP_TAC:tactic ref) = ref ALL_TAC;;
  31
  32 let (e:tactic ->goalstack) =
  33    fun tac -> refine(by(VALID
  34    (if !labels_flag then (tac THEN (!EVERY_STEP_TAC)) THEN LABEL_ALL_TAC
  35    else tac)));;
  36
  37 let has_stv t =
  38   let typ = (type_vars_in_term t) in
  39   can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
  40
  41 let prove_by_refinement(t,(tacl:tactic list)) =
  42   if (length (frees t) > 0)
  43     then failwith "prove_by_refinement: free vars" else
  44   if (has_stv t)
  45     then failwith "prove_by_refinement: has stv" else
  46   let gstate = mk_goalstate ([],t) in
  47   let _,sgs,just = rev_itlist
  48     (fun tac gs -> by
  49        (if !labels_flag then (tac THEN
  50          (!EVERY_STEP_TAC) THEN LABEL_ALL_TAC ) else tac) gs)
  51      tacl gstate in
  52   let th = if sgs = [] then just null_inst []
  53   else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  54   let t' = concl th in
  55   if t' = t then th else
  56   try EQ_MP (ALPHA t' t) th
  57   with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;
  58
  59
  60 (* ------------------------------------------------------------------ *)
  61 (* DUMPING AND PRELOADED THEOREMS *)
  62 (* ------------------------------------------------------------------ *)
  63
  64
  65 let saved_thm = ref ((Hashtbl.create 300):(term,thm) Hashtbl.t);;
  66 let save_thm thm = Hashtbl.add !saved_thm (concl thm) thm;;
  67 let mem_thm tm = Hashtbl.mem !saved_thm tm;;
  68 let remove_thm tm = Hashtbl.remove !saved_thm tm;;
  69 let find_thm tm = Hashtbl.find !saved_thm tm;;
  70
  71 let dump_thm file_name =
  72     let ch = open_out_bin file_name in
  73     (output_value ch !saved_thm;
  74     close_out ch);;
  75
  76 let load_thm file_name =
  77   let ch = open_in_bin file_name in
  78   (saved_thm := input_value ch;
  79    close_in ch);;
  80
  81 (* ------------------------------------------------------------------ *)
  82 (* PROOFS STORED.  *)
  83 (* ------------------------------------------------------------------ *)
  84
  85 let old_prove = prove;;
  86 let old_prove_by_refinement = prove_by_refinement;;
  87 let fast_load  = ref true;;
  88
  89 let set_fast_load file_name =
  90   (fast_load := true;
  91   load_thm file_name);;
  92
  93 let set_slow_load () =
  94   (fast_load := false;);;
  95
  96 let prove (x, tac) =
  97   if (!fast_load) then (try(find_thm x) with failure -> old_prove(x,tac))
  98   else (let t = old_prove(x,tac) in (save_thm t; t));;
  99
 100 let prove_by_refinement (x, tacl) =
 101   if (!fast_load) then (try(find_thm x)
 102                         with failure -> old_prove_by_refinement(x,tacl))
 103   else (let t = old_prove_by_refinement(x,tacl) in (save_thm t; t));;
 104
 105 if (false) then (set_fast_load "thm.dump") else (fast_load:=false);;
 106