# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 9e3e4563645937e51d81c972413e7471d3fa55ab # Parent 25ceb855a18bb6a7b55310fd0a508077e535980c generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas) diff -r 25ceb855a18b -r 9e3e45636459 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r 25ceb855a18b -r 9e3e45636459 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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