# HG changeset patch
# User boehmes
# Date 1306862480 -7200
# Node ID e0add071fa1073688d088e0da0b4e2246fed9db8
# Parent  6773d8a9e35129a523f965bf39a70e5f5ecf4eaa
use new monomorphizer for SMT;
simplify the monomorphizer by inlining functions and proper passing of arguments

diff -r 6773d8a9e351 -r e0add071fa10 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue May 31 18:13:00 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue May 31 19:21:20 2011 +0200
@@ -626,12 +626,44 @@
     val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
 
+local
+  val ignored = member (op =) [@{const_name All}, @{const_name Ex},
+    @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
+
+  val schematic_consts_of =
+    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 (t as Const (n, _)) = 
+            if not (ignored n) then Monomorph.add_schematic_consts_of t 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 (fn t => collect t Symtab.empty) end
+in
+
+fun monomorph xthms ctxt =
+  let val (xs, thms) = split_list xthms
+  in
+    (map (pair 1) thms, ctxt)
+    |-> Monomorph.monomorph schematic_consts_of
+    |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
+  end
+
+end
+
 fun normalize iwthms ctxt =
   iwthms
   |> gen_normalize ctxt
   |> unfold1 ctxt
   |> rpair ctxt
-  |-> SMT_Monomorph.monomorph
+  |-> monomorph
   |-> unfold2
   |-> apply_extra_norms
 
diff -r 6773d8a9e351 -r e0add071fa10 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Tue May 31 18:13:00 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue May 31 19:21:20 2011 +0200
@@ -91,31 +91,29 @@
     schematics: typ list Symtab.table,
     initial_round: int }
 
-fun make_thm_info index initial_round schematics thm =
-  if Symtab.is_empty schematics then Ground thm
-  else Schematic {
-    index = index,
-    theorem = thm,
-    tvars = Term.add_tvars (Thm.prop_of thm) [],
-    schematics = schematics,
-    initial_round = initial_round }
-
 fun prepare schematic_consts_of rthms =
   let
     val empty_subst = ((0, false, false), Vartab.empty)
 
     fun prep (r, thm) ((i, idx), (consts, substs)) =
-      let
-        (* increase indices to avoid clashes of type variables *)
-        val thm' = Thm.incr_indexes idx thm
-        val idx' = Thm.maxidx_of thm' + 1
-        val schematics = schematic_consts_of (Thm.prop_of thm')
-        val consts' =
-          Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
-        val substs' = Inttab.update (i, [empty_subst]) substs
-      in
-        (make_thm_info i r schematics thm', ((i+1, idx'), (consts', substs')))
-      end
+      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
+        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, substs)))
+      else
+        let
+          (* increase indices to avoid clashes of type variables *)
+          val thm' = Thm.incr_indexes idx thm
+          val idx' = Thm.maxidx_of thm' + 1
+          val schematics = schematic_consts_of (Thm.prop_of thm')
+          val consts' =
+            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
+          val substs' = Inttab.update (i, [empty_subst]) substs
+          val thm_info = Schematic {
+            index = i,
+            theorem = thm',
+            tvars = Term.add_tvars (Thm.prop_of thm') [],
+            schematics = schematics,
+            initial_round = r }
+      in (thm_info, ((i+1, idx'), (consts', substs'))) end
   in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
 
 
@@ -212,14 +210,14 @@
   end
 
 
-fun make_subst_ctxt ctxt thm_infos (known_grounds, substitutions) =
+fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
   let
     val limit = Config.get ctxt max_new_instances
 
     fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
       | add_ground_consts (Schematic _) = I
     val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
-  in (thm_infos, (known_grounds, (limit, substitutions, initial_grounds))) end
+  in (known_grounds, (limit, substitutions, initial_grounds)) end
 
 fun with_new round f thm_info =
   (case thm_info of
@@ -235,7 +233,7 @@
       else f (round, index, theorem, tvars, schematics)
   | Ground _ => I)
 
-fun collect_substitutions ctxt round thm_infos (known_grounds, subst_ctxt) =
+fun collect_substitutions thm_infos ctxt round (known_grounds, subst_ctxt) =
   let val (limit, substitutions, next_grounds) = subst_ctxt
   in
     (*
@@ -311,24 +309,31 @@
 
 (** overall procedure **)
 
-fun limit_rounds ctxt f thm_infos =
+fun limit_rounds ctxt f =
   let
     val max = Config.get ctxt max_rounds
 
-    fun round _ (true, x) = (thm_infos, x)
+    fun round _ (true, x) = x
       | round i (_, x) =
-          if i <= max then round (i + 1) (f ctxt i thm_infos x)
+          if i <= max then round (i + 1) (f ctxt i x)
           else (
             show_info ctxt "Warning: Monomorphization limit reached";
-            (thm_infos, x))
+            x)
   in round 1 o pair false end
 
 fun monomorph schematic_consts_of rthms ctxt =
-  rthms
-  |> prepare schematic_consts_of
-  |-> make_subst_ctxt ctxt
-  |-> limit_rounds ctxt collect_substitutions
-  |-> instantiate_all ctxt
+  let
+    val (thm_infos, (known_grounds, substitutions)) =
+      prepare schematic_consts_of rthms
+  in
+    if Symtab.is_empty known_grounds then
+      (map (single o pair 0 o snd) rthms, ctxt)
+    else
+      make_subst_ctxt ctxt thm_infos known_grounds substitutions
+      |> limit_rounds ctxt (collect_substitutions thm_infos)
+      |> instantiate_all ctxt thm_infos
+  end
+
 
 end