*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Monadic do notation for Isabelle*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 18 May 2010 11:27:17 -0700*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4BF11A08.3030604@uibk.ac.at>*References*: <4BF11A08.3030604@uibk.ac.at>*Sender*: huffman.brian.c at gmail.com

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 { ... } ... } > > This brings me to my actual question ;) > > If I would use Theory_Data to store the "current monad", my > parse_translations would have to modify the current theory. I assume, this > is bad (furthermore, I have no clue how to do this :)). Would it be okay to > use a reference for this? What about potential problems? Hi Christian, 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. - Brian

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

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

- Previous by Date: [isabelle] parse and print translations
- Next by Date: [isabelle] Call for Paper: The 3rd International Symposium on Unifying Theories of Programming
- Previous by Thread: [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