*** ML *** * ML structures TFrees, TVars, Frees, Vars, Names provide scalable operations to accumulate items from types and terms, using a fast syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set.
* Thm.instantiate, Thm.generalize and related operations require scalable datastructures from structure TVars, Vars, Names etc. INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate adoption; better use TVars.add, TVars.add_tfrees etc. for scalable accumulation of items. This refers to Isabelle/4974c3697fee. Many years ago, I made measurements that showed that the naive association lists were actually sufficient for most applications. Now I did change my mind and made it more scalable: the impact is hardly measurable, apart from https://isabelle.sketis.net/devel/build_status/macOS_11_Big_Sur_4_threads/index.html#session_HOL-Record_Benchmark where there is a clear reduction of runtime. That example also shows that more heap space is required: 2-3 trees require more overhead than plain list. Right now I am inclined to leave this new status-quo, unless someone comes with concrete applications that require further tuning (e.g. a different implementation behind the now abstract data types of Vars.table etc.) Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
