src/HOL/Tools/monomorph.ML
author boehmes
Mon, 05 Sep 2011 11:28:10 +0200
changeset 44717 c9cf0780cd4f
parent 43272 878c0935a4a4
child 51575 907efc894051
permissions -rw-r--r--
filter out all schematic theorems if the problem contains no ground constants
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43107
5792d6bb4fb1 fixed comment
blanchet
parents: 43041
diff changeset
     1
(*  Title:      HOL/Tools/monomorph.ML
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     3
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     4
Monomorphization of theorems, i.e., computation of all (necessary)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     5
instances.  This procedure is incomplete in general, but works well for
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     6
most practical problems.
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     7
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     8
For a list of universally closed theorems (without schematic term
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
     9
variables), monomorphization computes a list of theorems with schematic
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    10
term variables: all polymorphic constants (i.e., constants occurring both
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    11
with ground types and schematic type variables) are instantiated with all
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    12
(necessary) ground types; thereby theorems containing these constants are
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    13
copied.  To prevent nontermination, there is an upper limit for the number
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    14
of iterations involved in the fixpoint construction.
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    15
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    16
The search for instances is performed on the constants with schematic
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    17
types, which are extracted from the initial set of theorems.  The search
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    18
constructs, for each theorem with those constants, a set of substitutions,
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    19
which, in the end, is applied to all corresponding theorems.  Remaining
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    20
schematic type variables are substituted with fresh types.
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    21
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    22
Searching for necessary substitutions is an iterative fixpoint
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    23
construction: each iteration computes all required instances required by
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    24
the ground instances computed in the previous step and which haven't been
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    25
found before.  Computed substitutions are always nontrivial: schematic type
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    26
variables are never mapped to schematic type variables.
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    27
*)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    28
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    29
signature MONOMORPH =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    30
sig
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    31
  (* utility function *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    32
  val typ_has_tvars: typ -> bool
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    33
  val all_schematic_consts_of: term -> typ list Symtab.table
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    34
  val add_schematic_consts_of: term -> typ list Symtab.table ->
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    35
    typ list Symtab.table
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    36
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    37
  (* configuration options *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    38
  val max_rounds: int Config.T
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    39
  val max_new_instances: int Config.T
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43225
diff changeset
    40
  val keep_partial_instances: bool Config.T
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    41
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    42
  (* monomorphization *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    43
  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    44
    Proof.context -> (int * thm) list list * Proof.context
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    45
end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    46
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    47
structure Monomorph: MONOMORPH =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    48
struct
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    49
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    50
(* utility functions *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    51
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    52
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    53
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    54
fun add_schematic_const (c as (_, T)) =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    55
  if typ_has_tvars T then Symtab.insert_list (op =) c else I
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    56
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    57
fun add_schematic_consts_of t =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    58
  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    59
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    60
fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    61
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    62
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    63
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    64
(* configuration options *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    65
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    66
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    67
val max_new_instances =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    68
  Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43225
diff changeset
    69
val keep_partial_instances =
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43225
diff changeset
    70
  Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    71
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    72
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    73
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    74
(* monomorphization *)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    75
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    76
(** preparing the problem **)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    77
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    78
datatype thm_info =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    79
  Ground of thm |
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    80
  Schematic of {
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    81
    index: int,
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    82
    theorem: thm,
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    83
    tvars: (indexname * sort) list,
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    84
    schematics: typ list Symtab.table,
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    85
    initial_round: int }
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    86
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    87
fun prepare schematic_consts_of rthms =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    88
  let
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
    89
    val empty_sub = ((0, false, false), Vartab.empty)
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
    90
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
    91
    fun prep (r, thm) ((i, idx), (consts, subs)) =
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    92
      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
    93
        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    94
      else
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    95
        let
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    96
          (* increase indices to avoid clashes of type variables *)
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    97
          val thm' = Thm.incr_indexes idx thm
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    98
          val idx' = Thm.maxidx_of thm' + 1
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
    99
          val schematics = schematic_consts_of (Thm.prop_of thm')
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   100
          val consts' =
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   101
            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   102
          val subs' = Inttab.update (i, [empty_sub]) subs
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   103
          val thm_info = Schematic {
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   104
            index = i,
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   105
            theorem = thm',
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   106
            tvars = Term.add_tvars (Thm.prop_of thm') [],
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   107
            schematics = schematics,
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   108
            initial_round = r }
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   109
      in (thm_info, ((i+1, idx'), (consts', subs'))) end
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   110
  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   111
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   112
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   113
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   114
(** collecting substitutions **)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   115
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   116
fun exceeded limit = (limit <= 0)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   117
fun exceeded_limit (limit, _, _) = exceeded limit
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   118
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   119
43272
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   120
fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => 
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   121
  Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   122
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   123
fun eq_subst (subst1, subst2) =
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   124
  derived_subst subst1 subst2 andalso derived_subst subst2 subst1
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   125
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   126
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   127
fun with_all_grounds cx grounds f =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   128
  if exceeded_limit cx then I else Symtab.fold f grounds
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   129
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   130
fun with_all_type_combinations cx schematics f (n, Ts) =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   131
  if exceeded_limit cx then I
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   132
  else fold_product f (Symtab.lookup_list schematics n) Ts
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   133
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   134
fun derive_new_substs thy cx new_grounds schematics subst =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   135
  with_all_grounds cx new_grounds
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   136
    (with_all_type_combinations cx schematics (fn T => fn U =>
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   137
      (case try (Sign.typ_match thy (T, U)) subst of
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   138
        NONE => I
43272
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   139
      | SOME subst' => insert eq_subst subst'))) []
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   140
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   141
43272
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   142
fun known_subst sub subs1 subs2 subst' =
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   143
  let fun derived (_, subst) = derived_subst subst' subst
878c0935a4a4 only collect substituions neither seen before nor derived in the same refinement step
boehmes
parents: 43251
diff changeset
   144
  in derived sub orelse exists derived subs1 orelse exists derived subs2 end
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   145
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   146
fun within_limit f cx = if exceeded_limit cx then cx else f cx
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   147
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   148
fun fold_partial_substs derive add = within_limit (
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   149
  let
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   150
    fun fold_partial [] cx = cx
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   151
      | fold_partial (sub :: subs) (limit, subs', next) =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   152
          if exceeded limit then (limit, sub :: subs @ subs', next)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   153
          else sub |> (fn ((generation, full, _), subst) =>
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   154
            if full then fold_partial subs (limit, sub :: subs', next)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   155
            else
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   156
              (case filter_out (known_subst sub subs subs') (derive subst) of
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   157
                [] => fold_partial subs (limit, sub :: subs', next)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   158
              | substs =>
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   159
                  (limit, ((generation, full, true), subst) :: subs', next)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   160
                  |> fold (within_limit o add) substs
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   161
                  |> fold_partial subs))
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   162
  in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   163
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   164
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   165
fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   166
  let
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   167
    val thy = Proof_Context.theory_of ctxt
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43225
diff changeset
   168
    val count_partial = Config.get ctxt keep_partial_instances
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   169
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   170
    fun add_new_ground subst n T =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   171
      let val T' = Envir.subst_type subst T
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   172
      in
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   173
        (* FIXME: maybe keep types in a table or net for known_grounds,
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   174
           that might improve efficiency here
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   175
        *)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   176
        if typ_has_tvars T' then I
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   177
        else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   178
        else Symtab.cons_list (n, T')
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   179
      end
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   180
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   181
    fun add_new_subst subst (limit, subs, next_grounds) =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   182
      let
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   183
        val full = forall (Vartab.defined subst o fst) tvars
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   184
        val limit' =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   185
          if full orelse count_partial then limit - 1 else limit
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   186
        val sub = ((round, full, false), subst)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   187
        val next_grounds' =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   188
          (schematics, next_grounds)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   189
          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   190
      in (limit', sub :: subs, next_grounds') end
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   191
  in
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   192
    fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   193
      add_new_subst cx
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   194
  end
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   195
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   196
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   197
(*
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   198
  'known_grounds' are all constant names known to occur schematically
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   199
  associated with all ground instances considered so far
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   200
*)
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   201
fun add_relevant_instances known_grounds (Const (c as (n, T))) =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   202
      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   203
      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   204
      else Symtab.insert_list (op =) c
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   205
  | add_relevant_instances _ _ = I
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   206
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   207
fun collect_instances known_grounds thm =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   208
  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   209
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   210
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   211
fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   212
  let
43251
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   213
    (* The total limit of returned (ground) facts is the number of facts
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   214
       given to the monomorphizer increased by max_new_instances.  Since
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   215
       initially ground facts are returned anyway, the limit here is not
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   216
       counting them. *)
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   217
    val limit = Config.get ctxt max_new_instances + 
f4d15a58ed8b clarified (and slightly modified) the semantics of max_new_instances
boehmes
parents: 43234
diff changeset
   218
      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   219
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   220
    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   221
      | add_ground_consts (Schematic _) = I
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   222
    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   223
  in (known_grounds, (limit, substitutions, initial_grounds)) end
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   224
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   225
fun is_new round initial_round = (round = initial_round)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   226
fun is_active round initial_round = (round > initial_round)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   227
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   228
fun fold_schematic pred f = fold (fn
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   229
    Schematic {index, theorem, tvars, schematics, initial_round} =>
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   230
      if pred initial_round then f theorem (index, tvars, schematics) else I
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   231
  | Ground _ => I)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   232
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   233
fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   234
  let
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   235
    val (limit', isubs', next_grounds') =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   236
      (limit, Inttab.lookup_list subs index, next_grounds)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   237
      |> f (tvars, schematics)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   238
  in (limit', Inttab.update (index, isubs') subs, next_grounds') end
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   239
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   240
fun collect_substitutions thm_infos ctxt round subst_ctxt =
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   241
  let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   242
  in
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   243
    if exceeded limit then subst_ctxt
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   244
    else
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   245
      let
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   246
        fun collect thm _ = collect_instances known_grounds thm
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   247
        val new = fold_schematic (is_new round) collect thm_infos next_grounds
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   248
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   249
        val known' = Symtab.merge_list (op =) (known_grounds, new)
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   250
        val step = focus o refine ctxt round known'
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   251
      in
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   252
        (limit, subs, Symtab.empty)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   253
        |> not (Symtab.is_empty new) ?
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   254
            fold_schematic (is_active round) (step new) thm_infos
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   255
        |> fold_schematic (is_new round) (step known') thm_infos
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   256
        |> pair known'
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   257
      end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   258
  end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   259
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   260
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   261
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   262
(** instantiating schematic theorems **)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   263
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   264
fun super_sort (Ground _) S = S
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   265
  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   266
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   267
fun new_super_type ctxt thm_infos =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   268
  let val S = fold super_sort thm_infos @{sort type}
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   269
  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   270
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   271
fun add_missing_tvar T (ix, S) subst =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   272
  if Vartab.defined subst ix then subst
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   273
  else Vartab.update (ix, (S, T)) subst
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   274
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   275
fun complete tvars subst T =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   276
  subst
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   277
  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   278
  |> fold (add_missing_tvar T) tvars
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   279
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   280
fun instantiate_all' (mT, ctxt) subs thm_infos =
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   281
  let
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   282
    val thy = Proof_Context.theory_of ctxt
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   283
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   284
    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   285
    fun cert' subst = Vartab.fold (cons o cert) subst []
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   286
    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   287
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   288
    fun with_subst tvars f ((generation, full, _), subst) =
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   289
      if full then SOME (generation, f subst)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   290
      else Option.map (pair generation o f o complete tvars subst) mT
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   291
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   292
    fun inst (Ground thm) = [(0, thm)]
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   293
      | inst (Schematic {theorem, tvars, index, ...}) =
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   294
          Inttab.lookup_list subs index
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   295
          |> map_filter (with_subst tvars (instantiate theorem))
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   296
  in (map inst thm_infos, ctxt) end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   297
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   298
fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
43230
dabf6e311213 clarified meaning of monomorphization configuration option by renaming it
boehmes
parents: 43225
diff changeset
   299
  if Config.get ctxt keep_partial_instances then
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   300
    let fun is_refined ((_, _, refined), _) = refined
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   301
    in
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   302
      (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   303
      |-> instantiate_all' (new_super_type ctxt thm_infos)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   304
    end
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   305
  else instantiate_all' (NONE, ctxt) subs thm_infos
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   306
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   307
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   308
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   309
(** overall procedure **)
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   310
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   311
fun limit_rounds ctxt f =
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   312
  let
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   313
    val max = Config.get ctxt max_rounds
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   314
    fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   315
  in round 1 end
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   316
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   317
fun monomorph schematic_consts_of rthms ctxt =
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   318
  let
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   319
    val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   320
  in
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   321
    if Symtab.is_empty known_grounds then
44717
c9cf0780cd4f filter out all schematic theorems if the problem contains no ground constants
boehmes
parents: 43272
diff changeset
   322
      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   323
    else
43117
5de84843685f proper nesting of loops in new monomorphizer;
boehmes
parents: 43116
diff changeset
   324
      make_subst_ctxt ctxt thm_infos known_grounds subs
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   325
      |> limit_rounds ctxt (collect_substitutions thm_infos)
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   326
      |> instantiate_all ctxt thm_infos
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   327
  end
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 43107
diff changeset
   328
43041
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   329
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   330
end
218e3943d504 added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
boehmes
parents:
diff changeset
   331