# HG changeset patch # User boehmes # Date 1311161221 -7200 # Node ID cb7914f6e9b387ec28877ae218e87700e8f8bc6f # Parent 61d432e51aff0be64f3cedc464a3054b32b1802b# Parent 3264fbfd87d6e4ff42123b2687e8a18261c330f1 merged diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 20 13:24:49 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 20 13:27:01 2011 +0200 @@ -373,7 +373,6 @@ Tools/SMT/smt_config.ML \ Tools/SMT/smt_datatypes.ML \ Tools/SMT/smt_failure.ML \ - Tools/SMT/smt_monomorph.ML \ Tools/SMT/smt_normalize.ML \ Tools/SMT/smt_setup_solvers.ML \ Tools/SMT/smt_solver.ML \ diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Wed Jul 20 13:24:49 2011 +0200 +++ b/src/HOL/SMT.thy Wed Jul 20 13:27:01 2011 +0200 @@ -7,10 +7,10 @@ theory SMT imports Record uses + "Tools/lambda_lifting.ML" "Tools/SMT/smt_utils.ML" "Tools/SMT/smt_failure.ML" "Tools/SMT/smt_config.ML" - ("Tools/SMT/smt_monomorph.ML") ("Tools/SMT/smt_builtin.ML") ("Tools/SMT/smt_datatypes.ML") ("Tools/SMT/smt_normalize.ML") @@ -135,7 +135,6 @@ subsection {* Setup *} -use "Tools/SMT/smt_monomorph.ML" use "Tools/SMT/smt_builtin.ML" use "Tools/SMT/smt_datatypes.ML" use "Tools/SMT/smt_normalize.ML" diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Wed Jul 20 13:24:49 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,229 +0,0 @@ -(* Title: HOL/Tools/SMT/smt_monomorph.ML - Author: Sascha Boehme, TU Muenchen - -Monomorphization of theorems, i.e., computation of all (necessary) -instances. This procedure is incomplete in general, but works well for -most practical problems. - -For a list of universally closed theorems (without schematic term -variables), monomorphization computes a list of theorems with schematic -term variables: all polymorphic constants (i.e., constants occurring both -with ground types and schematic type variables) are instantiated with all -(necessary) ground types; thereby theorems containing these constants are -copied. To prevent non-termination, there is an upper limit for the number -of iterations involved in the fixpoint construction. - -The search for instances is performed on the constants with schematic -types, which are extracted from the initial set of theorems. The search -constructs, for each theorem with those constants, a set of substitutions, -which, in the end, is applied to all corresponding theorems. Remaining -schematic type variables are substituted with fresh types. - -Searching for necessary substitutions is an iterative fixpoint -construction: each iteration computes all required instances required by -the ground instances computed in the previous step and which haven't been -found before. Computed substitutions are always nontrivial: schematic type -variables are never mapped to schematic type variables. -*) - -signature SMT_MONOMORPH = -sig - val typ_has_tvars: typ -> bool - val monomorph: ('a * thm) list -> Proof.context -> - ('a * thm) list * Proof.context -end - -structure SMT_Monomorph: SMT_MONOMORPH = -struct - -(* utility functions *) - -fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat) - -fun pair_trans ((x, y), z) = (x, (y, z)) - -val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false) - -val ignored = member (op =) [@{const_name All}, @{const_name Ex}, - @{const_name Let}, @{const_name If}, @{const_name HOL.eq}] - -fun is_const pred (n, T) = not (ignored n) andalso pred T - -fun collect_consts_if pred f = - let - fun collect (@{const SMT.trigger} $ p $ t) = collect_trigger p #> collect t - | collect (t $ u) = collect t #> collect u - | collect (Abs (_, _, t)) = collect t - | collect (Const c) = if is_const pred c then f c else I - | collect _ = I - and collect_trigger t = - let val dest = these o try HOLogic.dest_list - in fold (fold collect_pat o dest) (dest t) end - and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t - | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t - | collect_pat _ = I - in collect o Thm.prop_of end - -val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord) - -fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm [] - -fun add_const_types pred = - collect_consts_if pred (fn (n, T) => Symtab.map_entry n (insert (op =) T)) - -fun incr_indexes ithms = - let - fun inc (i, thm) idx = - ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1) - in fst (fold_map inc ithms 0) end - - - -(* search for necessary substitutions *) - -fun new_substitutions thy limit grounds (n, T) subst instances = - if not (typ_has_tvars T) then ([subst], instances) - else - Symtab.lookup_list grounds n - |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst)) - |> (fn substs => (substs, instances - length substs)) - |>> take limit (* limit the breadth of the search as well as the width *) - |>> cons subst - -fun apply_subst grounds consts subst = - let - fun is_new_ground (n, T) = not (typ_has_tvars T) andalso - not (member (op =) (Symtab.lookup_list grounds n) T) - - fun apply_const (n, T) new_grounds = - let val c = (n, Envir.subst_type subst T) - in - new_grounds - |> is_new_ground c ? Symtab.insert_list (op =) c - |> pair c - end - in fold_map apply_const consts #>> pair subst end - -fun specialize thy limit all_grounds new_grounds scs = - let - fun spec (subst, consts) (next_grounds, instances) = - ([subst], instances) - |> fold_maps (new_substitutions thy limit new_grounds) consts - |>> rpair next_grounds - |>> uncurry (fold_map (apply_subst all_grounds consts)) - |> pair_trans - in - fold_map spec scs #>> (fn scss => - fold (fold (insert (eq_snd (op =)))) scss []) - end - -val limit_reached_warning = "Warning: Monomorphization limit reached" - -fun search_substitutions ctxt limit instances all_grounds new_grounds scss = - let - val thy = Proof_Context.theory_of ctxt - val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds) - val spec = specialize thy limit all_grounds' new_grounds - val (scss', (new_grounds', instances')) = - fold_map spec scss (Symtab.empty, instances) - in - if Symtab.is_empty new_grounds' then scss' - else if limit > 0 andalso instances' > 0 then - search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds' - scss' - else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss') - end - - - -(* instantiation *) - -fun filter_most_specific thy = - let - fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U) - - fun is_trivial subst = Vartab.is_empty subst orelse - forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst) - - fun match general specific = - (case try (fold2 typ_match general specific) Vartab.empty of - NONE => false - | SOME subst => not (is_trivial subst)) - - fun most_specific _ [] = [] - | most_specific css ((ss, cs) :: scs) = - let val substs = most_specific (cs :: css) scs - in - if exists (match cs) css orelse exists (match cs o snd) scs - then substs else ss :: substs - end - - in most_specific [] end - -fun instantiate full (i, thm) substs (ithms, ctxt) = - let - val thy = Proof_Context.theory_of ctxt - - val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) - val (Tenv, ctxt') = - ctxt - |> Variable.invent_types Ss - |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs - - exception PARTIAL_INST of unit - - fun update_subst vT subst = - if full then Vartab.update vT subst - else raise PARTIAL_INST () - - fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U - | replace _ T = T - - fun complete (vT as (v, _)) subst = - subst - |> not (Vartab.defined subst v) ? update_subst vT - |> Vartab.map (K (apsnd (Term.map_atyps (replace vT)))) - - fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) - - fun inst subst = - let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) [] - in SOME (i, Thm.instantiate (cTs, []) thm) end - handle PARTIAL_INST () => NONE - - in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end - - - -(* overall procedure *) - -fun mono_all ctxt polys monos = - let - val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys - - (* all known non-schematic instances of polymorphic constants: find all - names of polymorphic constants, then add all known ground types *) - val grounds = - Symtab.empty - |> fold (fold (fold (Symtab.update o rpair [] o fst) o snd)) scss - |> fold (add_const_types (K true) o snd) monos - |> fold (add_const_types (not o typ_has_tvars) o snd) polys - - val limit = Config.get ctxt SMT_Config.monomorph_limit - val instances = Config.get ctxt SMT_Config.monomorph_instances - val full = Config.get ctxt SMT_Config.monomorph_full - in - scss - |> search_substitutions ctxt limit instances Symtab.empty grounds - |> map (filter_most_specific (Proof_Context.theory_of ctxt)) - |> rpair (monos, ctxt) - |-> fold2 (instantiate full) polys - end - -fun monomorph irules ctxt = - irules - |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd) - |>> incr_indexes (* avoid clashes of schematic type variables *) - |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys) - -end diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Jul 20 13:24:49 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Jul 20 13:27:01 2011 +0200 @@ -38,8 +38,6 @@ (*translation*) val add_config: SMT_Utils.class * (Proof.context -> config) -> Context.generic -> Context.generic - val lift_lambdas: Proof.context -> bool -> term list -> - Proof.context * (term list * term list) val translate: Proof.context -> string list -> (int * thm) list -> string * recon end @@ -243,82 +241,6 @@ end -(** lambda-lifting **) - -local - fun mk_def triggers Ts T lhs rhs = - let - val eq = HOLogic.eq_const T $ lhs $ rhs - fun trigger () = - [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]] - |> map (HOLogic.mk_list @{typ SMT.pattern}) - |> HOLogic.mk_list @{typ "SMT.pattern list"} - fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t) - in - fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq - else eq) - end - - fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts - - fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t - | dest_abs Ts t = (Ts, t) - - fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) = - let - val t1 = mk_abs Us t - val bs = sort int_ord (Term.add_loose_bnos (t1, 0, [])) - fun rep i k = if member (op =) bs i then (Bound k, k+1) else (Bound i, k) - val (rs, _) = fold_map rep (0 upto length Ts - 1) 0 - val t2 = Term.subst_bounds (rs, t1) - val Ts' = map (nth Ts) bs - val (_, t3) = dest_abs [] t2 - val t4 = mk_abs Ts' t2 - - val T = Term.fastype_of1 (Us @ Ts, t) - fun app f = Term.list_comb (f, map Bound (rev bs)) - in - (case Termtab.lookup defs t4 of - SOME (f, _) => (app f, cx) - | NONE => - let - val (n, ctxt') = - yield_singleton Variable.variant_fixes Name.uu ctxt - val (is, UTs) = split_list (map_index I (Us @ Ts')) - val f = Free (n, rev UTs ---> T) - val lhs = Term.list_comb (f, map Bound (rev is)) - val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3 - in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end) - end - - fun traverse triggers Ts t = - (case t of - (q as Const (@{const_name All}, _)) $ Abs a => - abs_traverse triggers Ts a #>> (fn a' => q $ Abs a') - | (q as Const (@{const_name Ex}, _)) $ Abs a => - abs_traverse triggers Ts a #>> (fn a' => q $ Abs a') - | (l as Const (@{const_name Let}, _)) $ u $ Abs a => - traverse triggers Ts u ##>> abs_traverse triggers Ts a #>> - (fn (u', a') => l $ u' $ Abs a') - | Abs _ => - let val (Us, u) = dest_abs [] t - in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end - | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $) - | _ => pair t) - - and abs_traverse triggers Ts (n, T, t) = - traverse triggers (T::Ts) t #>> (fn t' => (n, T, t')) -in - -fun lift_lambdas ctxt triggers ts = - (Termtab.empty, ctxt) - |> fold_map (traverse triggers []) ts - |> (fn (us, (defs, ctxt')) => - (ctxt', (Termtab.fold (cons o snd o snd) defs [], us))) - -end - - (** introduce explicit applications **) local @@ -373,7 +295,7 @@ q $ Abs (x, T, in_trigger (T :: Ts) u) | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => q $ Abs (x, T, in_trigger (T :: Ts) u) - | (q as Const (@{const_name Let}, _), [u1 as Abs _, u2]) => + | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => q $ traverse Ts u1 $ traverse Ts u2 | (u as Const (c as (_, T)), ts) => (case SMT_Builtin.dest_builtin ctxt c ts of @@ -615,12 +537,30 @@ ((make_tr_context prefixes, ctxt), ts1) |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) + fun is_binder (Const (@{const_name Let}, _) $ _) = true + | is_binder t = Lambda_Lifting.is_quantifier t + + fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = + q $ Abs (n, T, mk_trigger t) + | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = + Term.domain_type T --> @{typ SMT.pattern} + |> (fn T => Const (@{const_name SMT.pat}, T) $ lhs) + |> HOLogic.mk_list @{typ SMT.pattern} o single + |> HOLogic.mk_list @{typ "SMT.pattern list"} o single + |> (fn t => @{const SMT.trigger} $ t $ eq) + | mk_trigger t = t + val (ctxt2, ts3) = ts2 |> eta_expand ctxt1 is_fol funcs - |> lift_lambdas ctxt1 true - ||> (op @) - |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) + |> rpair ctxt1 + |>> tap (map (tracing o PolyML.makestring)) + |-> Lambda_Lifting.lift_lambdas NONE is_binder + |-> (fn (ts', defs) => fn ctxt' => + map mk_trigger defs @ ts' + |> tap (map (tracing o PolyML.makestring)) + |> intro_explicit_application ctxt' funcs + |> pair ctxt') val ((rewrite_rules, extra_thms, builtin), ts4) = (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 13:24:49 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 13:27:01 2011 +0200 @@ -540,8 +540,9 @@ if trans = concealedN then rpair [] o map (conceal_lambdas ctxt) else if trans = liftingN then - map (close_form o Envir.eta_contract) - #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap + map (close_form o Envir.eta_contract) #> rpair ctxt + #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier + #> fst else if trans = combinatorsN then rpair [] o map (introduce_combinators ctxt) else if trans = lambdasN then diff -r 3264fbfd87d6 -r cb7914f6e9b3 src/HOL/Tools/lambda_lifting.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/lambda_lifting.ML Wed Jul 20 13:27:01 2011 +0200 @@ -0,0 +1,90 @@ +(* Title: HOL/Tools/lambda_lifting.ML + Author: Sascha Boehme, TU Muenchen + +Lambda-lifting on terms, i.e., replacing (some) lambda-abstractions by +fresh names accompanied with defining equations for these fresh names in +terms of the lambda-abstractions' bodies. +*) + +signature LAMBDA_LIFTING = +sig + type context = (term * term) Termtab.table * Proof.context + val init: Proof.context -> context + val is_quantifier: term -> bool + val lift_lambdas1: (term -> bool) -> string option -> term -> context -> + term * context + val finish: context -> term list * Proof.context + val lift_lambdas: string option -> (term -> bool) -> term list -> + Proof.context -> (term list * term list) * Proof.context +end + +structure Lambda_Lifting: LAMBDA_LIFTING = +struct + +fun mk_def Ts T lhs rhs = + let fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t) + in fold mk_all Ts (HOLogic.eq_const T $ lhs $ rhs) end + +fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts + +fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t + | dest_abs Ts t = (Ts, t) + +fun replace_lambda basename Us Ts t (cx as (defs, ctxt)) = + let + val t1 = mk_abs Us t + val bs = sort int_ord (Term.add_loose_bnos (t1, 0, [])) + fun rep i k = if member (op =) bs i then (Bound k, k+1) else (Bound i, k) + val (rs, _) = fold_map rep (0 upto length Ts - 1) 0 + val t2 = Term.subst_bounds (rs, t1) + val Ts' = map (nth Ts) bs + val (_, t3) = dest_abs [] t2 + val t4 = mk_abs Ts' t2 + + val T = Term.fastype_of1 (Us @ Ts, t) + fun app f = Term.list_comb (f, map Bound (rev bs)) + in + (case Termtab.lookup defs t4 of + SOME (f, _) => (app f, cx) + | NONE => + let + val (n, ctxt') = yield_singleton Variable.variant_fixes basename ctxt + val (is, UTs) = split_list (map_index I (Us @ Ts')) + val f = Free (n, rev UTs ---> T) + val lhs = Term.list_comb (f, map Bound (rev is)) + val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3 + in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end) + end + +type context = (term * term) Termtab.table * Proof.context + +fun init ctxt = (Termtab.empty, ctxt) + +fun is_quantifier (Const (@{const_name All}, _)) = true + | is_quantifier (Const (@{const_name Ex}, _)) = true + | is_quantifier _ = false + +fun lift_lambdas1 is_binder basename = + let + val basename' = the_default Name.uu basename + + fun traverse Ts (t $ (u as Abs (n, T, body))) = + if is_binder t then + traverse Ts t ##>> traverse (T :: Ts) body #>> (fn (t', body') => + t' $ Abs (n, T, body')) + else traverse Ts t ##>> traverse Ts u #>> (op $) + | traverse Ts (t as Abs _) = + let val (Us, u) = dest_abs [] t + in traverse (Us @ Ts) u #-> replace_lambda basename' Us Ts end + | traverse Ts (t $ u) = traverse Ts t ##>> traverse Ts u #>> (op $) + | traverse _ t = pair t + in traverse [] end + +fun finish (defs, ctxt) = (Termtab.fold (cons o snd o snd) defs [], ctxt) + +fun lift_lambdas basename is_binder ts ctxt = + init ctxt + |> fold_map (lift_lambdas1 is_binder basename) ts + |-> (fn ts' => finish #>> pair ts') + +end