1 (* Title: HOL/Tools/Sledgehammer/metis_clauses.ML |
|
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 |
|
5 Storing/printing FOL clauses and arity clauses. Typed equality is |
|
6 treated differently. |
|
7 *) |
|
8 |
|
9 signature METIS_CLAUSES = |
|
10 sig |
|
11 type name = string * string |
|
12 datatype type_literal = |
|
13 TyLitVar of name * name | |
|
14 TyLitFree of name * name |
|
15 datatype arLit = |
|
16 TConsLit of name * name * name list | |
|
17 TVarLit of name * name |
|
18 datatype arity_clause = |
|
19 ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
|
20 datatype class_rel_clause = |
|
21 ClassRelClause of {name: string, subclass: name, superclass: name} |
|
22 datatype combtyp = |
|
23 CombTVar of name | |
|
24 CombTFree of name | |
|
25 CombType of name * combtyp list |
|
26 datatype combterm = |
|
27 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
28 CombVar of name * combtyp | |
|
29 CombApp of combterm * combterm |
|
30 datatype fol_literal = FOLLiteral of bool * combterm |
|
31 |
|
32 val type_wrapper_name : string |
|
33 val bound_var_prefix : string |
|
34 val schematic_var_prefix: string |
|
35 val fixed_var_prefix: string |
|
36 val tvar_prefix: string |
|
37 val tfree_prefix: string |
|
38 val const_prefix: string |
|
39 val type_const_prefix: string |
|
40 val class_prefix: string |
|
41 val invert_const: string -> string |
|
42 val ascii_of: string -> string |
|
43 val unascii_of: string -> string |
|
44 val strip_prefix_and_unascii: string -> string -> string option |
|
45 val make_bound_var : string -> string |
|
46 val make_schematic_var : string * int -> string |
|
47 val make_fixed_var : string -> string |
|
48 val make_schematic_type_var : string * int -> string |
|
49 val make_fixed_type_var : string -> string |
|
50 val make_fixed_const : string -> string |
|
51 val make_fixed_type_const : string -> string |
|
52 val make_type_class : string -> string |
|
53 val skolem_theory_name: string |
|
54 val skolem_prefix: string |
|
55 val skolem_infix: string |
|
56 val is_skolem_const_name: string -> bool |
|
57 val num_type_args: theory -> string -> int |
|
58 val type_literals_for_types : typ list -> type_literal list |
|
59 val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list |
|
60 val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list |
|
61 val combtyp_of : combterm -> combtyp |
|
62 val strip_combterm_comb : combterm -> combterm * combterm list |
|
63 val combterm_from_term : |
|
64 theory -> (string * typ) list -> term -> combterm * typ list |
|
65 val literals_of_term : theory -> term -> fol_literal list * typ list |
|
66 val conceal_skolem_terms : |
|
67 int -> (string * term) list -> term -> (string * term) list * term |
|
68 val reveal_skolem_terms : (string * term) list -> term -> term |
|
69 val tfree_classes_of_terms : term list -> string list |
|
70 val tvar_classes_of_terms : term list -> string list |
|
71 val type_consts_of_terms : theory -> term list -> string list |
|
72 end |
|
73 |
|
74 structure Metis_Clauses : METIS_CLAUSES = |
|
75 struct |
|
76 |
|
77 val type_wrapper_name = "ti" |
|
78 |
|
79 val bound_var_prefix = "B_" |
|
80 val schematic_var_prefix = "V_" |
|
81 val fixed_var_prefix = "v_" |
|
82 |
|
83 val tvar_prefix = "T_"; |
|
84 val tfree_prefix = "t_"; |
|
85 |
|
86 val const_prefix = "c_"; |
|
87 val type_const_prefix = "tc_"; |
|
88 val class_prefix = "class_"; |
|
89 |
|
90 fun union_all xss = fold (union (op =)) xss [] |
|
91 |
|
92 (* Readable names for the more common symbolic functions. Do not mess with the |
|
93 last nine entries of the table unless you know what you are doing. *) |
|
94 val const_trans_table = |
|
95 Symtab.make [(@{type_name Product_Type.prod}, "prod"), |
|
96 (@{type_name Sum_Type.sum}, "sum"), |
|
97 (@{const_name HOL.eq}, "equal"), |
|
98 (@{const_name HOL.conj}, "and"), |
|
99 (@{const_name HOL.disj}, "or"), |
|
100 (@{const_name HOL.implies}, "implies"), |
|
101 (@{const_name Set.member}, "member"), |
|
102 (@{const_name fequal}, "fequal"), |
|
103 (@{const_name COMBI}, "COMBI"), |
|
104 (@{const_name COMBK}, "COMBK"), |
|
105 (@{const_name COMBB}, "COMBB"), |
|
106 (@{const_name COMBC}, "COMBC"), |
|
107 (@{const_name COMBS}, "COMBS"), |
|
108 (@{const_name True}, "True"), |
|
109 (@{const_name False}, "False"), |
|
110 (@{const_name If}, "If")] |
|
111 |
|
112 (* Invert the table of translations between Isabelle and ATPs. *) |
|
113 val const_trans_table_inv = |
|
114 Symtab.update ("fequal", @{const_name HOL.eq}) |
|
115 (Symtab.make (map swap (Symtab.dest const_trans_table))) |
|
116 |
|
117 val invert_const = perhaps (Symtab.lookup const_trans_table_inv) |
|
118 |
|
119 (*Escaping of special characters. |
|
120 Alphanumeric characters are left unchanged. |
|
121 The character _ goes to __ |
|
122 Characters in the range ASCII space to / go to _A to _P, respectively. |
|
123 Other characters go to _nnn where nnn is the decimal ASCII code.*) |
|
124 val A_minus_space = Char.ord #"A" - Char.ord #" "; |
|
125 |
|
126 fun stringN_of_int 0 _ = "" |
|
127 | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10); |
|
128 |
|
129 fun ascii_of_c c = |
|
130 if Char.isAlphaNum c then String.str c |
|
131 else if c = #"_" then "__" |
|
132 else if #" " <= c andalso c <= #"/" |
|
133 then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space)) |
|
134 else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*) |
|
135 |
|
136 val ascii_of = String.translate ascii_of_c; |
|
137 |
|
138 (** Remove ASCII armouring from names in proof files **) |
|
139 |
|
140 (*We don't raise error exceptions because this code can run inside the watcher. |
|
141 Also, the errors are "impossible" (hah!)*) |
|
142 fun unascii_aux rcs [] = String.implode(rev rcs) |
|
143 | unascii_aux rcs [#"_"] = unascii_aux (#"_"::rcs) [] (*ERROR*) |
|
144 (*Three types of _ escapes: __, _A to _P, _nnn*) |
|
145 | unascii_aux rcs (#"_" :: #"_" :: cs) = unascii_aux (#"_"::rcs) cs |
|
146 | unascii_aux rcs (#"_" :: c :: cs) = |
|
147 if #"A" <= c andalso c<= #"P" (*translation of #" " to #"/"*) |
|
148 then unascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs |
|
149 else |
|
150 let val digits = List.take (c::cs, 3) handle Subscript => [] |
|
151 in |
|
152 case Int.fromString (String.implode digits) of |
|
153 NONE => unascii_aux (c:: #"_"::rcs) cs (*ERROR*) |
|
154 | SOME n => unascii_aux (Char.chr n :: rcs) (List.drop (cs, 2)) |
|
155 end |
|
156 | unascii_aux rcs (c::cs) = unascii_aux (c::rcs) cs |
|
157 val unascii_of = unascii_aux [] o String.explode |
|
158 |
|
159 (* If string s has the prefix s1, return the result of deleting it, |
|
160 un-ASCII'd. *) |
|
161 fun strip_prefix_and_unascii s1 s = |
|
162 if String.isPrefix s1 s then |
|
163 SOME (unascii_of (String.extract (s, size s1, NONE))) |
|
164 else |
|
165 NONE |
|
166 |
|
167 (*Remove the initial ' character from a type variable, if it is present*) |
|
168 fun trim_type_var s = |
|
169 if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE) |
|
170 else error ("trim_type: Malformed type variable encountered: " ^ s); |
|
171 |
|
172 fun ascii_of_indexname (v,0) = ascii_of v |
|
173 | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i; |
|
174 |
|
175 fun make_bound_var x = bound_var_prefix ^ ascii_of x |
|
176 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v |
|
177 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x |
|
178 |
|
179 fun make_schematic_type_var (x,i) = |
|
180 tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); |
|
181 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); |
|
182 |
|
183 fun lookup_const c = |
|
184 case Symtab.lookup const_trans_table c of |
|
185 SOME c' => c' |
|
186 | NONE => ascii_of c |
|
187 |
|
188 (* HOL.eq MUST BE "equal" because it's built into ATPs. *) |
|
189 fun make_fixed_const @{const_name HOL.eq} = "equal" |
|
190 | make_fixed_const c = const_prefix ^ lookup_const c |
|
191 |
|
192 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c |
|
193 |
|
194 fun make_type_class clas = class_prefix ^ ascii_of clas; |
|
195 |
|
196 val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
|
197 val skolem_prefix = "sko_" |
|
198 val skolem_infix = "$" |
|
199 |
|
200 (* Hack: Could return false positives (e.g., a user happens to declare a |
|
201 constant called "SomeTheory.sko_means_shoe_in_$wedish". *) |
|
202 val is_skolem_const_name = |
|
203 Long_Name.base_name |
|
204 #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix |
|
205 |
|
206 (* The number of type arguments of a constant, zero if it's monomorphic. For |
|
207 (instances of) Skolem pseudoconstants, this information is encoded in the |
|
208 constant name. *) |
|
209 fun num_type_args thy s = |
|
210 if String.isPrefix skolem_theory_name s then |
|
211 s |> unprefix skolem_theory_name |
|
212 |> space_explode skolem_infix |> hd |
|
213 |> space_explode "_" |> List.last |> Int.fromString |> the |
|
214 else |
|
215 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
|
216 |
|
217 (**** Definitions and functions for FOL clauses for TPTP format output ****) |
|
218 |
|
219 type name = string * string |
|
220 |
|
221 (**** Isabelle FOL clauses ****) |
|
222 |
|
223 (* The first component is the type class; the second is a TVar or TFree. *) |
|
224 datatype type_literal = |
|
225 TyLitVar of name * name | |
|
226 TyLitFree of name * name |
|
227 |
|
228 exception CLAUSE of string * term; |
|
229 |
|
230 (*Make literals for sorted type variables*) |
|
231 fun sorts_on_typs_aux (_, []) = [] |
|
232 | sorts_on_typs_aux ((x,i), s::ss) = |
|
233 let val sorts = sorts_on_typs_aux ((x,i), ss) |
|
234 in |
|
235 if s = "HOL.type" then sorts |
|
236 else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts |
|
237 else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts |
|
238 end; |
|
239 |
|
240 fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) |
|
241 | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); |
|
242 |
|
243 (*Given a list of sorted type variables, return a list of type literals.*) |
|
244 fun type_literals_for_types Ts = |
|
245 fold (union (op =)) (map sorts_on_typs Ts) [] |
|
246 |
|
247 (** make axiom and conjecture clauses. **) |
|
248 |
|
249 (**** Isabelle arities ****) |
|
250 |
|
251 datatype arLit = |
|
252 TConsLit of name * name * name list | |
|
253 TVarLit of name * name |
|
254 |
|
255 datatype arity_clause = |
|
256 ArityClause of {name: string, conclLit: arLit, premLits: arLit list} |
|
257 |
|
258 |
|
259 fun gen_TVars 0 = [] |
|
260 | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1); |
|
261 |
|
262 fun pack_sort(_,[]) = [] |
|
263 | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt) (*IGNORE sort "type"*) |
|
264 | pack_sort(tvar, cls::srt) = |
|
265 (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) |
|
266 |
|
267 (*Arity of type constructor tcon :: (arg1,...,argN)res*) |
|
268 fun make_axiom_arity_clause (tcons, name, (cls,args)) = |
|
269 let |
|
270 val tvars = gen_TVars (length args) |
|
271 val tvars_srts = ListPair.zip (tvars, args) |
|
272 in |
|
273 ArityClause {name = name, |
|
274 conclLit = TConsLit (`make_type_class cls, |
|
275 `make_fixed_type_const tcons, |
|
276 tvars ~~ tvars), |
|
277 premLits = map TVarLit (union_all (map pack_sort tvars_srts))} |
|
278 end |
|
279 |
|
280 |
|
281 (**** Isabelle class relations ****) |
|
282 |
|
283 datatype class_rel_clause = |
|
284 ClassRelClause of {name: string, subclass: name, superclass: name} |
|
285 |
|
286 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) |
|
287 fun class_pairs _ [] _ = [] |
|
288 | class_pairs thy subs supers = |
|
289 let |
|
290 val class_less = Sorts.class_less (Sign.classes_of thy) |
|
291 fun add_super sub super = class_less (sub, super) ? cons (sub, super) |
|
292 fun add_supers sub = fold (add_super sub) supers |
|
293 in fold add_supers subs [] end |
|
294 |
|
295 fun make_class_rel_clause (sub,super) = |
|
296 ClassRelClause {name = sub ^ "_" ^ super, |
|
297 subclass = `make_type_class sub, |
|
298 superclass = `make_type_class super} |
|
299 |
|
300 fun make_class_rel_clauses thy subs supers = |
|
301 map make_class_rel_clause (class_pairs thy subs supers); |
|
302 |
|
303 |
|
304 (** Isabelle arities **) |
|
305 |
|
306 fun arity_clause _ _ (_, []) = [] |
|
307 | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*) |
|
308 arity_clause seen n (tcons,ars) |
|
309 | arity_clause seen n (tcons, (ar as (class,_)) :: ars) = |
|
310 if member (op =) seen class then (*multiple arities for the same tycon, class pair*) |
|
311 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: |
|
312 arity_clause seen (n+1) (tcons,ars) |
|
313 else |
|
314 make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) :: |
|
315 arity_clause (class::seen) n (tcons,ars) |
|
316 |
|
317 fun multi_arity_clause [] = [] |
|
318 | multi_arity_clause ((tcons, ars) :: tc_arlists) = |
|
319 arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists |
|
320 |
|
321 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy |
|
322 provided its arguments have the corresponding sorts.*) |
|
323 fun type_class_pairs thy tycons classes = |
|
324 let val alg = Sign.classes_of thy |
|
325 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single |
|
326 fun add_class tycon class = |
|
327 cons (class, domain_sorts tycon class) |
|
328 handle Sorts.CLASS_ERROR _ => I |
|
329 fun try_classes tycon = (tycon, fold (add_class tycon) classes []) |
|
330 in map try_classes tycons end; |
|
331 |
|
332 (*Proving one (tycon, class) membership may require proving others, so iterate.*) |
|
333 fun iter_type_class_pairs _ _ [] = ([], []) |
|
334 | iter_type_class_pairs thy tycons classes = |
|
335 let val cpairs = type_class_pairs thy tycons classes |
|
336 val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) |
|
337 |> subtract (op =) classes |> subtract (op =) HOLogic.typeS |
|
338 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses |
|
339 in (union (op =) classes' classes, union (op =) cpairs' cpairs) end; |
|
340 |
|
341 fun make_arity_clauses thy tycons classes = |
|
342 let val (classes', cpairs) = iter_type_class_pairs thy tycons classes |
|
343 in (classes', multi_arity_clause cpairs) end; |
|
344 |
|
345 datatype combtyp = |
|
346 CombTVar of name | |
|
347 CombTFree of name | |
|
348 CombType of name * combtyp list |
|
349 |
|
350 datatype combterm = |
|
351 CombConst of name * combtyp * combtyp list (* Const and Free *) | |
|
352 CombVar of name * combtyp | |
|
353 CombApp of combterm * combterm |
|
354 |
|
355 datatype fol_literal = FOLLiteral of bool * combterm |
|
356 |
|
357 (*********************************************************************) |
|
358 (* convert a clause with type Term.term to a clause with type clause *) |
|
359 (*********************************************************************) |
|
360 |
|
361 (*Result of a function type; no need to check that the argument type matches.*) |
|
362 fun result_type (CombType (_, [_, tp2])) = tp2 |
|
363 | result_type _ = raise Fail "non-function type" |
|
364 |
|
365 fun combtyp_of (CombConst (_, tp, _)) = tp |
|
366 | combtyp_of (CombVar (_, tp)) = tp |
|
367 | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1) |
|
368 |
|
369 (*gets the head of a combinator application, along with the list of arguments*) |
|
370 fun strip_combterm_comb u = |
|
371 let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts) |
|
372 | stripc x = x |
|
373 in stripc(u,[]) end |
|
374 |
|
375 fun type_of (Type (a, Ts)) = |
|
376 let val (folTypes,ts) = types_of Ts in |
|
377 (CombType (`make_fixed_type_const a, folTypes), ts) |
|
378 end |
|
379 | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp]) |
|
380 | type_of (tp as TVar (x, _)) = |
|
381 (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp]) |
|
382 and types_of Ts = |
|
383 let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in |
|
384 (folTyps, union_all ts) |
|
385 end |
|
386 |
|
387 (* same as above, but no gathering of sort information *) |
|
388 fun simp_type_of (Type (a, Ts)) = |
|
389 CombType (`make_fixed_type_const a, map simp_type_of Ts) |
|
390 | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a) |
|
391 | simp_type_of (TVar (x, _)) = |
|
392 CombTVar (make_schematic_type_var x, string_of_indexname x) |
|
393 |
|
394 (* Converts a term (with combinators) into a combterm. Also accummulates sort |
|
395 infomation. *) |
|
396 fun combterm_from_term thy bs (P $ Q) = |
|
397 let val (P', tsP) = combterm_from_term thy bs P |
|
398 val (Q', tsQ) = combterm_from_term thy bs Q |
|
399 in (CombApp (P', Q'), union (op =) tsP tsQ) end |
|
400 | combterm_from_term thy _ (Const (c, T)) = |
|
401 let |
|
402 val (tp, ts) = type_of T |
|
403 val tvar_list = |
|
404 (if String.isPrefix skolem_theory_name c then |
|
405 [] |> Term.add_tvarsT T |> map TVar |
|
406 else |
|
407 (c, T) |> Sign.const_typargs thy) |
|
408 |> map simp_type_of |
|
409 val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
|
410 in (c',ts) end |
|
411 | combterm_from_term _ _ (Free (v, T)) = |
|
412 let val (tp,ts) = type_of T |
|
413 val v' = CombConst (`make_fixed_var v, tp, []) |
|
414 in (v',ts) end |
|
415 | combterm_from_term _ _ (Var (v, T)) = |
|
416 let val (tp,ts) = type_of T |
|
417 val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp) |
|
418 in (v',ts) end |
|
419 | combterm_from_term _ bs (Bound j) = |
|
420 let |
|
421 val (s, T) = nth bs j |
|
422 val (tp, ts) = type_of T |
|
423 val v' = CombConst (`make_bound_var s, tp, []) |
|
424 in (v', ts) end |
|
425 | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs" |
|
426 |
|
427 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) |
|
428 | predicate_of thy (t, pos) = |
|
429 (combterm_from_term thy [] (Envir.eta_contract t), pos) |
|
430 |
|
431 fun literals_of_term1 args thy (@{const Trueprop} $ P) = |
|
432 literals_of_term1 args thy P |
|
433 | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) = |
|
434 literals_of_term1 (literals_of_term1 args thy P) thy Q |
|
435 | literals_of_term1 (lits, ts) thy P = |
|
436 let val ((pred, ts'), pol) = predicate_of thy (P, true) in |
|
437 (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') |
|
438 end |
|
439 val literals_of_term = literals_of_term1 ([], []) |
|
440 |
|
441 fun skolem_name i j num_T_args = |
|
442 skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ |
|
443 skolem_infix ^ "g" |
|
444 |
|
445 fun conceal_skolem_terms i skolems t = |
|
446 if exists_Const (curry (op =) @{const_name skolem} o fst) t then |
|
447 let |
|
448 fun aux skolems |
|
449 (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = |
|
450 let |
|
451 val (skolems, s) = |
|
452 if i = ~1 then |
|
453 (skolems, @{const_name undefined}) |
|
454 else case AList.find (op aconv) skolems t of |
|
455 s :: _ => (skolems, s) |
|
456 | [] => |
|
457 let |
|
458 val s = skolem_theory_name ^ "." ^ |
|
459 skolem_name i (length skolems) |
|
460 (length (Term.add_tvarsT T [])) |
|
461 in ((s, t) :: skolems, s) end |
|
462 in (skolems, Const (s, T)) end |
|
463 | aux skolems (t1 $ t2) = |
|
464 let |
|
465 val (skolems, t1) = aux skolems t1 |
|
466 val (skolems, t2) = aux skolems t2 |
|
467 in (skolems, t1 $ t2) end |
|
468 | aux skolems (Abs (s, T, t')) = |
|
469 let val (skolems, t') = aux skolems t' in |
|
470 (skolems, Abs (s, T, t')) |
|
471 end |
|
472 | aux skolems t = (skolems, t) |
|
473 in aux skolems t end |
|
474 else |
|
475 (skolems, t) |
|
476 |
|
477 fun reveal_skolem_terms skolems = |
|
478 map_aterms (fn t as Const (s, _) => |
|
479 if String.isPrefix skolem_theory_name s then |
|
480 AList.lookup (op =) skolems s |> the |
|
481 |> map_types Type_Infer.paramify_vars |
|
482 else |
|
483 t |
|
484 | t => t) |
|
485 |
|
486 |
|
487 (***************************************************************) |
|
488 (* Type Classes Present in the Axiom or Conjecture Clauses *) |
|
489 (***************************************************************) |
|
490 |
|
491 fun set_insert (x, s) = Symtab.update (x, ()) s |
|
492 |
|
493 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts) |
|
494 |
|
495 (*Remove this trivial type class*) |
|
496 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset; |
|
497 |
|
498 fun tfree_classes_of_terms ts = |
|
499 let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts |
|
500 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
|
501 |
|
502 fun tvar_classes_of_terms ts = |
|
503 let val sorts_list = map (map #2 o OldTerm.term_tvars) ts |
|
504 in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; |
|
505 |
|
506 (*fold type constructors*) |
|
507 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) |
|
508 | fold_type_consts _ _ x = x; |
|
509 |
|
510 (*Type constructors used to instantiate overloaded constants are the only ones needed.*) |
|
511 fun add_type_consts_in_term thy = |
|
512 let |
|
513 fun aux (Const x) = |
|
514 fold (fold_type_consts set_insert) (Sign.const_typargs thy x) |
|
515 | aux (Abs (_, _, u)) = aux u |
|
516 | aux (Const (@{const_name skolem}, _) $ _) = I |
|
517 | aux (t $ u) = aux t #> aux u |
|
518 | aux _ = I |
|
519 in aux end |
|
520 |
|
521 fun type_consts_of_terms thy ts = |
|
522 Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty); |
|
523 |
|
524 end; |
|