--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sat Jul 24 18:08:43 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Jul 25 15:43:53 2010 +0200
@@ -239,6 +239,43 @@
class_rel_clauses, arity_clauses))
end
+fun extract_clause_sequence output =
+ let
+ val tokens_of = String.tokens (not o Char.isAlphaNum)
+ fun extract_num ("clause" :: (ss as _ :: _)) =
+ Int.fromString (List.last ss)
+ | extract_num _ = NONE
+ in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+val parse_clause_formula_pair =
+ $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+ --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+ Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+ |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+ Substring.full
+ #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.string #> strip_spaces #> explode
+ #> parse_clause_formula_relation #> fst
+
+fun repair_theorem_names output thm_names =
+ if String.isSubstring set_ClauseFormulaRelationN output then
+ let
+ val seq = extract_clause_sequence output
+ val name_map = extract_clause_formula_relation output
+ in
+ seq |> map (the o AList.lookup (op =) name_map)
+ |> map (fn s => case try (unprefix axiom_prefix) s of
+ SOME s' => undo_ascii_of s'
+ | NONE => "")
+ |> Vector.fromList
+ end
+ else
+ thm_names
+
(* generic TPTP-based provers *)
@@ -298,15 +335,7 @@
(if Config.get ctxt measure_runtime then
"TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
else
- "exec " ^ core) ^ " 2>&1" ^
- (if overlord then
- " | sed 's/,/, /g' \
- \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \
- \| sed 's/ / /g' | sed 's/| |/||/g' \
- \| sed 's/ = = =/===/g' \
- \| sed 's/= = /== /g'"
- else
- "")
+ "exec " ^ core) ^ " 2>&1"
end
fun split_time s =
let
@@ -320,7 +349,9 @@
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
fun run_on probfile =
- if File.exists command then
+ if home = "" then
+ error ("The environment variable " ^ quote home_var ^ " is not set.")
+ else if File.exists command then
let
fun do_run complete =
let
@@ -350,8 +381,6 @@
(output, msecs0 + msecs, proof, outcome))
| result => result)
in ((pool, conjecture_shape), result) end
- else if home = "" then
- error ("The environment variable " ^ quote home_var ^ " is not set.")
else
error ("Bad executable: " ^ Path.implode command ^ ".");
@@ -367,6 +396,7 @@
val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
with_path cleanup export run_on (prob_pathname subgoal)
+ val internal_thm_names = repair_theorem_names output internal_thm_names
val (message, relevant_thm_names) =
case outcome of
@@ -417,11 +447,11 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
- {home_var = "SPASS_HOME",
- executable = "SPASS",
+ {home_var = "ISABELLE_ATP_MANAGER",
+ executable = "SPASS_TPTP",
(* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
- ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
+ ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^
string_of_int (to_generous_secs timeout div 2))
|> not complete ? prefix "-SOS=1 ",
@@ -432,8 +462,7 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
- (OldSpass, "unrecognized option `-TPTP'"),
- (OldSpass, "Unrecognized option TPTP")],
+ (OldSpass, "tptp2dfg")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
val spass = tptp_prover "spass" spass_config
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jul 24 18:08:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Jul 25 15:43:53 2010 +0200
@@ -33,12 +33,11 @@
type minimize_command = string list -> string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-
val index_in_shape : int -> int list list -> int =
find_index o exists o curry (op =)
-fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+fun is_axiom_clause_number thm_names num =
+ num > 0 andalso num <= Vector.length thm_names andalso
+ Vector.sub (thm_names, num - 1) <> ""
fun is_conjecture_clause_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
@@ -57,23 +56,6 @@
(**** PARSING OF TSTP FORMAT ****)
-fun strip_spaces_in_list [] = ""
- | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
- | strip_spaces_in_list [c1, c2] =
- strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
- | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
- if Char.isSpace c1 then
- strip_spaces_in_list (c2 :: c3 :: cs)
- else if Char.isSpace c2 then
- if Char.isSpace c3 then
- strip_spaces_in_list (c1 :: c3 :: cs)
- else
- str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
- strip_spaces_in_list (c3 :: cs)
- else
- str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
-
(* Syntax trees, either term list or formulae *)
datatype node = IntLeaf of int | StrNode of string * node list
@@ -85,9 +67,6 @@
(*Strings enclosed in single quotes, e.g. filenames*)
val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
-(*Integer constants, typically proof line numbers*)
-val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
val parse_dollar_name =
Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
@@ -102,7 +81,7 @@
forever at compile time. *)
fun parse_term pool x =
(parse_quoted >> str_leaf
- || parse_integer >> IntLeaf
+ || scan_integer >> IntLeaf
|| (parse_dollar_name >> repair_name pool)
-- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
|| $$ "(" |-- parse_term pool --| $$ ")"
@@ -149,11 +128,11 @@
fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
fun parse_tstp_line pool =
- ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
+ ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
--| Scan.this_string "definition" --| $$ "," -- parse_definition pool
--| parse_tstp_annotations --| $$ ")" --| $$ "."
>> finish_tstp_definition_line)
- || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
+ || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
--| Symbol.scan_id --| $$ "," -- parse_clause pool
-- parse_tstp_annotations --| $$ ")" --| $$ "."
>> finish_tstp_inference_line)
@@ -162,7 +141,7 @@
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
is not clear anyway. *)
-val parse_dot_name = parse_integer --| $$ "." --| parse_integer
+val parse_dot_name = scan_integer --| $$ "." --| scan_integer
val parse_spass_annotations =
Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
@@ -185,7 +164,7 @@
<cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
fun parse_spass_line pool =
- parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+ scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
>> finish_spass_line
@@ -529,14 +508,14 @@
(** EXTRACTING LEMMAS **)
(* A list consisting of the first number in each line is returned.
- TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
+ TSTP: Interesting lines have the form "fof(108, axiom, ...)", where the
number (108) is extracted.
SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
extracted. *)
-fun extract_clause_numbers_in_atp_proof atp_proof =
+fun extract_formula_numbers_in_atp_proof atp_proof =
let
- val tokens_of = String.tokens (not o is_ident_char)
- fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
+ val tokens_of = String.tokens (not o Char.isAlphaNum)
+ fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
| extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
| extract_num _ = NONE
in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
@@ -579,7 +558,7 @@
i) =
let
val raw_lemmas =
- atp_proof |> extract_clause_numbers_in_atp_proof
+ atp_proof |> extract_formula_numbers_in_atp_proof
|> filter (is_axiom_clause_number thm_names)
|> map (fn i => Vector.sub (thm_names, i - 1))
val (chained_lemmas, other_lemmas) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sat Jul 24 18:08:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sun Jul 25 15:43:53 2010 +0200
@@ -11,6 +11,7 @@
type arity_clause = Metis_Clauses.arity_clause
type fol_clause = Metis_Clauses.fol_clause
+ val axiom_prefix : string
val write_tptp_file :
theory -> bool -> bool -> bool -> Path.T
-> fol_clause list * fol_clause list * fol_clause list * fol_clause list
@@ -27,23 +28,44 @@
(** ATP problem **)
-datatype 'a atp_term = ATerm of 'a * 'a atp_term list
-type 'a atp_literal = bool * 'a atp_term
-datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list
+datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype quantifier = AForall | AExists
+datatype connective = ANot | AAnd | AOr | AImplies | AIff
+datatype 'a formula =
+ AQuant of quantifier * 'a list * 'a formula |
+ AConn of connective * 'a formula list |
+ APred of 'a fo_term
+
+fun mk_anot phi = AConn (ANot, [phi])
+
+datatype 'a problem_line = Fof of string * kind * 'a formula
type 'a problem = (string * 'a problem_line list) list
-fun string_for_atp_term (ATerm (s, [])) = s
- | string_for_atp_term (ATerm (s, ts)) =
- s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")"
-fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) =
- string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^
- string_for_atp_term t2
- | string_for_atp_literal (pos, t) =
- (if pos then "" else "~ ") ^ string_for_atp_term t
-fun string_for_problem_line (Cnf (ident, kind, lits)) =
- "cnf(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^
- " (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n"
+fun string_for_term (ATerm (s, [])) = s
+ | string_for_term (ATerm (s, ts)) =
+ if s = "equal" then space_implode " = " (map string_for_term ts)
+ else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+fun string_for_quantifier AForall = "!"
+ | string_for_quantifier AExists = "?"
+fun string_for_connective ANot = "~"
+ | string_for_connective AAnd = "&"
+ | string_for_connective AOr = "|"
+ | string_for_connective AImplies = "=>"
+ | string_for_connective AIff = "<=>"
+fun string_for_formula (AQuant (q, xs, phi)) =
+ string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^
+ string_for_formula phi
+ | string_for_formula (AConn (c, [phi])) =
+ string_for_connective c ^ " " ^ string_for_formula phi
+ | string_for_formula (AConn (c, phis)) =
+ "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
+ (map string_for_formula phis) ^ ")"
+ | string_for_formula (APred tm) = string_for_term tm
+
+fun string_for_problem_line (Fof (ident, kind, phi)) =
+ "fof(" ^ ident ^ ", " ^
+ (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
+ " (" ^ string_for_formula phi ^ ")).\n"
fun strings_for_problem problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
@@ -97,11 +119,17 @@
end
in add 0 |> apsnd SOME end
-fun nice_atp_term (ATerm (name, ts)) =
- nice_name name ##>> pool_map nice_atp_term ts #>> ATerm
-fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
-fun nice_problem_line (Cnf (ident, kind, lits)) =
- pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
+
+fun nice_term (ATerm (name, ts)) =
+ nice_name name ##>> pool_map nice_term ts #>> ATerm
+fun nice_formula (AQuant (q, xs, phi)) =
+ pool_map nice_name xs ##>> nice_formula phi
+ #>> (fn (xs, phi) => AQuant (q, xs, phi))
+ | nice_formula (AConn (c, phis)) =
+ pool_map nice_formula phis #>> curry AConn c
+ | nice_formula (APred tm) = nice_term tm #>> APred
+fun nice_problem_line (Fof (ident, kind, phi)) =
+ nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading) problem
@@ -109,20 +137,20 @@
(** Sledgehammer stuff **)
-val clause_prefix = "cls_"
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
val arity_clause_prefix = "clsarity_"
-fun hol_ident axiom_name clause_id =
- clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
+fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-fun atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
- | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
- | atp_term_for_combtyp (CombType (name, tys)) =
- ATerm (name, map atp_term_for_combtyp tys)
+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 atp_term_for_combterm full_types top_level u =
+fun fo_term_for_combterm full_types top_level u =
let
val (head, args) = strip_combterm_comb u
val (x, ty_args) =
@@ -135,58 +163,67 @@
(name, if full_types then [] else ty_args)
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
- val t = ATerm (x, map atp_term_for_combtyp ty_args @
- map (atp_term_for_combterm full_types false) args)
+ val t = ATerm (x, map fo_term_for_combtyp ty_args @
+ map (fo_term_for_combterm full_types false) args)
in
- if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t
+ if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t
else t
end
-fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
- (pos, atp_term_for_combterm full_types true t)
+fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) =
+ (pos, fo_term_for_combterm full_types true t)
-fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
+fun fo_literal_for_type_literal pos (TyLitVar (class, name)) =
(pos, ATerm (class, [ATerm (name, [])]))
- | atp_literal_for_type_literal pos (TyLitFree (class, name)) =
+ | fo_literal_for_type_literal pos (TyLitFree (class, name)) =
(pos, ATerm (class, [ATerm (name, [])]))
-fun atp_literals_for_axiom full_types
- (FOLClause {literals, ctypes_sorts, ...}) =
- map (atp_literal_for_literal full_types) literals @
- map (atp_literal_for_type_literal false)
+fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot
+fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), []))
+ | formula_for_fo_literals (lit :: lits) =
+ AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits])
+
+fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) =
+ map (fo_literal_for_literal full_types) literals @
+ map (fo_literal_for_type_literal false)
(type_literals_for_types ctypes_sorts)
+ |> formula_for_fo_literals
fun problem_line_for_axiom full_types
- (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
- Cnf (hol_ident axiom_name clause_id, kind,
- atp_literals_for_axiom full_types clause)
+ (clause as FOLClause {axiom_name, kind, ...}) =
+ Fof (hol_ident axiom_prefix axiom_name, kind,
+ formula_for_axiom full_types clause)
fun problem_line_for_class_rel_clause
(ClassRelClause {axiom_name, subclass, superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
- Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
- (true, ATerm (superclass, [ty_arg]))])
+ Fof (ascii_of axiom_name, Axiom,
+ AConn (AImplies, [APred (ATerm (subclass, [ty_arg])),
+ APred (ATerm (superclass, [ty_arg]))]))
end
-fun atp_literal_for_arity_literal (TConsLit (c, t, args)) =
+fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | atp_literal_for_arity_literal (TVarLit (c, sort)) =
+ | fo_literal_for_arity_literal (TVarLit (c, sort)) =
(false, ATerm (c, [ATerm (sort, [])]))
fun problem_line_for_arity_clause
(ArityClause {axiom_name, conclLit, premLits, ...}) =
- Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
- map atp_literal_for_arity_literal (conclLit :: premLits))
+ Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+ map fo_literal_for_arity_literal (conclLit :: premLits)
+ |> formula_for_fo_literals)
fun problem_line_for_conjecture full_types
- (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
- Cnf (hol_ident axiom_name clause_id, kind,
- map (atp_literal_for_literal full_types) literals)
+ (clause as FOLClause {axiom_name, kind, literals, ...}) =
+ Fof (hol_ident conjecture_prefix axiom_name, kind,
+ map (fo_literal_for_literal full_types) literals
+ |> formula_for_fo_literals |> mk_anot)
fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
- map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
+ map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
-fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
+fun problem_line_for_free_type lit =
+ Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
fun problem_lines_for_free_types conjectures =
let
val litss = map atp_free_type_literals_for_conjecture conjectures
@@ -197,10 +234,10 @@
type const_info = {min_arity: int, max_arity: int, sub_level: bool}
-fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
+fun is_variable s = Char.isUpper (String.sub (s, 0))
fun consider_term top_level (ATerm ((s, _), ts)) =
- (if is_atp_variable s then
+ (if is_variable s then
I
else
let val n = length ts in
@@ -212,8 +249,11 @@
sub_level = sub_level orelse not top_level})
end)
#> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
-fun consider_literal (_, t) = consider_term true t
-fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
+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 =
@@ -288,21 +328,43 @@
else
t |> not (is_predicate const_tab s) ? boolify
-fun repair_literal thy full_types const_tab (pos, t) =
- (pos, t |> repair_applications_in_term thy full_types const_tab
- |> repair_predicates_in_term const_tab)
-fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
- Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
-fun repair_problem_with_const_table thy full_types const_tab problem =
- map (apsnd (map (repair_problem_line thy full_types const_tab))) problem
-fun repair_problem thy full_types explicit_apply problem =
- repair_problem_with_const_table thy full_types
+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)
+val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line
+
+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 full_types explicit_apply file
(conjectures, axiom_clauses, extra_clauses, helper_clauses,
class_rel_clauses, arity_clauses) =
let
+ val explicit_forall = true (* FIXME *)
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
@@ -311,13 +373,14 @@
val conjecture_lines =
map (problem_line_for_conjecture full_types) conjectures
val tfree_lines = problem_lines_for_free_types conjectures
- 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 full_types explicit_apply
+ 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