Enhancements

engine/backends/fstar/fstar_backend.ml

@@ -327,7 +327,7 @@ struct
         @@ F.AST.Project (pexpr arg, F.lid [ "_" ^ string_of_int (n + 1) ])
     | App { f = { e = GlobalVar (`Projector (`Concrete cid)) }; args = [ arg ] }
       ->
-        F.term @@ F.AST.Project (pexpr arg, pfield_concrete_ident cid)
+        F.term @@ F.AST.Project (pexpr arg, pconcrete_ident cid)
     | App { f = { e = GlobalVar x }; args } when Map.mem operators x ->
         let arity, op = Map.find_exn operators x in
         if List.length args <> arity then
@@ -343,7 +343,20 @@ struct
                None,
                pexpr then_,
                Option.value_map else_ ~default:F.unit ~f:pexpr )
-    | Array l -> F.AST.mkConsList F.dummyRange (List.map ~f:pexpr l)
+    | Array l ->
+        let len = List.length l in
+        let body = F.AST.mkConsList F.dummyRange (List.map ~f:pexpr l) in
+        let array_of_list =
+          let id =
+            Concrete_ident.of_name Value Rust_primitives__hax__array_of_list
+          in
+          F.term @@ F.AST.Name (pconcrete_ident id)
+        in
+        F.term_of_string
+          ("(let l = " ^ term_to_string body
+         ^ " in assert_norm (List.Tot.length l == " ^ Int.to_string len ^ "); "
+          ^ term_to_string array_of_list
+          ^ " l)")
     | Let { lhs; rhs; body; monadic = Some monad } ->
         let p =
           F.pat @@ F.AST.PatAscribed (ppat lhs, (pty lhs.span lhs.typ, None))

engine/lib/concrete_ident/concrete_ident.ml

@@ -61,6 +61,17 @@ module Imported = struct
         | Some path, Some { data = Ctor; _ } -> path
         | _ -> path);
     }
+
+  let map_path_strings ~(f : string -> string) (did : def_id) : def_id =
+    let f : def_path_item -> def_path_item = function
+      | TypeNs s -> TypeNs (f s)
+      | ValueNs s -> ValueNs (f s)
+      | MacroNs s -> MacroNs (f s)
+      | LifetimeNs s -> LifetimeNs (f s)
+      | other -> other
+    in
+    let f x = { x with data = f x.data } in
+    { did with path = List.map ~f did.path }
 end
 
 module Kind = struct
@@ -85,6 +96,9 @@ end
 type t = { def_id : Imported.def_id; kind : Kind.t }
 [@@deriving show, yojson, sexp]
 
+let map_path_strings ~(f : string -> string) (cid : t) : t =
+  { cid with def_id = Imported.map_path_strings ~f cid.def_id }
+
 (* [kind] is really a metadata, it is not relevant, `def_id`s are unique *)
 let equal x y = [%equal: Imported.def_id] x.def_id y.def_id
 let compare x y = [%compare: Imported.def_id] x.def_id y.def_id
@@ -219,6 +233,8 @@ let rec to_view ({ def_id; kind } : t) : view =
 
 and to_definition_name (x : t) : string = (to_view x).definition
 
+let to_crate_name (x : t) : string = (to_view x).crate
+
 let to_namespace x =
   let View.{ crate; path; _ } = to_view x in
   (crate, path)

engine/lib/concrete_ident/concrete_ident.mli

@@ -22,4 +22,6 @@ type view = { crate : string; path : string list; definition : string }
 
 val to_view : t -> view
 val to_definition_name : t -> string
+val to_crate_name : t -> string
 val to_namespace : t -> string * string list
+val map_path_strings : f:(string -> string) -> t -> t