#
1ce5ae5a |
|
27-Sep-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Handle add_numeral_form et al with user-deltas Also take the opportunity to remove redundant add_actual_overloading entrypoint in Overload module.
|
#
51b08c16 |
|
05-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make PP.avoid_unicode also work for bare constant names. Previously, unicode infixes, suffixes were avoided, but if one did an outright overload_on("unicode-ish thing", ``constant``) then PP.avoid_unicode wouldn't help.
|
#
d2d3cc44 |
|
02-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Pretty-printer now annotates consts with their real names and types. In "complicated" overload situations, such as the overloads for NOTIN and <>, the annotation can't point to a "real" underlying constant, but does still provide the type for the emacs tool-tips. In passing, also create a new annotation form, the SymConst as well as the Const. This is done for the TeX backend's benefit, so that it can avoid treating things like + the same as normal identifiers. This works well for math-mode munging where you want "+" to map to $+$, but want "INSERT" to map to \textsf{INSERT}. Closes #39
|
#
7e68b4d9 |
|
21-Nov-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Use sets instead of lists to keep Overload print_maps small. Thanks to Scott to raising this issue. The use of a functor is so that I can use the same code for Anthony's use of LVTermNet, but have the underlying type be a list (this for the sake of backwards compatibility).
|
#
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.
|
#
6ebf8205 |
|
08-Sep-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
Add support for "inferior" overloads Use Parse.inferior_overload_on(s,t) instead of Parse.overload_on(s,t) to add the new resolution t of the token s at the lowest, instead of highest, priority. This allows the new resolution to be picked up when the types require it, but, when the types aren't constraining enough, the new resolution won't trump any existing resolutions. Printing is also affected: terms matching t will be printed as before, rather than using the overloaded string s. Caveat: if t is a more specific pattern than any existing overload, it will be printed in terms of s, since the printer won't realize that less specific overloads are competing with t. Also includes temp_inferior_overload_on, analogous to temp_overload_on.
|
#
fc103c62 |
|
05-Jul-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modify overload's internal timestamps to be successive integers rather than Time values. This prevents two very quick overload events from getting the same time-stamp, which I just observed happening (on Windows at least).
|
#
72be6cc9 |
|
25-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Adjust the way multiple matching abbreviations are discriminated amongst. In particular, it used to be that if an abbreviation required a smaller type instantiation, it would be preferred. Now, something that requires a smaller *term* instantiation gets the nod. Type instantiation size is the second factor considered, and then recentness. Also add raw_print_map entry-point to Overload module to add debugging.
|
#
d9003833 |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fairly dramatic change, supporting the use of "syntactic patterns". It is now possible to overload a name to term (typically a lambda-abstraction) in order to create syntax-only definitions. For example, there is a definition of not-equals now in the system: val _ = overload_on ("<>", ``\x y. ~(x = y)``) val _ = set_fixity "<>" (Infix(NONASSOC, 450)) This definition is parsed and pretty-printed. Two other annoying changes. The interface for adding unicode variants has changed, and I have made precedence level 450 of the parser non-associative. This latter change has caused most of the (minor) adjustments to the files below. The regression test doesn't go through yet. (Currently there is a failure in quotient/examples/sigma that I don't understand.)
|
#
d145b022 |
|
20-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More code for pretty-printing patterns. The interface in Parse stays the same, but you can now overload to type specific instances of constants. This is exploited in the ParseExtras structure, which is loaded with boolLib. This implements the <=> "constant" for if-and-only-if. This is just equality, but presented with a new face when applied to boolean arguments. The other obvious application of this is to make :string and alias for :char list, and to make the appropriate string constants overloads of the corresponding list constants. Code that relies on things like ``STRCAT`` mapping to {Thy = "string", Name = "STRCAT", Ty = ...} would fail. Otherwise, life should remain the same.
|
#
3b2b7c12 |
|
11-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modifications to support overloading to a pattern. For example, one can now do overload_on ("<>", ``\x y. ~(x = y)``) The parser does the right thing. The pretty-printer remains blissfully ignorant for the moment. I don't think Unicode aliasing will work quite yet either. Backwards compatible in that all the functions in Parse behave the same if given inputs that were previously acceptable. "The parser does the right thing" means the following - set_fixity "<>" (Infix(NONASSOC, 100)); > val it = () : unit - ``$<>``; <<HOL message: inventing new type variable names: 'a>> > val it = ``\x y. ~(x = y)`` : term - ``$<> p``; <<HOL message: inventing new type variable names: 'a>> > val it = ``\y. ~(p = y)`` : term - ``p <> q``; <<HOL message: inventing new type variable names: 'a>> > val it = ``~(p = q)`` : term When the pretty-printer is working correctly, the output will probably be ``\x y. x <> y`` ``\y. p <> y`` ``p <> q`` In the first two cases, fixing what would appear to the user to be an odd eta-expansion may be too difficult.
|
#
46f3d98f |
|
19-Jun-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added: Parse.send_to_back_overload : string -> {Name: string, Thy: string} -> unit Parse.bring_to_front_overload : string -> {Name: string, Thy: string} -> unit Parse.temp_send_to_back_overload : string -> {Name:string,Thy:string} -> unit Parse.temp_bring_to_front_overload : string -> {Name:string,Thy:string} -> unit These provide a more flexible way to control operator overloading. For example: - load "wordsTheory"; > val it = () : unit - ``a + b``; <<HOL message: more than one resolution of overloading was possible>> <<HOL message: inventing new type variable names: 'a>> > val it = ``(a :bool['a]) + (b :bool['a])`` - Parse.send_to_back_overload "+" {Name = "word_add", Thy = "words"}; > val it = () : unit - ``a + b``; <<HOL message: more than one resolution of overloading was possible>> > val it = ``(a :num) + (b :num)`` : term - ``a + b : word32``; > val it = ``(a :bool[32]) + (b :bool[32])`` : term
|
#
28a9f383 |
|
15-Jan-2004 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for bug #851064, which was caused by the parser's overload tables retaining information about constants that had been outdated by a call to new_theory.
|
#
607d3f54 |
|
19-Apr-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Cleaned up treatment of overloading and extended pretty-printer to show types verbosely, when appropriate.
|
#
3009bd41 |
|
23-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Overload.sml now uses a Binarymap internally to store the map from names to sets of constants. A slight change to Overload.sig affected only term_grammar's internals, and only the grammar pretty-printer at that.
|
#
f3c83832 |
|
16-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Final changes (I hope) for Kananaskis-1 parser. Implement remove_ovl_mapping for fine-tuning of overload maps.
|
#
6d0b0ee4 |
|
14-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More changes to Kananaskis parsing. System now doesn't allow for possibility of overloading to different type instantiations of polymorphic constants. Nor does it allow for printing of polymorphic constants in any more than one way. Treatment of number injection overloading is slightly simplified by actually having a constant in arithmeticTheory with the magical property that it can never be parsed as the LHS of an application.
|
#
0aaa9d6f |
|
13-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Made overload_info type opaque, and added a reverse map to it, under the hood, which remembers how constants should be printed. Also reworked Preterm slightly to stop it carking on type-checking errors involving overloaded constants (things like `0:bool`, if nothing else).
|
#
bf7d5c49 |
|
07-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Treatment of known constants and overloading was bogus. Now known constants are just the domain of the map in the overloading info. reveal now puts all constants of the given name into the overloading map. Will have to add a precise function for removing pairs from this.
|
#
5deefb75 |
|
03-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes to the way in which constant names are resolved. There is now a much simpler map from names in the abstract syntax tree to actual constant terms; everything now goes through the "overload" map.
|
#
a2511ab7 |
|
02-Nov-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes to bring about Kananaskis parser. Known bug exists in treatment of qualified identifiers.
|
#
9f67e582 |
|
10-Jul-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
The function allow_for_overloading_on has been completely removed from the system. The overload code now uses anti-unification of types to figure out the least generalisation of all the types that an overloaded operator needs to represent.
|
#
c03bd7b1 |
|
15-Oct-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implemented new operation of grammar merging. This will be used to deal with the dodgy implementation of internal grammar value calculation done in theories.
|
#
37b08cd9 |
|
24-Sep-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Greatly improved the efficiency of the treatment of the overloading when type-checking is done. This results in what appears to be a threefold speed-up. However, parsing as a whole is still too slow and this is because of the lexer being so inefficient.
|
#
259c8172 |
|
23-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Many changes to allow numerals to be overloaded as well as operators.
|
#
538a0f08 |
|
20-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes to get overloading to properly resolve types. I claimed yesterday that if an overloaded constant didn't have its type determined by normal type-checking, then it could be instantiated with any type in the candidate list of types because if type-checking hadn't constrained it, then it must be OK. This is rubbish though, because there may be constraints implicit in other overloaded operators. For example, imagine that ~ is overloaded to be both a boolean operator (not) and over integers (negation). Further, imagine that + is overloaded. Then consider the phrase ~x + 2 If we just guess the first type that comes to hand for x, then we may guess bool, and this will be wrong, because the + has to go to num->num->num or int->int->int. So, we need to do backtracking unifications through all of the possibilities. Hence the use of seqs and seqmonad to implement this.
|
#
3bed8d45 |
|
19-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Big raft of changes allowing a simple form of overloading to be supported.
|