#
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...)
|
#
2ef6f228 |
|
13-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start removing uses of pointer_eq It's flakey and seems to cause strange, hard-to-reproduce runtime failures.
|
#
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.
|
#
261e2abf |
|
21-Jan-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make mk_thy_type's error message slightly less unhelpful.
|
#
38036bab |
|
18-Aug-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide a trace variable enabling users to turn off the complaints the kernel is wont to make about type-variables with unusual names.
|
#
3c805984 |
|
17-May-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More fixity finangling.
|
#
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.
|
#
cb88a3c7 |
|
04-Jul-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update so that this works with the new ML execution code.
|
#
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.
|