diff options
| author | Thomas Bauereiss | 2018-03-05 15:54:45 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-05 15:58:43 +0000 |
| commit | 22883e5222a1a35cdca7177cdbefec8dec6d715d (patch) | |
| tree | 577429907c2e0f737b8ea13c46c3b4bbd09018ac /src | |
| parent | 21bb415d3c148361033576af6093f72f49d92866 (diff) | |
Add Print outcome to prompt monad for debugging and tracing
Currently ignored in the state monad
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/prompt_monad.lem | 4 | ||||
| -rw-r--r-- | src/gen_lib/state.lem | 1 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem index b4b8436f..747600a9 100644 --- a/src/gen_lib/prompt_monad.lem +++ b/src/gen_lib/prompt_monad.lem @@ -30,6 +30,8 @@ type monad 'regval 'a 'e = (* Request to write register *) | Write_reg of register_name * 'regval * monad 'regval 'a 'e | Undefined of (bool -> monad 'regval 'a 'e) + (* Print debugging or tracing information *) + | Print of string * monad 'regval 'a 'e (*Result of a failed assert with possible error message to report*) | Fail of string | Error of string @@ -54,6 +56,7 @@ let rec bind m f = match m with | Footprint k -> Footprint (bind k f) | Barrier bk k -> Barrier bk (bind k f) | Write_reg r v k -> Write_reg r v (bind k f) + | Print msg k -> Print msg (bind k f) | Fail descr -> Fail descr | Error descr -> Error descr | Exception e -> Exception e @@ -89,6 +92,7 @@ let rec try_catch m h = match m with | Footprint k -> Footprint (try_catch k h) | Barrier bk k -> Barrier bk (try_catch k h) | Write_reg r v k -> Write_reg r v (try_catch k h) + | Print msg k -> Print msg (try_catch k h) | Fail descr -> Fail descr | Error descr -> Error descr | Exception e -> h e diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index 85fa15e8..3ae0d7ba 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -22,6 +22,7 @@ let rec liftState ra s = match s with | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k) | (Footprint k) -> liftState ra k | (Barrier _ k) -> liftState ra k + | (Print _ k) -> liftState ra k (* TODO *) | (Fail descr) -> failS descr | (Error descr) -> failS descr | (Exception e) -> throwS e |