# HG changeset patch
# User boehmes
# Date 1311146589 -7200
# Node ID 3a87cb597832c7f933471e3f71dfd97d30d1ca86
# Parent  bce3de79c8ce405a54781b7a207e0b8038fcf1bb
removed old (unused) SMT monomorphizer

diff -r bce3de79c8ce -r 3a87cb597832 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 20 09:23:09 2011 +0200
@@ -373,7 +373,6 @@
   Tools/SMT/smt_config.ML \
   Tools/SMT/smt_datatypes.ML \
   Tools/SMT/smt_failure.ML \
-  Tools/SMT/smt_monomorph.ML \
   Tools/SMT/smt_normalize.ML \
   Tools/SMT/smt_setup_solvers.ML \
   Tools/SMT/smt_solver.ML \
diff -r bce3de79c8ce -r 3a87cb597832 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Jul 20 08:46:17 2011 +0200
+++ b/src/HOL/SMT.thy	Wed Jul 20 09:23:09 2011 +0200
@@ -10,7 +10,6 @@
   "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_failure.ML"
   "Tools/SMT/smt_config.ML"
-  ("Tools/SMT/smt_monomorph.ML")
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_datatypes.ML")
   ("Tools/SMT/smt_normalize.ML")
@@ -135,7 +134,6 @@
 
 subsection {* Setup *}
 
-use "Tools/SMT/smt_monomorph.ML"
 use "Tools/SMT/smt_builtin.ML"
 use "Tools/SMT/smt_datatypes.ML"
 use "Tools/SMT/smt_normalize.ML"
diff -r bce3de79c8ce -r 3a87cb597832 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Jul 20 08:46:17 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-(*  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: ('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 SMT.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 = Proof_Context.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 = Proof_Context.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 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
-    val full = Config.get ctxt SMT_Config.monomorph_full
-  in
-    scss
-    |> search_substitutions ctxt limit instances Symtab.empty grounds
-    |> map (filter_most_specific (Proof_Context.theory_of ctxt))
-    |> rpair (monos, ctxt)
-    |-> fold2 (instantiate full) polys
-  end
-
-fun monomorph 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 ctxt polys)
-
-end