Module type Theory.Effect

The theory of effects.

val perform : 'a Effect.sort -> 'a eff

perform s performs a generic effect of sort s.

val set : 'a var -> 'a pure -> data eff

set v x changes the value stored in v to the value of x.

val jmp : _ bitv -> ctrl eff

jmp dst passes the control to a program located at dst.

val goto : label -> ctrl eff

goto lbl passes the control to a program labeled with lbl.

val seq : 'a eff -> 'a eff -> 'a eff

seq x y performs effect x, after that perform effect y.

val blk : label -> data eff -> ctrl eff -> unit eff

blk lbl data ctrl an optionally labeled sequence of effects.

If lbl is Label.null then the block is unlabeled. If it is not Label.null then the denotations will preserve the label and assume that this blk is referenced from some other blocks.

  • since 2.4.0 the [blk] operator accepts (and welcomes)

Label.null as the label in cases when the block is not really expected to be called from anywhere else.

val repeat : bool -> data eff -> data eff

repeat c data repeats data effects until the condition c holds.

val branch : bool -> 'a eff -> 'a eff -> 'a eff

branch c lhs rhs if c holds then performs lhs else rhs.