Fix issues

11 files changed, 140 insertions, 57 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index bcfe4369..9ee94db2 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -218,44 +218,53 @@ let keywords () =
   List.concat [ named_unops; named_binops; misc ]
 
 let assumed_adts () : (assumed_ty * string) list =
-  List.map
-    (fun (t, s) ->
-      if !backend = Lean then
-        ( t,
-          Printf.sprintf "%c%s"
-            (Char.uppercase_ascii s.[0])
-            (String.sub s 1 (String.length s - 1)) )
-      else (t, s))
-    (match !backend with
-    | Lean ->
-        [
-          (State, "State");
-          (Result, "Result");
-          (Error, "Error");
-          (Fuel, "Nat");
-          (Option, "Option");
-          (Vec, "Vec");
-        ]
-    | Coq | FStar ->
-        [
-          (State, "state");
-          (Result, "result");
-          (Error, "error");
-          (Fuel, "nat");
-          (Option, "option");
-          (Vec, "vec");
-        ]
-    | HOL4 ->
-        [
-          (State, "state");
-          (Result, "result");
-          (Error, "error");
-          (Fuel, "num");
-          (Option, "option");
-          (Vec, "vec");
-        ])
+  match !backend with
+  | Lean ->
+      [
+        (State, "State");
+        (Result, "Result");
+        (Error, "Error");
+        (Fuel, "Nat");
+        (Option, "Option");
+        (Vec, "Vec");
+        (Array, "Array");
+        (Slice, "Slice");
+        (Str, "Str");
+        (Range, "Range");
+      ]
+  | Coq | FStar ->
+      [
+        (State, "state");
+        (Result, "result");
+        (Error, "error");
+        (Fuel, "nat");
+        (Option, "option");
+        (Vec, "vec");
+        (Array, "array");
+        (Slice, "slice");
+        (Str, "str");
+        (Range, "range");
+      ]
+  | HOL4 ->
+      [
+        (State, "state");
+        (Result, "result");
+        (Error, "error");
+        (Fuel, "num");
+        (Option, "option");
+        (Vec, "vec");
+        (Array, "array");
+        (Slice, "slice");
+        (Str, "str");
+        (Range, "range");
+      ]
 
-let assumed_structs : (assumed_ty * string) list = []
+let assumed_struct_constructors () : (assumed_ty * string) list =
+  match !backend with
+  | Lean -> [ (Range, "Range.mk"); (Array, "Array.mk") ]
+  | Coq -> [ (Range, "range.mk"); (Array, "array.mk") ]
+  | FStar -> [ (Range, "mkrange"); (Array, "mkarray") ]
+  | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
 
 let assumed_variants () : (assumed_ty * VariantId.id * string) list =
   match !backend with
