From 886cff213039c034bc78408ea52689514e0c9a69 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 3 Jan 2019 18:31:04 +0000
Subject: Add a few helper lemmas

---
 src/gen_lib/sail2_prompt_monad.lem | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 7a55056c..e0ac09f6 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -272,6 +272,8 @@ val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event
 let emitEvent m e = match (e, m) with
   | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
      if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing
   | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
      if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
   | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
-- 
cgit v1.2.3