Re: [isabelle] Monadic do notation for Isabelle



On Wed, 19 May 2010, Christian Sternagel wrote:

* 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?

Each check or uncheck operation operates on the whole textual situation, i.e. a context and a collection of terms to be treated simultaneously. Thus you do not only get the root of a single term, but the full chunk of text to be processed, i.e. the super-root. You can also keep information in the result context for later -- in the very end it is discarded, though.

Stages progress from smaller to larger integer values for check, and reverse for uncheck. At stage 0 there are the "standard" check/uncheck phases, there is also a final "fixate" check at stage 100 to finalize type-inference parameters that are left over. Anything else can be defined in the user context, and arbitrary things can be done here, i.e. this powerful mechanism needs to be used with some care.

Since the whole process iterates repeatedly over all stages, your part might get invoked multiple times, until a global fixed-point is reached (if it ever happens). This is a bit like a simplifier on abstract syntax, but without any builtin strategy to traverse the terms.


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

Somehow the standard type checking at phase 0 is special: it takes raw parser output (where all names and binder scopes are already resolved, but lacks type information apart from constraints that happen to be in the input), and produces fully types terms according to the usual Hindley-Milner scheme. If you act before, you won't get proper type information, but afterwards most of it is already finished. Typically, later check phases merely "improve" inferred types by specializing them, as is usually done in advanced Haskell-style systems.

Case 1: You operate after stage 0. This means that your concrete syntax needs to be mapped to auxiliary combinators etc. that will be accepted by the standard type check. That result can then be expanded to suitable logical constants by your function. In other words you need to be able to model your monad language using simply-typed higher-order abstract syntax.

Case 2: You operate before stage 0. This means you merely rearrange the user input schematically such that the later stages will synthesize just the right types accidentally. This is a bit like "for" in Scala, where the compiler expands nested comprehensions to certain combinators in an untyped fashion. (Maybe they now have some papers on the details, I did not find any 1-2 years ago. There are some basic explanations in the Scala book by Odersky-et-al.)


	Makarius






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