(* ------------------------------------------------------------------ *)
(* This bundles an interactive session into a proof. *)
(* ------------------------------------------------------------------ *)

let labels_flag = ref false;;


let LABEL_ALL_TAC:tactic = 
 let mk_label avoid =
  let rec mk_one_label i avoid  = 
    let label = "Z-"^(string_of_int i) in
      if not(mem label avoid) then label else mk_one_label (i+1) avoid in
    mk_one_label 0 avoid in
 let update_label i asl = 
  let rec f_at_i f j =
    function [] -> []
      | a::b -> if (j=0) then (f a)::b else a::(f_at_i f (j-1) b) in
  let avoid = map fst asl in
  let current = el i avoid in
  let new_label = mk_label avoid in
  if (String.length current > 0) then asl else 
    f_at_i (fun (_,y) -> (new_label,y) ) i asl in
  fun (asl,w) ->  
    let aslp = ref asl in
    (for i=0 to ((length asl)-1) do (aslp := update_label i !aslp) done;
    (ALL_TAC (!aslp,w)));;

(* global_var *)
let (EVERY_STEP_TAC:tactic ref) = ref ALL_TAC;;

let (e:tactic ->goalstack) =  
   fun tac -> refine(by(VALID 
   (if !labels_flag then (tac THEN (!EVERY_STEP_TAC)) THEN LABEL_ALL_TAC
   else tac)));;

let has_stv t = 
  let typ = (type_vars_in_term t) in
  can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;

let prove_by_refinement(t,(tacl:tactic list)) = 
  if (length (frees t) > 0) 
    then failwith "prove_by_refinement: free vars" else
  if (has_stv t) 
    then failwith "prove_by_refinement: has stv" else
  let gstate = mk_goalstate ([],t) in
  let _,sgs,just = rev_itlist 
    (fun tac gs -> by 
       (if !labels_flag then (tac THEN 
         (!EVERY_STEP_TAC) THEN LABEL_ALL_TAC ) else tac) gs)
     tacl gstate in
  let th = if sgs = [] then just null_inst []
  else failwith "BY_REFINEMENT_PROOF: Unsolved goals" in
  let t' = concl th in
  if t' = t then th else
  try EQ_MP (ALPHA t' t) th
  with Failure _ -> failwith "prove_by_refinement: generated wrong theorem";;


(* ------------------------------------------------------------------ *)
(* DUMPING AND PRELOADED THEOREMS *)
(* ------------------------------------------------------------------ *)


let saved_thm = ref ((Hashtbl.create 300):(term,thm) Hashtbl.t);;
let save_thm thm = Hashtbl.add !saved_thm (concl thm) thm;;
let mem_thm tm = Hashtbl.mem !saved_thm tm;;
let remove_thm tm = Hashtbl.remove !saved_thm tm;;
let find_thm tm = Hashtbl.find !saved_thm tm;;

let dump_thm file_name = 
    let ch = open_out_bin file_name in
    (output_value ch !saved_thm;
    close_out ch);;

let load_thm file_name =
  let ch = open_in_bin file_name in 
  (saved_thm := input_value ch;
   close_in ch);;

(* ------------------------------------------------------------------ *)
(* PROOFS STORED.  *)
(* ------------------------------------------------------------------ *)

let old_prove = prove;;
let old_prove_by_refinement = prove_by_refinement;;
let fast_load  = ref true;;

let set_fast_load file_name =
  (fast_load := true;
  load_thm file_name);;

let set_slow_load () = 
  (fast_load := false;);;

let prove (x, tac) = 
  if (!fast_load) then (try(find_thm x) with failure -> old_prove(x,tac))
  else (let t = old_prove(x,tac) in (save_thm t; t));;

let prove_by_refinement (x, tacl) = 
  if (!fast_load) then (try(find_thm x) 
			with failure -> old_prove_by_refinement(x,tacl))
  else (let t = old_prove_by_refinement(x,tacl) in (save_thm t; t));;

if (false) then (set_fast_load "thm.dump") else (fast_load:=false);;