src/HOL/SMT/Tools/smt_monomorph.ML

added new method "smt": an oracle-based connection to external SMT solvers

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

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

signature SMT_MONOMORPH =
sig
  val monomorph: theory -> term list -> term list
end

structure SMT_Monomorph: SMT_MONOMORPH =
struct

fun selection [] = []
  | selection (x :: xs) = (x, xs) :: map (apsnd (cons x)) (selection xs)

fun permute [] = []
  | permute [x] = [[x]]
  | permute xs = maps (fn (y, ys) => map (cons y) (permute ys)) (selection xs)

fun fold_all f = fold (fn x => maps (f x))


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

val ignored = member (op =) [
  @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
  @{const_name "op ="}, @{const_name zero_class.zero},
  @{const_name one_class.one}, @{const_name number_of}]
fun consts_of ts = AList.group (op =) (fold Term.add_consts ts [])
  |> filter_out (ignored o fst)

val join_consts = curry (AList.join (op =) (K (merge (op =))))
fun diff_consts cs ds = 
  let fun diff (n, Ts) =
    (case AList.lookup (op =) cs n of
      NONE => SOME (n, Ts)
    | SOME Us =>
        let val Ts' = fold (remove (op =)) Us Ts
        in if null Ts' then NONE else SOME (n, Ts') end)
  in map_filter diff ds end

fun instances thy is (n, Ts) env =
  let
    val Us = these (AList.lookup (op =) is n)
    val Ts' = filter typ_has_tvars (map (Envir.subst_type env) Ts)
  in
    (case map_product pair Ts' Us of
      [] => [env]
    | TUs => map_filter (try (fn TU => Sign.typ_match thy TU env)) TUs)
  end

fun proper_match ps env =
  forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps

val eq_tab = gen_eq_set (op =) o pairself Vartab.dest

fun specialize thy cs is ((r, ps), ces) (ts, ns) =
  let
    val ps' = filter (AList.defined (op =) is o fst) ps

    val envs = permute ps'
      |> maps (fn ps => fold_all (instances thy is) ps [Vartab.empty])
      |> filter (proper_match ps')
      |> filter_out (member eq_tab ces)
      |> distinct eq_tab

    val us = map (fn env => Envir.subst_term_types env r) envs
    val ns' = join_consts (diff_consts is (diff_consts cs (consts_of us))) ns
  in (envs @ ces, (fold (insert (op aconv)) us ts, ns')) end


fun incr_tvar_indices i t =
  let
    val incrT = Logic.incr_tvar i

    fun incr t =
      (case t of
        Const (n, T) => Const (n, incrT T)
      | Free (n, T) => Free (n, incrT T)
      | Abs (n, T, t1) => Abs (n, incrT T, incr t1)
      | t1 $ t2 => incr t1 $ incr t2
      | _ => t)
  in incr t end


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 terms containing those constants.
   To prevent non-termination, there is an upper limit for the number of
   recursions involved in the fixpoint construction. *)
fun monomorph thy ts =
  let
    val (ps, ms) = List.partition term_has_tvars ts

    fun with_tvar (n, Ts) =
      let val Ts' = filter typ_has_tvars Ts
      in if null Ts' then NONE else SOME (n, Ts') end
    fun incr t idx = (incr_tvar_indices idx t, idx + Term.maxidx_of_term t + 1)
    val rps = fst (fold_map incr ps 0)
      |> map (fn r => (r, map_filter with_tvar (consts_of [r])))

    fun mono count is ces cs ts =
      let
        val spec = specialize thy cs is
        val (ces', (ts', is')) = fold_map spec (rps ~~ ces) (ts, [])
        val cs' = join_consts is cs
      in
        if null is' then ts'
        else if count > monomorph_limit then
          (Output.warning "monomorphization limit reached"; ts')
        else mono (count + 1) is' ces' cs' ts'
      end
  in mono 0 (consts_of ms) (map (K []) rps) [] ms end

end