diff options
| author | Thomas Bauereiss | 2018-01-29 18:07:28 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-29 18:50:02 +0000 |
| commit | 2cb852f6ba093dcd59ddececea1e827c27e506aa (patch) | |
| tree | f2055460ce92814fd6e34f1957b392ee7c707e8e /src/gen_lib/state.lem | |
| parent | 2fdbc2993a9092121cf7f3eddeab688d83499553 (diff) | |
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.
Diffstat (limited to 'src/gen_lib/state.lem')
| -rw-r--r-- | src/gen_lib/state.lem | 2 |
1 files changed, 1 insertions, 1 deletions
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)] |