# HG changeset patch # User boehmes # Date 1291730502 -3600 # Node ID 0828bfa70b20d20e249ec3835caa832123348b72 # Parent 304cfdbc6475052502f10a06d6e2071a06a07899 reduced unnecessary complexity; improved documentation; tuned diff -r 304cfdbc6475 -r 0828bfa70b20 src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Tue Dec 07 15:01:37 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Tue Dec 07 15:01:42 2010 +0100 @@ -1,7 +1,29 @@ (* Title: HOL/Tools/SMT/smt_monomorph.ML Author: Sascha Boehme, TU Muenchen -Monomorphization of theorems, i.e., computation of all (necessary) instances. +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 = @@ -13,35 +35,36 @@ structure SMT_Monomorph: SMT_MONOMORPH = struct +(* utility functions *) + 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}] +val ignored = member (op =) [@{const_name All}, @{const_name Ex}, + @{const_name Let}, @{const_name If}, @{const_name HOL.eq}] -fun is_const f (n, T) = not (ignored n) andalso f T -fun add_const_if f g (Const c) = if is_const f c then g c else I - | add_const_if _ _ _ = I +fun is_const pred (n, T) = not (ignored n) andalso pred T -fun collect_consts_if f g thm = - Term.fold_aterms (add_const_if f g) (Thm.prop_of thm) - -fun add_consts f = - collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T)) +fun collect_consts_if pred f = + Thm.prop_of #> + Term.fold_aterms (fn Const c => if is_const pred c then f c else I | _ => I) 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 irules = +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 irules 0) end + in fst (fold_map inc ithms 0) end -(* Compute all substitutions from the types "Ts" to all relevant - types in "grounds", with respect to the given substitution. *) + +(* search for necessary substitutions *) + fun new_substitutions thy grounds (n, T) subst = if not (typ_has_tvars T) then [subst] else @@ -49,9 +72,6 @@ |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst)) |> cons subst - -(* Instantiate a set of constants with a substitution. Also collect - all new ground instances for the next round of specialization. *) fun apply_subst grounds consts subst = let fun is_new_ground (n, T) = not (typ_has_tvars T) andalso @@ -66,14 +86,7 @@ end in fold_map apply_const consts #>> pair subst end - -(* Compute new substitutions for the theorem "thm", based on - previously found substitutions. - Also collect new grounds, i.e., instantiated constants - (without schematic types) which do not occur in any of the - previous rounds. Note that thus no schematic type variables are - shared among theorems. *) -fun specialize thy all_grounds new_grounds (irule, scs) = +fun specialize thy all_grounds new_grounds scs = let fun spec (subst, consts) next_grounds = [subst] @@ -82,31 +95,28 @@ |-> fold_map (apply_subst all_grounds consts) in fold_map spec scs #>> (fn scss => - (irule, fold (fold (insert (eq_snd (op =)))) scss [])) + fold (fold (insert (eq_snd (op =)))) scss []) end +val limit_reached_warning = "Warning: Monomorphization limit reached" -(* Compute all necessary substitutions. - Instead of operating on the propositions of the theorems, the - computation uses only the constants occurring with schematic type - variables in the propositions. To ease comparisons, such sets of - costants are always kept in their initial order. *) -fun incremental_monomorph ctxt limit all_grounds new_grounds irules = +fun search_substitutions ctxt limit all_grounds new_grounds scss = let val thy = ProofContext.theory_of ctxt val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds) val spec = specialize thy all_grounds' new_grounds - val (irs, new_grounds') = fold_map spec irules Symtab.empty + val (scss', new_grounds') = fold_map spec scss Symtab.empty in - if Symtab.is_empty new_grounds' then irs - else if limit > 0 - then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs - else - (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached") - (); irs) + if Symtab.is_empty new_grounds' then scss' + else if limit > 0 then + search_substitutions ctxt (limit-1) 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) @@ -129,9 +139,16 @@ in most_specific [] end +fun instantiate (i, thm) substs (ithms, ctxt) = + let + 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 -fun instantiate thy Tenv = - let + val thy = ProofContext.theory_of ctxt' + fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U | replace _ T = T @@ -142,62 +159,41 @@ fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) - fun inst (i, thm) subst = + fun inst subst = let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) [] in (i, Thm.instantiate (cTs, []) thm) end - in uncurry (map o inst) end + in (map inst substs @ ithms, ctxt') end + -fun mono_all ctxt _ [] monos = (monos, ctxt) - | mono_all ctxt limit polys monos = - let - fun invent_types (_, thm) ctxt = - let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) - in - ctxt - |> Variable.invent_types Ss - |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs - end - val (Tenvs, ctxt') = fold_map invent_types polys ctxt +(* overall procedure *) - val thy = ProofContext.theory_of ctxt' - - val ths = polys - |> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)])) - - (* all constant names occurring with schematic types *) - val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths [] +fun mono_all ctxt polys monos = + let + val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys - (* all known instances with non-schematic types *) - val grounds = - Symtab.make (map (rpair []) ns) - |> fold (add_consts (K true) o snd) monos - |> fold (add_consts (not o typ_has_tvars) o snd) polys - in - polys - |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)])) - |> incremental_monomorph ctxt' limit Symtab.empty grounds - |> map (apsnd (filter_most_specific thy)) - |> flat o map2 (instantiate thy) Tenvs - |> append monos - |> rpair ctxt' - end + (* 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 + in + scss + |> search_substitutions ctxt limit Symtab.empty grounds + |> map (filter_most_specific (ProofContext.theory_of ctxt)) + |> rpair (monos, ctxt) + |-> fold2 instantiate polys + end -(* Instantiate all polymorphic constants (i.e., constants occurring - both with ground types and type variables) with all (necessary) - ground types; thereby create copies of theorems containing those - constants. - To prevent non-termination, there is an upper limit for the - number of recursions involved in the fixpoint construction. - The initial set of theorems must not contain any schematic term - variables, and the final list of theorems does not contain any - schematic type variables anymore. *) fun monomorph irules ctxt = irules |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd) - |>> incr_indexes - |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit) + |>> incr_indexes (* avoid clashes of schematic type variables *) + |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys) end