Re: [isabelle] Monadic do notation for Isabelle



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.
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.

Here is my new check function (as I said, when registered at stage 0, every example I have tried, did also work). Thanks to alex krauss, I am now using Pattern.rewrite_term, which makes everthing much more convenient. If I understand correctly, since I registered "check_monad" at stage 0, it is interleaved with type inference... and that is exactly what I need here.

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 [];
val taboos = [ at {const_name "returnM"}, @{const_name "bindM"}, @{const_name "thenM"}];
      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 if t = t' andalso no_abstract_consts t then NONE else SOME t' end;
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

PS: I will change the variable stuff according to your comment... it is sometimes difficult to see from the sources, which functions are supposed to be used and which not :D






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