55 val make_schematic_type_var : string * int -> string |
55 val make_schematic_type_var : string * int -> string |
56 val make_fixed_type_var : string -> string |
56 val make_fixed_type_var : string -> string |
57 val make_fixed_const : string -> string |
57 val make_fixed_const : string -> string |
58 val make_fixed_type_const : string -> string |
58 val make_fixed_type_const : string -> string |
59 val make_type_class : string -> string |
59 val make_type_class : string -> string |
60 val skolem_theory_name: string |
|
61 val skolem_prefix: string |
|
62 val skolem_infix: string |
|
63 val is_skolem_const_name: string -> bool |
|
64 val num_type_args: theory -> string -> int |
60 val num_type_args: theory -> string -> int |
65 val type_literals_for_types : typ list -> type_literal list |
61 val type_literals_for_types : typ list -> type_literal list |
66 val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list |
62 val make_class_rel_clauses : |
67 val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list |
63 theory -> class list -> class list -> class_rel_clause list |
|
64 val make_arity_clauses : |
|
65 theory -> string list -> class list -> class list * arity_clause list |
68 val combtyp_of : combterm -> combtyp |
66 val combtyp_of : combterm -> combtyp |
69 val strip_combterm_comb : combterm -> combterm * combterm list |
67 val strip_combterm_comb : combterm -> combterm * combterm list |
70 val combterm_from_term : |
68 val combterm_from_term : |
71 theory -> (string * typ) list -> term -> combterm * typ list |
69 theory -> (string * typ) list -> term -> combterm * typ list |
72 val literals_of_term : theory -> term -> fol_literal list * typ list |
|
73 val conceal_skolem_terms : |
|
74 int -> (string * term) list -> term -> (string * term) list * term |
|
75 val reveal_skolem_terms : (string * term) list -> term -> term |
70 val reveal_skolem_terms : (string * term) list -> term -> term |
76 val tfree_classes_of_terms : term list -> string list |
71 val tfree_classes_of_terms : term list -> string list |
77 val tvar_classes_of_terms : term list -> string list |
72 val tvar_classes_of_terms : term list -> string list |
78 val type_consts_of_terms : theory -> term list -> string list |
73 val type_consts_of_terms : theory -> term list -> string list |
79 val string_of_mode : mode -> string |
74 val string_of_mode : mode -> string |
80 val build_logic_map : |
75 val build_logic_map : |
81 mode -> Proof.context -> bool -> thm list -> thm list |
76 mode -> Proof.context -> bool -> thm list -> thm list -> mode * logic_map |
82 -> mode * logic_map |
|
83 end |
77 end |
84 |
78 |
85 structure Metis_Translate : METIS_TRANSLATE = |
79 structure Metis_Translate : METIS_TRANSLATE = |
86 struct |
80 struct |
87 |
81 |
202 |
196 |
203 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c |
197 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c |
204 |
198 |
205 fun make_type_class clas = class_prefix ^ ascii_of clas; |
199 fun make_type_class clas = class_prefix ^ ascii_of clas; |
206 |
200 |
207 val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
201 val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko" |
208 val skolem_prefix = "sko_" |
|
209 val skolem_infix = "$" |
|
210 |
|
211 (* Hack: Could return false positives (e.g., a user happens to declare a |
|
212 constant called "SomeTheory.sko_means_shoe_in_$wedish". *) |
|
213 val is_skolem_const_name = |
|
214 Long_Name.base_name |
|
215 #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix |
|
216 |
202 |
217 (* The number of type arguments of a constant, zero if it's monomorphic. For |
203 (* The number of type arguments of a constant, zero if it's monomorphic. For |
218 (instances of) Skolem pseudoconstants, this information is encoded in the |
204 (instances of) Skolem pseudoconstants, this information is encoded in the |
219 constant name. *) |
205 constant name. *) |
220 fun num_type_args thy s = |
206 fun num_type_args thy s = |
221 if String.isPrefix skolem_theory_name s then |
207 if String.isPrefix skolem_prefix s then |
222 s |> unprefix skolem_theory_name |
208 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the |
223 |> space_explode skolem_infix |> hd |
|
224 |> space_explode "_" |> List.last |> Int.fromString |> the |
|
225 else |
209 else |
226 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
210 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length |
227 |
211 |
228 (**** Definitions and functions for FOL clauses for TPTP format output ****) |
212 (**** Definitions and functions for FOL clauses for TPTP format output ****) |
229 |
213 |
408 in (CombApp (P', Q'), union (op =) tsP tsQ) end |
392 in (CombApp (P', Q'), union (op =) tsP tsQ) end |
409 | combterm_from_term thy _ (Const (c, T)) = |
393 | combterm_from_term thy _ (Const (c, T)) = |
410 let |
394 let |
411 val (tp, ts) = combtype_of T |
395 val (tp, ts) = combtype_of T |
412 val tvar_list = |
396 val tvar_list = |
413 (if String.isPrefix skolem_theory_name c then |
397 (if String.isPrefix skolem_prefix c then |
414 [] |> Term.add_tvarsT T |> map TVar |
398 [] |> Term.add_tvarsT T |> map TVar |
415 else |
399 else |
416 (c, T) |> Sign.const_typargs thy) |
400 (c, T) |> Sign.const_typargs thy) |
417 |> map simple_combtype_of |
401 |> map simple_combtype_of |
418 val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
402 val c' = CombConst (`make_fixed_const c, tp, tvar_list) |
446 (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') |
430 (FOLLiteral (pol, pred) :: lits, union (op =) ts ts') |
447 end |
431 end |
448 val literals_of_term = literals_of_term1 ([], []) |
432 val literals_of_term = literals_of_term1 ([], []) |
449 |
433 |
450 fun skolem_name i j num_T_args = |
434 fun skolem_name i j num_T_args = |
451 skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^ |
435 skolem_prefix ^ Long_Name.separator ^ |
452 skolem_infix ^ "g" |
436 (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) |
453 |
437 |
454 fun conceal_skolem_terms i skolems t = |
438 fun conceal_skolem_terms i skolems t = |
455 if exists_Const (curry (op =) @{const_name skolem} o fst) t then |
439 if exists_Const (curry (op =) @{const_name skolem} o fst) t then |
456 let |
440 let |
457 fun aux skolems |
441 fun aux skolems |
462 (skolems, @{const_name undefined}) |
446 (skolems, @{const_name undefined}) |
463 else case AList.find (op aconv) skolems t of |
447 else case AList.find (op aconv) skolems t of |
464 s :: _ => (skolems, s) |
448 s :: _ => (skolems, s) |
465 | [] => |
449 | [] => |
466 let |
450 let |
467 val s = skolem_theory_name ^ "." ^ |
451 val s = skolem_name i (length skolems) |
468 skolem_name i (length skolems) |
452 (length (Term.add_tvarsT T [])) |
469 (length (Term.add_tvarsT T [])) |
|
470 in ((s, t) :: skolems, s) end |
453 in ((s, t) :: skolems, s) end |
471 in (skolems, Const (s, T)) end |
454 in (skolems, Const (s, T)) end |
472 | aux skolems (t1 $ t2) = |
455 | aux skolems (t1 $ t2) = |
473 let |
456 let |
474 val (skolems, t1) = aux skolems t1 |
457 val (skolems, t1) = aux skolems t1 |