@@ -320,6 +329,21 @@ let assumed_llbc_functions () :
         (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
         (VecIndexMut, None, "vec_index_mut_fwd");
         (VecIndexMut, rg0, "vec_index_mut_back");
+        (ArraySharedIndex, None, "array_shared_index");
+        (ArrayMutIndex, None, "array_mut_index_fwd");
+        (ArrayMutIndex, rg0, "array_mut_index_back");
+        (ArrayToSharedSlice, None, "array_to_shared_slice");
+        (ArrayToMutSlice, None, "array_to_mut_slice_fwd");
+        (ArrayToMutSlice, rg0, "array_to_mut_slice_back");
+        (ArraySharedSubslice, None, "array_shared_subslice");
+        (ArrayMutSubslice, None, "array_mut_subslice_fwd");
+        (ArrayMutSubslice, rg0, "array_mut_subslice_back");
+        (SliceSharedIndex, None, "slice_shared_index");
+        (SliceMutIndex, None, "slice_mut_index_fwd");
+        (SliceMutIndex, rg0, "slice_mut_index_back");
+        (SliceSharedSubslice, None, "slice_shared_subslice");
+        (SliceMutSubslice, None, "slice_mut_subslice_fwd");
+        (SliceMutSubslice, rg0, "slice_mut_subslice_back");
       ]
   | Lean ->
       [
@@ -335,6 +359,21 @@ let assumed_llbc_functions () :
         (VecIndex, rg0, "Vec.index_back") (* shouldn't be used *);
         (VecIndexMut, None, "Vec.index_mut");
         (VecIndexMut, rg0, "Vec.index_mut_back");
+        (ArraySharedIndex, None, "Array.shared_index");
+        (ArrayMutIndex, None, "Array.mut_index");
+        (ArrayMutIndex, rg0, "Array.mut_index_back");
+        (ArrayToSharedSlice, None, "Array.to_shared_slice");
+        (ArrayToMutSlice, None, "Array.to_mut_slice");
+        (ArrayToMutSlice, rg0, "Array.to_mut_slice_back");
+        (ArraySharedSubslice, None, "Array.shared_subslice");
+        (ArrayMutSubslice, None, "Array.mut_subslice");
+        (ArrayMutSubslice, rg0, "Array.mut_subslice_back");
+        (SliceSharedIndex, None, "Slice.shared_index");
+        (SliceMutIndex, None, "Slice.mut_index");
+        (SliceMutIndex, rg0, "Slice.mut_index_back");
+        (SliceSharedSubslice, None, "Slice.shared_subslice");
+        (SliceMutSubslice, None, "Slice.mut_subslice");
+        (SliceMutSubslice, rg0, "Slice.mut_subslice_back");
       ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
@@ -361,7 +400,7 @@ let names_map_init () : names_map_init =
   {
     keywords = keywords ();
     assumed_adts = assumed_adts ();
-    assumed_structs;
+    assumed_structs = assumed_struct_constructors ();
     assumed_variants = assumed_variants ();
     assumed_llbc_functions = assumed_llbc_functions ();
     assumed_pure_functions = assumed_pure_functions ();
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 3d258b32..4d67a4e4 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -452,8 +452,8 @@ let give_back_symbolic_value (_config : C.config)
   | V.SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
     ->
       ()
-  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin ->
-      raise (Failure "Unrechable"));
+  | FunCallRet | SynthInput | Global | LoopOutput | LoopJoin | Aggregate ->
+      raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index c3ff8d4f..0834cfe2 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -713,17 +713,30 @@ let eval_rvalue_aggregate (config : C.config)
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
-    | E.AggregatedArray (ety, cg) ->
+    | E.AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
         assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
-        assert (Z.to_int len = List.length values);
+        assert (len = Z.of_int (List.length values));
         let v = V.Adt { variant_id = None; field_values = values } in
         let ty = T.Adt (T.Assumed T.Array, [], [ ety ], [ cg ]) in
         let aggregated : V.typed_value = { V.value = v; ty } in
+        (* In order to generate a better AST, we introduce a symbolic
+           value equal to the array. The reason is that otherwise, the
+           array we introduce here might be duplicated in the generated
+           code: by introducing a symbolic value we introduce a let-binding
+           in the generated code. *)
+        let saggregated =
+          mk_fresh_symbolic_typed_value_from_ety V.Aggregate ty
+        in
         (* Call the continuation *)
-        cf aggregated ctx
+        match cf saggregated ctx with
+        | None -> None
+        | Some e ->
+            (* Introduce the symbolic value in the AST *)
+            let sv = ValuesUtils.value_as_symbolic saggregated.value in
+            Some (SymbolicAst.IntroSymbolic (ctx, None, sv, aggregated, e)))
   in
   (* Compose and apply *)
   comp eval_ops compute cf
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 79fe79e7..207acef6 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1051,12 +1051,10 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
-    (region_args : T.erased_region list) (type_args : T.ety list)
+    (_region_args : T.erased_region list) (type_args : T.ety list)
     (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
  fun cf ctx ->
-  assert (region_args = []);
-
   (* Retrieve the (correctly instantiated) body *)
   let def = C.ctx_lookup_fun_decl ctx fid in
   (* We can evaluate the function call only if it is not opaque *)
@@ -1157,11 +1155,10 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
  *)
 and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (fid : A.fun_id) (inst_sg : A.inst_fun_sig)
-    (region_args : T.erased_region list) (type_args : T.ety list)
+    (_region_args : T.erased_region list) (type_args : T.ety list)
     (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
  fun cf ctx ->
-  assert (region_args = []);
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
   let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index a50bb7ac..7bd37550 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -255,7 +255,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack ->
+        | V.SynthRetGivenBack | V.Global | V.LoopGivenBack | V.Aggregate ->
             ()
     end
   in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index e73c09c4..f29c7f88 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -459,8 +459,20 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
             | T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
                 assert (v0.V.ty = inner_ty);
                 assert (v1.V.ty = inner_ty)
-            | (T.Array | T.Slice | T.Str), _, _, _, _ ->
-                raise (Failure "Unexpected")
+            | T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
+                (* *)
+                assert (
+                  List.for_all
+                    (fun (v : V.typed_value) -> v.V.ty = inner_ty)
+                    inner_values);
+                (* The length is necessarily concrete *)
+                let len =
+                  (PrimitiveValuesUtils.literal_as_scalar
+                     (TypesUtils.const_generic_as_literal cg))
+                    .value
+                in
+                assert (Z.of_int (List.length inner_values) = len)
+            | (T.Slice | T.Str), _, _, _, _ -> raise (Failure "Unexpected")
             | _ -> raise (Failure "Erroneous type"))
         | V.Bottom, _ -> (* Nothing to check *) ()
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 7d7e8549..9aa73d7c 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -126,7 +126,11 @@ module Values = struct
                 else raise (Failure "Unreachable")
             | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
             | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
-            | _ -> raise (Failure "Inconsistent value"))
+            | Array, _ ->
+                (* Happens when we aggregate values *)
+                "@Array[" ^ String.concat ", " field_values ^ "]"
+            | _ ->
+                raise (Failure ("Inconsistent value: " ^ V.show_typed_value v)))
         | _ -> raise (Failure "Inconsistent typed value"))
     | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty
     | Borrow bc -> borrow_content_to_string fmt bc
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 0f64720e..8f5b5df4 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -3,7 +3,11 @@
 open Pure
 open PureUtils
 
