--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 14:07:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 15:04:49 2010 +0200
@@ -27,23 +27,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 +118,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
@@ -117,12 +144,12 @@
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 +162,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)
+ Fof (hol_ident axiom_name clause_id, 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)
+ Fof (hol_ident axiom_name clause_id, 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 +233,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 +248,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 +327,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 +372,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