Add Print outcome to prompt monad for debugging and tracing

Currently ignored in the state monad

3 files changed, 8 insertions, 0 deletions

diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy
index ffed5afb..2f2d43ef 100644
--- a/lib/isabelle/Prompt_monad_lemmas.thy
+++ b/lib/isabelle/Prompt_monad_lemmas.thy
@@ -42,6 +42,7 @@ datatype 'regval event =
   (* Request to write register *)
   | e_write_reg string 'regval
   | e_undefined bool
+  | e_print string
 
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
   Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
@@ -55,6 +56,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
 | Undefined : "((Undefined k), e_undefined v, k v) \<in> T"
+| Print: "((Print msg k), e_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -85,6 +87,7 @@ lemma Traces_cases:
   | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
   | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
   | (Undefined) v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
   then show ?thesis by (auto intro: that(1))
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