# HG changeset patch # User blanchet # Date 1319886958 -7200 # Node ID bd03b08161ac6ef14784ec776b10592c53a5502f # Parent 04c87dec70b87a589c864103faf1a0c897c7de7c added DFG unsorted support (like in the old days) diff -r 04c87dec70b8 -r bd03b08161ac src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Oct 29 13:15:58 2011 +0200 @@ -25,6 +25,7 @@ datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice + datatype dfg_flavor = DFG_Unsorted | DFG_Sorted datatype atp_format = CNF | @@ -32,7 +33,7 @@ FOF | TFF of tptp_polymorphism * tptp_explicitness | THF of tptp_polymorphism * tptp_explicitness * thf_flavor | - DFG_Sorted + DFG of dfg_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -99,7 +100,7 @@ bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula -> 'd -> 'd val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula - val is_format_thf : atp_format -> bool + val is_format_higher_order : atp_format -> bool val is_format_typed : atp_format -> bool val lines_for_atp_problem : atp_format -> string problem -> string list val ensure_cnf_problem : @@ -140,6 +141,7 @@ datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_flavor = THF_Without_Choice | THF_With_Choice +datatype dfg_flavor = DFG_Unsorted | DFG_Sorted datatype atp_format = CNF | @@ -147,7 +149,7 @@ FOF | TFF of tptp_polymorphism * tptp_explicitness | THF of tptp_polymorphism * tptp_explicitness * thf_flavor | - DFG_Sorted + DFG of dfg_flavor datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -158,8 +160,9 @@ val isabelle_info_prefix = "isabelle_" -(* Currently, only SPASS supports Isabelle metainformation. *) -fun isabelle_info DFG_Sorted s = +(* Currently, only newer versions of SPASS, with sorted DFG format support, can + process Isabelle metainformation. *) +fun isabelle_info (DFG DFG_Sorted) s = SOME (ATerm ("[]", [ATerm (isabelle_info_prefix ^ s, [])])) | isabelle_info _ _ = NONE @@ -251,11 +254,11 @@ | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) -fun is_format_thf (THF _) = true - | is_format_thf _ = false +fun is_format_higher_order (THF _) = true + | is_format_higher_order _ = false fun is_format_typed (TFF _) = true | is_format_typed (THF _) = true - | is_format_typed (DFG_Sorted) = true + | is_format_typed (DFG DFG_Sorted) = true | is_format_typed _ = false fun tptp_string_for_kind Axiom = "axiom" @@ -265,7 +268,7 @@ | tptp_string_for_kind Conjecture = "conjecture" fun tptp_string_for_app format func args = - if is_format_thf format then + if is_format_higher_order format then "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" else func ^ "(" ^ commas args ^ ")" @@ -283,7 +286,7 @@ fun str_for_type format ty = let - val dfg = (format = DFG_Sorted) + val dfg = (format = DFG DFG_Sorted) fun str _ (AType (s, [])) = if dfg andalso s = tptp_individual_type then "Top" else s | str _ (AType (s, tys)) = @@ -337,7 +340,7 @@ else if is_tptp_equal s then space_implode (" " ^ tptp_equal ^ " ") (map (tptp_string_for_term format) ts) - |> is_format_thf format ? enclose "(" ")" + |> is_format_higher_order format ? enclose "(" ")" else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice andalso is_format_with_choice format, ts) of (true, _, [AAbs ((s', ty), tm)]) => @@ -367,11 +370,11 @@ (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") (map (tptp_string_for_term format) ts) - |> is_format_thf format ? enclose "(" ")" + |> is_format_higher_order format ? enclose "(" ")" | tptp_string_for_formula format (AConn (c, [phi])) = tptp_string_for_connective c ^ " " ^ (tptp_string_for_formula format phi - |> is_format_thf format ? enclose "(" ")") + |> is_format_higher_order format ? enclose "(" ")") |> enclose "(" ")" | tptp_string_for_formula format (AConn (c, phis)) = space_implode (" " ^ tptp_string_for_connective c ^ " ") @@ -389,7 +392,7 @@ | tptp_string_for_format FOF = tptp_fof | tptp_string_for_format (TFF _) = tptp_tff | tptp_string_for_format (THF _) = tptp_thf - | tptp_string_for_format DFG_Sorted = raise Fail "non-TPTP format" + | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format" fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) = tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ @@ -427,7 +430,7 @@ | is_predicate_type (AType (s, _)) = (s = tptp_bool_type) | is_predicate_type _ = false -fun dfg_string_for_formula info = +fun dfg_string_for_formula flavor info = let fun str_for_term simp (ATerm (s, tms)) = (if is_tptp_equal s then "equal" |> simp ? suffix ":lr" @@ -446,7 +449,7 @@ | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr" fun str_for_formula simp (AQuant (q, xs, phi)) = str_for_quant q ^ "(" ^ "[" ^ - commas (map (string_for_bound_var DFG_Sorted) xs) ^ "], " ^ + commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^ str_for_formula simp phi ^ ")" | str_for_formula simp (AConn (c, phis)) = str_for_conn simp c ^ "(" ^ @@ -454,19 +457,20 @@ | str_for_formula simp (AAtom tm) = str_for_term simp tm in str_for_formula (is_isabelle_info simpN info) end -fun dfg_lines problem = +fun dfg_lines flavor problem = let + val format = DFG flavor fun ary sym ty = "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")" fun fun_typ sym ty = - "function(" ^ sym ^ ", " ^ string_for_type DFG_Sorted ty ^ ")." + "function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")." fun pred_typ sym ty = "predicate(" ^ - commas (sym :: map (string_for_type DFG_Sorted) (binder_atypes ty)) ^ ")." + commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")." fun formula pred (Formula (ident, kind, phi, _, info)) = if pred kind then - SOME ("formula(" ^ dfg_string_for_formula info phi ^ ", " ^ ident ^ - ").") + SOME ("formula(" ^ dfg_string_for_formula flavor info phi ^ ", " ^ + ident ^ ").") else NONE | formula _ _ = NONE @@ -515,7 +519,9 @@ fun lines_for_atp_problem format problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: - (if format = DFG_Sorted then dfg_lines else tptp_lines format) problem + (case format of + DFG flavor => dfg_lines flavor + | _ => tptp_lines format) problem (** CNF (Metis) and CNF UEQ (Waldmeister) **) diff -r 04c87dec70b8 -r bd03b08161ac src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Oct 29 13:15:58 2011 +0200 @@ -341,9 +341,9 @@ prem_kind = #prem_kind spass_config, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*, - (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))), - (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)] + [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*, + (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))), + (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} diff -r 04c87dec70b8 -r bd03b08161ac src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Oct 29 13:15:58 2011 +0200 @@ -640,7 +640,7 @@ | adjust_type_enc (THF _) type_enc = type_enc | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) = Simple_Types (First_Order, Mangled_Monomorphic, level) - | adjust_type_enc DFG_Sorted (Simple_Types (_, _, level)) = + | adjust_type_enc (DFG DFG_Sorted) (Simple_Types (_, _, level)) = Simple_Types (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) = Simple_Types (First_Order, poly, level) @@ -2365,6 +2365,7 @@ | FOF => I | TFF (_, TPTP_Implicit) => I | THF (_, TPTP_Implicit, _) => I + | DFG DFG_Unsorted => I | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names diff -r 04c87dec70b8 -r bd03b08161ac src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sat Oct 29 13:15:58 2011 +0200 @@ -160,7 +160,7 @@ end val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ) -val is_ho_atp = is_atp_for_format is_format_thf +val is_ho_atp = is_atp_for_format is_format_higher_order fun is_prover_supported ctxt name = let val thy = Proof_Context.theory_of ctxt in