History log of /seL4-l4v-10.1.1/HOL4/src/monad/monadsyntax.sig
Revision Date Author Comments
# 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.


# 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


# 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.


# 32bf1e49 02-Feb-2015 Piotr Trojanek <piotr.trojanek@gmail.com>

extra semicolons removed from (some) .sig files


# 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.