author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36898 8e55aa1306c5
child 38864 4abe644fcea5
permissions -rw-r--r--
tuned titles

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

Monomorphization of theorems, i.e., computation of all (necessary) instances.

signature SMT_MONOMORPH =
  val monomorph: thm list -> Proof.context -> thm list * Proof.context

structure SMT_Monomorph: SMT_MONOMORPH =

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 "op ="}, @{const_name},
  @{const_name}, @{const_name number_of}]

fun is_const f (n, T) = not (ignored n) andalso f T
fun add_const_if f g (Const c) = if is_const f c then g c else I
  | add_const_if _ _ _ = I

fun collect_consts_if f g thm =
  Term.fold_aterms (add_const_if f g) (Thm.prop_of thm)

fun add_consts f =
  collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))

val insert_const = OrdList.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 incr_indexes thms =
  let fun inc thm idx = (Thm.incr_indexes idx thm, Thm.maxidx_of thm + idx + 1)
  in fst (fold_map inc thms 0) end

(* Compute all substitutions from the types "Ts" to all relevant
   types in "grounds", with respect to the given substitution. *)
fun new_substitutions thy grounds (n, T) subst =
  if not (typ_has_tvars T) then [subst]
    Symtab.lookup_list grounds n
    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
    |> cons subst

(* Instantiate a set of constants with a substitution.  Also collect
   all new ground instances for the next round of specialization. *)
fun apply_subst grounds consts subst =
    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)
        |> is_new_ground c ? Symtab.insert_list (op =) c
        |> pair c
  in fold_map apply_const consts #>> pair subst end

(* Compute new substitutions for the theorem "thm", based on
   previously found substitutions.
     Also collect new grounds, i.e., instantiated constants
   (without schematic types) which do not occur in any of the
   previous rounds. Note that thus no schematic type variables are
   shared among theorems. *)
fun specialize thy all_grounds new_grounds (thm, scs) =
    fun spec (subst, consts) next_grounds =
      |> fold (maps o new_substitutions thy new_grounds) consts
      |> rpair next_grounds
      |-> fold_map (apply_subst all_grounds consts)
    fold_map spec scs #>> (fn scss =>
    (thm, fold (fold (insert (eq_snd (op =)))) scss []))

(* Compute all necessary substitutions.
     Instead of operating on the propositions of the theorems, the
   computation uses only the constants occurring with schematic type
   variables in the propositions. To ease comparisons, such sets of
   costants are always kept in their initial order. *)
fun incremental_monomorph thy limit all_grounds new_grounds ths =
    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    val spec = specialize thy all_grounds' new_grounds
    val (ths', new_grounds') = fold_map spec ths Symtab.empty
    if Symtab.is_empty new_grounds' then ths'
    else if limit > 0
    then incremental_monomorph thy (limit-1) all_grounds' new_grounds' ths'
    else (warning "SMT: monomorphization limit reached"; ths')

fun filter_most_specific thy =
    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
            if exists (match cs) css orelse exists (match cs o snd) scs
            then substs else ss :: substs

  in most_specific [] end

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

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

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

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

  in uncurry (map o inst) end

fun mono_all ctxt _ [] monos = (monos, ctxt)
  | mono_all ctxt limit polys monos =
        fun invent_types thm ctxt =
          let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
            |> Variable.invent_types Ss
            |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
        val (Tenvs, ctxt') = fold_map invent_types polys ctxt

        val thy = ProofContext.theory_of ctxt'

        val ths = polys
          |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))

        (* all constant names occurring with schematic types *)
        val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []

        (* all known instances with non-schematic types *)
        val grounds =
          Symtab.make (map (rpair []) ns)
          |> fold (add_consts (K true)) monos
          |> fold (add_consts (not o typ_has_tvars)) polys
        |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
        |> incremental_monomorph thy limit Symtab.empty grounds
        |> map (apsnd (filter_most_specific thy))
        |> flat o map2 (instantiate thy) Tenvs
        |> append monos
        |> rpair ctxt'

val monomorph_limit = 10

(* Instantiate all polymorphic constants (i.e., constants occurring
   both with ground types and type variables) with all (necessary)
   ground types; thereby create copies of theorems containing those
     To prevent non-termination, there is an upper limit for the
   number of recursions involved in the fixpoint construction.
     The initial set of theorems must not contain any schematic term
   variables, and the final list of theorems does not contain any
   schematic type variables anymore. *)
fun monomorph thms ctxt =
  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of)
  |>> incr_indexes
  |-> mono_all ctxt monomorph_limit