# HG changeset patch # User blanchet # Date 1281348348 -7200 # Node ID 319c59682c510956f21bf0d6eecfc8738cc4a10e # Parent 601b7972eef296f6b73f9f9300a6c6ef1d107d33 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) diff -r 601b7972eef2 -r 319c59682c51 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Aug 09 12:05:48 2010 +0200 @@ -321,9 +321,10 @@ Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer.ML \ Tools/Sledgehammer/sledgehammer_fact_filter.ML \ - Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \ + Tools/Sledgehammer/sledgehammer_fact_minimize.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ + Tools/Sledgehammer/sledgehammer_translate.ML \ Tools/Sledgehammer/sledgehammer_util.ML \ Tools/SMT/cvc3_solver.ML \ Tools/SMT/smtlib_interface.ML \ diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 09 12:05:48 2010 +0200 @@ -391,7 +391,7 @@ val params = Sledgehammer_Isar.default_params thy [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")] val minimize = - Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st) + Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st) val _ = log separator in case minimize st (these (!named_thms)) of diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Mon Aug 09 12:05:48 2010 +0200 @@ -20,9 +20,10 @@ ("Tools/Sledgehammer/metis_tactics.ML") ("Tools/Sledgehammer/sledgehammer_util.ML") ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") + ("Tools/Sledgehammer/sledgehammer_translate.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") ("Tools/Sledgehammer/sledgehammer.ML") - ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") + ("Tools/Sledgehammer/sledgehammer_fact_minimize.ML") ("Tools/Sledgehammer/sledgehammer_isar.ML") begin @@ -100,10 +101,11 @@ use "Tools/Sledgehammer/sledgehammer_util.ML" use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" +use "Tools/Sledgehammer/sledgehammer_translate.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" use "Tools/Sledgehammer/sledgehammer.ML" setup Sledgehammer.setup -use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML" +use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML" use "Tools/Sledgehammer/sledgehammer_isar.ML" setup Metis_Tactics.setup diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 09 12:05:48 2010 +0200 @@ -149,6 +149,8 @@ string -> (string * string) list -> theory -> theory val unregister_frac_type : string -> Proof.context -> Proof.context val unregister_frac_type_global : string -> theory -> theory + val register_codatatype_generic : + typ -> string -> styp list -> Context.generic -> Context.generic val register_codatatype : typ -> string -> styp list -> Proof.context -> Proof.context val register_codatatype_global : diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 09 12:05:48 2010 +0200 @@ -100,7 +100,7 @@ val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); -(*FIXME: requires more use of cterm constructors*) +(* FIXME: Requires more use of cterm constructors. *) fun abstract ct = let val thy = theory_of_cterm ct diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 09 12:05:48 2010 +0200 @@ -39,7 +39,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - internal_thm_names: string Vector.vector, + axiom_names: string Vector.vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -64,6 +64,7 @@ open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter +open Sledgehammer_Translate open Sledgehammer_Proof_Reconstruct @@ -73,9 +74,6 @@ "Async_Manager". *) val das_Tool = "Sledgehammer" -(* Freshness almost guaranteed! *) -val sledgehammer_weak_prefix = "Sledgehammer:" - fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" val messages = Async_Manager.thread_messages das_Tool "ATP" @@ -112,7 +110,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - internal_thm_names: string Vector.vector, + axiom_names: string Vector.vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -158,471 +156,6 @@ else failure)) - -(* Clause preparation *) - -datatype fol_formula = - FOLFormula of {name: string, - kind: kind, - combformula: (name, combterm) formula, - ctypes_sorts: typ list} - -fun mk_anot phi = AConn (ANot, [phi]) -fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) -fun mk_ahorn [] phi = phi - | mk_ahorn (phi :: phis) psi = - AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) - -fun combformula_for_prop thy = - let - val do_term = combterm_from_term thy - fun do_quant bs q s T t' = - do_formula ((s, T) :: bs) t' - #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) - and do_conn bs c t1 t2 = - do_formula bs t1 ##>> do_formula bs t2 - #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) - and do_formula bs t = - case t of - @{const Not} $ t1 => - do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) - | Const (@{const_name All}, _) $ Abs (s, T, t') => - do_quant bs AForall s T t' - | Const (@{const_name Ex}, _) $ Abs (s, T, t') => - do_quant bs AExists s T t' - | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 - | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 - | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 - | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - do_conn bs AIff t1 t2 - | _ => (fn ts => do_term bs (Envir.eta_contract t) - |>> AAtom ||> union (op =) ts) - in do_formula [] end - -(* Converts an elim-rule into an equivalent theorem that does not have the - predicate variable. Leaves other theorems unchanged. We simply instantiate - the conclusion variable to False. (Cf. "transform_elim_term" in - "ATP_Systems".) *) -fun transform_elim_term t = - case Logic.strip_imp_concl t of - @{const Trueprop} $ Var (z, @{typ bool}) => - subst_Vars [(z, @{const False})] t - | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t - | _ => t - -fun presimplify_term thy = - Skip_Proof.make_thm thy - #> Meson.presimplify - #> prop_of - -fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString 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 introduce_combinators_in_term ctxt kind t = - let - val thy = ProofContext.theory_of ctxt - fun aux Ts t = - case t of - @{const Not} $ t1 => @{const Not} $ aux Ts t1 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => - t0 $ Abs (s, T, aux (T :: Ts) t') - | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 - | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) - $ t1 $ t2 => - t0 $ aux Ts t1 $ aux Ts t2 - | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then - t - else - let - val t = t |> conceal_bounds Ts - |> Envir.eta_contract - val ([t], ctxt') = Variable.import_terms true [t] ctxt - in - t |> cterm_of thy - |> Clausifier.introduce_combinators_in_cterm - |> singleton (Variable.export ctxt' ctxt) - |> prop_of |> Logic.dest_equals |> snd - |> reveal_bounds Ts - end - in t |> not (Meson.is_fol_term thy t) ? aux [] end - handle THM _ => - (* A type variable of sort "{}" will make abstraction fail. *) - case kind of - Axiom => HOLogic.true_const - | Conjecture => HOLogic.false_const - -(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the - same in Sledgehammer to prevent the discovery of unreplable proofs. *) -fun freeze_term t = - let - fun aux (t $ u) = aux t $ aux u - | aux (Abs (s, T, t)) = Abs (s, T, aux t) - | aux (Var ((s, i), T)) = - Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) - | aux t = t - in t |> exists_subterm is_Var t ? aux end - -(* making axiom and conjecture formulas *) -fun make_formula ctxt presimp (name, kind, t) = - let - val thy = ProofContext.theory_of ctxt - val t = t |> transform_elim_term - |> Object_Logic.atomize_term thy - val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop - |> extensionalize_term - |> presimp ? presimplify_term thy - |> perhaps (try (HOLogic.dest_Trueprop)) - |> introduce_combinators_in_term ctxt kind - |> kind = Conjecture ? freeze_term - val (combformula, ctypes_sorts) = combformula_for_prop thy t [] - in - FOLFormula {name = name, combformula = combformula, kind = kind, - ctypes_sorts = ctypes_sorts} - end - -fun make_axiom ctxt presimp (name, th) = - (name, make_formula ctxt presimp (name, Axiom, prop_of th)) -fun make_conjectures ctxt ts = - map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t)) - (0 upto length ts - 1) ts - -(** Helper facts **) - -fun count_combterm (CombConst ((s, _), _, _)) = - Symtab.map_entry s (Integer.add 1) - | count_combterm (CombVar _) = I - | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] -fun count_combformula (AQuant (_, _, phi)) = count_combformula phi - | count_combformula (AConn (_, phis)) = fold count_combformula phis - | count_combformula (AAtom tm) = count_combterm tm -fun count_fol_formula (FOLFormula {combformula, ...}) = - count_combformula combformula - -val optional_helpers = - [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), - (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), - (["c_COMBS"], @{thms COMBS_def})] -val optional_typed_helpers = - [(["c_True", "c_False"], @{thms True_or_False}), - (["c_If"], @{thms if_True if_False True_or_False})] -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} - -val init_counters = - Symtab.make (maps (maps (map (rpair 0) o fst)) - [optional_helpers, optional_typed_helpers]) - -fun get_helper_facts ctxt is_FO full_types conjectures axioms = - let - val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters - fun is_needed c = the (Symtab.lookup ct c) > 0 - in - (optional_helpers - |> full_types ? append optional_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map (`Thm.get_name_hint) ths - else [])) @ - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) - |> map (snd o make_axiom ctxt false) - end - -fun meta_not t = @{const "==>"} $ t $ @{prop False} - -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = - let - val thy = ProofContext.theory_of ctxt - (* Remove existing axioms from the conjecture, as this can dramatically - boost an ATP's performance (for some reason). *) - val axiom_ts = map (prop_of o snd) axioms - val hyp_ts = - if null hyp_ts then - [] - else - let - val axiom_table = fold (Termtab.update o rpair ()) axiom_ts - Termtab.empty - in hyp_ts |> filter_out (Termtab.defined axiom_table) end - val goal_t = Logic.list_implies (hyp_ts, concl_t) - val is_FO = Meson.is_fol_term thy goal_t - val subs = tfree_classes_of_terms [goal_t] - val supers = tvar_classes_of_terms axiom_ts - val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) - (* TFrees in the conjecture; TVars in the axioms *) - val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt - val (axiom_names, axioms) = - ListPair.unzip (map (make_axiom ctxt true) axioms) - val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in - (Vector.fromList axiom_names, - (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) - end - -fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) - -fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) - | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) - | fo_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map fo_term_for_combtyp tys) - -fun fo_literal_for_type_literal (TyLitVar (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - | fo_literal_for_type_literal (TyLitFree (class, name)) = - (true, ATerm (class, [ATerm (name, [])])) - -fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot - -fun fo_term_for_combterm full_types = - let - fun aux top_level u = - let - val (head, args) = strip_combterm_comb u - val (x, ty_args) = - case head of - CombConst (name as (s, s'), _, ty_args) => - if s = "equal" then - (if top_level andalso length args = 2 then name - else ("c_fequal", @{const_name fequal}), []) - else if top_level then - case s of - "c_False" => (("$false", s'), []) - | "c_True" => (("$true", s'), []) - | _ => (name, if full_types then [] else ty_args) - else - (name, if full_types then [] else ty_args) - | CombVar (name, _) => (name, []) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map fo_term_for_combtyp ty_args @ - map (aux false) args) - in - if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t - end - in aux true end - -fun formula_for_combformula full_types = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) - in aux end - -fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = - mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) - (type_literals_for_types ctypes_sorts)) - (formula_for_combformula full_types combformula) - -fun problem_line_for_fact prefix full_types - (formula as FOLFormula {name, kind, ...}) = - Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) - -fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, - superclass, ...}) = - let val ty_arg = ATerm (("T", "T"), []) in - Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, - AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), - AAtom (ATerm (superclass, [ty_arg]))])) - end - -fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = - (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | fo_literal_for_arity_literal (TVarLit (c, sort)) = - (false, ATerm (c, [ATerm (sort, [])])) - -fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, - ...}) = - Fof (arity_clause_prefix ^ ascii_of name, Axiom, - mk_ahorn (map (formula_for_fo_literal o apfst not - o fo_literal_for_arity_literal) premLits) - (formula_for_fo_literal - (fo_literal_for_arity_literal conclLit))) - -fun problem_line_for_conjecture full_types - (FOLFormula {name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ name, kind, - formula_for_combformula full_types combformula) - -fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = - map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) - -fun problem_line_for_free_type lit = - Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) -fun problem_lines_for_free_types conjectures = - let - val litss = map free_type_literals_for_conjecture conjectures - val lits = fold (union (op =)) litss [] - in map problem_line_for_free_type lits end - -(** "hBOOL" and "hAPP" **) - -type const_info = {min_arity: int, max_arity: int, sub_level: bool} - -fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_tptp_variable s then - I - else - let val n = length ts in - Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => - {min_arity = Int.min (n, min_arity), - max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) - end) - #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_formula (AQuant (_, _, phi)) = consider_formula phi - | consider_formula (AConn (_, phis)) = fold consider_formula phis - | consider_formula (AAtom tm) = consider_term true tm - -fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi -fun consider_problem problem = fold (fold consider_problem_line o snd) problem - -fun const_table_for_problem explicit_apply problem = - if explicit_apply then NONE - else SOME (Symtab.empty |> consider_problem problem) - -val tc_fun = make_fixed_type_const @{type_name fun} - -fun min_arity_of thy full_types NONE s = - (if s = "equal" orelse s = type_wrapper_name orelse - String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s then - 16383 (* large number *) - else if full_types then - 0 - else case strip_prefix_and_undo_ascii const_prefix s of - SOME s' => num_type_args thy (invert_const s') - | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity - | NONE => 0 - -fun full_type_of (ATerm ((s, _), [ty, _])) = - if s = type_wrapper_name then ty else raise Fail "expected type wrapper" - | full_type_of _ = raise Fail "expected type wrapper" - -fun list_hAPP_rev _ t1 [] = t1 - | list_hAPP_rev NONE t1 (t2 :: ts2) = - ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) - | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = - let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, - [full_type_of t2, ty]) in - ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) - end - -fun repair_applications_in_term thy full_types const_tab = - let - fun aux opt_ty (ATerm (name as (s, _), ts)) = - if s = type_wrapper_name then - case ts of - [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) - | _ => raise Fail "malformed type wrapper" - else - let - val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts - in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end - in aux NONE end - -fun boolify t = ATerm (`I "hBOOL", [t]) - -(* 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_predicate NONE s = - s = "equal" orelse String.isPrefix type_const_prefix s orelse - String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity - | NONE => false - -fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = - if s = type_wrapper_name then - case ts of - [_, t' as ATerm ((s', _), _)] => - if is_predicate const_tab s' then t' else boolify t - | _ => raise Fail "malformed type wrapper" - else - t |> not (is_predicate const_tab s) ? boolify - -fun close_universally phi = - let - fun term_vars bounds (ATerm (name as (s, _), tms)) = - (is_tptp_variable s andalso not (member (op =) bounds name)) - ? insert (op =) name - #> fold (term_vars bounds) tms - fun formula_vars bounds (AQuant (q, xs, phi)) = - formula_vars (xs @ bounds) phi - | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis - | formula_vars bounds (AAtom tm) = term_vars bounds tm - in - case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) - end - -fun repair_formula thy explicit_forall full_types const_tab = - let - fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) - | aux (AConn (c, phis)) = AConn (c, map aux phis) - | aux (AAtom tm) = - AAtom (tm |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) - in aux #> explicit_forall ? close_universally end - -fun repair_problem_line thy explicit_forall full_types const_tab - (Fof (ident, kind, phi)) = - Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) -fun repair_problem_with_const_table thy = - map o apsnd o map ooo repair_problem_line thy - -fun repair_problem thy explicit_forall full_types explicit_apply problem = - repair_problem_with_const_table thy explicit_forall full_types - (const_table_for_problem explicit_apply problem) problem - -fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axioms, helper_facts, class_rel_clauses, - arity_clauses) = - let - val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms - val helper_lines = - map (problem_line_for_fact helper_prefix full_types) helper_facts - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures - val class_rel_lines = - map problem_line_for_class_rel_clause class_rel_clauses - val arity_lines = map problem_line_for_arity_clause arity_clauses - (* Reordering these might or might not confuse the proof reconstruction - code or the SPASS Flotter hack. *) - val problem = - [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy explicit_forall full_types explicit_apply - val (problem, pool) = nice_tptp_problem readable_names problem - val conjecture_offset = - length axiom_lines + length class_rel_lines + length arity_lines - + length helper_lines - val _ = File.write_list file (strings_for_tptp_problem problem) - in - (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, - conjecture_offset) - end - fun extract_clause_sequence output = let val tokens_of = String.tokens (not o Char.isAlphaNum) @@ -694,8 +227,6 @@ max_new_relevant_facts_per_iter (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t - val (internal_thm_names, formulas) = - prepare_formulas ctxt full_types hyp_ts concl_t the_axioms (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -760,9 +291,10 @@ known_failures output in (output, msecs, proof, outcome) end val readable_names = debug andalso overlord - val (pool, conjecture_offset) = - write_tptp_file thy readable_names explicit_forall full_types - explicit_apply probfile formulas + val (problem, pool, conjecture_offset, axiom_names) = + prepare_problem ctxt readable_names explicit_forall full_types + explicit_apply hyp_ts concl_t the_axioms + val _ = File.write_list probfile (strings_for_tptp_problem problem) val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |> map single @@ -773,7 +305,7 @@ |> (fn (output, msecs, proof, outcome) => (output, msecs0 + msecs, proof, outcome)) | result => result) - in ((pool, conjecture_shape), result) end + in ((pool, conjecture_shape, axiom_names), result) end else error ("Bad executable: " ^ Path.implode command ^ ".") @@ -787,24 +319,24 @@ else File.write (Path.explode (Path.implode probfile ^ "_proof")) output - val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = + val ((pool, conjecture_shape, axiom_names), + (output, msecs, proof, outcome)) = with_path cleanup export run_on (prob_pathname subgoal) - val (conjecture_shape, internal_thm_names) = + val (conjecture_shape, axiom_names) = repair_conjecture_shape_and_theorem_names output conjecture_shape - internal_thm_names + axiom_names val (message, used_thm_names) = case outcome of NONE => proof_text isar_proof (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (full_types, minimize_command, proof, internal_thm_names, th, - subgoal) + (full_types, minimize_command, proof, axiom_names, th, subgoal) | SOME failure => (string_for_failure failure ^ "\n", []) in {outcome = outcome, message = message, pool = pool, used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, - output = output, proof = proof, internal_thm_names = internal_thm_names, + output = output, proof = proof, axiom_names = axiom_names, conjecture_shape = conjecture_shape} end diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Mon Aug 09 12:05:48 2010 +0200 @@ -0,0 +1,174 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML + Author: Philipp Meyer, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Minimization of theorem list for Metis using automatic theorem provers. +*) + +signature SLEDGEHAMMER_FACT_MINIMIZE = +sig + type params = Sledgehammer.params + + val minimize_theorems : + params -> int -> int -> Proof.state -> (string * thm list) list + -> (string * thm list) list option * string + val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit +end; + +structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE = +struct + +open ATP_Systems +open Sledgehammer_Util +open Sledgehammer_Fact_Filter +open Sledgehammer_Proof_Reconstruct +open Sledgehammer + +(* wrapper for calling external prover *) + +fun string_for_failure Unprovable = "Unprovable." + | string_for_failure TimedOut = "Timed out." + | string_for_failure _ = "Unknown error." + +fun n_theorems name_thms_pairs = + let val n = length name_thms_pairs in + string_of_int n ^ " theorem" ^ plural_s n ^ + (if n > 0 then + ": " ^ space_implode " " + (name_thms_pairs + |> map (perhaps (try (unprefix chained_prefix))) + |> sort_distinct string_ord) + else + "") + end + +fun test_theorems ({debug, verbose, overlord, atps, full_types, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, isar_shrink_factor, + ...} : params) + (prover : prover) explicit_apply timeout subgoal state + name_thms_pairs = + let + val _ = + priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") + val params = + {debug = debug, verbose = verbose, overlord = overlord, atps = atps, + full_types = full_types, explicit_apply = explicit_apply, + relevance_threshold = relevance_threshold, + relevance_convergence = relevance_convergence, + theory_relevant = theory_relevant, defs_relevant = defs_relevant, + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + timeout = timeout, minimize_timeout = timeout} + val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs + val {context = ctxt, facts, goal} = Proof.goal state + val problem = + {subgoal = subgoal, goal = (ctxt, (facts, goal)), + relevance_override = {add = [], del = [], only = false}, + axioms = SOME axioms} + val result as {outcome, used_thm_names, ...} = + prover params (K "") problem + in + priority (case outcome of + NONE => + if length used_thm_names = length name_thms_pairs then + "Found proof." + else + "Found proof with " ^ n_theorems used_thm_names ^ "." + | SOME failure => string_for_failure failure); + result + end + +(* minimalization of thms *) + +fun filter_used_facts used = + filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) + +fun sublinear_minimize _ [] p = p + | sublinear_minimize test (x :: xs) (seen, result) = + case test (xs @ seen) of + result as {outcome = NONE, proof, used_thm_names, ...} + : prover_result => + sublinear_minimize test (filter_used_facts used_thm_names xs) + (filter_used_facts used_thm_names seen, result) + | _ => sublinear_minimize test xs (x :: seen, result) + +(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer + preprocessing time is included in the estimate below but isn't part of the + timeout. *) +val fudge_msecs = 250 + +fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." + | minimize_theorems + (params as {debug, verbose, overlord, atps as atp :: _, full_types, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, isar_shrink_factor, + minimize_timeout, ...}) + i n state name_thms_pairs = + let + val thy = Proof.theory_of state + val prover = get_prover_fun thy atp + val msecs = Time.toMilliseconds minimize_timeout + val _ = + priority ("Sledgehammer minimize: ATP " ^ quote atp ^ + " with a time limit of " ^ string_of_int msecs ^ " ms.") + val {context = ctxt, goal, ...} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i + val explicit_apply = + not (forall (Meson.is_fol_term thy) + (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs)) + fun do_test timeout = + test_theorems params prover explicit_apply timeout i state + val timer = Timer.startRealTimer () + in + (case do_test minimize_timeout name_thms_pairs of + result as {outcome = NONE, pool, used_thm_names, + conjecture_shape, ...} => + let + val time = Timer.checkRealTimer timer + val new_timeout = + Int.min (msecs, Time.toMilliseconds time + fudge_msecs) + |> Time.fromMilliseconds + val (min_thms, {proof, axiom_names, ...}) = + sublinear_minimize (do_test new_timeout) + (filter_used_facts used_thm_names name_thms_pairs) ([], result) + val n = length min_thms + val _ = priority (cat_lines + ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ + (case filter (String.isPrefix chained_prefix o fst) min_thms of + [] => "" + | chained => " (including " ^ Int.toString (length chained) ^ + " chained)") ^ ".") + in + (SOME min_thms, + proof_text isar_proof + (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) + (full_types, K "", proof, axiom_names, goal, i) |> fst) + end + | {outcome = SOME TimedOut, ...} => + (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {outcome = SOME UnknownError, ...} => + (* Failure sometimes mean timeout, unfortunately. *) + (NONE, "Failure: No proof was found with the current time limit. You \ + \can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {message, ...} => (NONE, "ATP error: " ^ message)) + handle ERROR msg => (NONE, "Error: " ^ msg) + end + +fun run_minimize params i refs state = + let + val ctxt = Proof.context_of state + val chained_ths = #facts (Proof.goal state) + val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs + in + case subgoal_count state of + 0 => priority "No subgoal!" + | n => + (kill_atps (); + priority (#2 (minimize_theorems params i n state name_thms_pairs))) + end + +end; diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon Aug 09 11:05:45 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML - Author: Philipp Meyer, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -Minimization of theorem list for Metis using automatic theorem provers. -*) - -signature SLEDGEHAMMER_FACT_MINIMIZER = -sig - type params = Sledgehammer.params - - val minimize_theorems : - params -> int -> int -> Proof.state -> (string * thm list) list - -> (string * thm list) list option * string - val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit -end; - -structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = -struct - -open ATP_Systems -open Sledgehammer_Util -open Sledgehammer_Fact_Filter -open Sledgehammer_Proof_Reconstruct -open Sledgehammer - -(* wrapper for calling external prover *) - -fun string_for_failure Unprovable = "Unprovable." - | string_for_failure TimedOut = "Timed out." - | string_for_failure _ = "Unknown error." - -fun n_theorems name_thms_pairs = - let val n = length name_thms_pairs in - string_of_int n ^ " theorem" ^ plural_s n ^ - (if n > 0 then - ": " ^ space_implode " " - (name_thms_pairs - |> map (perhaps (try (unprefix chained_prefix))) - |> sort_distinct string_ord) - else - "") - end - -fun test_theorems ({debug, verbose, overlord, atps, full_types, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, - ...} : params) - (prover : prover) explicit_apply timeout subgoal state - name_thms_pairs = - let - val _ = - priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") - val params = - {debug = debug, verbose = verbose, overlord = overlord, atps = atps, - full_types = full_types, explicit_apply = explicit_apply, - relevance_threshold = relevance_threshold, - relevance_convergence = relevance_convergence, - theory_relevant = theory_relevant, defs_relevant = defs_relevant, - isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, - timeout = timeout, minimize_timeout = timeout} - val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val {context = ctxt, facts, goal} = Proof.goal state - val problem = - {subgoal = subgoal, goal = (ctxt, (facts, goal)), - relevance_override = {add = [], del = [], only = false}, - axioms = SOME axioms} - val result as {outcome, used_thm_names, ...} = - prover params (K "") problem - in - priority (case outcome of - NONE => - if length used_thm_names = length name_thms_pairs then - "Found proof." - else - "Found proof with " ^ n_theorems used_thm_names ^ "." - | SOME failure => string_for_failure failure); - result - end - -(* minimalization of thms *) - -fun filter_used_facts used = - filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) - -fun sublinear_minimize _ [] p = p - | sublinear_minimize test (x :: xs) (seen, result) = - case test (xs @ seen) of - result as {outcome = NONE, proof, used_thm_names, ...} - : prover_result => - sublinear_minimize test (filter_used_facts used_thm_names xs) - (filter_used_facts used_thm_names seen, result) - | _ => sublinear_minimize test xs (x :: seen, result) - -(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer - preprocessing time is included in the estimate below but isn't part of the - timeout. *) -val fudge_msecs = 250 - -fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." - | minimize_theorems - (params as {debug, verbose, overlord, atps as atp :: _, full_types, - relevance_threshold, relevance_convergence, theory_relevant, - defs_relevant, isar_proof, isar_shrink_factor, - minimize_timeout, ...}) - i n state name_thms_pairs = - let - val thy = Proof.theory_of state - val prover = get_prover_fun thy atp - val msecs = Time.toMilliseconds minimize_timeout - val _ = - priority ("Sledgehammer minimizer: ATP " ^ quote atp ^ - " with a time limit of " ^ string_of_int msecs ^ " ms.") - val {context = ctxt, goal, ...} = Proof.goal state - val (_, hyp_ts, concl_t) = strip_subgoal goal i - val explicit_apply = - not (forall (Meson.is_fol_term thy) - (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs)) - fun do_test timeout = - test_theorems params prover explicit_apply timeout i state - val timer = Timer.startRealTimer () - in - (case do_test minimize_timeout name_thms_pairs of - result as {outcome = NONE, pool, used_thm_names, - conjecture_shape, ...} => - let - val time = Timer.checkRealTimer timer - val new_timeout = - Int.min (msecs, Time.toMilliseconds time + fudge_msecs) - |> Time.fromMilliseconds - val (min_thms, {proof, internal_thm_names, ...}) = - sublinear_minimize (do_test new_timeout) - (filter_used_facts used_thm_names name_thms_pairs) ([], result) - val n = length min_thms - val _ = priority (cat_lines - ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ - (case filter (String.isPrefix chained_prefix o fst) min_thms of - [] => "" - | chained => " (including " ^ Int.toString (length chained) ^ - " chained)") ^ ".") - in - (SOME min_thms, - proof_text isar_proof - (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (full_types, K "", proof, internal_thm_names, goal, i) |> fst) - end - | {outcome = SOME TimedOut, ...} => - (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {outcome = SOME UnknownError, ...} => - (* Failure sometimes mean timeout, unfortunately. *) - (NONE, "Failure: No proof was found with the current time limit. You \ - \can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {message, ...} => (NONE, "ATP error: " ^ message)) - handle ERROR msg => (NONE, "Error: " ^ msg) - end - -fun run_minimizer params i refs state = - let - val ctxt = Proof.context_of state - val chained_ths = #facts (Proof.goal state) - val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs - in - case subgoal_count state of - 0 => priority "No subgoal!" - | n => - (kill_atps (); - priority (#2 (minimize_theorems params i n state name_thms_pairs))) - end - -end; diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 09 12:05:48 2010 +0200 @@ -20,7 +20,7 @@ open ATP_Systems open Sledgehammer_Util open Sledgehammer -open Sledgehammer_Fact_Minimizer +open Sledgehammer_Fact_Minimize (** Sledgehammer commands **) @@ -226,9 +226,9 @@ (minimize_command override_params i) state end else if subcommand = minimizeN then - run_minimizer (get_params thy (map (apfst minimizize_raw_param_name) - override_params)) - (the_default 1 opt_i) (#add relevance_override) state + run_minimize (get_params thy (map (apfst minimizize_raw_param_name) + override_params)) + (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = available_atpsN then diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 09 11:05:45 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 09 12:05:48 2010 +0200 @@ -10,12 +10,6 @@ sig type minimize_command = string list -> string - val axiom_prefix : string - val conjecture_prefix : string - val helper_prefix : string - val class_rel_clause_prefix : string - val arity_clause_prefix : string - val tfrees_name : string val metis_line: bool -> int -> int -> string list -> string val metis_proof_text: bool * minimize_command * string * string vector * thm * int @@ -37,16 +31,10 @@ open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter +open Sledgehammer_Translate type minimize_command = string list -> string -val axiom_prefix = "ax_" -val conjecture_prefix = "conj_" -val helper_prefix = "help_" -val class_rel_clause_prefix = "clrel_"; -val arity_clause_prefix = "arity_" -val tfrees_name = "tfrees" - (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) fun s_not @{const False} = @{const True} @@ -71,9 +59,9 @@ fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) fun index_in_shape x = find_index (exists (curry (op =) x)) -fun is_axiom_number thm_names num = - num > 0 andalso num <= Vector.length thm_names andalso - Vector.sub (thm_names, num - 1) <> "" +fun is_axiom_number axiom_names num = + num > 0 andalso num <= Vector.length axiom_names andalso + Vector.sub (axiom_names, num - 1) <> "" fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -491,10 +479,10 @@ (* Discard axioms; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) fun add_line _ _ (line as Definition _) lines = line :: lines - | add_line conjecture_shape thm_names (Inference (num, t, [])) lines = + | add_line conjecture_shape axiom_names (Inference (num, t, [])) lines = (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or definitions. *) - if is_axiom_number thm_names num then + if is_axiom_number axiom_names num then (* Axioms are not proof lines. *) if is_only_type_information t then map (replace_deps_in_line (num, [])) lines @@ -540,10 +528,10 @@ fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = (j, line :: map (replace_deps_in_line (num, [])) lines) - | add_desired_line isar_shrink_factor conjecture_shape thm_names frees + | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, - if is_axiom_number thm_names num orelse + if is_axiom_number axiom_names num orelse is_conjecture_number conjecture_shape num orelse (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso @@ -562,16 +550,18 @@ (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where the first number (108) is extracted. For Vampire, we look for "108. ... [input]". *) -fun used_facts_in_atp_proof thm_names atp_proof = +fun used_facts_in_atp_proof axiom_names atp_proof = let fun axiom_name num = let val j = Int.fromString num |> the_default ~1 in - if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1)) - else NONE + if is_axiom_number axiom_names j then + SOME (Vector.sub (axiom_names, j - 1)) + else + NONE end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") - val thm_name_list = Vector.foldr (op ::) [] thm_names + val thm_name_list = Vector.foldr (op ::) [] axiom_names fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) = (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of SOME name => @@ -617,16 +607,16 @@ val unprefix_chained = perhaps (try (unprefix chained_prefix)) -fun used_facts thm_names = - used_facts_in_atp_proof thm_names +fun used_facts axiom_names = + used_facts_in_atp_proof axiom_names #> List.partition (String.isPrefix chained_prefix) #>> map (unprefix chained_prefix) #> pairself (sort_distinct string_ord) -fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal, - i) = +fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, + goal, i) = let - val (chained_lemmas, other_lemmas) = used_facts thm_names atp_proof + val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof val lemmas = other_lemmas @ chained_lemmas val n = Logic.count_prems (prop_of goal) in @@ -656,9 +646,9 @@ fun smart_case_split [] facts = ByMetis facts | smart_case_split proofs facts = CaseSplit (proofs, facts) -fun add_fact_from_dep thm_names num = - if is_axiom_number thm_names num then - apsnd (insert (op =) (Vector.sub (thm_names, num - 1))) +fun add_fact_from_dep axiom_names num = + if is_axiom_number axiom_names num then + apsnd (insert (op =) (Vector.sub (axiom_names, num - 1))) else apfst (insert (op =) (raw_prefix, num)) @@ -667,27 +657,27 @@ fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2) | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) - | step_for_line thm_names j (Inference (num, t, deps)) = + | step_for_line axiom_names j (Inference (num, t, deps)) = Have (if j = 1 then [Show] else [], (raw_prefix, num), forall_vars t, - ByMetis (fold (add_fact_from_dep thm_names) deps ([], []))) + ByMetis (fold (add_fact_from_dep axiom_names) deps ([], []))) fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor - atp_proof conjecture_shape thm_names params frees = + atp_proof conjecture_shape axiom_names params frees = let val lines = atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof pool |> sort (int_ord o pairself raw_step_number) |> decode_lines ctxt full_types tfrees - |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names) + |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor - conjecture_shape thm_names frees) + conjecture_shape axiom_names frees) |> snd in (if null params then [] else [Fix params]) @ - map2 (step_for_line thm_names) (length lines downto 1) lines + map2 (step_for_line axiom_names) (length lines downto 1) lines end (* When redirecting proofs, we keep information about the labels seen so far in @@ -995,8 +985,8 @@ in do_proof end fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) - (other_params as (full_types, _, atp_proof, thm_names, goal, - i)) = + (other_params as (full_types, _, atp_proof, axiom_names, + goal, i)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal i val frees = fold Term.add_frees (concl_t :: hyp_ts) [] @@ -1005,7 +995,7 @@ val (one_line_proof, lemma_names) = metis_proof_text other_params fun isar_proof_for () = case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor - atp_proof conjecture_shape thm_names params + atp_proof conjecture_shape axiom_names params frees |> redirect_proof conjecture_shape hyp_ts concl_t |> kill_duplicate_assumptions_in_proof diff -r 601b7972eef2 -r 319c59682c51 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 09 12:05:48 2010 +0200 @@ -0,0 +1,505 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Translation of HOL to FOL. +*) + +signature SLEDGEHAMMER_TRANSLATE = +sig + type 'a problem = 'a ATP_Problem.problem + + val axiom_prefix : string + val conjecture_prefix : string + val helper_prefix : string + val class_rel_clause_prefix : string + val arity_clause_prefix : string + val tfrees_name : string + val prepare_problem : + Proof.context -> bool -> bool -> bool -> bool -> term list -> term + -> (string * thm) list + -> string problem * string Symtab.table * int * string Vector.vector +end; + +structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = +struct + +open ATP_Problem +open Metis_Clauses +open Sledgehammer_Util + +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" +val helper_prefix = "help_" +val class_rel_clause_prefix = "clrel_"; +val arity_clause_prefix = "arity_" +val tfrees_name = "tfrees" + +(* Freshness almost guaranteed! *) +val sledgehammer_weak_prefix = "Sledgehammer:" + +datatype fol_formula = + FOLFormula of {name: string, + kind: kind, + combformula: (name, combterm) formula, + ctypes_sorts: typ list} + +fun mk_anot phi = AConn (ANot, [phi]) +fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) +fun mk_ahorn [] phi = phi + | mk_ahorn (phi :: phis) psi = + AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) + +fun combformula_for_prop thy = + let + val do_term = combterm_from_term thy + fun do_quant bs q s T t' = + do_formula ((s, T) :: bs) t' + #>> (fn phi => AQuant (q, [`make_bound_var s], phi)) + and do_conn bs c t1 t2 = + do_formula bs t1 ##>> do_formula bs t2 + #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) + and do_formula bs t = + case t of + @{const Not} $ t1 => + do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) + | Const (@{const_name All}, _) $ Abs (s, T, t') => + do_quant bs AForall s T t' + | Const (@{const_name Ex}, _) $ Abs (s, T, t') => + do_quant bs AExists s T t' + | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2 + | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2 + | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2 + | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => + do_conn bs AIff t1 t2 + | _ => (fn ts => do_term bs (Envir.eta_contract t) + |>> AAtom ||> union (op =) ts) + in do_formula [] end + +(* Converts an elim-rule into an equivalent theorem that does not have the + predicate variable. Leaves other theorems unchanged. We simply instantiate + the conclusion variable to False. (Cf. "transform_elim_term" in + "ATP_Systems".) *) +fun transform_elim_term t = + case Logic.strip_imp_concl t of + @{const Trueprop} $ Var (z, @{typ bool}) => + subst_Vars [(z, @{const False})] t + | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t + | _ => t + +fun presimplify_term thy = + Skip_Proof.make_thm thy + #> Meson.presimplify + #> prop_of + +fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString 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 introduce_combinators_in_term ctxt kind t = + let + val thy = ProofContext.theory_of ctxt + fun aux Ts t = + case t of + @{const Not} $ t1 => @{const Not} $ aux Ts t1 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => + t0 $ Abs (s, T, aux (T :: Ts) t') + | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 + | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _]))) + $ t1 $ t2 => + t0 $ aux Ts t1 $ aux Ts t2 + | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then + t + else + let + val t = t |> conceal_bounds Ts + |> Envir.eta_contract + val ([t], ctxt') = Variable.import_terms true [t] ctxt + in + t |> cterm_of thy + |> Clausifier.introduce_combinators_in_cterm + |> singleton (Variable.export ctxt' ctxt) + |> prop_of |> Logic.dest_equals |> snd + |> reveal_bounds Ts + end + in t |> not (Meson.is_fol_term thy t) ? aux [] end + handle THM _ => + (* A type variable of sort "{}" will make abstraction fail. *) + case kind of + Axiom => HOLogic.true_const + | Conjecture => HOLogic.false_const + +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the + same in Sledgehammer to prevent the discovery of unreplable proofs. *) +fun freeze_term t = + let + fun aux (t $ u) = aux t $ aux u + | aux (Abs (s, T, t)) = Abs (s, T, aux t) + | aux (Var ((s, i), T)) = + Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) + | aux t = t + in t |> exists_subterm is_Var t ? aux end + +(* making axiom and conjecture formulas *) +fun make_formula ctxt presimp (name, kind, t) = + let + val thy = ProofContext.theory_of ctxt + val t = t |> transform_elim_term + |> Object_Logic.atomize_term thy + val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop + |> extensionalize_term + |> presimp ? presimplify_term thy + |> perhaps (try (HOLogic.dest_Trueprop)) + |> introduce_combinators_in_term ctxt kind + |> kind = Conjecture ? freeze_term + val (combformula, ctypes_sorts) = combformula_for_prop thy t [] + in + FOLFormula {name = name, combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts} + end + +fun make_axiom ctxt presimp (name, th) = + (name, make_formula ctxt presimp (name, Axiom, prop_of th)) +fun make_conjectures ctxt ts = + map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t)) + (0 upto length ts - 1) ts + +(** Helper facts **) + +fun count_combterm (CombConst ((s, _), _, _)) = + Symtab.map_entry s (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2] +fun count_combformula (AQuant (_, _, phi)) = count_combformula phi + | count_combformula (AConn (_, phis)) = fold count_combformula phis + | count_combformula (AAtom tm) = count_combterm tm +fun count_fol_formula (FOLFormula {combformula, ...}) = + count_combformula combformula + +val optional_helpers = + [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}), + (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}), + (["c_COMBS"], @{thms COMBS_def})] +val optional_typed_helpers = + [(["c_True", "c_False"], @{thms True_or_False}), + (["c_If"], @{thms if_True if_False True_or_False})] +val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} + +val init_counters = + Symtab.make (maps (maps (map (rpair 0) o fst)) + [optional_helpers, optional_typed_helpers]) + +fun get_helper_facts ctxt is_FO full_types conjectures axioms = + let + val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters + fun is_needed c = the (Symtab.lookup ct c) > 0 + in + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, ths) => + if exists is_needed ss then map (`Thm.get_name_hint) ths + else [])) @ + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) + |> map (snd o make_axiom ctxt false) + end + +fun meta_not t = @{const "==>"} $ t $ @{prop False} + +fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = + let + val thy = ProofContext.theory_of ctxt + val axiom_ts = map (prop_of o snd) axioms + val hyp_ts = + if null hyp_ts then + [] + else + (* Remove existing axioms from the conjecture, as this can dramatically + boost an ATP's performance (for some reason). *) + let + val axiom_table = fold (Termtab.update o rpair ()) axiom_ts + Termtab.empty + in hyp_ts |> filter_out (Termtab.defined axiom_table) end + val goal_t = Logic.list_implies (hyp_ts, concl_t) + val is_FO = Meson.is_fol_term thy goal_t + val subs = tfree_classes_of_terms [goal_t] + val supers = tvar_classes_of_terms axiom_ts + val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) + (* TFrees in the conjecture; TVars in the axioms *) + val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt + val (axiom_names, axioms) = + ListPair.unzip (map (make_axiom ctxt true) axioms) + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms + val (supers', arity_clauses) = make_arity_clauses thy tycons supers + val class_rel_clauses = make_class_rel_clauses thy subs supers' + in + (Vector.fromList axiom_names, + (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) + end + +fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) + +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) + +fun fo_literal_for_type_literal (TyLitVar (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + | fo_literal_for_type_literal (TyLitFree (class, name)) = + (true, ATerm (class, [ATerm (name, [])])) + +fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot + +fun fo_term_for_combterm full_types = + let + fun aux top_level u = + let + val (head, args) = strip_combterm_comb u + val (x, ty_args) = + case head of + CombConst (name as (s, s'), _, ty_args) => + if s = "equal" then + (if top_level andalso length args = 2 then name + else ("c_fequal", @{const_name fequal}), []) + else if top_level then + case s of + "c_False" => (("$false", s'), []) + | "c_True" => (("$true", s'), []) + | _ => (name, if full_types then [] else ty_args) + else + (name, if full_types then [] else ty_args) + | CombVar (name, _) => (name, []) + | CombApp _ => raise Fail "impossible \"CombApp\"" + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (aux false) args) + in + if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t + end + in aux true end + +fun formula_for_combformula full_types = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm) + in aux end + +fun formula_for_axiom full_types (FOLFormula {combformula, ctypes_sorts, ...}) = + mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) + (type_literals_for_types ctypes_sorts)) + (formula_for_combformula full_types combformula) + +fun problem_line_for_fact prefix full_types + (formula as FOLFormula {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) + +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, + superclass, ...}) = + let val ty_arg = ATerm (("T", "T"), []) in + Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, + AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), + AAtom (ATerm (superclass, [ty_arg]))])) + end + +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = + (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) + | fo_literal_for_arity_literal (TVarLit (c, sort)) = + (false, ATerm (c, [ATerm (sort, [])])) + +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, + ...}) = + Fof (arity_clause_prefix ^ ascii_of name, Axiom, + mk_ahorn (map (formula_for_fo_literal o apfst not + o fo_literal_for_arity_literal) premLits) + (formula_for_fo_literal + (fo_literal_for_arity_literal conclLit))) + +fun problem_line_for_conjecture full_types + (FOLFormula {name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ name, kind, + formula_for_combformula full_types combformula) + +fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = + map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) + +fun problem_line_for_free_type lit = + Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit)) +fun problem_lines_for_free_types conjectures = + let + val litss = map free_type_literals_for_conjecture conjectures + val lits = fold (union (op =)) litss [] + in map problem_line_for_free_type lits end + +(** "hBOOL" and "hAPP" **) + +type const_info = {min_arity: int, max_arity: int, sub_level: bool} + +fun consider_term top_level (ATerm ((s, _), ts)) = + (if is_tptp_variable s then + I + else + let val n = length ts in + Symtab.map_default + (s, {min_arity = n, max_arity = 0, sub_level = false}) + (fn {min_arity, max_arity, sub_level} => + {min_arity = Int.min (n, min_arity), + max_arity = Int.max (n, max_arity), + sub_level = sub_level orelse not top_level}) + end) + #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (AAtom tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi +fun consider_problem problem = fold (fold consider_problem_line o snd) problem + +fun const_table_for_problem explicit_apply problem = + if explicit_apply then NONE + else SOME (Symtab.empty |> consider_problem problem) + +fun min_arity_of thy full_types NONE s = + (if s = "equal" orelse s = type_wrapper_name orelse + String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s then + 16383 (* large number *) + else if full_types then + 0 + else case strip_prefix_and_undo_ascii const_prefix s of + SOME s' => num_type_args thy (invert_const s') + | NONE => 0) + | min_arity_of _ _ (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME ({min_arity, ...} : const_info) => min_arity + | NONE => 0 + +fun full_type_of (ATerm ((s, _), [ty, _])) = + if s = type_wrapper_name then ty else raise Fail "expected type wrapper" + | full_type_of _ = raise Fail "expected type wrapper" + +fun list_hAPP_rev _ t1 [] = t1 + | list_hAPP_rev NONE t1 (t2 :: ts2) = + ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) + | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = + let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, + [full_type_of t2, ty]) in + ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) + end + +fun repair_applications_in_term thy full_types const_tab = + let + fun aux opt_ty (ATerm (name as (s, _), ts)) = + if s = type_wrapper_name then + case ts of + [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) + | _ => raise Fail "malformed type wrapper" + else + let + val ts = map (aux NONE) ts + val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts + in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end + in aux NONE end + +fun boolify t = ATerm (`I "hBOOL", [t]) + +(* 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_predicate NONE s = + s = "equal" orelse String.isPrefix type_const_prefix s orelse + String.isPrefix class_prefix s + | is_predicate (SOME the_const_tab) s = + case Symtab.lookup the_const_tab s of + SOME {min_arity, max_arity, sub_level} => + not sub_level andalso min_arity = max_arity + | NONE => false + +fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) = + if s = type_wrapper_name then + case ts of + [_, t' as ATerm ((s', _), _)] => + if is_predicate const_tab s' then t' else boolify t + | _ => raise Fail "malformed type wrapper" + else + t |> not (is_predicate const_tab s) ? boolify + +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_tptp_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (q, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (AAtom tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (AAtom tm) = + AAtom (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +fun repair_problem_with_const_table thy = + map o apsnd o map ooo repair_problem_line thy + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types + (const_table_for_problem explicit_apply problem) problem + +fun prepare_problem ctxt readable_names explicit_forall full_types + explicit_apply hyp_ts concl_t axiom_ts = + let + val thy = ProofContext.theory_of ctxt + val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, + arity_clauses)) = + prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts + val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms + val helper_lines = + map (problem_line_for_fact helper_prefix full_types) helper_facts + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures + val class_rel_lines = + map problem_line_for_class_rel_clause class_rel_clauses + val arity_lines = map problem_line_for_arity_clause arity_clauses + (* Reordering these might or might not confuse the proof reconstruction + code or the SPASS Flotter hack. *) + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply + val (problem, pool) = nice_tptp_problem readable_names problem + val conjecture_offset = + length axiom_lines + length class_rel_lines + length arity_lines + + length helper_lines + in + (problem, + case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset, axiom_names) + end + +end;