src/HOL/Tools/SMT/smt_monomorph.ML
author boehmes
Thu Mar 31 14:02:03 2011 +0200 (2011-03-31)
changeset 42183 173b0f488428
parent 42181 8f25605e646c
child 42190 b6b5846504cd
permissions -rw-r--r--
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/smt_monomorph.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@41063
     4
Monomorphization of theorems, i.e., computation of all (necessary)
boehmes@41063
     5
instances.  This procedure is incomplete in general, but works well for
boehmes@41063
     6
most practical problems.
boehmes@41063
     7
boehmes@41063
     8
For a list of universally closed theorems (without schematic term
boehmes@41063
     9
variables), monomorphization computes a list of theorems with schematic
boehmes@41063
    10
term variables: all polymorphic constants (i.e., constants occurring both
boehmes@41063
    11
with ground types and schematic type variables) are instantiated with all
boehmes@41063
    12
(necessary) ground types; thereby theorems containing these constants are
boehmes@41063
    13
copied.  To prevent non-termination, there is an upper limit for the number
boehmes@41063
    14
of iterations involved in the fixpoint construction.
boehmes@41063
    15
boehmes@41063
    16
The search for instances is performed on the constants with schematic
boehmes@41063
    17
types, which are extracted from the initial set of theorems.  The search
boehmes@41063
    18
constructs, for each theorem with those constants, a set of substitutions,
boehmes@41063
    19
which, in the end, is applied to all corresponding theorems.  Remaining
boehmes@41063
    20
schematic type variables are substituted with fresh types.
boehmes@41063
    21
boehmes@41063
    22
Searching for necessary substitutions is an iterative fixpoint
boehmes@41063
    23
construction: each iteration computes all required instances required by
boehmes@41063
    24
the ground instances computed in the previous step and which haven't been
boehmes@41063
    25
found before.  Computed substitutions are always nontrivial: schematic type
boehmes@41063
    26
variables are never mapped to schematic type variables.
boehmes@36898
    27
*)
boehmes@36898
    28
boehmes@36898
    29
signature SMT_MONOMORPH =
boehmes@36898
    30
sig
blanchet@42181
    31
  val typ_has_tvars: typ -> bool
