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