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.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 99105a6d..074ad60f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1884,7 +1884,12 @@ let rewrite_fix_val_specs (Defs defs) =
            TypSchm_aux (TypSchm_ts (tq, typ), Parse_ast.Unknown), val_specs
          end else begin
            let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
-           typschm, Bindings.add id (tq, typ) val_specs
+           (* Add rreg effect to internal _reg_deref function (cf. bitfield.ml) *)
+           let vs =
+             if string_of_id id = "_reg_deref" then
+               add_eff_to_vs (mk_effect [BE_rreg]) (tq, typ)
+             else (tq, typ) in
+           typschm, Bindings.add id vs val_specs
          end
        in
        (val_specs, defs @ [DEF_spec (VS_aux (VS_val_spec (typschm, id, ext_opt, is_cast), a))])