#
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)).
|