#
f6b4ebd0 |
|
25-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove unused code in Parse_support
|
#
37c730f2 |
|
20-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make progress with functional pretype The change to pretty-printing raises an exception, but parsing simple cases seems to work.
|
#
6af175af |
|
20-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Begin to make pretypes purely functional I want to do without the references that are used in the unification algorithm.
|
#
c9ff14bd |
|
21-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Slightly more open-ness in core src/parse APIs
|
#
43cfb1f2 |
|
21-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Allow for user "preterm processors" These are inserted into the process where the abstract syntax gets turned into preterms, and can call back to the builtin processor if necessary. Something like this is necessary if you are going to mess with binding structure and need to do so in a way that is itself aware of what the context's free variables are. This technology is needed for pattern-matching, and should allow us to move the handling of set-comprehension out of src/parse as well.
|
#
68a92502 |
|
21-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make Parse_support API more open See earlier (reverted) 9fc2c8a
|
#
66031f8d |
|
20-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Undo all pmatch changes to src/parse I now want to make new-style pmatch parsing happen via the mechanism of absyn post-processors (as is done with monad syntax). I don't think that changing the "core" parser is necessary (and it's certainly not desirable).
|
#
9fc2c8a9 |
|
18-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Open up some of the internal parsing APIs
|
#
fb3bc705 |
|
17-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Code for new style pattern-match parsing Syntax as described in github issue #286 parses. Examples: > ``case x of 0 => 3 | SUC n when n < 10 => n + 1``; val it = ``PMATCH x [PMATCH_ROW (λ_. 0) (K T) (λ_. 3); PMATCH_ROW (λn. SUC n) (λn. n < 10) (λn. n + 1)]``: term > Datatype `tree = Lf | Nd tree 'a tree`; <<HOL message: Defined type: "tree">> val it = (): unit > ``case t of Lf => 0 | Nd t1 x t2 => x + f t1``; val it = ``PMATCH t [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0); PMATCH_ROW (λ(t1,x,t2). Nd t1 x t2) (K T) (λ(t1,x,t2). x + f t1)]``: term > ``x + case t of Lf => 0 | x .| Nd t1 x t2 => f t1``; <<HOL message: inventing new type variable names: 'a>> val it = ``x + PMATCH t [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0); PMATCH_ROW (λx. Nd t1 x t2) (K T) (λx. f t1)]``: term > ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 => f t1``; val it = ``x + PMATCH t [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0); PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (K T) (λ(t1,t2). f t1)]``: term > ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 when g t2 > 6 => f t1``; val it = ``x + PMATCH t [PMATCH_ROW (λ_. Lf) (K T) (λ_. 0); PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (λ(t1,t2). g t2 > 6) (λ(t1,t2). f t1)]``: term I think we do still need a separate notation to indicate no variables are to be bound, as | .| pat => rhs won't work when .| is an infix. Maybe | ..| pat => rhs This would be needed in a situation where all of the variables in pat have to be read as free (referring to variables occurring in a wider context).
|
#
49cd6127 |
|
17-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rename Parse_support.make_case_arrow New name is old_make_case_arrow, with intention that this is only called with pmatch_on is false.
|
#
c3cde98f |
|
16-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Polish preterm API to remove unused parameter. make_qconst didn't read/use its overload_info parameter, so there seems no point having that parameter in the API.
|
#
16ba3dd2 |
|
18-Jan-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Variables in the patterns of case expressions are now properly 'fresh'. They bind expressions on the other side of the case-arrow, but do not affect variables outside the case expression or in other branches. This revealed a bug in DecodeScript, where a theorem about encoding sums ended up being about sums of type 'a + 'a only because case pattern variables that should have been independent weren't.
|
#
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.
|
#
adf911c8 |
|
25-Jul-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Revised exportML so that it takes a path parameter, which tells where the ML corresponding to a theory is to be written. This has been propagated to all the theories that already export ML, and the mkword.exe tool has been upgraded to also take a path where it should write the generated ML. This is useful, because doing an exportML to the same directory as the theory files will end up confusing Holmake.
|
#
164e7a23 |
|
25-Sep-2002 |
Keith Wansbrough <keith@lochan.org> |
Add a Locn field to each constructor of Preterm.preterm, in preparation for located type error messages etc. * Thanks to Joe Hurd for helping locate a bug in an earlier version: Preterm, while still an equality type, is no longer safe to compare for equality. Instead, Preterm.eq must be used; this ignores the locations. (The symptom was a parse_in_context failing to notice that the binder variables were the same as the bound occurrences, leading to weird failure in Q.PAT_ASSUM). * Constrained and Antiq now take records, to accommodate the Locn field. * Lots of small changes, mainly adding ",...", to code using preterms. * Pass locations down into the preterm constructor functions.
|
#
52b44cd4 |
|
24-Sep-2002 |
Keith Wansbrough <keith@lochan.org> |
Further improve error reporting: * make_atom failures (e.g., update of nonexistent field) now give located errors; ditto all friends in Parse_support. Modified absyn_to_preterm and Parse_suport.* to pass locations downward to accommodate this. * Fix a bug in parse_term that was causing ranges to be confused for certain sequences of tokens (was reporting left edge of last token to right edge of first token, oops!). * Add text " (possibly missing semicolon)" to error "May not use record update functions at top level", as this is a common error. * Fix a small bug in location-handling in type_tokens. Other changes: * Remove another printing of the tail of the input (no longer necessary). * Various code tidy-ups. * Reduce Loc_Near (Loc_Near locn) to Loc_Near locn (otherwise they pile up dramatically!).
|
#
6da5e079 |
|
10-Feb-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Minor change.....
|
#
67cbea0e |
|
10-Feb-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Support for new representation of strings.Minor changes.
|
#
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.
|
#
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.
|
#
ef50e06b |
|
03-May-2000 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implementation of move of hide/show information from Parse_support list into grammars.
|
#
3bed8d45 |
|
19-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Big raft of changes allowing a simple form of overloading to be supported.
|
#
076b63b7 |
|
13-Aug-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implementation of type checking is now entirely above the level of the kernel. New TCPretype module (type-checking pretype) implements much of the required functionality, including type unification. Parse_type generalised to target any type providing the appropriate constructor functions.
|
#
accadd48 |
|
12-Jul-1999 |
Konrad Slind <konrad.slind@gmail.com> |
Change to antiquote processing. Now free variables in the antiquotation will affect type inference in the surrounding term. This is the way it was done in HOL88, but not HOL90. Also, some now outdated code has been removed.
|
#
0058df84 |
|
28-Jun-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixed to bring it up to date with Taupo release 0. (Changes have come across from parse_branch development.)
|
#
caf74236 |
|
29-Apr-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial revision
|