# HG changeset patch # User blanchet # Date 1313568238 -7200 # Node ID 85e9dad3c187c3a0a26850cd0c35662904409abd # Parent 17ae4af434aadcd753fd779460f067b3f448926d distinguish THF syntax with and without choice (Satallax vs. LEO-II) diff -r 17ae4af434aa -r 85e9dad3c187 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 16 15:02:20 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 17 10:03:58 2011 +0200 @@ -19,7 +19,14 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type - datatype format = CNF | CNF_UEQ | FOF | TFF | THF + datatype thf_flavor = Without_Choice | With_Choice + datatype format = + CNF | + CNF_UEQ | + FOF | + TFF | + THF of thf_flavor + datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a ho_type | @@ -73,6 +80,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 : format -> bool val is_format_typed : format -> bool val tptp_lines_for_atp_problem : format -> string problem -> string list val ensure_cnf_problem : @@ -107,7 +115,14 @@ datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type -datatype format = CNF | CNF_UEQ | FOF | TFF | THF +datatype thf_flavor = Without_Choice | With_Choice +datatype format = + CNF | + CNF_UEQ | + FOF | + TFF | + THF of thf_flavor + datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = Decl of string * 'a * 'a ho_type | @@ -189,7 +204,11 @@ | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) -val is_format_typed = member (op =) [TFF, THF] +fun is_format_thf (THF _) = true + | is_format_thf _ = false +fun is_format_typed TFF = true + | is_format_typed (THF _) = true + | is_format_typed _ = false fun string_for_kind Axiom = "axiom" | string_for_kind Definition = "definition" @@ -202,7 +221,7 @@ raise Fail "unexpected higher-order type in first-order format" | strip_tff_type (AType s) = ([], s) -fun string_for_type THF ty = +fun string_for_type (THF _) ty = let fun aux _ (AType s) = s | aux rhs (AFun (ty1, ty2)) = @@ -228,7 +247,7 @@ | string_for_connective AIff = tptp_iff fun string_for_bound_var format (s, ty) = - s ^ (if format = TFF orelse format = THF then + s ^ (if is_format_typed format then " " ^ tptp_has_type ^ " " ^ string_for_type format (ty |> the_default (AType tptp_individual_type)) else @@ -241,7 +260,7 @@ "[" ^ commas (map (string_for_term format) ts) ^ "]" else if is_tptp_equal s then space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) - |> format = THF ? enclose "(" ")" + |> is_format_thf format ? enclose "(" ")" else (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of (true, [AAbs ((s', ty), tm)]) => @@ -252,14 +271,14 @@ [(s', SOME ty)], AAtom tm)) | _ => let val ss = map (string_for_term format) ts in - if format = THF then + if is_format_thf format then "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")" else s ^ "(" ^ commas ss ^ ")" end) - | string_for_term THF (AAbs ((s, ty), tm)) = - "(^[" ^ s ^ " : " ^ string_for_type THF ty ^ "] : " ^ - string_for_term THF tm ^ ")" + | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = + "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^ + string_for_term format tm ^ ")" | string_for_term _ _ = raise Fail "unexpected term in first-order format" and string_for_formula format (AQuant (q, xs, phi)) = string_for_quantifier q ^ @@ -270,10 +289,10 @@ (AConn (ANot, [AAtom (ATerm ("=" (* tptp_equal *), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") (map (string_for_term format) ts) - |> format = THF ? enclose "(" ")" + |> is_format_thf format ? enclose "(" ")" | string_for_formula format (AConn (c, [phi])) = string_for_connective c ^ " " ^ - (string_for_formula format phi |> format = THF ? enclose "(" ")") + (string_for_formula format phi |> is_format_thf format ? enclose "(" ")") |> enclose "(" ")" | string_for_formula format (AConn (c, phis)) = space_implode (" " ^ string_for_connective c ^ " ") @@ -290,7 +309,7 @@ | string_for_format CNF_UEQ = tptp_cnf | string_for_format FOF = tptp_fof | string_for_format TFF = tptp_tff - | string_for_format THF = tptp_thf + | string_for_format (THF _) = tptp_thf fun string_for_problem_line format (Decl (ident, sym, ty)) = string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ diff -r 17ae4af434aa -r 85e9dad3c187 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 16 15:02:20 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 17 10:03:58 2011 +0200 @@ -242,7 +242,7 @@ known_failures = [], conj_sym_kind = Axiom, prem_kind = Hypothesis, - formats = [THF, FOF], + formats = [THF Without_Choice, FOF], best_slices = fn ctxt => (* FUDGE *) [(0.667, (false, (150, "simple_higher", sosN))), @@ -265,7 +265,7 @@ known_failures = [(ProofMissing, "SZS status Theorem")], conj_sym_kind = Axiom, prem_kind = Hypothesis, - formats = [THF], + formats = [THF With_Choice], best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)} val satallax = (satallaxN, satallax_config) diff -r 17ae4af434aa -r 85e9dad3c187 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 16 15:02:20 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 17 10:03:58 2011 +0200 @@ -604,12 +604,14 @@ val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc fun choose_format formats (Simple_Types (order, level)) = - if member (op =) formats THF then - (THF, Simple_Types (order, level)) - else if member (op =) formats TFF then - (TFF, Simple_Types (First_Order, level)) - else - choose_format formats (Guards (Mangled_Monomorphic, level, Heavyweight)) + (case find_first is_format_thf formats of + SOME format => (format, Simple_Types (order, level)) + | NONE => + if member (op =) formats TFF then + (TFF, Simple_Types (First_Order, level)) + else + choose_format formats + (Guards (Mangled_Monomorphic, level, Heavyweight))) | choose_format formats type_enc = (case hd formats of CNF_UEQ => @@ -760,7 +762,7 @@ (true, @{type_name bool}) => `I tptp_bool_type | (true, @{type_name fun}) => `I tptp_fun_type | _ => if s = homo_infinite_type_name andalso - (format = TFF orelse format = THF) then + is_format_typed format then `I tptp_individual_type else `make_fixed_type_const s,