From 2cb852f6ba093dcd59ddececea1e827c27e506aa Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 29 Jan 2018 18:07:28 +0000
Subject: Add rreg effect to _reg_deref in fix_val_specs rewrite

The internal function _reg_deref is declared as pure, so that bitfield setters
can be implemented as read-modify-write, while only having a wreg effect.
However, for the Lem shallow embedding, the read step of those setters needs to
be embedded into the monad.  This could be special-cased in the Lem pretty
printer, but then the pretty printer would have to replicate some logic of the
letbind_effects rewriting step.  It seems simplest to add the effect annotation
early in the Lem rewriting pipeline, in the fix_val_specs step.  This means
that this rewriting step can only be used for other backends if these
additional effects are acceptable.
---
 src/gen_lib/state.lem | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index df530bc7..b6852aaf 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -182,7 +182,7 @@ let write_tag t state =
   let tagstate = Map.insert taddr t state.tagstate in
   [(Value true,  <| state with tagstate = tagstate |>)]
 
-val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M  'regs 'a 'e
+val read_reg : forall 'regs 'a 'e. register_ref 'regs 'a -> M 'regs 'a 'e
 let read_reg reg state =
   let v = reg.read_from state.regstate in
   [(Value v,state)]
-- 
cgit v1.2.3