src/HOL/Tools/SMT/smt_monomorph.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40512 fd218201da5e
child 41063 0828bfa70b20
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/smt_monomorph.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Monomorphization of theorems, i.e., computation of all (necessary) instances.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature SMT_MONOMORPH =
boehmes@36898
     8
sig
boehmes@40161
     9
  val monomorph: (int * thm) list -> Proof.context ->
boehmes@40161
    10
    (int * thm) list * Proof.context
boehmes@36898
    11
end
boehmes@36898
    12
boehmes@36898
    13
structure SMT_Monomorph: SMT_MONOMORPH =
boehmes@36898
    14
struct
boehmes@36898
    15
boehmes@36898
    16
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
boehmes@36898
    17
boehmes@36898
    18
val ignored = member (op =) [
boehmes@36898
    19
  @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
boehmes@40512
    20
  @{const_name HOL.eq}]
boehmes@36898
    21
boehmes@36898
    22
fun is_const f (n, T) = not (ignored n) andalso f T
boehmes@36898
    23
fun add_const_if f g (Const c) = if is_const f c then g c else I
boehmes@36898
    24
  | add_const_if _ _ _ = I
boehmes@36898
    25
boehmes@36898
    26
fun collect_consts_if f g thm =
boehmes@36898
    27
  Term.fold_aterms (add_const_if f g) (Thm.prop_of thm)
boehmes@36898
    28
boehmes@36898
    29
fun add_consts f =
boehmes@36898
    30
  collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
boehmes@36898
    31
wenzelm@39687
    32
val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
boehmes@36898
    33
fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
boehmes@36898
    34
boehmes@36898
    35
boehmes@40161
    36
fun incr_indexes irules =
boehmes@40161
    37
  let
boehmes@40161
    38
    fun inc (i, thm) idx =
boehmes@40161
    39
      ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
boehmes@40161
    40
  in fst (fold_map inc irules 0) end
boehmes@36898
    41
boehmes@36898
    42
boehmes@36898
    43
(* Compute all substitutions from the types "Ts" to all relevant
boehmes@36898
    44
   types in "grounds", with respect to the given substitution. *)
boehmes@36898
    45
fun new_substitutions thy grounds (n, T) subst =
boehmes@36898
    46
  if not (typ_has_tvars T) then [subst]
boehmes@36898
    47
  else
boehmes@36898
    48
    Symtab.lookup_list grounds n
boehmes@36898
    49
    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
boehmes@36898
    50
    |> cons subst
boehmes@36898
    51
boehmes@36898
    52
boehmes@36898
    53
(* Instantiate a set of constants with a substitution.  Also collect
boehmes@36898
    54
   all new ground instances for the next round of specialization. *)
boehmes@36898
    55
fun apply_subst grounds consts subst =
boehmes@36898
    56
  let
boehmes@36898
    57
    fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
boehmes@36898
    58
      not (member (op =) (Symtab.lookup_list grounds n) T)
boehmes@36898
    59
boehmes@36898
    60
    fun apply_const (n, T) new_grounds =
boehmes@36898
    61
      let val c = (n, Envir.subst_type subst T)
boehmes@36898
    62
      in
boehmes@36898
    63
        new_grounds
boehmes@36898
    64
        |> is_new_ground c ? Symtab.insert_list (op =) c
boehmes@36898
    65
        |> pair c
boehmes@36898
    66
      end
boehmes@36898
    67
  in fold_map apply_const consts #>> pair subst end
boehmes@36898
    68
boehmes@36898
    69
boehmes@36898
    70
(* Compute new substitutions for the theorem "thm", based on
boehmes@36898
    71
   previously found substitutions.
boehmes@36898
    72
     Also collect new grounds, i.e., instantiated constants
boehmes@36898
    73
   (without schematic types) which do not occur in any of the
boehmes@36898
    74
   previous rounds. Note that thus no schematic type variables are
boehmes@36898
    75
   shared among theorems. *)
boehmes@40161
    76
fun specialize thy all_grounds new_grounds (irule, scs) =
boehmes@36898
    77
  let
boehmes@36898
    78
    fun spec (subst, consts) next_grounds =
boehmes@36898
    79
      [subst]
boehmes@36898
    80
      |> fold (maps o new_substitutions thy new_grounds) consts
boehmes@36898
    81
      |> rpair next_grounds
boehmes@36898
    82
      |-> fold_map (apply_subst all_grounds consts)
boehmes@36898
    83
  in
boehmes@36898
    84
    fold_map spec scs #>> (fn scss =>
boehmes@40161
    85
    (irule, fold (fold (insert (eq_snd (op =)))) scss []))
boehmes@36898
    86
  end
boehmes@36898
    87
boehmes@36898
    88
boehmes@36898
    89
(* Compute all necessary substitutions.
boehmes@36898
    90
     Instead of operating on the propositions of the theorems, the
boehmes@36898
    91
   computation uses only the constants occurring with schematic type
boehmes@36898
    92
   variables in the propositions. To ease comparisons, such sets of
boehmes@36898
    93
   costants are always kept in their initial order. *)
boehmes@40424
    94
fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
boehmes@36898
    95
  let
boehmes@40424
    96
    val thy = ProofContext.theory_of ctxt
boehmes@36898
    97
    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
boehmes@36898
    98
    val spec = specialize thy all_grounds' new_grounds
