# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 7a506b0b644f667cb5a36015116a1848518b4e55 # Parent 3df98f0de5a034b963fed00c2e6b808ad205ccbb distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree diff -r 3df98f0de5a0 -r 7a506b0b644f 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 @@ -16,9 +16,11 @@ AAtom of 'b type 'a uniform_formula = ('a, 'a fo_term) formula - datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture - datatype 'a problem_line = - Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option + datatype logic = Fof | Tff + datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture + type 'a problem_line = + logic * string * formula_kind * ('a, 'a fo_term) formula + * string fo_term option type 'a problem = (string * 'a problem_line list) list val timestamp : unit -> string @@ -45,9 +47,11 @@ AAtom of 'b type 'a uniform_formula = ('a, 'a fo_term) formula -datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture -datatype 'a problem_line = - Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option +datatype logic = Fof | Tff +datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture +type 'a problem_line = + logic * string * formula_kind * ('a, 'a fo_term) formula + * 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 @@ -88,7 +92,7 @@ | string_for_formula (AAtom tm) = string_for_term tm fun string_for_problem_line use_conjecture_for_hypotheses - (Fof (ident, kind, phi, source)) = + (logic, ident, kind, phi, source) = let val (kind, phi) = if kind = Hypothesis andalso use_conjecture_for_hypotheses then @@ -96,7 +100,8 @@ else (kind, phi) in - "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ + (case logic of Fof => "fof" | Tff => "tff") ^ + "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^ string_for_formula phi ^ ")" ^ (case source of SOME tm => ", " ^ string_for_term tm @@ -179,8 +184,8 @@ | nice_formula (AConn (c, phis)) = pool_map nice_formula phis #>> curry AConn c | nice_formula (AAtom tm) = nice_term tm #>> AAtom -fun nice_problem_line (Fof (ident, kind, phi, source)) = - nice_formula phi #>> (fn phi => Fof (ident, kind, phi, source)) +fun nice_problem_line (logic, ident, kind, phi, source) = + nice_formula phi #>> (fn phi => (logic, ident, kind, phi, source)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem diff -r 3df98f0de5a0 -r 7a506b0b644f src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200 @@ -276,10 +276,11 @@ val vampire_unknown_fact = "unknown" -(* Syntax: (fof|cnf)\(, , \). +(* Syntax: (cnf|fof|tff)\(, , \). The could be an identifier, but we assume integers. *) val parse_tstp_line = - ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(") + ((Scan.this_string "cnf" || Scan.this_string "fof" || Scan.this_string "tff") + -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ "," -- parse_formula -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), deps) => diff -r 3df98f0de5a0 -r 7a506b0b644f 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 @@ -54,7 +54,7 @@ type translated_formula = {name: string, - kind: kind, + kind: formula_kind, combformula: (name, combterm) formula, ctypes_sorts: typ list} @@ -311,9 +311,9 @@ fun var s = ATerm (`I s, []) fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) in - [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom, - AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) - |> close_formula_universally, NONE)] + [(Fof, helper_prefix ^ ascii_of "ti_ti", Axiom, + AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) + |> close_formula_universally, NONE)] end else []) @@ -498,20 +498,23 @@ (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, ...}) = - Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, - formula_for_fact ctxt type_sys formula, NONE) + (logic_for_type_sys type_sys, prefix ^ string_of_int j ^ "_" ^ ascii_of name, + kind, formula_for_fact ctxt type_sys formula, NONE) fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in - Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, - AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))]), NONE) + (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom, + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))]), NONE) end fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = @@ -521,26 +524,25 @@ fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, ...}) = - 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 - (fo_literal_for_arity_literal conclLit)), NONE) + (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 + (fo_literal_for_arity_literal conclLit)), NONE) fun problem_line_for_conjecture ctxt type_sys ({name, kind, combformula, ...} : translated_formula) = - Fof (conjecture_prefix ^ name, kind, - formula_for_combformula ctxt type_sys - (close_combformula_universally combformula), - NONE) + (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind, + formula_for_combformula ctxt type_sys + (close_combformula_universally combformula), NONE) fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) = ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture |> map fo_literal_for_type_literal fun problem_line_for_free_type j lit = - Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit, - NONE) + (Fof, tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit, + NONE) fun problem_lines_for_free_types type_sys facts = let val litss = map (free_type_literals type_sys) facts @@ -568,7 +570,7 @@ | consider_formula (AConn (_, phis)) = fold consider_formula phis | consider_formula (AAtom tm) = consider_term true tm -fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi +fun consider_problem_line (_, _, _, 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 *) @@ -659,12 +661,10 @@ |> repair_predicates_in_term pred_sym_tab) in aux #> close_formula_universally end -fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) = - Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source) +fun repair_problem_line thy type_sys sym_tab (logic, ident, kind, phi, source) = + (logic, ident, kind, repair_formula thy type_sys sym_tab phi, source) fun repair_problem thy = map o apsnd o map oo repair_problem_line thy -fun dest_Fof (Fof z) = z - val factsN = "Relevant facts" val class_relsN = "Class relationships" val aritiesN = "Arity declarations" @@ -696,7 +696,7 @@ val sym_tab = sym_table_for_problem explicit_apply problem val problem = problem |> repair_problem thy type_sys sym_tab val helper_facts = - get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem) + get_helper_facts ctxt type_sys (maps (map #4 o snd) problem) val helper_lines = helper_facts |>> map (pair 0 @@ -722,7 +722,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 (Fof (_, _, phi, _)) = +fun add_problem_line_weights weight (_, _, _, phi, _) = fold_formula (add_term_weights weight) phi fun add_conjectures_weights [] = I