Email Gateway (Sep 22 2021 at 10:32): Email Gateway (Sep 22 2021 at 10:32):From: Makarius <makarius@sketis.net>
* 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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Jul 15 2022 at 23:21 UTC