src/HOL/Tools/SMT/smt_monomorph.ML

provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

(*  Title:      HOL/Tools/SMT/smt_monomorph.ML
    Author:     Sascha Boehme, TU Muenchen

Monomorphization of theorems, i.e., computation of all (necessary)
instances.  This procedure is incomplete in general, but works well for
most practical problems.

For a list of universally closed theorems (without schematic term
variables), monomorphization computes a list of theorems with schematic
term variables: all polymorphic constants (i.e., constants occurring both
with ground types and schematic type variables) are instantiated with all
(necessary) ground types; thereby theorems containing these constants are
copied.  To prevent non-termination, there is an upper limit for the number
of iterations involved in the fixpoint construction.

The search for instances is performed on the constants with schematic
types, which are extracted from the initial set of theorems.  The search
constructs, for each theorem with those constants, a set of substitutions,
which, in the end, is applied to all corresponding theorems.  Remaining
schematic type variables are substituted with fresh types.

Searching for necessary substitutions is an iterative fixpoint
construction: each iteration computes all required instances required by
the ground instances computed in the previous step and which haven't been
found before.  Computed substitutions are always nontrivial: schematic type
variables are never mapped to schematic type variables.
*)

signature SMT_MONOMORPH =
sig
  val typ_has_tvars: typ -> bool
  val monomorph: bool -> ('a * thm) list -> Proof.context ->
    ('a * thm) list * Proof.context
end

structure SMT_Monomorph: SMT_MONOMORPH =
struct

(* utility functions *)

fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat)

fun pair_trans ((x, y), z) = (x, (y, z))

val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)

val ignored = member (op =) [@{const_name All}, @{const_name Ex},
  @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]

fun is_const pred (n, T) = not (ignored n) andalso pred T

fun collect_consts_if pred f =
  let
    fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
      | collect (t $ u) = collect t #> collect u
      | collect (Abs (_, _, t)) = collect t
      | collect (Const c) = if is_const pred c then f c else I
      | collect _ = I
    and collect_trigger t =
      let val dest = these o try HOLogic.dest_list 
      in fold (fold collect_pat o dest) (dest t) end
    and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
      | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
      | collect_pat _ = I
  in collect o Thm.prop_of end

val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)

fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []

fun add_const_types pred =
  collect_consts_if pred (fn (n, T) => Symtab.map_entry n (insert (op =) T))

fun incr_indexes ithms =
  let
    fun inc (i, thm) idx =
      ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
  in fst (fold_map inc ithms 0) end



(* search for necessary substitutions *)

fun new_substitutions thy limit grounds (n, T) subst instances =
  if not (typ_has_tvars T) then ([subst], instances)
  else
    Symtab.lookup_list grounds n
    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
    |> (fn substs => (substs, instances - length substs))
    |>> take limit (* limit the breadth of the search as well as the width *)
    |>> cons subst

fun apply_subst grounds consts subst =
  let
    fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
      not (member (op =) (Symtab.lookup_list grounds n) T)

    fun apply_const (n, T) new_grounds =
      let val c = (n, Envir.subst_type subst T)
      in
        new_grounds
        |> is_new_ground c ? Symtab.insert_list (op =) c
        |> pair c
      end
  in fold_map apply_const consts #>> pair subst end

fun specialize thy limit all_grounds new_grounds scs =
  let
    fun spec (subst, consts) (next_grounds, instances) =
      ([subst], instances)
      |> fold_maps (new_substitutions thy limit new_grounds) consts
      |>> rpair next_grounds
      |>> uncurry (fold_map (apply_subst all_grounds consts))
      |> pair_trans
  in
    fold_map spec scs #>> (fn scss =>
    fold (fold (insert (eq_snd (op =)))) scss [])
  end

val limit_reached_warning = "Warning: Monomorphization limit reached"

fun search_substitutions ctxt limit instances all_grounds new_grounds scss =
  let
    val thy = ProofContext.theory_of ctxt
    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    val spec = specialize thy limit all_grounds' new_grounds
    val (scss', (new_grounds', instances')) =
      fold_map spec scss (Symtab.empty, instances)
  in
    if Symtab.is_empty new_grounds' then scss'
    else if limit > 0 andalso instances' > 0 then
      search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds'
        scss'
    else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss')
  end



(* instantiation *)

fun filter_most_specific thy =
  let
    fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)

    fun is_trivial subst = Vartab.is_empty subst orelse
      forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)

    fun match general specific =
      (case try (fold2 typ_match general specific) Vartab.empty of
        NONE => false
      | SOME subst => not (is_trivial subst))

    fun most_specific _ [] = []
      | most_specific css ((ss, cs) :: scs) =
          let val substs = most_specific (cs :: css) scs
          in
            if exists (match cs) css orelse exists (match cs o snd) scs
            then substs else ss :: substs
          end

  in most_specific [] end

fun instantiate full (i, thm) substs (ithms, ctxt) =
  let
    val thy = ProofContext.theory_of ctxt

    val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
    val (Tenv, ctxt') =
      ctxt
      |> Variable.invent_types Ss
      |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs

    exception PARTIAL_INST of unit

    fun update_subst vT subst =
      if full then Vartab.update vT subst
      else raise PARTIAL_INST ()

    fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
      | replace _ T = T

    fun complete (vT as (v, _)) subst =
      subst
      |> not (Vartab.defined subst v) ? update_subst vT
      |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))

    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)

    fun inst subst =
      let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
      in SOME (i, Thm.instantiate (cTs, []) thm) end
      handle PARTIAL_INST () => NONE

  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end



(* overall procedure *)

fun mono_all full ctxt polys monos =
  let
    val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys

    (* all known non-schematic instances of polymorphic constants: find all
       names of polymorphic constants, then add all known ground types *)
    val grounds =
      Symtab.empty
      |> fold (fold (fold (Symtab.update o rpair [] o fst) o snd)) scss
      |> fold (add_const_types (K true) o snd) monos
      |> fold (add_const_types (not o typ_has_tvars) o snd) polys

    val limit = Config.get ctxt SMT_Config.monomorph_limit
    val instances = Config.get ctxt SMT_Config.monomorph_instances
  in
    scss
    |> search_substitutions ctxt limit instances Symtab.empty grounds
    |> map (filter_most_specific (ProofContext.theory_of ctxt))
    |> rpair (monos, ctxt)
    |-> fold2 (instantiate full) polys
  end

fun monomorph full irules ctxt =
  irules
  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
  |>> incr_indexes  (* avoid clashes of schematic type variables *)
  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)

end