Dear HOL4 Developers,
In a recent thread on this list, Makarius mentioned experiments to load
HOL4 in the Isabelle Prover IDE. I participate in such experiments to
load HOL4 with Isabelle/HOL as kernel.
Anyhow, some of the main obstructions concern references (type 'a ref in
SML).
1) In a couple of places, the HOL4 code uses ref matching (i.e., ref is
used as a pseudo constructor that dereferences the cell).
Would you mind converting those to explicit dereference operations? E.g.
according to (or pulling) changeset [1]?
Such a change would make it easier to abstract over the concrete
implementation of reference cells.
2) It seems like type 'a ref is used with (at least) two different
intended meanings: one, to track global state variables and two, for
private program variables.
It seems like Isabelle/ML's module for thread-local data (that you
recently incorporated [2]) could be used for the first (global) meaning,
and 'a ref could be retained for private variables.
Would you support distinguishing those different usages in one way or
another?
Best regards,
Fabian
[1] https://github.com/immler/HOL/commit/b3ae0ef
[2]
https://github.com/HOL-Theorem-Prover/HOL/blob/1e8573d/src/portableML/poly/fromIsabelle/thread_data.ML
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
