Re: [isabelle] about longer computation syntax sugar



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





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