diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/gen_lib/sail_values.ml | 8 | ||||
| -rw-r--r-- | src/pretty_print.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index b86ff572..c8181572 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -6,7 +6,7 @@ type number = Big_int_Z.big_int type value = | Vvector of vbit array * int * bool - | VvectorR of value array * int * bool + | VvectorR of value ref array * int * bool | Vregister of vbit array * int * bool * (string * (int * int)) list | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*) @@ -27,8 +27,8 @@ let get_varray = function let vector_access v n = match v with | VvectorR(array,start,is_inc) -> if is_inc - then array.(n-start) - else array.(start-n) + then !(array.(n-start)) + else !(array.(start-n)) | _ -> assert false let bit_vector_access v n = match v with @@ -51,7 +51,7 @@ let vector_subrange v n m = match v with | VvectorR(array,start,is_inc) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in - VvectorR(builder array length offset (VvectorR([||], 0, is_inc)),n,is_inc) + VvectorR(builder array length offset (ref (VvectorR([||], 0, is_inc))),n,is_inc) | Vvector(array,start,is_inc) -> let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in Vvector(builder array length offset Vzero,n,is_inc) diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 310ca9d4..b9d4fa2c 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1482,7 +1482,7 @@ let doc_exp_ocaml, doc_let_ocaml = match annot with | Base((_,t),External(Some name),_,_,_) -> string name | _ -> doc_id_ocaml id in - separate space [call; parens (separate_map comma exp [e1;e2])] + parens (separate space [call; parens (separate_map comma exp [e1;e2])]) | E_internal_let(lexp, eq_exp, in_exp) -> separate space [string "let"; doc_lexp_ocaml lexp; (*Rewriter/typecheck should ensure this is only cast or id*) |