#
66465004 |
|
27-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up handling of type_grammar deltas and interaction with Thyops Need a slightly better interface for querying the kernel name signature information for types, and also alter term functions to not return constants that don't have up-to-date types. Now deleting a type doesn't result in broken theories. With a regression test. Closes #179
|
#
17990a1d |
|
08-Nov-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement "input only type abbreviations" Closes #599
|
#
a80bef55 |
|
13-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Updated as far as type_grammar.sml
|
#
af6c06dc |
|
03-Oct-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Convert type-grammars to use deltas for updates This is very much analogous to what has been done for term grammars.
|
#
d5c76759 |
|
30-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Polish type-grammar pretty-printing
|
#
a2c78998 |
|
29-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide a hide_tyop function on type_grammars The result of hide_tyop s is that the bare type-operator/abbrev name s will no longer map to anything; the standard parser will stop parsing when it sees such a name.
|
#
b9a590e8 |
|
29-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Unify handling of type abbrevs and type operators This is analogous to what is done with terms, where the handling of genuine constants passes through the overload map. The main desirable effect should be that if multiple genuine type operators with the same name are in the grammar, then only one will print unqualified; all the others will print with theory-qualification. Currently fails in src/datatype's selftest as ParseDatatype doesn't see bare names that are existing types as possible occurrences of recursive types.
|
#
e9e05308 |
|
28-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add preliminary, unused delta type for type grammars
|
#
d639b93f |
|
28-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move type_grammar datatype decls into new _dtype struct
|
#
8b046b8b |
|
20-Sep-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement theory namespaces for type abbreviations Closes #168
|
#
2831eaec |
|
20-Oct-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up type grammars to reflect reality of suffixes as tightest operators. Also, fix a minor pretty-printing bug that was affecting types like ('a + 'b) [32] and document this in src/n-bit/selftest.sml
|
#
b6ec410a |
|
09-Sep-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
Functions to list specific overloads/abbrevs, and to print without them Add the following functions to Parse: pp_overloads_on s print the parsing and printing overloads associated with the token s pp_abbrev s print the type abbreviations associated with the token s pp_term_without_overloads_on (ls : string list) print a term without applying any overloads on the tokens in ls pp_term_without_overloads (ls : (string * term) list) same as above, but specify the overloads to remove more precisely pp_type_without_abbrevs (ls : string list) print a type without using any abbreviations on tokens in ls Also add printing versions, with the prefix "pp_" replaced by "print_", which don't need a ppstream and print to stdout. For the last three functions, also add "print_backend_" versions. Also add string versions of the last three functions, with the prefix "pp_" removed and the suffix "_to_string" or "_to_backend_string" added, which don't need a ppstream and return a string. Apart from Parse.sig, also modify two other signatures: Reveal the function structure_to_type in type_grammar, and Add the function gen_remove_mapping to Overload, which removes an arbitrary overload to a term, since remove_mapping can only handle overloads to constants.
|
#
c2976fa7 |
|
25-Feb-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move theory min's grammars into {type,term}_grammar (out of Parse).
|
#
add6d16c |
|
01-Sep-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix a bug that allowed type abbreviations to be applied to more type arguments than expected. E.g., type_abbrev("foo", ``:bool``) followed by ``:'a foo`` used to work. No more!
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
7d307422 |
|
22-Aug-2007 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update to support ty1[ty2] syntax for array types. This means that a 32-bit word type now prints and parses as :bool[32]. I haven't quite managed to rebuild all of the system (because I'm about to go to bed), but I'm pretty confident the change won't break anything serious. Where it might break things is in input such as f:num list -> bool [3;4] The above used to work, but is pretty unlikely. It will now break because the type parser will grab the [ token that used to "belong" only to the term level.
|
#
ee4bf8b5 |
|
05-Oct-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
My change to type grammars (allowing for printing of abbreviations) silently invalidated an assumption in EmitML about taking grammars apart and putting them back together again. So, I add a new entry-point in type_grammars to allow deletion of type operators by their infix names. This then allows the EmitML behaviour to be recoded. Also extend the type_grammar pretty-printer so that it shows which abbreviations are not being printed.
|
#
e33b8b0a |
|
21-Sep-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Type abbreviations now print by default. Where this is "problematic", as with the set and bag abbreviations, this printing can be turned off by calling disable_tyabbrev_printing, which takes the abbreviation name as an argument. (There is also a trace variable controlling tyabbrev printing globally.) Bag and set abbreviations are "problematic" because if left on they do things like - type_of ``(/\)``; > val it = ``:bool -> bool set`` : hol_type and - type_of ``(+)``; > val it = ``:num -> num multiset`` : hol_type This code isn't done yet because it doesn't pick between multiple possibilities in an intelligent way. The heuristic I want to implement will take the most specific abbreviation first, and then the most recently asserted if two are equally specific.
|
#
512123cb |
|
22-Apr-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Adapting to new Basis (and SML/NJ).
|
#
2edb9e51 |
|
21-Jul-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
New function to allow abbreviation removal.
|
#
e8de8c14 |
|
26-Jun-2003 |
Konrad Slind <konrad.slind@gmail.com> |
Not sure what has been added here. Probably trivial.
|
#
e62fa301 |
|
23-Aug-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implementation of "parse only" type abbreviations. The main function to use is type_abbrev : (string * hol_type) -> unit If the hol_type has type variables in it, then these become parameters to the string, making it an abbreviation for a type operator. E.g., type_abbrev("set", ``:'a -> bool``) allows you to write ``:num set``. No attempt to pretty-print types in accordance with stored abbreviations, so the system will spit back ``:num -> bool`` in response to this. (Hey, if it's good enough for Moscow ML, it's good enough for us.) Also split off type_grammars into their own source module.
|