HandlersEx.thy.in

theory HandlersEx
imports Main Handlers
begin

definition computation :: compt where
  "computation \<equiv> [[
     get () (\xx.
     put inl xx (\uu.
     get () (\yy.
     put (xx,yy) (\uuu.
     get () (\zz.
     return zz))))) ]]"

definition runState :: "compt \<Rightarrow> compt" where
  "runState \<equiv> \<lambda>m. [[
     handle m with
       { return xxx -> \st. (xxx,st)! }
     + { get xxx kk -> \st. ((kk! st) st) }
     + { put xxx kk -> \st. ((kk! ()) xxx) } ]]"

definition outer :: "compt \<Rightarrow> compt" where
  "outer \<equiv> \<lambda>m. [[ m inr () ]]"

definition expectedResult :: compt where
  "expectedResult \<equiv> [[ ((inr (), inl inr ()) , (inr (), inl inr ()))! ]]"

definition bad :: compt where
  "bad \<equiv> [[ 
     let xx <- handle let yy <- get () (\xx. return xx) in return xx with
                 { return xxx -> return () }
               + { get xxx kk -> return () } in
     return () ]]"

end