# HG changeset patch # User blanchet # Date 1321391619 -3600 # Node ID b216dc1b36308cee7a909905776a5ac498e4dd8d # Parent 6975db7fd6f0f2ab056c5a661072cf92d24fa53e started implementing lambda-lifting in Metis diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/TPTP/atp_export.ML Tue Nov 15 22:13:39 2011 +0100 @@ -175,7 +175,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val facts = facts_of thy - val (atp_problem, _, _, _, _, _, _) = + val (atp_problem, _, _, _, _, _, _, _) = facts |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100 @@ -45,7 +45,7 @@ val const_prefix : string val type_const_prefix : string val class_prefix : string - val polymorphic_free_prefix : string + val lambda_lifted_prefix : string val skolem_const_prefix : string val old_skolem_const_prefix : string val new_skolem_const_prefix : string @@ -87,6 +87,8 @@ val is_type_enc_fairly_sound : type_enc -> bool val type_enc_from_string : soundness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc + val lift_lambdas : + Proof.context -> type_enc -> term list -> term list * term list val mk_aconns : connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula val unmangled_const : string -> string * (string, 'b) ho_term list @@ -98,7 +100,8 @@ -> bool -> string -> bool -> bool -> term list -> term -> ((string * locality) * term) list -> string problem * string Symtab.table * int * int - * (string * locality) list vector * int list * int Symtab.table + * (string * locality) list vector * int list * (string * term) list + * int Symtab.table val atp_problem_weights : string problem -> (string * real) list end; @@ -140,7 +143,8 @@ val simple_type_prefix = "s_" val class_prefix = "cl_" -val polymorphic_free_prefix = "poly_free" +val lambda_lifted_prefix = "lambda" +val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "_poly" val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko" val old_skolem_const_prefix = skolem_const_prefix ^ "o" @@ -494,7 +498,7 @@ atomic_types_of T) | iterm_from_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, - if String.isPrefix polymorphic_free_prefix s then [T] else []), + if String.isPrefix lambda_lifted_poly_prefix s then [T] else []), atomic_types_of T) | iterm_from_term _ format _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then @@ -653,10 +657,10 @@ fun lift_lambdas ctxt type_enc = map (close_form o Envir.eta_contract) #> rpair ctxt #-> Lambda_Lifting.lift_lambdas - (if polymorphism_of_type_enc type_enc = Polymorphic then - SOME polymorphic_free_prefix - else - NONE) + (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then + lambda_lifted_poly_prefix + else + lambda_lifted_prefix)) Lambda_Lifting.is_quantifier #> fst @@ -1117,7 +1121,7 @@ do_cheaply_conceal_lambdas Ts t1 $ do_cheaply_conceal_lambdas Ts t2 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) = - Free (polymorphic_free_prefix ^ serial_string (), + Free (lambda_lifted_poly_prefix ^ serial_string (), T --> fastype_of1 (T :: Ts, t)) | do_cheaply_conceal_lambdas _ t = t @@ -1630,7 +1634,7 @@ | add (Const x) = x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert) | add (Free (s, T)) = - if String.isPrefix polymorphic_free_prefix s then + if String.isPrefix lambda_lifted_poly_prefix s then T |> fold_type_constrs set_insert else I @@ -1641,6 +1645,17 @@ fun type_constrs_of_terms thy ts = Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) +val extract_lambda_def = + let + fun extr [] (@{const Trueprop} $ t) = extr [] t + | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) = + extr ((s, T) :: bs) t + | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) = + (t |> head_of |> dest_Free |> fst, + fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u) + | extr _ _ = raise Fail "malformed lifted lambda" + in extr [] end + fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts = let @@ -1657,7 +1672,7 @@ map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)] |> map (apsnd freeze_term) |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts) - val ((conjs, facts), lambdas) = + val ((conjs, facts), lambda_facts) = if preproc then conjs @ facts |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts))) @@ -1672,8 +1687,10 @@ make_fact ctxt format type_enc true (name, t) |> Option.map (pair name)) |> ListPair.unzip - val lambdas = - lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd) + val lifted = lambda_facts |> map (extract_lambda_def o snd o snd) + val lambda_facts = + lambda_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 @@ -1683,8 +1700,8 @@ else make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers in - (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas, - class_rel_clauses, arity_clauses) + (fact_names |> map single, union (op =) subs supers, conjs, + facts @ lambda_facts, class_rel_clauses, arity_clauses, lifted) end val type_guard = `(make_fixed_const NONE) type_guard_name @@ -2095,8 +2112,10 @@ | NONE => case strip_prefix_and_unascii fixed_var_prefix s of SOME s' => - if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a]) - else raise Fail "unexpected type arguments to free variable" + if String.isPrefix lambda_lifted_poly_prefix s' then + (tvar_a, [tvar_a]) + else + raise Fail "unexpected type arguments to free variable" | NONE => raise Fail "unexpected type arguments" in Decl (sym_decl_prefix ^ s, (s, s'), @@ -2317,7 +2336,8 @@ else error ("Unknown lambda translation method: " ^ quote lambda_trans ^ ".") - val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) = + val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, + lifted) = translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts val sym_tab = @@ -2390,6 +2410,7 @@ offset_of_heading_in_problem factsN problem 0, fact_names |> Vector.fromList, typed_helpers, + lifted, Symtab.empty |> Symtab.fold add_sym_ary sym_tab) end diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100 @@ -15,7 +15,8 @@ val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool val ss_only : thm list -> simpset val cnf_axiom : - Proof.context -> bool -> int -> thm -> (thm * term) option * thm list + Proof.context -> bool -> bool -> int -> thm + -> (thm * term) option * thm list end; structure Meson_Clausify : MESON_CLAUSIFY = @@ -364,7 +365,7 @@ end (* Convert a theorem to CNF, with additional premises due to skolemization. *) -fun cnf_axiom ctxt0 new_skolemizer ax_no th = +fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th = let val thy = Proof_Context.theory_of ctxt0 val choice_ths = choice_theorems thy @@ -385,7 +386,7 @@ (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) ##> (term_of #> HOLogic.dest_Trueprop #> singleton (Variable.export_terms ctxt ctxt0))), - cnf_ths |> map (introduce_combinators_in_theorem + cnf_ths |> map (combinators ? introduce_combinators_in_theorem #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |> Variable.export ctxt ctxt0 |> finish_cnf diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Meson/meson_tactic.ML --- a/src/HOL/Tools/Meson/meson_tactic.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Meson/meson_tactic.ML Tue Nov 15 22:13:39 2011 +0100 @@ -18,7 +18,7 @@ fun meson_general_tac ctxt ths = let val ctxt' = put_claset HOL_cs ctxt - in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end + in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end val setup = Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100 @@ -14,11 +14,12 @@ exception METIS of string * string val hol_clause_from_metis : - Proof.context -> type_enc -> int Symtab.table -> (string * term) list - -> Metis_Thm.thm -> term + Proof.context -> type_enc -> int Symtab.table + -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val replay_one_inference : - Proof.context -> type_enc -> (string * term) list -> int Symtab.table + Proof.context -> type_enc + -> (string * term) list * (string * term) list -> int Symtab.table -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : @@ -55,24 +56,24 @@ | atp_clause_from_metis type_enc lits = lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr -fun reveal_old_skolems_and_infer_types ctxt old_skolems = - map (reveal_old_skolem_terms old_skolems) +fun polish_hol_terms ctxt (lifted, old_skolems) = + map (reveal_lambda_lifted lifted + #> reveal_old_skolem_terms old_skolems) #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) -fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems = +fun hol_clause_from_metis ctxt type_enc sym_tab concealed = Metis_Thm.clause #> Metis_LiteralSet.toList #> atp_clause_from_metis type_enc #> prop_from_atp ctxt false sym_tab - #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems) + #> singleton (polish_hol_terms ctxt concealed) -fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms = +fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms = let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms val _ = trace_msg ctxt (fn () => " calling type inference:") val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = - ts |> reveal_old_skolems_and_infer_types ctxt old_skolems + val ts' = ts |> polish_hol_terms ctxt concealed val _ = app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) @@ -114,10 +115,10 @@ val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] in cterm_instantiate substs th end; -fun assume_inference ctxt type_enc old_skolems sym_tab atom = +fun assume_inference ctxt type_enc concealed sym_tab atom = inst_excluded_middle (Proof_Context.theory_of ctxt) - (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) + (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)) (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying @@ -125,14 +126,14 @@ sorts. Instead we try to arrange that new TVars are distinct and that types can be inferred from terms. *) -fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th = +fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th = let val thy = Proof_Context.theory_of ctxt val i_th = lookth th_pairs th val i_th_vars = Term.add_vars (prop_of i_th) [] fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) fun subst_translation (x,y) = let val v = find_var x - (* We call "reveal_old_skolems_and_infer_types" below. *) + (* We call "polish_hol_terms" below. *) val t = hol_term_from_metis ctxt type_enc sym_tab y in SOME (cterm_of thy (Var v), t) end handle Option.Option => @@ -156,7 +157,7 @@ val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) val (vars, tms) = ListPair.unzip (map_filter subst_translation substs) - ||> reveal_old_skolems_and_infer_types ctxt old_skolems + ||> polish_hol_terms ctxt concealed val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) val substs' = ListPair.zip (vars, map ctm_of tms) val _ = trace_msg ctxt (fn () => @@ -258,7 +259,7 @@ (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) val select_literal = negate_head oo make_last -fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 = +fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 = let val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => @@ -274,7 +275,7 @@ let val thy = Proof_Context.theory_of ctxt val i_atom = - singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) + singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom) val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) @@ -303,11 +304,11 @@ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; -fun refl_inference ctxt type_enc old_skolems sym_tab t = +fun refl_inference ctxt type_enc concealed sym_tab t = let val thy = Proof_Context.theory_of ctxt val i_t = - singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t + singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end @@ -317,11 +318,11 @@ val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} -fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr = +fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr = let val thy = Proof_Context.theory_of ctxt val m_tm = Metis_Term.Fn atom val [i_atom, i_tm] = - hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr] + hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr] val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls @@ -382,22 +383,22 @@ val factor = Seq.hd o distinct_subgoals_tac -fun one_step ctxt type_enc old_skolems sym_tab th_pairs p = +fun one_step ctxt type_enc concealed sym_tab th_pairs p = case p of (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atom) => - assume_inference ctxt type_enc old_skolems sym_tab f_atom + assume_inference ctxt type_enc concealed sym_tab f_atom | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1 + inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => - resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1 + resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor | (_, Metis_Proof.Refl f_tm) => - refl_inference ctxt type_enc old_skolems sym_tab f_tm + refl_inference ctxt type_enc concealed sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r + equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r fun flexflex_first_order th = case Thm.tpairs_of th of @@ -449,7 +450,7 @@ end end -fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf) +fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf) th_pairs = if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then @@ -465,7 +466,7 @@ (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf) + val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf) |> flexflex_first_order |> resynchronize ctxt fol_th val _ = trace_msg ctxt diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100 @@ -75,9 +75,9 @@ "t => t'", where "t" and "t'" are the same term modulo type tags. In Isabelle, type tags are stripped away, so we are left with "t = t" or "t => t". Type tag idempotence is also handled this way. *) -fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth = +fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth = let val thy = Proof_Context.theory_of ctxt in - case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of + case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of Const (@{const_name HOL.eq}, _) $ _ $ t => let val ct = cterm_of thy t @@ -106,14 +106,15 @@ val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = +fun FOL_SOLVE (type_enc :: fallback_type_syss) lambda_trans ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) val th_cls_pairs = map2 (fn j => fn th => (Thm.get_name_hint th, - Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) + Meson_Clausify.cnf_axiom ctxt new_skolemizer + (lambda_trans = combinatorsN) j th)) (0 upto length ths0 - 1) ths0 val ths = maps (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs @@ -121,10 +122,10 @@ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) val type_enc = type_enc_from_string Sound type_enc - val (sym_tab, axioms, old_skolems) = - prepare_metis_problem ctxt type_enc cls ths + val (sym_tab, axioms, concealed) = + prepare_metis_problem ctxt type_enc lambda_trans cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = - reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth + reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth | get_isa_thm _ (Isa_Raw ith) = ith val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") @@ -148,7 +149,7 @@ val proof = Metis_Proof.proof mth val result = axioms - |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof + |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used @@ -193,12 +194,12 @@ (verbose_warning ctxt ("Falling back on " ^ quote (method_call_for_type_enc fallback_type_syss) ^ "..."); - FOL_SOLVE fallback_type_syss ctxt cls ths0) + FOL_SOLVE fallback_type_syss lambda_trans ctxt cls ths0) -fun neg_clausify ctxt = +fun neg_clausify ctxt combinators = single #> Meson.make_clauses_unsorted ctxt - #> map Meson_Clausify.introduce_combinators_in_theorem + #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem #> Meson.finish_cnf fun preskolem_tac ctxt st0 = @@ -214,16 +215,19 @@ fun generic_metis_tac type_syss ctxt ths i st0 = let + val lambda_trans = Config.get ctxt lambda_translation val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) - fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 + fun tac clause = + resolve_tac (FOL_SOLVE type_syss lambda_trans ctxt clause ths) 1 in if exists_type type_has_top_sort (prop_of st0) then verbose_warning ctxt "Proof state contains the universal sort {}" else (); - Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0 + Meson.MESON (preskolem_tac ctxt) + (maps (neg_clausify ctxt (lambda_trans = combinatorsN))) tac ctxt i st0 end fun metis_tac [] = generic_metis_tac partial_type_syss diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100 @@ -23,13 +23,16 @@ val metis_generated_var_prefix : string val trace : bool Config.T val verbose : bool Config.T + val lambda_translation : string Config.T val trace_msg : Proof.context -> (unit -> string) -> unit val verbose_warning : Proof.context -> string -> unit val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list val reveal_old_skolem_terms : (string * term) list -> term -> term + val reveal_lambda_lifted : (string * term) list -> term -> term val prepare_metis_problem : - Proof.context -> type_enc -> thm list -> thm list - -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list + Proof.context -> type_enc -> string -> thm list -> thm list + -> int Symtab.table * (Metis_Thm.thm * isa_thm) list + * ((string * term) list * (string * term) list) end structure Metis_Translate : METIS_TRANSLATE = @@ -48,6 +51,9 @@ val trace = Attrib.setup_config_bool @{binding metis_trace} (K false) val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true) +val lambda_translation = + Attrib.setup_config_string @{binding metis_lambda_translation} + (K combinatorsN) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () fun verbose_warning ctxt msg = @@ -107,6 +113,16 @@ t | t => t) +fun reveal_lambda_lifted lambdas = + map_aterms (fn t as Free (s, _) => + if String.isPrefix lambda_lifted_prefix s then + case AList.lookup (op =) lambdas s of + SOME t => t |> map_types (map_type_tvar (K dummyT)) + | NONE => t + else + t + | t => t) + (* ------------------------------------------------------------------------- *) (* Logic maps manage the interface between HOL and first-order logic. *) @@ -175,7 +191,7 @@ | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula" (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses = +fun prepare_metis_problem ctxt type_enc lambda_trans conj_clauses fact_clauses = let val (conj_clauses, fact_clauses) = if polymorphism_of_type_enc type_enc = Polymorphic then @@ -205,17 +221,18 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o snd) props)) *) - val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN - false false [] @{prop False} props - (* + val (lambda_trans, preproc) = + if lambda_trans = combinatorsN then (no_lambdasN, false) + else (lambda_trans, true) + val (atp_problem, _, _, _, _, _, lifted, sym_tab) = + prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans + false preproc [] @{prop False} props val _ = tracing ("ATP PROBLEM: " ^ - cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) - *) - (* "rev" is for compatibility. *) + cat_lines (lines_for_atp_problem CNF atp_problem)) + (* "rev" is for compatibility with existing proof scripts. *) val axioms = atp_problem |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev - in (sym_tab, axioms, old_skolems) end + in (sym_tab, axioms, (lifted, old_skolems)) end end; diff -r 6975db7fd6f0 -r b216dc1b3630 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 15:38:50 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 15 22:13:39 2011 +0100 @@ -672,7 +672,7 @@ else () val (atp_problem, pool, conjecture_offset, facts_offset, - fact_names, typed_helpers, sym_tab) = + fact_names, typed_helpers, _, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc false (Config.get ctxt atp_lambda_translation) (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t