*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Monadic do notation for Isabelle*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Date*: Fri, 21 May 2010 22:19:10 +0200*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.1.10.1005212103100.25528@atbroy100.informatik.tu-muenchen.de>*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>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100430 Fedora/3.0.4-2.fc12 Lightning/1.0b2pre Thunderbird/3.0.4

On 05/21/2010 09:11 PM, Makarius wrote:

On Fri, 21 May 2010, Christian Sternagel wrote:Hence here is just my check function: fun check_monad ts ctxt = let| subst_monad_app ctxt (Const (@{const_name "thenM"}, T), [m, n]) = (case add_monad_type ctxt n (add_monad_type ctxt m []) of typ :: _ => let val used = Term.add_free_names n []; val v = Free (Name.variant used "x", dummyT);At this point it is important to use the proper context to invent fresh names, not just the terms you hold in your hand. Term.add_free_names and Name.variant belong to a very old layer of the system. Use Variable.variant_frees or similar -- its implementation may even serve as an example how it works with contexts: fun variant_frees ctxt ts frees = let val names = Variable.names_of (fold Variable.declare_names ts ctxt); val xs = fst (Name.variants (map #1 frees) names); in xs ~~ map snd frees end;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.

fun check_monad ts ctxt = let val thy = ProofContext.theory_of ctxt; fun map_default f xs = let val ys = map f xs in if exists is_some ys then SOME (map2 the_default xs ys) else NONE end; fun subst_monad ctxt (Const (@{const_name "returnM"}, T)) = let val typ = range_type T in if is_monad_type ctxt typ then SOME (Const (get_return typ ctxt, dummyT)) else NONE end | subst_monad ctxt (Const (@{const_name "bindM"}, T) $ m $ f) = let val mty :: fty :: rty = binder_types T in (case filter (is_monad_type ctxt) (mty :: range_type fty :: rty) of typ :: _ => SOME (Const (get_bind typ ctxt, dummyT) $ m $ f) | [] => NONE) end | 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 fun no_abstract_consts t = let val cs = Term.add_const_names t [];

in (case inter (op =) cs taboos of [] => true | _ => more_err ()) end; fun check t = let val t' = Pattern.rewrite_term thy [] [subst_monad ctxt] t

in map_default check ts |> Option.map (rpair ctxt) end;

I've heard that you have made some progress off-list. If there is a nice result emerging here, it is worth posting it again.

I will :)

Makarius

chris

**Follow-Ups**:**Re: [isabelle] Monadic do notation for Isabelle***From:*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

- Previous by Date: Re: [isabelle] Monadic do notation for Isabelle
- Next by Date: Re: [isabelle] Fwd: Isatool not in 2009-1 distribution package?
- 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