#
fdc8d449 |
|
15-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Complete refactoring of Sharing code There's now an API for exporting theorems, terms and types to s-expressions that should be generally useful (not just in the theory data management setting).
|
#
430af99f |
|
15-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Start to refactor Sharing code
|
#
ddd8263e |
|
14-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Delete some unused code
|
#
50b30f65 |
|
14-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Change theory files to use an s-expression representation This wastes some disk-space in the form of extra white-space that the Oppen pretty-printer introduces for indentation purposes, but with the string table used, the number of lines and the number of non-whitespace characters is lower. The string table can and will be used in more places in subsequent commits to try to improve file size and sharing. The theory data may also shift to directly use s-expressions rather than strings (people wedded to a string representation can always embed those into s-expressions of course).
|
#
ddcc13f7 |
|
12-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Optimise theory dat space a bit - use a slightly more compact term representation that saves a bit of space when binary or unary applications happen - build a table of strings to reuse at the top of theory files The strings table still needs to be used in a bunch more places throughout Theory.dat files.
|
#
b72e391c |
|
20-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move smpp to Portable - get everything up to arithmeticScript working
|
#
3f252166 |
|
13-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Work towards use of PolyML.pretty type for most pretty-printing Compiles up to src/parse under Poly/ML
|
#
0775443a |
|
21-Aug-2017 |
Thibault Gauthier <thibault.gauthier@uibk.ac.at> |
Use _Theory.dat for loading theory data into _Theory.sml
|
#
32bf1e49 |
|
02-Feb-2015 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
extra semicolons removed from (some) .sig files
|
#
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.)
|