*To*: "Gerwin Klein" <gerwin.klein at nicta.com.au>*Subject*: Re: [isabelle] about longer computation syntax sugar*From*: "Liu Jian" <gjk.liu at gmail.com>*Date*: Sat, 29 Nov 2008 23:21:09 +0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <492FD0F5.5050608@nicta.com.au>*References*: <8c2dc7030811252119x2e9adc04j711b378d57aeaebe@mail.gmail.com> <492D29BF.2090900@nicta.com.au> <8c2dc7030811270724l6731ddbfr4e2e4d67d8acfa53@mail.gmail.com> <492FD0F5.5050608@nicta.com.au>

Hi, I have tried a test like "StateMonad.thy" under your direction, But A error occur when deal with "if ... then ... else..." or "case ... of ..." statement as following activateThread == do thread <- getCurThread; state <- getWaitState thread; case state of NotWaiting => return () | WaitingToSend eptr badge fault cap => if cap = None then doIPCTransfer thread (waitingIPCPartner state) else arbitrary | WaitinToReciev Note idefinition | WaitingToReceive eptr => doIPCTransfer (waitingIPCPartner state) thread | => arbitrary Note in the above definition, monads embeds in a case statement. As "State_Monad.thy" says there are some "do...done" examples in "HOL/ex/Random.thy". Lines 101~107 (Random.thy) show me a example as following: range :: "index => seed => index => seed" where "range k = (do v <- range_aux (log 2147483561 k) 1; return (v mod k) done)" When you simply change it as following, a error occurs. range :: "index => seed => index => seed" where "range k = (do v <- range_aux (log 2147483561 k) 1; if True return (v mod k) else return (v mod k) done)" cheers, Liu Jian BTW: what's the meaning of following lines. Here, I can not understand the meaning of "CONST" and the difference between "=>" and "==" in a translation translations "_do f" => "CONST run f" On Fri, Nov 28, 2008 at 7:07 PM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote: > Hi Liu, > > you need to do the rest as well, see lines 125-192 in > HOL/Library/StateMonad.thy. The file is part of Isabelle2008 already, I > believe, if not, you can find it in the Isabelle development snapshot. > > Specifically, you will need _scomp (and _fcomp if you want to leave out the > "_ <-" part) and for printing also the ML print translation. Florian > Haftmann wrote that specific theory, he'll be able to explain in more detail > how it works. > > Cheers, > Gerwin > > > Liu Jian wrote: >> >> 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

**References**:**[isabelle] about longer computation syntax sugar***From:*Liu Jian

**Re: [isabelle] about longer computation syntax sugar***From:*Gerwin Klein

**Re: [isabelle] about longer computation syntax sugar***From:*Liu Jian

**Re: [isabelle] about longer computation syntax sugar***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] load HOL4
- Next by Date: [isabelle] conversion in Isabelle
- Previous by Thread: Re: [isabelle] about longer computation syntax sugar
- Next by Thread: [isabelle] CADE-22 final call for workshop and tutorial proposals
- Cl-isabelle-users November 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list