*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*: Tue, 25 May 2010 14:18:00 +0200 (CEST)*In-reply-to*: <4BF6EABE.3060303@uibk.ac.at>*References*: <4BF11A08.3030604@uibk.ac.at> <AANLkTimuMcFBrcb9lNhNalOMrv8eo58W7j6ktMGR4snt@mail.gmail.com> <alpine.LNX.1.10.1005191015360.10540@atbroy100.informatik.tu-muenchen.de> <4BF44AAF.3010009@uibk.ac.at> <alpine.LNX.1.10.1005201925001.14391@atbroy100.informatik.tu-muenchen.de> <4BF69E41.1050302@uibk.ac.at> <alpine.LNX.1.10.1005212103100.25528@atbroy100.informatik.tu-muenchen.de> <4BF6EABE.3060303@uibk.ac.at>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Fri, 21 May 2010, Christian Sternagel wrote:

I) Currently I'm going for Case 2 (of makarius suggestion) and registered the check function at stage 0.I recommend to use a stage number <> 0. While there are standard policies about precedence of plugins at the same stage, it is better to make your intention fully clear.The problem is that I have a solution that works when using stage 0. Butnot on any other stage :). On stage ~1 I get a MATCH exception for acall to range_type (to find out the specific "return" to use) and onstage 1 I can not use dummyT without getting a TYPE exception.

| subst_monad ctxt (Const (@{const_name "thenM"}, T) $ m $ n) = (case filter (is_monad_type ctxt) (binder_types T) of typ :: _ => let val used = Term.add_free_names n []; val v = Free (Name.variant used "x", dummyT); in SOME (Const (get_bind typ ctxt, dummyT) $ m $ lambda v n) end | [] => NONE) | subst_monad ctxt _ = NONE

Makarius

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

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

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

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

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

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

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

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

- Previous by Date: [isabelle] New AFP entry: Regular Sets and Expressions
- Next by Date: [isabelle] A very strange case
- 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