adapted pp for Kathy's effect type changes

2 files changed, 31 insertions, 21 deletions

diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index eeff4717..7777cf5e 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -74,8 +74,8 @@ let write_memory addr l (V bits _ _) s =
   let bytes = byte_chunks l bits in
   (Left (), <| s with memstate = foldl write_memstate s.memstate (zip addrs bytes) |>)
 
-val read_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> M state 'e (vector bit)
-let read_reg_range reg (i,j) s =
+val read_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> M state 'e (vector bit)
+let read_reg_range reg i j s =
   let v = slice (read_regstate s reg) i j in
   (Left v,s)
 
@@ -84,8 +84,8 @@ let read_reg_bit reg i s =
   let v = access (read_regstate s reg) i in
   (Left v,s)
 
-val write_reg_range : forall 'e. register -> (integer * integer) (*(nat * nat)*) -> vector bit -> M state 'e unit
-let write_reg_range (reg : register) (i,j) (v : vector bit) s =
+val write_reg_range : forall 'e. register -> integer -> integer (*(nat * nat)*) -> vector bit -> M state 'e unit
+let write_reg_range reg i j v s =
   let v' = update (read_regstate s reg) i j v in
   let s' = write_regstate s reg v' in
   (Left (),s')
@@ -148,10 +148,10 @@ let rec foreachM_dec (i,stop,by) vars body =
   else return ((),vars)
 
 val read_reg_field : forall 'e. register -> register_field -> M state 'e (vector bit)
-let read_reg_field reg rfield = read_reg_range reg (field_indices rfield)
+let read_reg_field reg rfield = uncurry (read_reg_range reg) (field_indices rfield)
 
 val write_reg_field : forall 'e. register -> register_field -> vector bit -> M state 'e unit
-let write_reg_field reg rfield = write_reg_range reg (field_indices rfield)
+let write_reg_field reg rfield = uncurry (write_reg_range reg) (field_indices rfield)
 
 val read_reg_field_bit : forall 'e. register -> register_field_bit -> M state 'e bit
 let read_reg_field_bit reg rbit = read_reg_bit reg (field_index_bit rbit)
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 7e2e87b0..1e8f185c 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2082,25 +2082,35 @@ let doc_exp_lem, doc_let_lem =
                if aexp_needed then parens (align epp) else epp
            )
        )
-    | E_vector_access(v,e) ->
-       let epp = separate space [string "access";exp v;exp e] in
+    | E_vector_access (v,e) ->
+       let (Base (_,_,_,_,eff,_)) = annot in
+       let epp =
+         if has_rreg_effect eff then
+           separate space [string "read_reg_bit";exp v;exp e]
+         else
+           separate space [string "access";exp v;exp e] in
        if aexp_needed then parens (align epp) else epp
-    | E_vector_subrange(v,e1,e2) ->
-       let epp = align (string "slice" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) in
+    | E_vector_subrange (v,e1,e2) ->
+       let (Base (_,_,_,_,eff,_)) = annot in
+       let epp =
+         if has_rreg_effect eff then
+           align (string "read_reg_range" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2)
+         else
+           align (string "slice" ^^ space ^^ exp v ^//^ exp e1 ^//^ exp e2) in
        if aexp_needed then parens (align epp) else epp
     | E_field((E_aux(_,(_,fannot)) as fexp),id) ->
        let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in
-      (match t with
-       | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) ->
-          let field_f = match annot with
-            | Base((_,{t = Tid "bit"}),_,_,_,_,_)
-            | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
-             string "read_reg_field_bit"
-            | _ -> string "read_reg_field" in
-          let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^
-                      string (regtyp ^ "_") ^^ doc_id_lem id in
-         if aexp_needed then parens (align epp) else epp
-      | _ -> exp fexp ^^ dot ^^ doc_id_lem id)
+       (match t with
+        | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) ->
+           let field_f = match annot with
+             | Base((_,{t = Tid "bit"}),_,_,_,_,_)
+               | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
+                string "read_reg_field_bit"
+             | _ -> string "read_reg_field" in
+           let epp = field_f ^^ space ^^ (exp fexp) ^^ space ^^
+                       string (regtyp ^ "_") ^^ doc_id_lem id in
+           if aexp_needed then parens (align epp) else epp
+        | _ -> exp fexp ^^ dot ^^ doc_id_lem id)
     | E_block [] -> string "()"
     | E_block exps -> failwith "Blocks should have been removed till now."
     | E_nondet exps -> failwith "Nondet blocks not supported."