diff options
| author | Thomas Bauereiss | 2017-10-31 16:17:45 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-10-31 16:17:45 +0000 |
| commit | fe486c7b4126131920157c9348478fe6b40d3636 (patch) | |
| tree | 1866f3e7a7c6259745214dcb94040b23a7031a6e /src/gen_lib/prompt.lem | |
| parent | a88e0182b05acf417b262173a2b83ecd9a35c93a (diff) | |
Pretty-print Sail assertions in Lem
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
Diffstat (limited to 'src/gen_lib/prompt.lem')
| -rw-r--r-- | src/gen_lib/prompt.lem | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem index 23f81f0e..cdff2972 100644 --- a/src/gen_lib/prompt.lem +++ b/src/gen_lib/prompt.lem @@ -34,6 +34,9 @@ let inline (>>) m n = m >>= fun _ -> n val exit : forall 'a 'b. 'b -> M 'a let exit s = Fail Nothing +val assert_exp : bool -> string -> M unit +let assert_exp exp msg = if exp then Done () else Fail (Just msg) + val early_return : forall 'r. 'r -> MR unit 'r let early_return r = Return r |