boehmes@42183
    32
  val monomorph: bool -> ('a * thm) list -> Proof.context ->
blanchet@42180
    33
    ('a * thm) list * Proof.context
boehmes@36898
    34
end
boehmes@36898
    35
boehmes@36898
    36
structure SMT_Monomorph: SMT_MONOMORPH =
boehmes@36898
    37
struct
boehmes@36898
    38
boehmes@41063
    39
(* utility functions *)
boehmes@41063
    40
boehmes@41762
    41
fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat)
boehmes@41762
    42
boehmes@41762
    43
fun pair_trans ((x, y), z) = (x, (y, z))
boehmes@41762
    44
boehmes@36898
    45
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
boehmes@36898
    46
boehmes@41063
    47
val ignored = member (op =) [@{const_name All}, @{const_name Ex},
boehmes@41063
    48
  @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
boehmes@36898
    49
boehmes@41063
    50
fun is_const pred (n, T) = not (ignored n) andalso pred T
boehmes@36898
    51
boehmes@41063
    52
fun collect_consts_if pred f =
boehmes@41174
    53
  let
boehmes@41174
    54
    fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
boehmes@41174
    55
      | collect (t $ u) = collect t #> collect u
boehmes@41174
    56
      | collect (Abs (_, _, t)) = collect t
boehmes@41174
    57
      | collect (Const c) = if is_const pred c then f c else I
boehmes@41174
    58
      | collect _ = I
boehmes@41174
    59
    and collect_trigger t =
boehmes@41174
    60
      let val dest = these o try HOLogic.dest_list 
boehmes@41174
    61
      in fold (fold collect_pat o dest) (dest t) end
boehmes@41174
    62
    and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
boehmes@41174
    63
      | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
boehmes@41174
    64
      | collect_pat _ = I
boehmes@41174
    65
  in collect o Thm.prop_of end
boehmes@36898
    66
wenzelm@39687
    67
val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
boehmes@41063
    68
boehmes@36898
    69
fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
boehmes@36898
    70
boehmes@41063
    71
fun add_const_types pred =
boehmes@41063
    72
  collect_consts_if pred (fn (n, T) => Symtab.map_entry n (insert (op =) T))
boehmes@36898
    73
boehmes@41063
    74
fun incr_indexes ithms =
boehmes@40161
    75
  let
boehmes@40161
    76
    fun inc (i, thm) idx =
boehmes@40161
    77
      ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
boehmes@41063
    78
  in fst (fold_map inc ithms 0) end
boehmes@36898
    79
boehmes@36898
    80
boehmes@41063
    81
boehmes@41063
    82
(* search for necessary substitutions *)
boehmes@41063
    83
boehmes@41762
    84
fun new_substitutions thy limit grounds (n, T) subst instances =
boehmes@41762
    85
  if not (typ_has_tvars T) then ([subst], instances)
boehmes@36898
    86
  else
boehmes@36898
    87
    Symtab.lookup_list grounds n
boehmes@36898
    88
    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
boehmes@41762
    89
    |> (fn substs => (substs, instances - length substs))
boehmes@41762
    90
    |>> take limit (* limit the breadth of the search as well as the width *)
boehmes@41762
    91
    |>> cons subst
boehmes@36898
    92
boehmes@36898
    93
fun apply_subst grounds consts subst =
boehmes@36898
    94
  let
boehmes@36898
    95
    fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
boehmes@36898
    96
      not (member (op =) (Symtab.lookup_list grounds n) T)
boehmes@36898
    97
boehmes@36898
    98
    fun apply_const (n, T) new_grounds =
boehmes@36898
    99
      let val c = (n, Envir.subst_type subst T)
boehmes@36898
   100
      in
boehmes@36898
   101
        new_grounds
boehmes@36898
   102
        |> is_new_ground c ? Symtab.insert_list (op =) c
boehmes@36898
   103
        |> pair c
boehmes@36898
   104
      end
boehmes@36898
   105
  in fold_map apply_const consts #>> pair subst end
boehmes@36898
   106
blanchet@41212
   107
fun specialize thy limit all_grounds new_grounds scs =
boehmes@36898
   108
  let
boehmes@41762
   109
    fun spec (subst, consts) (next_grounds, instances) =
boehmes@41762
   110
      ([subst], instances)
boehmes@41762
   111
      |> fold_maps (new_substitutions thy limit new_grounds) consts
boehmes@41762
   112
      |>> rpair next_grounds
boehmes@41762
   113
      |>> uncurry (fold_map (apply_subst all_grounds consts))
boehmes@41762
   114
      |> pair_trans
boehmes@36898
   115
  in
boehmes@36898
   116
    fold_map spec scs #>> (fn scss =>
boehmes@41063
   117
    fold (fold (insert (eq_snd (op =)))) scss [])
boehmes@36898
   118
  end
boehmes@36898
   119
boehmes@41063
   120
val limit_reached_warning = "Warning: Monomorphization limit reached"
boehmes@36898
   121
boehmes@41762
   122
fun search_substitutions ctxt limit instances all_grounds new_grounds scss =
boehmes@36898
   123
  let
boehmes@40424
   124
    val thy = ProofContext.theory_of ctxt
boehmes@36898
   125
    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
blanchet@41212
   126
    val spec = specialize thy limit all_grounds' new_grounds
boehmes@41762
   127
    val (scss', (new_grounds', instances')) =
boehmes@41762
   128
      fold_map spec scss (Symtab.empty, instances)
boehmes@36898
   129
  in
boehmes@41063
   130
    if Symtab.is_empty new_grounds' then scss'
boehmes@41762
   131
    else if limit > 0 andalso instances' > 0 then
boehmes@41762
   132
      search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds'
boehmes@41762
   133
        scss'
boehmes@41063
   134
    else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss')
boehmes@36898
   135
  end
boehmes@36898
   136
boehmes@36898
   137
boehmes@41063
   138
boehmes@41063
   139
(* instantiation *)
boehmes@41063
   140
boehmes@36898
   141
fun filter_most_specific thy =
boehmes@36898
   142
  let
boehmes@36898
   143
    fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
boehmes@36898
   144
boehmes@36898
   145
    fun is_trivial subst = Vartab.is_empty subst orelse
boehmes@36898
   146
      forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
boehmes@36898
   147
boehmes@36898
   148
    fun match general specific =
boehmes@36898
   149
      (case try (fold2 typ_match general specific) Vartab.empty of
boehmes@36898
   150
        NONE => false
boehmes@36898
   151
      | SOME subst => not (is_trivial subst))
boehmes@36898
   152
boehmes@36898
   153
    fun most_specific _ [] = []
boehmes@36898
   154
      | most_specific css ((ss, cs) :: scs) =
boehmes@36898
   155
          let val substs = most_specific (cs :: css) scs
boehmes@36898
   156
          in
boehmes@36898
   157
            if exists (match cs) css orelse exists (match cs o snd) scs
boehmes@36898
   158
            then substs else ss :: substs
boehmes@36898
   159
          end
boehmes@36898
   160
boehmes@36898
   161
  in most_specific [] end
boehmes@36898
   162
boehmes@42183
   163
fun instantiate full (i, thm) substs (ithms, ctxt) =
boehmes@41063
   164
  let
boehmes@42183
   165
    val thy = ProofContext.theory_of ctxt
boehmes@42183
   166
boehmes@41063
   167
    val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
boehmes@41063
   168
    val (Tenv, ctxt') =
boehmes@41063
   169
      ctxt
boehmes@41063
   170
      |> Variable.invent_types Ss
boehmes@41063
   171
      |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
boehmes@36898
   172
boehmes@42183
   173
    exception PARTIAL_INST of unit
boehmes@42183
   174
boehmes@42183
   175
    fun update_subst vT subst =
boehmes@42183
   176
      if full then Vartab.update vT subst
boehmes@42183
   177
      else raise PARTIAL_INST ()
boehmes@41063
   178
boehmes@36898
   179
    fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
boehmes@36898
   180
      | replace _ T = T
boehmes@36898
   181
boehmes@36898
   182
    fun complete (vT as (v, _)) subst =
boehmes@36898
   183
      subst
boehmes@42183
   184
      |> not (Vartab.defined subst v) ? update_subst vT
haftmann@39020
   185
      |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
boehmes@36898
   186
boehmes@36898
   187
    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
boehmes@36898
   188
boehmes@41063
   189
    fun inst subst =
boehmes@36898
   190
      let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
boehmes@42183
   191
      in SOME (i, Thm.instantiate (cTs, []) thm) end
boehmes@42183
   192
      handle PARTIAL_INST () => NONE
boehmes@36898
   193
boehmes@42183
   194
  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
boehmes@41063
   195
boehmes@36898
   196
boehmes@36898
   197
boehmes@41063
   198
(* overall procedure *)
boehmes@36898
   199
boehmes@42183
   200
fun mono_all full ctxt polys monos =
boehmes@41063
   201
  let
boehmes@41063
   202
    val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
boehmes@36898
   203
boehmes@41063
   204
    (* all known non-schematic instances of polymorphic constants: find all
boehmes@41063
   205
       names of polymorphic constants, then add all known ground types *)
boehmes@41063
   206
    val grounds =
boehmes@41063
   207
      Symtab.empty
boehmes@41063
   208
      |> fold (fold (fold (Symtab.update o rpair [] o fst) o snd)) scss
boehmes@41063
   209
      |> fold (add_const_types (K true) o snd) monos
boehmes@41063
   210
      |> fold (add_const_types (not o typ_has_tvars) o snd) polys
boehmes@36898
   211
boehmes@41063
   212
    val limit = Config.get ctxt SMT_Config.monomorph_limit
boehmes@41762
   213
    val instances = Config.get ctxt SMT_Config.monomorph_instances
boehmes@41063
   214
  in
boehmes@41063
   215
    scss
boehmes@41762
   216
    |> search_substitutions ctxt limit instances Symtab.empty grounds
boehmes@41063
   217
    |> map (filter_most_specific (ProofContext.theory_of ctxt))
boehmes@41063
   218
    |> rpair (monos, ctxt)
boehmes@42183
   219
    |-> fold2 (instantiate full) polys
boehmes@41063
   220
  end
boehmes@36898
   221
boehmes@42183
   222
fun monomorph full irules ctxt =
boehmes@40161
   223
  irules
boehmes@40161
   224
  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
boehmes@41063
   225
  |>> incr_indexes  (* avoid clashes of schematic type variables *)
boehmes@42183
   226
  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
boehmes@36898
   227
boehmes@36898
   228
end