#
1e0d2028 |
|
11-Apr-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Re-implement Datatype package with TypeBase sexps (not adjoin)
|
#
6a881dff |
|
30-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix ParseDatatype to handle recursive redefinitions
|
#
b4161465 |
|
30-Mar-2014 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement most of a new Datatype function with nicer syntax. (Pair-programming with Magnus who wanted it.) Still need to implement change to EmitTeX.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
2cc44ee2 |
|
26-Oct-2010 |
Konrad Slind <konrad.slind@gmail.com> |
Cleaned up signature Datatype.sig. Added entrypoint to call Hol_datatype on ParseDatatype.AST list input.
|
#
1ea184ec |
|
03-Dec-2008 |
Konrad Slind <konrad.slind@gmail.com> |
End of the *v saga. I found the spot in Pmatch.sml that was failing to collect all the free vars that needed to be renamed away from. Misc. other tidying, including an incomplete attempt at getting datatype constructors to be defined in terms of numerals rather than successors.
|
#
d8d60b60 |
|
28-Aug-2006 |
Konrad Slind <konrad.slind@gmail.com> |
Liberate an AST interface to datatype declarations.
|
#
efd1294a |
|
30-Oct-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A slight extension to the way big records are handled, designed to give users more control, and to also make the default behaviour more reluctant to use big records (they can induce serious confusion if you're not expecting them).
|
#
4cd281d5 |
|
03-Sep-2002 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modify TypeBases so that they can store conversions as well as theorems in a tyinfo's "simpls_of" slot. This is then used to implement a conversion for enumerated type equalities. Previously, we just used a rewrite directly, which meant that something of the form (x = C10) might turn into the rather ugly (foo_to_num x = 11). Now, the rewrite is only applied to equalities between constants. Some comments in the .sig files in Datatype, RecordType and EnumType hopefully also make it clearer what the weird string results are doing, and how they get added into theory files.
|
#
c3393882 |
|
03-Jul-2002 |
Joe Hurd <joe@gilith.com> |
Moved the code to automatically generate "boolify" functions for datatypes from src/datatype/Datatype.sml to src/Boolify/src/Boolify.sml. It uses the register_update_function hook to add the boolification info (more on that later). Also added a test suite for boolification.
|
#
829cbafd |
|
30-Jan-2002 |
Konrad Slind <konrad.slind@gmail.com> |
Minor inconsequential cosmetic changes made in the course of tracking down various bugs.
|
#
e3a8e6d4 |
|
14-Dec-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Numerous small changes.
|
#
3d2f9ce3 |
|
20-Jun-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Change stemming from split of TypeBase into TypeBasePure and TypeBase.
|
#
1a23a8fb |
|
18-Jun-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Idiotic hacking about to get aligned with EnumType.
|
#
cfdc1706 |
|
11-Apr-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modifications caused by change of TypeBase signature.
|
#
77efd725 |
|
04-Feb-2001 |
Konrad Slind <konrad.slind@gmail.com> |
New work aimed at making a single global EVAL function, with an underlying compset.
|
#
3d71668f |
|
12-Feb-2000 |
Konrad Slind <konrad.slind@gmail.com> |
Proper size definitions.
|
#
4a62b3fd |
|
11-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modified to put size definitions correctly into the various tyinfos that are generated, rather than defining the same set of constants once for every type.
|
#
de2ed6a8 |
|
10-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes due to the incorporation of John Harrison's datatype definition package. Here are the rest of the significant changes. The interface in Datatype has been fleshed out quite a bit, but what was there has stayed pretty much the same (except that prim_Hol_datatype doesn't write stuff out to disk anymore; it's hardly very pure if it does so). The ind_type theory is the basis for ind_types, which is in turn called from Datatype.
|
#
17721c0c |
|
03-Sep-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Moved function for defining case constants over standard datatypes to Prim_rec from Datatype.
|
#
ebdd2725 |
|
18-Aug-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Moved type_size and tysize to basicHol90/TypeBase. This lowers the support required to apply these functions.
|
#
58841e67 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|