#
798ac6f3 |
|
10-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Complete implementation of new API for declaring+using monads Monadsyntax in general (the do..od notation) can be turned on and off. In addition, specific monad instances can be declared and subsequently enabled by just calling something like monadsyntax.enable_monad "option" Having state_transformerTheory as an ancestor turns on monadsyntax, and enables the state monad. (Enabling a monad causes a bunch of calls to overload to occur; disabling a monad undoes those calls.)
|
#
e8895bc2 |
|
08-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
WIP for change to list syntax handling. Very broken at the moment
|
#
525bfe3c |
|
20-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Allow multiple case-like constants in a grammar Parsing handled; printing still not quite right
|
#
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).
|
#
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).
|
#
ceffb740 |
|
17-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Special internal name for .| infix (pmatch syntax)
|
#
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
|
#
d3e399bb |
|
28-Jul-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Parse decimal fractions, turning them into divisions. Client theories need to overload the magic string GrammarSpecials.decimal_fraction_special to their division constant in order to get this to work.
|
#
fdd2d3c2 |
|
02-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add a new function whereby the pretty-printer can be told to treat certain "impossible-to-occur-naturally" variables as constants. This is a prerequisite for my scheme to print "syntactic macro" patterns (like not-equals, not-a-member, boolean-equality).
|
#
13f030c2 |
|
07-Feb-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Wide-ranging change to make the TypeBase export an interface forcing users to be concerned about which theory their types are from. Interactive users of the "induction_of", "axiom_of" and similar functions are thrown the only bone: they can effectively omit the theory parameter by using "" instead of a theory name. Prompted by a bug found by Tom Ridge where it was impossible to define a pattern matching function on a type with the same name as another type because the pattern-matching code was using dest_type and TypeBase.read on just the type-operator name.
|
#
08b17008 |
|
17-Jul-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes to make it easier to dispense with the let-and concrete syntax and put something else there instead. Even without throwing them away it is now possible to write ``$let`` and have this just be a variable of type alpha, rather than a parse error. So that's an improvement. If you wanted to define a constant "and", allowing this would be as simple as chucking the rule for "and", by using remove_termtok {term = GrammarSpecials.and_special, tok = "and"} and then defining the new constant "and" with Define, and possibly giving it fixities etc, as you might with any other constant. Similarly for let.
|
#
67274ad0 |
|
07-Oct-2003 |
Joe Hurd <joe@gilith.com> |
Added a few newlines at end of files to suppress warnings from my Mosml -> MLton preprocessor.
|
#
f770ee34 |
|
07-Jan-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes to accommodate the efficient definition and manipulation of big records. It's not a pretty picture underneath, but the pretty-printer is called on to make everything look as if nothing has changed.
|
#
18c87632 |
|
14-Dec-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Added new facilities for dropping or preferring certain numeric types all at once. Documented one of the new functions, and fixed the documentation for add_numeral_form, which now automatically adds the appropriate overloading for "&" (I realised that we didn't need to force the user to do this themselves).
|
#
03b97a87 |
|
08-May-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modifications to implement parsing and printing of case expressions.
|
#
3eb0895b |
|
04-May-2001 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Case expressions now parse and convert appropriately. Still to print them.
|
#
d28425f8 |
|
06-Sep-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Quite radical changes which allow for "." to be used as the record field selection operator. Lexer has changed quite dramatically: it is no longer responsible for determining whether or not a token is a "keyword" or not. Instead this is done at the parsing level. The lexer is also now unable to cope with identifiers that are a mix of alphabetically acceptable and symbolically acceptable characters.
|
#
dc18dcf9 |
|
03-Sep-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Many changes, mainly to do with record syntax. Also implemented long IDs as theory-name$id. All of HOL doesn't quite build because field selection operator is ->, which is used in the real library. Will change this to be just a simple "." Have also started on concrete syntax for updates.
|