aboutsummaryrefslogtreecommitdiffstats
path: root/src/common
diff options
context:
space:
mode:
authorMichalis Pardalos <m.pardalos@gmail.com>2021-04-18 12:52:49 +0100
committerMichalis Pardalos <m.pardalos@gmail.com>2021-04-18 12:56:01 +0100
commit4a8cfae2e3920af8aa42223635818e822d04417a (patch)
tree2f72d5199921bd0400eb6179e3cd27e28ff2a6bc /src/common
parent21e8b6ab2dcf632b6ab1ee59d25c6a15b3bd0027 (diff)
downloadvericert-4a8cfae2e3920af8aa42223635818e822d04417a.tar.gz
vericert-4a8cfae2e3920af8aa42223635818e822d04417a.zip
[WIP] Generate calling verilog in RTL->HTL
Diffstat (limited to 'src/common')
-rw-r--r--src/common/Statemonad.v8
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).