#
6a81a039 |
|
21-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from src Will also make selftest to check that they aren't introduced
|
#
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.
|
#
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.
|
#
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.
|
#
8b3ffef1 |
|
03-Oct-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make Theory.sml files' raw term format more compact I noticed that these strings sometimes included quite long runs of @ characters (standing for applications). The new format run-length encodes these so that a single @ stands for one, and otherwise something like @10 stands for ten of them.
|
#
640c7e80 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make match error messages in kernels closer Some code is relying on the exact message that the kernel generates as part of its HOL_ERR...
|
#
914184ad |
|
04-Feb-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
Modify term-encoding in theory files to be more compact. Both kernels now use a reverse-polish encoding (with the two binary operators being application and abstraction). There is no whitespace or any parentheses in the new encoding. On "typical" core theories such as integerTheory and wordsTheory, this saves about 10% in total theory size. On larger theories (such as those in CakeML), I hope the saving will be even greater.
|
#
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.
|
#
0235335e |
|
20-Mar-2012 |
Peter Homeier <palantir@trustworthytools.com> |
Fix for an error in Term.free_vars_lr. This was prompted by a bug using Define discovered by Ramana Kumar. I traced it down to the kernel function Term.free_vars_lr, which in the experimental kernel gives the incorrect result - free_vars_lr ``(x:'a, \x:'a. 0)``; > val it = [] : term list whereas the standard kernel gives the correct result - free_vars_lr ``(x:'a, \x:'a. 0)``; > val it = [``x``] : term list
|
#
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.)
|
#
559a2b40 |
|
29-Jan-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Fixed function name in errors raised by raw_match_term.
|
#
2637ec1d |
|
23-Jan-2010 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Improved the implementation of vsubst to not collect free variables in abstraction bodies in which all redexes are bound, unless renaming occurs. Complexity reduced from linearithmic (I think) to constant for these cases. Previously, "vsubst [y/x] (\x. t)" would first collect all variables in t, before returning "\x. t" unchanged. Note that when renaming occurs, vsubst must still inspect the entire term (to rename away from all free variables).
|
#
a26c9e98 |
|
02-Dec-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Added a comment pointing out that subst can cause accidental variable capture. This can only occur when the term contains a bound variable that is a not-yet-generated genvar (which is unlikely to happen unless the user is malicious) and at least one redex is not a variable. The main issue is that freshness of genvars is assumed, but not guaranteed by the Term implementation. Fortunately, all calls to subst in Thm seem to use only variables as redexes, so there should be no soundness issue. Still, a correct implementation would seem desirable.
|
#
f026e55d |
|
02-Dec-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Tuned.
|
#
6c326c6c |
|
02-Dec-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Tuned.
|
#
2525541e |
|
17-Jun-2009 |
Peter Homeier <palantir@trustworthytools.com> |
This is a fix of a soundness bug in the experimental kernel of Kananaskis-5, as recently described on the Hol-developers list.
|
#
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.
|
#
e59c3207 |
|
16-Apr-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make a couple of operations in experimental-kernel/Term.sml more efficient.
|
#
8dfcc5d8 |
|
15-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Make Holmake see some dependencies
|
#
b067d478 |
|
01-Mar-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Attempt to return a little more information about failing matches (at least when the two terms are both constants).
|
#
e7f6ecf7 |
|
26-Apr-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for another instance of old constants coming to compare equal with new constants (caused by del_segment not oldifying constants that are being cleared out of the theory segment).
|
#
c450dfd3 |
|
25-Oct-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for soundness bug; Globals.old changes its behaviour, and is no longer a reference. It is used in the kernel to do semantically significant things so can't just be left to a user to change arbitrarily.
|
#
2827f4fa |
|
25-Oct-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update implementations of terms and types so that they behave like the dB kernel in their treatment of old, out-of-date constants. Also fix the Term implementation so that out-of-date constants undergo the name change to "old->name<-old" that happens in the dB kernel. Previously this did not happen with Terms. Now, both implementations store pointers in their internal symbol tables, rather than records of information that included an out-of-date pointer. This means that when a pointer is removed from the symbol table, what it's pointing at can be updated with a changed name.
|
#
7d4cd42d |
|
03-Jun-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Each unique string literal in a .sml file consumes a slot in some sort of global value table that Moscow ML uses. If you have lots of big theories, as we do in netsem, then this table can get exhausted with not very much interactive use (every binding made interactively, even all those "it"s consumes another slot I think), and it dies with a Chr exception. So, I realised that generating code that parsed strings to create terms was unnecessary. We can just create code that creates terms directly. This means I can kill some code in Term too. (Only in experimental-kernel for the moment.)
|
#
a03aca36 |
|
21-Jul-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A fix for the HOL Light INST_TYPE bug, that also affected the experimental kernel. Basically, you can't blindly do type instantiation across a theorem because it may cause what was a free variable to become captured. The dB implementation is immune to this of course. Test for the bug in the selftest program to extend the regression suite.
|
#
94e5dc43 |
|
01-Jul-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
free_vars_lr also needed fixing here.
|
#
2e4c7d83 |
|
06-Mar-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Efficiency tweak for substitution; don't bother with {redex,residue} pairs that are the same.
|
#
264811d3 |
|
25-Feb-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Model this code on Konrad's existing src/0 code and make it go 10 times faster. Asymptotically still linear, but factors of ten not to be sneezed at. I believe this was what was behind the slowness of the definition of case constants for enumerated types in the name-carrying case. (The calls to var_occurs are made during calls to GEN, and were being repeatedly made over bigger and bigger assumptions.)
|
#
75aa3bb9 |
|
20-Jan-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a bug in the calculation of free names. This was causing a bug in the implementation of substitution.
|
#
d4d3de78 |
|
22-Dec-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New implementation of subst, not exponential, which works by pre-computing free variables of all sub-terms when an abstraction is encountered. Also a reversion to theory files that don't share every possible term. Types are still shared though.
|
#
1b90a010 |
|
17-Dec-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Some efficiency improvements in this directory. Code now runs build about 20% faster. There remains a horrendous time blow-up in Hol_datatype, which I'm working on. I think it may be subst's potentially exponential behaviour.
|
#
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.
|