src/HOL/Tools/monomorph.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 57209 7ffa0f7e2775
child 59058 a78612c67ec0
permissions -rw-r--r--
specialized specification: avoid trivial instances
blanchet@43107
     1
(*  Title:      HOL/Tools/monomorph.ML
boehmes@43041
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@43041
     3
boehmes@51575
     4
Monomorphization of theorems, i.e., computation of ground instances for
boehmes@51575
     5
theorems with type variables.  This procedure is incomplete in general,
boehmes@51575
     6
but works well for most practical problems.
boehmes@43041
     7
boehmes@51575
     8
Monomorphization is essentially an enumeration of substitutions that map
boehmes@51575
     9
schematic types to ground types. Applying these substitutions to theorems
boehmes@51575
    10
with type variables results in monomorphized ground instances. The
boehmes@51575
    11
enumeration is driven by schematic constants (constants occurring with
boehmes@51575
    12
type variables) and all ground instances of such constants (occurrences
boehmes@51575
    13
without type variables). The enumeration is organized in rounds in which
boehmes@51575
    14
all substitutions for the schematic constants are computed that are induced
boehmes@51575
    15
by the ground instances. Any new ground instance may induce further
boehmes@51575
    16
substitutions in a subsequent round. To prevent nontermination, there is
boehmes@51575
    17
an upper limit of rounds involved and of the number of monomorphized ground
boehmes@51575
    18
instances computed.
boehmes@43041
    19
boehmes@51575
    20
Theorems to be monomorphized must be tagged with a number indicating the
boehmes@51575
    21
initial round in which they participate first. The initial round is
boehmes@51575
    22
ignored for theorems without type variables. For any other theorem, the
boehmes@51575
    23
initial round must be greater than zero. Returned monomorphized theorems
boehmes@51575
    24
carry a number showing from which monomorphization round they emerged.
boehmes@43041
    25
*)
boehmes@43041
    26
boehmes@43041
    27
signature MONOMORPH =
boehmes@43041
    28
sig
boehmes@51575
    29
  (* utility functions *)
boehmes@43041
    30
  val typ_has_tvars: typ -> bool
boehmes@43041
    31
  val all_schematic_consts_of: term -> typ list Symtab.table
boehmes@43041
    32
  val add_schematic_consts_of: term -> typ list Symtab.table ->
boehmes@43041
    33
    typ list Symtab.table
boehmes@43041
    34
boehmes@43041
    35
  (* configuration options *)
boehmes@43041
    36
  val max_rounds: int Config.T
boehmes@43041
    37
  val max_new_instances: int Config.T
blanchet@53480
    38
  val max_thm_instances: int Config.T
blanchet@54061
    39
  val max_new_const_instances_per_round: int Config.T
boehmes@43041
    40
boehmes@43041
    41
  (* monomorphization *)
boehmes@51575
    42
  val monomorph: (term -> typ list Symtab.table) -> Proof.context ->
boehmes@51575
    43
    (int * thm) list -> (int * thm) list list
boehmes@43041
    44
end
boehmes@43041
    45
boehmes@43041
    46
structure Monomorph: MONOMORPH =
boehmes@43041
    47
struct
boehmes@43041
    48
boehmes@43041
    49
(* utility functions *)
boehmes@43041
    50
boehmes@43041
    51
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
boehmes@43041
    52
boehmes@43041
    53
fun add_schematic_const (c as (_, T)) =
boehmes@43041
    54
  if typ_has_tvars T then Symtab.insert_list (op =) c else I
boehmes@43041
    55
boehmes@43041
    56
fun add_schematic_consts_of t =
boehmes@43041
    57
  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
boehmes@43041
    58
boehmes@43041
    59
fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
boehmes@43041
    60
boehmes@51575
    61
fun clear_grounds grounds = Symtab.map (K (K [])) grounds
boehmes@51575
    62
boehmes@43041
    63
boehmes@43041
    64
(* configuration options *)
boehmes@43041
    65
boehmes@43041
    66
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
boehmes@51575
    67
boehmes@43041
    68
val max_new_instances =
blanchet@57209
    69
  Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 500)
boehmes@43041
    70
blanchet@53480
    71
val max_thm_instances =
blanchet@54061
    72
  Attrib.setup_config_int @{binding monomorph_max_thm_instances} (K 20)
blanchet@54061
    73
blanchet@54061
    74
val max_new_const_instances_per_round =
blanchet@57209
    75
  Attrib.setup_config_int @{binding monomorph_max_new_const_instances_per_round} (K 5)
blanchet@53480
    76
boehmes@43116
    77
fun limit_rounds ctxt f =
boehmes@43041
    78
  let
boehmes@43041
    79
    val max = Config.get ctxt max_rounds
boehmes@43117
    80
    fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
boehmes@43117
    81
  in round 1 end
