From 22883e5222a1a35cdca7177cdbefec8dec6d715d Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 5 Mar 2018 15:54:45 +0000
Subject: Add Print outcome to prompt monad for debugging and tracing

Currently ignored in the state monad
---
 src/gen_lib/prompt_monad.lem | 4 ++++
 src/gen_lib/state.lem        | 1 +
 2 files changed, 5 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3