new, simpler implementation of monomorphization;
authorboehmes
Thu Mar 28 23:44:41 2013 +0100 (2013-03-28)
changeset 51575907efc894051
parent 51574 2b58d7b139d6
child 51576 39896f83c1ab
new, simpler implementation of monomorphization;
old monomorphization code is still available as Legacy_Monomorphization;
modified SMT integration to use the new monomorphization code
src/HOL/ATP.thy
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/legacy_monomorph.ML
src/HOL/Tools/monomorph.ML
     1.1 --- a/src/HOL/ATP.thy	Thu Mar 28 22:42:18 2013 +0100
     1.2 +++ b/src/HOL/ATP.thy	Thu Mar 28 23:44:41 2013 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  
     1.5  ML_file "Tools/lambda_lifting.ML"
     1.6  ML_file "Tools/monomorph.ML"
     1.7 +ML_file "Tools/legacy_monomorph.ML"
     1.8  ML_file "Tools/ATP/atp_util.ML"
     1.9  ML_file "Tools/ATP/atp_problem.ML"
    1.10  ML_file "Tools/ATP/atp_proof.ML"
     2.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Thu Mar 28 22:42:18 2013 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu Mar 28 23:44:41 2013 +0100
     2.3 @@ -216,8 +216,8 @@
     2.4        else
     2.5          conj_clauses @ fact_clauses
     2.6          |> map (pair 0)
     2.7 -        |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false)
     2.8 -        |-> Monomorph.monomorph atp_schematic_consts_of
     2.9 +        |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false)
    2.10 +        |-> Legacy_Monomorph.monomorph atp_schematic_consts_of
    2.11          |> fst |> chop (length conj_clauses)
    2.12          |> pairself (maps (map (zero_var_indexes o snd)))
    2.13      val num_conjs = length conj_clauses
     3.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 28 22:42:18 2013 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Mar 28 23:44:41 2013 +0100
     3.3 @@ -32,7 +32,6 @@
     3.4    val trace_used_facts: bool Config.T
     3.5    val monomorph_limit: int Config.T
     3.6    val monomorph_instances: int Config.T
     3.7 -  val monomorph_full: bool Config.T
     3.8    val infer_triggers: bool Config.T
     3.9    val drop_bad_facts: bool Config.T
    3.10    val filter_only_facts: bool Config.T
    3.11 @@ -160,7 +159,6 @@
    3.12  val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false)
    3.13  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    3.14  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    3.15 -val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true)
    3.16  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
    3.17  val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
    3.18  val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
     4.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 22:42:18 2013 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 28 23:44:41 2013 +0100
     4.3 @@ -571,11 +571,10 @@
     4.4      val (thms', extra_thms) = f thms
     4.5    in (is ~~ thms') @ map (pair ~1) extra_thms end
     4.6  
     4.7 -fun unfold2 ithms ctxt =
     4.8 +fun unfold2 ctxt ithms =
     4.9    ithms
    4.10    |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
    4.11    |> burrow_ids add_nat_embedding
    4.12 -  |> rpair ctxt
    4.13  
    4.14  
    4.15  
    4.16 @@ -594,11 +593,11 @@
    4.17  fun add_extra_norm (cs, norm) =
    4.18    Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
    4.19  
    4.20 -fun apply_extra_norms ithms ctxt =
    4.21 +fun apply_extra_norms ctxt ithms =
    4.22    let
    4.23      val cs = SMT_Config.solver_class_of ctxt
    4.24      val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
    4.25 -  in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
    4.26 +  in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
    4.27  
    4.28  local
    4.29    val ignored = member (op =) [@{const_name All}, @{const_name Ex},
    4.30 @@ -622,12 +621,12 @@
    4.31      in (fn t => collect t Symtab.empty) end
    4.32  in
    4.33  
    4.34 -fun monomorph xthms ctxt =
    4.35 +fun monomorph ctxt xthms =
    4.36    let val (xs, thms) = split_list xthms
    4.37    in
    4.38 -    (map (pair 1) thms, ctxt)
    4.39 -    |-> Monomorph.monomorph schematic_consts_of
    4.40 -    |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
    4.41 +    map (pair 1) thms
    4.42 +    |> Monomorph.monomorph schematic_consts_of ctxt
    4.43 +    |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
    4.44    end
    4.45  
    4.46  end
    4.47 @@ -636,10 +635,10 @@
    4.48    iwthms
    4.49    |> gen_normalize ctxt
    4.50    |> unfold1 ctxt
    4.51 +  |> monomorph ctxt
    4.52 +  |> unfold2 ctxt
    4.53 +  |> apply_extra_norms ctxt
    4.54    |> rpair ctxt
    4.55 -  |-> monomorph
    4.56 -  |-> unfold2
    4.57 -  |-> apply_extra_norms
    4.58  
    4.59  val setup = Context.theory_map (
    4.60    setup_atomize #>
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 28 22:42:18 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 28 23:44:41 2013 +0100
     5.3 @@ -640,10 +640,10 @@
     5.4  
     5.5  fun repair_monomorph_context max_iters best_max_iters max_new_instances
     5.6                               best_max_new_instances =
     5.7 -  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
     5.8 -  #> Config.put Monomorph.max_new_instances
     5.9 +  Config.put Legacy_Monomorph.max_rounds (max_iters |> the_default best_max_iters)
    5.10 +  #> Config.put Legacy_Monomorph.max_new_instances
    5.11           (max_new_instances |> the_default best_max_new_instances)
    5.12 -  #> Config.put Monomorph.keep_partial_instances false
    5.13 +  #> Config.put Legacy_Monomorph.keep_partial_instances false
    5.14  
    5.15  fun suffix_for_mode Auto_Try = "_try"
    5.16    | suffix_for_mode Try = "_try"
    5.17 @@ -747,7 +747,7 @@
    5.18                      |> op @
    5.19                      |> cons (0, subgoal_th)
    5.20            in
    5.21 -            Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
    5.22 +            Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
    5.23              |> curry ListPair.zip (map fst facts)
    5.24              |> maps (fn (name, rths) =>
    5.25                          map (pair name o zero_var_indexes o snd) rths)
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/legacy_monomorph.ML	Thu Mar 28 23:44:41 2013 +0100
     6.3 @@ -0,0 +1,331 @@
     6.4 +(*  Title:      HOL/Tools/legacy_monomorph.ML
     6.5 +    Author:     Sascha Boehme, TU Muenchen
     6.6 +
     6.7 +Monomorphization of theorems, i.e., computation of all (necessary)
     6.8 +instances.  This procedure is incomplete in general, but works well for
     6.9 +most practical problems.
    6.10 +
    6.11 +For a list of universally closed theorems (without schematic term
    6.12 +variables), monomorphization computes a list of theorems with schematic
    6.13 +term variables: all polymorphic constants (i.e., constants occurring both
    6.14 +with ground types and schematic type variables) are instantiated with all
    6.15 +(necessary) ground types; thereby theorems containing these constants are
    6.16 +copied.  To prevent nontermination, there is an upper limit for the number
    6.17 +of iterations involved in the fixpoint construction.
    6.18 +
    6.19 +The search for instances is performed on the constants with schematic
    6.20 +types, which are extracted from the initial set of theorems.  The search
    6.21 +constructs, for each theorem with those constants, a set of substitutions,
    6.22 +which, in the end, is applied to all corresponding theorems.  Remaining
    6.23 +schematic type variables are substituted with fresh types.
    6.24 +
    6.25 +Searching for necessary substitutions is an iterative fixpoint
    6.26 +construction: each iteration computes all required instances required by
    6.27 +the ground instances computed in the previous step and which haven't been
    6.28 +found before.  Computed substitutions are always nontrivial: schematic type
    6.29 +variables are never mapped to schematic type variables.
    6.30 +*)
    6.31 +
    6.32 +signature LEGACY_MONOMORPH =
    6.33 +sig
    6.34 +  (* utility function *)
    6.35 +  val typ_has_tvars: typ -> bool
    6.36 +  val all_schematic_consts_of: term -> typ list Symtab.table
    6.37 +  val add_schematic_consts_of: term -> typ list Symtab.table ->
    6.38 +    typ list Symtab.table
    6.39 +
    6.40 +  (* configuration options *)
    6.41 +  val max_rounds: int Config.T
    6.42 +  val max_new_instances: int Config.T
    6.43 +  val keep_partial_instances: bool Config.T
    6.44 +
    6.45 +  (* monomorphization *)
    6.46 +  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
    6.47 +    Proof.context -> (int * thm) list list * Proof.context
    6.48 +end
    6.49 +
    6.50 +structure Legacy_Monomorph: LEGACY_MONOMORPH =
    6.51 +struct
    6.52 +
    6.53 +(* utility functions *)
    6.54 +
    6.55 +val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
    6.56 +
    6.57 +fun add_schematic_const (c as (_, T)) =
    6.58 +  if typ_has_tvars T then Symtab.insert_list (op =) c else I
    6.59 +
    6.60 +fun add_schematic_consts_of t =
    6.61 +  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
    6.62 +
    6.63 +fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
    6.64 +
    6.65 +
    6.66 +
    6.67 +(* configuration options *)
    6.68 +
    6.69 +val max_rounds = Attrib.setup_config_int @{binding legacy_monomorph_max_rounds} (K 5)
    6.70 +val max_new_instances =
    6.71 +  Attrib.setup_config_int @{binding legacy_monomorph_max_new_instances} (K 300)
    6.72 +val keep_partial_instances =
    6.73 +  Attrib.setup_config_bool @{binding legacy_monomorph_keep_partial_instances} (K true)
    6.74 +
    6.75 +
    6.76 +
    6.77 +(* monomorphization *)
    6.78 +
    6.79 +(** preparing the problem **)
    6.80 +
    6.81 +datatype thm_info =
    6.82 +  Ground of thm |
    6.83 +  Schematic of {
    6.84 +    index: int,
    6.85 +    theorem: thm,
    6.86 +    tvars: (indexname * sort) list,
    6.87 +    schematics: typ list Symtab.table,
    6.88 +    initial_round: int }
    6.89 +
    6.90 +fun prepare schematic_consts_of rthms =
    6.91 +  let
    6.92 +    val empty_sub = ((0, false, false), Vartab.empty)
    6.93 +
    6.94 +    fun prep (r, thm) ((i, idx), (consts, subs)) =
    6.95 +      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
    6.96 +        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
    6.97 +      else
    6.98 +        let
    6.99 +          (* increase indices to avoid clashes of type variables *)
   6.100 +          val thm' = Thm.incr_indexes idx thm
   6.101 +          val idx' = Thm.maxidx_of thm' + 1
   6.102 +          val schematics = schematic_consts_of (Thm.prop_of thm')
   6.103 +          val consts' =
   6.104 +            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
   6.105 +          val subs' = Inttab.update (i, [empty_sub]) subs
   6.106 +          val thm_info = Schematic {
   6.107 +            index = i,
   6.108 +            theorem = thm',
   6.109 +            tvars = Term.add_tvars (Thm.prop_of thm') [],
   6.110 +            schematics = schematics,
   6.111 +            initial_round = r }
   6.112 +      in (thm_info, ((i+1, idx'), (consts', subs'))) end
   6.113 +  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
   6.114 +
   6.115 +
   6.116 +
   6.117 +(** collecting substitutions **)
   6.118 +
   6.119 +fun exceeded limit = (limit <= 0)
   6.120 +fun exceeded_limit (limit, _, _) = exceeded limit
   6.121 +
   6.122 +
   6.123 +fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => 
   6.124 +  Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
   6.125 +
   6.126 +fun eq_subst (subst1, subst2) =
   6.127 +  derived_subst subst1 subst2 andalso derived_subst subst2 subst1
   6.128 +
   6.129 +
   6.130 +fun with_all_grounds cx grounds f =
   6.131 +  if exceeded_limit cx then I else Symtab.fold f grounds
   6.132 +
   6.133 +fun with_all_type_combinations cx schematics f (n, Ts) =
   6.134 +  if exceeded_limit cx then I
   6.135 +  else fold_product f (Symtab.lookup_list schematics n) Ts
   6.136 +
   6.137 +fun derive_new_substs thy cx new_grounds schematics subst =
   6.138 +  with_all_grounds cx new_grounds
   6.139 +    (with_all_type_combinations cx schematics (fn T => fn U =>
   6.140 +      (case try (Sign.typ_match thy (T, U)) subst of
   6.141 +        NONE => I
   6.142 +      | SOME subst' => insert eq_subst subst'))) []
   6.143 +
   6.144 +
   6.145 +fun known_subst sub subs1 subs2 subst' =
   6.146 +  let fun derived (_, subst) = derived_subst subst' subst
   6.147 +  in derived sub orelse exists derived subs1 orelse exists derived subs2 end
   6.148 +
   6.149 +fun within_limit f cx = if exceeded_limit cx then cx else f cx
   6.150 +
   6.151 +fun fold_partial_substs derive add = within_limit (
   6.152 +  let
   6.153 +    fun fold_partial [] cx = cx
   6.154 +      | fold_partial (sub :: subs) (limit, subs', next) =
   6.155 +          if exceeded limit then (limit, sub :: subs @ subs', next)
   6.156 +          else sub |> (fn ((generation, full, _), subst) =>
   6.157 +            if full then fold_partial subs (limit, sub :: subs', next)
   6.158 +            else
   6.159 +              (case filter_out (known_subst sub subs subs') (derive subst) of
   6.160 +                [] => fold_partial subs (limit, sub :: subs', next)
   6.161 +              | substs =>
   6.162 +                  (limit, ((generation, full, true), subst) :: subs', next)
   6.163 +                  |> fold (within_limit o add) substs
   6.164 +                  |> fold_partial subs))
   6.165 +  in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
   6.166 +
   6.167 +
   6.168 +fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
   6.169 +  let
   6.170 +    val thy = Proof_Context.theory_of ctxt
   6.171 +    val count_partial = Config.get ctxt keep_partial_instances
   6.172 +
   6.173 +    fun add_new_ground subst n T =
   6.174 +      let val T' = Envir.subst_type subst T
   6.175 +      in
   6.176 +        (* FIXME: maybe keep types in a table or net for known_grounds,
   6.177 +           that might improve efficiency here
   6.178 +        *)
   6.179 +        if typ_has_tvars T' then I
   6.180 +        else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
   6.181 +        else Symtab.cons_list (n, T')
   6.182 +      end
   6.183 +
   6.184 +    fun add_new_subst subst (limit, subs, next_grounds) =
   6.185 +      let
   6.186 +        val full = forall (Vartab.defined subst o fst) tvars
   6.187 +        val limit' =
   6.188 +          if full orelse count_partial then limit - 1 else limit
   6.189 +        val sub = ((round, full, false), subst)
   6.190 +        val next_grounds' =
   6.191 +          (schematics, next_grounds)
   6.192 +          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
   6.193 +      in (limit', sub :: subs, next_grounds') end
   6.194 +  in
   6.195 +    fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
   6.196 +      add_new_subst cx
   6.197 +  end
   6.198 +
   6.199 +
   6.200 +(*
   6.201 +  'known_grounds' are all constant names known to occur schematically
   6.202 +  associated with all ground instances considered so far
   6.203 +*)
   6.204 +fun add_relevant_instances known_grounds (Const (c as (n, T))) =
   6.205 +      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
   6.206 +      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
   6.207 +      else Symtab.insert_list (op =) c
   6.208 +  | add_relevant_instances _ _ = I
   6.209 +
   6.210 +fun collect_instances known_grounds thm =
   6.211 +  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
   6.212 +
   6.213 +
   6.214 +fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
   6.215 +  let
   6.216 +    (* The total limit of returned (ground) facts is the number of facts
   6.217 +       given to the monomorphizer increased by max_new_instances.  Since
   6.218 +       initially ground facts are returned anyway, the limit here is not
   6.219 +       counting them. *)
   6.220 +    val limit = Config.get ctxt max_new_instances + 
   6.221 +      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
   6.222 +
   6.223 +    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
   6.224 +      | add_ground_consts (Schematic _) = I
   6.225 +    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
   6.226 +  in (known_grounds, (limit, substitutions, initial_grounds)) end
   6.227 +
   6.228 +fun is_new round initial_round = (round = initial_round)
   6.229 +fun is_active round initial_round = (round > initial_round)
   6.230 +
   6.231 +fun fold_schematic pred f = fold (fn
   6.232 +    Schematic {index, theorem, tvars, schematics, initial_round} =>
   6.233 +      if pred initial_round then f theorem (index, tvars, schematics) else I
   6.234 +  | Ground _ => I)
   6.235 +
   6.236 +fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
   6.237 +  let
   6.238 +    val (limit', isubs', next_grounds') =
   6.239 +      (limit, Inttab.lookup_list subs index, next_grounds)
   6.240 +      |> f (tvars, schematics)
   6.241 +  in (limit', Inttab.update (index, isubs') subs, next_grounds') end
   6.242 +
   6.243 +fun collect_substitutions thm_infos ctxt round subst_ctxt =
   6.244 +  let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
   6.245 +  in
   6.246 +    if exceeded limit then subst_ctxt
   6.247 +    else
   6.248 +      let
   6.249 +        fun collect thm _ = collect_instances known_grounds thm
   6.250 +        val new = fold_schematic (is_new round) collect thm_infos next_grounds
   6.251 +
   6.252 +        val known' = Symtab.merge_list (op =) (known_grounds, new)
   6.253 +        val step = focus o refine ctxt round known'
   6.254 +      in
   6.255 +        (limit, subs, Symtab.empty)
   6.256 +        |> not (Symtab.is_empty new) ?
   6.257 +            fold_schematic (is_active round) (step new) thm_infos
   6.258 +        |> fold_schematic (is_new round) (step known') thm_infos
   6.259 +        |> pair known'
   6.260 +      end
   6.261 +  end
   6.262 +
   6.263 +
   6.264 +
   6.265 +(** instantiating schematic theorems **)
   6.266 +
   6.267 +fun super_sort (Ground _) S = S
   6.268 +  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
   6.269 +
   6.270 +fun new_super_type ctxt thm_infos =
   6.271 +  let val S = fold super_sort thm_infos @{sort type}
   6.272 +  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
   6.273 +
   6.274 +fun add_missing_tvar T (ix, S) subst =
   6.275 +  if Vartab.defined subst ix then subst
   6.276 +  else Vartab.update (ix, (S, T)) subst
   6.277 +
   6.278 +fun complete tvars subst T =
   6.279 +  subst
   6.280 +  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
   6.281 +  |> fold (add_missing_tvar T) tvars
   6.282 +
   6.283 +fun instantiate_all' (mT, ctxt) subs thm_infos =
   6.284 +  let
   6.285 +    val thy = Proof_Context.theory_of ctxt
   6.286 +
   6.287 +    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   6.288 +    fun cert' subst = Vartab.fold (cons o cert) subst []
   6.289 +    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
   6.290 +
   6.291 +    fun with_subst tvars f ((generation, full, _), subst) =
   6.292 +      if full then SOME (generation, f subst)
   6.293 +      else Option.map (pair generation o f o complete tvars subst) mT
   6.294 +
   6.295 +    fun inst (Ground thm) = [(0, thm)]
   6.296 +      | inst (Schematic {theorem, tvars, index, ...}) =
   6.297 +          Inttab.lookup_list subs index
   6.298 +          |> map_filter (with_subst tvars (instantiate theorem))
   6.299 +  in (map inst thm_infos, ctxt) end
   6.300 +
   6.301 +fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
   6.302 +  if Config.get ctxt keep_partial_instances then
   6.303 +    let fun is_refined ((_, _, refined), _) = refined
   6.304 +    in
   6.305 +      (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
   6.306 +      |-> instantiate_all' (new_super_type ctxt thm_infos)
   6.307 +    end
   6.308 +  else instantiate_all' (NONE, ctxt) subs thm_infos
   6.309 +
   6.310 +
   6.311 +
   6.312 +(** overall procedure **)
   6.313 +
   6.314 +fun limit_rounds ctxt f =
   6.315 +  let
   6.316 +    val max = Config.get ctxt max_rounds
   6.317 +    fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
   6.318 +  in round 1 end
   6.319 +
   6.320 +fun monomorph schematic_consts_of rthms ctxt =
   6.321 +  let
   6.322 +    val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
   6.323 +  in
   6.324 +    if Symtab.is_empty known_grounds then
   6.325 +      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
   6.326 +    else
   6.327 +      make_subst_ctxt ctxt thm_infos known_grounds subs
   6.328 +      |> limit_rounds ctxt (collect_substitutions thm_infos)
   6.329 +      |> instantiate_all ctxt thm_infos
   6.330 +  end
   6.331 +
   6.332 +
   6.333 +end
   6.334 +
     7.1 --- a/src/HOL/Tools/monomorph.ML	Thu Mar 28 22:42:18 2013 +0100
     7.2 +++ b/src/HOL/Tools/monomorph.ML	Thu Mar 28 23:44:41 2013 +0100
     7.3 @@ -1,34 +1,32 @@
     7.4  (*  Title:      HOL/Tools/monomorph.ML
     7.5      Author:     Sascha Boehme, TU Muenchen
     7.6  
     7.7 -Monomorphization of theorems, i.e., computation of all (necessary)
     7.8 -instances.  This procedure is incomplete in general, but works well for
     7.9 -most practical problems.
    7.10 -
    7.11 -For a list of universally closed theorems (without schematic term
    7.12 -variables), monomorphization computes a list of theorems with schematic
    7.13 -term variables: all polymorphic constants (i.e., constants occurring both
    7.14 -with ground types and schematic type variables) are instantiated with all
    7.15 -(necessary) ground types; thereby theorems containing these constants are
    7.16 -copied.  To prevent nontermination, there is an upper limit for the number
    7.17 -of iterations involved in the fixpoint construction.
    7.18 +Monomorphization of theorems, i.e., computation of ground instances for
    7.19 +theorems with type variables.  This procedure is incomplete in general,
    7.20 +but works well for most practical problems.
    7.21  
    7.22 -The search for instances is performed on the constants with schematic
    7.23 -types, which are extracted from the initial set of theorems.  The search
    7.24 -constructs, for each theorem with those constants, a set of substitutions,
    7.25 -which, in the end, is applied to all corresponding theorems.  Remaining
    7.26 -schematic type variables are substituted with fresh types.
    7.27 +Monomorphization is essentially an enumeration of substitutions that map
    7.28 +schematic types to ground types. Applying these substitutions to theorems
    7.29 +with type variables results in monomorphized ground instances. The
    7.30 +enumeration is driven by schematic constants (constants occurring with
    7.31 +type variables) and all ground instances of such constants (occurrences
    7.32 +without type variables). The enumeration is organized in rounds in which
    7.33 +all substitutions for the schematic constants are computed that are induced
    7.34 +by the ground instances. Any new ground instance may induce further
    7.35 +substitutions in a subsequent round. To prevent nontermination, there is
    7.36 +an upper limit of rounds involved and of the number of monomorphized ground
    7.37 +instances computed.
    7.38  
    7.39 -Searching for necessary substitutions is an iterative fixpoint
    7.40 -construction: each iteration computes all required instances required by
    7.41 -the ground instances computed in the previous step and which haven't been
    7.42 -found before.  Computed substitutions are always nontrivial: schematic type
    7.43 -variables are never mapped to schematic type variables.
    7.44 +Theorems to be monomorphized must be tagged with a number indicating the
    7.45 +initial round in which they participate first. The initial round is
    7.46 +ignored for theorems without type variables. For any other theorem, the
    7.47 +initial round must be greater than zero. Returned monomorphized theorems
    7.48 +carry a number showing from which monomorphization round they emerged.
    7.49  *)
    7.50  
    7.51  signature MONOMORPH =
    7.52  sig
    7.53 -  (* utility function *)
    7.54 +  (* utility functions *)
    7.55    val typ_has_tvars: typ -> bool
    7.56    val all_schematic_consts_of: term -> typ list Symtab.table
    7.57    val add_schematic_consts_of: term -> typ list Symtab.table ->
    7.58 @@ -37,11 +35,10 @@
    7.59    (* configuration options *)
    7.60    val max_rounds: int Config.T
    7.61    val max_new_instances: int Config.T
    7.62 -  val keep_partial_instances: bool Config.T
    7.63  
    7.64    (* monomorphization *)
    7.65 -  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
    7.66 -    Proof.context -> (int * thm) list list * Proof.context
    7.67 +  val monomorph: (term -> typ list Symtab.table) -> Proof.context ->
    7.68 +    (int * thm) list -> (int * thm) list list
    7.69  end
    7.70  
    7.71  structure Monomorph: MONOMORPH =
    7.72 @@ -59,254 +56,16 @@
    7.73  
    7.74  fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
    7.75  
    7.76 +fun clear_grounds grounds = Symtab.map (K (K [])) grounds
    7.77 +
    7.78  
    7.79  
    7.80  (* configuration options *)
    7.81  
    7.82  val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
    7.83 +
    7.84  val max_new_instances =
    7.85    Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
    7.86 -val keep_partial_instances =
    7.87 -  Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
    7.88 -
    7.89 -
    7.90 -
    7.91 -(* monomorphization *)
    7.92 -
    7.93 -(** preparing the problem **)
    7.94 -
    7.95 -datatype thm_info =
    7.96 -  Ground of thm |
    7.97 -  Schematic of {
    7.98 -    index: int,
    7.99 -    theorem: thm,
   7.100 -    tvars: (indexname * sort) list,
   7.101 -    schematics: typ list Symtab.table,
   7.102 -    initial_round: int }
   7.103 -
   7.104 -fun prepare schematic_consts_of rthms =
   7.105 -  let
   7.106 -    val empty_sub = ((0, false, false), Vartab.empty)
   7.107 -
   7.108 -    fun prep (r, thm) ((i, idx), (consts, subs)) =
   7.109 -      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
   7.110 -        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
   7.111 -      else
   7.112 -        let
   7.113 -          (* increase indices to avoid clashes of type variables *)
   7.114 -          val thm' = Thm.incr_indexes idx thm
   7.115 -          val idx' = Thm.maxidx_of thm' + 1
   7.116 -          val schematics = schematic_consts_of (Thm.prop_of thm')
   7.117 -          val consts' =
   7.118 -            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
   7.119 -          val subs' = Inttab.update (i, [empty_sub]) subs
   7.120 -          val thm_info = Schematic {
   7.121 -            index = i,
   7.122 -            theorem = thm',
   7.123 -            tvars = Term.add_tvars (Thm.prop_of thm') [],
   7.124 -            schematics = schematics,
   7.125 -            initial_round = r }
   7.126 -      in (thm_info, ((i+1, idx'), (consts', subs'))) end
   7.127 -  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
   7.128 -
   7.129 -
   7.130 -
   7.131 -(** collecting substitutions **)
   7.132 -
   7.133 -fun exceeded limit = (limit <= 0)
   7.134 -fun exceeded_limit (limit, _, _) = exceeded limit
   7.135 -
   7.136 -
   7.137 -fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => 
   7.138 -  Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
   7.139 -
   7.140 -fun eq_subst (subst1, subst2) =
   7.141 -  derived_subst subst1 subst2 andalso derived_subst subst2 subst1
   7.142 -
   7.143 -
   7.144 -fun with_all_grounds cx grounds f =
   7.145 -  if exceeded_limit cx then I else Symtab.fold f grounds
   7.146 -
   7.147 -fun with_all_type_combinations cx schematics f (n, Ts) =
   7.148 -  if exceeded_limit cx then I
   7.149 -  else fold_product f (Symtab.lookup_list schematics n) Ts
   7.150 -
   7.151 -fun derive_new_substs thy cx new_grounds schematics subst =
   7.152 -  with_all_grounds cx new_grounds
   7.153 -    (with_all_type_combinations cx schematics (fn T => fn U =>
   7.154 -      (case try (Sign.typ_match thy (T, U)) subst of
   7.155 -        NONE => I
   7.156 -      | SOME subst' => insert eq_subst subst'))) []
   7.157 -
   7.158 -
   7.159 -fun known_subst sub subs1 subs2 subst' =
   7.160 -  let fun derived (_, subst) = derived_subst subst' subst
   7.161 -  in derived sub orelse exists derived subs1 orelse exists derived subs2 end
   7.162 -
   7.163 -fun within_limit f cx = if exceeded_limit cx then cx else f cx
   7.164 -
   7.165 -fun fold_partial_substs derive add = within_limit (
   7.166 -  let
   7.167 -    fun fold_partial [] cx = cx
   7.168 -      | fold_partial (sub :: subs) (limit, subs', next) =
   7.169 -          if exceeded limit then (limit, sub :: subs @ subs', next)
   7.170 -          else sub |> (fn ((generation, full, _), subst) =>
   7.171 -            if full then fold_partial subs (limit, sub :: subs', next)
   7.172 -            else
   7.173 -              (case filter_out (known_subst sub subs subs') (derive subst) of
   7.174 -                [] => fold_partial subs (limit, sub :: subs', next)
   7.175 -              | substs =>
   7.176 -                  (limit, ((generation, full, true), subst) :: subs', next)
   7.177 -                  |> fold (within_limit o add) substs
   7.178 -                  |> fold_partial subs))
   7.179 -  in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
   7.180 -
   7.181 -
   7.182 -fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
   7.183 -  let
   7.184 -    val thy = Proof_Context.theory_of ctxt
   7.185 -    val count_partial = Config.get ctxt keep_partial_instances
   7.186 -
   7.187 -    fun add_new_ground subst n T =
   7.188 -      let val T' = Envir.subst_type subst T
   7.189 -      in
   7.190 -        (* FIXME: maybe keep types in a table or net for known_grounds,
   7.191 -           that might improve efficiency here
   7.192 -        *)
   7.193 -        if typ_has_tvars T' then I
   7.194 -        else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
   7.195 -        else Symtab.cons_list (n, T')
   7.196 -      end
   7.197 -
   7.198 -    fun add_new_subst subst (limit, subs, next_grounds) =
   7.199 -      let
   7.200 -        val full = forall (Vartab.defined subst o fst) tvars
   7.201 -        val limit' =
   7.202 -          if full orelse count_partial then limit - 1 else limit
   7.203 -        val sub = ((round, full, false), subst)
   7.204 -        val next_grounds' =
   7.205 -          (schematics, next_grounds)
   7.206 -          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
   7.207 -      in (limit', sub :: subs, next_grounds') end
   7.208 -  in
   7.209 -    fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
   7.210 -      add_new_subst cx
   7.211 -  end
   7.212 -
   7.213 -
   7.214 -(*
   7.215 -  'known_grounds' are all constant names known to occur schematically
   7.216 -  associated with all ground instances considered so far
   7.217 -*)
   7.218 -fun add_relevant_instances known_grounds (Const (c as (n, T))) =
   7.219 -      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
   7.220 -      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
   7.221 -      else Symtab.insert_list (op =) c
   7.222 -  | add_relevant_instances _ _ = I
   7.223 -
   7.224 -fun collect_instances known_grounds thm =
   7.225 -  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
   7.226 -
   7.227 -
   7.228 -fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
   7.229 -  let
   7.230 -    (* The total limit of returned (ground) facts is the number of facts
   7.231 -       given to the monomorphizer increased by max_new_instances.  Since
   7.232 -       initially ground facts are returned anyway, the limit here is not
   7.233 -       counting them. *)
   7.234 -    val limit = Config.get ctxt max_new_instances + 
   7.235 -      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
   7.236 -
   7.237 -    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
   7.238 -      | add_ground_consts (Schematic _) = I
   7.239 -    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
   7.240 -  in (known_grounds, (limit, substitutions, initial_grounds)) end
   7.241 -
   7.242 -fun is_new round initial_round = (round = initial_round)
   7.243 -fun is_active round initial_round = (round > initial_round)
   7.244 -
   7.245 -fun fold_schematic pred f = fold (fn
   7.246 -    Schematic {index, theorem, tvars, schematics, initial_round} =>
   7.247 -      if pred initial_round then f theorem (index, tvars, schematics) else I
   7.248 -  | Ground _ => I)
   7.249 -
   7.250 -fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
   7.251 -  let
   7.252 -    val (limit', isubs', next_grounds') =
   7.253 -      (limit, Inttab.lookup_list subs index, next_grounds)
   7.254 -      |> f (tvars, schematics)
   7.255 -  in (limit', Inttab.update (index, isubs') subs, next_grounds') end
   7.256 -
   7.257 -fun collect_substitutions thm_infos ctxt round subst_ctxt =
   7.258 -  let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
   7.259 -  in
   7.260 -    if exceeded limit then subst_ctxt
   7.261 -    else
   7.262 -      let
   7.263 -        fun collect thm _ = collect_instances known_grounds thm
   7.264 -        val new = fold_schematic (is_new round) collect thm_infos next_grounds
   7.265 -
   7.266 -        val known' = Symtab.merge_list (op =) (known_grounds, new)
   7.267 -        val step = focus o refine ctxt round known'
   7.268 -      in
   7.269 -        (limit, subs, Symtab.empty)
   7.270 -        |> not (Symtab.is_empty new) ?
   7.271 -            fold_schematic (is_active round) (step new) thm_infos
   7.272 -        |> fold_schematic (is_new round) (step known') thm_infos
   7.273 -        |> pair known'
   7.274 -      end
   7.275 -  end
   7.276 -
   7.277 -
   7.278 -
   7.279 -(** instantiating schematic theorems **)
   7.280 -
   7.281 -fun super_sort (Ground _) S = S
   7.282 -  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
   7.283 -
   7.284 -fun new_super_type ctxt thm_infos =
   7.285 -  let val S = fold super_sort thm_infos @{sort type}
   7.286 -  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
   7.287 -
   7.288 -fun add_missing_tvar T (ix, S) subst =
   7.289 -  if Vartab.defined subst ix then subst
   7.290 -  else Vartab.update (ix, (S, T)) subst
   7.291 -
   7.292 -fun complete tvars subst T =
   7.293 -  subst
   7.294 -  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
   7.295 -  |> fold (add_missing_tvar T) tvars
   7.296 -
   7.297 -fun instantiate_all' (mT, ctxt) subs thm_infos =
   7.298 -  let
   7.299 -    val thy = Proof_Context.theory_of ctxt
   7.300 -
   7.301 -    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   7.302 -    fun cert' subst = Vartab.fold (cons o cert) subst []
   7.303 -    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
   7.304 -
   7.305 -    fun with_subst tvars f ((generation, full, _), subst) =
   7.306 -      if full then SOME (generation, f subst)
   7.307 -      else Option.map (pair generation o f o complete tvars subst) mT
   7.308 -
   7.309 -    fun inst (Ground thm) = [(0, thm)]
   7.310 -      | inst (Schematic {theorem, tvars, index, ...}) =
   7.311 -          Inttab.lookup_list subs index
   7.312 -          |> map_filter (with_subst tvars (instantiate theorem))
   7.313 -  in (map inst thm_infos, ctxt) end
   7.314 -
   7.315 -fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
   7.316 -  if Config.get ctxt keep_partial_instances then
   7.317 -    let fun is_refined ((_, _, refined), _) = refined
   7.318 -    in
   7.319 -      (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
   7.320 -      |-> instantiate_all' (new_super_type ctxt thm_infos)
   7.321 -    end
   7.322 -  else instantiate_all' (NONE, ctxt) subs thm_infos
   7.323 -
   7.324 -
   7.325 -
   7.326 -(** overall procedure **)
   7.327  
   7.328  fun limit_rounds ctxt f =
   7.329    let
   7.330 @@ -314,18 +73,220 @@
   7.331      fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
   7.332    in round 1 end
   7.333  
   7.334 -fun monomorph schematic_consts_of rthms ctxt =
   7.335 +fun reached_limit ctxt n = (n >= Config.get ctxt max_new_instances)
   7.336 +
   7.337 +
   7.338 +
   7.339 +(* theorem information and related functions *)
   7.340 +
   7.341 +datatype thm_info =
   7.342 +  Ground of thm |
   7.343 +  Ignored |
   7.344 +  Schematic of {
   7.345 +    id: int,
   7.346 +    theorem: thm,
   7.347 +    tvars: (indexname * sort) list,
   7.348 +    schematics: (string * typ) list,
   7.349 +    initial_round: int}
   7.350 +
   7.351 +
   7.352 +fun fold_grounds f = fold (fn Ground thm => f thm | _ => I)
   7.353 +
   7.354 +
   7.355 +fun fold_schematic f thm_info =
   7.356 +  (case thm_info of
   7.357 +    Schematic {id, theorem, tvars, schematics, initial_round} =>
   7.358 +      f id theorem tvars schematics initial_round
   7.359 +  | _ => I)
   7.360 +
   7.361 +
   7.362 +fun fold_schematics pred f =
   7.363 +  let
   7.364 +    fun apply id thm tvars schematics initial_round x =
   7.365 +      if pred initial_round then f id thm tvars schematics x else x
   7.366 +  in fold (fold_schematic apply) end
   7.367 +
   7.368 +
   7.369 +
   7.370 +(* collecting data *)
   7.371 +
   7.372 +(*
   7.373 +  Theorems with type variables that cannot be instantiated should be ignored.
   7.374 +  A type variable has only a chance to be instantiated if it occurs in the
   7.375 +  type of one of the schematic constants.
   7.376 +*)
   7.377 +fun groundable all_tvars schematics =
   7.378 +  let val tvars' = Symtab.fold (fold Term.add_tvarsT o snd) schematics []
   7.379 +  in forall (member (op =) tvars') all_tvars end
   7.380 +
   7.381 +
   7.382 +fun prepare schematic_consts_of rthms =
   7.383    let
   7.384 -    val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
   7.385 +    fun prep (initial_round, thm) ((id, idx), consts) =
   7.386 +      if Term.exists_type typ_has_tvars (Thm.prop_of thm) then
   7.387 +        let
   7.388 +          (* increase indices to avoid clashes of type variables *)
   7.389 +          val thm' = Thm.incr_indexes idx thm
   7.390 +          val idx' = Thm.maxidx_of thm' + 1
   7.391 +
   7.392 +          val tvars = Term.add_tvars (Thm.prop_of thm') []
   7.393 +          val schematics = schematic_consts_of (Thm.prop_of thm')
   7.394 +          val schematics' =
   7.395 +            Symtab.fold (fn (n, Ts) => fold (cons o pair n) Ts) schematics []
   7.396 +
   7.397 +          (* collect the names of all constants that need to be instantiated *)
   7.398 +          val consts' =
   7.399 +            consts
   7.400 +            |> Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics
   7.401 +
   7.402 +          val thm_info =
   7.403 +            if not (groundable tvars schematics) then Ignored
   7.404 +            else
   7.405 +              Schematic {
   7.406 +                id = id,
   7.407 +                theorem = thm',
   7.408 +                tvars = tvars,
   7.409 +                schematics = schematics',
   7.410 +                initial_round = initial_round}
   7.411 +        in (thm_info, ((id + 1, idx'), consts')) end
   7.412 +      else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts))
   7.413 +
   7.414 +  in fold_map prep rthms ((0, 0), Symtab.empty) ||> snd end
   7.415 +
   7.416 +
   7.417 +
   7.418 +(* collecting instances *)
   7.419 +
   7.420 +fun instantiate thy subst =
   7.421 +  let
   7.422 +    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   7.423 +    fun cert' subst = Vartab.fold (cons o cert) subst []
   7.424 +  in Thm.instantiate (cert' subst, []) end
   7.425 +
   7.426 +
   7.427 +fun add_new_grounds used_grounds new_grounds thm =
   7.428 +  let
   7.429 +    fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T
   7.430 +    fun add (Const (c as (n, _))) =
   7.431 +          if mem used_grounds c orelse mem new_grounds c then I
   7.432 +          else if not (Symtab.defined used_grounds n) then I
   7.433 +          else Symtab.insert_list (op =) c
   7.434 +      | add _ = I
   7.435 +  in Term.fold_aterms add (Thm.prop_of thm) end
   7.436 +
   7.437 +
   7.438 +fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx =
   7.439 +  let
   7.440 +    exception ENOUGH of
   7.441 +      typ list Symtab.table * (int * (int * thm) list Inttab.table)
   7.442 +
   7.443 +    val thy = Proof_Context.theory_of ctxt
   7.444 +
   7.445 +    fun add subst (next_grounds, (n, insts)) =
   7.446 +      let
   7.447 +        val thm' = instantiate thy subst thm
   7.448 +        val rthm = (round, thm')
   7.449 +        val n_insts' =
   7.450 +          if member (eq_snd Thm.eq_thm) (Inttab.lookup_list insts id) rthm then
   7.451 +            (n, insts)
   7.452 +          else (n + 1, Inttab.cons_list (id, rthm) insts)
   7.453 +        val next_grounds' =
   7.454 +          add_new_grounds used_grounds new_grounds thm' next_grounds
   7.455 +        val cx' = (next_grounds', n_insts')
   7.456 +      in if reached_limit ctxt n then raise ENOUGH cx' else cx' end
   7.457 +
   7.458 +    fun with_grounds (n, T) f subst (n', Us) =
   7.459 +      let
   7.460 +        fun matching U = (* one-step refinement of the given substitution *)
   7.461 +          (case try (Sign.typ_match thy (T, U)) subst of
   7.462 +            NONE => I
   7.463 +          | SOME subst' => f subst')
   7.464 +      in if n = n' then fold matching Us else I end
   7.465 +
   7.466 +    fun with_matching_ground c subst f =
   7.467 +      (* Try new grounds before already used grounds. Otherwise only
   7.468 +         substitutions already seen in previous rounds get enumerated. *)
   7.469 +      Symtab.fold (with_grounds c (f true) subst) new_grounds #>
   7.470 +      Symtab.fold (with_grounds c (f false) subst) used_grounds
   7.471 +
   7.472 +    fun is_complete subst =
   7.473 +      (* Check if a substitution is defined for all TVars of the theorem,
   7.474 +         which guarantees that the instantiation with this substitution results
   7.475 +         in a ground theorem since all matchings that led to this substitution
   7.476 +         are with ground types only. *)
   7.477 +      subset (op =) (tvars, Vartab.fold (cons o apsnd fst) subst [])
   7.478 +
   7.479 +    fun for_schematics _ [] _ = I
   7.480 +      | for_schematics used_new (c :: cs) subst =
   7.481 +          with_matching_ground c subst (fn new => fn subst' =>
   7.482 +            if is_complete subst' then
   7.483 +              if used_new orelse new then add subst'
   7.484 +              else I
   7.485 +            else for_schematics (used_new orelse new) cs subst') #>
   7.486 +          for_schematics used_new cs subst
   7.487    in
   7.488 -    if Symtab.is_empty known_grounds then
   7.489 -      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
   7.490 -    else
   7.491 -      make_subst_ctxt ctxt thm_infos known_grounds subs
   7.492 -      |> limit_rounds ctxt (collect_substitutions thm_infos)
   7.493 -      |> instantiate_all ctxt thm_infos
   7.494 +    (* Enumerate all substitutions that lead to a ground instance of the
   7.495 +       theorem not seen before. A necessary condition for such a new ground
   7.496 +       instance is the usage of at least one ground from the new_grounds
   7.497 +       table. The approach used here is to match all schematics of the theorem
   7.498 +       with all relevant grounds. *)
   7.499 +    for_schematics false schematics Vartab.empty cx
   7.500 +    handle ENOUGH cx' => cx'
   7.501    end
   7.502  
   7.503  
   7.504 +fun is_new round initial_round = (round = initial_round)
   7.505 +fun is_active round initial_round = (round > initial_round)
   7.506 +
   7.507 +
   7.508 +fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) =
   7.509 +  let
   7.510 +    val add_new = add_insts ctxt round
   7.511 +    fun consider_all pred f (cx as (_, (n, _))) =
   7.512 +      if reached_limit ctxt n then cx
   7.513 +      else fold_schematics pred f thm_infos cx
   7.514 +
   7.515 +    val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
   7.516 +    val empty_grounds = clear_grounds known_grounds'
   7.517 +
   7.518 +    val (new_grounds', insts') =
   7.519 +      (Symtab.empty, insts)
   7.520 +      |> consider_all (is_active round) (add_new known_grounds new_grounds)
   7.521 +      |> consider_all (is_new round) (add_new empty_grounds known_grounds')
   7.522 +
   7.523 +  in (known_grounds', new_grounds', insts') end
   7.524 +
   7.525 +
   7.526 +fun add_ground_types thm =
   7.527 +  let fun add (n, T) = Symtab.map_entry n (insert (op =) T)
   7.528 +  in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end
   7.529 +
   7.530 +
   7.531 +fun collect_instances ctxt thm_infos consts =
   7.532 +  let
   7.533 +    val known_grounds = fold_grounds add_ground_types thm_infos consts
   7.534 +    val empty_grounds = clear_grounds known_grounds
   7.535 +  in
   7.536 +    (empty_grounds, known_grounds, (0, Inttab.empty))
   7.537 +    |> limit_rounds ctxt (find_instances thm_infos)
   7.538 +    |> (fn (_, _, (_, insts)) => insts)
   7.539 +  end
   7.540 +
   7.541 +
   7.542 +
   7.543 +(* monomorphization *)
   7.544 +
   7.545 +fun instantiated_thms _ (Ground thm) = [(0, thm)]
   7.546 +  | instantiated_thms _ Ignored = []
   7.547 +  | instantiated_thms insts (Schematic {id, ...}) = Inttab.lookup_list insts id
   7.548 +
   7.549 +
   7.550 +fun monomorph schematic_consts_of ctxt rthms =
   7.551 +  let
   7.552 +    val (thm_infos, consts) = prepare schematic_consts_of rthms
   7.553 +    val insts =
   7.554 +      if Symtab.is_empty consts then Inttab.empty
   7.555 +      else collect_instances ctxt thm_infos consts
   7.556 +  in map (instantiated_thms insts) thm_infos end
   7.557 +
   7.558  end
   7.559 -