diff --git a/src/HOL/Tools/ATP/atp_problem.ML b/src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML +++ b/src/HOL/Tools/ATP/atp_problem.ML @@ -1,998 +1,998 @@ (* Title: HOL/Tools/ATP/atp_problem.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Abstract representation of ATP problems and TPTP syntax. *) signature ATP_PROBLEM = sig datatype ('a, 'b) atp_term = ATerm of ('a * 'b list) * ('a, 'b) atp_term list | AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list datatype atp_quantifier = AForall | AExists datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c, 'd) atp_formula = ATyQuant of atp_quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) atp_formula | AQuant of atp_quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) atp_formula | AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list | AAtom of 'c datatype 'a atp_type = AType of ('a * 'a list) * 'a atp_type list | AFun of 'a atp_type * 'a atp_type | APi of 'a list * 'a atp_type type term_order = {is_lpo : bool, gen_weights : bool, gen_prec : bool, gen_simp : bool} datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic - datatype thf_flavor = THF_Without_Choice | THF_With_Choice + datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | CNF_UEQ | FOF | TFF of fool * polymorphism | THF of fool * polymorphism * thf_flavor | DFG of polymorphism datatype atp_formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | Plain | Type_Role | Unknown datatype 'a atp_problem_line = Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a atp_type | Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool | Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | Formula of (string * string) * atp_formula_role * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula * (string, string atp_type) atp_term option * (string, string atp_type) atp_term list type 'a atp_problem = (string * 'a atp_problem_line list) list val tptp_cnf : string val tptp_fof : string val tptp_tff : string val tptp_thf : string val tptp_has_type : string val tptp_type_of_types : string val tptp_bool_type : string val tptp_individual_type : string val tptp_fun_type : string val tptp_product_type : string val tptp_forall : string val tptp_ho_forall : string val tptp_pi_binder : string val tptp_exists : string val tptp_ho_exists : string val tptp_choice : string val tptp_ho_choice : string val tptp_hilbert_choice : string val tptp_hilbert_the : string val tptp_not : string val tptp_and : string val tptp_not_and : string val tptp_or : string val tptp_not_or : string val tptp_implies : string val tptp_if : string val tptp_iff : string val tptp_not_iff : string val tptp_app : string val tptp_not_infix : string val tptp_equal : string val tptp_not_equal : string val tptp_old_equal : string val tptp_false : string val tptp_true : string val tptp_lambda : string val tptp_empty_list : string val dfg_individual_type : string val isabelle_info_prefix : string val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list val extract_isabelle_status : (string, 'a) atp_term list -> string option val extract_isabelle_rank : (string, 'a) atp_term list -> int val inductionN : string val introN : string val inductiveN : string val elimN : string val simpN : string val non_rec_defN : string val rec_defN : string val rankN : string val minimum_rank : int val default_rank : int val default_term_order_weight : int val is_tptp_equal : string -> bool val is_built_in_tptp_symbol : string -> bool val is_tptp_variable : string -> bool val is_tptp_user_symbol : string -> bool val bool_atype : (string * string) atp_type val individual_atype : (string * string) atp_type val mk_anot : ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula val mk_aconn : atp_connective -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'c, 'd) atp_formula val mk_app : (string, 'a) atp_term -> (string, 'a) atp_term -> (string, 'a) atp_term val mk_apps : (string, 'a) atp_term -> (string, 'a) atp_term list -> (string, 'a) atp_term val mk_simple_aterm: 'a -> ('a, 'b) atp_term val aconn_fold : bool option -> (bool option -> 'a -> 'b -> 'b) -> atp_connective * 'a list -> 'b -> 'b val aconn_map : bool option -> (bool option -> 'a -> ('b, 'c, 'd, 'e) atp_formula) -> atp_connective * 'a list -> ('b, 'c, 'd, 'e) atp_formula val formula_fold : bool option -> (bool option -> 'c -> 'e -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> 'e -> 'e val formula_map : ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type) val is_format_higher_order : atp_format -> bool val tptp_string_of_format : atp_format -> string val tptp_string_of_role : atp_formula_role -> string val tptp_string_of_line : atp_format -> string atp_problem_line -> string val lines_of_atp_problem : atp_format -> term_order -> (unit -> (string * int) list) -> string atp_problem -> string list val ensure_cnf_problem : (string * string) atp_problem -> (string * string) atp_problem val filter_cnf_ueq_problem : (string * string) atp_problem -> (string * string) atp_problem val declared_in_atp_problem : 'a atp_problem -> ('a list * 'a list) * 'a list val nice_atp_problem : bool -> atp_format -> ('a * (string * string) atp_problem_line list) list -> ('a * string atp_problem_line list) list * (string Symtab.table * string Symtab.table) option end; structure ATP_Problem : ATP_PROBLEM = struct open ATP_Util val parens = enclose "(" ")" (** ATP problem **) datatype ('a, 'b) atp_term = ATerm of ('a * 'b list) * ('a, 'b) atp_term list | AAbs of (('a * 'b) * ('a, 'b) atp_term) * ('a, 'b) atp_term list datatype atp_quantifier = AForall | AExists datatype atp_connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c, 'd) atp_formula = ATyQuant of atp_quantifier * ('b * 'd list) list * ('a, 'b, 'c, 'd) atp_formula | AQuant of atp_quantifier * ('a * 'b option) list * ('a, 'b, 'c, 'd) atp_formula | AConn of atp_connective * ('a, 'b, 'c, 'd) atp_formula list | AAtom of 'c datatype 'a atp_type = AType of ('a * 'a list) * 'a atp_type list | AFun of 'a atp_type * 'a atp_type | APi of 'a list * 'a atp_type type term_order = {is_lpo : bool, gen_weights : bool, gen_prec : bool, gen_simp : bool} datatype fool = Without_FOOL | With_FOOL datatype polymorphism = Monomorphic | Polymorphic -datatype thf_flavor = THF_Without_Choice | THF_With_Choice +datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice datatype atp_format = CNF | CNF_UEQ | FOF | TFF of fool * polymorphism | THF of fool * polymorphism * thf_flavor | DFG of polymorphism datatype atp_formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | Plain | Type_Role | Unknown datatype 'a atp_problem_line = Class_Decl of string * 'a * 'a list | Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a atp_type | Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool | Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a | Formula of (string * string) * atp_formula_role * ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula * (string, string atp_type) atp_term option * (string, string atp_type) atp_term list type 'a atp_problem = (string * 'a atp_problem_line list) list (* official TPTP syntax *) val tptp_cnf = "cnf" val tptp_fof = "fof" val tptp_tff = "tff" val tptp_thf = "thf" val tptp_has_type = ":" val tptp_type_of_types = "$tType" val tptp_bool_type = "$o" val tptp_individual_type = "$i" val tptp_fun_type = ">" val tptp_product_type = "*" val tptp_forall = "!" val tptp_ho_forall = "!!" val tptp_pi_binder = "!>" val tptp_exists = "?" val tptp_ho_exists = "??" val tptp_choice = "@+" val tptp_ho_choice = "@@+" val tptp_not = "~" val tptp_and = "&" val tptp_not_and = "~&" val tptp_or = "|" val tptp_not_or = "~|" val tptp_implies = "=>" val tptp_if = "<=" val tptp_iff = "<=>" val tptp_not_iff = "<~>" val tptp_app = "@" val tptp_hilbert_choice = "@+" val tptp_hilbert_the = "@-" val tptp_not_infix = "!" val tptp_equal = "=" val tptp_not_equal = "!=" val tptp_old_equal = "equal" val tptp_false = "$false" val tptp_true = "$true" val tptp_lambda = "^" val tptp_empty_list = "[]" val dfg_individual_type = "iii" (* cannot clash *) val isabelle_info_prefix = "isabelle_" val inductionN = "induction" val introN = "intro" val inductiveN = "inductive" val elimN = "elim" val simpN = "simp" val non_rec_defN = "non_rec_def" val rec_defN = "rec_def" val rankN = "rank" val minimum_rank = 0 val default_rank = 1000 val default_term_order_weight = 1 (* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle metainformation. *) fun isabelle_info generate_info status rank = if generate_info then [] |> rank <> default_rank ? cons (ATerm ((isabelle_info_prefix ^ rankN, []), [ATerm ((string_of_int rank, []), [])])) |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), [])) else [] fun extract_isabelle_status (ATerm ((s, []), []) :: _) = try (unprefix isabelle_info_prefix) s | extract_isabelle_status _ = NONE fun extract_isabelle_rank (tms as _ :: _) = (case List.last tms of ATerm ((_, []), [ATerm ((rank, []), [])]) => the (Int.fromString rank) | _ => default_rank) | extract_isabelle_rank _ = default_rank fun is_tptp_equal s = (s = tptp_equal orelse s = tptp_old_equal) fun is_built_in_tptp_symbol s = s = tptp_old_equal orelse not (Char.isAlpha (String.sub (s, 0))) fun is_tptp_variable s = s <> "" andalso Char.isUpper (String.sub (s, 0)) val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol) val bool_atype = AType ((`I tptp_bool_type, []), []) val individual_atype = AType ((`I tptp_individual_type, []), []) fun raw_polarities_of_conn ANot = (SOME false, NONE) | raw_polarities_of_conn AAnd = (SOME true, SOME true) | raw_polarities_of_conn AOr = (SOME true, SOME true) | raw_polarities_of_conn AImplies = (SOME false, SOME true) | raw_polarities_of_conn AIff = (NONE, NONE) fun polarities_of_conn NONE = K (NONE, NONE) | polarities_of_conn (SOME pos) = raw_polarities_of_conn #> not pos ? apply2 (Option.map not) fun mk_anot (AConn (ANot, [phi])) = phi | mk_anot phi = AConn (ANot, [phi]) fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) fun mk_app t u = ATerm ((tptp_app, []), [t, u]) fun mk_apps f xs = fold (fn x => fn f => mk_app f x) xs f fun mk_simple_aterm p = ATerm ((p, []), []) fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi | aconn_fold pos f (AImplies, [phi1, phi2]) = f (Option.map not pos) phi1 #> f pos phi2 | aconn_fold pos f (AAnd, phis) = fold (f pos) phis | aconn_fold pos f (AOr, phis) = fold (f pos) phis | aconn_fold _ f (_, phis) = fold (f NONE) phis fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi]) | aconn_map pos f (AImplies, [phi1, phi2]) = AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2]) | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis) | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis) | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis) fun formula_fold pos f = let fun fld pos (AQuant (_, _, phi)) = fld pos phi | fld pos (ATyQuant (_, _, phi)) = fld pos phi | fld pos (AConn conn) = aconn_fold pos fld conn | fld pos (AAtom tm) = f pos tm in fld pos end fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi) | formula_map f (ATyQuant (q, xs, phi)) = ATyQuant (q, xs, formula_map f phi) | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis) | formula_map f (AAtom tm) = AAtom (f tm) fun strip_api (APi (tys, ty)) = strip_api ty |>> append tys | strip_api ty = ([], ty) fun strip_afun (AFun (ty1, ty2)) = strip_afun ty2 |>> cons ty1 | strip_afun ty = ([], ty) fun strip_atype ty = ty |> strip_api ||> strip_afun fun is_function_atype ty = snd (snd (strip_atype ty)) <> AType ((tptp_bool_type, []), []) fun is_predicate_atype ty = not (is_function_atype ty) fun is_nontrivial_predicate_atype (AType _) = false | is_nontrivial_predicate_atype ty = is_predicate_atype ty 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 _) = true | is_format_typed _ = false fun is_format_with_fool (THF (With_FOOL, _, _)) = true | is_format_with_fool (TFF (With_FOOL, _)) = true | is_format_with_fool _ = false fun tptp_string_of_role Axiom = "axiom" | tptp_string_of_role Definition = "definition" | tptp_string_of_role Lemma = "lemma" | tptp_string_of_role Hypothesis = "hypothesis" | tptp_string_of_role Conjecture = "conjecture" | tptp_string_of_role Negated_Conjecture = "negated_conjecture" | tptp_string_of_role Plain = "plain" | tptp_string_of_role Type_Role = "type" | tptp_string_of_role Unknown = "unknown" fun tptp_string_of_app _ func [] = func | tptp_string_of_app format func args = if is_format_higher_order format then "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" else func ^ "(" ^ commas args ^ ")" fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty) | uncurry_type (ty as AFun (ty1 as AType _, ty2)) = (case uncurry_type ty2 of AFun (ty' as AType ((s, _), tys), ty) => AFun (AType ((tptp_product_type, []), ty1 :: (if s = tptp_product_type then tys else [ty'])), ty) | _ => ty) | uncurry_type (ty as AType _) = ty | uncurry_type _ = raise Fail "unexpected higher-order type in first-order format" val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types) fun str_of_type format ty = let val dfg = (case format of DFG _ => true | _ => false) fun str _ (AType ((s, _), [])) = if dfg andalso s = tptp_individual_type then dfg_individual_type else s | str rhs (AType ((s, _), tys)) = if s = tptp_fun_type then let val [ty1, ty2] = tys in str rhs (AFun (ty1, ty2)) end else let val ss = tys |> map (str false) in if s = tptp_product_type then ss |> space_implode (if dfg then ", " else " " ^ tptp_product_type ^ " ") |> (not dfg andalso length ss > 1) ? parens else tptp_string_of_app format s ss end | str rhs (AFun (ty1, ty2)) = (str false ty1 |> dfg ? parens) ^ " " ^ (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2 |> not rhs ? parens | str _ (APi (ss, ty)) = if dfg then "[" ^ commas ss ^ "], " ^ str true ty else tptp_pi_binder ^ "[" ^ commas (map suffix_type_of_types ss) ^ "]: " ^ str false ty in str true ty end fun string_of_type (format as THF _) ty = str_of_type format ty | string_of_type format ty = str_of_type format (uncurry_type ty) fun tptp_string_of_quantifier AForall = tptp_forall | tptp_string_of_quantifier AExists = tptp_exists fun tptp_string_of_connective ANot = tptp_not | tptp_string_of_connective AAnd = tptp_and | tptp_string_of_connective AOr = tptp_or | tptp_string_of_connective AImplies = tptp_implies | tptp_string_of_connective AIff = tptp_iff fun string_of_bound_var format (s, ty) = s ^ (if is_format_typed format then " " ^ tptp_has_type ^ " " ^ (ty |> the_default (AType ((tptp_individual_type, []), [])) |> string_of_type format) else "") fun tptp_string_of_term _ (ATerm ((s, []), [])) = s | tptp_string_of_term format (ATerm ((s, tys), ts)) = let val of_type = string_of_type format val of_term = tptp_string_of_term format fun app () = tptp_string_of_app format s (map (of_type #> is_format_higher_order format ? parens) tys @ map of_term ts) in if s = tptp_empty_list then (* used for lists in the optional "source" field of a derivation *) "[" ^ commas (map of_term ts) ^ "]" else if is_tptp_equal s then space_implode (" " ^ tptp_equal ^ " ") (map of_term ts) |> (is_format_higher_order format orelse is_format_with_fool format) ? parens else if s = tptp_ho_forall orelse s = tptp_ho_exists then (case ts of [AAbs (((s', ty), tm), [])] => (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work around LEO-II 1.2.8 parser limitation. *) tptp_string_of_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) | _ => app ()) else if s = tptp_choice then (case ts of [AAbs (((s', ty), tm), args)] => (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an abstraction. *) tptp_string_of_app format (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^ "]: " ^ of_term tm ^ "" |> parens) (map of_term args) | _ => app ()) else if s = tptp_not then (* agsyHOL doesn't like negations applied like this: "~ @ t". *) (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens | _ => s) else if member (op =) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal] s then (* agsyHOL doesn't like connectives applied like this: "& @ t1 @ t2". *) (case ts of [t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens | _ => app ()) else app () end | tptp_string_of_term (format as THF _) (AAbs (((s, ty), tm), args)) = tptp_string_of_app format ("(^[" ^ s ^ " : " ^ string_of_type format ty ^ "]: " ^ tptp_string_of_term format tm ^ ")") (map (tptp_string_of_term format) args) | tptp_string_of_term _ _ = raise Fail "unexpected term in first-order format" and tptp_string_of_formula format (ATyQuant (q, xs, phi)) = tptp_string_of_quantifier q ^ "[" ^ commas (map (suffix_type_of_types o string_of_type format o fst) xs) ^ "]: " ^ tptp_string_of_formula format phi |> parens | tptp_string_of_formula format (AQuant (q, xs, phi)) = tptp_string_of_quantifier q ^ "[" ^ commas (map (string_of_bound_var format) xs) ^ "]: " ^ tptp_string_of_formula format phi |> parens | tptp_string_of_formula format (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") (map (tptp_string_of_term format) ts) |> is_format_higher_order format ? parens | tptp_string_of_formula format (AConn (c, [phi])) = tptp_string_of_connective c ^ " " ^ (tptp_string_of_formula format phi |> is_format_higher_order format ? parens) |> parens | tptp_string_of_formula format (AConn (c, phis)) = space_implode (" " ^ tptp_string_of_connective c ^ " ") (map (tptp_string_of_formula format) phis) |> parens | tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm fun tptp_string_of_format CNF = tptp_cnf | tptp_string_of_format CNF_UEQ = tptp_cnf | tptp_string_of_format FOF = tptp_fof | tptp_string_of_format (TFF _) = tptp_tff | tptp_string_of_format (THF _) = tptp_thf | tptp_string_of_format (DFG _) = raise Fail "non-TPTP format" val atype_of_types = AType ((tptp_type_of_types, []), []) fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types fun maybe_alt "" = "" | maybe_alt s = " % " ^ s fun tptp_string_of_line format (Type_Decl (ident, ty, ary)) = tptp_string_of_line format (Sym_Decl (ident, ty, nary_type_decl_type ary)) | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) = tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ string_of_type format ty ^ ").\n" | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) = tptp_string_of_format format ^ "(" ^ ident ^ ", " ^ tptp_string_of_role kind ^ "," ^ "\n (" ^ tptp_string_of_formula format phi ^ ")" ^ (case source of SOME tm => ", " ^ tptp_string_of_term format tm | NONE => if null info then "" else ", []") ^ (case info of [] => "" | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^ ")." ^ maybe_alt alt ^ "\n" fun tptp_lines format = maps (fn (_, []) => [] | (heading, lines) => "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: map (tptp_string_of_line format) lines) fun arity_of_type (APi (tys, ty)) = arity_of_type ty |>> Integer.add (length tys) | arity_of_type (AFun (_, ty)) = arity_of_type ty ||> Integer.add 1 | arity_of_type _ = (0, 0) fun string_of_arity (0, n) = string_of_int n | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n val dfg_class_inter = space_implode " & " fun dfg_string_of_term (ATerm ((s, tys), tms)) = s ^ (if null tys then "" else "<" ^ commas (map (string_of_type (DFG Polymorphic)) tys) ^ ">") ^ (if null tms then "" else "(" ^ commas (map dfg_string_of_term tms) ^ ")") | dfg_string_of_term _ = raise Fail "unexpected atom in first-order format" fun dfg_string_of_formula poly gen_simp info = let val str_of_typ = string_of_type (DFG poly) fun str_of_bound_typ (ty, []) = str_of_typ ty | str_of_bound_typ (ty, cls) = str_of_typ ty ^ " : " ^ dfg_class_inter cls fun suffix_tag top_level s = if top_level then (case extract_isabelle_status info of SOME s' => if s' = non_rec_defN then s ^ ":lt" else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then s ^ ":lr" else s | NONE => s) else s fun str_of_atom top_level (ATerm ((s, tys), tms)) = let val s' = if is_tptp_equal s then "equal" |> suffix_tag top_level else if s = tptp_true then "true" else if s = tptp_false then "false" else s in dfg_string_of_term (ATerm ((s', tys), tms)) end | str_of_atom _ _ = raise Fail "unexpected atom in first-order format" fun str_of_quant AForall = "forall" | str_of_quant AExists = "exists" fun str_of_conn _ ANot = "not" | str_of_conn _ AAnd = "and" | str_of_conn _ AOr = "or" | str_of_conn _ AImplies = "implies" | str_of_conn top_level AIff = "equiv" |> suffix_tag top_level fun str_of_formula top_level (ATyQuant (q, xs, phi)) = str_of_quant q ^ "_sorts([" ^ commas (map str_of_bound_typ xs) ^ "], " ^ str_of_formula top_level phi ^ ")" | str_of_formula top_level (AQuant (q, xs, phi)) = str_of_quant q ^ "([" ^ commas (map (string_of_bound_var (DFG poly)) xs) ^ "], " ^ str_of_formula top_level phi ^ ")" | str_of_formula top_level (AConn (c, phis)) = str_of_conn top_level c ^ "(" ^ commas (map (str_of_formula false) phis) ^ ")" | str_of_formula top_level (AAtom tm) = str_of_atom top_level tm in str_of_formula true end fun maybe_enclose bef aft "" = "% " ^ bef ^ aft | maybe_enclose bef aft s = bef ^ s ^ aft fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = let val typ = string_of_type (DFG poly) val term = dfg_string_of_term fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")" fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty)) fun ty_ary 0 ty = ty | ty_ary n ty = "(" ^ ty ^ ", " ^ string_of_int n ^ ")" fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ typ ty ^ ")." fun pred_typ sym ty = let val (ty_vars, (tys, _)) = strip_atype ty |>> (fn [] => [] | xs => ["[" ^ commas xs ^ "]"]) in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end fun bound_tvar (ty, []) = ty | bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls fun binder_typ xs ty = (if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^ typ ty fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")." fun datatype_decl xs ty tms exhaust = "datatype(" ^ commas (binder_typ xs ty :: map term tms @ (if exhaust then [] else ["..."])) ^ ")." fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ ", " ^ ident ^ (if rank = default_rank then "" else ", " ^ string_of_int rank) ^ ")." ^ maybe_alt alt |> SOME end else NONE | formula _ _ = NONE fun filt f = problem |> map (map_filter f o snd) |> filter_out null val func_aries = filt (fn Sym_Decl (_, sym, ty) => if is_function_atype ty then SOME (tm_ary sym ty) else NONE | _ => NONE) |> flat |> commas |> maybe_enclose "functions [" "]." val pred_aries = filt (fn Sym_Decl (_, sym, ty) => if is_predicate_atype ty then SOME (tm_ary sym ty) else NONE | _ => NONE) |> flat |> commas |> maybe_enclose "predicates [" "]." val sorts = filt (try (fn Type_Decl (_, ty, ary) => ty_ary ary ty)) @ [[ty_ary 0 dfg_individual_type]] |> flat |> commas |> maybe_enclose "sorts [" "]." val classes = filt (try (fn Class_Decl (_, cl, _) => cl)) |> flat |> commas |> maybe_enclose "classes [" "]." val ord_info = if gen_weights orelse gen_prec then ord_info () else [] val do_term_order_weights = (if gen_weights then ord_info else []) |> map (spair o apsnd string_of_int) |> commas |> maybe_enclose "weights [" "]." val syms = [func_aries, pred_aries, do_term_order_weights, sorts, classes] val func_decls = filt (fn Sym_Decl (_, sym, ty) => if is_function_atype ty then SOME (fun_typ sym ty) else NONE | _ => NONE) |> flat val pred_decls = filt (fn Sym_Decl (_, sym, ty) => if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty) else NONE | _ => NONE) |> flat val datatype_decls = filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) => datatype_decl xs ty tms exhaust)) |> flat val sort_decls = filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat val subclass_decls = filt (try (fn Class_Decl (_, sub, supers) => map (subclass_of sub) supers)) |> flat |> flat val decls = func_decls @ pred_decls @ datatype_decls @ sort_decls @ subclass_decls val axioms = filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat val conjs = filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat val settings = (if is_lpo then ["set_flag(Ordering, 1)."] else []) @ (if gen_prec then [ord_info |> map fst |> rev |> commas |> maybe_enclose "set_precedence(" ")."] else []) fun list_of _ [] = [] | list_of heading ss = "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @ ["end_of_list.\n\n"] in "\nbegin_problem(isabelle).\n\n" :: list_of "descriptions" ["name({**}).", "author({**}).", "status(unknown).", "description({**})."] @ list_of "symbols" syms @ list_of "declarations" decls @ list_of "formulae(axioms)" axioms @ list_of "formulae(conjectures)" conjs @ list_of "settings(SPASS)" settings @ ["end_problem.\n"] end fun lines_of_atp_problem format ord ord_info problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: (case format of DFG poly => dfg_lines poly ord ord_info | _ => tptp_lines format) problem (** CNF (Metis) and CNF UEQ (Waldmeister) **) fun is_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true | is_line_negated _ = false fun is_line_cnf_ueq (Formula (_, _, AAtom (ATerm (((s, _), _), _)), _, _)) = is_tptp_equal s | is_line_cnf_ueq _ = false fun open_conjecture_term (ATerm (((s, s'), tys), tms)) = ATerm ((if is_tptp_variable s then (s |> Name.desymbolize (SOME false), s') else (s, s'), tys), tms |> map open_conjecture_term) | open_conjecture_term _ = raise Fail "unexpected higher-order term" fun open_formula conj = let (* We are conveniently assuming that all bound variable names are distinct, which should be the case for the formulas we generate. *) fun opn (pos as SOME true) (AQuant (AForall, _, phi)) = opn pos phi | opn (pos as SOME false) (AQuant (AExists, _, phi)) = opn pos phi | opn pos (AConn (ANot, [phi])) = mk_anot (opn (Option.map not pos) phi) | opn pos (AConn (c, [phi1, phi2])) = let val (pos1, pos2) = polarities_of_conn pos c in AConn (c, [opn pos1 phi1, opn pos2 phi2]) end | opn _ (AAtom t) = AAtom (t |> conj ? open_conjecture_term) | opn _ phi = phi in opn (SOME (not conj)) end fun open_formula_line (Formula (ident, kind, phi, source, info)) = Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info) | open_formula_line line = line fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) = Formula (ident, Hypothesis, mk_anot phi, source, info) | negate_conjecture_line line = line exception CLAUSIFY of unit (* This "clausification" only expands syntactic sugar, such as "phi => psi" to "~ phi | psi" and "phi <=> psi" to "~ phi | psi" and "~ psi | phi". We don't attempt to distribute conjunctions over disjunctions. *) fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot] | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi | clausify_formula true (AConn (AOr, [phi1, phi2])) = (phi1, phi2) |> apply2 (clausify_formula true) |> uncurry (map_product (mk_aconn AOr)) | clausify_formula false (AConn (AAnd, [phi1, phi2])) = (phi1, phi2) |> apply2 (clausify_formula false) |> uncurry (map_product (mk_aconn AOr)) | clausify_formula true (AConn (AImplies, [phi1, phi2])) = clausify_formula true (AConn (AOr, [mk_anot phi1, phi2])) | clausify_formula true (AConn (AIff, phis)) = clausify_formula true (AConn (AImplies, phis)) @ clausify_formula true (AConn (AImplies, rev phis)) | clausify_formula _ _ = raise CLAUSIFY () fun clausify_formula_line (Formula ((ident, alt), kind, phi, source, info)) = let val (n, phis) = phi |> try (clausify_formula true) |> these |> `length in map2 (fn phi => fn j => Formula ((ident ^ replicate_string (j - 1) "x", alt), kind, phi, source, info)) phis (1 upto n) end | clausify_formula_line _ = [] fun ensure_cnf_line line = line |> open_formula_line |> negate_conjecture_line |> clausify_formula_line fun ensure_cnf_problem problem = problem |> map (apsnd (maps ensure_cnf_line)) fun filter_cnf_ueq_problem problem = problem |> map (apsnd (map open_formula_line #> filter is_line_cnf_ueq #> map negate_conjecture_line)) |> (fn problem => let val lines = problem |> maps snd val conjs = lines |> filter is_line_negated in if length conjs = 1 andalso conjs <> lines then problem else [] end) (** Symbol declarations **) fun add_declared_in_line (Class_Decl (_, cl, _)) = apfst (apfst (cons cl)) | add_declared_in_line (Type_Decl (_, ty, _)) = apfst (apsnd (cons ty)) | add_declared_in_line (Sym_Decl (_, sym, _)) = apsnd (cons sym) | add_declared_in_line _ = I fun declared_in_atp_problem problem = fold (fold add_declared_in_line o snd) problem (([], []), []) (** Nice names **) val no_qualifiers = let fun skip [] = [] | skip (#"." :: cs) = skip cs | skip (c :: cs) = if Char.isAlphaNum c then skip cs else c :: keep cs and keep [] = [] | keep (#"." :: cs) = skip cs | keep (c :: cs) = c :: keep cs in String.explode #> rev #> keep #> rev #> String.implode end (* Long names can slow down the ATPs. *) val max_readable_name_size = 20 (* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the problem files. "eq" is reserved to ensure that "HOL.eq" is correctly mapped to equality (not clear whether this is still necessary). *) val reserved_nice_names = [tptp_old_equal, "op", "eq"] (* hack to get the same hashing across Mirabelle runs (see "mirabelle.pl") *) fun cleanup_mirabelle_name s = let val mirabelle_infix = "_Mirabelle_" val random_suffix_len = 10 val (s1, s2) = Substring.position mirabelle_infix (Substring.full s) in if Substring.isEmpty s2 then s else Substring.string s1 ^ Substring.string (Substring.triml (size mirabelle_infix + random_suffix_len) s2) end fun readable_name protect full_name s = (if s = full_name then s else s |> no_qualifiers |> unquote_tvar |> Name.desymbolize (SOME (Char.isUpper (String.sub (full_name, 0)))) |> (fn s => if size s > max_readable_name_size then String.substring (s, 0, max_readable_name_size div 2 - 4) ^ string_of_int (hash_string (cleanup_mirabelle_name full_name)) ^ String.extract (s, size s - max_readable_name_size div 2 + 4, NONE) else s) |> (fn s => if member (op =) reserved_nice_names s then full_name else s)) |> protect fun nice_name _ (full_name, _) NONE = (full_name, NONE) | nice_name protect (full_name, desired_name) (SOME the_pool) = if is_built_in_tptp_symbol full_name then (full_name, SOME the_pool) else (case Symtab.lookup (fst the_pool) full_name of SOME nice_name => (nice_name, SOME the_pool) | NONE => let val nice_prefix = readable_name protect full_name desired_name fun add j = let val nice_name = nice_prefix ^ (if j = 1 then "" else string_of_int j) in (case Symtab.lookup (snd the_pool) nice_name of SOME full_name' => if full_name = full_name' then (nice_name, the_pool) else add (j + 1) | NONE => (nice_name, (Symtab.update_new (full_name, nice_name) (fst the_pool), Symtab.update_new (nice_name, full_name) (snd the_pool)))) end in add 1 |> apsnd SOME end) fun avoid_clash_with_dfg_keywords s = let val n = String.size s in if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse String.isSubstring "_" s then s else if is_tptp_variable s then s ^ "_" else String.substring (s, 0, n - 1) ^ String.str (Char.toUpper (String.sub (s, n - 1))) end fun nice_atp_problem readable_names format problem = let val empty_pool = if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE val avoid_clash = (case format of DFG _ => avoid_clash_with_dfg_keywords | _ => I) val nice_name = nice_name avoid_clash fun nice_bound_tvars xs = fold_map (nice_name o fst) xs ##>> fold_map (fold_map nice_name o snd) xs #>> op ~~ fun nice_type (AType ((name, clss), tys)) = nice_name name ##>> fold_map nice_name clss ##>> fold_map nice_type tys #>> AType | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun | nice_type (APi (names, ty)) = fold_map nice_name names ##>> nice_type ty #>> APi fun nice_term (ATerm ((name, tys), ts)) = nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts #>> ATerm | nice_term (AAbs (((name, ty), tm), args)) = nice_name name ##>> nice_type ty ##>> nice_term tm ##>> fold_map nice_term args #>> AAbs fun nice_formula (ATyQuant (q, xs, phi)) = fold_map (nice_type o fst) xs ##>> fold_map (fold_map nice_name o snd) xs ##>> nice_formula phi #>> (fn ((tys, cls), phi) => ATyQuant (q, tys ~~ cls, phi)) | nice_formula (AQuant (q, xs, phi)) = fold_map (nice_name o fst) xs ##>> fold_map (fn (_, NONE) => pair NONE | (_, SOME ty) => nice_type ty #>> SOME) xs ##>> nice_formula phi #>> (fn ((ss, ts), phi) => AQuant (q, ss ~~ ts, phi)) | nice_formula (AConn (c, phis)) = fold_map nice_formula phis #>> curry AConn c | nice_formula (AAtom tm) = nice_term tm #>> AAtom fun nice_line (Class_Decl (ident, cl, cls)) = nice_name cl ##>> fold_map nice_name cls #>> (fn (cl, cls) => Class_Decl (ident, cl, cls)) | nice_line (Type_Decl (ident, ty, ary)) = nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary)) | nice_line (Sym_Decl (ident, sym, ty)) = nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty)) | nice_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) = nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust)) | nice_line (Class_Memb (ident, xs, ty, cl)) = nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl)) | nice_line (Formula (ident, kind, phi, source, info)) = nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info)) fun nice_problem problem = fold_map (fn (heading, lines) => fold_map nice_line lines #>> pair heading) problem in nice_problem problem empty_pool end end; diff --git a/src/HOL/Tools/ATP/atp_problem_generate.ML b/src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML @@ -1,2835 +1,2848 @@ (* Title: HOL/Tools/ATP/atp_problem_generate.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Translation of HOL to FOL for Metis and Sledgehammer. *) signature ATP_PROBLEM_GENERATE = sig type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type atp_connective = ATP_Problem.atp_connective type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type 'a atp_problem = 'a ATP_Problem.atp_problem datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def type stature = scope * status datatype strictness = Strict | Non_Strict datatype uniformity = Uniform | Non_Uniform datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim datatype type_level = All_Types | Undercover_Types | Nonmono_Types of strictness * uniformity | Const_Types of ctr_optim | No_Types type type_enc val no_lamsN : string val hide_lamsN : string val liftingN : string val combsN : string val combs_and_liftingN : string val combs_or_liftingN : string val lam_liftingN : string val keep_lamsN : string val schematic_var_prefix : string val fixed_var_prefix : string val tvar_prefix : string val tfree_prefix : string val const_prefix : string val type_const_prefix : string val class_prefix : string val lam_lifted_prefix : string val lam_lifted_mono_prefix : string val lam_lifted_poly_prefix : string val skolem_const_prefix : string val old_skolem_const_prefix : string val new_skolem_const_prefix : string val combinator_prefix : string val class_decl_prefix : string val type_decl_prefix : string val sym_decl_prefix : string val datatype_decl_prefix : string val class_memb_prefix : string val guards_sym_formula_prefix : string val tags_sym_formula_prefix : string val fact_prefix : string val conjecture_prefix : string val helper_prefix : string val subclass_prefix : string val tcon_clause_prefix : string val tfree_clause_prefix : string val lam_fact_prefix : string val typed_helper_suffix : string val untyped_helper_suffix : string val predicator_name : string val app_op_name : string val type_guard_name : string val type_tag_name : string val native_type_prefix : string val prefixed_predicator_name : string val prefixed_app_op_name : string val prefixed_type_tag_name : string val ascii_of : string -> string val unascii_of : string -> string val unprefix_and_unascii : string -> string -> string option val proxy_table : (string * (string * (thm * (string * string)))) list val proxify_const : string -> (string * string) option val invert_const : string -> string val unproxify_const : string -> string val new_skolem_var_name_of_const : string -> string val atp_logical_consts : string list val atp_irrelevant_consts : string list val atp_widely_irrelevant_consts : string list val is_irrelevant_const : string -> bool val is_widely_irrelevant_const : string -> bool val atp_schematic_consts_of : term -> typ list Symtab.table val is_type_enc_higher_order : type_enc -> bool val is_type_enc_polymorphic : type_enc -> bool val level_of_type_enc : type_enc -> type_level val is_type_enc_sound : type_enc -> bool val type_enc_of_string : strictness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc val is_lambda_free : term -> bool val do_cheaply_conceal_lambdas : typ list -> term -> term val mk_aconns : atp_connective -> ('a, 'b, 'c, 'd) atp_formula list -> ('a, 'b, 'c, 'd) atp_formula val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term val unmangled_const : string -> string * (string, 'b) atp_term list val unmangled_const_name : string -> string list val helper_table : ((string * bool) * (status * thm) list) list val trans_lams_of_string : Proof.context -> type_enc -> string -> term list -> term list * term list val string_of_status : status -> string val factsN : string val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc -> mode -> string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list -> string atp_problem * string Symtab.table * (string * term) list * int Symtab.table val atp_problem_selection_weights : string atp_problem -> (string * real) list val atp_problem_term_order_info : string atp_problem -> (string * int) list end; structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = struct open ATP_Util open ATP_Problem datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator datatype scope = Global | Local | Assum | Chained datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def type stature = scope * status datatype order = First_Order | Higher_Order of thf_flavor datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars datatype polymorphism = Type_Class_Polymorphic | Raw_Polymorphic of phantom_policy | Raw_Monomorphic | Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype uniformity = Uniform | Non_Uniform datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim datatype type_level = All_Types | Undercover_Types | Nonmono_Types of strictness * uniformity | Const_Types of ctr_optim | No_Types datatype type_enc = Native of order * fool * polymorphism * type_level | Guards of polymorphism * type_level | Tags of polymorphism * type_level (* not clear whether ATPs prefer to have their negative variables tagged *) val tag_neg_vars = false fun is_type_enc_native (Native _) = true | is_type_enc_native _ = false +fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Bool_Free, _, _, _)) = false + | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true + | is_type_enc_full_higher_order _ = false fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true | is_type_enc_fool _ = false fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true | is_type_enc_higher_order _ = false fun polymorphism_of_type_enc (Native (_, _, poly, _)) = poly | polymorphism_of_type_enc (Guards (poly, _)) = poly | polymorphism_of_type_enc (Tags (poly, _)) = poly fun is_type_enc_polymorphic type_enc = (case polymorphism_of_type_enc type_enc of Raw_Polymorphic _ => true | Type_Class_Polymorphic => true | _ => false) fun is_type_enc_mangling type_enc = polymorphism_of_type_enc type_enc = Mangled_Monomorphic fun level_of_type_enc (Native (_, _, _, level)) = level | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false | is_type_level_uniform Undercover_Types = false | is_type_level_uniform _ = true fun is_type_level_sound (Const_Types _) = false | is_type_level_sound No_Types = false | is_type_level_sound _ = true val is_type_enc_sound = is_type_level_sound o level_of_type_enc fun is_type_level_monotonicity_based (Nonmono_Types _) = true | is_type_level_monotonicity_based _ = false val no_lamsN = "no_lams" (* used internally; undocumented *) val hide_lamsN = "hide_lams" val liftingN = "lifting" val combsN = "combs" val combs_and_liftingN = "combs_and_lifting" val combs_or_liftingN = "combs_or_lifting" val keep_lamsN = "keep_lams" val lam_liftingN = "lam_lifting" (* legacy FIXME: remove *) val bound_var_prefix = "B_" val all_bound_var_prefix = "A_" val exist_bound_var_prefix = "E_" val schematic_var_prefix = "V_" val fixed_var_prefix = "v_" val tvar_prefix = "T_" val tfree_prefix = "tf_" val const_prefix = "c_" val type_const_prefix = "t_" val native_type_prefix = "n_" val class_prefix = "cl_" (* Freshness almost guaranteed! *) val atp_prefix = "ATP" ^ Long_Name.separator val atp_weak_prefix = "ATP:" val atp_weak_suffix = ":ATP" val lam_lifted_prefix = atp_weak_prefix ^ "Lam" val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m" val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p" val skolem_const_prefix = atp_prefix ^ "Sko" val old_skolem_const_prefix = skolem_const_prefix ^ "o" val new_skolem_const_prefix = skolem_const_prefix ^ "n" val combinator_prefix = "COMB" val class_decl_prefix = "cl_" val type_decl_prefix = "ty_" val sym_decl_prefix = "sy_" val datatype_decl_prefix = "dt_" val class_memb_prefix = "cm_" val guards_sym_formula_prefix = "gsy_" val tags_sym_formula_prefix = "tsy_" val uncurried_alias_eq_prefix = "unc_" val fact_prefix = "fact_" val conjecture_prefix = "conj_" val helper_prefix = "help_" val subclass_prefix = "subcl_" val tcon_clause_prefix = "tcon_" val tfree_clause_prefix = "tfree_" val lam_fact_prefix = "ATP.lambda_" val typed_helper_suffix = "_T" val untyped_helper_suffix = "_U" val predicator_name = "pp" val app_op_name = "aa" val type_guard_name = "gg" val type_tag_name = "tt" val prefixed_predicator_name = const_prefix ^ predicator_name val prefixed_app_op_name = const_prefix ^ app_op_name val prefixed_type_tag_name = const_prefix ^ type_tag_name (*Escaping of special characters. Alphanumeric characters are left unchanged. The character _ goes to __. Characters in the range ASCII space to / go to _A to _P, respectively. Other characters go to _nnn where nnn is the decimal ASCII code. *) val upper_a_minus_space = Char.ord #"A" - Char.ord #" " fun ascii_of_char c = if Char.isAlphaNum c then String.str c else if c = #"_" then "__" else if #" " <= c andalso c <= #"/" then "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space)) else (* fixed width, in case more digits follow *) "_" ^ stringN_of_int 3 (Char.ord c) val ascii_of = String.translate ascii_of_char (** Remove ASCII armoring from names in proof files **) (* We don't raise error exceptions because this code can run inside a worker thread. Also, the errors are impossible. *) val unascii_of = let fun un rcs [] = String.implode (rev rcs) | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *) (* Three types of _ escapes: __, _A to _P, _nnn *) | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs | un rcs (#"_" :: c :: cs) = if #"A" <= c andalso c<= #"P" then (* translation of #" " to #"/" *) un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs else let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in (case Int.fromString (String.implode digits) of SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2)) | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)) end | un rcs (c :: cs) = un (c :: rcs) cs in un [] o String.explode end (* If string s has the prefix s1, return the result of deleting it, un-ASCII'd. *) fun unprefix_and_unascii s1 s = if String.isPrefix s1 s then SOME (unascii_of (String.extract (s, size s1, NONE))) else NONE val proxy_table = [("c_False", (\<^const_name>\False\, (@{thm fFalse_def}, ("fFalse", \<^const_name>\fFalse\)))), ("c_True", (\<^const_name>\True\, (@{thm fTrue_def}, ("fTrue", \<^const_name>\fTrue\)))), ("c_Not", (\<^const_name>\Not\, (@{thm fNot_def}, ("fNot", \<^const_name>\fNot\)))), ("c_conj", (\<^const_name>\conj\, (@{thm fconj_def}, ("fconj", \<^const_name>\fconj\)))), ("c_disj", (\<^const_name>\disj\, (@{thm fdisj_def}, ("fdisj", \<^const_name>\fdisj\)))), ("c_implies", (\<^const_name>\implies\, (@{thm fimplies_def}, ("fimplies", \<^const_name>\fimplies\)))), ("equal", (\<^const_name>\HOL.eq\, (@{thm fequal_def}, ("fequal", \<^const_name>\fequal\)))), ("c_All", (\<^const_name>\All\, (@{thm fAll_def}, ("fAll", \<^const_name>\fAll\)))), ("c_Ex", (\<^const_name>\Ex\, (@{thm fEx_def}, ("fEx", \<^const_name>\fEx\))))] val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd) (* Readable names for the more common symbolic functions. Do not mess with the table unless you know what you are doing. *) val const_trans_table = [(\<^const_name>\False\, "False"), (\<^const_name>\True\, "True"), (\<^const_name>\Not\, "Not"), (\<^const_name>\conj\, "conj"), (\<^const_name>\disj\, "disj"), (\<^const_name>\implies\, "implies"), (\<^const_name>\HOL.eq\, "equal"), (\<^const_name>\All\, "All"), (\<^const_name>\Ex\, "Ex"), (\<^const_name>\If\, "If"), (\<^const_name>\Set.member\, "member"), (\<^const_name>\Meson.COMBI\, combinator_prefix ^ "I"), (\<^const_name>\Meson.COMBK\, combinator_prefix ^ "K"), (\<^const_name>\Meson.COMBB\, combinator_prefix ^ "B"), (\<^const_name>\Meson.COMBC\, combinator_prefix ^ "C"), (\<^const_name>\Meson.COMBS\, combinator_prefix ^ "S")] |> Symtab.make |> fold (Symtab.update o swap o snd o snd o snd) proxy_table (* Invert the table of translations between Isabelle and ATPs. *) val const_trans_table_inv = const_trans_table |> Symtab.dest |> map swap |> Symtab.make val const_trans_table_unprox = Symtab.empty |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table val invert_const = perhaps (Symtab.lookup const_trans_table_inv) val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox) fun lookup_const c = (case Symtab.lookup const_trans_table c of SOME c' => c' | NONE => ascii_of c) fun ascii_of_indexname (v, 0) = ascii_of v | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i fun make_bound_var x = bound_var_prefix ^ ascii_of x fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v fun make_fixed_var x = fixed_var_prefix ^ ascii_of x fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unquote_tvar s, i) fun make_tfree s = tfree_prefix ^ ascii_of (unquote_tvar s) fun tvar_name ((x as (s, _)), _) = (make_tvar x, s) (* "HOL.eq" and choice are mapped to the ATP's equivalents *) local val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT fun default c = const_prefix ^ lookup_const c in fun make_fixed_const _ \<^const_name>\HOL.eq\ = tptp_old_equal | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c = if c = choice_const then tptp_choice else default c | make_fixed_const _ c = default c end fun make_fixed_type_const c = type_const_prefix ^ lookup_const c fun make_class clas = class_prefix ^ ascii_of clas fun new_skolem_var_name_of_const s = let val ss = Long_Name.explode s in nth ss (length ss - 2) end (* These are ignored anyway by the relevance filter (unless they appear in higher-order places) but not by the monomorphizer. *) val atp_logical_consts = [\<^const_name>\Pure.prop\, \<^const_name>\Pure.conjunction\, \<^const_name>\Pure.all\, \<^const_name>\Pure.imp\, \<^const_name>\Pure.eq\, \<^const_name>\Trueprop\, \<^const_name>\All\, \<^const_name>\Ex\, \<^const_name>\Ex1\, \<^const_name>\Ball\, \<^const_name>\Bex\] (* These are either simplified away by "Meson.presimplify" (most of the time) or handled specially via "fFalse", "fTrue", ..., "fequal". *) val atp_irrelevant_consts = [\<^const_name>\False\, \<^const_name>\True\, \<^const_name>\Not\, \<^const_name>\conj\, \<^const_name>\disj\, \<^const_name>\implies\, \<^const_name>\HOL.eq\, \<^const_name>\If\, \<^const_name>\Let\] val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts val atp_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_irrelevant_consts) val atp_widely_irrelevant_const_tab = Symtab.make (map (rpair ()) atp_widely_irrelevant_consts) val is_irrelevant_const = Symtab.defined atp_irrelevant_const_tab val is_widely_irrelevant_const = Symtab.defined atp_widely_irrelevant_const_tab fun add_schematic_const (x as (_, T)) = Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x val add_schematic_consts_of = Term.fold_aterms (fn Const (x as (s, _)) => not (member (op =) atp_widely_irrelevant_consts s) ? add_schematic_const x | _ => I) fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty val tvar_a_str = "'a" val tvar_a_z = ((tvar_a_str, 0), \<^sort>\type\) val tvar_a = TVar tvar_a_z val tvar_a_name = tvar_name tvar_a_z val itself_name = `make_fixed_type_const \<^type_name>\itself\ val TYPE_name = `(make_fixed_const NONE) \<^const_name>\Pure.type\ val tvar_a_atype = AType ((tvar_a_name, []), []) val a_itself_atype = AType ((itself_name, []), [tvar_a_atype]) (** Definitions and functions for FOL clauses and formulas for TPTP **) (** Type class membership **) (* In our data structures, [] exceptionally refers to the top class, not to the empty class. *) val class_of_types = the_single \<^sort>\type\ fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls (* Arity of type constructor "s :: (arg1, ..., argN) res" *) fun make_axiom_tcon_clause (s, name, (cl, args)) = let val args = args |> map normalize_classes val tvars = 1 upto length args |> map (fn j => TVar ((tvar_a_str, j), \<^sort>\type\)) in (name, args ~~ tvars, (cl, Type (s, tvars))) end (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in theory thy provided its arguments have the corresponding sorts. *) fun class_pairs thy tycons cls = let val alg = Sign.classes_of thy fun domain_sorts tycon = Sorts.mg_domain alg tycon o single fun add_class tycon cl = cons (cl, domain_sorts tycon cl) handle Sorts.CLASS_ERROR _ => I fun try_classes tycon = (tycon, fold (add_class tycon) cls []) in map try_classes tycons end (* Proving one (tycon, class) membership may require proving others, so iterate. *) fun all_class_pairs _ _ _ [] = ([], []) | all_class_pairs thy tycons old_cls cls = let val old_cls' = cls @ old_cls fun maybe_insert_class s = not (member (op =) old_cls' s) ? insert (op =) s val pairs = class_pairs thy tycons cls val new_cls = fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs [] val (cls', pairs') = all_class_pairs thy tycons old_cls' new_cls in (cls' @ cls, union (op =) pairs' pairs) end fun tcon_clause _ _ [] = [] | tcon_clause seen n ((_, []) :: rest) = tcon_clause seen n rest | tcon_clause seen n ((tcons, (ar as (cl, _)) :: ars) :: rest) = if cl = class_of_types then tcon_clause seen n ((tcons, ars) :: rest) else if member (op =) seen cl then (* multiple clauses for the same (tycon, cl) pair *) make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, ar) :: tcon_clause seen (n + 1) ((tcons, ars) :: rest) else make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, ar) :: tcon_clause (cl :: seen) n ((tcons, ars) :: rest) fun make_tcon_clauses thy tycons = all_class_pairs thy tycons [] ##> tcon_clause [] 1 (** Isabelle class relations **) (* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all "supers". *) fun make_subclass_pairs thy subs supers = let val class_less = curry (Sorts.class_less (Sign.classes_of thy)) fun supers_of sub = (sub, filter (class_less sub) supers) in map supers_of subs |> filter_out (null o snd) end (* intermediate terms *) datatype iterm = IConst of (string * string) * typ * typ list | IVar of (string * string) * typ | IApp of iterm * iterm | IAbs of ((string * string) * typ) * iterm fun ityp_of (IConst (_, T, _)) = T | ityp_of (IVar (_, T)) = T | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1)) | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm (*gets the head of a combinator application, along with the list of arguments*) fun strip_iterm_comb u = let fun stripc (IApp (t, u), ts) = stripc (t, u :: ts) | stripc x = x in stripc (u, []) end fun atomic_types_of T = fold_atyps (insert (op =)) T [] fun new_skolem_const_name s num_T_args = [new_skolem_const_prefix, s, string_of_int num_T_args] |> Long_Name.implode val alpha_to_beta = Logic.varifyT_global \<^typ>\'a => 'b\ val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta fun robust_const_type thy s = if s = app_op_name then alpha_to_beta_to_alpha_to_beta else if String.isPrefix lam_lifted_prefix s then alpha_to_beta else (* Old Skolems throw a "TYPE" exception here, which will be caught. *) s |> Sign.the_const_type thy fun ary_of (Type (\<^type_name>\fun\, [_, T])) = 1 + ary_of T | ary_of _ = 0 (* This function only makes sense if "T" is as general as possible. *) fun robust_const_type_args thy (s, T) = if s = app_op_name then let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end else if String.isPrefix old_skolem_const_prefix s then [] |> Term.add_tvarsT T |> rev |> map TVar else if String.isPrefix lam_lifted_prefix s then if String.isPrefix lam_lifted_poly_prefix s then let val (T1, T2) = T |> dest_funT in [T1, T2] end else [] else (s, T) |> Sign.const_typargs thy (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort infomation. *) fun iterm_of_term thy type_enc bs (P $ Q) = let val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end | iterm_of_term thy type_enc _ (Const (c, T)) = (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)), atomic_types_of T) | iterm_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T) | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let val Ts = T |> strip_type |> swap |> op :: val s' = new_skolem_const_name s (length Ts) in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end else IVar ((make_schematic_var v, s), T), atomic_types_of T) | iterm_of_term _ _ bs (Bound j) = nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T)) | iterm_of_term thy type_enc bs (Abs (s, T, t)) = let fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string val s = vary s val name = `make_bound_var s val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *) val queries = ["?", "_query"] val ats = ["@", "_at"] fun try_unsuffixes ss s = fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE fun type_enc_of_string strictness s = let val (poly, s) = (case try (unprefix "tc_") s of SOME s => (SOME Type_Class_Polymorphic, s) | NONE => (case try (unprefix "poly_") s of SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s) | NONE => (case try (unprefix "ml_poly_") s of SOME s => (SOME (Raw_Polymorphic Without_Phantom_Type_Vars), s) | NONE => (case try (unprefix "raw_mono_") s of SOME s => (SOME Raw_Monomorphic, s) | NONE => (case try (unprefix "mono_") s of SOME s => (SOME Mangled_Monomorphic, s) | NONE => (NONE, s)))))) val (level, s) = case try_unsuffixes queries s of SOME s => (case try_unsuffixes queries s of SOME s => (Nonmono_Types (strictness, Non_Uniform), s) | NONE => (Nonmono_Types (strictness, Uniform), s)) | NONE => (case try_unsuffixes ats s of SOME s => (Undercover_Types, s) | NONE => (All_Types, s)) fun native_of_string s = let val (fool, core) = (case try (unsuffix "_fool") s of SOME s => (With_FOOL, s) | NONE => (Without_FOOL, s)) in (case (core, poly) of ("native", SOME poly) => (case (poly, level) of (Mangled_Monomorphic, _) => if is_type_level_uniform level then Native (First_Order, fool, Mangled_Monomorphic, level) else raise Same.SAME | (Raw_Monomorphic, _) => raise Same.SAME | (poly, All_Types) => Native (First_Order, fool, poly, All_Types)) | ("native_higher", SOME poly) => (case (poly, level) of (_, Nonmono_Types _) => raise Same.SAME | (_, Undercover_Types) => raise Same.SAME | (Mangled_Monomorphic, _) => if is_type_level_uniform level then Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level) else raise Same.SAME | (poly as Raw_Polymorphic _, All_Types) => Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types) | _ => raise Same.SAME)) end fun nonnative_of_string core = (case (core, poly, level) of ("guards", SOME poly, _) => if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse poly = Type_Class_Polymorphic then raise Same.SAME else Guards (poly, level) | ("tags", SOME poly, _) => if (poly = Mangled_Monomorphic andalso level = Undercover_Types) orelse poly = Type_Class_Polymorphic then raise Same.SAME else Tags (poly, level) | ("args", SOME poly, All_Types (* naja *)) => if poly = Type_Class_Polymorphic then raise Same.SAME else Guards (poly, Const_Types Without_Ctr_Optim) | ("args", SOME poly, Nonmono_Types (_, Uniform) (* naja *)) => if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then raise Same.SAME else Guards (poly, Const_Types With_Ctr_Optim) | ("erased", NONE, All_Types (* naja *)) => Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) | _ => raise Same.SAME) in if String.isPrefix "native" s then native_of_string s else nonnative_of_string s end handle Same.SAME => error ("Unknown type encoding: " ^ quote s) -fun min_hologic THF_Without_Choice _ = THF_Without_Choice +fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free + | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free + | min_hologic THF_Without_Choice _ = THF_Without_Choice | min_hologic _ THF_Without_Choice = THF_Without_Choice | min_hologic _ _ = THF_With_Choice fun adjust_hologic hologic (Higher_Order hologic') = Higher_Order (min_hologic hologic hologic') | adjust_hologic _ type_enc = type_enc fun adjust_fool Without_FOOL _ = Without_FOOL | adjust_fool _ fool = fool fun no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars | no_type_classes poly = poly fun adjust_type_enc (THF (fool, Polymorphic, hologic)) (Native (order, fool', poly, level)) = Native (adjust_hologic hologic order, adjust_fool fool fool', no_type_classes poly, level) | adjust_type_enc (THF (fool, Monomorphic, hologic)) (Native (order, fool', _, level)) = Native (adjust_hologic hologic order, adjust_fool fool fool', Mangled_Monomorphic, level) | adjust_type_enc (TFF (fool, Monomorphic)) (Native (_, fool', _, level)) = Native (First_Order, adjust_fool fool fool', Mangled_Monomorphic, level) | adjust_type_enc (DFG Polymorphic) (Native (_, _, poly, level)) = Native (First_Order, Without_FOOL, poly, level) | adjust_type_enc (DFG Monomorphic) (Native (_, _, _, level)) = Native (First_Order, Without_FOOL, Mangled_Monomorphic, level) | adjust_type_enc (TFF (fool, _)) (Native (_, fool', poly, level)) = Native (First_Order, adjust_fool fool fool', no_type_classes poly, level) | adjust_type_enc format (Native (_, _, poly, level)) = adjust_type_enc format (Guards (no_type_classes poly, level)) | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) = (if is_type_enc_sound type_enc then Tags else Guards) stuff | adjust_type_enc _ type_enc = type_enc fun is_lambda_free t = (case t of \<^const>\Not\ $ t1 => is_lambda_free t1 | Const (\<^const_name>\All\, _) $ Abs (_, _, t') => is_lambda_free t' | Const (\<^const_name>\All\, _) $ t1 => is_lambda_free t1 | Const (\<^const_name>\Ex\, _) $ Abs (_, _, t') => is_lambda_free t' | Const (\<^const_name>\Ex\, _) $ t1 => is_lambda_free t1 | \<^const>\HOL.conj\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 | \<^const>\HOL.disj\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 | \<^const>\HOL.implies\ $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 | Const (\<^const_name>\HOL.eq\, Type (_, [\<^typ>\bool\, _])) $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)) fun simple_translate_lambdas do_lambdas ctxt t = if is_lambda_free t then t else let fun trans Ts t = (case t of \<^const>\Not\ $ t1 => \<^const>\Not\ $ trans Ts t1 | (t0 as Const (\<^const_name>\All\, _)) $ Abs (s, T, t') => t0 $ Abs (s, T, trans (T :: Ts) t') | (t0 as Const (\<^const_name>\All\, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1) | (t0 as Const (\<^const_name>\Ex\, _)) $ Abs (s, T, t') => t0 $ Abs (s, T, trans (T :: Ts) t') | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1) | (t0 as \<^const>\HOL.conj\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 | (t0 as \<^const>\HOL.disj\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 | (t0 as \<^const>\HOL.implies\) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 | (t0 as Const (\<^const_name>\HOL.eq\, Type (_, [\<^typ>\bool\, _]))) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then t else t |> Envir.eta_contract |> do_lambdas ctxt Ts) val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end fun do_cheaply_conceal_lambdas Ts (t1 $ t2) = do_cheaply_conceal_lambdas Ts t1 $ do_cheaply_conceal_lambdas Ts t2 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) = Const (lam_lifted_poly_prefix ^ serial_string (), T --> fastype_of1 (T :: Ts, t)) | do_cheaply_conceal_lambdas _ t = t fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j fun conceal_bounds Ts t = subst_bounds (map (Free o apfst concealed_bound_name) (0 upto length Ts - 1 ~~ Ts), t) fun reveal_bounds Ts = subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) (0 upto length Ts - 1 ~~ Ts)) fun do_introduce_combinators ctxt Ts t = (t |> conceal_bounds Ts |> Thm.cterm_of ctxt |> Meson_Clausify.introduce_combinators_in_cterm ctxt |> Thm.prop_of |> Logic.dest_equals |> snd |> reveal_bounds Ts) (* A type variable of sort "{}" will make abstraction fail. *) handle THM _ => t |> do_cheaply_conceal_lambdas Ts val introduce_combinators = simple_translate_lambdas do_introduce_combinators fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) | constify_lifted (Free (x as (s, _))) = (if String.isPrefix lam_lifted_prefix s then Const else Free) x | constify_lifted t = t fun lift_lams_part_1 ctxt type_enc = map hol_close_form #> rpair ctxt #-> Lambda_Lifting.lift_lambdas (SOME ((if is_type_enc_polymorphic type_enc then lam_lifted_poly_prefix else lam_lifted_mono_prefix) ^ "_a")) Lambda_Lifting.is_quantifier #> fst fun lift_lams_part_2 ctxt (facts, lifted) = (facts, lifted) (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid of them *) |> apply2 (map (introduce_combinators ctxt)) |> apply2 (map constify_lifted) (* Requires bound variables not to clash with any schematic variables (as should be the case right after lambda-lifting). *) |>> map (hol_open_form (unprefix hol_close_form_prefix)) ||> map (hol_open_form I) fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt fun intentionalize_def (Const (\<^const_name>\All\, _) $ Abs (_, _, t)) = intentionalize_def t | intentionalize_def (Const (\<^const_name>\HOL.eq\, _) $ t $ u) = let fun lam T t = Abs (Name.uu, T, t) val (head, args) = strip_comb t ||> rev val head_T = fastype_of head val n = length args val arg_Ts = head_T |> binder_types |> take n |> rev val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1)) in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end | intentionalize_def t = t type ifact = {name : string, stature : stature, role : atp_formula_role, iformula : (string * string, typ, iterm, string * string) atp_formula, atomic_types : typ list} fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) = {name = name, stature = stature, role = role, iformula = f iformula, atomic_types = atomic_types} : ifact fun ifact_lift f ({iformula, ...} : ifact) = f iformula fun insert_type thy get_T x xs = let val T = get_T x in if exists (type_instance thy T o get_T) xs then xs else x :: filter_out (type_generalization thy T o get_T) xs end fun chop_fun 0 T = ([], T) | chop_fun n (Type (\<^type_name>\fun\, [dom_T, ran_T])) = chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ T = ([], T) fun filter_type_args thy ctrss type_enc s ary T_args = let val poly = polymorphism_of_type_enc type_enc in if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *) T_args else (case type_enc of Native (_, _, Raw_Polymorphic _, _) => T_args | Native (_, _, Type_Class_Polymorphic, _) => T_args | _ => let fun gen_type_args _ _ [] = [] | gen_type_args keep strip_ty T_args = let val U = robust_const_type thy s val (binder_Us, body_U) = strip_ty U val in_U_vars = fold Term.add_tvarsT binder_Us [] val out_U_vars = Term.add_tvarsT body_U [] fun filt (U_var, T) = if keep (member (op =) in_U_vars U_var, member (op =) out_U_vars U_var) then T else dummyT val U_args = (s, U) |> robust_const_type_args thy in map (filt o apfst dest_TVar) (U_args ~~ T_args) end handle TYPE _ => T_args fun is_always_ctr (s', T') = s' = s andalso type_equiv thy (T', robust_const_type thy s') val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary) val ctr_infer_type_args = gen_type_args fst strip_type val level = level_of_type_enc type_enc in if level = No_Types orelse s = \<^const_name>\HOL.eq\ orelse (case level of Const_Types _ => s = app_op_name | _ => false) then [] else if poly = Mangled_Monomorphic then T_args else if level = All_Types then (case type_enc of Guards _ => noninfer_type_args T_args | Tags _ => []) else if level = Undercover_Types then noninfer_type_args T_args else if level <> Const_Types Without_Ctr_Optim andalso exists (exists is_always_ctr) ctrss then ctr_infer_type_args T_args else T_args end) end fun raw_atp_type_of_typ type_enc = let fun term (Type (s, Ts)) = AType ((if s = \<^type_name>\fun\ andalso is_type_enc_higher_order type_enc then `I tptp_fun_type else if s = \<^type_name>\bool\ andalso - (is_type_enc_higher_order type_enc orelse is_type_enc_fool type_enc) then + (is_type_enc_full_higher_order type_enc orelse is_type_enc_fool type_enc) then `I tptp_bool_type else `make_fixed_type_const s, []), map term Ts) | term (TFree (s, _)) = AType ((`make_tfree s, []), []) | term (TVar z) = AType ((tvar_name z, []), []) in term end fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys) | atp_term_of_atp_type _ = raise Fail "unexpected type" fun atp_type_of_type_arg type_enc T = if T = dummyT then NONE else SOME (raw_atp_type_of_typ type_enc T) (* This shouldn't clash with anything else. *) val uncurried_alias_sep = "\000" val mangled_type_sep = "\001" val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep fun generic_mangled_type_name f (AType ((name, _), [])) = f name | generic_mangled_type_name f (AType ((name, _), tys)) = f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")" | generic_mangled_type_name _ _ = raise Fail "unexpected type" fun mangled_type type_enc = generic_mangled_type_name fst o raw_atp_type_of_typ type_enc fun make_native_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s else native_type_prefix ^ ascii_of s fun native_atp_type_of_raw_atp_type type_enc pred_sym ary = let fun to_mangled_atype ty = AType (((make_native_type (generic_mangled_type_name fst ty), generic_mangled_type_name snd ty), []), []) fun to_poly_atype (AType ((name, clss), tys)) = AType ((name, clss), map to_poly_atype tys) | to_poly_atype _ = raise Fail "unexpected type" val to_atype = if is_type_enc_polymorphic type_enc then to_poly_atype else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) fun to_ho (ty as AType (((s, _), _), tys)) = if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty | to_ho _ = raise Fail "unexpected type" + fun to_lfho (ty as AType (((s, _), _), tys)) = + if s = tptp_fun_type then to_afun to_ho to_lfho tys + else if pred_sym then bool_atype + else to_atype ty + | to_lfho _ = raise Fail "unexpected type" fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty | to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys | to_fo _ _ = raise Fail "unexpected type" in - if is_type_enc_higher_order type_enc then to_ho + if is_type_enc_full_higher_order type_enc then to_ho + else if is_type_enc_higher_order type_enc then to_lfho else to_fo ary end fun native_atp_type_of_typ type_enc pred_sym ary = native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc (* Make atoms for sorted type variables. *) fun generic_add_sorts_on_type _ [] = I | generic_add_sorts_on_type T (s :: ss) = generic_add_sorts_on_type T ss #> (if s = the_single \<^sort>\type\ then I else insert (op =) (s, T)) fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S | add_sorts_on_tfree _ = I fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S | add_sorts_on_tvar _ = I fun process_type_args type_enc T_args = if is_type_enc_native type_enc then (map (native_atp_type_of_typ type_enc false 0) T_args, []) else ([], map_filter (Option.map atp_term_of_atp_type o atp_type_of_type_arg type_enc) T_args) fun class_atom type_enc (cl, T) = let val cl = `make_class cl val (ty_args, tm_args) = process_type_args type_enc [T] val tm_args = tm_args @ (case type_enc of Native (_, _, Raw_Polymorphic Without_Phantom_Type_Vars, _) => [ATerm ((TYPE_name, ty_args), [])] | _ => []) in AAtom (ATerm ((cl, ty_args), tm_args)) end fun class_atoms type_enc (cls, T) = map (fn cl => class_atom type_enc (cl, T)) cls fun class_membs_of_types type_enc add_sorts_on_typ Ts = [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c)) fun mk_ahorn [] phi = phi | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi]) fun mk_aquant _ [] phi = phi | mk_aquant q xs (phi as AQuant (q', xs', phi')) = if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi) | mk_aquant q xs phi = AQuant (q, xs, phi) fun mk_atyquant _ [] phi = phi | mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) = if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi) | mk_atyquant q xs phi = ATyQuant (q, xs, phi) fun close_universally add_term_vars phi = let fun add_formula_vars bounds (ATyQuant (_, _, phi)) = add_formula_vars bounds phi | add_formula_vars bounds (AQuant (_, xs, phi)) = add_formula_vars (map fst xs @ bounds) phi | add_formula_vars bounds (AConn (_, phis)) = fold (add_formula_vars bounds) phis | add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm in mk_aquant AForall (rev (add_formula_vars [] phi [])) phi end fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) = (if is_tptp_variable s andalso not (String.isPrefix tvar_prefix s) andalso not (member (op =) bounds name) then insert (op =) (name, NONE) else I) #> fold (add_term_vars bounds) tms | add_term_vars bounds (AAbs (((name, _), tm), args)) = add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args fun close_formula_universally phi = close_universally add_term_vars phi fun add_iterm_vars bounds (IApp (tm1, tm2)) = fold (add_iterm_vars bounds) [tm1, tm2] | add_iterm_vars _ (IConst _) = I | add_iterm_vars bounds (IVar (name, T)) = not (member (op =) bounds name) ? insert (op =) (name, SOME T) | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm fun aliased_uncurried ary (s, s') = (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary) fun unaliased_uncurried (s, s') = (case space_explode uncurried_alias_sep s of [_] => (s, s') | [s1, s2] => (s1, unsuffix s2 s') | _ => raise Fail "ill-formed explicit application alias") fun raw_mangled_const_name type_name ty_args (s, s') = let fun type_suffix f g = fold_rev (prefix o g o prefix mangled_type_sep o type_name f) ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end fun mangled_const_name type_enc = map_filter (atp_type_of_type_arg type_enc) #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode fun parse_mangled_type x = (parse_mangled_ident -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")") [] >> (ATerm o apfst (rpair []))) x and parse_mangled_types x = (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x fun unmangled_type s = s |> suffix ")" |> raw_explode |> Scan.finite Symbol.stopper (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ quote s)) parse_mangled_type)) |> fst fun unmangled_const_name s = (s, s) |> unaliased_uncurried |> fst |> space_explode mangled_type_sep fun unmangled_const s = let val ss = unmangled_const_name s in (hd ss, map unmangled_type (tl ss)) end val unmangled_invert_const = invert_const o hd o unmangled_const_name fun introduce_proxies_in_iterm type_enc = let fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, []) | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ = (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser limitation. This works in conjuction with special code in "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever possible. *) IAbs ((`I "P", p_T), IApp (IConst (`I ho_quant, T, []), IAbs ((`I "X", x_T), IApp (IConst (`I "P", p_T, []), IConst (`I "X", x_T, []))))) | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier" fun intro top_level args (IApp (tm1, tm2)) = IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2) | intro top_level args (IConst (name as (s, _), T, T_args)) = (case proxify_const s of SOME proxy_base => let val argc = length args val plain_const = IConst (name, T, []) fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args) val is_fool = is_type_enc_fool type_enc fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const in - if top_level orelse is_fool orelse is_type_enc_higher_order type_enc then + if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then (case (top_level, s) of (_, "c_False") => IConst (`I tptp_false, T, []) | (_, "c_True") => IConst (`I tptp_true, T, []) | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, [])) | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, [])) | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, [])) | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, [])) | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args) | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args) | (false, s) => if is_tptp_equal s then if argc = 2 then IConst (`I tptp_equal, T, []) else if is_fool then proxy_const () else (* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers complain about not being able to infer the type of "=". *) let val i_T = domain_type T in IAbs ((`I "Y", i_T), IAbs ((`I "Z", i_T), IApp (IApp (IConst (`I tptp_equal, T, []), IConst (`I "Y", i_T, [])), IConst (`I "Z", i_T, [])))) end else plain_const | _ => plain_const) else IConst (proxy_base |>> prefix const_prefix, T, T_args) end | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args else IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end fun mangle_type_args_in_const type_enc (name as (s, _)) T_args = if String.isPrefix const_prefix s andalso is_type_enc_mangling type_enc then (mangled_const_name type_enc T_args name, []) else (name, T_args) fun mangle_type_args_in_iterm type_enc = if is_type_enc_mangling type_enc then let fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2) | mangle (tm as IConst (_, _, [])) = tm | mangle (IConst (name, T, T_args)) = mangle_type_args_in_const type_enc name T_args |> (fn (name, T_args) => IConst (name, T, T_args)) | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm) | mangle tm = tm in mangle end else I fun filter_type_args_in_const _ _ _ _ _ [] = [] | filter_type_args_in_const thy ctrss type_enc ary s T_args = (case unprefix_and_unascii const_prefix s of NONE => if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] else T_args | SOME s'' => filter_type_args thy ctrss type_enc (unmangled_invert_const s'') ary T_args) fun filter_type_args_in_iterm thy ctrss type_enc = let fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) | filt ary (IConst (name as (s, _), T, T_args)) = filter_type_args_in_const thy ctrss type_enc ary s T_args |> (fn T_args => IConst (name, T, T_args)) | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) | filt _ tm = tm in filt 0 end fun iformula_of_prop ctxt type_enc iff_for_eq = let val thy = Proof_Context.theory_of ctxt fun do_term bs t atomic_Ts = iterm_of_term thy type_enc bs (Envir.eta_contract t) |>> (introduce_proxies_in_iterm type_enc #> mangle_type_args_in_iterm type_enc #> AAtom) ||> union (op =) atomic_Ts fun do_quant bs q pos s T t' = let val s = singleton (Name.variant_list (map fst bs)) s val universal = Option.map (q = AExists ? not) pos val name = s |> `(case universal of SOME true => make_all_bound_var | SOME false => make_exist_bound_var | NONE => make_bound_var) in do_formula ((s, (name, T)) :: bs) pos t' #>> mk_aquant q [(name, SOME T)] ##> union (op =) (atomic_types_of T) end and do_conn bs c pos1 t1 pos2 t2 = do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c) and do_formula bs pos t = (case t of \<^const>\Trueprop\ $ t1 => do_formula bs pos t1 | \<^const>\Not\ $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot | Const (\<^const_name>\All\, _) $ Abs (s, T, t') => do_quant bs AForall pos s T t' | (t0 as Const (\<^const_name>\All\, _)) $ t1 => do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1) | Const (\<^const_name>\Ex\, _) $ Abs (s, T, t') => do_quant bs AExists pos s T t' | (t0 as Const (\<^const_name>\Ex\, _)) $ t1 => do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1) | \<^const>\HOL.conj\ $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2 | \<^const>\HOL.disj\ $ t1 $ t2 => do_conn bs AOr pos t1 pos t2 | \<^const>\HOL.implies\ $ t1 $ t2 => do_conn bs AImplies (Option.map not pos) t1 pos t2 | Const (\<^const_name>\HOL.eq\, Type (_, [\<^typ>\bool\, _])) $ t1 $ t2 => if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t | _ => do_term bs t) in do_formula [] end fun presimplify_term ctxt t = if exists_Const (member (op =) Meson.presimplified_consts o fst) t then t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |> Meson.presimplify ctxt |> Thm.prop_of else t fun preprocess_abstractions_in_terms trans_lams facts = let val (facts, lambda_ts) = facts |> map (snd o snd) |> trans_lams |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts val lam_facts = map2 (fn t => fn j => ((lam_fact_prefix ^ Int.toString j, (Global, Non_Rec_Def)), (Axiom, t))) lambda_ts (1 upto length lambda_ts) in (facts, lam_facts) end (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to prevent the discovery of unreplayable proofs. *) fun freeze_term t = let (* Freshness is desirable for completeness, but not for soundness. *) fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix fun freeze (t $ u) = freeze t $ freeze u | freeze (Abs (s, T, t)) = Abs (s, T, freeze t) | freeze (Var (x, T)) = Free (indexed_name x, T) | freeze t = t fun freeze_tvar (x, S) = TFree (indexed_name x, S) in t |> exists_subterm is_Var t ? freeze |> exists_type (exists_subtype is_TVar) t ? map_types (map_type_tvar freeze_tvar) end fun presimp_prop ctxt type_enc t = let val t = t |> Envir.beta_eta_contract |> transform_elim_prop |> Object_Logic.atomize_term ctxt val need_trueprop = (fastype_of t = \<^typ>\bool\) - val is_ho = is_type_enc_higher_order type_enc + val is_ho = is_type_enc_full_higher_order type_enc in t |> need_trueprop ? HOLogic.mk_Trueprop |> (if is_ho then unextensionalize_def else cong_extensionalize_term ctxt #> abs_extensionalize_term ctxt) |> presimplify_term ctxt |> HOLogic.dest_Trueprop end handle TERM _ => \<^const>\True\ (* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical reasons. *) fun should_use_iff_for_eq CNF _ = false - | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format) + | should_use_iff_for_eq (THF _) format = not (is_type_enc_full_higher_order format) | should_use_iff_for_eq _ _ = true fun make_formula ctxt format type_enc iff_for_eq name stature role t = let val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc val (iformula, atomic_Ts) = iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t [] |>> close_universally add_iterm_vars in {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts} end fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) = (case make_formula ctxt format type_enc iff_for_eq name stature Axiom t of formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula | formula => SOME formula) fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => let val t' = t |> role = Conjecture ? s_not in make_formula ctxt format type_enc true name stature role t' end) (** Finite and infinite type inference **) fun tvar_footprint thy s ary = (case unprefix_and_unascii const_prefix s of SOME s => let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in s |> unmangled_invert_const |> robust_const_type thy |> chop_fun ary |> fst |> map tvars_of end | NONE => []) handle TYPE _ => [] fun type_arg_cover thy pos s ary = if is_tptp_equal s then if pos = SOME false then [] else 0 upto ary - 1 else let val footprint = tvar_footprint thy s ary val eq = (s = \<^const_name>\HOL.eq\) fun cover _ [] = [] | cover seen ((i, tvars) :: args) = cover (union (op =) seen tvars) args |> (eq orelse exists (fn tvar => not (member (op =) seen tvar)) tvars) ? cons i in if forall null footprint then [] else 0 upto length footprint - 1 ~~ footprint |> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd) |> cover [] end type monotonicity_info = {maybe_finite_Ts : typ list, surely_infinite_Ts : typ list, maybe_nonmono_Ts : typ list} (* These types witness that the type classes they belong to allow infinite models and hence that any types with these type classes is monotonic. *) val known_infinite_types = [\<^typ>\nat\, HOLogic.intT, HOLogic.realT, \<^typ>\nat => bool\] fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T = strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are dangerous because their "exhaust" properties can easily lead to unsound ATP proofs. On the other hand, all HOL infinite types can be given the same models in first-order logic (via Loewenheim-Skolem). *) fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts} (Nonmono_Types (strictness, _)) T = let val thy = Proof_Context.theory_of ctxt in (exists (type_intersect thy T) maybe_nonmono_Ts andalso not (exists (type_instance thy T) surely_infinite_Ts orelse (not (member (type_equiv thy) maybe_finite_Ts T) andalso is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T))) end | should_encode_type _ _ level _ = (level = All_Types orelse level = Undercover_Types) fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T = should_guard_var () andalso should_encode_type ctxt mono level T | should_guard_type _ _ _ _ _ = false fun is_maybe_universal_name s = String.isPrefix bound_var_prefix s orelse String.isPrefix all_bound_var_prefix s fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s | is_maybe_universal_var (IVar _) = true | is_maybe_universal_var _ = false datatype site = Top_Level of bool option | Eq_Arg of bool option | Arg of string * int * int | Elsewhere fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false | should_tag_with_type ctxt mono (Tags (_, level)) site u T = let val thy = Proof_Context.theory_of ctxt in (case level of Nonmono_Types (_, Non_Uniform) => (case (site, is_maybe_universal_var u) of (Eq_Arg pos, true) => (pos <> SOME false orelse tag_neg_vars) andalso should_encode_type ctxt mono level T | _ => false) | Undercover_Types => (case (site, is_maybe_universal_var u) of (Eq_Arg pos, true) => pos <> SOME false | (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy NONE s ary) j | _ => false) | _ => should_encode_type ctxt mono level T) end | should_tag_with_type _ _ _ _ _ _ = false (** predicators and application operators **) type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool} fun default_sym_tab_entries type_enc = (make_fixed_const NONE \<^const_name>\undefined\, {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) :: ([tptp_false, tptp_true] |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @ ([tptp_equal, tptp_old_equal] |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false})) - |> not (is_type_enc_fool type_enc orelse is_type_enc_higher_order type_enc) + |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc) ? cons (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false}) datatype app_op_level = Min_App_Op | Sufficient_App_Op | Sufficient_App_Op_And_Predicator | Full_App_Op_And_Predicator fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact = let val thy = Proof_Context.theory_of ctxt fun consider_var_ary const_T var_T max_ary = let fun iter ary T = if ary = max_ary orelse type_instance thy var_T T orelse type_instance thy T var_T then ary else iter (ary + 1) (range_type T) in iter 0 const_T end fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) = if (app_op_level = Sufficient_App_Op andalso can dest_funT T) orelse (app_op_level = Sufficient_App_Op_And_Predicator andalso (can dest_funT T orelse T = \<^typ>\bool\)) then let val bool_vars' = bool_vars orelse (app_op_level = Sufficient_App_Op_And_Predicator andalso body_type T = \<^typ>\bool\) fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} = {pred_sym = pred_sym andalso not bool_vars', min_ary = fold (fn T' => consider_var_ary T' T) types min_ary, max_ary = max_ary, types = types, in_conj = in_conj} val fun_var_Ts' = fun_var_Ts |> can dest_funT T ? insert_type thy I T in if bool_vars' = bool_vars andalso fun_var_Ts' = fun_var_Ts then accum else ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab) end else accum fun add_iterm_syms top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, _), T, _) => if is_maybe_universal_name s then add_universal_var T accum else if String.isPrefix exist_bound_var_prefix s then accum else let val ary = length args in ((bool_vars, fun_var_Ts), (case Symtab.lookup sym_tab s of SOME {pred_sym, min_ary, max_ary, types, in_conj} => let val pred_sym = pred_sym andalso top_level andalso not bool_vars val types' = types |> insert_type thy I T val in_conj = in_conj orelse conj_fact val min_ary = if (app_op_level = Sufficient_App_Op orelse app_op_level = Sufficient_App_Op_And_Predicator) andalso types' <> types then fold (consider_var_ary T) fun_var_Ts min_ary else min_ary in Symtab.update (s, {pred_sym = pred_sym, min_ary = Int.min (ary, min_ary), max_ary = Int.max (ary, max_ary), types = types', in_conj = in_conj}) sym_tab end | NONE => let val max_ary = (case unprefix_and_unascii const_prefix s of SOME s => (if String.isSubstring uncurried_alias_sep s then ary else (case try (ary_of o robust_const_type thy o unmangled_invert_const) s of SOME ary0 => Int.min (ary0, ary) | NONE => ary)) | NONE => ary) val pred_sym = top_level andalso max_ary = ary andalso not bool_vars val min_ary = (case app_op_level of Min_App_Op => max_ary | Full_App_Op_And_Predicator => 0 | _ => fold (consider_var_ary T) fun_var_Ts max_ary) in Symtab.update_new (s, {pred_sym = pred_sym, min_ary = min_ary, max_ary = max_ary, types = [T], in_conj = conj_fact}) sym_tab end)) end | IVar (_, T) => add_universal_var T accum | IAbs ((_, T), tm) => accum |> add_universal_var T |> add_iterm_syms false tm | _ => accum) |> fold (add_iterm_syms false) args end in add_iterm_syms end fun sym_table_of_facts ctxt type_enc app_op_level conjs facts = let fun add_iterm_syms conj_fact = add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true fun add_fact_syms conj_fact = ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact))) in ((false, []), Symtab.empty) |> fold (add_fact_syms true) conjs |> fold (add_fact_syms false) facts ||> fold Symtab.update (default_sym_tab_entries type_enc) end fun min_ary_of sym_tab s = (case Symtab.lookup sym_tab s of SOME ({min_ary, ...} : sym_info) => min_ary | NONE => (case unprefix_and_unascii const_prefix s of SOME s => let val s = s |> unmangled_invert_const in if s = predicator_name then 1 else if s = app_op_name then 2 else if s = type_guard_name then 1 else 0 end | NONE => 0)) (* True if the constant ever appears outside of the top-level position in literals, or if it appears with different arities (e.g., because of different type instantiations). If false, the constant always receives all of its arguments and is used as a predicate. *) fun is_pred_sym sym_tab s = (case Symtab.lookup sym_tab s of SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) => pred_sym andalso min_ary = max_ary | NONE => false) val fTrue_iconst = IConst ((const_prefix ^ "fTrue", \<^const_name>\fTrue\), \<^typ>\bool\, []) val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, \<^typ>\bool => bool\, []) fun predicatify completish tm = if completish > 1 then IApp (IApp (IConst (`I tptp_equal, \<^typ>\bool => bool => bool\, []), tm), fTrue_iconst) else IApp (predicator_iconst, tm) val app_op = `(make_fixed_const NONE) app_op_name fun list_app head args = fold (curry (IApp o swap)) args head fun mk_app_op type_enc head arg = let val head_T = ityp_of head val (arg_T, res_T) = dest_funT head_T val app = IConst (app_op, head_T --> head_T, [arg_T, res_T]) |> mangle_type_args_in_iterm type_enc in list_app app [head, arg] end fun firstorderize_fact thy ctrss type_enc uncurried_aliases completish sym_tab = let fun do_app arg head = mk_app_op type_enc head arg fun list_app_ops (head, args) = fold do_app args head fun introduce_app_ops tm = let val (head, args) = tm |> strip_iterm_comb ||> map introduce_app_ops in (case head of IConst (name as (s, _), T, T_args) => let val min_ary = min_ary_of sym_tab s val ary = if uncurried_aliases andalso String.isPrefix const_prefix s then let val ary = length args (* In polymorphic native type encodings, it is impossible to declare a fully polymorphic symbol that takes more arguments than its signature (even though such concrete instances, where a type variable is instantiated by a function type, are possible.) *) val official_ary = if is_type_enc_polymorphic type_enc then (case unprefix_and_unascii const_prefix s of SOME s' => (case try (ary_of o robust_const_type thy) (invert_const s') of SOME ary => ary | NONE => min_ary) | NONE => min_ary) else 1000000000 (* irrealistically big arity *) in Int.min (ary, official_ary) end else min_ary val head = if ary = min_ary then head else IConst (aliased_uncurried ary name, T, T_args) in args |> chop ary |>> list_app head |> list_app_ops end | _ => list_app_ops (head, args)) end fun introduce_predicators tm = (case strip_iterm_comb tm of (IConst ((s, _), _, _), _) => if is_pred_sym sym_tab s then tm else predicatify completish tm | _ => predicatify completish tm) + val is_ho = is_type_enc_higher_order type_enc + val is_full_ho = is_type_enc_full_higher_order type_enc + val is_fool = is_type_enc_fool type_enc val do_iterm = - (not (is_type_enc_higher_order type_enc) ? - (introduce_app_ops #> - not (is_type_enc_fool type_enc) ? introduce_predicators)) + (not is_ho ? introduce_app_ops) + #> (not (is_full_ho orelse is_fool) ? introduce_predicators) #> filter_type_args_in_iterm thy ctrss type_enc in update_iformula (formula_map do_iterm) end (** Helper facts **) val not_ffalse = @{lemma "\ fFalse" by (unfold fFalse_def) fast} val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast} (* The Boolean indicates that a fairly sound type encoding is needed. *) val base_helper_table = [(("COMBI", false), [(Non_Rec_Def, @{thm Meson.COMBI_def})]), (("COMBK", false), [(Non_Rec_Def, @{thm Meson.COMBK_def})]), (("COMBB", false), [(Non_Rec_Def, @{thm Meson.COMBB_def})]), (("COMBC", false), [(Non_Rec_Def, @{thm Meson.COMBC_def})]), (("COMBS", false), [(Non_Rec_Def, @{thm Meson.COMBS_def})]), ((predicator_name, false), [(General, not_ffalse), (General, ftrue)]), (("fFalse", false), [(General, not_ffalse)]), (("fFalse", true), [(General, @{thm True_or_False})]), (("fTrue", false), [(General, ftrue)]), (("fTrue", true), [(General, @{thm True_or_False})]), (("If", true), [(Non_Rec_Def, @{thm if_True}), (Non_Rec_Def, @{thm if_False}), (General, @{thm True_or_False})])] val helper_table = base_helper_table @ [(("fNot", false), @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]} |> map (pair Non_Rec_Def)), (("fconj", false), @{lemma "\ P \ \ Q \ fconj P Q" "\ fconj P Q \ P" "\ fconj P Q \ Q" by (unfold fconj_def) fast+} |> map (pair General)), (("fdisj", false), @{lemma "\ P \ fdisj P Q" "\ Q \ fdisj P Q" "\ fdisj P Q \ P \ Q" by (unfold fdisj_def) fast+} |> map (pair General)), (("fimplies", false), @{lemma "P \ fimplies P Q" "\ Q \ fimplies P Q" "\ fimplies P Q \ \ P \ Q" by (unfold fimplies_def) fast+} |> map (pair General)), (("fequal", true), (* This is a lie: Higher-order equality doesn't need a sound type encoding. However, this is done so for backward compatibility: Including the equality helpers by default in Metis breaks a few existing proofs. *) @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]} |> map (pair General)), (* Partial characterization of "fAll" and "fEx". A complete characterization would require the axiom of choice for replay with Metis. *) (("fAll", false), [(General, @{lemma "\ fAll P \ P x" by (auto simp: fAll_def)})]), (("fEx", false), [(General, @{lemma "\ P x \ fEx P" by (auto simp: fEx_def)})])] |> map (apsnd (map (apsnd zero_var_indexes))) val completish_helper_table = helper_table @ [((predicator_name, true), @{thms True_or_False fTrue_ne_fFalse} |> map (pair General)), ((app_op_name, true), [(General, @{lemma "\x. \ f x = g x \ f = g" by blast}), (General, @{lemma "\p. (p x \ p y) \ x = y" by blast})]), (("fconj", false), @{thms fconj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fdisj", false), @{thms fdisj_table fconj_laws fdisj_laws} |> map (pair Non_Rec_Def)), (("fimplies", false), @{thms fimplies_table fconj_laws fdisj_laws fimplies_laws} |> map (pair Non_Rec_Def)), (("fequal", false), (@{thms fequal_table} |> map (pair Non_Rec_Def)) @ (@{thms fequal_laws} |> map (pair General))), (("fAll", false), @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def)), (("fEx", false), @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Non_Rec_Def))] |> map (apsnd (map (apsnd zero_var_indexes))) fun bound_tvars type_enc sorts Ts = (case filter is_TVar Ts of [] => I | Ts => ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic) ? mk_ahorn (Ts |> class_membs_of_types type_enc add_sorts_on_tvar |> map (class_atom type_enc))) #> (case type_enc of Native (_, _, Type_Class_Polymorphic, _) => mk_atyquant AForall (map (fn TVar (z as (_, S)) => (AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts) | Native (_, _, Raw_Polymorphic _, _) => mk_atyquant AForall (map (fn TVar (z as _) => (AType ((tvar_name z, []), []), [])) Ts) | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))) fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 = (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2]))) |> mk_aquant AForall bounds |> close_formula_universally |> bound_tvars type_enc true atomic_Ts val helper_rank = default_rank val min_rank = 9 * helper_rank div 10 val max_rank = 4 * min_rank fun rank_of_fact_num n j = min_rank + (max_rank - min_rank) * j div n val type_tag = `(make_fixed_const NONE) type_tag_name fun could_specialize_helpers type_enc = not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types fun should_specialize_helper type_enc t = could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t)) fun add_helper_facts_of_sym ctxt format type_enc completish (s, {types, ...} : sym_info) = (case unprefix_and_unascii const_prefix s of SOME mangled_s => let val thy = Proof_Context.theory_of ctxt val unmangled_s = mangled_s |> unmangled_const_name |> hd fun dub needs_sound j k = ascii_of unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^ (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^ (if needs_sound then typed_helper_suffix else untyped_helper_suffix) fun specialize_helper t T = if unmangled_s = app_op_name then let val tyenv = Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty in Envir.subst_term_types tyenv t end else specialize_type thy (invert_const unmangled_s, T) t fun dub_and_inst needs_sound ((status, t), j) = (if should_specialize_helper type_enc t then map_filter (try (specialize_helper t)) types else [t]) |> tag_list 1 |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t)) val make_facts = map_filter (make_fact ctxt format type_enc false) val sound = is_type_enc_sound type_enc val could_specialize = could_specialize_helpers type_enc in fold (fn ((helper_s, needs_sound), ths) => if (needs_sound andalso not sound) orelse (helper_s <> unmangled_s andalso (completish < 3 orelse could_specialize)) then I else ths ~~ (1 upto length ths) |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of)) |> make_facts |> union (op = o apply2 #iformula)) (if completish >= 3 then completish_helper_table else helper_table) end | NONE => I) fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab [] (***************************************************************) (* Type Classes Present in the Axiom or Conjecture Clauses *) (***************************************************************) fun set_insert (x, s) = Symtab.update (x, ()) s fun add_classes (cls, cset) = List.foldl set_insert cset (flat cls) fun classes_of_terms get_Ts = map (map snd o get_Ts) #> List.foldl add_classes Symtab.empty #> Symtab.delete_safe class_of_types #> Symtab.keys val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars fun fold_type_ctrs f (Type (s, Ts)) x = fold (fold_type_ctrs f) Ts (f (s, x)) | fold_type_ctrs _ _ x = x (* Type constructors used to instantiate overloaded constants are the only ones needed. *) fun add_type_ctrs_in_term thy = let fun add (Const (\<^const_name>\Meson.skolem\, _) $ _) = I | add (t $ u) = add t #> add u | add (Const x) = x |> robust_const_type_args thy |> fold (fold_type_ctrs set_insert) | add (Abs (_, _, u)) = add u | add _ = I in add end fun type_ctrs_of_terms thy ts = Symtab.keys (fold (add_type_ctrs_in_term thy) ts Symtab.empty) fun trans_lams_of_string ctxt type_enc lam_trans = if lam_trans = no_lamsN then rpair [] else if lam_trans = hide_lamsN then lift_lams ctxt type_enc ##> K [] else if lam_trans = liftingN orelse lam_trans = lam_liftingN then lift_lams ctxt type_enc else if lam_trans = combsN then map (introduce_combinators ctxt) #> rpair [] else if lam_trans = combs_and_liftingN then lift_lams_part_1 ctxt type_enc ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) #> lift_lams_part_2 ctxt else if lam_trans = combs_or_liftingN then lift_lams_part_1 ctxt type_enc ##> map (fn t => (case head_of (strip_qnt_body \<^const_name>\All\ t) of \<^term>\(=) ::bool => bool => bool\ => t | _ => introduce_combinators ctxt (intentionalize_def t))) #> lift_lams_part_2 ctxt else if lam_trans = keep_lamsN then map (Envir.eta_contract) #> rpair [] else error ("Unknown lambda translation scheme: " ^ quote lam_trans) val pull_and_reorder_definitions = let fun add_consts (IApp (t, u)) = fold add_consts [t, u] | add_consts (IAbs (_, t)) = add_consts t | add_consts (IConst (name, _, _)) = insert (op =) name | add_consts (IVar _) = I fun consts_of_hs l_or_r ({iformula, ...} : ifact) = (case iformula of AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) [] | _ => []) (* Quadratic, but usually OK. *) fun reorder [] [] = [] | reorder (fact :: skipped) [] = fact :: reorder [] skipped (* break cycle *) | reorder skipped (fact :: facts) = let val rhs_consts = consts_of_hs snd fact in if exists (exists (exists (member (op =) rhs_consts) o consts_of_hs fst)) [skipped, facts] then reorder (fact :: skipped) facts else fact :: reorder [] (facts @ skipped) end in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end fun s_not_prop (\<^const>\Trueprop\ $ t) = \<^const>\Trueprop\ $ s_not t | s_not_prop (\<^const>\Pure.imp\ $ t $ \<^prop>\False\) = t | s_not_prop t = \<^const>\Pure.imp\ $ t $ \<^prop>\False\ fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val trans_lams = trans_lams_of_string ctxt type_enc lam_trans val fact_ts = facts |> map snd (* Remove existing facts from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then \<^prop>\True\ else t) val hyp_ts = map freeze_term hyp_ts; val concl_t = freeze_term concl_t; val facts = facts |> map (apsnd (pair Axiom)) val conjs = map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)] |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts) val ((conjs, facts), lam_facts) = (conjs, facts) |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop ctxt type_enc)))) |> (if lam_trans = no_lamsN then rpair [] else op @ #> preprocess_abstractions_in_terms trans_lams #>> chop (length conjs)) val conjs = conjs |> make_conjecture ctxt format type_enc |> pull_and_reorder_definitions val facts = facts |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t)) |> pull_and_reorder_definitions val lifted = lam_facts |> map (extract_lambda_def dest_Const o snd o snd) val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) val all_ts = concl_t :: hyp_ts @ fact_ts val subs = tfree_classes_of_terms all_ts val supers = tvar_classes_of_terms all_ts val tycons = type_ctrs_of_terms thy all_ts val (supers, tcon_clauses) = if level_of_type_enc type_enc = No_Types then ([], []) else make_tcon_clauses thy tycons supers val subclass_pairs = make_subclass_pairs thy subs supers in (union (op =) subs supers, conjs, facts @ lam_facts, subclass_pairs, tcon_clauses, lifted) end val type_guard = `(make_fixed_const NONE) type_guard_name fun type_guard_iterm type_enc T tm = IApp (IConst (type_guard, T --> \<^typ>\bool\, [T]) |> mangle_type_args_in_iterm type_enc, tm) fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum | is_var_positively_naked_in_term name _ (ATerm (((s, _), _), tms)) accum = accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), []))) | is_var_positively_naked_in_term _ _ _ _ = true fun is_var_undercover_in_term thy name pos tm accum = accum orelse let val var = ATerm ((name, []), []) fun is_undercover (ATerm (_, [])) = false | is_undercover (ATerm (((s, _), _), tms)) = let val ary = length tms val cover = type_arg_cover thy pos s ary in exists (fn (j, tm) => tm = var andalso member (op =) cover j) (0 upto ary - 1 ~~ tms) orelse exists is_undercover tms end | is_undercover _ = true in is_undercover tm end fun should_guard_var_in_formula thy level pos phi (SOME true) name = (case level of All_Types => true | Undercover_Types => formula_fold pos (is_var_undercover_in_term thy name) phi false | Nonmono_Types (_, Uniform) => true | Nonmono_Types (_, Non_Uniform) => formula_fold pos (is_var_positively_naked_in_term name) phi false | _ => false) | should_guard_var_in_formula _ _ _ _ _ _ = true fun always_guard_var_in_formula _ _ _ _ _ _ = true fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T = not (is_type_level_uniform level) andalso should_encode_type ctxt mono level T | should_generate_tag_bound_decl _ _ _ _ _ = false fun mk_aterm type_enc name T_args args = let val (ty_args, tm_args) = process_type_args type_enc T_args in ATerm ((name, ty_args), tm_args @ args) end fun do_bound_type type_enc = (case type_enc of Native _ => native_atp_type_of_typ type_enc false 0 #> SOME | _ => K NONE) fun tag_with_type ctxt mono type_enc pos T tm = IConst (type_tag, T --> T, [T]) |> mangle_type_args_in_iterm type_enc |> atp_term_of_iterm ctxt mono type_enc pos |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") and atp_term_of_iterm ctxt mono type_enc pos = let fun term site u = let val (head, args) = strip_iterm_comb u val pos = (case site of Top_Level pos => pos | Eq_Arg pos => pos | _ => NONE) val T = ityp_of u val t = (case head of IConst (name as (s, _), _, T_args) => let val ary = length args fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary) in map2 (fn j => term (arg_site j)) (0 upto ary - 1) args |> mk_aterm type_enc name T_args end | IVar (name, _) => map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => if is_type_enc_higher_order type_enc then AAbs (((name, native_atp_type_of_typ type_enc false 0 T), term Elsewhere tm), map (term Elsewhere) args) else raise Fail "unexpected lambda-abstraction" | IApp _ => raise Fail "impossible \"IApp\"") val tag = should_tag_with_type ctxt mono type_enc site u T in t |> tag ? tag_with_type ctxt mono type_enc pos T end in term (Top_Level pos) end and formula_of_iformula ctxt mono type_enc should_guard_var = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc val do_term = atp_term_of_iterm ctxt mono type_enc fun do_out_of_bound_type pos phi universal (name, T) = if should_guard_type ctxt mono type_enc (fn () => should_guard_var thy level pos phi universal name) T then IVar (name, T) |> type_guard_iterm type_enc T |> do_term pos |> AAtom |> SOME else if should_generate_tag_bound_decl ctxt mono type_enc universal T then let val var = ATerm ((name, []), []) val tagged_var = tag_with_type ctxt mono type_enc pos T var in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end else NONE fun do_formula pos (ATyQuant (q, xs, phi)) = ATyQuant (q, map (apfst (native_atp_type_of_typ type_enc false 0)) xs, do_formula pos phi) | do_formula pos (AQuant (q, xs, phi)) = let val phi = phi |> do_formula pos val universal = Option.map (q = AExists ? not) pos in AQuant (q, xs |> map (apsnd (fn NONE => NONE | SOME T => do_bound_type type_enc T)), (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd)) (map_filter (fn (_, NONE) => NONE | (s, SOME T) => do_out_of_bound_type pos phi universal (s, T)) xs) phi) end | do_formula pos (AConn conn) = aconn_map pos do_formula conn | do_formula pos (AAtom tm) = AAtom (do_term pos tm) in do_formula end fun string_of_status General = "" | string_of_status Induction = inductionN | string_of_status Intro = introN | string_of_status Inductive = inductiveN | string_of_status Elim = elimN | string_of_status Simp = simpN | string_of_status Non_Rec_Def = non_rec_defN | string_of_status Rec_Def = rec_defN (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP forbids name clashes, and some of the remote provers might care. *) fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank (j, {name, stature = (_, status), role, iformula, atomic_types}) = Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, alt name), role, iformula |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (if pos then SOME true else NONE) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, isabelle_info generate_info (string_of_status status) (rank j)) fun lines_of_subclass generate_info type_enc sub super = Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], NONE, isabelle_info generate_info inductiveN helper_rank) fun lines_of_subclass_pair generate_info type_enc (sub, supers) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)] else map (lines_of_subclass generate_info type_enc sub) supers fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems, native_atp_type_of_typ type_enc false 0 T, `make_class cl) else Formula ((tcon_clause_prefix ^ name, ""), Axiom, mk_ahorn (maps (class_atoms type_enc) prems) (class_atom type_enc (cl, T)) |> bound_tvars type_enc true (snd (dest_Type T)), NONE, isabelle_info generate_info inductiveN helper_rank) fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) = Formula ((conjecture_prefix ^ name, ""), role, iformula |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false) |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) fun lines_of_free_types type_enc (facts : ifact list) = if is_type_enc_polymorphic type_enc then let val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic) fun line j (cl, T) = if type_classes then Class_Memb (class_memb_prefix ^ string_of_int j, [], native_atp_type_of_typ type_enc false 0 T, `make_class cl) else Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis, class_atom type_enc (cl, T), NONE, []) val membs = fold (union (op =)) (map #atomic_types facts) [] |> class_membs_of_types type_enc add_sorts_on_tfree in map2 line (0 upto length membs - 1) membs end else [] (** Symbol declarations **) fun decl_line_of_class phantoms s = let val name as (s, _) = `make_class s in Sym_Decl (sym_decl_prefix ^ s, name, APi ([tvar_a_name], if phantoms = Without_Phantom_Type_Vars then AFun (a_itself_atype, bool_atype) else bool_atype)) end fun decl_lines_of_classes type_enc = (case type_enc of Native (_, _, Raw_Polymorphic phantoms, _) => map (decl_line_of_class phantoms) | _ => K []) fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) = let fun add_iterm_syms tm = let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, s'), T, T_args) => let val (pred_sym, in_conj) = (case Symtab.lookup sym_tab s of SOME ({pred_sym, in_conj, ...} : sym_info) => (pred_sym, in_conj) | NONE => (false, false)) val decl_sym = (case type_enc of Guards _ => not pred_sym | _ => true) andalso is_tptp_user_symbol s in if decl_sym then Symtab.map_default (s, []) (insert_type thy #3 (s', T_args, T, pred_sym, length args, in_conj)) else I end | IAbs (_, tm) => add_iterm_syms tm | _ => I) #> fold add_iterm_syms args end val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms)) fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi | add_formula_var_types (AQuant (_, xs, phi)) = fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs #> add_formula_var_types phi | add_formula_var_types (AConn (_, phis)) = fold add_formula_var_types phis | add_formula_var_types _ = I fun var_types () = if is_type_enc_polymorphic type_enc then [tvar_a] else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let (* FIXME: make sure type arguments are filtered / clean up code *) val (s, s') = `(make_fixed_const NONE) \<^const_name>\undefined\ |> (is_type_enc_mangling type_enc ? mangled_const_name type_enc [T]) in Symtab.map_default (s, []) (insert_type thy #3 (s', [T], T, false, 0, false)) end fun add_TYPE_const () = let val (s, s') = TYPE_name in Symtab.map_default (s, []) (insert_type thy #3 (s', [tvar_a], \<^typ>\'a itself\, false, 0, false)) end in Symtab.empty |> is_type_enc_sound type_enc ? (fold (fold add_fact_syms) [conjs, facts] #> fold add_iterm_syms extra_tms #> (case type_enc of Native (_, _, Raw_Polymorphic phantoms, _) => phantoms = Without_Phantom_Type_Vars ? add_TYPE_const () | Native _ => I | _ => fold add_undefined_const (var_types ()))) end (* We add "bool" in case the helper "True_or_False" is included later. *) fun default_mono level completish = {maybe_finite_Ts = [\<^typ>\bool\], surely_infinite_Ts = (case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types), maybe_nonmono_Ts = [if completish >= 3 then tvar_a else \<^typ>\bool\]} (* This inference is described in section 4 of Blanchette et al., "Encoding monomorphic and polymorphic types", TACAS 2013. *) fun add_iterm_mononotonicity_info ctxt level polarity tm (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) = let val thy = Proof_Context.theory_of ctxt fun update_mono T mono = (case level of Nonmono_Types (strictness, _) => if exists (type_instance thy T) surely_infinite_Ts orelse member (type_equiv thy) maybe_finite_Ts T then mono else if is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T then {maybe_finite_Ts = maybe_finite_Ts, surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T, maybe_nonmono_Ts = maybe_nonmono_Ts} else {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T, surely_infinite_Ts = surely_infinite_Ts, maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T} | _ => mono) fun update_mono_rec (IConst ((_, s'), Type (_, [T, _]), _)) = if String.isPrefix \<^const_name>\fequal\ s' then update_mono T else I | update_mono_rec (IApp (tm1, tm2)) = fold update_mono_rec [tm1, tm2] | update_mono_rec (IAbs (_, tm)) = update_mono_rec tm | update_mono_rec _ = I in mono |> (case tm of IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2) => ((polarity <> SOME false andalso is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2]) ? update_mono T) #> fold update_mono_rec [tm1, tm2] | _ => update_mono_rec tm) end fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) = formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula fun mononotonicity_info_of_facts ctxt type_enc completish facts = let val level = level_of_type_enc type_enc in default_mono level completish |> is_type_level_monotonicity_based level ? fold (add_fact_mononotonicity_info ctxt level) facts end fun fold_arg_types f (IApp (tm1, tm2)) = fold_arg_types f tm1 #> fold_term_types f tm2 | fold_arg_types _ _ = I and fold_term_types f tm = f (ityp_of tm) #> fold_arg_types f tm fun add_iformula_monotonic_types ctxt mono type_enc = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc val should_encode = should_encode_type ctxt mono level fun add_type T = not (should_encode T) ? insert_type thy I T in formula_fold NONE (K (fold_term_types add_type)) end fun add_fact_monotonic_types ctxt mono type_enc = ifact_lift (add_iformula_monotonic_types ctxt mono type_enc) fun monotonic_types_of_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in [] |> (is_type_enc_polymorphic type_enc andalso is_type_level_monotonicity_based level) ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end fun line_of_guards_mono_type ctxt generate_info mono type_enc T = Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, IConst (`make_bound_var "X", T, []) |> type_guard_iterm type_enc T |> AAtom |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), NONE, isabelle_info generate_info inductiveN helper_rank) fun line_of_tags_mono_type ctxt generate_info mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, NONE, isabelle_info generate_info non_rec_defN helper_rank) end fun lines_of_mono_types ctxt generate_info mono type_enc = (case type_enc of Native _ => K [] | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc) | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc)) fun decl_line_of_sym ctxt type_enc s (s', T_args, T, pred_sym, ary, _) = let val thy = Proof_Context.theory_of ctxt val (T, T_args) = if null T_args then (T, []) else (case unprefix_and_unascii const_prefix s of SOME s' => let val s' = s' |> unmangled_invert_const val T = s' |> robust_const_type thy in (T, robust_const_type_args thy (s', T)) end | NONE => raise Fail "unexpected type arguments") in Sym_Decl (sym_decl_prefix ^ s, (s, s'), T |> native_atp_type_of_typ type_enc pred_sym ary |> not (null T_args) ? curry APi (map (tvar_name o dest_TVar) T_args)) end fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt val (role, maybe_negate) = honor_conj_sym_role in_conj val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, [])) val bound_Ts = (case level_of_type_enc type_enc of All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts | Undercover_Types => let val cover = type_arg_cover thy NONE s ary in map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts end | _ => replicate ary NONE) in Formula ((guards_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else ""), ""), role, IConst ((s, s'), T, T_args) |> fold (curry (IApp o swap)) bounds |> type_guard_iterm type_enc res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, NONE, isabelle_info generate_info inductiveN helper_rank) end fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc val ident = tags_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") val (role, maybe_negate) = honor_conj_sym_role in_conj val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names |> map (fn name => ATerm ((name, []), [])) val cst = mk_aterm type_enc (s, s') T_args val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE, isabelle_info generate_info non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] else if level = Undercover_Types then let val cover = type_arg_cover thy NONE s ary fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts) in formula (cst bounds) end else formula (cst bounds) end fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) = let val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, \<^sort>\type\)) in if forall (type_generalization thy T o result_type_of_decl) decls' then [decl] else decls end | rationalize_decls _ decls = decls fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) = (case type_enc of Native _ => [decl_line_of_sym ctxt type_enc s (hd decls)] | Guards (_, level) => let val thy = Proof_Context.theory_of ctxt val decls = decls |> rationalize_decls thy val n = length decls val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl) in (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s) end | Tags (_, level) => if is_type_level_uniform level then [] else let val n = length decls in (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s) end) fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab = let val syms = sym_decl_tab |> Symtab.dest |> sort_by fst val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms in mono_lines @ decl_lines end fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases sym_tab = if is_type_enc_polymorphic type_enc then let val thy = Proof_Context.theory_of ctxt fun do_ctr (s, T) = let val s' = make_fixed_const (SOME type_enc) s val ary = ary_of T fun mk name = SOME (mk_aterm type_enc name (robust_const_type_args thy (s, T)) []) in if T = HOLogic.boolT then (case proxify_const s' of SOME proxy_base => mk (proxy_base |>> prefix const_prefix) | NONE => NONE) else (case Symtab.lookup sym_tab s' of NONE => NONE | SOME ({min_ary, ...} : sym_info) => if ary = min_ary then mk (s', s) else if uncurried_aliases then mk (aliased_uncurried ary (s', s)) else NONE) end fun datatype_of_ctrs (ctrs as (_, T1) :: _) = let val ctrs' = map do_ctr ctrs in (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs', forall is_some ctrs') end in ctrss |> map datatype_of_ctrs |> filter #3 end else [] | datatypes_of_sym_table _ _ _ _ _ _ = [] fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs, exhaust) = let val xs = map (fn AType ((name, _), []) => name) ty_args in Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust) end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0 types in_conj = let fun do_alias ary = let val thy = Proof_Context.theory_of ctxt val (role, maybe_negate) = honor_conj_sym_role in_conj val base_name = base_s0 |> `(make_fixed_const (SOME type_enc)) val T = (case types of [T] => T | _ => robust_const_type thy base_s0) val T_args = robust_const_type_args thy (base_s0, T) val (base_name as (base_s, _), T_args) = mangle_type_args_in_const type_enc base_name T_args val base_ary = min_ary_of sym_tab0 base_s fun do_const name = IConst (name, T, T_args) val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc val atp_term_of = atp_term_of_iterm ctxt mono type_enc (SOME true) val name1 as (s1, _) = base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) val name2 as (s2, _) = base_name |> aliased_uncurried ary val (arg_Ts, _) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names ~~ arg_Ts val (first_bounds, last_bound) = bounds |> map (fn (name, T) => IConst (name, T, [])) |> split_last val tm1 = mk_app_op type_enc (list_app (do_const name1) first_bounds) last_bound |> filter_ty_args val tm2 = list_app (do_const name2) (first_bounds @ [last_bound]) |> filter_ty_args val eq = eq_formula type_enc (atomic_types_of T) (map (apsnd (do_bound_type type_enc)) bounds) false (atp_term_of tm1) (atp_term_of tm2) in ([tm1, tm2], [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE, isabelle_info generate_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end in do_alias end fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = (case unprefix_and_unascii const_prefix s of SOME mangled_s => if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_invert_const in do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], [])) fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab) sym_tab val implicit_declsN = "Could-be-implicit typings" val explicit_declsN = "Explicit typings" val uncurried_alias_eqsN = "Uncurried aliases" val factsN = "Relevant facts" val subclassesN = "Subclasses" val tconsN = "Type constructors" val helpersN = "Helper facts" val conjsN = "Conjectures" val free_typesN = "Free types" (* TFF allows implicit declarations of types, function symbols, and predicate symbols (with "$i" as the type of individuals), but some provers (e.g., SNARK) require explicit declarations. The situation is similar for THF. *) fun default_type pred_sym = let fun typ 0 0 = if pred_sym then bool_atype else individual_atype | typ 0 tm_ary = AFun (individual_atype, typ 0 (tm_ary - 1)) | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary) in typ end fun undeclared_in_problem problem = let fun do_sym (name as (s, _)) value = if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I fun do_class name = apfst (apfst (do_sym name ())) val do_bound_tvars = fold do_class o snd fun do_type (AType ((name, _), tys)) = apfst (apsnd (do_sym name (length tys))) #> fold do_type tys | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 | do_type (APi (_, ty)) = do_type ty fun do_term pred_sym (ATerm ((name, tys), tms)) = apsnd (do_sym name (fn _ => default_type pred_sym (length tys) (length tms))) #> fold do_type tys #> fold (do_term false) tms | do_term _ (AAbs (((_, ty), tm), args)) = do_type ty #> do_term false tm #> fold (do_term false) args fun do_formula (ATyQuant (_, xs, phi)) = fold (do_type o fst) xs #> fold (fold do_class o snd) xs #> do_formula phi | do_formula (AQuant (_, xs, phi)) = fold do_type (map_filter snd xs) #> do_formula phi | do_formula (AConn (_, phis)) = fold do_formula phis | do_formula (AAtom tm) = do_term true tm fun do_line (Class_Decl (_, _, cls)) = fold do_class cls | do_line (Type_Decl _) = I | do_line (Sym_Decl (_, _, ty)) = do_type ty | do_line (Datatype_Decl (_, xs, ty, tms, _)) = fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms | do_line (Class_Memb (_, xs, ty, cl)) = fold do_bound_tvars xs #> do_type ty #> do_class cl | do_line (Formula (_, _, phi, _, _)) = do_formula phi val ((cls, tys), syms) = declared_in_atp_problem problem in ((Symtab.empty, Symtab.empty), Symtab.empty) |>> apfst (fold (fn (s, _) => Symtab.default (s, (("", ""), ()))) cls) |>> apsnd (fold (fn (s, _) => Symtab.default (s, (("", ""), 0))) tys) ||> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype))) syms |> fold (fold do_line o snd) problem end fun declare_undeclared_in_problem heading problem = let val ((cls, tys), syms) = undeclared_in_problem problem val decls = Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) | (s, (cls, ())) => cons (Class_Decl (class_decl_prefix ^ s, cls, []))) cls [] @ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) | (s, (ty, ary)) => cons (Type_Decl (type_decl_prefix ^ s, ty, ary))) tys [] @ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) | (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms [] in (heading, decls) :: problem end val all_ctrss_of_datatypes = map (map_filter (try dest_Const) o #ctrs) o Ctr_Sugar.ctr_sugars_of val app_op_and_predicator_threshold = 45 fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans uncurried_aliases readable_names presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt val type_enc = type_enc |> adjust_type_enc format val completish = (case mode of Sledgehammer_Completish k => k | _ => 0) (* Forcing explicit applications is expensive for polymorphic encodings, because it takes only one existential variable ranging over "'a => 'b" to ruin everything. Hence we do it only if there are few facts (which is normally the case for "metis" and the minimizer). *) val app_op_level = if completish > 0 then Full_App_Op_And_Predicator else if length facts + length hyp_ts >= app_op_and_predicator_threshold then if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op else Sufficient_App_Op_And_Predicator val lam_trans = - if lam_trans = keep_lamsN andalso not (is_type_enc_higher_order type_enc) then liftingN + if lam_trans = keep_lamsN andalso not (is_type_enc_full_higher_order type_enc) then liftingN else lam_trans val (classes, conjs, facts, subclass_pairs, tcon_clauses, lifted) = translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish val ctrss = all_ctrss_of_datatypes ctxt fun firstorderize in_helper = firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish sym_tab0 val (conjs, facts) = (conjs, facts) |> apply2 (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) uncurried_alias_eq_tms val helpers = sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish |> map (firstorderize true) val all_facts = helpers @ conjs @ facts val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts val datatypes = datatypes_of_sym_table ctxt ctrss format type_enc uncurried_aliases sym_tab val class_decl_lines = decl_lines_of_classes type_enc classes val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) |> sym_decl_table_of_facts thy type_enc sym_tab |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts val datatype_decl_lines = map decl_line_of_datatype datatypes val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines val num_facts = length facts val freshen = mode <> Exporter andalso mode <> Translator val pos = mode <> Exporter val rank_of = rank_of_fact_num num_facts val fact_lines = map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of) (0 upto num_facts - 1 ~~ facts) val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc (K default_rank)) val free_type_lines = lines_of_free_types type_enc (facts @ conjs) val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) val problem = [(explicit_declsN, decl_lines), (uncurried_alias_eqsN, uncurried_alias_eq_lines), (factsN, fact_lines), (subclassesN, subclass_lines), (tconsN, tcon_lines), (helpersN, helper_lines), (free_typesN, free_type_lines), (conjsN, conj_lines)] val problem = problem |> (case format of CNF => ensure_cnf_problem | CNF_UEQ => filter_cnf_ueq_problem | FOF => I | _ => declare_undeclared_in_problem implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names format fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary) in (problem, Option.map snd pool |> the_default Symtab.empty, lifted, Symtab.fold add_sym_ary sym_tab Symtab.empty) end (* FUDGE *) val conj_weight = 0.0 val hyp_weight = 0.1 val fact_min_weight = 0.2 val fact_max_weight = 1.0 val type_info_default_weight = 0.8 (* Weights are from 0.0 (most important) to 1.0 (least important). *) fun atp_problem_selection_weights problem = let fun add_term_weights weight (ATerm ((s, _), tms)) = is_tptp_user_symbol s ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms | add_term_weights weight (AAbs ((_, tm), args)) = add_term_weights weight tm #> fold (add_term_weights weight) args fun add_line_weights weight (Formula (_, _, phi, _, _)) = formula_fold NONE (K (add_term_weights weight)) phi | add_line_weights _ _ = I fun add_conjectures_weights [] = I | add_conjectures_weights conjs = let val (hyps, conj) = split_last conjs in add_line_weights conj_weight conj #> fold (add_line_weights hyp_weight) hyps end fun add_facts_weights facts = let val num_facts = length facts fun weight_of j = fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j / Real.fromInt num_facts in map weight_of (0 upto num_facts - 1) ~~ facts |> fold (uncurry add_line_weights) end val get = these o AList.lookup (op =) problem in Symtab.empty |> add_conjectures_weights (get free_typesN @ get conjsN) |> add_facts_weights (get factsN) |> fold (fold (add_line_weights type_info_default_weight) o get) [explicit_declsN, subclassesN, tconsN] |> Symtab.dest |> sort (prod_ord Real.compare string_ord o apply2 swap) end (* Ugly hack: may make innocent victims (collateral damage) *) fun may_be_app s args = String.isPrefix app_op_name s andalso length args = 2 fun may_be_predicator s = member (op =) [predicator_name, prefixed_predicator_name] s fun strip_predicator (tm as ATerm ((s, _), [tm'])) = if may_be_predicator s then tm' else tm | strip_predicator tm = tm fun make_head_roll (ATerm ((s, _), tms)) = if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms) else (s, tms) | make_head_roll _ = ("", []) fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi | strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis | strip_up_to_predicator (AAtom tm) = [strip_predicator tm] fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi | strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) = strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1) | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi)) fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi | strip_iff_etc (AConn (AIff, [phi1, phi2])) = apply2 strip_up_to_predicator (phi1, phi2) | strip_iff_etc _ = ([], []) val max_term_order_weight = 2147483647 fun atp_problem_term_order_info problem = let fun add_edge s s' = Graph.default_node (s, ()) #> Graph.default_node (s', ()) #> Graph.add_edge_acyclic (s, s') fun add_term_deps head (ATerm ((s, _), args)) = if is_tptp_user_symbol head then (if is_tptp_user_symbol s then perhaps (try (add_edge s head)) else I) #> fold (add_term_deps head) args else I | add_term_deps head (AAbs ((_, tm), args)) = add_term_deps head tm #> fold (add_term_deps head) args fun add_intro_deps pred (Formula (_, role, phi, _, info)) = if pred (role, info) then let val (hyps, concl) = strip_ahorn_etc phi in (case make_head_roll concl of (head, args as _ :: _) => fold (add_term_deps head) (hyps @ args) | _ => I) end else I | add_intro_deps _ _ = I fun add_atom_eq_deps (SOME true) (ATerm ((s, _), [lhs as _, rhs])) = if is_tptp_equal s then (case make_head_roll lhs of (head, args as _ :: _) => fold (add_term_deps head) (rhs :: args) | _ => I) else I | add_atom_eq_deps _ _ = I fun add_eq_deps pred (Formula (_, role, phi, _, info)) = if pred (role, info) then (case strip_iff_etc phi of ([lhs], rhs) => (case make_head_roll lhs of (head, args as _ :: _) => fold (add_term_deps head) (rhs @ args) | _ => I) | _ => formula_fold (SOME (role <> Conjecture)) add_atom_eq_deps phi) else I | add_eq_deps _ _ = I fun has_status status (_, info) = extract_isabelle_status info = SOME status fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis) val graph = Graph.empty |> fold (fold (add_eq_deps (has_status non_rec_defN)) o snd) problem |> fold (fold (add_eq_deps (has_status rec_defN orf has_status simpN orf is_conj)) o snd) problem |> fold (fold (add_intro_deps (has_status inductiveN)) o snd) problem |> fold (fold (add_intro_deps (has_status introN)) o snd) problem fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1 fun add_weights _ [] = I | add_weights weight syms = fold (AList.update (op =) o rpair weight) syms #> add_weights (next_weight weight) (fold (union (op =) o Graph.immediate_succs graph) syms []) in (* Sorting is not just for aesthetics: It specifies the precedence order for the term ordering (KBO or LPO), from smaller to larger values. *) [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o apply2 snd) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML @@ -1,726 +1,726 @@ (* Title: HOL/Tools/ATP/atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature SLEDGEHAMMER_ATP_SYSTEMS = sig type term_order = ATP_Problem.term_order type atp_format = ATP_Problem.atp_format type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : bool -> string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} val default_max_mono_iters : int val default_max_new_mono_instances : int val force_sos : bool Config.T val term_order : string Config.T val e_smartN : string val e_autoN : string val e_fun_weightN : string val e_sym_offset_weightN : string val e_selection_heuristic : string Config.T val e_default_fun_weight : real Config.T val e_fun_weight_base : real Config.T val e_fun_weight_span : real Config.T val e_default_sym_offs_weight : real Config.T val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T val spass_H1SOS : string val spass_H2 : string val spass_H2LR0LT0 : string val spass_H2NuVS0 : string val spass_H2NuVS0Red2 : string val spass_H2SOS : string val is_vampire_noncommercial_license_accepted : unit -> bool option val remote_atp : string -> string -> string list -> (string * string) list -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config) val add_atp : string * (unit -> atp_config) -> theory -> theory val get_atp : theory -> string -> (unit -> atp_config) val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val effective_term_order : Proof.context -> string -> term_order end; structure Sledgehammer_ATP_Systems : SLEDGEHAMMER_ATP_SYSTEMS = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate (* ATP configuration *) val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) type slice_spec = (int * string) * atp_format * string * string * bool type atp_config = {exec : bool -> string list * string list, arguments : Proof.context -> bool -> string -> Time.time -> string -> term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string, proof_delims : (string * string) list, known_failures : (atp_failure * string) list, prem_role : atp_formula_role, best_slices : Proof.context -> (real * (slice_spec * string)) list, best_max_mono_iters : int, best_max_new_mono_instances : int} (* "best_slices" must be found empirically, taking a holistic approach since the ATPs are run in parallel. Each slice has the format (time_frac, ((max_facts, fact_filter), format, type_enc, lam_trans, uncurried_aliases), extra) where time_frac = faction of the time available given to the slice (which should add up to 1.0) extra = extra information to the prover (e.g., SOS or no SOS). The last slice should be the most "normal" one, because it will get all the time available if the other slices fail early and also because it is used if slicing is disabled (e.g., by the minimizer). *) val mepoN = "mepo" val mashN = "mash" val meshN = "mesh" val tstp_proof_delims = [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation"), ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")] val known_perl_failures = [(CantConnect, "HTTP error"), (NoPerl, "env: perl"), (NoLibwwwPerl, "Can't locate HTTP")] fun known_szs_failures wrap = [(Unprovable, wrap "CounterSatisfiable"), (Unprovable, wrap "Satisfiable"), (GaveUp, wrap "GaveUp"), (GaveUp, wrap "Unknown"), (GaveUp, wrap "Incomplete"), (ProofMissing, wrap "Theorem"), (ProofMissing, wrap "Unsatisfiable"), (TimedOut, wrap "Timeout"), (Inappropriate, wrap "Inappropriate"), (OutOfResources, wrap "ResourceOut"), (OutOfResources, wrap "MemoryOut"), (Interrupted, wrap "Forced"), (Interrupted, wrap "User")] val known_szs_status_failures = known_szs_failures (prefix "SZS status ") val known_says_failures = known_szs_failures (prefix " says ") structure Data = Theory_Data ( type T = ((unit -> atp_config) * stamp) Symtab.table val empty = Symtab.empty val extend = I fun merge data : T = Symtab.merge (eq_snd (op =)) data handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) ) fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) val sosN = "sos" val no_sosN = "no_sos" val force_sos = Attrib.setup_config_bool \<^binding>\atp_force_sos\ (K false) val smartN = "smart" (* val kboN = "kbo" *) val lpoN = "lpo" val xweightsN = "_weights" val xprecN = "_prec" val xsimpN = "_simp" (* SPASS-specific *) (* Possible values for "atp_term_order": "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *) val term_order = Attrib.setup_config_string \<^binding>\atp_term_order\ (K smartN) (* agsyHOL *) val agsyhol_config : atp_config = {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val agsyhol = (agsyholN, fn () => agsyhol_config) (* Alt-Ergo *) val alt_ergo_config : atp_config = {exec = K (["WHY3_HOME"], ["why3"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [], known_failures = [(ProofMissing, ": Valid"), (TimedOut, ": Timeout"), (GaveUp, ": Unknown")], prem_role = Hypothesis, best_slices = fn _ => (* FUDGE *) [(1.0, (((100, ""), TFF (Without_FOOL, Polymorphic), "poly_native", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val alt_ergo = (alt_ergoN, fn () => alt_ergo_config) (* E *) val e_smartN = "smart" val e_autoN = "auto" val e_fun_weightN = "fun_weight" val e_sym_offset_weightN = "sym_offset_weight" val e_selection_heuristic = Attrib.setup_config_string \<^binding>\atp_e_selection_heuristic\ (K e_smartN) (* FUDGE *) val e_default_fun_weight = Attrib.setup_config_real \<^binding>\atp_e_default_fun_weight\ (K 20.0) val e_fun_weight_base = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_base\ (K 0.0) val e_fun_weight_span = Attrib.setup_config_real \<^binding>\atp_e_fun_weight_span\ (K 40.0) val e_default_sym_offs_weight = Attrib.setup_config_real \<^binding>\atp_e_default_sym_offs_weight\ (K 1.0) val e_sym_offs_weight_base = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_base\ (K ~20.0) val e_sym_offs_weight_span = Attrib.setup_config_real \<^binding>\atp_e_sym_offs_weight_span\ (K 60.0) fun e_selection_heuristic_case heuristic fw sow = if heuristic = e_fun_weightN then fw else if heuristic = e_sym_offset_weightN then sow else raise Fail ("unexpected " ^ quote heuristic) fun scaled_e_selection_weight ctxt heuristic w = w * Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_span e_sym_offs_weight_span) + Config.get ctxt (e_selection_heuristic_case heuristic e_fun_weight_base e_sym_offs_weight_base) |> Real.ceil |> signed_string_of_int fun e_selection_weight_arguments ctxt heuristic sel_weights = if heuristic = e_fun_weightN orelse heuristic = e_sym_offset_weightN then (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS," ^ (e_selection_heuristic_case heuristic e_default_fun_weight e_default_sym_offs_weight |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^ ",20,1.5,1.5,1" ^ (sel_weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_selection_weight ctxt heuristic w) |> implode) ^ "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ \FIFOWeight(PreferProcessed))' " else "-xAuto " val e_ord_weights = map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode "," fun e_ord_precedence [_] = "" | e_ord_precedence info = info |> map fst |> space_implode "<" fun e_term_order_info_arguments false false _ = "" | e_term_order_info_arguments gen_weights gen_prec ord_info = let val ord_info = ord_info () in (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' " else "") ^ (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' " else "") end val e_config : atp_config = {exec = fn _ => (["E_HOME"], ["eprover"]), arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--auto-schedule --tstp-in --tstp-out --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ file_name, proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ known_szs_status_failures, prem_role = Conjecture, best_slices = fn ctxt => let val heuristic = Config.get ctxt e_selection_heuristic val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS val (format, enc) = if modern then - (THF (With_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher") + (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher") else (TFF (Without_FOOL, Monomorphic), "mono_native") in (* FUDGE *) if heuristic = e_smartN then [(0.15, (((128, meshN), format, enc, combsN, false), e_fun_weightN)), (0.15, (((128, mashN), format, enc, combsN, false), e_sym_offset_weightN)), (0.15, (((91, mepoN), format, enc, combsN, false), e_autoN)), (0.15, (((1000, meshN), format, "poly_guards??", combsN, false), e_sym_offset_weightN)), (0.15, (((256, mepoN), format, enc, liftingN, false), e_fun_weightN)), (0.25, (((64, mashN), format, enc, combsN, false), e_fun_weightN))] else [(1.0, (((500, ""), format, enc, combsN, false), heuristic))] end, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e = (eN, fn () => e_config) (* iProver *) val iprover_config : atp_config = {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$E_HOME\"/eprover " ^ "--clausifier_options \"--tstp-format --silent --cnf\" " ^ "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(ProofIncomplete, "% SZS output start CNFRefutation")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), FOF, "mono_guards??", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val iprover = (iproverN, fn () => iprover_config) (* LEO-II *) val leo2_config : atp_config = {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => "--foatp e --atp e=\"$E_HOME\"/eprover \ \--atp epclextract=\"$E_HOME\"/epclextract \ \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^ file_name, proof_delims = tstp_proof_delims, known_failures = [(TimedOut, "CPU time limit exceeded, terminating"), (GaveUp, "No.of.Axioms")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo2 = (leo2N, fn () => leo2_config) (* Leo-III *) (* Include choice? Disabled now since it's disabled for Satallax as well. *) val leo3_config : atp_config = {exec = K (["LEO3_HOME"], ["leo3"]), arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \ \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ (if full_proofs then "--nleq --naeq " else ""), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val leo3 = (leo3N, fn () => leo3_config) (* Satallax *) (* Choice is disabled until there is proper reconstruction for it. *) val satallax_config : atp_config = {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => (case getenv "E_HOME" of "" => "" | home => "-E " ^ home ^ "/eprover ") ^ "-p tstp -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("% SZS output start Proof", "% SZS output end Proof")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((150, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} val satallax = (satallaxN, fn () => satallax_config) (* SPASS *) val spass_H1SOS = "-Heuristic=1 -SOS" val spass_H2 = "-Heuristic=2" val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0" val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0" val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" val spass_H2SOS = "-Heuristic=2 -SOS" val spass_config : atp_config = {exec = K (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = [(GaveUp, "SPASS beiseite: Completion found"), (TimedOut, "SPASS beiseite: Ran out of time"), (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), (InternalError, "Please report this error")] @ known_perl_failures, prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")), (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)), (0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)), (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)), (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val spass = (spassN, fn () => spass_config) (* Vampire *) fun is_vampire_noncommercial_license_accepted () = let val flag = Options.default_string \<^system_option>\vampire_noncommercial\ |> String.map Char.toLower in if flag = "yes" then SOME true else if flag = "no" then SOME false else NONE end fun check_vampire_noncommercial () = (case is_vampire_noncommercial_license_accepted () of SOME true => () | SOME false => error (Pretty.string_of (Pretty.para "The Vampire prover may be used only for noncommercial applications")) | NONE => error (Pretty.string_of (Pretty.para "The Vampire prover is not activated; to activate it, set the Isabelle system option \ \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \ \/ Isabelle / General)"))) val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS" val vampire_full_proof_options = " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0" val remote_vampire_command = "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s" val vampire_config : atp_config = {exec = K (["VAMPIRE_HOME"], ["vampire"]), arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ => (check_vampire_noncommercial (); vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name |> sos = sosN ? prefix "--sos on "), proof_delims = [("=========== Refutation ==========", "======= End of refutation =======")] @ tstp_proof_delims, known_failures = [(GaveUp, "UNPROVABLE"), (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), (Interrupted, "Aborted by signal SIGINT")] @ known_szs_status_failures, prem_role = Hypothesis, best_slices = fn ctxt => (* FUDGE *) [(0.333, (((500, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), sosN)), (0.333, (((150, meshN), TFF (Without_FOOL, Monomorphic), "poly_tags??", combs_or_liftingN, false), sosN)), (0.334, (((50, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), no_sosN))] |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single), best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val vampire = (vampireN, fn () => vampire_config) (* Z3 with TPTP syntax (half experimental, half legacy) *) val z3_tptp_config : atp_config = {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name, proof_delims = [("SZS status Theorem", "")], known_failures = known_szs_status_failures, prem_role = Hypothesis, best_slices = (* FUDGE *) K [(0.5, (((250, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), (0.25, (((125, mepoN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), (0.125, (((62, mashN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")), (0.125, (((31, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) (* Zipperposition *) val zipperposition_blsimp = "--mode ho-pragmatic --max-inferences 3 --ho-max-app-projections 0 --ho-max-elims 0 --ho-max-rigid-imitations 2 --ho-max-identifications 0 --ho-unif-max-depth 2 --boolean-reasoning no-cases --ext-rules ext-family --ext-rules-max-depth 1 --kbo-weight-fun invdocc --ho-prim-enum tf --ho-prim-enum-early-bird true --tptp-def-as-rewrite --ho-unif-level pragmatic-framework -q '1|const|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)' -q '1|prefer-sos|staggered(1)' -q '2|prefer-fo|default' -q '1|prefer-neg-unit|orient-lmax(2,1,2,1,1)' -q '2|prefer-easy-ho|conjecture-relative-struct(1.5,3.5,2,3)' --ho-elim-leibniz 2 --ho-fixpoint-decider true --ho-pattern-decider false --ho-solid-decider true --ho-max-solidification 12 --select e-selection11 --solve-formulas true --sup-at-vars false --sup-at-var-headed false --lazy-cnf true --lazy-cnf-kind simp --lazy-cnf-renaming-threshold 4 --sine 50 --sine-tolerance 1.7 --sine-depth-max 3 --sine-depth-min 1 --sine-trim-implications true --ho-selection-restriction none --sup-from-var-headed false --sine-trim-implications true" val zipperposition_s6 = "--tptp-def-as-rewrite --rewrite-before-cnf true --mode ho-competitive --boolean-reasoning no-cases --ext-rules off --ho-prim-enum none --recognize-injectivity true --ho-elim-leibniz off --ho-unif-level full-framework --no-max-vars -q '3|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-ho-steps|conjecture-relative-var(1,s,f)' -q '1|prefer-processed|fifo' -q '3|by-app-var-num|pnrefined(2,1,1,1,2,2,2)' --select ho-selection5 --prec-gen-fun unary_first --solid-subsumption false --ignore-orphans false --ho-solid-decider true --ho-fixpoint-decider true --ho-pattern-decider true --sup-at-vars false --sup-at-var-headed false --sup-from-var-headed false --ho-neg-ext-simpl true" val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -q '6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)' -q '6|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-processed|fifo' -q '1|prefer-non-goals|conjecture-relative-var(1,l,f)' -q '4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)' --select e-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank" val zipperposition_config : atp_config = {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ => "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name |> extra_options <> "" ? prefix (extra_options ^ " "), proof_delims = tstp_proof_delims, known_failures = known_szs_status_failures, prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) [(0.333, (((128, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)), (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)), (0.334, (((512, "meshN"), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val zipperposition = (zipperpositionN, fn () => zipperposition_config) (* Remote ATP invocation via SystemOnTPTP *) val remote_systems = Synchronized.var "atp_remote_systems" ([] : string list) fun get_remote_systems () = Timeout.apply (seconds 10.0) (fn () => (case Isabelle_System.bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of (output, 0) => split_lines output | (output, _) => (warning (case extract_known_atp_failure known_perl_failures output of SOME failure => string_of_atp_failure failure | NONE => trim_line output); []))) () handle Timeout.TIMEOUT _ => [] fun find_remote_system name [] systems = find_first (String.isPrefix (name ^ "---")) systems | find_remote_system name (version :: versions) systems = case find_first (String.isPrefix (name ^ "---" ^ version)) systems of NONE => find_remote_system name versions systems | res => res fun get_remote_system name versions = Synchronized.change_result remote_systems (fn systems => (if null systems then get_remote_systems () else systems) |> `(`(find_remote_system name versions))) fun the_remote_system name versions = (case get_remote_system name versions of (SOME sys, _) => sys | (NONE, []) => error "SystemOnTPTP is currently not available" | (NONE, syss) => (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of [] => error "SystemOnTPTP is currently not available" | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) | syss => error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *) fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice = {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]), arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ => (if command <> "" then "-c " ^ quote command ^ " " else "") ^ "-s " ^ the_remote_system system_name system_versions ^ " " ^ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ " " ^ file_name, proof_delims = union (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ known_says_failures, prem_role = prem_role, best_slices = fn ctxt => [(1.0, best_slice ctxt)], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} : atp_config fun remotify_config system_name system_versions best_slice ({proof_delims, known_failures, prem_role, ...} : atp_config) = remote_config system_name system_versions proof_delims known_failures prem_role best_slice fun remote_atp name system_name system_versions proof_delims known_failures prem_role best_slice = (remote_prefix ^ name, fn () => remote_config system_name system_versions proof_delims known_failures prem_role best_slice) fun remotify_atp (name, config) system_name system_versions best_slice = (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) fun gen_remote_waldmeister name type_enc = remote_atp name "Waldmeister" ["710"] tstp_proof_delims ([(OutOfResources, "Too many function symbols"), (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis (K (((50, ""), CNF_UEQ, type_enc, combsN, false), "") (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K (((60, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] (K (((250, ""), TFF (Without_FOOL, Polymorphic), "poly_native", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K (((750, ""), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K (((40, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", liftingN, false), "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K (((150, ""), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["THF-4.4"] (K (((400, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), remote_vampire_command) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.0"] (K (((512, ""), THF (Without_FOOL, Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) (* Dummy prover *) fun dummy_config prem_role format type_enc uncurried_aliases : atp_config = {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]), arguments = K (K (K (K (K (K ""))))), proof_delims = [], known_failures = known_szs_status_failures, prem_role = prem_role, best_slices = K [(1.0, (((200, ""), format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val dummy_tfx_format = TFF (With_FOOL, Polymorphic) val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config) (* Setup *) fun add_atp (name, config) thy = Data.map (Symtab.update_new (name, (config, stamp ()))) thy handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) fun get_atp thy name = fst (the (Symtab.lookup (Data.get thy) name)) handle Option.Option => error ("Unknown ATP: " ^ name) val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = let val {exec, ...} = get_atp thy name () in exists (fn var => getenv var <> "") (fst (exec false)) end fun refresh_systems_on_tptp () = Synchronized.change remote_systems (fn _ => get_remote_systems ()) fun effective_term_order ctxt atp = let val ord = Config.get ctxt term_order in if ord = smartN then {is_lpo = false, gen_weights = (atp = spassN), gen_prec = (atp = spassN), gen_simp = false} else let val is_lpo = String.isSubstring lpoN ord in {is_lpo = is_lpo, gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, gen_prec = String.isSubstring xprecN ord, gen_simp = String.isSubstring xsimpN ord} end end val atps = [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3, remote_vampire, remote_waldmeister, remote_zipperposition, dummy_tfx] val _ = Theory.setup (fold add_atp atps) end;