# HG changeset patch # User boehmes # Date 1311146592 -7200 # Node ID 24d6e759753f81d12f6a8838a643a29b8c4ae364 # Parent 3a87cb597832c7f933471e3f71dfd97d30d1ca86 moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT) diff -r 3a87cb597832 -r 24d6e759753f src/HOL/SMT.thy --- a/src/HOL/SMT.thy Wed Jul 20 09:23:09 2011 +0200 +++ b/src/HOL/SMT.thy Wed Jul 20 09:23:12 2011 +0200 @@ -13,6 +13,7 @@ ("Tools/SMT/smt_builtin.ML") ("Tools/SMT/smt_datatypes.ML") ("Tools/SMT/smt_normalize.ML") + ("Tools/lambda_lifting.ML") ("Tools/SMT/smt_translate.ML") ("Tools/SMT/smt_solver.ML") ("Tools/SMT/smtlib_interface.ML") @@ -137,6 +138,7 @@ use "Tools/SMT/smt_builtin.ML" use "Tools/SMT/smt_datatypes.ML" use "Tools/SMT/smt_normalize.ML" +use "Tools/lambda_lifting.ML" use "Tools/SMT/smt_translate.ML" use "Tools/SMT/smt_solver.ML" use "Tools/SMT/smtlib_interface.ML" diff -r 3a87cb597832 -r 24d6e759753f src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Jul 20 09:23:09 2011 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Jul 20 09:23:12 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 @@ -618,7 +540,7 @@ val (ctxt2, ts3) = ts2 |> eta_expand ctxt1 is_fol funcs - |> lift_lambdas ctxt1 true + |> Lambda_Lifting.lift_lambdas ctxt1 true ||> (op @) |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs) diff -r 3a87cb597832 -r 24d6e759753f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 09:23:09 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 20 09:23:12 2011 +0200 @@ -541,7 +541,7 @@ 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 + #> Lambda_Lifting.lift_lambdas ctxt false #> snd #> swap else if trans = combinatorsN then rpair [] o map (introduce_combinators ctxt) else if trans = lambdasN then diff -r 3a87cb597832 -r 24d6e759753f 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 09:23:12 2011 +0200 @@ -0,0 +1,87 @@ +(* 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 + val lift_lambdas: Proof.context -> bool -> term list -> + Proof.context * (term list * term list) +end + +structure Lambda_Lifting: LAMBDA_LIFTING = +struct + +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')) + +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