generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)
1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 01 18:37:24 2011 +0200
1.3 @@ -15,10 +15,11 @@
1.4 AConn of connective * ('a, 'b, 'c) formula list |
1.5 AAtom of 'c
1.6
1.7 + datatype logic = Fof | Tff
1.8 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.9 datatype 'a problem_line =
1.10 Type_Decl of string * 'a * 'a list * 'a |
1.11 - Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.12 + Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
1.13 * string fo_term option * string fo_term option
1.14 type 'a problem = (string * 'a problem_line list) list
1.15
1.16 @@ -45,10 +46,11 @@
1.17 AConn of connective * ('a, 'b, 'c) formula list |
1.18 AAtom of 'c
1.19
1.20 +datatype logic = Fof | Tff
1.21 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
1.22 datatype 'a problem_line =
1.23 Type_Decl of string * 'a * 'a list * 'a |
1.24 - Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
1.25 + Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
1.26 * string fo_term option * string fo_term option
1.27 type 'a problem = (string * 'a problem_line list) list
1.28
1.29 @@ -92,12 +94,6 @@
1.30 (map string_for_formula phis) ^ ")"
1.31 | string_for_formula (AAtom tm) = string_for_term tm
1.32
1.33 -fun formula_needs_typed_logic (AQuant (_, xs, phi)) =
1.34 - exists (is_some o snd) xs orelse formula_needs_typed_logic phi
1.35 - | formula_needs_typed_logic (AConn (_, phis)) =
1.36 - exists formula_needs_typed_logic phis
1.37 - | formula_needs_typed_logic (AAtom _) = false
1.38 -
1.39 fun string_for_symbol_type [] res_ty = res_ty
1.40 | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
1.41 | string_for_symbol_type arg_tys res_ty =
1.42 @@ -107,7 +103,7 @@
1.43 "tff(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^
1.44 string_for_symbol_type arg_tys res_ty ^ ").\n"
1.45 | string_for_problem_line use_conjecture_for_hypotheses
1.46 - (Formula (ident, kind, phi, source, useful_info)) =
1.47 + (Formula (logic, ident, kind, phi, source, useful_info)) =
1.48 let
1.49 val (kind, phi) =
1.50 if kind = Hypothesis andalso use_conjecture_for_hypotheses then
1.51 @@ -115,7 +111,7 @@
1.52 else
1.53 (kind, phi)
1.54 in
1.55 - (if formula_needs_typed_logic phi then "tff" else "fof") ^
1.56 + (case logic of Fof => "fof" | Tff => "tff") ^
1.57 "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
1.58 string_for_formula phi ^ ")" ^
1.59 (case (source, useful_info) of
1.60 @@ -210,9 +206,9 @@
1.61 ##>> pool_map nice_name arg_tys
1.62 ##>> nice_name res_ty
1.63 #>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
1.64 - | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
1.65 + | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
1.66 nice_formula phi
1.67 - #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
1.68 + #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
1.69 fun nice_problem problem =
1.70 pool_map (fn (heading, lines) =>
1.71 pool_map nice_problem_line lines #>> pair heading) problem
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:24 2011 +0200
2.3 @@ -332,7 +332,7 @@
2.4 fun var s = ATerm (`I s, [])
2.5 fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
2.6 in
2.7 - [Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
2.8 + [Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
2.9 AAtom (ATerm (`I "equal",
2.10 [tag (tag (var "Y")), tag (var "Y")]))
2.11 |> close_formula_universally, NONE, NONE)]
2.12 @@ -549,18 +549,22 @@
2.13 (formula_for_combformula ctxt type_sys
2.14 (close_combformula_universally combformula))
2.15
2.16 +fun logic_for_type_sys Many_Typed = Tff
2.17 + | logic_for_type_sys _ = Fof
2.18 +
2.19 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
2.20 of monomorphization). The TPTP explicitly forbids name clashes, and some of
2.21 the remote provers might care. *)
2.22 fun problem_line_for_fact ctxt prefix type_sys
2.23 (j, formula as {name, kind, ...}) =
2.24 - Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name,
2.25 - kind, formula_for_fact ctxt type_sys formula, NONE, NONE)
2.26 + Formula (logic_for_type_sys type_sys,
2.27 + prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
2.28 + formula_for_fact ctxt type_sys formula, NONE, NONE)
2.29
2.30 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
2.31 superclass, ...}) =
2.32 let val ty_arg = ATerm (("T", "T"), []) in
2.33 - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
2.34 + Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
2.35 AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
2.36 AAtom (ATerm (superclass, [ty_arg]))]),
2.37 NONE, NONE)
2.38 @@ -573,7 +577,7 @@
2.39
2.40 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
2.41 ...}) =
2.42 - Formula (arity_clause_prefix ^ ascii_of name, Axiom,
2.43 + Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
2.44 mk_ahorn (map (formula_for_fo_literal o apfst not
2.45 o fo_literal_for_arity_literal) premLits)
2.46 (formula_for_fo_literal
2.47 @@ -581,7 +585,7 @@
2.48
2.49 fun problem_line_for_conjecture ctxt type_sys
2.50 ({name, kind, combformula, ...} : translated_formula) =
2.51 - Formula (conjecture_prefix ^ name, kind,
2.52 + Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
2.53 formula_for_combformula ctxt type_sys
2.54 (close_combformula_universally combformula),
2.55 NONE, NONE)
2.56 @@ -591,7 +595,7 @@
2.57 |> map fo_literal_for_type_literal
2.58
2.59 fun problem_line_for_free_type j lit =
2.60 - Formula (tfree_prefix ^ string_of_int j, Hypothesis,
2.61 + Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
2.62 formula_for_fo_literal lit, NONE, NONE)
2.63 fun problem_lines_for_free_types type_sys facts =
2.64 let
2.65 @@ -619,7 +623,7 @@
2.66 val consider_formula_syms = fold_formula (consider_term_syms true)
2.67
2.68 fun consider_problem_line_syms (Type_Decl _) = I
2.69 - | consider_problem_line_syms (Formula (_, _, phi, _, _)) =
2.70 + | consider_problem_line_syms (Formula (_, _, _, phi, _, _)) =
2.71 consider_formula_syms phi
2.72 fun consider_problem_syms problem =
2.73 fold (fold consider_problem_line_syms o snd) problem
2.74 @@ -714,9 +718,9 @@
2.75 in aux #> close_formula_universally end
2.76
2.77 fun repair_problem_line thy type_sys sym_tab
2.78 - (Formula (ident, kind, phi, source, useful_info)) =
2.79 - Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source,
2.80 - useful_info)
2.81 + (Formula (logic, ident, kind, phi, source, useful_info)) =
2.82 + Formula (logic, ident, kind, repair_formula thy type_sys sym_tab phi,
2.83 + source, useful_info)
2.84 | repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula"
2.85 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
2.86
2.87 @@ -771,7 +775,7 @@
2.88 val bound_tms =
2.89 map (fn (name, ty) => CombConst (name, the ty, [])) bounds
2.90 in
2.91 - Formula (type_decl_prefix ^ ascii_of s, Axiom,
2.92 + Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom,
2.93 mk_aquant AForall bounds
2.94 (has_type_combatom res_ty
2.95 (fold (curry (CombApp o swap)) bound_tms
2.96 @@ -815,7 +819,7 @@
2.97 val sym_tab = sym_table_for_problem explicit_apply problem
2.98 val problem = problem |> repair_problem thy type_sys sym_tab
2.99 val helper_facts =
2.100 - problem |> maps (map_filter (fn Formula (_, _, phi, _, _) => SOME phi
2.101 + problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
2.102 | _ => NONE) o snd)
2.103 |> get_helper_facts ctxt type_sys
2.104 val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
2.105 @@ -848,7 +852,7 @@
2.106 fun add_term_weights weight (ATerm (s, tms)) =
2.107 (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
2.108 #> fold (add_term_weights weight) tms
2.109 -fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
2.110 +fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
2.111 fold_formula (add_term_weights weight) phi
2.112 | add_problem_line_weights _ _ = I
2.113