summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/prelude.sail2
-rw-r--r--src/gen_lib/sail_operators.lem8
-rw-r--r--src/gen_lib/sail_operators_mwords.lem2
-rw-r--r--src/gen_lib/sail_values.lem7
-rw-r--r--src/pretty_print_lem.ml70
5 files changed, 51 insertions, 38 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail
index 215f63b2..e5b5004f 100644
--- a/lib/prelude.sail
+++ b/lib/prelude.sail
@@ -310,7 +310,7 @@ val extern forall Num 'n. [:'n:] -> [:2** 'n:] effect pure pow2
val extern forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'m:] effect pure vector_length = "length"
val extern forall Type 'a. list<'a> -> nat effect pure list_length
-val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bvlength"
+val extern forall Num 'n, Num 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [:'m:] effect pure bitvector_length = "bitvector_length"
overload length [bitvector_length; vector_length; list_length]
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index f14ef2e4..b94257f0 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -5,7 +5,7 @@ open import Sail_values
(*** Bit vector operations *)
-let bvlength = length
+let bitvector_length = length
let set_bitvector_start = set_vector_start
let reset_bitvector_start = reset_vector_start
@@ -25,8 +25,10 @@ let vector_subrange_bl_dec = vector_subrange_bl
let bitvector_access_inc = vector_access_inc
let bitvector_access_dec = vector_access_dec
-let bitvector_update_pos_dec = update_pos
-let bitvector_update_subrange_dec = vector_update_dec
+let bitvector_update_pos_inc = vector_update_pos_inc
+let bitvector_update_pos_dec = vector_update_pos_dec
+let bitvector_update_subrange_inc = vector_update_subrange_inc
+let bitvector_update_subrange_dec = vector_update_subrange_dec
let extract_only_bit = extract_only_element
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 4d1cc713..a1fc1fd7 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,7 +5,7 @@ open import Sail_values
(*** Bit vector operations *)
-let bvlength bs = integerFromNat (word_length bs)
+let bitvector_length bs = integerFromNat (word_length bs)
(*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 95a61eca..48d728bf 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -246,8 +246,8 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector '
let update (Vector bs start is_inc) i j (Vector bs' _ _) =
Vector (update_aux is_inc start bs i j bs') start is_inc
-let vector_update_inc (start, v, i, j, v') = update v i j v'
-let vector_update_dec (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_inc (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_dec (start, v, i, j, v') = update v i j v'
val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a
let access_aux is_inc start xs n =
@@ -264,6 +264,9 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
let update_pos v n b =
update v n n (Vector [b] 0 false)
+let vector_update_pos_inc (start, v, i, x) = update_pos v i x
+let vector_update_pos_dec (start, v, i, x) = update_pos v i x
+
let extract_only_element (Vector elems _ _) = match elems with
| [] -> failwith "extract_only_element called for empty vector"
| [e] -> e
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 451be476..5f520dfa 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -581,7 +581,7 @@ let doc_exp_lem, doc_let_lem =
currently broken. *)
let [arg] = args in
let targ = typ_of arg in
- let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in
+ let call = if mwords && is_bitvector_typ targ then "bitvector_length" else "length" in
let epp = separate space [string call;expY arg] in
if aexp_needed then parens (align epp) else epp
(*)| Id_aux (Id "bool_not", _) ->
@@ -620,17 +620,19 @@ let doc_exp_lem, doc_let_lem =
end
| E_vector_access (v,e) ->
let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+ let (start, len, ord, etyp) = vector_typ_args_of vtyp in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ vtyp (*&& mwords*)
- then "bitvector_access" ^ ord_suffix
- else "vector_access" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
+ let call = bit_prefix ^ "vector_access" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e]) in
if aexp_needed then parens (align epp) else epp
(* raise (Reporting_basic.err_unreachable l
@@ -646,17 +648,19 @@ let doc_exp_lem, doc_let_lem =
if aexp_needed then parens (align epp) else epp*)
| E_vector_subrange (v,e1,e2) ->
let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+ let (start, len, ord, etyp) = vector_typ_args_of vtyp in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ vtyp (*&& mwords*)
- then "bitvector_subrange" ^ ord_suffix
- else "vector_subrange" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
+ let call = bit_prefix ^ "vector_subrange" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
if aexp_needed then parens (align epp) else epp
(* raise (Reporting_basic.err_unreachable l
@@ -841,33 +845,37 @@ let doc_exp_lem, doc_let_lem =
if aexp_needed then parens (align epp) else epp
(* *)
| E_vector_update(v,e1,e2) ->
- let t = typ_of full_exp in
- let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+ let t = typ_of v in
+ let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update_pos" ^ ord_suffix
- else "vector_update_pos" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ t then "bit" else "" in
+ let call = bit_prefix ^ "vector_update_pos" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
if aexp_needed then parens (align epp) else epp
| E_vector_update_subrange(v,e1,e2,e3) ->
- let t = typ_of full_exp in
- let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+ let t = typ_of v in
+ let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update_subrange" ^ ord_suffix
- else "vector_update_subrange" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ t then "bit" else "" in
+ let call = bit_prefix ^ "vector_update_subrange" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp =
align (string call ^//^
parens (separate comma_sp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:01:17 +0000