|
1 (* Title: HOL/Tools/Sledgehammer/metis_translate.ML |
|
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
|
3 Author: Kong W. Susanto, Cambridge University Computer Laboratory |
|
4 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
5 Author: Jasmin Blanchette, TU Muenchen |
|
6 |
|
7 Translation of HOL to FOL for Metis. |
|
8 *) |
|
9 |
|
10 signature METIS_TRANSLATE = |
|
11 sig |
|
12 type name = string * string |
|
13 datatype type_literal = |
|
14 TyLitVar of name * name | |
|
15 TyLitFree of name * name |
|
16 datatype arLit = |
|
17 TConsLit of name * name * name list | |
|
18 TVarLit of name * name |
|
19 datatype arity_clause = |
|
20 ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
|
21 datatype class_rel_clause = |
|
22 ClassRelClause of {name: string, subclass: name, superclass: name} |
|
23 datatype combtyp = |
|
24 CombTVar of name | |
|
25 CombTFree of name | |
|
26 CombType of name * combtyp list |
|
27 datatype combterm = |
|
28 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
29 CombVar of name * combtyp | |
|
30 CombApp of combterm * combterm |
|
31 datatype fol_literal = FOLLiteral of bool * combterm |
|
32 |
|
33 datatype mode = FO | HO | FT |
|
34 type logic_map = |
|
35 {axioms: (Metis_Thm.thm * thm) list, |
|
36 tfrees: type_literal list, |
|
37 old_skolems: (string * term) list} |
|
38 |
|
39 val type_wrapper_name : string |
|
40 val bound_var_prefix : string |
|
41 val schematic_var_prefix: string |
|
42 val fixed_var_prefix: string |
|
43 val tvar_prefix: string |
|
44 val tfree_prefix: string |
|
45 val const_prefix: string |
|
46 val type_const_prefix: string |
|
47 val class_prefix: string |
|
48 val new_skolem_const_prefix : string |
|
49 val invert_const: string -> string |
|
50 val ascii_of: string -> string |
|
51 val unascii_of: string -> string |
|
52 val strip_prefix_and_unascii: string -> string -> string option |
|
53 val make_bound_var : string -> string |
|
54 val make_schematic_var : string * int -> string |
|
55 val make_fixed_var : string -> string |
|
56 val make_schematic_type_var : string * int -> string |
|
57 val make_fixed_type_var : string -> string |
|
58 val make_fixed_const : string -> string |
|
59 val make_fixed_type_const : string -> string |
|
60 val make_type_class : string -> string |
|
61 val num_type_args: theory -> string -> int |
|
62 val new_skolem_var_from_const: string -> indexname |
|
63 val type_literals_for_types : typ list -> type_literal list |
|
64 val make_class_rel_clauses : |
|
65 theory -> class list -> class list -> class_rel_clause list |
|
66 val make_arity_clauses : |
|
67 theory -> string list -> class list -> class list * arity_clause list |
|
68 val combtyp_of : combterm -> combtyp |
|
69 val strip_combterm_comb : combterm -> combterm * combterm list |
|
70 val combterm_from_term : |
|
71 theory -> int -> (string * typ) list -> term -> combterm * typ list |
|
72 val reveal_old_skolem_terms : (string * term) list -> term -> term |
|
73 val tfree_classes_of_terms : term list -> string list |
|
74 val tvar_classes_of_terms : term list -> string list |
|
75 val type_consts_of_terms : theory -> term list -> string list |
|
76 val string_of_mode : mode -> string |
|
77 val build_logic_map : |
|
78 mode -> Proof.context -> bool -> thm list -> thm list list |
|
79 -> mode * logic_map |
|
80 end |
|
81 |
|
82 structure Metis_Translate : METIS_TRANSLATE = |
|
83 struct |
|
84 |
|
85 val type_wrapper_name = "ti" |
|
86 |
|
87 val bound_var_prefix = "B_" |
|
88 val schematic_var_prefix = "V_" |
|
89 val fixed_var_prefix = "v_" |
|
90 |
|
91 val tvar_prefix = "T_"; |
|
92 val tfree_prefix = "t_"; |
|
93 |
|
94 val const_prefix = "c_"; |
|
95 val type_const_prefix = "tc_"; |
|
96 val class_prefix = "class_"; |
|
97 |
|
98 val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
|
99 val old_skolem_const_prefix = skolem_const_prefix ^ "o" |
|
100 val new_skolem_const_prefix = skolem_const_prefix ^ "n" |
|
101 |
|
102 fun union_all xss = fold (union (op =)) xss [] |
|
103 |
|
104 (* Readable names for the more common symbolic functions. Do not mess with the |
|
105 last nine entries of the table unless you know what you are doing. *) |
|
106 val const_trans_table = |
|
107 Symtab.make [(@{type_name Product_Type.prod}, "prod"), |
|
108 (@{type_name Sum_Type.sum}, "sum"), |
|
109 (@{const_name HOL.eq}, "equal"), |
|
110 (@{const_name HOL.conj}, "and"), |
|
111 (@{const_name HOL.disj}, "or"), |
|
112 (@{const_name HOL.implies}, "implies"), |
|
113 (@{const_name Set.member}, "member"), |
|
114 (@{const_name fequal}, "fequal"), |
|
115 (@{const_name COMBI}, "COMBI"), |
|
116 (@{const_name COMBK}, "COMBK"), |
|
117 (@{const_name COMBB}, "COMBB"), |
|
118 (@{const_name COMBC}, "COMBC"), |
|
119 (@{const_name COMBS}, "COMBS"), |
|
120 (@{const_name True}, "True"), |
|
121 (@{const_name False}, "False"), |
|
122 (@{const_name If}, "If")] |
|
123 |
|
124 (* Invert the table of translations between Isabelle and ATPs. *) |
|
125 val const_trans_table_inv = |
|
126 Symtab.update ("fequal", @{const_name HOL.eq}) |
|
127 (Symtab.make (map swap (Symtab.dest const_trans_table))) |
|
128 |
|
129 val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
|
130 |
|
131 (*Escaping of special characters. |
|
132 Alphanumeric characters are left unchanged. |
|
133 The character _ goes to __ |
|
134 Characters in the range ASCII space to / go to _A to _P, respectively. |
|
135 Other characters go to _nnn where nnn is the decimal ASCII code.*) |
|
136 val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
137 |
|
138 fun stringN_of_int 0 _ = "" |
|
139 | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); |
|
140 |
|
141 fun ascii_of_c c = |
|
142 if Char.isAlphaNum c then String.str c |
|
143 else if c = #"_" then "__" |
|
144 else if #" " <= c andalso c <= #"/" |
|
145 then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
|
146 else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) |
|
147 |
|
148 val ascii_of = String.translate ascii_of_c; |
|
149 |
|
150 (** Remove ASCII armouring from names in proof files **) |
|
151 |
|
152 (*We don't raise error exceptions because this code can run inside the watcher. |
|
153 Also, the errors are "impossible" (hah!)*) |
|
154 fun unascii_aux rcs [] = String.implode(rev rcs) |
|
155 | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) |
|
156 (*Three types of _ escapes: __, _A to _P, _nnn*) |
|
157 | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs |
|
158 | unascii_aux rcs (#"_" :: c :: cs) = |
|
159 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) |
|
160 then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs |
|
161 else |
|
162 let val digits = List.take (c::cs, 3) handle Subscript => [] |
|
163 in |
|
164 case Int.fromString (String.implode digits) of |
|
165 NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) |
|
166 | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) |
|
167 end |
|
168 | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs |
|
169 val unascii_of = unascii_aux [] o String.explode |
|
170 |
|
171 (* If string s has the prefix s1, return the result of deleting it, |
|
172 un-ASCII'd. *) |
|
173 fun strip_prefix_and_unascii s1 s = |
|
174 if String.isPrefix s1 s then |
|
175 SOME (unascii_of (String.extract (s, size s1, NONE))) |
|
176 else |
|
177 NONE |
|
178 |
|
179 (*Remove the initial ' character from a type variable, if it is present*) |
|
180 fun trim_type_var s = |
|
181 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
|
182 else error ("trim_type: Malformed type variable encountered: " ^ s); |
|
183 |
|
184 fun ascii_of_indexname (v,0) = ascii_of v |
|
185 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; |
|
186 |
|
187 fun make_bound_var x = bound_var_prefix ^ ascii_of x |
|
188 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v |
|
189 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x |
|
190 |
|
191 fun make_schematic_type_var (x,i) = |
|
192 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
|
193 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
|
194 |
|
195 fun lookup_const c = |
|
196 case Symtab.lookup const_trans_table c of |
|
197 SOME c' => c' |
|
198 | NONE => ascii_of c |
|
199 |
|
200 (* HOL.eq MUST BE "equal" because it's built into ATPs. *) |
|
201 fun make_fixed_const @{const_name HOL.eq} = "equal" |
|
202 | make_fixed_const c = const_prefix ^ lookup_const c |
|
203 |
|
204 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c |
|
205 |
|
206 fun make_type_class clas = class_prefix ^ ascii_of clas; |
|
207 |
|
208 (* The number of type arguments of a constant, zero if it's monomorphic. For |
|
209 (instances of) Skolem pseudoconstants, this information is encoded in the |
|
210 constant name. *) |
|
211 fun num_type_args thy s = |
|
212 if String.isPrefix skolem_const_prefix s then |
|
213 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the |
|
214 else |
|
215 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
|
216 |
|
217 fun new_skolem_var_from_const s = |
|
218 let |
|
219 val ss = s |> space_explode Long_Name.separator |
|
220 val n = length ss |
|
221 in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end |
|
222 |
|
223 |
|
224 (**** Definitions and functions for FOL clauses for TPTP format output ****) |
|
225 |
|
226 type name = string * string |
|
227 |
|
228 (**** Isabelle FOL clauses ****) |
|
229 |
|
230 (* The first component is the type class; the second is a TVar or TFree. *) |
|
231 datatype type_literal = |
|
232 TyLitVar of name * name | |
|
233 TyLitFree of name * name |
|
234 |
|
235 (*Make literals for sorted type variables*) |
|
236 fun sorts_on_typs_aux (_, []) = [] |
|
237 | sorts_on_typs_aux ((x,i), s::ss) = |
|
238 let val sorts = sorts_on_typs_aux ((x,i), ss) |
|
239 in |
|
240 if s = "HOL.type" then sorts |
|
241 else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts |
|
242 else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts |
|
243 end; |
|
244 |
|
245 fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) |
|
246 | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); |
|
247 |
|
248 (*Given a list of sorted type variables, return a list of type literals.*) |
|
249 fun type_literals_for_types Ts = |
|
250 fold (union (op =)) (map sorts_on_typs Ts) [] |
|
251 |
|
252 (** make axiom and conjecture clauses. **) |
|
253 |
|
254 (**** Isabelle arities ****) |
|
255 |
|
256 datatype arLit = |
|
257 TConsLit of name * name * name list | |
|
258 TVarLit of name * name |
|
259 |
|
260 datatype arity_clause = |
|
261 ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
|
262 |
|
263 |
|
264 fun gen_TVars 0 = [] |
|
265 | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); |
|
266 |
|
267 fun pack_sort(_,[]) = [] |
|
268 | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) |
|
269 | pack_sort(tvar, cls::srt) = |
|
270 (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) |
|
271 |
|
272 (*Arity of type constructor tcon :: (arg1,...,argN)res*) |
|
273 fun make_axiom_arity_clause (tcons, name, (cls,args)) = |
|
274 let |
|
275 val tvars = gen_TVars (length args) |
|
276 val tvars_srts = ListPair.zip (tvars, args) |
|
277 in |
|
278 ArityClause {name = name, |
|
279 conclLit = TConsLit (`make_type_class cls, |
|
280 `make_fixed_type_const tcons, |
|
281 tvars ~~ tvars), |
|
282 premLits = map TVarLit (union_all (map pack_sort tvars_srts))} |
|
283 end |
|
284 |
|
285 |
|
286 (**** Isabelle class relations ****) |
|
287 |
|
288 datatype class_rel_clause = |
|
289 ClassRelClause of {name: string, subclass: name, superclass: name} |
|
290 |
|
291 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) |
|
292 fun class_pairs _ [] _ = [] |
|
293 | class_pairs thy subs supers = |
|
294 let |
|
295 val class_less = Sorts.class_less (Sign.classes_of thy) |
|
296 fun add_super sub super = class_less (sub, super) ? cons (sub, super) |
|
297 fun add_supers sub = fold (add_super sub) supers |
|
298 in fold add_supers subs [] end |
|
299 |
|
300 fun make_class_rel_clause (sub,super) = |
|
301 ClassRelClause {name = sub ^ "_" ^ super, |
|
302 subclass = `make_type_class sub, |
|
303 superclass = `make_type_class super} |
|
304 |
|
305 fun make_class_rel_clauses thy subs supers = |
|
306 map make_class_rel_clause (class_pairs thy subs supers); |
|
307 |
|
308 |
|
309 (** Isabelle arities **) |
|
310 |
|
311 fun arity_clause _ _ (_, []) = [] |
|
312 | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) |
|
313 arity_clause seen n (tcons,ars) |
|
314 | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = |
|
315 if member (op =) seen class then (*multiple arities for the same tycon, class pair*) |
|
316 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: |
|
317 arity_clause seen (n+1) (tcons,ars) |
|
318 else |
|
319 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: |
|
320 arity_clause (class::seen) n (tcons,ars) |
|
321 |
|
322 fun multi_arity_clause [] = [] |
|
323 | multi_arity_clause ((tcons, ars) :: tc_arlists) = |
|
324 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists |
|
325 |
|
326 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy |
|
327 provided its arguments have the corresponding sorts.*) |
|
328 fun type_class_pairs thy tycons classes = |
|
329 let val alg = Sign.classes_of thy |
|
330 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single |
|
331 fun add_class tycon class = |
|
332 cons (class, domain_sorts tycon class) |
|
333 handle Sorts.CLASS_ERROR _ => I |
|
334 fun try_classes tycon = (tycon, fold (add_class tycon) classes []) |
|
335 in map try_classes tycons end; |
|
336 |
|
337 (*Proving one (tycon, class) membership may require proving others, so iterate.*) |
|
338 fun iter_type_class_pairs _ _ [] = ([], []) |
|
339 | iter_type_class_pairs thy tycons classes = |
|
340 let val cpairs = type_class_pairs thy tycons classes |
|
341 val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) |
|
342 |> subtract (op =) classes |> subtract (op =) HOLogic.typeS |
|
343 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses |
|
344 in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; |
|
345 |
|
346 fun make_arity_clauses thy tycons classes = |
|
347 let val (classes', cpairs) = iter_type_class_pairs thy tycons classes |
|
348 in (classes', multi_arity_clause cpairs) end; |
|
349 |
|
350 datatype combtyp = |
|
351 CombTVar of name | |
|
352 CombTFree of name | |
|
353 CombType of name * combtyp list |
|
354 |
|
355 datatype combterm = |
|
356 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
357 CombVar of name * combtyp | |
|
358 CombApp of combterm * combterm |
|
359 |
|
360 datatype fol_literal = FOLLiteral of bool * combterm |
|
361 |
|
362 (*********************************************************************) |
|
363 (* convert a clause with type Term.term to a clause with type clause *) |
|
364 (*********************************************************************) |
|
365 |
|
366 (*Result of a function type; no need to check that the argument type matches.*) |
|
367 fun result_type (CombType (_, [_, tp2])) = tp2 |
|
368 | result_type _ = raise Fail "non-function type" |
|
369 |
|
370 fun combtyp_of (CombConst (_, tp, _)) = tp |
|
371 | combtyp_of (CombVar (_, tp)) = tp |
|
372 | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) |
|
373 |
|
374 (*gets the head of a combinator application, along with the list of arguments*) |
|
375 fun strip_combterm_comb u = |
|
376 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
|
377 | stripc x = x |
|
378 in stripc(u,[]) end |
|
379 |
|
380 fun combtype_of (Type (a, Ts)) = |
|
381 let val (folTypes, ts) = combtypes_of Ts in |
|
382 (CombType (`make_fixed_type_const a, folTypes), ts) |
|
383 end |
|
384 | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) |
|
385 | combtype_of (tp as TVar (x, _)) = |
|
386 (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
|
387 and combtypes_of Ts = |
|
388 let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in |
|
389 (folTyps, union_all ts) |
|
390 end |
|
391 |
|
392 (* same as above, but no gathering of sort information *) |
|
393 fun simple_combtype_of (Type (a, Ts)) = |
|
394 CombType (`make_fixed_type_const a, map simple_combtype_of Ts) |
|
395 | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) |
|
396 | simple_combtype_of (TVar (x, _)) = |
|
397 CombTVar (make_schematic_type_var x, string_of_indexname x) |
|
398 |
|
399 fun new_skolem_const_name th_no s num_T_args = |
|
400 [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args] |
|
401 |> space_implode Long_Name.separator |
|
402 |
|
403 (* Converts a term (with combinators) into a combterm. Also accummulates sort |
|
404 infomation. *) |
|
405 fun combterm_from_term thy th_no bs (P $ Q) = |
|
406 let val (P', tsP) = combterm_from_term thy th_no bs P |
|
407 val (Q', tsQ) = combterm_from_term thy th_no bs Q |
|
408 in (CombApp (P', Q'), union (op =) tsP tsQ) end |
|
409 | combterm_from_term thy _ _ (Const (c, T)) = |
|
410 let |
|
411 val (tp, ts) = combtype_of T |
|
412 val tvar_list = |
|
413 (if String.isPrefix old_skolem_const_prefix c then |
|
414 [] |> Term.add_tvarsT T |> map TVar |
|
415 else |
|
416 (c, T) |> Sign.const_typargs thy) |
|
417 |> map simple_combtype_of |
|
418 val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
|
419 in (c',ts) end |
|
420 | combterm_from_term _ _ _ (Free (v, T)) = |
|
421 let val (tp, ts) = combtype_of T |
|
422 val v' = CombConst (`make_fixed_var v, tp, []) |
|
423 in (v',ts) end |
|
424 | combterm_from_term _ th_no _ (Var (v as (s, _), T)) = |
|
425 let |
|
426 val (tp, ts) = combtype_of T |
|
427 val v' = |
|
428 if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then |
|
429 let |
|
430 val tys = T |> strip_type |> swap |> op :: |
|
431 val s' = new_skolem_const_name th_no s (length tys) |
|
432 in |
|
433 CombConst (`make_fixed_const s', tp, map simple_combtype_of tys) |
|
434 end |
|
435 else |
|
436 CombVar ((make_schematic_var v, string_of_indexname v), tp) |
|
437 in (v', ts) end |
|
438 | combterm_from_term _ _ bs (Bound j) = |
|
439 let |
|
440 val (s, T) = nth bs j |
|
441 val (tp, ts) = combtype_of T |
|
442 val v' = CombConst (`make_bound_var s, tp, []) |
|
443 in (v', ts) end |
|
444 | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs" |
|
445 |
|
446 fun predicate_of thy th_no ((@{const Not} $ P), pos) = |
|
447 predicate_of thy th_no (P, not pos) |
|
448 | predicate_of thy th_no (t, pos) = |
|
449 (combterm_from_term thy th_no [] (Envir.eta_contract t), pos) |
|
450 |
|
451 fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) = |
|
452 literals_of_term1 args thy th_no P |
|
453 | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) = |
|
454 literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q |
|
455 | literals_of_term1 (lits, ts) thy th_no P = |
|
456 let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in |
|
457 (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') |
|
458 end |
|
459 val literals_of_term = literals_of_term1 ([], []) |
|
460 |
|
461 fun old_skolem_const_name i j num_T_args = |
|
462 old_skolem_const_prefix ^ Long_Name.separator ^ |
|
463 (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) |
|
464 |
|
465 fun conceal_old_skolem_terms i old_skolems t = |
|
466 if exists_Const (curry (op =) @{const_name skolem} o fst) t then |
|
467 let |
|
468 fun aux old_skolems |
|
469 (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = |
|
470 let |
|
471 val (old_skolems, s) = |
|
472 if i = ~1 then |
|
473 (old_skolems, @{const_name undefined}) |
|
474 else case AList.find (op aconv) old_skolems t of |
|
475 s :: _ => (old_skolems, s) |
|
476 | [] => |
|
477 let |
|
478 val s = old_skolem_const_name i (length old_skolems) |
|
479 (length (Term.add_tvarsT T [])) |
|
480 in ((s, t) :: old_skolems, s) end |
|
481 in (old_skolems, Const (s, T)) end |
|
482 | aux old_skolems (t1 $ t2) = |
|
483 let |
|
484 val (old_skolems, t1) = aux old_skolems t1 |
|
485 val (old_skolems, t2) = aux old_skolems t2 |
|
486 in (old_skolems, t1 $ t2) end |
|
487 | aux old_skolems (Abs (s, T, t')) = |
|
488 let val (old_skolems, t') = aux old_skolems t' in |
|
489 (old_skolems, Abs (s, T, t')) |
|
490 end |
|
491 | aux old_skolems t = (old_skolems, t) |
|
492 in aux old_skolems t end |
|
493 else |
|
494 (old_skolems, t) |
|
495 |
|
496 fun reveal_old_skolem_terms old_skolems = |
|
497 map_aterms (fn t as Const (s, _) => |
|
498 if String.isPrefix old_skolem_const_prefix s then |
|
499 AList.lookup (op =) old_skolems s |> the |
|
500 |> map_types Type_Infer.paramify_vars |
|
501 else |
|
502 t |
|
503 | t => t) |
|
504 |
|
505 |
|
506 (***************************************************************) |
|
507 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
|
508 (***************************************************************) |
|
509 |
|
510 fun set_insert (x, s) = Symtab.update (x, ()) s |
|
511 |
|
512 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) |
|
513 |
|
514 (*Remove this trivial type class*) |
|
515 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; |
|
516 |
|
517 fun tfree_classes_of_terms ts = |
|
518 let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts |
|
519 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
|
520 |
|
521 fun tvar_classes_of_terms ts = |
|
522 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts |
|
523 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
|
524 |
|
525 (*fold type constructors*) |
|
526 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) |
|
527 | fold_type_consts _ _ x = x; |
|
528 |
|
529 (*Type constructors used to instantiate overloaded constants are the only ones needed.*) |
|
530 fun add_type_consts_in_term thy = |
|
531 let |
|
532 fun aux (Const x) = |
|
533 fold (fold_type_consts set_insert) (Sign.const_typargs thy x) |
|
534 | aux (Abs (_, _, u)) = aux u |
|
535 | aux (Const (@{const_name skolem}, _) $ _) = I |
|
536 | aux (t $ u) = aux t #> aux u |
|
537 | aux _ = I |
|
538 in aux end |
|
539 |
|
540 fun type_consts_of_terms thy ts = |
|
541 Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); |
|
542 |
|
543 (* ------------------------------------------------------------------------- *) |
|
544 (* HOL to FOL (Isabelle to Metis) *) |
|
545 (* ------------------------------------------------------------------------- *) |
|
546 |
|
547 datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) |
|
548 |
|
549 fun string_of_mode FO = "FO" |
|
550 | string_of_mode HO = "HO" |
|
551 | string_of_mode FT = "FT" |
|
552 |
|
553 fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) |
|
554 | fn_isa_to_met_sublevel x = x |
|
555 fun fn_isa_to_met_toplevel "equal" = "=" |
|
556 | fn_isa_to_met_toplevel x = x |
|
557 |
|
558 fun metis_lit b c args = (b, (c, args)); |
|
559 |
|
560 fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s |
|
561 | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, []) |
|
562 | metis_term_from_combtyp (CombType ((s, _), tps)) = |
|
563 Metis_Term.Fn (s, map metis_term_from_combtyp tps); |
|
564 |
|
565 (*These two functions insert type literals before the real literals. That is the |
|
566 opposite order from TPTP linkup, but maybe OK.*) |
|
567 |
|
568 fun hol_term_to_fol_FO tm = |
|
569 case strip_combterm_comb tm of |
|
570 (CombConst ((c, _), _, tys), tms) => |
|
571 let val tyargs = map metis_term_from_combtyp tys |
|
572 val args = map hol_term_to_fol_FO tms |
|
573 in Metis_Term.Fn (c, tyargs @ args) end |
|
574 | (CombVar ((v, _), _), []) => Metis_Term.Var v |
|
575 | _ => raise Fail "non-first-order combterm" |
|
576 |
|
577 fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = |
|
578 Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) |
|
579 | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s |
|
580 | hol_term_to_fol_HO (CombApp (tm1, tm2)) = |
|
581 Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); |
|
582 |
|
583 (*The fully-typed translation, to avoid type errors*) |
|
584 fun wrap_type (tm, ty) = |
|
585 Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty]) |
|
586 |
|
587 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty) |
|
588 | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = |
|
589 wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty) |
|
590 | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = |
|
591 wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), |
|
592 combtyp_of tm) |
|
593 |
|
594 fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = |
|
595 let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm |
|
596 val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys |
|
597 val lits = map hol_term_to_fol_FO tms |
|
598 in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end |
|
599 | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = |
|
600 (case strip_combterm_comb tm of |
|
601 (CombConst(("equal", _), _, _), tms) => |
|
602 metis_lit pos "=" (map hol_term_to_fol_HO tms) |
|
603 | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) |
|
604 | hol_literal_to_fol FT (FOLLiteral (pos, tm)) = |
|
605 (case strip_combterm_comb tm of |
|
606 (CombConst(("equal", _), _, _), tms) => |
|
607 metis_lit pos "=" (map hol_term_to_fol_FT tms) |
|
608 | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); |
|
609 |
|
610 fun literals_of_hol_term thy th_no mode t = |
|
611 let val (lits, types_sorts) = literals_of_term thy th_no t |
|
612 in (map (hol_literal_to_fol mode) lits, types_sorts) end; |
|
613 |
|
614 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) |
|
615 fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = |
|
616 metis_lit pos s [Metis_Term.Var s'] |
|
617 | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = |
|
618 metis_lit pos s [Metis_Term.Fn (s',[])] |
|
619 |
|
620 fun default_sort _ (TVar _) = false |
|
621 | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); |
|
622 |
|
623 fun metis_of_tfree tf = |
|
624 Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); |
|
625 |
|
626 fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th = |
|
627 let |
|
628 val thy = ProofContext.theory_of ctxt |
|
629 val (old_skolems, (mlits, types_sorts)) = |
|
630 th |> prop_of |> Logic.strip_imp_concl |
|
631 |> conceal_old_skolem_terms j old_skolems |
|
632 ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode) |
|
633 in |
|
634 if is_conjecture then |
|
635 (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), |
|
636 type_literals_for_types types_sorts, old_skolems) |
|
637 else |
|
638 let |
|
639 val tylits = filter_out (default_sort ctxt) types_sorts |
|
640 |> type_literals_for_types |
|
641 val mtylits = |
|
642 if type_lits then map (metis_of_type_literals false) tylits else [] |
|
643 in |
|
644 (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], |
|
645 old_skolems) |
|
646 end |
|
647 end; |
|
648 |
|
649 val helpers = |
|
650 [("c_COMBI", (false, map (`I) @{thms COMBI_def})), |
|
651 ("c_COMBK", (false, map (`I) @{thms COMBK_def})), |
|
652 ("c_COMBB", (false, map (`I) @{thms COMBB_def})), |
|
653 ("c_COMBC", (false, map (`I) @{thms COMBC_def})), |
|
654 ("c_COMBS", (false, map (`I) @{thms COMBS_def})), |
|
655 ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) |
|
656 @{thms fequal_imp_equal equal_imp_fequal})), |
|
657 ("c_True", (true, map (`I) @{thms True_or_False})), |
|
658 ("c_False", (true, map (`I) @{thms True_or_False})), |
|
659 ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] |
|
660 |
|
661 (* ------------------------------------------------------------------------- *) |
|
662 (* Logic maps manage the interface between HOL and first-order logic. *) |
|
663 (* ------------------------------------------------------------------------- *) |
|
664 |
|
665 type logic_map = |
|
666 {axioms: (Metis_Thm.thm * thm) list, |
|
667 tfrees: type_literal list, |
|
668 old_skolems: (string * term) list} |
|
669 |
|
670 fun is_quasi_fol_clause thy = |
|
671 Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of |
|
672 |
|
673 (*Extract TFree constraints from context to include as conjecture clauses*) |
|
674 fun init_tfrees ctxt = |
|
675 let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in |
|
676 Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] |
|
677 |> type_literals_for_types |
|
678 end; |
|
679 |
|
680 (*Insert non-logical axioms corresponding to all accumulated TFrees*) |
|
681 fun add_tfrees {axioms, tfrees, old_skolems} : logic_map = |
|
682 {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ |
|
683 axioms, |
|
684 tfrees = tfrees, old_skolems = old_skolems} |
|
685 |
|
686 (*transform isabelle type / arity clause to metis clause *) |
|
687 fun add_type_thm [] lmap = lmap |
|
688 | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = |
|
689 add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, |
|
690 old_skolems = old_skolems} |
|
691 |
|
692 fun const_in_metis c (pred, tm_list) = |
|
693 let |
|
694 fun in_mterm (Metis_Term.Var _) = false |
|
695 | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list |
|
696 | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list |
|
697 in c = pred orelse exists in_mterm tm_list end; |
|
698 |
|
699 (* ARITY CLAUSE *) |
|
700 fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = |
|
701 metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] |
|
702 | m_arity_cls (TVarLit ((c, _), (s, _))) = |
|
703 metis_lit false c [Metis_Term.Var s] |
|
704 (*TrueI is returned as the Isabelle counterpart because there isn't any.*) |
|
705 fun arity_cls (ArityClause {conclLit, premLits, ...}) = |
|
706 (TrueI, |
|
707 Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); |
|
708 |
|
709 (* CLASSREL CLAUSE *) |
|
710 fun m_class_rel_cls (subclass, _) (superclass, _) = |
|
711 [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]]; |
|
712 fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = |
|
713 (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); |
|
714 |
|
715 fun type_ext thy tms = |
|
716 let val subs = tfree_classes_of_terms tms |
|
717 val supers = tvar_classes_of_terms tms |
|
718 and tycons = type_consts_of_terms thy tms |
|
719 val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
|
720 val class_rel_clauses = make_class_rel_clauses thy subs supers' |
|
721 in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses |
|
722 end; |
|
723 |
|
724 (* Function to generate metis clauses, including comb and type clauses *) |
|
725 fun build_logic_map mode0 ctxt type_lits cls thss = |
|
726 let val thy = ProofContext.theory_of ctxt |
|
727 (*The modes FO and FT are sticky. HO can be downgraded to FO.*) |
|
728 fun set_mode FO = FO |
|
729 | set_mode HO = |
|
730 if forall (forall (is_quasi_fol_clause thy)) (cls :: thss) then FO |
|
731 else HO |
|
732 | set_mode FT = FT |
|
733 val mode = set_mode mode0 |
|
734 (*transform isabelle clause to metis clause *) |
|
735 fun add_thm th_no is_conjecture (metis_ith, isa_ith) |
|
736 {axioms, tfrees, old_skolems} : logic_map = |
|
737 let |
|
738 val (mth, tfree_lits, old_skolems) = |
|
739 hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms) |
|
740 old_skolems metis_ith |
|
741 in |
|
742 {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, |
|
743 tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} |
|
744 end; |
|
745 val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} |
|
746 |> fold (add_thm 0 true o `I) cls |
|
747 |> add_tfrees |
|
748 |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths) |
|
749 (1 upto length thss ~~ thss) |
|
750 val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) |
|
751 fun is_used c = |
|
752 exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists |
|
753 val lmap = |
|
754 if mode = FO then |
|
755 lmap |
|
756 else |
|
757 let |
|
758 val helper_ths = |
|
759 helpers |> filter (is_used o fst) |
|
760 |> maps (fn (c, (needs_full_types, thms)) => |
|
761 if not (is_used c) orelse |
|
762 needs_full_types andalso mode <> FT then |
|
763 [] |
|
764 else |
|
765 thms) |
|
766 in lmap |> fold (add_thm ~1 false) helper_ths end |
|
767 in |
|
768 (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap) |
|
769 end |
|
770 |
|
771 end; |