boehmes@40161
    99
    val (irs, new_grounds') = fold_map spec irules Symtab.empty
boehmes@36898
   100
  in
boehmes@40161
   101
    if Symtab.is_empty new_grounds' then irs
boehmes@36898
   102
    else if limit > 0
boehmes@40424
   103
    then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
boehmes@40424
   104
    else
boehmes@40424
   105
     (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
boehmes@40424
   106
      (); irs)
boehmes@36898
   107
  end
boehmes@36898
   108
boehmes@36898
   109
boehmes@36898
   110
fun filter_most_specific thy =
boehmes@36898
   111
  let
boehmes@36898
   112
    fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
boehmes@36898
   113
boehmes@36898
   114
    fun is_trivial subst = Vartab.is_empty subst orelse
boehmes@36898
   115
      forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
boehmes@36898
   116
boehmes@36898
   117
    fun match general specific =
boehmes@36898
   118
      (case try (fold2 typ_match general specific) Vartab.empty of
boehmes@36898
   119
        NONE => false
boehmes@36898
   120
      | SOME subst => not (is_trivial subst))
boehmes@36898
   121
boehmes@36898
   122
    fun most_specific _ [] = []
boehmes@36898
   123
      | most_specific css ((ss, cs) :: scs) =
boehmes@36898
   124
          let val substs = most_specific (cs :: css) scs
boehmes@36898
   125
          in
boehmes@36898
   126
            if exists (match cs) css orelse exists (match cs o snd) scs
boehmes@36898
   127
            then substs else ss :: substs
boehmes@36898
   128
          end
boehmes@36898
   129
boehmes@36898
   130
  in most_specific [] end
boehmes@36898
   131
boehmes@36898
   132
boehmes@36898
   133
fun instantiate thy Tenv =
boehmes@36898
   134
  let
boehmes@36898
   135
    fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
boehmes@36898
   136
      | replace _ T = T
boehmes@36898
   137
boehmes@36898
   138
    fun complete (vT as (v, _)) subst =
boehmes@36898
   139
      subst
boehmes@36898
   140
      |> not (Vartab.defined subst v) ? Vartab.update vT
haftmann@39020
   141
      |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
boehmes@36898
   142
boehmes@36898
   143
    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
boehmes@36898
   144
boehmes@40161
   145
    fun inst (i, thm) subst =
boehmes@36898
   146
      let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
boehmes@40161
   147
      in (i, Thm.instantiate (cTs, []) thm) end
boehmes@36898
   148
boehmes@36898
   149
  in uncurry (map o inst) end
boehmes@36898
   150
boehmes@36898
   151
boehmes@36898
   152
fun mono_all ctxt _ [] monos = (monos, ctxt)
boehmes@36898
   153
  | mono_all ctxt limit polys monos =
boehmes@36898
   154
      let
boehmes@40161
   155
        fun invent_types (_, thm) ctxt =
boehmes@36898
   156
          let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
boehmes@36898
   157
          in
boehmes@36898
   158
            ctxt
boehmes@36898
   159
            |> Variable.invent_types Ss
boehmes@36898
   160
            |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
boehmes@36898
   161
          end
boehmes@36898
   162
        val (Tenvs, ctxt') = fold_map invent_types polys ctxt
boehmes@36898
   163
boehmes@36898
   164
        val thy = ProofContext.theory_of ctxt'
boehmes@36898
   165
boehmes@36898
   166
        val ths = polys
boehmes@40161
   167
          |> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)]))
boehmes@36898
   168
boehmes@36898
   169
        (* all constant names occurring with schematic types *)
boehmes@36898
   170
        val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []
boehmes@36898
   171
boehmes@36898
   172
        (* all known instances with non-schematic types *)
boehmes@36898
   173
        val grounds =
boehmes@36898
   174
          Symtab.make (map (rpair []) ns)
boehmes@40161
   175
          |> fold (add_consts (K true) o snd) monos
boehmes@40161
   176
          |> fold (add_consts (not o typ_has_tvars) o snd) polys
boehmes@36898
   177
      in
boehmes@36898
   178
        polys
boehmes@40161
   179
        |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
boehmes@40424
   180
        |> incremental_monomorph ctxt' limit Symtab.empty grounds
boehmes@36898
   181
        |> map (apsnd (filter_most_specific thy))
boehmes@36898
   182
        |> flat o map2 (instantiate thy) Tenvs
boehmes@36898
   183
        |> append monos
boehmes@36898
   184
        |> rpair ctxt'
boehmes@36898
   185
      end
boehmes@36898
   186
boehmes@36898
   187
boehmes@36898
   188
(* Instantiate all polymorphic constants (i.e., constants occurring
boehmes@36898
   189
   both with ground types and type variables) with all (necessary)
boehmes@36898
   190
   ground types; thereby create copies of theorems containing those
boehmes@36898
   191
   constants.
boehmes@36898
   192
     To prevent non-termination, there is an upper limit for the
boehmes@36898
   193
   number of recursions involved in the fixpoint construction.
boehmes@36898
   194
     The initial set of theorems must not contain any schematic term
boehmes@36898
   195
   variables, and the final list of theorems does not contain any
boehmes@36898
   196
   schematic type variables anymore. *)
boehmes@40161
   197
fun monomorph irules ctxt =
boehmes@40161
   198
  irules
boehmes@40161
   199
  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
boehmes@36898
   200
  |>> incr_indexes
boehmes@40424
   201
  |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
boehmes@36898
   202
boehmes@36898
   203
end