# HG changeset patch # User blanchet # Date 1280244730 -7200 # Node ID 3ad3e3ca24511ca22f4f36b86a2245e854495a73 # Parent 135f7d48949259b4f964074efec4ed634c1bc950 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format" diff -r 135f7d489492 -r 3ad3e3ca2451 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:15:12 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jul 27 17:32:10 2010 +0200 @@ -118,13 +118,26 @@ (* Clause preparation *) +datatype fol_formula = + FOLFormula of {formula_name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_ahorn [] phi = phi + | mk_ahorn (phi :: phis) psi = + AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) + +(* ### FIXME: reintroduce fun make_clause_table xs = fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty - (* Remove existing axiom clauses from the conjecture clauses, as this can dramatically boost an ATP's performance (for some reason). *) fun subtract_cls ax_clauses = filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) +*) fun combformula_for_prop thy = let @@ -320,6 +333,262 @@ class_rel_clauses, arity_clauses)) end +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" +val arity_clause_prefix = "clsarity_" +val tfrees_name = "tfrees" + +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) + +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) + +fun fo_literal_for_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_for_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot + +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name, _, ty_args) => + if fst name = "equal" then + (if top_level andalso length args = 2 then name + else ("c_fequal", @{const_name fequal}), []) + else + (name, if full_types then [] else ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = APred (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = + mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) + (type_literals_for_types ctypes_sorts)) + (formula_for_combformula full_types combformula) + +fun problem_line_for_axiom full_types + (formula as FOLFormula {formula_name, kind, ...}) = + Fof (axiom_prefix ^ ascii_of formula_name, kind, + formula_for_axiom full_types formula) + +fun problem_line_for_class_rel_clause + (ClassRelClause {axiom_name, subclass, superclass, ...}) = + let val ty_arg = ATerm (("T", "T"), []) in + Fof (ascii_of axiom_name, Axiom, + AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), + APred (ATerm (superclass, [ty_arg]))])) + end + +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_for_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun problem_line_for_arity_clause + (ArityClause {axiom_name, conclLit, premLits, ...}) = + Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, + mk_ahorn (map (formula_for_fo_literal o apfst not + o fo_literal_for_arity_literal) premLits) + (formula_for_fo_literal + (fo_literal_for_arity_literal conclLit))) + +fun problem_line_for_conjecture full_types + (FOLFormula {formula_name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ formula_name, kind, + formula_for_combformula full_types combformula) + +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = + map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) + +fun problem_line_for_free_type lit = + Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) +fun problem_lines_for_free_types conjectures = + let + val litss = map free_type_literals_for_conjecture conjectures + val lits = fold (union (op =)) litss [] + in map problem_line_for_free_type lits end + +(** "hBOOL" and "hAPP" **) + +type const_info = {min_arity: int, max_arity: int, sub_level: bool} + +fun consider_term top_level (ATerm ((s, _), ts)) = + (if is_tptp_variable s then + I + else + let val n = length ts in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end) + #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (APred tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem problem = fold (fold consider_problem_line o snd) problem + +fun const_table_for_problem explicit_apply problem = + if explicit_apply then NONE + else SOME (Symtab.empty |> consider_problem problem) + +val tc_fun = make_fixed_type_const @{type_name fun} + +fun min_arity_of thy full_types NONE s = + (if s = "equal" orelse s = type_wrapper_name orelse + String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s then + 16383 (* large number *) + else if full_types then + 0 + else case strip_prefix_and_undo_ascii const_prefix s of + SOME s' => num_type_args thy (invert_const s') + | NONE => 0) + | min_arity_of _ _ (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME ({min_arity, ...} : const_info) => min_arity + | NONE => 0 + +fun full_type_of (ATerm ((s, _), [ty, _])) = + if s = type_wrapper_name then ty else raise Fail "expected type wrapper" + | full_type_of _ = raise Fail "expected type wrapper" + +fun list_hAPP_rev _ t1 [] = t1 + | list_hAPP_rev NONE t1 (t2 :: ts2) = + ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) + | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [full_type_of t2, ty]) in + ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + +fun repair_applications_in_term thy full_types const_tab = + let + fun aux opt_ty (ATerm (name as (s, _), ts)) = + if s = type_wrapper_name then + case ts of + [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) + | _ => raise Fail "malformed type wrapper" + else + let + val ts = map (aux NONE) ts + val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts + in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end + in aux NONE end + +fun boolify t = ATerm (`I "hBOOL", [t]) + +(* True if the constant ever appears outside of the top-level position in + literals, or if it appears with different arities (e.g., because of different + type instantiations). If false, the constant always receives all of its + arguments and is used as a predicate. *) +fun is_predicate NONE s = + s = "equal" orelse String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s + | is_predicate (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME {min_arity, max_arity, sub_level} => + not sub_level andalso min_arity = max_arity + | NONE => false + +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = + if s = type_wrapper_name then + case ts of + [_, t' as ATerm ((s', _), _)] => + if is_predicate const_tab s' then t' else boolify t + | _ => raise Fail "malformed type wrapper" + else + t |> not (is_predicate const_tab s) ? boolify + +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_tptp_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (q, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (APred tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = + APred (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +fun repair_problem_with_const_table thy = + map o apsnd o map ooo repair_problem_line thy + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types + (const_table_for_problem explicit_apply problem) problem + +fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply + file (conjectures, axiom_clauses, extra_clauses, + helper_clauses, class_rel_clauses, arity_clauses) = + let + val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses + val class_rel_lines = + map problem_line_for_class_rel_clause class_rel_clauses + val arity_lines = map problem_line_for_arity_clause arity_clauses + val helper_lines = map (problem_line_for_axiom full_types) helper_clauses + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures + (* Reordering these might or might not confuse the proof reconstruction + code or the SPASS Flotter hack. *) + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply + val (problem, pool) = nice_tptp_problem readable_names problem + val conjecture_offset = + length axiom_lines + length class_rel_lines + length arity_lines + + length helper_lines + val _ = File.write_list file (strings_for_tptp_problem problem) + in + (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset) + end + fun extract_clause_sequence output = let val tokens_of = String.tokens (not o Char.isAlphaNum) diff -r 135f7d489492 -r 3ad3e3ca2451 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:15:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jul 27 17:32:10 2010 +0200 @@ -323,8 +323,10 @@ case strip_prefix_and_undo_ascii schematic_var_prefix a of SOME b => Var ((b, 0), T) | NONE => - if is_variable a then Var ((fix_atp_variable_name a, 0), T) - else raise Fail ("Unexpected constant: " ^ quote a) + if is_tptp_variable a then + Var ((fix_atp_variable_name a, 0), T) + else + raise Fail ("Unexpected constant: " ^ quote a) in list_comb (t, ts) end in aux (SOME HOLogic.boolT) [] end diff -r 135f7d489492 -r 3ad3e3ca2451 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 17:15:12 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 17:32:10 2010 +0200 @@ -7,11 +7,7 @@ signature SLEDGEHAMMER_TPTP_FORMAT = sig - type name = Metis_Clauses.name type kind = Metis_Clauses.kind - type combterm = Metis_Clauses.combterm - type class_rel_clause = Metis_Clauses.class_rel_clause - type arity_clause = Metis_Clauses.arity_clause datatype 'a fo_term = ATerm of 'a * 'a fo_term list datatype quantifier = AForall | AExists @@ -21,28 +17,24 @@ AConn of connective * ('a, 'b) formula list | APred of 'b - datatype fol_formula = - FOLFormula of {formula_name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} + datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula + type 'a problem = (string * 'a problem_line list) list - val axiom_prefix : string - val conjecture_prefix : string - val is_variable : string -> bool - val write_tptp_file : - theory -> bool -> bool -> bool -> bool -> Path.T - -> fol_formula list * fol_formula list * fol_formula list * fol_formula list - * class_rel_clause list * arity_clause list - -> string Symtab.table * int + val is_tptp_variable : string -> bool + val strings_for_tptp_problem : + (string * string problem_line list) list -> string list + val nice_tptp_problem : + bool -> ('a * (string * string) problem_line list) list + -> ('a * string problem_line list) list + * (string Symtab.table * string Symtab.table) option end; structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = struct -open Metis_Clauses open Sledgehammer_Util +type kind = Metis_Clauses.kind (** ATP problem **) @@ -54,12 +46,6 @@ AConn of connective * ('a, 'b) formula list | APred of 'b -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) -fun mk_ahorn [] phi = phi - | mk_ahorn (phi :: phis) psi = - AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) - datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula type 'a problem = (string * 'a problem_line list) list @@ -92,7 +78,7 @@ "fof(" ^ ident ^ ", " ^ (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ " (" ^ string_for_formula phi ^ ")).\n" -fun strings_for_problem problem = +fun strings_for_tptp_problem problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: maps (fn (_, []) => [] @@ -100,6 +86,8 @@ "\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" :: map string_for_problem_line lines) problem +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0)) + (** Nice names **) @@ -159,272 +147,7 @@ fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem - - -(** Sledgehammer stuff **) - -datatype fol_formula = - FOLFormula of {formula_name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - -val axiom_prefix = "ax_" -val conjecture_prefix = "conj_" -val arity_clause_prefix = "clsarity_" -val tfrees_name = "tfrees" - -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) - -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot - -fun fo_term_for_combterm full_types = - let - fun aux top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name, _, ty_args) => - if fst name = "equal" then - (if top_level andalso length args = 2 then name - else ("c_fequal", @{const_name fequal}), []) - else - (name, if full_types then [] else ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) - in - if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t - end - in aux true end - -fun formula_for_combformula full_types = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = APred (fo_term_for_combterm full_types tm) - in aux end - -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (type_literals_for_types ctypes_sorts)) - (formula_for_combformula full_types combformula) - -fun problem_line_for_axiom full_types - (formula as FOLFormula {formula_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of formula_name, kind, - formula_for_axiom full_types formula) - -fun problem_line_for_class_rel_clause - (ClassRelClause {axiom_name, subclass, superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in - Fof (ascii_of axiom_name, Axiom, - AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), - APred (ATerm (superclass, [ty_arg]))])) - end - -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun problem_line_for_arity_clause - (ArityClause {axiom_name, conclLit, premLits, ...}) = - Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) - -fun problem_line_for_conjecture full_types - (FOLFormula {formula_name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ formula_name, kind, - formula_for_combformula full_types combformula) - -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = - map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) - -fun problem_line_for_free_type lit = - Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) -fun problem_lines_for_free_types conjectures = - let - val litss = map free_type_literals_for_conjecture conjectures - val lits = fold (union (op =)) litss [] - in map problem_line_for_free_type lits end - -(** "hBOOL" and "hAPP" **) - -type const_info = {min_arity: int, max_arity: int, sub_level: bool} - -fun is_variable s = Char.isUpper (String.sub (s, 0)) - -fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi - | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (APred tm) = consider_term true tm - -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi -fun consider_problem problem = fold (fold consider_problem_line o snd) problem - -fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) - -val tc_fun = make_fixed_type_const @{type_name fun} - -fun min_arity_of thy full_types NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse - String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s then - 16383 (* large number *) - else if full_types then - 0 - else case strip_prefix_and_undo_ascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') - | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity - | NONE => 0 - -fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" - -fun list_hAPP_rev _ t1 [] = t1 - | list_hAPP_rev NONE t1 (t2 :: ts2) = - ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) - | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end - -fun repair_applications_in_term thy full_types const_tab = - let - fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then - case ts of - [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" - else - let - val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts - in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end - in aux NONE end - -fun boolify t = ATerm (`I "hBOOL", [t]) - -(* True if the constant ever appears outside of the top-level position in - literals, or if it appears with different arities (e.g., because of different - type instantiations). If false, the constant always receives all of its - arguments and is used as a predicate. *) -fun is_predicate NONE s = - s = "equal" orelse String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity - | NONE => false - -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" - else - t |> not (is_predicate const_tab s) ? boolify - -fun close_universally phi = - let - fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_variable s andalso not (member (op =) bounds name)) - ? insert (op =) name - #> fold (term_vars bounds) tms - fun formula_vars bounds (AQuant (q, xs, phi)) = - formula_vars (xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (APred tm) = term_vars bounds tm - in - case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) - end - -fun repair_formula thy explicit_forall full_types const_tab = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (APred tm) = - APred (tm |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) - in aux #> explicit_forall ? close_universally end - -fun repair_problem_line thy explicit_forall full_types const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy - -fun repair_problem thy explicit_forall full_types explicit_apply problem = - repair_problem_with_const_table thy explicit_forall full_types - (const_table_for_problem explicit_apply problem) problem - -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, extra_clauses, - helper_clauses, class_rel_clauses, arity_clauses) = - let - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses - val class_rel_lines = - map problem_line_for_class_rel_clause class_rel_clauses - val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures - (* Reordering these might or might not confuse the proof reconstruction - code or the SPASS Flotter hack. *) - val problem = - [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall full_types explicit_apply - val (problem, pool) = nice_problem problem (empty_name_pool readable_names) - val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines - + length helper_lines - val _ = File.write_list file (strings_for_problem problem) - in - (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset) - end +fun nice_tptp_problem readable_names problem = + nice_problem problem (empty_name_pool readable_names) end;