Merge pull request #590 from hacspec/fstar-add-type-annotations-on-li…

…st-literals F*: add type annotations on list literals
hacspec · Apr 9, 2024 · f7e3bbe · f7e3bbe
2 parents 00b125b + a717533
commit f7e3bbe
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 0 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -453,6 +453,23 @@ struct
         let formula = F.mk_e_app equality [ length; len ] in
         let assertion = F.mk_e_app assert_norm [ formula ] in
         let pat = F.AST.PatVar (list_ident, None, []) |> F.pat in
+        let pat =
+          match l with
+          | [] ->
+              let list_ty =
+                let prims_list = F.term_of_lid [ "Prims"; "list" ] in
+                let inner_typ =
+                  match e.typ with
+                  | TArray { typ; _ } -> pty e.span typ
+                  | _ ->
+                      Error.assertion_failure e.span
+                        "Malformed type for array literal"
+                in
+                F.mk_e_app prims_list [ inner_typ ]
+              in
+              F.pat @@ F.AST.PatAscribed (pat, (list_ty, None))
+          | _ -> pat
+        in
         F.term
         @@ F.AST.Let
              ( NoLetQualifier,

diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
@@ -58,6 +58,10 @@ Definition numeric (_ : unit) : unit :=
   let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in
   tt.
 
+Definition empty_array (_ : unit) : unit :=
+  let (_ : seq int8) := unsize !TODO empty array! : seq int8 in
+  tt.
+
 Definition panic_with_msg (_ : unit) : unit :=
   never_to_any (panic_fmt (impl_2__new_const (unsize (array_from_list [with msg])))).
 

diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
@@ -112,6 +112,14 @@ let numeric (_: Prims.unit) : Prims.unit =
   let (_: u128):u128 = pub_u128 22222222222222222222 in
   ()
 
+let empty_array (_: Prims.unit) : Prims.unit =
+  let (_: t_Slice u8):t_Slice u8 =
+    Rust_primitives.unsize (let list:Prims.list u8 = [] in
+        FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
+        Rust_primitives.Hax.array_of_list 0 list)
+  in
+  ()
+
 let panic_with_msg (_: Prims.unit) : Prims.unit =
   Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (Rust_primitives.unsize
                 (let list = ["with msg"] in

diff --git a/tests/literals/src/lib.rs b/tests/literals/src/lib.rs
@@ -44,3 +44,7 @@ fn casts(x8: u8, x16: u16, x32: u32, x64: u64, xs: usize) {
     let _: i16 = x8 as i16 + x16 as i16 + x32 as i16 + x64 as i16 + xs as i16;
     let _: i8 = x8 as i8 + x16 as i8 + x32 as i8 + x64 as i8 + xs as i8;
 }
+
+pub fn empty_array() {
+    let _: &[u8] = &[];
+}