diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-18 12:52:49 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-18 12:56:01 +0100 |
commit | 4a8cfae2e3920af8aa42223635818e822d04417a (patch) | |
tree | 2f72d5199921bd0400eb6179e3cd27e28ff2a6bc /src/common/Statemonad.v | |
parent | 21e8b6ab2dcf632b6ab1ee59d25c6a15b3bd0027 (diff) | |
download | vericert-4a8cfae2e3920af8aa42223635818e822d04417a.tar.gz vericert-4a8cfae2e3920af8aa42223635818e822d04417a.zip |
[WIP] Generate calling verilog in RTL->HTL
Diffstat (limited to 'src/common/Statemonad.v')
-rw-r--r-- | src/common/Statemonad.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 16dcbbf..20558e0 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -63,6 +63,14 @@ Module Statemonad(S : State) <: Monad. | Error _ => g s end. + Definition handle_opt {A : Type} (err : Errors.errmsg) (val : option A) + : mon A := + fun s => + match val with + | Some a => OK a s (S.st_refl s) + | None => Error err + 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). |