fact: Fixpoint denote {A} (p : program A) : M A := match p with | p_ret _ v => Ret v | p_bind _ _ m f => denote m >>= (denote \o f) | p_cond _ b p1 p2 => if b then denote p1 else denote p2 | p_repeat n p => (fix loop m : M unit := if m is m'.+1 then denote p >> loop m' else Ret tt) n | p_while fuel c p => (fix loop m : M unit := if m is m'.+1 then (st_get >>= (fun s => if c s then denote p >> loop m' else Ret tt)) else Ret tt) fuel | p_get => st_get | p_put s' => st_put s' | p_mark t => st_mark t end.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model