boehmes@43041
    82
boehmes@51575
    83
boehmes@51575
    84
(* theorem information and related functions *)
boehmes@51575
    85
boehmes@51575
    86
datatype thm_info =
boehmes@51575
    87
  Ground of thm |
boehmes@51575
    88
  Ignored |
boehmes@51575
    89
  Schematic of {
boehmes@51575
    90
    id: int,
boehmes@51575
    91
    theorem: thm,
boehmes@51575
    92
    tvars: (indexname * sort) list,
boehmes@51575
    93
    schematics: (string * typ) list,
boehmes@51575
    94
    initial_round: int}
boehmes@51575
    95
boehmes@51575
    96
fun fold_grounds f = fold (fn Ground thm => f thm | _ => I)
boehmes@51575
    97
boehmes@51575
    98
fun fold_schematic f thm_info =
boehmes@51575
    99
  (case thm_info of
boehmes@51575
   100
    Schematic {id, theorem, tvars, schematics, initial_round} =>
boehmes@51575
   101
      f id theorem tvars schematics initial_round
boehmes@51575
   102
  | _ => I)
boehmes@51575
   103
boehmes@51575
   104
fun fold_schematics pred f =
boehmes@51575
   105
  let
boehmes@51575
   106
    fun apply id thm tvars schematics initial_round x =
boehmes@51575
   107
      if pred initial_round then f id thm tvars schematics x else x
boehmes@51575
   108
  in fold (fold_schematic apply) end
boehmes@51575
   109
boehmes@51575
   110
boehmes@51575
   111
(* collecting data *)
boehmes@51575
   112
boehmes@51575
   113
(*
boehmes@51575
   114
  Theorems with type variables that cannot be instantiated should be ignored.
boehmes@51575
   115
  A type variable has only a chance to be instantiated if it occurs in the
boehmes@51575
   116
  type of one of the schematic constants.
boehmes@51575
   117
*)
boehmes@51575
   118
fun groundable all_tvars schematics =
boehmes@51575
   119
  let val tvars' = Symtab.fold (fold Term.add_tvarsT o snd) schematics []
