Re: [isabelle] Monadic do notation for Isabelle



On 05/19/2010 10:22 AM, Makarius wrote:
* The translation functions (advanced parse translations etc.) only take
care of producing proper binders.
I am not sure what you mean by that... currently I first introduce:

nonterminals
  do_expr

syntax
  ...
  "_do_bind" :: "pttrn => 'a => do_expr => do_expr"
    ("_ <- _;//_") [1000, 13, 12] 12)
  ...

consts
  ...
  bindM :: "'a => ('b => 'c) => 'c"
  ...

translations
  ...
  "_do_bind x m n" => "CONST bindM m (%x n)"
  ...

and then use Syntax.add_term_check to register a transformation from this general constants to specific ones (that have to be registered first by e.g., setup {* Monad.add_monad "option" "option_bind" "Some" *}), depending on the type.

* Further transformations within the type-checking phase are done by
your own "check" operation, which is installed via Syntax.add_term_check

1) Are those term_checks applied bottom-up to all subterms or do I have to use a recursive function that will be applied at the root?

2) Further, I saw the "stage" parameter. Do I assume correctly that the stage gives the order of the checks and that type checking is done at stage 0?

3) Is add_term_uncheck the symmetric operation before printing?

4) I find this framework very convenient :D. With few lines of code I seem to have a working solution (for the parsing direction and modulo the fact that it is currently necessary to provide typing contraints at the "right" places, but that is due to my lack of knowledge about how to use types properly in Isabelle programming).

cheers

chris





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