generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
authorboehmes
Wed Jul 20 12:23:20 2011 +0200 (2011-07-20)
changeset 4392961d432e51aff
parent 43928 24d6e759753f
child 43930 cb7914f6e9b3
generalized lambda-lifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMT-specific code)
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/lambda_lifting.ML
     1.1 --- a/src/HOL/SMT.thy	Wed Jul 20 09:23:12 2011 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Jul 20 12:23:20 2011 +0200
     1.3 @@ -7,13 +7,13 @@
     1.4  theory SMT
     1.5  imports Record
     1.6  uses
     1.7 +  "Tools/lambda_lifting.ML"
     1.8    "Tools/SMT/smt_utils.ML"
     1.9    "Tools/SMT/smt_failure.ML"
    1.10    "Tools/SMT/smt_config.ML"
    1.11    ("Tools/SMT/smt_builtin.ML")
    1.12    ("Tools/SMT/smt_datatypes.ML")
    1.13    ("Tools/SMT/smt_normalize.ML")
    1.14 -  ("Tools/lambda_lifting.ML")
    1.15    ("Tools/SMT/smt_translate.ML")
    1.16    ("Tools/SMT/smt_solver.ML")
    1.17    ("Tools/SMT/smtlib_interface.ML")
    1.18 @@ -138,7 +138,6 @@
    1.19  use "Tools/SMT/smt_builtin.ML"
    1.20  use "Tools/SMT/smt_datatypes.ML"
    1.21  use "Tools/SMT/smt_normalize.ML"
    1.22 -use "Tools/lambda_lifting.ML"
    1.23  use "Tools/SMT/smt_translate.ML"
    1.24  use "Tools/SMT/smt_solver.ML"
    1.25  use "Tools/SMT/smtlib_interface.ML"
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 09:23:12 2011 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 12:23:20 2011 +0200
     2.3 @@ -295,7 +295,7 @@
     2.4            q $ Abs (x, T, in_trigger (T :: Ts) u)
     2.5        | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) =>
     2.6            q $ Abs (x, T, in_trigger (T :: Ts) u)
     2.7 -      | (q as Const (@{const_name Let}, _), [u1 as Abs _, u2]) =>
     2.8 +      | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) =>
     2.9            q $ traverse Ts u1 $ traverse Ts u2
    2.10        | (u as Const (c as (_, T)), ts) =>
    2.11            (case SMT_Builtin.dest_builtin ctxt c ts of
    2.12 @@ -537,12 +537,30 @@
    2.13        ((make_tr_context prefixes, ctxt), ts1)
    2.14        |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps)
    2.15  
    2.16 +    fun is_binder (Const (@{const_name Let}, _) $ _) = true
    2.17 +      | is_binder t = Lambda_Lifting.is_quantifier t
    2.18 +
    2.19 +    fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) =
    2.20 +          q $ Abs (n, T, mk_trigger t)
    2.21 +      | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) =
    2.22 +          Term.domain_type T --> @{typ SMT.pattern}
    2.23 +          |> (fn T => Const (@{const_name SMT.pat}, T) $ lhs)
    2.24 +          |> HOLogic.mk_list @{typ SMT.pattern} o single
    2.25 +          |> HOLogic.mk_list @{typ "SMT.pattern list"} o single
    2.26 +          |> (fn t => @{const SMT.trigger} $ t $ eq)
    2.27 +      | mk_trigger t = t
    2.28 +
    2.29      val (ctxt2, ts3) =
    2.30        ts2
    2.31        |> eta_expand ctxt1 is_fol funcs
    2.32 -      |> Lambda_Lifting.lift_lambdas ctxt1 true
    2.33 -      ||> (op @)
    2.34 -      |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
    2.35 +      |> rpair ctxt1
    2.36 +      |>> tap (map (tracing o PolyML.makestring))
    2.37 +      |-> Lambda_Lifting.lift_lambdas NONE is_binder
    2.38 +      |-> (fn (ts', defs) => fn ctxt' =>
    2.39 +          map mk_trigger defs @ ts'
    2.40 +          |> tap (map (tracing o PolyML.makestring))
    2.41 +          |> intro_explicit_application ctxt' funcs 
    2.42 +          |> pair ctxt')
    2.43  
    2.44      val ((rewrite_rules, extra_thms, builtin), ts4) =
    2.45        (if is_fol then folify ctxt2 else pair ([], [], I)) ts3
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 20 09:23:12 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 20 12:23:20 2011 +0200
     3.3 @@ -540,8 +540,9 @@
     3.4           if trans = concealedN then
     3.5             rpair [] o map (conceal_lambdas ctxt)
     3.6           else if trans = liftingN then
     3.7 -           map (close_form o Envir.eta_contract)
     3.8 -           #> Lambda_Lifting.lift_lambdas ctxt false #> snd #> swap
     3.9 +           map (close_form o Envir.eta_contract) #> rpair ctxt
    3.10 +           #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier
    3.11 +           #> fst
    3.12           else if trans = combinatorsN then
    3.13             rpair [] o map (introduce_combinators ctxt)
    3.14           else if trans = lambdasN then
     4.1 --- a/src/HOL/Tools/lambda_lifting.ML	Wed Jul 20 09:23:12 2011 +0200
     4.2 +++ b/src/HOL/Tools/lambda_lifting.ML	Wed Jul 20 12:23:20 2011 +0200
     4.3 @@ -8,32 +8,29 @@
     4.4  
     4.5  signature LAMBDA_LIFTING =
     4.6  sig
     4.7 -  val lift_lambdas: Proof.context -> bool -> term list ->
     4.8 -    Proof.context * (term list * term list)
     4.9 +  type context = (term * term) Termtab.table * Proof.context
    4.10 +  val init: Proof.context -> context
    4.11 +  val is_quantifier: term -> bool
    4.12 +  val lift_lambdas1: (term -> bool) -> string option -> term -> context ->
    4.13 +    term * context
    4.14 +  val finish: context -> term list * Proof.context
    4.15 +  val lift_lambdas: string option -> (term -> bool) -> term list ->
    4.16 +    Proof.context -> (term list * term list) * Proof.context
    4.17  end
    4.18  
    4.19  structure Lambda_Lifting: LAMBDA_LIFTING =
    4.20  struct
    4.21  
    4.22 -fun mk_def triggers Ts T lhs rhs =
    4.23 -  let
    4.24 -    val eq = HOLogic.eq_const T $ lhs $ rhs
    4.25 -    fun trigger () =
    4.26 -      [[Const (@{const_name SMT.pat}, T --> @{typ SMT.pattern}) $ lhs]]
    4.27 -      |> map (HOLogic.mk_list @{typ SMT.pattern})
    4.28 -      |> HOLogic.mk_list @{typ "SMT.pattern list"}
    4.29 -    fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
    4.30 -  in
    4.31 -    fold mk_all Ts (if triggers then @{const SMT.trigger} $ trigger () $ eq
    4.32 -      else eq)
    4.33 -  end
    4.34 +fun mk_def Ts T lhs rhs =
    4.35 +  let fun mk_all T t = HOLogic.all_const T $ Abs (Name.uu, T, t)
    4.36 +  in fold mk_all Ts (HOLogic.eq_const T $ lhs $ rhs) end
    4.37  
    4.38  fun mk_abs Ts = fold (fn T => fn t => Abs (Name.uu, T, t)) Ts
    4.39  
    4.40  fun dest_abs Ts (Abs (_, T, t)) = dest_abs (T :: Ts) t
    4.41    | dest_abs Ts t = (Ts, t)
    4.42  
    4.43 -fun replace_lambda triggers Us Ts t (cx as (defs, ctxt)) =
    4.44 +fun replace_lambda basename Us Ts t (cx as (defs, ctxt)) =
    4.45    let
    4.46      val t1 = mk_abs Us t
    4.47      val bs = sort int_ord (Term.add_loose_bnos (t1, 0, []))
    4.48 @@ -51,37 +48,43 @@
    4.49        SOME (f, _) => (app f, cx)
    4.50      | NONE =>
    4.51          let
    4.52 -          val (n, ctxt') =
    4.53 -            yield_singleton Variable.variant_fixes Name.uu ctxt
    4.54 +          val (n, ctxt') = yield_singleton Variable.variant_fixes basename ctxt
    4.55            val (is, UTs) = split_list (map_index I (Us @ Ts'))
    4.56            val f = Free (n, rev UTs ---> T)
    4.57            val lhs = Term.list_comb (f, map Bound (rev is))
    4.58 -          val def = mk_def triggers UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
    4.59 +          val def = mk_def UTs (Term.fastype_of1 (Us @ Ts, t)) lhs t3
    4.60          in (app f, (Termtab.update (t4, (f, def)) defs, ctxt')) end)
    4.61    end
    4.62  
    4.63 -fun traverse triggers Ts t =
    4.64 -  (case t of
    4.65 -    (q as Const (@{const_name All}, _)) $ Abs a =>
    4.66 -      abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    4.67 -  | (q as Const (@{const_name Ex}, _)) $ Abs a =>
    4.68 -      abs_traverse triggers Ts a #>> (fn a' => q $ Abs a')
    4.69 -  | (l as Const (@{const_name Let}, _)) $ u $ Abs a =>
    4.70 -      traverse triggers Ts u ##>> abs_traverse triggers Ts a #>>
    4.71 -      (fn (u', a') => l $ u' $ Abs a')
    4.72 -  | Abs _ =>
    4.73 -      let val (Us, u) = dest_abs [] t
    4.74 -      in traverse triggers (Us @ Ts) u #-> replace_lambda triggers Us Ts end
    4.75 -  | u1 $ u2 => traverse triggers Ts u1 ##>> traverse triggers Ts u2 #>> (op $)
    4.76 -  | _ => pair t)
    4.77 +type context = (term * term) Termtab.table * Proof.context
    4.78 +
    4.79 +fun init ctxt = (Termtab.empty, ctxt)
    4.80 +
    4.81 +fun is_quantifier (Const (@{const_name All}, _)) = true
    4.82 +  | is_quantifier (Const (@{const_name Ex}, _)) = true
    4.83 +  | is_quantifier _ = false
    4.84 +
    4.85 +fun lift_lambdas1 is_binder basename =
    4.86 +  let
    4.87 +    val basename' = the_default Name.uu basename
    4.88  
    4.89 -and abs_traverse triggers Ts (n, T, t) =
    4.90 -  traverse triggers (T::Ts) t #>> (fn t' => (n, T, t'))
    4.91 +    fun traverse Ts (t $ (u as Abs (n, T, body))) =
    4.92 +          if is_binder t then
    4.93 +            traverse Ts t ##>> traverse (T :: Ts) body #>> (fn (t', body') =>
    4.94 +            t' $ Abs (n, T, body'))
    4.95 +          else traverse Ts t ##>> traverse Ts u #>> (op $)
    4.96 +      | traverse Ts (t as Abs _) =
    4.97 +          let val (Us, u) = dest_abs [] t
    4.98 +          in traverse (Us @ Ts) u #-> replace_lambda basename' Us Ts end
    4.99 +      | traverse Ts (t $ u) = traverse Ts t ##>> traverse Ts u #>> (op $)
   4.100 +      | traverse _ t = pair t
   4.101 +  in traverse [] end
   4.102  
   4.103 -fun lift_lambdas ctxt triggers ts =
   4.104 -  (Termtab.empty, ctxt)
   4.105 -  |> fold_map (traverse triggers []) ts
   4.106 -  |> (fn (us, (defs, ctxt')) =>
   4.107 -       (ctxt', (Termtab.fold (cons o snd o snd) defs [], us)))
   4.108 +fun finish (defs, ctxt) = (Termtab.fold (cons o snd o snd) defs [], ctxt)
   4.109 +
   4.110 +fun lift_lambdas basename is_binder ts ctxt =
   4.111 +  init ctxt
   4.112 +  |> fold_map (lift_lambdas1 is_binder basename) ts
   4.113 +  |-> (fn ts' => finish #>> pair ts')
   4.114  
   4.115  end