# HG changeset patch
# User desharna
# Date 1614879536 -3600
# Node ID 96ef620c8b1eda5a1f9a366c4e5366df14ce5295
# Parent  a80fd78c85bd7f0052376d9ea953cc4c4fcea8e8
added upper bound on monomorphisation duplicate instances

diff -r a80fd78c85bd -r 96ef620c8b1e src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Thu Mar 04 11:06:39 2021 +0100
+++ b/src/HOL/Tools/monomorph.ML	Thu Mar 04 18:38:56 2021 +0100
@@ -37,6 +37,7 @@
   val max_new_instances: int Config.T
   val max_thm_instances: int Config.T
   val max_new_const_instances_per_round: int Config.T
+  val max_duplicated_instances: int Config.T
 
   (* monomorphization *)
   val monomorph: (term -> typ list Symtab.table) -> Proof.context ->
@@ -74,6 +75,9 @@
 val max_new_const_instances_per_round =
   Attrib.setup_config_int \<^binding>\<open>monomorph_max_new_const_instances_per_round\<close> (K 5)
 
+val max_duplicated_instances =
+  Attrib.setup_config_int \<^binding>\<open>monomorph_max_duplicated_instances\<close> (K 16000)
+
 fun limit_rounds ctxt f =
   let
     val max = Config.get ctxt max_rounds
@@ -173,28 +177,32 @@
       | add _ = I
   in Term.fold_aterms add (Thm.prop_of thm) end
 
-fun add_insts max_instances max_thm_insts ctxt round used_grounds
+fun add_insts max_instances max_duplicated_instances max_thm_insts ctxt round used_grounds
     new_grounds id thm tvars schematics cx =
   let
     exception ENOUGH of
-      typ list Symtab.table * (int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table)
+      typ list Symtab.table * (int * int * ((int * (sort * typ) Vartab.table) * thm) list Inttab.table)
 
     val thy = Proof_Context.theory_of ctxt
 
-    fun add subst (cx as (next_grounds, (n, insts))) =
-      if n >= max_instances then
+    fun add subst (cx as (next_grounds, (hits, misses, insts))) =
+      if hits >= max_instances orelse misses >= max_duplicated_instances then
         raise ENOUGH cx
       else
         let
           val thm' = instantiate ctxt subst thm
           val rthm = ((round, subst), thm')
-          val rthms = Inttab.lookup_list insts id;
+          val rthms = Inttab.lookup_list insts id
           val n_insts' =
             if member (eq_snd Thm.eq_thm) rthms rthm then
-              (n, insts)
+              (hits, misses + 1, insts)
             else
-              (if length rthms >= max_thm_insts then n else n + 1,
-               Inttab.cons_list (id, rthm) insts)
+              let
+                val (hits', misses') =
+                  if length rthms >= max_thm_insts then (hits, misses + 1) else (hits + 1, misses)
+              in
+                (hits', misses', Inttab.cons_list (id, rthm) insts)
+              end
           val next_grounds' =
             add_new_grounds used_grounds new_grounds thm' next_grounds
         in (next_grounds', n_insts') end
@@ -241,17 +249,20 @@
 fun is_new round initial_round = (round = initial_round)
 fun is_active round initial_round = (round > initial_round)
 
-fun find_instances max_instances max_thm_insts max_new_grounds thm_infos ctxt round
-    (known_grounds, new_grounds0, insts) =
+fun find_instances max_instances max_duplicated_instances max_thm_insts max_new_grounds thm_infos
+    ctxt round (known_grounds, new_grounds0, insts) =
   let
     val new_grounds =
       Symtab.map (fn _ => fn grounds =>
         if length grounds <= max_new_grounds then grounds
         else take max_new_grounds (sort Term_Ord.typ_ord grounds)) new_grounds0
 
-    val add_new = add_insts max_instances max_thm_insts ctxt round
-    fun consider_all pred f (cx as (_, (n, _))) =
-      if n >= max_instances then cx else fold_schematics pred f thm_infos cx
+    val add_new = add_insts max_instances max_duplicated_instances max_thm_insts ctxt round
+    fun consider_all pred f (cx as (_, (hits, misses, _))) =
+      if hits >= max_instances orelse misses >= max_duplicated_instances then
+        cx
+      else
+        fold_schematics pred f thm_infos cx
 
     val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
     val empty_grounds = clear_grounds known_grounds'
@@ -274,11 +285,12 @@
     val empty_grounds = clear_grounds known_grounds
     val max_instances = Config.get ctxt max_new_instances
       |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos
+    val max_duplicated_instances = Config.get ctxt max_duplicated_instances
+    val (_, _, (_, _, insts)) =
+      limit_rounds ctxt (find_instances max_instances max_duplicated_instances max_thm_insts
+      max_new_grounds thm_infos) (empty_grounds, known_grounds, (0, 0, Inttab.empty))
   in
-    (empty_grounds, known_grounds, (0, Inttab.empty))
-    |> limit_rounds ctxt (find_instances max_instances max_thm_insts
-      max_new_grounds thm_infos)
-    |> (fn (_, _, (_, insts)) => insts)
+    insts
   end