--- 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;