-(** Utility function, used for type checking *)
+(** Utility function, used for type checking.
+
+    We need the number of fields for cases like `Slice`, when the number of fields
+    varies.
+ *)
 let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
     (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list)
     (cgs : const_generic list) : ty list =
@@ -51,10 +55,18 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           let ty = Collections.List.to_cons_nil tys in
           assert (variant_id = None);
           [ ty; ty ]
-      | Vec | Array | Slice | Str ->
-          raise
-            (Failure
-               "Unreachable: trying to access the fields of an opaque type"))
+      | Array ->
+          let ty = Collections.List.to_cons_nil tys in
+          let cg = Collections.List.to_cons_nil cgs in
+          let len =
+            (PrimitiveValuesUtils.literal_as_scalar
+               (TypesUtils.const_generic_as_literal cg))
+              .value
+          in
+          let len = Z.to_int len in
+          Collections.List.repeat len ty
+      | Vec | Slice | Str ->
+          raise (Failure "Attempting to access the fields of an opaque type"))
 
 type tc_ctx = {
   type_decls : type_decl TypeDeclId.Map.t;  (** The type declarations *)
diff --git a/compiler/Values.ml b/compiler/Values.ml
index f70b9b4b..d884c319 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -50,6 +50,8 @@ type sv_kind =
       (** A value given back by a loop (when ending abstractions while going backwards) *)
   | LoopJoin
       (** The result of a loop join (when computing loop fixed points) *)
+  | Aggregate
+      (** A symbolic value we introduce in place of an aggregate value *)
 [@@deriving show, ord]
 
 (** Ancestor for {!symbolic_value} iter visitor *)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index d748cc2e..527434c1 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -17,6 +17,9 @@ let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
 let mk_abottom (ty : rty) : typed_avalue = { value = ABottom; ty }
 let mk_aignored (ty : rty) : typed_avalue = { value = AIgnored; ty }
 
+let value_as_symbolic (v : value) : symbolic_value =
+  match v with Symbolic v -> v | _ -> raise (Failure "Unexpected")
+
 (** Box a value *)
 let mk_box_value (v : typed_value) : typed_value =
   let box_ty = mk_box_ty v.ty in
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index ae63b129..cc63c48f 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -17,3 +17,4 @@ package «tests» {}
 @[default_target] lean_lib noNestedBorrows
 @[default_target] lean_lib paper
 @[default_target] lean_lib poloniusList
+@[default_target] lean_lib array