src/HOL/Tools/monomorph.ML
changeset 43116 e0add071fa10
parent 43107 5792d6bb4fb1
child 43117 5de84843685f
     1.1 --- a/src/HOL/Tools/monomorph.ML	Tue May 31 18:13:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/monomorph.ML	Tue May 31 19:21:20 2011 +0200
     1.3 @@ -91,31 +91,29 @@
     1.4      schematics: typ list Symtab.table,
     1.5      initial_round: int }
     1.6  
     1.7 -fun make_thm_info index initial_round schematics thm =
     1.8 -  if Symtab.is_empty schematics then Ground thm
     1.9 -  else Schematic {
    1.10 -    index = index,
    1.11 -    theorem = thm,
    1.12 -    tvars = Term.add_tvars (Thm.prop_of thm) [],
    1.13 -    schematics = schematics,
    1.14 -    initial_round = initial_round }
    1.15 -
    1.16  fun prepare schematic_consts_of rthms =
    1.17    let
    1.18      val empty_subst = ((0, false, false), Vartab.empty)
    1.19  
    1.20      fun prep (r, thm) ((i, idx), (consts, substs)) =
    1.21 -      let
    1.22 -        (* increase indices to avoid clashes of type variables *)
    1.23 -        val thm' = Thm.incr_indexes idx thm
    1.24 -        val idx' = Thm.maxidx_of thm' + 1
    1.25 -        val schematics = schematic_consts_of (Thm.prop_of thm')
    1.26 -        val consts' =
    1.27 -          Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
    1.28 -        val substs' = Inttab.update (i, [empty_subst]) substs
    1.29 -      in
    1.30 -        (make_thm_info i r schematics thm', ((i+1, idx'), (consts', substs')))
    1.31 -      end
    1.32 +      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
    1.33 +        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, substs)))
    1.34 +      else
    1.35 +        let
    1.36 +          (* increase indices to avoid clashes of type variables *)
    1.37 +          val thm' = Thm.incr_indexes idx thm
    1.38 +          val idx' = Thm.maxidx_of thm' + 1
    1.39 +          val schematics = schematic_consts_of (Thm.prop_of thm')
    1.40 +          val consts' =
    1.41 +            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
    1.42 +          val substs' = Inttab.update (i, [empty_subst]) substs
    1.43 +          val thm_info = Schematic {
    1.44 +            index = i,
    1.45 +            theorem = thm',
    1.46 +            tvars = Term.add_tvars (Thm.prop_of thm') [],
    1.47 +            schematics = schematics,
    1.48 +            initial_round = r }
    1.49 +      in (thm_info, ((i+1, idx'), (consts', substs'))) end
    1.50    in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
    1.51  
    1.52  
    1.53 @@ -212,14 +210,14 @@
    1.54    end
    1.55  
    1.56  
    1.57 -fun make_subst_ctxt ctxt thm_infos (known_grounds, substitutions) =
    1.58 +fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
    1.59    let
    1.60      val limit = Config.get ctxt max_new_instances
    1.61  
    1.62      fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
    1.63        | add_ground_consts (Schematic _) = I
    1.64      val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
    1.65 -  in (thm_infos, (known_grounds, (limit, substitutions, initial_grounds))) end
    1.66 +  in (known_grounds, (limit, substitutions, initial_grounds)) end
    1.67  
    1.68  fun with_new round f thm_info =
    1.69    (case thm_info of
    1.70 @@ -235,7 +233,7 @@
    1.71        else f (round, index, theorem, tvars, schematics)
    1.72    | Ground _ => I)
    1.73  
    1.74 -fun collect_substitutions ctxt round thm_infos (known_grounds, subst_ctxt) =
    1.75 +fun collect_substitutions thm_infos ctxt round (known_grounds, subst_ctxt) =
    1.76    let val (limit, substitutions, next_grounds) = subst_ctxt
    1.77    in
    1.78      (*
    1.79 @@ -311,24 +309,31 @@
    1.80  
    1.81  (** overall procedure **)
    1.82  
    1.83 -fun limit_rounds ctxt f thm_infos =
    1.84 +fun limit_rounds ctxt f =
    1.85    let
    1.86      val max = Config.get ctxt max_rounds
    1.87  
    1.88 -    fun round _ (true, x) = (thm_infos, x)
    1.89 +    fun round _ (true, x) = x
    1.90        | round i (_, x) =
    1.91 -          if i <= max then round (i + 1) (f ctxt i thm_infos x)
    1.92 +          if i <= max then round (i + 1) (f ctxt i x)
    1.93            else (
    1.94              show_info ctxt "Warning: Monomorphization limit reached";
    1.95 -            (thm_infos, x))
    1.96 +            x)
    1.97    in round 1 o pair false end
    1.98  
    1.99  fun monomorph schematic_consts_of rthms ctxt =
   1.100 -  rthms
   1.101 -  |> prepare schematic_consts_of
   1.102 -  |-> make_subst_ctxt ctxt
   1.103 -  |-> limit_rounds ctxt collect_substitutions
   1.104 -  |-> instantiate_all ctxt
   1.105 +  let
   1.106 +    val (thm_infos, (known_grounds, substitutions)) =
   1.107 +      prepare schematic_consts_of rthms
   1.108 +  in
   1.109 +    if Symtab.is_empty known_grounds then
   1.110 +      (map (single o pair 0 o snd) rthms, ctxt)
   1.111 +    else
   1.112 +      make_subst_ctxt ctxt thm_infos known_grounds substitutions
   1.113 +      |> limit_rounds ctxt (collect_substitutions thm_infos)
   1.114 +      |> instantiate_all ctxt thm_infos
   1.115 +  end
   1.116 +
   1.117  
   1.118  end
   1.119