moved lambda-lifting on terms into a separate structure (for better re-use in tools other than SMT)

--- 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"

--- 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)
 

--- 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

--- /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