Skip to content
This repository has been archived by the owner on Jul 24, 2019. It is now read-only.

Commit

Permalink
Usage of the call function instead of the Call constructor
Browse files Browse the repository at this point in the history
  • Loading branch information
clarus committed Mar 24, 2015
1 parent bf8d0bb commit ebd63b8
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/Exception.v
Original file line number Diff line number Diff line change
Expand Up @@ -25,19 +25,19 @@ Definition effect (E : Effect.t) (Exc : Type) : Effect.t :=

Definition lift {E : Effect.t} {Exc A : Type} (x : C.t E A)
: C.t (effect E Exc) A :=
C.run (fun c => C.Call (effect E Exc) (Command.Ok c)) x.
C.run (fun c => call (effect E Exc) (Command.Ok c)) x.

Definition raise {E : Effect.t} {Exc A : Type} (exc : Exc)
: C.t (effect E Exc) A :=
let! absurd := C.Call (effect E Exc) (Command.Exc exc) in
let! absurd := call (effect E Exc) (Command.Exc exc) in
match absurd with end.

Fixpoint run {E : Effect.t} {Exc A : Type} (x : C.t (effect E Exc) A)
: C.t E (A + list Exc) :=
match x with
| C.Ret _ x => ret @@ inl x
| C.Call (Command.Ok c) =>
let! answer := C.Call E c in
let! answer := call E c in
ret @@ inl answer
| C.Call (Command.Exc exc) => ret @@ inr [exc]
| C.Let _ _ x f =>
Expand Down

0 comments on commit ebd63b8

Please sign in to comment.