#
a587378e |
|
10-Jan-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make experimental kernel's term representation visible to Thm Thm can then exploit the fact that both the experimental and standard kernels have a datatype as the term representation. There's not much that can be exploited there, but it does make it clear that both are equality types. (To make it clearer, Thm should arguably be a functor...)
|
#
aa9f83cb |
|
09-Jan-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Standard and experimental kernels now share Thm.sml implementation It should now be possible to have the logging kernel work over either implementation of terms, and to delete its copy of Type, Term etc.
|
#
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.
|
#
fb840c11 |
|
13-Dec-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Thanks to an enlightened Internet cafe in Perth running DHCP, I can finally check this in. It's a name-carrying implementation of the kernel, and should be a drop-in replacement for the existing code. To make the replacement change src/0 in tools/build.sml to be src/experimental-kernel. Sadly, the code is not as fast as I'd like just yet. In particular, the benchmark example is 20% slower. I don't know quite why this should be, but I'm looking into it. The performance of the checked-in code will be even worse than it should be at the moment because I've used Profile-ing throughout. (The most called (potentially expensive) function in the kernel? Term.compare it seems.) This profiling seems to cause a strange Time exception on big builds, which has stopped me testing the new code on the netsem examples (which are 90% of the motivation for the change---argh). Anyway, if anyone feels the urge to fix obvious bugs, please feel free. Though access to the 'net for my Linux partition is a tad on the tedious side, I can read my e-mail at home, and this means that I can see messages to hol-checkins without any difficulties.
|