Improve rewriting of sizeof expressions

If some type-level variables in a sizeof expression in a function body cannot
be directly extracted from the parameters of the function, add a new parameter
for each unresolved parameter, and rewrite calls to the function accordingly

1 files changed, 12 insertions, 0 deletions

diff --git a/test/typecheck/pass/sizeof_vector_start_index.sail b/test/typecheck/pass/sizeof_vector_start_index.sail
new file mode 100644
index 00000000..6ad8ef06
--- /dev/null
+++ b/test/typecheck/pass/sizeof_vector_start_index.sail
@@ -0,0 +1,12 @@
+val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'n:] effect pure vector_start_index
+
+function forall Num 'n, Num 'm, Order 'ord, Type 'a. [:'n:] vector_start_index ((vector<'n,'m,'ord,'a>) vec) =
+{
+  sizeof 'n
+}
+
+function int test ((vector<47,11,dec,bit>) vec) =
+{
+  vector_start_index(vec)
+}
+