#
e13bfb29 |
|
26-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move lambda type, dest_term function to kernel; add identical fn dest_term is quite heavily used (it implements SML's best approximation of a "view" for pattern-matching against terms), and its implementation outside the kernel is needlessly inefficient. Also extend signature with identical function, which correctly says whether or not two terms are identical, including in their choice of bound names. In the standard kernel, the possible presence of explicit substitution terms means that this notion is not the same as simple equality on terms.
|
#
dcc6ed15 |
|
27-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put equality constant into signature for Term
|
#
e72ba6f7 |
|
14-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put a fast/approximate equality check into Term API This points at the pointer-equality function for the moment, but should eventually be swung to point at something that works reliably and doesn't cause strange unreproducible crashes.
|
#
649f70e4 |
|
25-Apr-2013 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extend kernel API with new all_atoms entrypoint. Use this in theory pretty-printing routine to deal with issue #115. Closes #115.
|
#
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.)
|
#
c90ce71a |
|
02-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Handle the discrepancy in the behaviour between the way CHOOSE_THEN and GEN_TAC choose variants by making them do the same thing (Konrad earlier fixed GEN_TAC to use prim_variant, but CHOOSE_THEN was using variant). Decided that avoiding constant names in the current grammar was probably a good idea, so open up the internal gen_variant function in Term.sml, and feed it with the new predicate "is_constname" from Parse. is_constname is true if a string is the name of a "constant" as the parser sees things. In particular, if you do overload_on ("foo", ``SUC``) then "foo" (as well as "SUC") will be considered a const's name. Hidden constants are not const names in this sense, so C doesn't get primed in either of STRIP_TAC ([], ``(?C. P C) ==> Q``) or STRIP_TAC ([], ``!C. P C ==> Q``) even with combinTheory as an ancestor.
|
#
ffb6bc8a |
|
20-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Size functions for terms and types that count the size of the respective trees. Have written these so many times that it seems useful to have them in the kernel and available for all. (The term_size function doesn't include the sizes of the attached types; haven't ever felt the need for this.)
|
#
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.
|