From d3abe2547c8921d2b324da67370822b7fb89b6c0 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 26 Sep 2022 13:13:51 +0100 Subject: Add global monad notation using Instances This was mostly inspired by the std++ library. --- src/common/Statemonad.v | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'src/common/Statemonad.v') diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 16dcbbf..c667fd9 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -42,7 +42,7 @@ Module Statemonad(S : State) <: Monad. Definition ret {A: Type} (x: A) : mon A := fun (s : S.st) => OK x s (S.st_refl s). - Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := + Definition bind {A B: Type} (g: A -> mon B) (f: mon A) : mon B := fun (s : S.st) => match f s with | Error msg => Error msg @@ -53,8 +53,8 @@ Module Statemonad(S : State) <: Monad. end end. - Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := - bind f (fun xy => g (fst xy) (snd xy)). + Definition bind2 {A B C: Type} (g: A -> B -> mon C) (f: mon (A * B)) : mon C := + bind (fun xy => g (fst xy) (snd xy)) (f: mon (A * B)). Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s : S.st) => @@ -76,4 +76,7 @@ Module Statemonad(S : State) <: Monad. | Error err => Errors.Error err end. + #[global] Instance statemonad_ret : MRet mon := @ret. + #[global] Instance statemonad_bind : MBind mon := @bind. + End Statemonad. -- cgit