Skip to content

Commit

Permalink
TC: sizeof rewriting for vector types
Browse files Browse the repository at this point in the history
  • Loading branch information
bacam committed Jan 14, 2025
1 parent ae8c345 commit 46e755d
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 1 deletion.
2 changes: 1 addition & 1 deletion lib/vector.sail
Original file line number Diff line number Diff line change
Expand Up @@ -397,6 +397,6 @@ val signed = pure {

$endif

overload __size = {__id, bitvector_length}
overload __size = {__id, bitvector_length, vector_length}

$endif
2 changes: 2 additions & 0 deletions src/lib/type_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1145,6 +1145,8 @@ let rec rewrite_sizeof' l env (Nexp_aux (aux, _) as nexp) =
| Typ_app (id, [A_aux (A_nexp n, _)]) when string_of_id id = "atom" -> prove __POS__ env (nc_eq (nvar v) n)
| Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)]) when string_of_id id = "bitvector" ->
Kid.compare v v' = 0
| Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _); _]) when string_of_id id = "vector" ->
Kid.compare v v' = 0
| _ -> false
in
begin
Expand Down
7 changes: 7 additions & 0 deletions test/typecheck/pass/implicit_vector.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
default Order dec
$include <prelude.sail>

val f : forall 'n, 'n > 0. (implicit('n), vector('n, int)) -> unit
val g : forall 'n, 'n > 0. vector('n, int) -> unit

function g(bv) = f(bv)

0 comments on commit 46e755d

Please sign in to comment.