diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:05 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-24 13:36:05 +0100 |
commit | d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b (patch) | |
tree | 892fdd7d4d241cd456689463707cc50f8564da56 /src/common/Statemonad.v | |
parent | 39a4348657c2f3efb3feafe9cf65b0f2a1a263c2 (diff) | |
download | vericert-kvx-d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b.tar.gz vericert-kvx-d1bea5e0f88ad2cfcd0b0667fb11279100d02e6b.zip |
Add statemonad declaration
Diffstat (limited to 'src/common/Statemonad.v')
-rw-r--r-- | src/common/Statemonad.v | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v new file mode 100644 index 0000000..ed1b9e7 --- /dev/null +++ b/src/common/Statemonad.v @@ -0,0 +1,61 @@ +From compcert Require Errors. +From coqup Require Import Monad. +From Coq Require Import Lists.List. + +Module Type State. + Parameter st : Type. + Parameter st_prop : st -> st -> Prop. + + Axiom st_refl : forall s, st_prop s s. + Axiom st_trans : forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. +End State. + +Module Statemonad(S : State) <: Monad. + + Inductive res (A: Type) (s: S.st): Type := + | Error : Errors.errmsg -> res A s + | OK : A -> forall (s' : S.st), S.st_prop s s' -> res A s. + + Arguments OK [A s]. + Arguments Error [A s]. + + Definition mon (A: Type) : Type := forall (s: S.st), res A s. + + 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 := + fun (s : S.st) => + match f s with + | Error msg => Error msg + | OK a s' i => + match g a s' with + | Error msg => Error msg + | OK b s'' i' => OK b s'' (S.st_trans s s' s'' i i') + 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 handle_error {A: Type} (f g: mon A) : mon A := + fun (s : S.st) => + match f s with + | OK a s' i => OK a s' i + | Error _ => g s + end. + + Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: S.st) => Error err. + + Definition get : mon S.st := fun s => OK s s (S.st_refl s). + + Definition set (s: S.st) (i: forall s', S.st_prop s' s) : mon unit := + fun s' => OK tt s (i s'). + + Definition run_mon {A: Type} (s: S.st) (m: mon A): Errors.res A := + match m s with + | OK a s' i => Errors.OK a + | Error err => Errors.Error err + end. + +End Statemonad. |