There is a funny comment here:
http://isabelle.in.tum.de/repos/isabelle/file/cdba0c3cb4c2/src/HOL/Spec_Check/base_generator.ML#l94
(* Isabelle does not use vectors? *)
Isn't live nice without vectors, arrays, a host of "int" types that are
not int at all?
The one exception is src/Pure/Syntax/parser.ML, where arrays are used
internally due to some historic "optimization". It probably wastes a lot
of space, since every grammar update needs a fresh copy of the whole
thing.
Working routinely on the JVM now (due to Scala), I've found so many
inefficiencies in the libraries due to the historic predominance of these
mutable bulk data structures (aka arrays). This is particularly bad when
working with plain text, aka strings.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
