--- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
@@ -15,10 +15,11 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
+ datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Type_Decl of string * 'a * 'a list * 'a |
- Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+ Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -45,10 +46,11 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
+datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Type_Decl of string * 'a * 'a list * 'a |
- Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
+ Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
* string fo_term option * string fo_term option
type 'a problem = (string * 'a problem_line list) list
@@ -92,12 +94,6 @@
(map string_for_formula phis) ^ ")"
| string_for_formula (AAtom tm) = string_for_term tm
-fun formula_needs_typed_logic (AQuant (_, xs, phi)) =
- exists (is_some o snd) xs orelse formula_needs_typed_logic phi
- | formula_needs_typed_logic (AConn (_, phis)) =
- exists formula_needs_typed_logic phis
- | formula_needs_typed_logic (AAtom _) = false
-
fun string_for_symbol_type [] res_ty = res_ty
| string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
| string_for_symbol_type arg_tys res_ty =
@@ -107,7 +103,7 @@
"tff(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
string_for_symbol_type arg_tys res_ty ^ ").\n"
| string_for_problem_line use_conjecture_for_hypotheses
- (Formula (ident, kind, phi, source, useful_info)) =
+ (Formula (logic, ident, kind, phi, source, useful_info)) =
let
val (kind, phi) =
if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -115,7 +111,7 @@
else
(kind, phi)
in
- (if formula_needs_typed_logic phi then "tff" else "fof") ^
+ (case logic of Fof => "fof" | Tff => "tff") ^
"(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
string_for_formula phi ^ ")" ^
(case (source, useful_info) of
@@ -210,9 +206,9 @@
##>> pool_map nice_name arg_tys
##>> nice_name res_ty
#>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
- | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
+ | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
nice_formula phi
- #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
+ #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading) problem
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
@@ -332,7 +332,7 @@
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
in
- [Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
+ [Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
AAtom (ATerm (`I "equal",
[tag (tag (var "Y")), tag (var "Y")]))
|> close_formula_universally, NONE, NONE)]
@@ -549,18 +549,22 @@
(formula_for_combformula ctxt type_sys
(close_combformula_universally combformula))
+fun logic_for_type_sys Many_Typed = Tff
+ | logic_for_type_sys _ = Fof
+
(* Each fact is given a unique fact number to avoid name clashes (e.g., because
of monomorphization). The TPTP explicitly forbids name clashes, and some of
the remote provers might care. *)
fun problem_line_for_fact ctxt prefix type_sys
(j, formula as {name, kind, ...}) =
- Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name,
- kind, formula_for_fact ctxt type_sys formula, NONE, NONE)
+ Formula (logic_for_type_sys type_sys,
+ prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
+ formula_for_fact ctxt type_sys formula, NONE, NONE)
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
- Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+ Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
AAtom (ATerm (superclass, [ty_arg]))]),
NONE, NONE)
@@ -573,7 +577,7 @@
fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
...}) =
- Formula (arity_clause_prefix ^ ascii_of name, Axiom,
+ Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
mk_ahorn (map (formula_for_fo_literal o apfst not
o fo_literal_for_arity_literal) premLits)
(formula_for_fo_literal
@@ -581,7 +585,7 @@
fun problem_line_for_conjecture ctxt type_sys
({name, kind, combformula, ...} : translated_formula) =
- Formula (conjecture_prefix ^ name, kind,
+ Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
formula_for_combformula ctxt type_sys
(close_combformula_universally combformula),
NONE, NONE)
@@ -591,7 +595,7 @@
|> map fo_literal_for_type_literal
fun problem_line_for_free_type j lit =
- Formula (tfree_prefix ^ string_of_int j, Hypothesis,
+ Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
formula_for_fo_literal lit, NONE, NONE)
fun problem_lines_for_free_types type_sys facts =
let
@@ -619,7 +623,7 @@
val consider_formula_syms = fold_formula (consider_term_syms true)
fun consider_problem_line_syms (Type_Decl _) = I
- | consider_problem_line_syms (Formula (_, _, phi, _, _)) =
+ | consider_problem_line_syms (Formula (_, _, _, phi, _, _)) =
consider_formula_syms phi
fun consider_problem_syms problem =
fold (fold consider_problem_line_syms o snd) problem
@@ -714,9 +718,9 @@
in aux #> close_formula_universally end
fun repair_problem_line thy type_sys sym_tab
- (Formula (ident, kind, phi, source, useful_info)) =
- Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source,
- useful_info)
+ (Formula (logic, ident, kind, phi, source, useful_info)) =
+ Formula (logic, ident, kind, repair_formula thy type_sys sym_tab phi,
+ source, useful_info)
| repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula"
fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
@@ -771,7 +775,7 @@
val bound_tms =
map (fn (name, ty) => CombConst (name, the ty, [])) bounds
in
- Formula (type_decl_prefix ^ ascii_of s, Axiom,
+ Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom,
mk_aquant AForall bounds
(has_type_combatom res_ty
(fold (curry (CombApp o swap)) bound_tms
@@ -815,7 +819,7 @@
val sym_tab = sym_table_for_problem explicit_apply problem
val problem = problem |> repair_problem thy type_sys sym_tab
val helper_facts =
- problem |> maps (map_filter (fn Formula (_, _, phi, _, _) => SOME phi
+ problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
| _ => NONE) o snd)
|> get_helper_facts ctxt type_sys
val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
@@ -848,7 +852,7 @@
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
+fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
fold_formula (add_term_weights weight) phi
| add_problem_line_weights _ _ = I