# HG changeset patch
# User boehmes
# Date 1301572923 -7200
# Node ID 173b0f488428e06e58ff4e77b9108eae64226305
# Parent  a630978fc96758053212332ce7537c50189c0d16
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)

diff -r a630978fc967 -r 173b0f488428 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:54 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 14:02:03 2011 +0200
@@ -29,7 +29,7 @@
 signature SMT_MONOMORPH =
 sig
   val typ_has_tvars: typ -> bool
-  val monomorph: ('a * thm) list -> Proof.context ->
+  val monomorph: bool -> ('a * thm) list -> Proof.context ->
     ('a * thm) list * Proof.context
 end
 
@@ -160,37 +160,44 @@
 
   in most_specific [] end
 
-fun instantiate (i, thm) substs (ithms, ctxt) =
+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
 
-    val thy = ProofContext.theory_of ctxt'
+    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) ? Vartab.update vT
+      |> 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 (i, Thm.instantiate (cTs, []) thm) end
+      in SOME (i, Thm.instantiate (cTs, []) thm) end
+      handle PARTIAL_INST () => NONE
 
-  in (map inst substs @ ithms, ctxt') end
+  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
 
 
 
 (* overall procedure *)
 
-fun mono_all ctxt polys monos =
+fun mono_all full ctxt polys monos =
   let
     val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
 
@@ -209,13 +216,13 @@
     |> search_substitutions ctxt limit instances Symtab.empty grounds
     |> map (filter_most_specific (ProofContext.theory_of ctxt))
     |> rpair (monos, ctxt)
-    |-> fold2 instantiate polys
+    |-> fold2 (instantiate full) polys
   end
 
-fun monomorph irules ctxt =
+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 ctxt polys)
+  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
 
 end
diff -r a630978fc967 -r 173b0f488428 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 31 11:16:54 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Mar 31 14:02:03 2011 +0200
@@ -631,7 +631,7 @@
   |> gen_normalize ctxt
   |> unfold1 ctxt
   |> rpair ctxt
-  |-> SMT_Monomorph.monomorph
+  |-> SMT_Monomorph.monomorph true
   |-> unfold2
   |-> apply_extra_norms
 
diff -r a630978fc967 -r 173b0f488428 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:54 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 14:02:03 2011 +0200
@@ -355,7 +355,7 @@
         val (mono_facts, ctxt') =
           ctxt |> Config.put SMT_Config.verbose debug
                |> Config.put SMT_Config.monomorph_limit monomorphize_limit
-               |> SMT_Monomorph.monomorph indexed_facts
+               |> SMT_Monomorph.monomorph true indexed_facts
       in
         mono_facts
         |> sort (int_ord o pairself fst)