History log of /seL4-l4v-master/HOL4/src/portableML/ImplicitGraph.sig
Revision Date Author Comments
# 0801c6f2 12-Oct-2020 Michael Norrish <michael.norrish@data61.csiro.au>

Simplify grammar handling by using abstract ancestral data framework

This is not fully worked out yet, and the abstract framework has only
been instantiated on the one test-case. It's definitely worth it
there though as there can be less awful code smashed into
fooTheory.sml files as a result. Aim is to instantiate theorem-sets
in the same way though so that it will be possible to access srw_ss()
as it was at different points in the theory hierarchy.

Not yet clear if AncestryData should be responsible for holding onto
the underlying references that hold the global "values" (grammars,
simpsets, etc).

Changes in examples fix various adjoin calls that either shouldn't be
there at all (TypeBase now has export; or need to be made "after
completion" so that parses work correctly (these should be using
exportable data themselves)).