#
32bf1e49 |
|
02-Feb-2015 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
extra semicolons removed from (some) .sig files
|
#
08d7a558 |
|
23-Oct-2014 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
trailing newlines in *.{sml,sig} files from src/ removed Trailing newlines from SML files in src/ were rendered in HTML documentation.
|
#
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.)
|
#
20851e7a |
|
20-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Forgot to include the new functions in the 0-kernel signature files. Also, fix for the Makefile to make it see a dependency.
|
#
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.
|
#
0da1be26 |
|
01-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New Kananaskis kernel.
|
#
e3f389de |
|
16-Aug-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Deletion of "dummy" type. No longer needed because of MN's new type inference implementation.
|
#
d470aaf0 |
|
13-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Removed references (Link and Stv constructors) as type unification is now done at the level of the TCPretype in the parse directory. This simplifies the implementation considerably.
|
#
0058df84 |
|
28-Jun-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed to bring it up to date with Taupo release 0. (Changes have come across from parse_branch development.)
|
#
58841e67 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|