Experimental check (1000) for identifier size growth during roundup draft default tip
authorballarin
Mon, 15 Aug 2022 23:20:43 +0200
changeset 76386 e7671364745e
parent 76322 3581dcee70db
Experimental check (1000) for identifier size growth during roundup
src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Aug 15 23:20:43 2022 +0200
@@ -295,29 +295,16 @@
 
 local
 
-val roundup_bound = 120;
-
-fun add thy depth stem export (name, morph) (deps, marked) =
-  if depth > roundup_bound
-  then error "Roundup bound exceeded (sublocale relation probably not terminating)."
-  else
-    let
-      val instance = instance_of thy name (morph $> stem $> export);
-    in
-      if redundant_ident thy marked (name, instance) then (deps, marked)
-      else
-        let
-          (*no inheritance of mixins, regardless of requests by clients*)
-          val dependencies =
-            dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} =>
-              (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep))));
-          val marked' = insert_idents (name, instance) marked;
-          val (deps', marked'') =
-            fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies
-              ([], marked');
-        in ((name, morph $> stem) :: deps' @ deps, marked'') end
-    end;
-
+val roundup_depth_bound = 120;
+val roundup_size_growth_bound = 1000;
+(*
+400
+*** Roundup size growth bound exceeded at depth 7 (sublocale relation probably not terminating)
+*** At command "interpretation" (line 939 of "$AFP/Category3/ZFC_SetCat.thy")
+200
+*** Roundup size growth bound exceeded at depth 6 (sublocale relation probably not terminating)
+*** At command "locale" (line 2964 of "$AFP/Category3/Limit.thy")
+*)
 in
 
 (* Note that while identifiers always have the external (exported) view, activate_dep
@@ -325,10 +312,37 @@
 
 fun roundup thy activate_dep export (name, morph) (marked, input) =
   let
+    val roundup_size_bound = roundup_size_growth_bound *
+      (Integer.sum (map Term.size_of_term (instance_of thy name (morph $> export))) + 1)
+
+    fun add depth stem export (name, morph) (deps, marked) =
+      if depth > roundup_depth_bound
+      then error "Roundup depth bound exceeded (sublocale relation probably not terminating)"
+      else
+        let
+          val instance = instance_of thy name (morph $> stem $> export);
+        in
+          if redundant_ident thy marked (name, instance) then (deps, marked)
+          else if Integer.sum (map Term.size_of_term instance) > roundup_size_bound
+          then error ("Roundup size growth bound exceeded at depth " ^ string_of_int depth  ^
+            " (sublocale relation probably not terminating)")
+          else
+            let
+              (*no inheritance of mixins, regardless of requests by clients*)
+              val dependencies =
+                dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} =>
+                  (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep))));
+              val marked' = insert_idents (name, instance) marked;
+              val (deps', marked'') =
+                fold_rev (add (depth + 1) (morph $> stem) export) dependencies
+                  ([], marked');
+            in ((name, morph $> stem) :: deps' @ deps, marked'') end
+        end;
+
     (* Find all dependencies including new ones (which are dependencies enriching
       existing registrations). *)
     val (dependencies, marked') =
-      add thy 0 Morphism.identity export (name, morph) ([], empty_idents);
+      add 0 Morphism.identity export (name, morph) ([], empty_idents);
     (* Filter out fragments from marked; these won't be activated. *)
     val dependencies' = filter_out (fn (name, morph) =>
       redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies;