Update from HH
[hl193./.git] / IsabelleLight / support.ml
1 (* ========================================================================= *)
2 (*                              Isabelle Light                               *)
3 (*   Isabelle/Procedural style additions and other user-friendly shortcuts.  *)
4 (*                                                                           *)
5 (*                   Petros Papapanagiotou, Jacques Fleuriot                 *)
6 (*              Center of Intelligent Systems and their Applications         *)
7 (*                          University of Edinburgh                          *)
8 (*                                 2009-2012                                 *)
9 (* ========================================================================= *)
10 (* FILE         : support.ml                                                 *)
11 (* DESCRIPTION  : Support functions and various shortcuts.                   *)
12 (* LAST MODIFIED: October 2012                                               *)
13 (* ========================================================================= *)
14
15 (* ------------------------------------------------------------------------- *)
16 (* Functions to deal with triplets:                                          *)
17 (* ------------------------------------------------------------------------- *)
18
19 let fst3 (x,_,_) = x;;
20 let snd3 (_,x,_) = x;;
21 let thd3 (_,_,x) = x;;
22
23
24 (*----------------------------------------------------------------------------*)
25 (* num_list : a' list -> (a' * int) list                                      *)
26 (*                                                                            *)
27 (* Numbers a list of elements,                                                *)
28 (* e.g. [`a`;`b`;`c`] ---> [(0,`a`);(1,`b`);(2,`c`)].                         *)
29 (*----------------------------------------------------------------------------*)
30
31 let num_list l =
32    let rec number_list' n l =
33       if ( l = [] ) then []
34       else (n,hd l)::(number_list' (n + 1) (tl l))
35    in number_list' 0 l;;
36
37
38 (* ------------------------------------------------------------------------- *)
39 (* list_match_first: (a' -> b') -> a' list -> b'                             *)
40 (* Tries to apply a function to the members of a list. Returns the result    *)
41 (* from the first member that succeeds.                                      *)
42 (* ------------------------------------------------------------------------- *)
43
44 let rec list_match_first f alist =
45   if (alist = []) then failwith "list_match_first: No matches!"
46   else try f (hd alist) with Failure _ -> list_match_first f (tl alist);;
47
48
49 (* ------------------------------------------------------------------------- *)
50 (* terms_match: term list -> term -> term list -> instantiation              *)
51 (* Tries to apply term_match to the first possible term in a list.           *)
52 (* Returns the insantiation.                                                 *)
53 (* ------------------------------------------------------------------------- *)
54
55 let (terms_match: term list -> term -> term list -> instantiation ) =
56   fun consts key tlist ->
57     try (list_match_first (term_match consts key) tlist)
58     with Failure _ -> failwith "terms_match: No terms match!";;
59
60
61 (* ------------------------------------------------------------------------- *)
62 (* thm_mk_primed_vars: term list -> thm -> thm                               *)
63 (* Renames all free variables in a theorem to avoid specified and constant   *)
64 (* names.                                                                    *)
65 (* ------------------------------------------------------------------------- *)
66
67 let thm_mk_primed_vars avoids thm =
68   let fvars = thm_frees thm in
69   let new_vars = map (mk_primed_var avoids) fvars in
70   let insts = List.combine new_vars fvars in
71   INST insts thm;;
72
73
74 (* ------------------------------------------------------------------------- *)
75 (* gl_frees: goal -> term list                                               *)
76 (* Finds the free variables in a subgoal (assumptions and goal).             *)
77 (* ------------------------------------------------------------------------- *)
78
79 let gl_frees : goal -> term list =
80   fun (asl,w) -> itlist (union o thm_frees o snd) asl (frees w);;
81
82
83 (* ------------------------------------------------------------------------- *)
84 (* ADD_HYP: thm -> thm -> thm                                                *)
85 (* Trivially adds the hypotheses of a theorem to the premises of another.    *)
86 (* ------------------------------------------------------------------------- *)
87 (* (+) Used in the justification of erule and drule to add the eliminated    *)
88 (* assumption to the proven subgoals.                                        *)
89 (* (+) Could have been based on ADD_ASSUM but it's more convenient this way. *)
90 (* ------------------------------------------------------------------------- *)
91
92 let ADD_HYP hyp_thm thm = CONJUNCT2 (CONJ hyp_thm thm);;
93
94
95 (* ------------------------------------------------------------------------- *)
96 (* DISCHL: term list -> thm -> thm                                           *)
97 (* Applies DISCH for several terms.                                          *)
98 (* ------------------------------------------------------------------------- *)
99
100 let rec (DISCHL: term list -> thm -> thm) =
101   fun tms thm ->
102     if (tms = []) then thm
103         else DISCH (hd tms) (DISCHL (tl tms) thm);;
104
105
106 (* ------------------------------------------------------------------------- *)
107 (* print_thl:                                                                *)
108 (* Print a list of theorems (for debugging).                                 *)
109 (* ------------------------------------------------------------------------- *)
110
111 let print_thl thl =
112   map (fun thm -> ( print_thm thm ; print_newline ())) thl;;
113
114
115 (* ------------------------------------------------------------------------- *)
116 (* print_tml:                                                                *)
117 (* Print a list of terms (for debugging).                                    *)
118 (* ------------------------------------------------------------------------- *)
119
120 let print_tml tml =
121     map (fun tm -> ( print_term tm ; print_newline ())) tml;;
122
123
124 (* ------------------------------------------------------------------------- *)
125 (* print_varandtype, show_types, hide_types:                                 *)
126 (* Prints the type after each variable.  Useful for "debugging" type issues. *)
127 (* ------------------------------------------------------------------------- *)
128 (* Source:                                                                   *)
129 (* http://code.google.com/p/flyspeck/wiki/TipsAndTricks#Investigating_Types  *)
130 (* ------------------------------------------------------------------------- *)
131
132 let print_varandtype fmt tm =
133   let hop,args = strip_comb tm in
134   let s = name_of hop
135   and ty = type_of hop in
136   if is_var hop & args = [] then
137    (pp_print_string fmt "(";
138     pp_print_string fmt s;
139     pp_print_string fmt ":";
140     pp_print_type fmt ty;
141     pp_print_string fmt ")")
142   else fail() ;;
143
144 let show_types,hide_types =
145   (fun () -> install_user_printer ("Show Types",print_varandtype)),
146   (fun () -> try delete_user_printer "Show Types"
147              with Failure _ -> failwith ("hide_types: "^
148                                          "Types are already hidden."));;
149
150
151 (* ------------------------------------------------------------------------- *)
152 (* count_goals : unit -> int                                                 *)
153 (* Shortcut to count the subgoals in the current goalstate.                  *)
154 (* ------------------------------------------------------------------------- *)
155
156 let count_goals () =
157   if (!current_goalstack = []) then 0 else
158   ( let _,gls,_ = hd !current_goalstack in length gls );;
159
160
161
162 (* ------------------------------------------------------------------------- *)
163 (* top_asms : goalstack -> (string * thm) list                               *)
164 (* Shortcut to get the assumption list of the top goal of a given goalstack. *)
165 (* ------------------------------------------------------------------------- *)
166
167 let top_asms (gs:goalstack) = (fst o hd o snd3 o hd) gs;;
168
169
170 (* ------------------------------------------------------------------------- *)
171 (* top_metas : goalstack -> term list                                        *)
172 (* Returns the list of metavariables in the current goalstate.               *)
173 (* ------------------------------------------------------------------------- *)
174
175 let top_metas (gs:goalstack) = (fst o fst3 o hd) gs;;
176
177
178 (* ------------------------------------------------------------------------- *)
179 (* top_inst : goalstack -> instantiation                                     *)
180 (* Returns the metavariable instantiations in the current goalstate.         *)
181 (* ------------------------------------------------------------------------- *)
182
183 let top_inst (gs:goalstack) = (snd o fst3 o hd) gs;;
184
185
186 (* ------------------------------------------------------------------------- *)
187 (* print_goalstack_all :                                                     *)
188 (* Alternative goalstack printer that always prints all subgoals.            *)
189 (* Also prints list of metavariables with their types.                       *)
190 (* ------------------------------------------------------------------------- *)
191 (* Original printer only prints more than one subgoals iff they were         *)
192 (* generated by the last step. Otherwise it only prints the 'active' subgoal.*)
193 (* Replace by #install_printer print_goalstack_all;;                         *)
194 (* Revert to original by #install_printer print_goalstack;;                  *)
195 (* ------------------------------------------------------------------------- *)
196
197 let (print_goalstack_all:goalstack->unit) =
198   let print_goalstate k gs =
199     let ((mvs,_),gl,_) = gs in
200     let n = length gl in
201     let s = if n = 0 then "No subgoals" else
202               (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
203            ^" ("^(string_of_int n)^" total)" in
204     let print_mv v = print_string " `" ;
205                      print_varandtype std_formatter v ;
206                      print_string "`;" in
207     print_string s; print_newline();
208     if (length mvs > 0) then (
209       print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
210     ) ;
211     if gl = [] then () else
212     do_list (print_goal o C el gl) (rev(0--(k-1))) in
213   fun l ->
214     if l = [] then print_string "Empty goalstack"
215     else
216       let (_,gl,_ as gs) = hd l in
217       print_goalstate (length gl) gs;;
218
219
220 (* ------------------------------------------------------------------------- *)
221 (* print_goalstack :                                                         *)
222 (* Upgrade to print_goalstack that also prints a list of metavariables with  *)
223 (* their types.                                                              *)
224 (* ------------------------------------------------------------------------- *)
225
226 let (print_goalstack:goalstack->unit) =
227   let print_goalstate k gs =
228     let ((mvs,_),gl,_) = gs in
229     let n = length gl in
230     let s = if n = 0 then "No subgoals" else
231               (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
232            ^" ("^(string_of_int n)^" total)" in
233     let print_mv v = print_string " `" ;
234                      print_varandtype std_formatter v ;
235                      print_string "`;" in
236     print_string s; print_newline();
237     if (length mvs > 0) then (
238       print_string "Metas:" ; let _ = map print_mv mvs in () ; print_newline()
239     ) ;
240     if gl = [] then () else
241     do_list (print_goal o C el gl) (rev(0--(k-1))) in
242   fun l ->
243     if l = [] then print_string "Empty goalstack"
244     else if tl l = [] then
245       let (_,gl,_ as gs) = hd l in
246       print_goalstate 1 gs
247     else
248       let (_,gl,_ as gs) = hd l
249       and (_,gl0,_) = hd(tl l) in
250       let p = length gl - length gl0 in
251       let p' = if p < 1 then 1 else p + 1 in
252       print_goalstate p' gs;;
253
254 #install_printer print_goalstack;;
255
256
257