*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Monadic do notation for Isabelle*From*: Makarius <makarius at sketis.net>*Date*: Wed, 19 May 2010 10:22:55 +0200 (CEST)*In-reply-to*: <AANLkTimuMcFBrcb9lNhNalOMrv8eo58W7j6ktMGR4snt@mail.gmail.com>*References*: <4BF11A08.3030604@uibk.ac.at> <AANLkTimuMcFBrcb9lNhNalOMrv8eo58W7j6ktMGR4snt@mail.gmail.com>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Tue, 18 May 2010, Brian Huffman wrote:

On Mon, May 17, 2010 at 3:27 AM, Christian Sternagel <christian.sternagel at uibk.ac.at> wrote:I would like to be able to write, e.g., do { let xs = [Some 0, Some 1, None]; x <- xs; y <- xs; let r = do { m <- x; n <- y; Some (x + y) }; return [r] } which is an admittedly contrived example. My first thought, was to give "do" an optional argument (the name of the monad that should be used), as in do List { ... do Option { ... } ... }

I can see that your parse_translation might need to read information from the current theory, but I don't see why it would have to *modify* the current theory. The parse_translation for case syntax (function case_tr in HOL/Tools/Datatype/datatype_case.ML) probably uses all the relevant techniques that you would need to implement your generic monadic syntax: it reads information about constructors from theory data, and translates the case branches (built with the "_case1" and "_case2" syntactic constructors) into the appropriate case combinators. It does not modify any theory data during parsing. I'm not sure how your current parse_translation is implemented, but here's the approach I would take: First, define some syntactic constructors for the do-syntax, similar to how the case syntax is defined in HOL.thy: nonterminals dobinds syntax "_do1" :: "'a => dobinds" ("_") "_do2" :: "[pttrn, 'a, dobinds] => dobinds" ("_ <- _;/ _") "_do_syntax" :: "[string, dobinds] => 'a" ("do _ {_}") Then define a parse_translation for "_do_syntax" that would parse the list of "_do2" and "_do1" constructors, then choose an appropriate monad instance based on the value of the string argument (obtaining the table of monad instances from the theory data). Alternatively you could omit the "string" argument to "_do_syntax" and look up the monad instance based on the type of the last statement of the do-block (except I'm not sure whether the type information would be available yet). Or you could do a lookup based on what the top-level constant of the last statement is, e.g. a term of the form [_] indicates the list monad, and Some _ indicates the option monad.

This is going in the right direction.

* The translation functions (advanced parse translations etc.) only take care of producing proper binders. * Further transformations within the type-checking phase are done by your own "check" operation, which is installed via Syntax.add_term_check

Makarius

**Follow-Ups**:**Re: [isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

**References**:**[isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

**Re: [isabelle] Monadic do notation for Isabelle***From:*Brian Huffman

- Previous by Date: [isabelle] Call for Paper: The 3rd International Symposium on Unifying Theories of Programming
- Next by Date: Re: [isabelle] parse and print translations
- Previous by Thread: Re: [isabelle] Monadic do notation for Isabelle
- Next by Thread: Re: [isabelle] Monadic do notation for Isabelle
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list