#
5f99e73a |
|
15-Dec-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
BIG refactor: mainly to allow stdknl to use SharingTables technology. SharingTables implements hash-consing for types as they are written out to disk. This can make a big difference to the theory file size, and thus to theory-loading times. The big visible change is that Theory, TheoryPP and Definition are no longer really part of the kernel, and are found in src/postkernel instead. They don't need to know about secret implementation details in terms, types or theorems. They do need to have access to Term.{write,read}_raw and primitive definition principles (which are in Thm). Another API change is that Tags no longer use user-visible string refs to record use of axioms. Instead, the refs are hidden behind a new Nonce type. This in turn means that the Tag.axioms_of function can move to be visible to all users after the kernel. (If we kept the axioms as string refs, users could alter the strings being pointed to.)
|
#
1cba282f |
|
17-Apr-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rework a bunch of code in the two kernels so that they can share even more stuff in src/prekernel. In particular, the latter is now home to a special purpose symbol table that knows all about things being up-to-date. Also move the final signatures for Terms and Types that are what is ultimately presented to the user into prekernel so that both kernels can use them. In src/0 also move the signatures in Raw-sig into Type.sig and Term.sig so that {Type,Term}.sml can be compiled in normal mode against those signatures. I think this makes things a deal cleaner there. Finally, witnesses have entirely disappeared from src/0. If we wanted to reinstate them for whatever reason, they could be stored in a KernelSig.symbol_table along with arities and base types.
|