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