Update from HH
[hl193./.git] / 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