boehmes@51575
   120
  in forall (member (op =) tvars') all_tvars end
boehmes@51575
   121
boehmes@51575
   122
boehmes@51575
   123
fun prepare schematic_consts_of rthms =
boehmes@43116
   124
  let
boehmes@51575
   125
    fun prep (initial_round, thm) ((id, idx), consts) =
boehmes@51575
   126
      if Term.exists_type typ_has_tvars (Thm.prop_of thm) then
boehmes@51575
   127
        let
boehmes@51575
   128
          (* increase indices to avoid clashes of type variables *)
boehmes@51575
   129
          val thm' = Thm.incr_indexes idx thm
boehmes@51575
   130
          val idx' = Thm.maxidx_of thm' + 1
boehmes@51575
   131
boehmes@51575
   132
          val tvars = Term.add_tvars (Thm.prop_of thm') []
boehmes@51575
   133
          val schematics = schematic_consts_of (Thm.prop_of thm')
boehmes@51575
   134
          val schematics' =
boehmes@51575
   135
            Symtab.fold (fn (n, Ts) => fold (cons o pair n) Ts) schematics []
boehmes@51575
   136
boehmes@51575
   137
          (* collect the names of all constants that need to be instantiated *)
boehmes@51575
   138
          val consts' =
boehmes@51575
   139
            consts
boehmes@51575
   140
            |> Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics
boehmes@51575
   141
boehmes@51575
   142
          val thm_info =
boehmes@51575
   143
            if not (groundable tvars schematics) then Ignored
boehmes@51575
   144
            else
boehmes@51575
   145
              Schematic {
boehmes@51575
   146
                id = id,
boehmes@51575
   147
                theorem = thm',
boehmes@51575
   148
                tvars = tvars,
boehmes@51575
   149
                schematics = schematics',
boehmes@51575
   150
                initial_round = initial_round}
boehmes@51575
   151
        in (thm_info, ((id + 1, idx'), consts')) end
boehmes@51575
   152
      else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts))
blanchet@57209
   153
  in
blanchet@57209
   154
    fold_map prep rthms ((0, 0), Symtab.empty) ||> snd
blanchet@57209
   155
  end
boehmes@51575
   156
boehmes@51575
   157
boehmes@51575
   158
(* collecting instances *)
boehmes@51575
   159
boehmes@51575
   160
fun instantiate thy subst =
boehmes@51575
   161
  let
boehmes@51575
   162
    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
boehmes@51575
   163
    fun cert' subst = Vartab.fold (cons o cert) subst []
boehmes@51575
   164
  in Thm.instantiate (cert' subst, []) end
boehmes@51575
   165
boehmes@51575
   166
fun add_new_grounds used_grounds new_grounds thm =
boehmes@51575
   167
  let
boehmes@51575
   168
    fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T
boehmes@51575
   169
    fun add (Const (c as (n, _))) =
boehmes@51575
   170
          if mem used_grounds c orelse mem new_grounds c then I
boehmes@51575
   171
          else if not (Symtab.defined used_grounds n) then I
boehmes@51575
   172
          else Symtab.insert_list (op =) c
boehmes@51575
   173
      | add _ = I
boehmes@51575
   174
  in Term.fold_aterms add (Thm.prop_of thm) end
boehmes@51575
   175
blanchet@53823
   176
fun add_insts max_instances max_thm_insts ctxt round used_grounds
blanchet@53482
   177
    new_grounds id thm tvars schematics cx =
boehmes@51575
   178
  let
boehmes@51575
   179
    exception ENOUGH of
blanchet@53823
   180
      typ list Symtab.table * (int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table)
boehmes@51575
   181
boehmes@51575
   182
    val thy = Proof_Context.theory_of ctxt
boehmes@51575
   183
blanchet@53481
   184
    fun add subst (cx as (next_grounds, (n, insts))) =
blanchet@53481
   185
      if n >= max_instances then
blanchet@53481
   186
        raise ENOUGH cx
blanchet@53481
   187
      else
blanchet@53481
   188
        let
blanchet@53481
   189
          val thm' = instantiate thy subst thm
blanchet@53823
   190
          val rthm = ((round, subst), thm')
blanchet@53481
   191
          val rthms = Inttab.lookup_list insts id;
blanchet@53481
   192
          val n_insts' =
blanchet@53823
   193
            if member (eq_snd Thm.eq_thm) rthms rthm then
blanchet@53481
   194
              (n, insts)
blanchet@53481
   195
            else
blanchet@53823
   196
              (if length rthms >= max_thm_insts then n else n + 1,
blanchet@53823
   197
               Inttab.cons_list (id, rthm) insts)
blanchet@53481
   198
          val next_grounds' =
blanchet@53481
   199
            add_new_grounds used_grounds new_grounds thm' next_grounds
blanchet@53481
   200
        in (next_grounds', n_insts') end
boehmes@51575
   201
boehmes@51575
   202
    fun with_grounds (n, T) f subst (n', Us) =
boehmes@51575
   203
      let
boehmes@51575
   204
        fun matching U = (* one-step refinement of the given substitution *)
boehmes@51575
   205
          (case try (Sign.typ_match thy (T, U)) subst of
boehmes@51575
   206
            NONE => I
boehmes@51575
   207
          | SOME subst' => f subst')
boehmes@51575
   208
      in if n = n' then fold matching Us else I end
boehmes@51575
   209
boehmes@51575
   210
    fun with_matching_ground c subst f =
boehmes@51575
   211
      (* Try new grounds before already used grounds. Otherwise only
boehmes@51575
   212
         substitutions already seen in previous rounds get enumerated. *)
boehmes@51575
   213
      Symtab.fold (with_grounds c (f true) subst) new_grounds #>
boehmes@51575
   214
      Symtab.fold (with_grounds c (f false) subst) used_grounds
boehmes@51575
   215
boehmes@51575
   216
    fun is_complete subst =
boehmes@51575
   217
      (* Check if a substitution is defined for all TVars of the theorem,
boehmes@51575
   218
         which guarantees that the instantiation with this substitution results
boehmes@51575
   219
         in a ground theorem since all matchings that led to this substitution
boehmes@51575
   220
         are with ground types only. *)
boehmes@51575
   221
      subset (op =) (tvars, Vartab.fold (cons o apsnd fst) subst [])
boehmes@51575
   222
boehmes@51575
   223
    fun for_schematics _ [] _ = I
boehmes@51575
   224
      | for_schematics used_new (c :: cs) subst =
boehmes@51575
   225
          with_matching_ground c subst (fn new => fn subst' =>
boehmes@51575
   226
            if is_complete subst' then
boehmes@51575
   227
              if used_new orelse new then add subst'
boehmes@51575
   228
              else I
boehmes@51575
   229
            else for_schematics (used_new orelse new) cs subst') #>
boehmes@51575
   230
          for_schematics used_new cs subst
boehmes@43116
   231
  in
boehmes@51575
   232
    (* Enumerate all substitutions that lead to a ground instance of the
boehmes@51575
   233
       theorem not seen before. A necessary condition for such a new ground
boehmes@51575
   234
       instance is the usage of at least one ground from the new_grounds
boehmes@51575
   235
       table. The approach used here is to match all schematics of the theorem
boehmes@51575
   236
       with all relevant grounds. *)
boehmes@51575
   237
    for_schematics false schematics Vartab.empty cx
boehmes@51575
   238
    handle ENOUGH cx' => cx'
boehmes@43116
   239
  end
boehmes@43116
   240
boehmes@51575
   241
fun is_new round initial_round = (round = initial_round)
boehmes@51575
   242
fun is_active round initial_round = (round > initial_round)
boehmes@51575
   243
blanchet@57209
   244
fun find_instances max_instances max_thm_insts max_new_grounds thm_infos ctxt round
blanchet@57209
   245
    (known_grounds, new_grounds0, insts) =
boehmes@51575
   246
  let
blanchet@54061
   247
    val new_grounds =
blanchet@54061
   248
      Symtab.map (fn _ => fn grounds =>
blanchet@54061
   249
        if length grounds <= max_new_grounds then grounds
blanchet@54061
   250
        else take max_new_grounds (sort Term_Ord.typ_ord grounds)) new_grounds0
blanchet@54061
   251
blanchet@53823
   252
    val add_new = add_insts max_instances max_thm_insts ctxt round
boehmes@51575
   253
    fun consider_all pred f (cx as (_, (n, _))) =
blanchet@53481
   254
      if n >= max_instances then cx else fold_schematics pred f thm_infos cx
boehmes@51575
   255
boehmes@51575
   256
    val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
boehmes@51575
   257
    val empty_grounds = clear_grounds known_grounds'
boehmes@51575
   258
boehmes@51575
   259
    val (new_grounds', insts') =
boehmes@51575
   260
      (Symtab.empty, insts)
boehmes@51575
   261
      |> consider_all (is_active round) (add_new known_grounds new_grounds)
boehmes@51575
   262
      |> consider_all (is_new round) (add_new empty_grounds known_grounds')
blanchet@57209
   263
  in
blanchet@57209
   264
    (known_grounds', new_grounds', insts')
blanchet@57209
   265
  end
boehmes@51575
   266
boehmes@51575
   267
fun add_ground_types thm =
boehmes@51575
   268
  let fun add (n, T) = Symtab.map_entry n (insert (op =) T)
boehmes@51575
   269
  in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end
boehmes@51575
   270
blanchet@54061
   271
fun collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts =
boehmes@51575
   272
  let
boehmes@51575
   273
    val known_grounds = fold_grounds add_ground_types thm_infos consts
boehmes@51575
   274
    val empty_grounds = clear_grounds known_grounds
blanchet@53482
   275
    val max_instances = Config.get ctxt max_new_instances
blanchet@53481
   276
      |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos
boehmes@51575
   277
  in
boehmes@51575
   278
    (empty_grounds, known_grounds, (0, Inttab.empty))
blanchet@54061
   279
    |> limit_rounds ctxt (find_instances max_instances max_thm_insts
blanchet@54061
   280
      max_new_grounds thm_infos)
boehmes@51575
   281
    |> (fn (_, _, (_, insts)) => insts)
boehmes@51575
   282
  end
boehmes@51575
   283
boehmes@51575
   284
boehmes@51575
   285
(* monomorphization *)
boehmes@51575
   286
blanchet@53823
   287
fun size_of_subst subst =
blanchet@53823
   288
  Vartab.fold (Integer.add o size_of_typ o snd o snd) subst 0
blanchet@53823
   289
blanchet@53833
   290
fun subst_ord subst = int_ord (pairself size_of_subst subst)
boehmes@51575
   291
blanchet@53823
   292
fun instantiated_thms _ _ (Ground thm) = [(0, thm)]
blanchet@53823
   293
  | instantiated_thms _ _ Ignored = []
blanchet@53823
   294
  | instantiated_thms max_thm_insts insts (Schematic {id, ...}) =
blanchet@53823
   295
    Inttab.lookup_list insts id
blanchet@53823
   296
    |> (fn rthms => if length rthms <= max_thm_insts then rthms
blanchet@53823
   297
      else take max_thm_insts
blanchet@53823
   298
        (sort (prod_ord int_ord subst_ord o pairself fst) rthms))
blanchet@53823
   299
    |> map (apfst fst)
boehmes@51575
   300
boehmes@51575
   301
fun monomorph schematic_consts_of ctxt rthms =
boehmes@51575
   302
  let
blanchet@53823
   303
    val max_thm_insts = Config.get ctxt max_thm_instances
blanchet@54061
   304
    val max_new_grounds = Config.get ctxt max_new_const_instances_per_round
boehmes@51575
   305
    val (thm_infos, consts) = prepare schematic_consts_of rthms
boehmes@51575
   306
    val insts =
boehmes@51575
   307
      if Symtab.is_empty consts then Inttab.empty
blanchet@54061
   308
      else collect_instances ctxt max_thm_insts max_new_grounds thm_infos consts
blanchet@53823
   309
  in map (instantiated_thms max_thm_insts insts) thm_infos end
boehmes@51575
   310
boehmes@43041
   311
end