diff --git a/src/HOL/ATP.thy b/src/HOL/ATP.thy --- a/src/HOL/ATP.thy +++ b/src/HOL/ATP.thy @@ -1,158 +1,142 @@ (* Title: HOL/ATP.thy Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen *) section \Automatic Theorem Provers (ATPs)\ theory ATP imports Meson begin subsection \ATP problems and proofs\ ML_file \Tools/ATP/atp_util.ML\ ML_file \Tools/ATP/atp_problem.ML\ ML_file \Tools/ATP/atp_proof.ML\ ML_file \Tools/ATP/atp_proof_redirect.ML\ ML_file \Tools/ATP/atp_satallax.ML\ subsection \Higher-order reasoning helpers\ definition fFalse :: bool where "fFalse \ False" definition fTrue :: bool where "fTrue \ True" definition fNot :: "bool \ bool" where "fNot P \ \ P" definition fComp :: "('a \ bool) \ 'a \ bool" where "fComp P = (\x. \ P x)" definition fconj :: "bool \ bool \ bool" where "fconj P Q \ P \ Q" definition fdisj :: "bool \ bool \ bool" where "fdisj P Q \ P \ Q" definition fimplies :: "bool \ bool \ bool" where "fimplies P Q \ (P \ Q)" definition fAll :: "('a \ bool) \ bool" where "fAll P \ All P" definition fEx :: "('a \ bool) \ bool" where "fEx P \ Ex P" definition fequal :: "'a \ 'a \ bool" where "fequal x y \ (x = y)" lemma fTrue_ne_fFalse: "fFalse \ fTrue" unfolding fFalse_def fTrue_def by simp lemma fNot_table: "fNot fFalse = fTrue" "fNot fTrue = fFalse" unfolding fFalse_def fTrue_def fNot_def by auto lemma fconj_table: "fconj fFalse P = fFalse" "fconj P fFalse = fFalse" "fconj fTrue fTrue = fTrue" unfolding fFalse_def fTrue_def fconj_def by auto lemma fdisj_table: "fdisj fTrue P = fTrue" "fdisj P fTrue = fTrue" "fdisj fFalse fFalse = fFalse" unfolding fFalse_def fTrue_def fdisj_def by auto lemma fimplies_table: "fimplies P fTrue = fTrue" "fimplies fFalse P = fTrue" "fimplies fTrue fFalse = fFalse" unfolding fFalse_def fTrue_def fimplies_def by auto lemma fAll_table: "Ex (fComp P) \ fAll P = fTrue" "All P \ fAll P = fFalse" unfolding fFalse_def fTrue_def fComp_def fAll_def by auto lemma fEx_table: "All (fComp P) \ fEx P = fTrue" "Ex P \ fEx P = fFalse" unfolding fFalse_def fTrue_def fComp_def fEx_def by auto lemma fequal_table: "fequal x x = fTrue" "x = y \ fequal x y = fFalse" unfolding fFalse_def fTrue_def fequal_def by auto lemma fNot_law: "fNot P \ P" unfolding fNot_def by auto lemma fComp_law: "fComp P x \ \ P x" unfolding fComp_def .. lemma fconj_laws: "fconj P P \ P" "fconj P Q \ fconj Q P" "fNot (fconj P Q) \ fdisj (fNot P) (fNot Q)" unfolding fNot_def fconj_def fdisj_def by auto lemma fdisj_laws: "fdisj P P \ P" "fdisj P Q \ fdisj Q P" "fNot (fdisj P Q) \ fconj (fNot P) (fNot Q)" unfolding fNot_def fconj_def fdisj_def by auto lemma fimplies_laws: "fimplies P Q \ fdisj (\ P) Q" "fNot (fimplies P Q) \ fconj P (fNot Q)" unfolding fNot_def fconj_def fdisj_def fimplies_def by auto lemma fAll_law: "fNot (fAll R) \ fEx (fComp R)" unfolding fNot_def fComp_def fAll_def fEx_def by auto lemma fEx_law: "fNot (fEx R) \ fAll (fComp R)" unfolding fNot_def fComp_def fAll_def fEx_def by auto lemma fequal_laws: "fequal x y = fequal y x" "fequal x y = fFalse \ fequal y z = fFalse \ fequal x z = fTrue" "fequal x y = fFalse \ fequal (f x) (f y) = fTrue" unfolding fFalse_def fTrue_def fequal_def by auto -subsection \Waldmeister helpers\ - -(* Has all needed simplification lemmas for logic. *) -lemma boolean_equality: "(P \ P) = True" - by simp - -lemma boolean_comm: "(P \ Q) = (Q \ P)" - by auto - -lemmas waldmeister_fol = boolean_equality boolean_comm - simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc - - subsection \Basic connection between ATPs and HOL\ ML_file \Tools/lambda_lifting.ML\ ML_file \Tools/monomorph.ML\ ML_file \Tools/ATP/atp_problem_generate.ML\ ML_file \Tools/ATP/atp_proof_reconstruct.ML\ ML_file \Tools/ATP/atp_systems.ML\ -ML_file \Tools/ATP/atp_waldmeister.ML\ - -hide_fact (open) waldmeister_fol boolean_equality boolean_comm 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,2827 +1,2827 @@ (* 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_choice 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 * 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_Predicate_Free, _, _)) = false | is_type_enc_full_higher_order (Native (Higher_Order _, _, _)) = true | is_type_enc_full_higher_order _ = 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 = (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)))))) ||> (fn 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)))) |> (fn (poly, (level, core)) => (case (core, (poly, level)) of ("native", (SOME poly, _)) => (case (poly, level) of (Mangled_Monomorphic, _) => if is_type_level_uniform level then Native (First_Order, Mangled_Monomorphic, level) else raise Same.SAME | (Raw_Monomorphic, _) => raise Same.SAME | (poly, All_Types) => Native (First_Order, 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, Mangled_Monomorphic, level) else raise Same.SAME | (poly as Raw_Polymorphic _, All_Types) => Native (Higher_Order THF_With_Choice, poly, All_Types) | _ => raise Same.SAME) | ("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)) handle Same.SAME => error ("Unknown type encoding: " ^ quote s) fun min_hologic THF_Predicate_Free _ = THF_Predicate_Free | min_hologic _ THF_Predicate_Free = THF_Predicate_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 no_type_classes Type_Class_Polymorphic = Raw_Polymorphic With_Phantom_Type_Vars | no_type_classes poly = poly fun adjust_type_enc (THF (Polymorphic, hologic)) (Native (order, poly, level)) = Native (adjust_hologic hologic order, no_type_classes poly, level) | adjust_type_enc (THF (Monomorphic, hologic)) (Native (order, _, level)) = Native (adjust_hologic hologic order, Mangled_Monomorphic, level) | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) = Native (First_Order, poly, level) | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (TFF _) (Native (_, poly, level)) = Native (First_Order, 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 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *) val fused_infinite_type = Type (fused_infinite_type_name, []) 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_full_higher_order type_enc then `I tptp_bool_type else if s = fused_infinite_type_name andalso is_type_enc_native type_enc then `I tptp_individual_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_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 => if top_level 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") => IConst (`I tptp_not, T, []) | (false, "c_conj") => IConst (`I tptp_and, T, []) | (false, "c_disj") => IConst (`I tptp_or, T, []) | (false, "c_implies") => IConst (`I tptp_implies, T, []) | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args | (false, s) => if is_tptp_equal s then if length args = 2 then IConst (`I tptp_equal, T, []) 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 IConst (name, T, []) | _ => IConst (name, T, [])) else IConst (proxy_base |>> prefix const_prefix, T, T_args) | 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_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_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 fun fused_type ctxt mono level = let val should_encode = should_encode_type ctxt mono level fun fuse 0 T = if should_encode T then T else fused_infinite_type | fuse ary (Type (\<^type_name>\fun\, [T1, T2])) = fuse 0 T1 --> fuse (ary - 1) T2 | fuse _ _ = raise Fail "expected function type" in fuse end (** 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_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 do_iterm = (not (is_type_enc_higher_order type_enc) ? introduce_app_ops) #> (not (is_type_enc_full_higher_order type_enc) ? 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 (_, S)) => (AType ((tvar_name z, []), []), [])) Ts) + 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 ctxt mono type_enc = (case type_enc of Native (_, _, level) => fused_type ctxt mono level 0 #> 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 val do_bound_type = do_bound_type ctxt mono type_enc in AQuant (q, xs |> map (apsnd (fn NONE => NONE | SOME T => do_bound_type 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 mono 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 |> fused_type ctxt mono (level_of_type_enc type_enc) ary |> 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 mono 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 do_bound_type = do_bound_type ctxt mono type_enc val eq = eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) 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 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/ATP/atp_proof.ML b/src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML +++ b/src/HOL/Tools/ATP/atp_proof.ML @@ -1,744 +1,742 @@ (* Title: HOL/Tools/ATP/atp_proof.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Author: Mathias Fleury, ENS Rennes Abstract representation of ATP proofs and TSTP/SPASS syntax. *) signature ATP_PROOF = sig type 'a atp_type = 'a ATP_Problem.atp_type type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type atp_formula_role = ATP_Problem.atp_formula_role type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type 'a atp_problem = 'a ATP_Problem.atp_problem exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | UnsoundProof of bool * string list | CantConnect | TimedOut | Inappropriate | OutOfResources | NoPerl | NoLibwwwPerl | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string type atp_step_name = string * string list type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list (* Named ATPs *) val agsyholN : string val alt_ergoN : string val dummy_thfN : string val dummy_thf_mlN : string val eN : string val e_malesN : string val e_parN : string val e_sineN : string val e_tofofN : string val ehohN : string val iproverN : string val iprover_eqN : string val leo2N : string val leo3N : string val pirateN : string val satallaxN : string val snarkN : string val spassN : string val vampireN : string val waldmeisterN : string - val waldmeister_newN : string val z3_tptpN : string val zipperpositionN : string val remote_prefix : string val agsyhol_core_rule : string val spass_input_rule : string val spass_pre_skolemize_rule : string val spass_skolemize_rule : string val z3_tptp_core_rule : string val short_output : bool -> string -> string val string_of_atp_failure : atp_failure -> string val extract_important_message : string -> string val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option val extract_tstplike_proof_and_outcome : bool -> (string * string) list -> (atp_failure * string) list -> string -> string * atp_failure option val is_same_atp_step : atp_step_name -> atp_step_name -> bool val scan_general_id : string list -> string * string list val parse_formula : string list -> (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof val skip_term: string list -> string * string list val parse_thf_formula :string list -> ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string list val dummy_atype : string ATP_Problem.atp_type val role_of_tptp_string: string -> ATP_Problem.atp_formula_role val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list -> string list -> ((string * string list) * ATP_Problem.atp_formula_role * (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string * (string * 'd list) list) list * string list val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role * ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list val vampire_step_name_ord : (string * 'a) ord val core_of_agsyhol_proof : string -> string list option end; structure ATP_Proof : ATP_PROOF = struct open ATP_Util open ATP_Problem (* Named ATPs *) val agsyholN = "agsyhol" val alt_ergoN = "alt_ergo" val dummy_thfN = "dummy_thf" (* for experiments *) val dummy_thf_mlN = "dummy_thf_ml" (* for experiments *) val eN = "e" val e_malesN = "e_males" val e_parN = "e_par" val e_sineN = "e_sine" val e_tofofN = "e_tofof" val ehohN = "ehoh" val iproverN = "iprover" val iprover_eqN = "iprover_eq" val leo2N = "leo2" val leo3N = "leo3" val pirateN = "pirate" val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" val vampireN = "vampire" val waldmeisterN = "waldmeister" -val waldmeister_newN = "waldmeister_new" val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) val spass_input_rule = "Inp" val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *) val spass_skolemize_rule = "__Sko" (* arbitrary *) val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *) exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | UnsoundProof of bool * string list | CantConnect | TimedOut | Inappropriate | OutOfResources | NoPerl | NoLibwwwPerl | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string fun short_output verbose output = if verbose then if output = "" then "No details available" else elide_string 1000 output else "" val missing_message_tail = " appears to be missing; you will need to install it if you want to invoke \ \remote provers" fun from_lemmas [] = "" | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable" | string_of_atp_failure Unprovable = "The generated problem is unprovable" | string_of_atp_failure GaveUp = "The prover gave up" | string_of_atp_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof" | string_of_atp_failure ProofIncomplete = "The prover claims the conjecture is a theorem but provided an incomplete proof" | string_of_atp_failure ProofUnparsable = "The prover claims the conjecture is a theorem but provided an unparsable proof" | string_of_atp_failure (UnsoundProof (false, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ "; specify a sound type encoding or omit the \"type_enc\" option" | string_of_atp_failure (UnsoundProof (true, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" | string_of_atp_failure CantConnect = "Cannot connect to server" | string_of_atp_failure TimedOut = "Timed out" | string_of_atp_failure Inappropriate = "The generated problem lies outside the prover's scope" | string_of_atp_failure OutOfResources = "The prover ran out of resources" | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail | string_of_atp_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail | string_of_atp_failure MalformedInput = "The generated problem is malformed" | string_of_atp_failure MalformedOutput = "The prover output is malformed" | string_of_atp_failure Interrupted = "The prover was interrupted" | string_of_atp_failure Crashed = "The prover crashed" | string_of_atp_failure InternalError = "An internal prover error occurred" | string_of_atp_failure (UnknownError s) = "A prover error occurred" ^ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = (case first_field begin_delim output of SOME (_, tail) => (case first_field "\n" tail of SOME (_, tail') => if end_delim = "" then tail' else (case first_field end_delim tail' of SOME (body, _) => body | NONE => "") | NONE => "") | NONE => "") val tstp_important_message_delims = ("% SZS start RequiredInformation", "% SZS end RequiredInformation") fun extract_important_message output = (case extract_delimited tstp_important_message_delims output of "" => "" | s => s |> space_explode "\n" |> filter_out (curry (op =) "") |> map (perhaps (try (unprefix "%"))) |> map (perhaps (try (unprefix " "))) |> space_implode "\n " |> quote) (* Splits by the first possible of a list of delimiters. *) fun extract_tstplike_proof delims output = (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output | _ => "") fun extract_known_atp_failure known_failures output = known_failures |> find_first (fn (_, pattern) => String.isSubstring pattern output) |> Option.map fst fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output = (case (extract_tstplike_proof proof_delims output, extract_known_atp_failure known_failures output) of (_, SOME ProofIncomplete) => ("", NONE) | (_, SOME ProofUnparsable) => ("", NONE) | ("", SOME ProofMissing) => ("", NONE) | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) | res as ("", _) => res | (tstplike_proof, _) => (tstplike_proof, NONE)) type atp_step_name = string * string list fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 val vampire_fact_prefix = "f" fun vampire_step_name_ord p = let val q = apply2 fst p in (* The "unprefix" part is to cope with Vampire's output. *) (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of (SOME i, SOME j) => int_ord (i, j) | _ => raise Fail "not Vampire") end type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list (**** PARSING OF TSTP FORMAT ****) (* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting with "$" and possibly with "!" in them (for "z3_tptp"). *) val scan_general_id = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) "" >> op ^ fun skip_term x = let fun skip _ accum [] = (accum, []) | skip n accum (ss as s :: ss') = if (s = "," orelse s = ".") andalso n = 0 then (accum, ss) else if member (op =) [")", "]"] s then if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' else if member (op =) ["(", "["] s then skip (n + 1) (s :: accum) ss' else skip n (s :: accum) ss' in (skip 0 [] #>> (rev #> implode)) x end and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x datatype source = File_Source of string * string option | Inference_Source of string * string list | Introduced_Source of string val dummy_phi = AAtom (ATerm (("", []), [])) val dummy_inference = Inference_Source ("", []) val dummy_atype = AType (("", []), []) (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *) fun parse_dependency x = (parse_inference_source >> snd || scan_general_id --| skip_term >> single) x and parse_dependencies x = (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency) >> (filter_out (curry (op =) "theory"))) x and parse_file_source x = (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- Scan.option ($$ "," |-- scan_general_id --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x and parse_inference_source x = (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" --| $$ ")") x and parse_introduced_source x = (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x and parse_source x = (parse_file_source >> File_Source || parse_inference_source >> Inference_Source || parse_introduced_source >> Introduced_Source || scan_general_id >> (fn s => Inference_Source ("", [s])) (* for E *) || skip_term >> K dummy_inference) x fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f fun parse_class x = scan_general_id x and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x fun parse_type x = (($$ "(" |-- parse_type --| $$ ")" || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *)) || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []) -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] >> AType) -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type) >> (fn (a, NONE) => a | (a, SOME (bin_op, b)) => if bin_op = tptp_app then (case a of AType (s_clss, tys) => AType (s_clss, tys @ [b]) | _ => raise UNRECOGNIZED_ATP_PROOF ()) else if bin_op = tptp_fun_type then AFun (a, b) else if bin_op = tptp_product_type then AType ((tptp_product_type, []), [a, b]) else raise Fail "impossible case")) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x (* We currently half ignore types. *) fun parse_optional_type_signature x = (Scan.option ($$ tptp_has_type |-- parse_type) >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some | res => res)) x and parse_arg x = ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature || scan_general_id -- parse_optional_type_signature -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> (fn (((s, ty_opt), tyargs), args) => if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then ATerm ((s, the_list ty_opt), []) else ATerm ((s, tyargs), args))) x and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) --| parse_optional_type_signature >> list_app) x and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x fun parse_atom x = (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_term) >> (fn (u1, NONE) => AAtom u1 | (u1, SOME (neg, u2)) => AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *) fun parse_literal x = ((Scan.repeat ($$ tptp_not) >> length) -- ($$ "(" |-- parse_formula --| $$ ")" || parse_quantified_formula || parse_atom) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x and parse_formula x = (parse_literal -- Scan.option ((Scan.this_string tptp_implies || Scan.this_string tptp_iff || Scan.this_string tptp_not_iff || Scan.this_string tptp_if || $$ tptp_or || $$ tptp_and) -- parse_formula) >> (fn (phi1, NONE) => phi1 | (phi1, SOME (c, phi2)) => if c = tptp_implies then mk_aconn AImplies phi1 phi2 else if c = tptp_iff then mk_aconn AIff phi1 phi2 else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2) else if c = tptp_if then mk_aconn AImplies phi2 phi1 else if c = tptp_or then mk_aconn AOr phi1 phi2 else if c = tptp_and then mk_aconn AAnd phi1 phi2 else raise Fail ("impossible connective " ^ quote c))) x and parse_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) dummy_inference val waldmeister_conjecture_name = "conjecture_1" val tofof_fact_prefix = "fof_" fun is_same_term subst tm1 tm2 = let fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2)) (SOME subst) = if typ1 <> typ2 andalso length args1 = length args2 then NONE else let val ls = length subst in SOME ((var1, var2) :: subst) |> do_term_pair body1 body2 |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst) | NONE => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) end | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) = (case apply2 is_tptp_variable (s1, s2) of (true, true) => (case AList.lookup (op =) subst s1 of SOME s2' => if s2' = s2 then SOME subst else NONE | NONE => if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst) else NONE) | (false, false) => if s1 = s2 then SOME subst else NONE | _ => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) | do_term_pair _ _ _ = NONE in SOME subst |> do_term_pair tm1 tm2 |> is_some end fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) = q1 = q2 andalso length xs1 = length xs2 andalso is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) = if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE fun find_formula_in_problem phi = maps snd #> map_filter (matching_formula_line_identifier phi) #> try (single o hd) #> the_default [] fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom | role_of_tptp_string "definition" = Definition | role_of_tptp_string "lemma" = Lemma | role_of_tptp_string "hypothesis" = Hypothesis | role_of_tptp_string "conjecture" = Conjecture | role_of_tptp_string "negated_conjecture" = Negated_Conjecture | role_of_tptp_string "plain" = Plain | role_of_tptp_string "type" = Type_Role | role_of_tptp_string _ = Unknown val tptp_binary_ops = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal, tptp_not_equal, tptp_app] fun parse_one_in_list xs = foldl1 (op ||) (map Scan.this_string xs) fun parse_binary_op x = (parse_one_in_list tptp_binary_ops >> (fn c => if c = tptp_equal then "equal" else c)) x val parse_fo_quantifier = parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the] val parse_ho_quantifier = parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the] fun mk_ho_of_fo_quant q = if q = tptp_forall then tptp_ho_forall else if q = tptp_exists then tptp_ho_exists else if q = tptp_hilbert_choice then tptp_hilbert_choice else if q = tptp_hilbert_the then tptp_hilbert_the else raise Fail ("unrecognized quantification: " ^ q) fun remove_thf_app (ATerm ((x, ty), arg)) = if x = tptp_app then (case arg of ATerm ((x, ty), arg) :: t => remove_thf_app (ATerm ((x, ty), map remove_thf_app arg @ t)) | [AAbs ((var, tvar), phi), t] => remove_thf_app (AAbs ((var, tvar), map remove_thf_app phi @ [t]))) else ATerm ((x, ty), map remove_thf_app arg) | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t) fun parse_typed_var x = (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) --| Scan.option (Scan.this_string ",")) || $$ "(" |-- parse_typed_var --| $$ ")") x fun parse_simple_thf_term x = (parse_fo_quantifier -- ($$ "[" |-- parse_typed_var --| $$ "]" --| $$ ":") -- parse_thf_term >> (fn ((q, ys), t) => fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []) |> (if tptp_lambda <> q then mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm) else I)) ys t) || Scan.this_string tptp_not |-- parse_thf_term >> mk_app (mk_simple_aterm tptp_not) || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), [])) || parse_ho_quantifier >> mk_simple_aterm || $$ "(" |-- parse_thf_term --| $$ ")" || parse_binary_op >> mk_simple_aterm) x and parse_thf_term x = (parse_simple_thf_term -- Scan.option (parse_binary_op -- parse_thf_term) >> (fn (t1, SOME (c, t2)) => if c = tptp_app then mk_app t1 t2 else mk_apps (mk_simple_aterm c) [t1, t2] | (t, NONE) => t)) x fun parse_thf_formula x = (parse_thf_term #>> remove_thf_app #>> AAtom) x fun parse_tstp_thf_line problem = (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," -- (parse_thf_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), deps) => let val role' = role_of_tptp_string role val ((name, phi), rule, deps) = (case deps of File_Source (_, SOME s) => if role' = Definition then (((num, map fst (find_formula_in_problem phi problem)), phi), "", []) else (((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), "", []) | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)) in [(name, role', phi, rule, map (rpair []) deps)] end) (* Syntax: (cnf|fof|tff|thf)\(, , \). The could be an identifier, but we assume integers. *) fun parse_tstp_line problem = ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role0), phi), src) => let val role = role_of_tptp_string role0 val ((name, phi), role', rule, deps) = (* Waldmeister isn't exactly helping. *) (case src of File_Source (_, SOME s) => (if s = waldmeister_conjecture_name then (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => ((num, [s]), phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq) | _ => ((num, []), phi)) else ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]), phi), role, "", []) | File_Source _ => (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", []) | Inference_Source (rule, deps) => (((num, []), phi), role, rule, deps) | Introduced_Source rule => (((num, []), phi), Lemma, rule, [])) fun mk_step () = (name, role', phi, rule, map (rpair []) deps) in [(case role' of Definition => (case phi of AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) | _ => mk_step ())] end) (**** PARSING OF SPASS OUTPUT ****) (* SPASS returns clause references of the form "x.y". We ignore "y". *) val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id val parse_spass_annotations = Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) [] (* We ignore the stars and the pluses that follow literals. *) fun parse_decorated_atom x = (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits) fun parse_horn_clause x = (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|" -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">" -- Scan.repeat parse_decorated_atom >> (mk_horn o apfst (op @))) x val parse_spass_debug = Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")") (* Syntax: [0:] || -> . derived from formulae * *) fun parse_spass_line x = (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." -- Scan.option (Scan.this_string "derived from formulae " |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) >> (fn ((((num, rule), deps), u), names) => [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x fun parse_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x fun parse_pirate_dependencies x = Scan.repeat (parse_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x fun parse_pirate_file_source x = ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id --| $$ ")") x fun parse_pirate_inference_source x = (scan_general_id -- ($$ "(" |-- parse_pirate_dependencies --| $$ ")")) x fun parse_pirate_source x = (parse_pirate_file_source >> (fn s => File_Source ("", SOME s)) || parse_pirate_inference_source >> Inference_Source) x (* Syntax: || -> . origin\(\) *) fun parse_pirate_line x = (scan_general_id --| Scan.repeat (~$$ "|") -- parse_horn_clause --| $$ "." --| Scan.this_string "origin" --| $$ "(" -- parse_pirate_source --| $$ ")" >> (fn ((((num, u), source))) => let val (names, rule, deps) = (case source of File_Source (_, SOME s) => ([s], spass_input_rule, []) | Inference_Source (rule, deps) => ([], rule, deps)) in [((num, names), Unknown, u, rule, map (rpair []) deps)] end)) x fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) (* Syntax: SZS core ... *) fun parse_z3_tptp_core_line x = (Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id) >> map (core_inference z3_tptp_core_rule)) x fun parse_line local_name problem = (* Satallax is handled separately, in "atp_satallax.ML". *) if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf_line problem else if local_name = spassN then parse_spass_line else if local_name = pirateN then parse_pirate_line else if local_name = z3_tptpN then parse_z3_tptp_core_line else parse_tstp_line problem fun core_of_agsyhol_proof s = (case split_lines s of "The transformed problem consists of the following conjectures:" :: conj :: _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term) | _ => NONE) fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: clean_up_dependencies (name :: seen) steps fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof fun map_term_names_in_atp_proof f = let fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys) | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts) | map_term (AAbs (((s, ty), tm), args)) = AAbs (((f s, map_type ty), map_term tm), map map_term args) fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi) | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis) | map_formula (AAtom t) = AAtom (map_term t) fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps) in map map_step end fun nasty_name pool s = Symtab.lookup pool s |> the_default s fun nasty_atp_proof pool = not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool) end; diff --git a/src/HOL/Tools/ATP/atp_systems.ML b/src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML +++ b/src/HOL/Tools/ATP/atp_systems.ML @@ -1,843 +1,842 @@ (* Title: HOL/Tools/ATP/atp_systems.ML Author: Fabian Immler, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Setup for supported ATPs. *) signature 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 spass_extra_options : string Config.T 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 ATP_Systems : 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 wholistic 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_thf0 = THF (Monomorphic, THF_Without_Choice) 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, ""), agsyhol_thf0, "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 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_tff0 = TFF Monomorphic 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 in (* FUDGE *) if heuristic = e_smartN then [(0.15, (((128, meshN), e_tff0, "mono_native", combsN, false), e_fun_weightN)), (0.15, (((128, mashN), e_tff0, "mono_native", combsN, false), e_sym_offset_weightN)), (0.15, (((91, mepoN), e_tff0, "mono_native", combsN, false), e_autoN)), (0.15, (((1000, meshN), e_tff0, "poly_guards??", combsN, false), e_sym_offset_weightN)), (0.15, (((256, mepoN), e_tff0, "mono_native", liftingN, false), e_fun_weightN)), (0.25, (((64, mashN), e_tff0, "mono_native", combsN, false), e_fun_weightN))] else [(1.0, (((500, ""), e_tff0, "mono_native", 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) (* E-MaLeS *) val e_males_config : atp_config = {exec = K (["E_MALES_HOME"], ["emales.py"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name, proof_delims = tstp_proof_delims, known_failures = #known_failures e_config, prem_role = Conjecture, best_slices = (* FUDGE *) K [(0.25, (((500, meshN), FOF, "mono_guards??", combs_or_liftingN, false), "")), (0.25, (((150, meshN), FOF, "poly_tags??", combs_or_liftingN, false), "")), (0.25, (((50, meshN), FOF, "mono_tags??", combs_or_liftingN, false), "")), (0.25, (((1000, meshN), FOF, "poly_guards??", combsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e_males = (e_malesN, fn () => e_males_config) (* E-Par *) val e_par_config : atp_config = {exec = K (["E_HOME"], ["runepar.pl"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^ " 2" (* proofs *), proof_delims = tstp_proof_delims, known_failures = #known_failures e_config, prem_role = Conjecture, best_slices = #best_slices e_males_config, best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val e_par = (e_parN, fn () => e_par_config) (* Ehoh *) val ehoh_thf0 = THF (Monomorphic, THF_Predicate_Free) val ehoh_config : atp_config = {exec = fn _ => (["E_HOME"], ["eprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--auto-schedule --tstp-in --tstp-out --silent --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 = Hypothesis, best_slices = (* FUDGE *) K [(1.0, (((500, ""), ehoh_thf0, "mono_native_higher", liftingN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val ehoh = (ehohN, fn () => ehoh_config) (* iProver *) val iprover_config : atp_config = {exec = K (["IPROVER_HOME"], ["iprover"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "--clausifier \"$IPROVER_HOME\"/vclausify_rel --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) (* iProver-Eq *) val iprover_eq_config : atp_config = {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]), arguments = #arguments iprover_config, proof_delims = #proof_delims iprover_config, known_failures = #known_failures iprover_config, prem_role = #prem_role iprover_config, best_slices = #best_slices iprover_config, best_max_mono_iters = #best_max_mono_iters iprover_config, best_max_new_mono_instances = #best_max_new_mono_instances iprover_config} val iprover_eq = (iprover_eqN, fn () => iprover_eq_config) (* LEO-II *) val leo2_thf0 = THF (Monomorphic, THF_Without_Choice) 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, ""), leo2_thf0, "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_thf1 = THF (Polymorphic, THF_Without_Choice) 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, ""), leo3_thf1, "poly_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_thf0 = THF (Monomorphic, THF_Without_Choice) 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, ""), satallax_thf0, "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_extra_options = Attrib.setup_config_string \<^binding>\atp_spass_extra_options\ (K "") 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 ctxt => (* 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))] |> (case Config.get ctxt spass_extra_options of "" => I | opts => map (apsnd (apsnd (K opts)))), 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_tff0 = TFF Monomorphic val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS" (* cf. p. 20 of https://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *) val vampire_full_proof_options = " --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\ \naming=0" val remote_vampire_full_proof_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), vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)), (0.333, (((150, meshN), vampire_tff0, "poly_tags??", combs_or_liftingN, false), sosN)), (0.334, (((50, meshN), vampire_tff0, "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_tff0 = TFF Monomorphic 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), z3_tff0, "mono_native", combsN, false), "")), (0.25, (((125, mepoN), z3_tff0, "mono_native", combsN, false), "")), (0.125, (((62, mashN), z3_tff0, "mono_native", combsN, false), "")), (0.125, (((31, meshN), z3_tff0, "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_thf1 = THF (Polymorphic, THF_Predicate_Free) val zipperposition_config : atp_config = {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => "-print none -proof tstp -print-types -timeout " ^ 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 = fn _ => (* FUDGE *) [(1.0, (((100, ""), zipperposition_thf1, "poly_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val zipperposition = (zipperpositionN, fn () => zipperposition_config) (* Not really a prover: Experimental Polymorphic THF and DFG output *) 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_thf_format = THF (Polymorphic, THF_With_Choice) val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config) val pirate_format = DFG Polymorphic val remote_pirate_config : atp_config = {exec = K (["ISABELLE_ATP"], ["scripts/remote_pirate"]), arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => string_of_int (to_secs 1 timeout) ^ " " ^ file_name, proof_delims = [("Involved clauses:", "Involved clauses:")], known_failures = known_szs_status_failures, prem_role = #prem_role spass_config, best_slices = K [(1.0, (((200, ""), pirate_format, "tc_native", combsN, true), ""))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} val remote_pirate = (remote_prefix ^ pirateN, fn () => remote_pirate_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 = 240 (* 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 full_proofs => fn full_proof_command => fn timeout => fn file_name => fn _ => (if full_proofs andalso full_proof_command <> "" then "-c " ^ quote full_proof_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 explicit_tff0 = TFF Monomorphic val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] (K (((750, ""), e_tff0, "mono_native", combsN, false), "") (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] (K (((150, ""), FOF, "mono_guards??", liftingN, false), "") (* FUDGE *)) val remote_iprover_eq = remotify_atp iprover_eq "iProver-Eq" ["0.8"] (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, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) val remote_e_sine = remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture (K (((500, ""), FOF, "mono_guards??", combsN, false), "") (* FUDGE *)) val remote_snark = remote_atp snarkN "SNARK" ["20120808r022", "20080805r029", "20080805r024"] [("refutation.", "end_refutation.")] [] Hypothesis (K (((100, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_e_tofof = remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis (K (((150, ""), explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" -val remote_waldmeister_new = gen_remote_waldmeister waldmeister_newN "mono_args" (* 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 = String.isSuffix pirateN atp} 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, e_males, e_par, ehoh, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, - remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new] + remote_vampire, remote_snark, remote_pirate, remote_waldmeister] val _ = Theory.setup (fold add_atp atps) end; diff --git a/src/HOL/Tools/ATP/atp_waldmeister.ML b/src/HOL/Tools/ATP/atp_waldmeister.ML deleted file mode 100644 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML +++ /dev/null @@ -1,596 +0,0 @@ -(* Title: HOL/Tools/ATP/atp_waldmeister.ML - Author: Albert Steckermeier, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -General-purpose functions used by the Sledgehammer modules. -*) - -exception FailureMessage of string - -signature ATP_WALDMEISTER_SKOLEMIZER = -sig - val skolemize : bool -> Proof.context -> term -> (Proof.context * (term list * term)) -end; - -signature ATP_WALDMEISTER_TYPE_ENCODER = -sig - val encode_type : typ -> string - val decode_type_string : string -> typ - val encode_types : typ list -> string - val decode_types : string -> typ list - val encode_const : string * typ list -> string - val decode_const : string -> string * typ list -end; - -signature ATP_WALDMEISTER = -sig - type 'a atp_problem = 'a ATP_Problem.atp_problem - type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - type 'a atp_proof = 'a ATP_Proof.atp_proof - type stature = ATP_Problem_Generate.stature - type waldmeister_info = (string * (term list * (term option * term))) list - - val waldmeister_skolemize_rule : string - - val generate_waldmeister_problem : Proof.context -> term list -> term -> - ((string * stature) * term) list -> - string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * - waldmeister_info - val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof -> - (term, string) atp_step list - val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> - (term, string) atp_step list -end; - -structure ATP_Waldmeister_Skolemizer : ATP_WALDMEISTER_SKOLEMIZER = -struct - -open HOLogic - -fun contains_quantor (Const (\<^const_name>\Ex\, _) $ _) = true - | contains_quantor (Const (\<^const_name>\All\, _) $ _) = true - | contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2 - | contains_quantor _ = false - -fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name, ty) = - let - val fun_type = (map type_of arg_trms) ---> ty - val (fun_name, _) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type) - val (_, ctxt1_new) = Variable.add_fixes [fun_name] ctxt1 - val (_, ctxt2_new) = Variable.add_fixes [fun_name] ctxt2 - in - (Term.list_comb (Free (fun_name,fun_type), arg_trms), ctxt1_new, ctxt2_new) - end - -fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) = - let - val (fun_trm, ctxt1_new, ctxt2_new) = - mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty) - in - (Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new) - end - -fun skolem_var ctxt (bound_name, ty, trm) = - let - val (var_name, _) = singleton (Variable.variant_frees ctxt []) (bound_name, ty) - val (_, ctxt') = Variable.add_fixes [var_name] ctxt - val var = Var ((var_name, 0), ty) - in - (Term.subst_bounds ([var], trm), ctxt', var) - end - -fun skolem_bound is_free ctxt1 ctxt2 spets vars x = - if is_free then - let - val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x - in - (ctxt1', ctxt2',spets, trm', vars) - end - else - let - val (trm', ctxt2', var) = skolem_var ctxt2 x - in - (ctxt1, ctxt2', spets, trm', var :: vars) - end - -fun skolemize' pos ctxt1 ctxt2 spets vars (Const (\<^const_name>\Not\, _) $ trm') = - let - val (ctxt1', ctxt2', spets', trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm' - in - (ctxt1', ctxt2', map mk_not spets', mk_not trm'') - end - | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (\<^const_name>\HOL.eq\, t) $ a $ b)) = - if t = \<^typ>\bool \ bool \ bool\ andalso contains_quantor trm then - skolemize' pos ctxt1 ctxt2 (trm :: spets) vars (mk_conj (mk_imp (a, b), mk_imp (b, a))) - else - (ctxt1, ctxt2, spets, trm) - | skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) = - if name = \<^const_name>\Ex\ orelse name = \<^const_name>\All\ then - let - val is_free = (name = \<^const_name>\Ex\ andalso pos) - orelse (name = \<^const_name>\All\ andalso not pos) - val (ctxt1', ctxt2', spets', trm', vars') = - skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x - in - skolemize' pos ctxt1' ctxt2' spets' vars' trm' - end - else - (ctxt1, ctxt2, spets, trm) - | skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) = - if name = \<^const_name>\conj\ orelse name = \<^const_name>\disj\ orelse - name = \<^const_name>\implies\ then - let - val pos_a = if name = \<^const_name>\implies\ then not pos else pos - val (ctxt1', ctxt2', spets', a') = skolemize' pos_a ctxt1 ctxt2 [] vars a - val (ctxt1'', ctxt2'', spets'', b') = skolemize' pos ctxt1' ctxt2' [] vars b - in - (ctxt1'', ctxt2'', - map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets, - c $ a' $ b') - end - else - (ctxt1,ctxt2,spets,c $ a $ b) - | skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm) - - fun vars_of trm = - rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm [])); - - fun skolemize positve ctxt trm = - let - val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm - in - (ctxt1, (trm :: List.rev spets, skolemized_trm)) - end - -end; - -structure ATP_Waldmeister_Type_Encoder : ATP_WALDMEISTER_TYPE_ENCODER = -struct - -val delimiter = ";" -val open_paranthesis = "[" -val close_parathesis = "]" -val type_prefix = "Type" -val tfree_prefix = "TFree" -val tvar_prefix = "TVar" - -val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis] - -fun encode_type (Type (name, types)) = - type_prefix ^ open_paranthesis ^ name ^ delimiter ^ - (map encode_type types |> space_implode delimiter) ^ close_parathesis -| encode_type (TFree (name, sorts)) = - tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ space_implode delimiter sorts ^ - close_parathesis -| encode_type (TVar ((name, i), sorts)) = - tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ - close_parathesis ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis - -fun encode_types types = space_implode delimiter (map encode_type types) - -fun parse_identifier x = - (Scan.many identifier_character >> implode) x - -fun parse_star delim scanner x = - (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x - -fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --| - $$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x -and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --| - $$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x -and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis - |-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ - close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| - $$ close_parathesis >> TVar) x -and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x - -fun parse_types x = parse_star delimiter parse_any_type x - -fun decode_type_string s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ - quote s)) parse_type)) (Symbol.explode s) |> fst - -fun decode_types s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ - quote s))) parse_types) (Symbol.explode s) |> fst - -fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys - -fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s - -fun decode_const s = Scan.finite Symbol.stopper - (Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^ - quote s))) parse_const) (Symbol.explode s) |> fst - -end; - -structure ATP_Waldmeister (*** : ATP_WALDMEISTER *) = -struct - -open ATP_Util -open ATP_Problem -open ATP_Problem_Generate -open ATP_Proof -open ATP_Proof_Reconstruct -open ATP_Waldmeister_Skolemizer -open ATP_Waldmeister_Type_Encoder -open HOLogic - -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 -type waldmeister_info = (string * (term list * (term option * term))) list - -val const_prefix = #"c" -val var_prefix = #"V" -val free_prefix = #"v" -val conjecture_condition_name = "condition" -val waldmeister_equals = "eq" -val waldmeister_true = "true" -val waldmeister_false = "false" -val waldmeister_skolemize_rule = "waldmeister_skolemize" -val lam_lift_waldmeister_prefix = "lambda_wm" -val waldmeister_apply = "wm_apply" - -val factsN = "Relevant facts" -val helpersN = "Helper facts" -val conjN = "Conjecture" -val conj_identifier = conjecture_prefix ^ "0" - -val WM_ERROR_MSG = "Waldmeister problem generator failed: " - -(* - Some utilitary functions for translation. -*) - -fun gen_ascii_tuple str = (str, ascii_of str) - -fun mk_eq_true (trm as (Const (\<^const_name>\HOL.eq\, _) $ _ $ _)) = (NONE,trm) - | mk_eq_true trm = (SOME trm,HOLogic.mk_eq (trm, \<^term>\True\)) - -val is_lambda_name = String.isPrefix lam_lifted_poly_prefix - -fun lookup table k = - List.find (fn (key, _) => key = k) table - -fun dest_list' (f $ t) = - let - val (function, trms) = dest_list' f - in - (function, t :: trms) - end - | dest_list' t = (t,[]); - -fun dest_list trm = dest_list' trm ||> List.rev - -fun list_update x [] = [x] - | list_update (a,b) ((c,d) :: xs) = - if a = c andalso b < d then - (a,b) :: xs - else - (c,d) :: list_update (a,b) xs - -(* - Hiding partial applications in terms -*) - -fun map_minimal_app' info (trm :: trms) = - map_minimal_app' (minimal_app' info trm) trms - | map_minimal_app' info _ = info - -and minimal_app' info (trm as _ $ _) = - let - val (function, trms) = dest_list trm - val info' = map_minimal_app' info trms - in - case function of - (Const _) => list_update (function, length trms) info' | - (Free _) => list_update (function, length trms) info' | - _ => info - end - | minimal_app' info (trm as Const _) = - list_update (trm, 0) info - | minimal_app' info (trm as Free _) = - list_update (trm, 0) info - | minimal_app' info _ = info; - -fun map_minimal_app trms = map_minimal_app' [] trms - -fun mk_waldmeister_app function [] = function - | mk_waldmeister_app function (a :: args) = - let - val funT = type_of function - val argT = type_of a - val resT = dest_funT funT |> snd - val newT = funT --> argT --> resT - in - mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ - encode_types [resT, argT], newT) $ function $ a) args - end - -fun hide_partial_applications info (trm as (_ $ _)) = - let - val (function, trms) = dest_list trm - val trms' = map (hide_partial_applications info) trms - in - case function of - Var _ => mk_waldmeister_app function trms' | - _ => - let - val min_args = lookup info function |> the |> snd - val args0 = List.take (trms',min_args) - val args1 = List.drop (trms',min_args) - val function' = list_comb (function,args0) - in - mk_waldmeister_app function' args1 - end - end - | hide_partial_applications _ t = t; - -fun remove_waldmeister_app ((c as Const (name, _)) $ x $ y) = - if String.isPrefix waldmeister_apply name then - remove_waldmeister_app x $ remove_waldmeister_app y - else - c $ remove_waldmeister_app x $ remove_waldmeister_app y - | remove_waldmeister_app (x $ y) = remove_waldmeister_app x $ remove_waldmeister_app y - | remove_waldmeister_app x = x - -(* - Translation from Isabelle terms to ATP terms. -*) - -fun trm_to_atp'' thy (Const (x, ty)) args = - let - val ty_args = if is_lambda_name x orelse String.isPrefix waldmeister_apply x then - [] else Sign.const_typargs thy (x, ty) - in - [ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)] - end - | trm_to_atp'' _ (Free (x, _)) args = - [ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)] - | trm_to_atp'' _ (Var ((x, _), _)) args = - [ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)] - | trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args) - | trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term") - -fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd - -fun eq_trm_to_atp thy (Const (\<^const_name>\HOL.eq\, _) $ lhs $ rhs) = - ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs]) - | eq_trm_to_atp _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Non-eq term") - -(* Translation from ATP terms to Isabelle terms. *) - -fun construct_term thy (name, args) = - let - val prefix = String.sub (name, 0) - val encoded_name = String.extract(name, 1, NONE) - fun dummy_fun_type () = replicate (length args) dummyT ---> dummyT - in - if prefix = const_prefix then - let - val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then - (waldmeister_apply, []) else decode_const encoded_name - val const_trans_name = - if is_lambda_name const_name then - lam_lift_waldmeister_prefix ^ (* ?? *) - String.extract(const_name, size lam_lifted_poly_prefix, NONE) - else - const_name - in - Const (const_trans_name, - if is_lambda_name const_name orelse String.isPrefix waldmeister_apply const_name then - dummyT - else - Sign.const_instance thy (const_name, ty_args)) - end - else if prefix = free_prefix then - Free (encoded_name, dummy_fun_type ()) - else if Char.isUpper prefix then - Var ((name, 0), dummy_fun_type ()) - (* Use name instead of encoded_name because Waldmeister renames free variables. *) - else if name = waldmeister_equals then - (case args of - [_, _] => eq_const dummyT - | _ => raise FailureMessage - (WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ - Int.toString (length args))) - else if name = waldmeister_true then - \<^term>\True\ - else if name = waldmeister_false then - \<^term>\False\ - else - raise FailureMessage - (WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name) - end - -and atp_to_trm' thy (ATerm ((name,_), args)) = - (case args of - [] => construct_term thy (name, args) - | _ => Term.list_comb (construct_term thy (name, args), map (atp_to_trm' thy) args)) - | atp_to_trm' _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm") - -fun atp_to_trm thy (ATerm (("equal", _), [lhs, rhs])) = - mk_eq (atp_to_trm' thy lhs, atp_to_trm' thy rhs) - | atp_to_trm _ (ATerm (("$true", _), _)) = \<^term>\True\ - | atp_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm") - -fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy - | formula_to_trm thy (AConn (ANot, [aterm])) = - mk_not (formula_to_trm thy aterm) - | formula_to_trm _ _ = - raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") - -(* Abstract translation *) - -fun mk_formula prefix_name name atype aterm = - Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, []) - -fun problem_lines_of_fact thy prefix (s, (_, (_, t))) = - mk_formula (prefix ^ "0_") s Axiom (eq_trm_to_atp thy t) - -fun make_nice problem = nice_atp_problem true CNF problem - -fun mk_conjecture aterm = - let - val formula = mk_anot (AAtom aterm) - in - Formula ((conj_identifier, ""), Hypothesis, formula, NONE, []) - end - -fun generate_waldmeister_problem ctxt hyps_t0 concl_t0 facts0 = - let - val thy = Proof_Context.theory_of ctxt - - val preproc = Object_Logic.atomize_term ctxt - - val conditions = map preproc hyps_t0 - val consequence = preproc concl_t0 - val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list - - fun map_ctxt' _ ctxt [] ys = (ctxt, ys) - | map_ctxt' f ctxt (x :: xs) ys = - let - val (ctxt', x') = f ctxt x - in - map_ctxt' f ctxt' xs (x' :: ys) - end - - fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs [] - - fun skolemize_fact ctxt (name, trm) = - let - val (ctxt', (steps, trm')) = skolemize true ctxt trm - in - (ctxt', (name, (steps, trm'))) - end - - fun name_list' _ [] _ = [] - | name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1) - - fun name_list prefix xs = name_list' prefix xs 0 - - (* Skolemization, hiding lambdas and translating formulas to equations *) - val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts - val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions - - val post_skolem = do_cheaply_conceal_lambdas [] - - val sko_eq_facts0 = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts - val sko_eq_conditions0 = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions - |> name_list conjecture_condition_name - val (_, eq_conseq as (_, (non_eq_consequence0, eq_consequence0))) = - skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) - - val sko_eq_info = - (((conj_identifier, eq_conseq) :: sko_eq_conditions0) - @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0) - - (* Translation of partial function applications *) - val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info) - - fun hide_partial_apps_in_last (x, (y, (z, term))) = - (x, (y, (z, hide_partial_applications fun_app_info term))) - - val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0 - val sko_eq_conditions = map hide_partial_apps_in_last sko_eq_conditions0 - val eq_consequence = hide_partial_applications fun_app_info eq_consequence0 - - (* Problem creation *) - val fact_lines = map (problem_lines_of_fact thy fact_prefix) sko_eq_facts - val condition_lines = - map (fn (name, (_, (_, trm))) => - mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions - val axiom_lines = fact_lines @ condition_lines - - val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence) - - val helper_lemmas_needed = exists (snd #> snd #> fst #> is_some) sko_eq_facts - orelse exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse - is_some non_eq_consequence0 - - val helper_lines = - if helper_lemmas_needed then - [(helpersN, - @{thms waldmeister_fol} - |> map (fn th => (("", (Global, General)), preproc (Thm.prop_of th))) - |> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))] - else - [] - - val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] - - val (nice_problem, pool) = make_nice problem - in - (nice_problem, Option.map snd pool |> the_default Symtab.empty, [], Symtab.empty, sko_eq_info) - end - -fun termify_line ctxt (name, role, u, rule, deps) = - let - val thy = Proof_Context.theory_of ctxt - val t = u |> formula_to_trm thy |> remove_waldmeister_app - |> singleton (infer_formulas_types ctxt) - |> HOLogic.mk_Trueprop - in - (name, role, t, rule, deps) - end - -fun termify_waldmeister_proof ctxt pool = - nasty_atp_proof pool - #> map (termify_line ctxt) - #> repair_waldmeister_endgame - -fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of - SOME x => x | - NONE => NONE - -fun fix_name name = - if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then - String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> - (fn x => fact_prefix ^ "0_" ^ x) - else - name - -fun skolemization_steps info - (proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) = - case get_skolem_info info (map fix_name isabelle_names) of - NONE => [proof_step] | - SOME (_, ([], _)) => [proof_step] | - SOME (_, (step :: steps,_)) => - let - val raw_trm = dest_Trueprop trm - val is_narrowing = raw_trm = \<^term>\True = False\ orelse raw_trm = \<^term>\False = True\ - val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name andalso not is_narrowing - in - if is_narrowing then - [proof_step] - else - let - fun mk_steps _ [] = [] - | mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]), - Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule, - [(waldmeister_name ^ "_" ^ Int.toString (i-1), - if i = 1 then isabelle_names else [])]) - :: mk_steps (i+1) xs - - val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown, - mk_Trueprop ((is_conjecture ? mk_not) step), rule, []) - - val sub_steps = mk_steps 1 steps - - val skolem_steps = first_step :: sub_steps - val num_of_steps = length skolem_steps - in - (skolem_steps @ - [((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule, - [(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1), - if num_of_steps = 1 then isabelle_names else [])])]) - end - end - -fun introduce_waldmeister_skolems info proof_steps = proof_steps - |> maps (skolemization_steps info) -end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML @@ -1,478 +1,478 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen Isar proof reconstruction from ATP proofs. *) signature SLEDGEHAMMER_ISAR = sig type atp_step_name = ATP_Proof.atp_step_name type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature type one_line_params = Sledgehammer_Proof_Methods.one_line_params val trace : bool Config.T type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string end; structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct open ATP_Util open ATP_Problem +open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct -open ATP_Waldmeister open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Compress open Sledgehammer_Isar_Minimize structure String_Redirect = ATP_Proof_Redirect( type key = atp_step_name val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') val string_of = fst) open String_Redirect val trace = Attrib.setup_config_bool \<^binding>\sledgehammer_isar_trace\ (K false) val e_definition_rule = "definition" val e_skolemize_rule = "skolemize" val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" val pirate_datatype_rule = "DT" val satallax_skolemize_rule = "tab_ex" val vampire_skolemisation_rule = "skolemisation" val veriT_la_generic_rule = "la_generic" val veriT_simp_arith_rule = "simp_arith" val veriT_tmp_skolemize_rule = "tmp_skolemize" val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") val zipperposition_cnf_rule = "cnf" val skolemize_rules = [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, - spass_skolemize_rule, vampire_skolemisation_rule, - veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] + spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, + zipperposition_cnf_rule] fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix val is_skolemize_rule = member (op =) skolemize_rules fun is_arith_rule rule = String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse rule = veriT_la_generic_rule val is_datatype_rule = String.isPrefix pirate_datatype_rule fun raw_label_of_num num = (num, 0) fun label_of_clause [(num, _)] = raw_label_of_num num | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) fun add_global_fact ss = apsnd (union (op =) ss) fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) fun add_line_pass1 (line as (name, role, t, rule, [])) lines = (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or definitions. *) if role = Conjecture orelse role = Negated_Conjecture then line :: lines else if t aconv \<^prop>\True\ then map (replace_dependencies_in_line (name, [])) lines else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines else if role = Axiom then lines (* axioms (facts) need no proof lines *) else map (replace_dependencies_in_line (name, [])) lines | add_line_pass1 line lines = line :: lines fun add_lines_pass2 res [] = rev res | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) = let fun normalize role = role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) val norm_t = normalize role t val is_duplicate = exists (fn (prev_name, prev_role, prev_t, _, _) => (prev_role = Hypothesis andalso prev_t aconv t) orelse (member (op =) deps prev_name andalso Term.aconv_untyped (normalize prev_role prev_t, norm_t))) res fun looks_boring () = t aconv \<^prop>\False\ orelse length deps < 2 fun is_skolemizing_line (_, _, _, rule', deps') = is_skolemize_rule rule' andalso member (op =) deps' name fun is_before_skolemize_rule () = exists is_skolemizing_line lines in if is_duplicate orelse (role = Plain andalso not (is_skolemize_rule rule) andalso not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) else add_lines_pass2 (line :: res) lines end type isar_params = bool * (string option * string option) * Time.time * real option * bool * bool * (term, string) atp_step list * thm val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods val datatype_methods = [Simp_Method, Simp_Size_Method] val systematic_methods = basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods val skolem_methods = Moura_Method :: systematic_methods fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = let val _ = if debug then writeln "Constructing Isar proof..." else () fun generate_proof_text () = let val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = isar_params () in if null atp_proof0 then one_line_proof_text ctxt 0 one_line_params else let val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods fun massage_methods (meths as meth :: _) = if not try0 then [meth] else if smt_proofs = SOME true then SMT_Method :: meths else meths val (params, _, concl_t) = strip_subgoal goal subgoal ctxt val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd val do_preplay = preplay_timeout <> Time.zeroTime val compress = (case compress of NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 | SOME n => n) fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev fun get_role keep_role ((num, _), role, t, rule, _) = if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE val atp_proof = fold_rev add_line_pass1 atp_proof0 [] |> add_lines_pass2 [] val conjs = map_filter (fn (name, role, _, _, _) => if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) atp_proof val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof fun add_lemma ((l, t), rule) ctxt = let val (skos, meths) = (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) else if is_arith_rule rule then ([], arith_methods) else ([], rewrite_methods)) ||> massage_methods in (Prove ([], skos, l, t, [], ([], []), meths, ""), ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) end val (lems, _) = fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt val bot = #1 (List.last atp_proof) val refute_graph = atp_proof |> map (fn (name, _, _, _, from) => (from, name)) |> make_refute_graph bot |> fold (Atom_Graph.default_node o rpair ()) conjs val axioms = axioms_of_refute_graph refute_graph conjs val tainted = tainted_atoms_of_refute_graph refute_graph conjs val is_clause_tainted = exists (member (op =) tainted) val steps = Symtab.empty |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then HOLogic.dest_Trueprop #> role <> Conjecture ? s_not #> fold exists_of (map Var (Term.add_vars t [])) #> HOLogic.mk_Trueprop else I)))) atp_proof fun is_referenced_in_step _ (Let _) = false | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) = member (op =) ls l orelse exists (is_referenced_in_proof l) subs and is_referenced_in_proof l (Proof (_, _, steps)) = exists (is_referenced_in_step l) steps fun insert_lemma_in_step lem (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = let val l' = the (label_of_isar_step lem) in if member (op =) ls l' then [lem, step] else let val refs = map (is_referenced_in_proof l') subs in if length (filter I refs) = 1 then let val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs in [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] end else [lem, step] end end and insert_lemma_in_steps lem [] = [lem] | insert_lemma_in_steps lem (step :: steps) = if is_referenced_in_step (the (label_of_isar_step lem)) step then insert_lemma_in_step lem step @ steps else step :: insert_lemma_in_steps lem steps and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = Proof (fix, assms, insert_lemma_in_steps lem steps) val rule_of_clause_id = fst o the o Symtab.lookup steps o fst val finish_off = close_form #> rename_bound_vars fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off | prop_of_clause names = let val lits = map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) | _ => fold (curry s_disj) lits \<^term>\False\) end |> HOLogic.mk_Trueprop |> finish_off fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] fun isar_steps outer predecessor accum [] = accum |> (if tainted = [] then (* e.g., trivial, empty proof by Z3 *) cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) else I) |> rev | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = let val l = label_of_clause c val t = prop_of_clause c val rule = rule_of_clause_id id val skolem = is_skolemize_rule rule val deps = ([], []) |> fold add_fact_of_dependency gamma |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |> sort_facts val meths = (if skolem then skolem_methods else if is_arith_rule rule then arith_methods else if is_datatype_rule rule then datatype_methods else systematic_methods') |> massage_methods fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs in if is_clause_tainted c then (case gamma of [g] => if skolem andalso is_clause_tainted g then let val skos = skolems_of ctxt (prop_of_clause g) val subproof = Proof (skos, [], rev accum) in isar_steps outer (SOME l) [prove [subproof] ([], [])] infs end else steps_of_rest (prove [] deps) | _ => steps_of_rest (prove [] deps)) else steps_of_rest (if skolem then (case skolems_of ctxt t of [] => prove [] deps | skos => Prove ([], skos, l, t, [], deps, meths, "")) else prove [] deps) end | isar_steps outer predecessor accum (Cases cases :: infs) = let fun isar_case (c, subinfs) = isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs val c = succedent_of_cases cases val l = label_of_clause c val t = prop_of_clause c val step = Prove (maybe_show outer c, [], l, t, map isar_case (filter_out (null o snd) cases), sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") in isar_steps outer (SOME l) (step :: accum) infs end and isar_proof outer fix assms lems infs = Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) val trace = Config.get ctxt trace val canonical_isar_proof = refute_graph |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |> redirect_graph axioms tainted bot |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |> isar_proof true params assms lems |> postprocess_isar_proof_remove_show_stuttering |> postprocess_isar_proof_remove_unreferenced_steps I |> relabel_isar_proof_canonically val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty val _ = fold_isar_steps (fn meth => K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) (steps_of_isar_proof canonical_isar_proof) () fun str_of_preplay_outcome outcome = if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" fun str_of_meth l meth = string_of_proof_method ctxt [] meth ^ " " ^ str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) fun comment_of l = map (str_of_meth l) #> commas fun trace_isar_proof label proof = if trace then tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof ctxt subgoal subgoal_count (comment_isar_proof comment_of proof) ^ "\n") else () fun comment_of l (meth :: _) = (case (verbose, Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of (false, Played _) => "" | (_, outcome) => string_of_play_outcome outcome) val (play_outcome, isar_proof) = canonical_isar_proof |> tap (trace_isar_proof "Original") |> compress_isar_proof ctxt compress preplay_timeout preplay_data |> tap (trace_isar_proof "Compressed") |> postprocess_isar_proof_remove_unreferenced_steps (keep_fastest_method_of_isar_step (!preplay_data) #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |> tap (trace_isar_proof "Minimized") |> `(preplay_outcome_of_isar_proof (!preplay_data)) ||> (comment_isar_proof comment_of #> chain_isar_proof #> kill_useless_labels_in_isar_proof #> relabel_isar_proof_nicely #> rationalize_obtains_in_isar_proofs ctxt) in (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of (0, 1) => one_line_proof_text ctxt 0 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then (case isar_proof of Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => let val used_facts' = map_filter (fn s => if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) used_facts then NONE else SOME (s, (Global, General))) gfs in ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) end) else one_line_params) ^ (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") | (_, num_steps) => let val msg = (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) in one_line_proof_text ctxt 0 one_line_params ^ "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup_command (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) end) end end in if debug then generate_proof_text () else (case try generate_proof_text () of SOME s => s | NONE => one_line_proof_text ctxt 0 one_line_params ^ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = (case play of Played _ => meth = SMT_Method andalso smt_proofs <> SOME true | Play_Timed_Out time => time > Time.zeroTime | Play_Failed => true) fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained (one_line_params as ((_, preplay), _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else one_line_proof_text ctxt num_chained) one_line_params end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,416 +1,407 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val is_ho_atp : Proof.context -> string -> bool val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct -open ATP_Waldmeister open ATP_Satallax open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun is_atp_of_format is_format ctxt name = let val thy = Proof_Context.theory_of ctxt in (case try (get_atp thy) name of SOME config => exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt) | NONE => false) end val is_ho_atp = is_atp_of_format is_format_higher_order fun choose_type_enc strictness best_type_enc format = the_default best_type_enc #> type_enc_of_string strictness #> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^const>\Trueprop\ $ t1) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^const>\Pure.imp\ $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^const>\HOL.implies\ $ t1 $ t2) => do_formula (not pos) t1 andalso (t2 = \<^const>\False\ orelse do_formula pos t2) | (_, \<^const>\Not\ $ t1) => do_formula (not pos) t1 | (true, \<^const>\HOL.disj\ $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (false, \<^const>\HOL.conj\ $ t1 $ t2) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) fun get_slices slice slices = (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single) fun get_facts_of_filter _ [(_, facts)] = facts | get_facts_of_filter fact_filter factss = (case AList.lookup (op =) factss fact_filter of SOME facts => facts | NONE => snd (hd factss)) (* For low values of "max_facts", this fudge value ensures that most slices are invoked with a nontrivial amount of facts. *) val max_fact_factor_fudge = 5 val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be the only ATP that does not honor its time limit. *) val atp_timeout_slack = seconds 1.0 (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout, preplay_timeout, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, best_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name - val waldmeister_new = (local_name = waldmeister_newN) val spassy = (local_name = pirateN orelse local_name = spassN) val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) val prob_path = if dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode dest_dir) then Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir) val exec = exec full_proofs val command0 = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun split_time s = let val split = String.tokens (fn c => str c = "\n") val (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int) val digit = Scan.one Symbol.is_ascii_digit val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int) val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b) val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0 in (output, as_time t |> Time.fromMilliseconds) end fun run () = let (* If slicing is disabled, we expand the last slice to fill the entire time available. *) val all_slices = best_slices ctxt val actual_slices = get_slices slice all_slices fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) = fold (Integer.max o fst o #1 o fst o snd) slices 0 val num_actual_slices = length actual_slices val max_fact_factor = Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max) / Real.fromInt (max_facts_of_slices (map snd actual_slices)) fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters best_max_mono_iters max_new_mono_instances best_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end fun run_slice time_left (cache_key, cache_value) (slice, (time_frac, (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans, best_uncurried_aliases), extra))) = let val effective_fact_filter = fact_filter |> the_default best_fact_filter val facts = get_facts_of_filter effective_fact_filter factss val num_facts = Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge |> Integer.min (length facts) val generate_info = (case format of DFG _ => true | _ => false) val strictness = if strict then Strict else Non_Strict val type_enc = type_enc |> choose_type_enc strictness best_type_enc format val sound = is_type_enc_sound type_enc val real_ms = Real.fromInt o Time.toMilliseconds val slice_timeout = (real_ms time_left |> (if slice < num_actual_slices - 1 then curry Real.min (time_frac * real_ms timeout) else I)) * 0.001 |> seconds val generous_slice_timeout = if mode = MaSh then one_day else slice_timeout + atp_timeout_slack val _ = if debug then quote name ^ " slice #" ^ string_of_int (slice + 1) ^ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..." |> writeln else () val readable_names = not (Config.get ctxt atp_full_names) val lam_trans = lam_trans |> the_default best_lam_trans val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases - val value as (atp_problem, _, _, _, _) = + val value as (atp_problem, _, _, _) = if cache_key = SOME key then cache_value else facts |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) - |> (if waldmeister_new then - generate_waldmeister_problem ctxt hyp_ts concl_t - #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e)) - else - generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode - lam_trans uncurried_aliases readable_names true hyp_ts concl_t - #> (fn (a, b, c, d) => (a, b, c, d, NONE))) + |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode + lam_trans uncurried_aliases readable_names true hyp_ts concl_t fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra slice_timeout (File.bash_path prob_path) (ord, ord_info, sel_weights) val command = "(exec 2>&1; " ^ File.bash_path command0 ^ " " ^ args ^ " " ^ ")" |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem |> lines_of_atp_problem format ord ord_info |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = Timeout.apply generous_slice_timeout Isabelle_System.bash_output command |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I) |> fst |> split_time |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut)) val outcome = (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => (found_proof (); NONE)) | _ => outcome) in ((SOME key, value), (output, run_time, facts, atp_proof, outcome), SOME (format, type_enc)) end val timer = Timer.startRealTimer () fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _), _)) = let val time_left = timeout - Timer.checkRealTimer timer in if time_left <= Time.zeroTime then result else run_slice time_left cache slice |> (fn (cache, (output, run_time, used_from, atp_proof, outcome), format_type_enc) => (cache, (output, run_time0 + run_time, used_from, atp_proof, outcome), format_type_enc)) end | maybe_run_slice _ result = result in - ((NONE, ([], Symtab.empty, [], Symtab.empty,NONE)), + ((NONE, ([], Symtab.empty, [], Symtab.empty)), ("", Time.zeroTime, [], [], SOME InternalError), NONE) |> fold maybe_run_slice actual_slices end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _), _) = if dest_dir = "" then () else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output - val ((_, (_, pool, lifted, sym_tab,wm_info)), (output, run_time, used_from, atp_proof, outcome), + val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome), SOME (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred_methss = (Metis_Method (NONE, NONE), bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)) in (used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val metis_type_enc = if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE val atp_proof = atp_proof - |> (if waldmeister_new then termify_waldmeister_proof ctxt pool - else termify_atp_proof ctxt name format type_enc pool lifted sym_tab) + |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> spassy ? introduce_spassy_skolems - |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I) |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;