Re: [isabelle] about longer computation syntax sugar



Thanks Gerwin! following your direction, I write the following statements

types ('s, 'a)state_monad = " 's => ('a , 's)"

constdefs bind :: "('s, 'a)state_monad =>('a => ('s, 'b)state_monad)
=>('s, 'b)state_monad" (infixr ">>=" 60)
" f >>= g  == % s . let  (v, s') = f s in g v s'"

nonterminals
dobind

syntax
  "_bind"       :: "[pttrn, 'a] => dobind"              ("(2_ <-/ _)" 10)
  "_do"         :: "[dobind, 'a] =>  'b"               ("( do _ ;/ _
od )" [0,0] 10)

translations
 " do x <- f ; g od" == " f >>= (% x. g)"

Now, binding two monads is easy. But How to bind three or more monads
in a "do ... od"
statement? Moreover, what is the association attribute of "bind"
operator? infixr or infixl.
In the above definition I use the former. But I can not hold the
difference between them.

cheers:)

Liu Jian

On Wed, Nov 26, 2008 at 6:49 PM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
> Liu Jian wrote:
>>
>>  do x <- f; g x od == f >>= g
>>
>> But how to write the real isabelle statements for the above
>> definition? (Note there is parameter "x")
>
> It's fairly standard syntax black magic and works roughly like the normal
> let bindings in Isabelle (e.g. see HOL/HOL.thy).
>
> A more complex example directly with "do" syntax can be found in
> HOL/Library/StateMonad.thy. It's slightly different from the one in our
> papers, but the effect is the same.
>
> Cheers,
> Gerwin
>



-- 
email to: gjk.liu at gmail.com





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