# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 747736d8b47e26010366b88899beceefc1c79f6b # Parent a15f0db2bcaf3a76a0bd60248420359d9fe9c54c added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS diff -r a15f0db2bcaf -r 747736d8b47e 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 @@ -20,7 +20,7 @@ datatype 'a problem_line = Type_Decl of string * 'a * 'a list * 'a | Formula of string * formula_kind * ('a, 'a fo_term) formula - * string fo_term option + * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list val timestamp : unit -> string @@ -51,7 +51,7 @@ datatype 'a problem_line = Type_Decl of string * 'a * 'a list * 'a | Formula of string * formula_kind * ('a, 'a fo_term) formula - * string fo_term option + * string fo_term option * string fo_term option type 'a problem = (string * 'a problem_line list) list val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now @@ -109,7 +109,7 @@ "tff(" ^ ident ^ ", type, " ^ sym ^ " : " ^ string_for_symbol_type arg_tys res_ty ^ ").\n" | string_for_problem_line use_conjecture_for_hypotheses - (Formula (ident, kind, phi, source)) = + (Formula (ident, kind, phi, source, useful_info)) = let val (kind, phi) = if kind = Hypothesis andalso use_conjecture_for_hypotheses then @@ -120,9 +120,12 @@ (if formula_needs_typed_logic phi then "tff" else "fof") ^ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ string_for_formula phi ^ ")" ^ - (case source of - SOME tm => ", " ^ string_for_term tm - | NONE => "") ^ ").\n" + (case (source, useful_info) of + (NONE, NONE) => "" + | (SOME tm, NONE) => ", " ^ string_for_term tm + | (_, SOME tm) => + ", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^ + ", " ^ string_for_term tm) ^ ").\n" end fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ @@ -209,8 +212,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)) = - nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source)) + | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) = + nice_formula phi + #>> (fn phi => Formula (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 a15f0db2bcaf -r 747736d8b47e 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 @@ -318,7 +318,7 @@ [Formula (helper_prefix ^ ascii_of "ti_ti", Axiom, AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) - |> close_formula_universally, NONE)] + |> close_formula_universally, NONE, NONE)] end else []) @@ -509,14 +509,15 @@ 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) + 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, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))]), NONE) + AAtom (ATerm (superclass, [ty_arg]))]), + NONE, NONE) end fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = @@ -530,14 +531,14 @@ mk_ahorn (map (formula_for_fo_literal o apfst not o fo_literal_for_arity_literal) premLits) (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit)), NONE) + (fo_literal_for_arity_literal conclLit)), NONE, NONE) fun problem_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, formula_for_combformula ctxt type_sys (close_combformula_universally combformula), - NONE) + NONE, NONE) fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture @@ -545,7 +546,7 @@ fun problem_line_for_free_type j lit = Formula (tfree_prefix ^ string_of_int j, Hypothesis, - formula_for_fo_literal lit, NONE) + formula_for_fo_literal lit, NONE, NONE) fun problem_lines_for_free_types type_sys facts = let val litss = map (free_type_literals type_sys) facts @@ -574,7 +575,7 @@ | consider_formula (AAtom tm) = consider_term true tm fun consider_problem_line (Type_Decl _) = I - | consider_problem_line (Formula (_, _, phi, _)) = consider_formula phi + | consider_problem_line (Formula (_, _, phi, _, _)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem (* needed for helper facts if the problem otherwise does not involve equality *) @@ -667,8 +668,9 @@ in aux #> close_formula_universally end fun repair_problem_line thy type_sys sym_tab - (Formula (ident, kind, phi, source)) = - Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source) + (Formula (ident, kind, phi, source, useful_info)) = + Formula (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 @@ -703,7 +705,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 helper_lines = @@ -731,7 +733,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