Re: [isabelle] Monadic do notation for Isabelle



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. But not on any other stage :). On stage ~1 I get a MATCH exception for a call to range_type (to find out the specific "return" to use) and on stage 1 I can not use dummyT without getting a TYPE exception.

Stage 0 is perfectly OK, if you really mean to be a peer of the standard typecheck mechnism, which seems to be the case here.

BTW, the exception raised by Term.range_type is the builtin Match of SML, not MATCH (which some other modules define internally). It is important to be hypercritical concerning the naming of any exception with unqualified name and without argument, because mispelling will result in a dreaded catch-all pattern. This would make the meaning of the programm depend on the weather, since various external events are injected as Interrupt exception into the regular program executation.


 | 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

Back again to this part of inventing locally fresh names, which is suprisingly hard to get right in many practical situations.

In fact, the above is technically right, because you merely feed the name to the Term.lambda function, which will then abstract over v that is not in the body n. It is also a bit confusing, because lambda terms work via de-Bruijn indices, so you do not need to invent names in most situations -- the pretty printer will take care of the renaming if required.

Above you merely do a dummy abstraction, which usually works by incrementing "loose bounds" in the body and adding an Abs constructor on top, with a "comment" for the bound variable as you like, e.g. "x". The incrementing can be skipped if the term is "closed", which is actually a precondition for the lambda function. Your subterms seem to be indeed closed like that, because you operate as a plugin to Pattern.rewrite_term which strips off abstractions before entering the body.

Interestingly, Pattern.rewrite_term invents auxiliary free variables only by looking at the visible term material. This means there is an implicit assumption that the rewrite process will not introduce other fixed variables from the surrounding context.

Anyway, to cut a long story short, you can just use Term.abs_dummy above without your own inventing of variables. Like lambda it assumes a closed body.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.