#
0b62008b |
|
17-Jun-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Properly record monadsyntax's dependency on optionTheory This is important for the Moscow ML build
|
#
aab87e30 |
|
14-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add enable_monadsyntax as alias for add_monadsyntax; document it all Closes #523
|
#
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.)
|
#
376cf5e8 |
|
06-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide machinery for declaring/exporting monad information Declare options, lists, state-transformers (bad name!) and errorStateMonads as monads. For the moment, this infrastructure is not used, but next step will be to link it into the parsing and printing machinery.
|
#
d35b02e2 |
|
28-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Restore ppstream_funs as nullary type operator in term_pp_types This name is used in user-written code (users' special purpose pretty-printers), and there is no reason to rebind this name, forcing them to change things.
|
#
a8fbc262 |
|
25-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix TeX code to compile- some tests still not passing
|
#
ab22e51d |
|
02-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use grammar-deltas for user-provided absyn post-processors
|
#
5d5a8494 |
|
09-Mar-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Preserve add_user_printer properly in grammar data This requires a slightly involved process for storing references to code in theory files. Update the .doc file on add_user_printer (which was already incredibly long), and add a test. Closes #367
|
#
1478d63c |
|
04-Dec-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change monadsyntax to NOT change global grammar on load Instead, users must explicitly call {temp_,}add_monadsyntax to turn do .. od and the <- syntax on, along with the pretty-printing and augmented parsing.
|
#
53b7dbc7 |
|
26-Oct-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Tidy monad-syntax printing tests * Make sure that printing is not tested with two printers simultaneously installed * Check printing of "_unitbind" form
|
#
e2a8b9bc |
|
20-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Absyn post-processors now see the current grammar
|
#
30f78bd2 |
|
14-Dec-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
User pp fns can note terms as binders to system printer This allows better behaviour in a test case shown to me by Mike, where annotations in monad-syntax weren't appearing.
|
#
76e7cc6c |
|
12-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make monadsyntax more flexible with monad_unitbind Previously, one had to bind "monad_unitbind" to a real constant, such as option$OPTION_IGNORE_BIND. Now one can bind to a pattern, such as \m1 m2. OPTION_BIND m1 (K m2) This means that one doesn't have to define as many constants when working with a fresh monad, which feels like an advantage. Also clean-up monad selftest, and test new behaviour.
|
#
742c71b9 |
|
10-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Some minor fixes to TeX hacking for monad syntax. In short, spaces shouldn't appear in the "hol" field of TeX_notation call because tokens with spaces in them aren't going to get omitted if the grammar rule is remotely sensible (math mode munging gets hard if there are literal spaces around). Putting spaces into the TeX field is wrong (even wronger, really) for the same reason.
|
#
d88eb17f |
|
07-Nov-2014 |
Ramana Kumar <ramana@member.fsf.org> |
TeX notation for monad syntax I thought I had done this before but apparently not. Make do and od keywords (this was already the case for parmonadsyntax, now it also works for monadsyntax). Also, fix (I hope - correct if I'm wrong) parmonadsyntax's length for the left arrow.
|
#
dc4bbe43 |
|
13-May-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Tweak monad pretty-printing of ``monad_bind a f`` with f not an abstraction. In particular, the old behaviour was to print this as do a; f od which is very misleading as it suggests that there is a unit-bind happening, when in fact f has type α → β M, not just β M, for some monad M. Now the behaviour is to just give up and print ``monad_bind a f`` as ``monad_bind a f``. I am tempted to define some nice infix for this case though, perhaps a ||> f or f ' a (I’ve used the latter in the CakeML work.) But if there’s a nice infix for monad_bind a f, then there should probably be nice syntax for monad_bind a (return o f) (e.g., which is OPTION_MAP in the option monad). The case for the first syntax, is that the alternative is do v1 <- f x; v2 <- g v1; v3 <- h v2; return (ii v3) od when this might be collapsed to do v3 <- x ||> f ||> g ||> h; return (ii v3) od An infix (|-> ?) for (λx f. monad_bind x (SOME o f)) could then turn the above into x ||> f ||> g ||> h |-> ii Maybe.
|
#
7535d076 |
|
03-Feb-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Stop monadsyntax printing out “Inventing ty. vars” messages.
|
#
de504bc4 |
|
09-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Move state_transformer stuff to its own directory src/monad. This facilitates the addition of a FOR constant to state_transformerTheory.
|