From 9d27e2e27db06eaad7565b55366ca8734b364fca Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 11:03:59 +0200
Subject: Make progress proapagating the changes

---
 compiler/SymbolicToPure.ml | 46 +++++++++++++++++++++++++++++-----------------
 1 file changed, 29 insertions(+), 17 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5dc8664a..ba2a6525 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -240,6 +240,8 @@ let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
     r_to_string;
     type_var_id_to_string;
     type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
+    const_generic_var_id_to_string = ast_fmt.const_generic_var_id_to_string;
+    global_decl_id_to_string = ast_fmt.global_decl_id_to_string;
     adt_variant_to_string = ast_fmt.adt_variant_to_string;
     var_id_to_string;
     adt_field_names = ast_fmt.adt_field_names;
@@ -247,10 +249,12 @@ let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
 
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
   let type_params = ctx.fun_decl.signature.type_params in
+  let cg_params = ctx.fun_decl.signature.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+    cg_params
 
 let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
   let fmt = bs_ctx_to_ctx_formatter ctx in
@@ -273,8 +277,12 @@ let rty_to_string (ctx : bs_ctx) (ty : T.rty) : string =
 
 let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
   let type_params = def.type_params in
+  let cg_params = def.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
-  let fmt = PrintPure.mk_type_formatter type_decls type_params in
+  let global_decls = ctx.global_context.llbc_global_decls in
+  let fmt =
+    PrintPure.mk_type_formatter type_decls global_decls type_params cg_params
+  in
   PrintPure.type_decl_to_string fmt def
 
 let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
@@ -283,21 +291,25 @@ let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
 
 let fun_sig_to_string (ctx : bs_ctx) (sg : fun_sig) : string =
   let type_params = sg.type_params in
+  let cg_params = sg.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
     PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+      cg_params
   in
   PrintPure.fun_sig_to_string fmt sg
 
 let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
   let type_params = def.signature.type_params in
+  let cg_params = def.signature.const_generic_params in
   let type_decls = ctx.type_context.llbc_type_decls in
   let fun_decls = ctx.fun_context.llbc_fun_decls in
   let global_decls = ctx.global_context.llbc_global_decls in
   let fmt =
     PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+      cg_params
   in
   PrintPure.fun_decl_to_string fmt def
 
@@ -315,16 +327,17 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
   Print.Values.abs_to_string fmt verbose indent indent_incr abs
 
 let get_instantiated_fun_sig (fun_id : A.fun_id)
-    (back_id : T.RegionGroupId.id option) (tys : ty list) (ctx : bs_ctx) :
-    inst_fun_sig =
+    (back_id : T.RegionGroupId.id option) (tys : ty list)
+    (cgs : const_generic list) (ctx : bs_ctx) : inst_fun_sig =
   (* Lookup the non-instantiated function signature *)
   let sg =
     (RegularFunIdNotLoopMap.find (fun_id, back_id) ctx.fun_context.fun_sigs).sg
   in
   (* Create the substitution *)
   let tsubst = make_type_subst sg.type_params tys in
+  let cgsubst = make_const_generic_subst sg.const_generic_params cgs in
   (* Apply *)
-  fun_sig_substitute tsubst sg
+  fun_sig_substitute tsubst cgsubst sg
 
 let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
     T.type_decl =
@@ -380,17 +393,17 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
 let rec translate_sty (ty : T.sty) : ty =
   let translate = translate_sty in
   match ty with
-  | T.Adt (type_id, regions, tys) -> (
+  | T.Adt (type_id, regions, tys, cgs) -> (
       (* Can't translate types with regions for now *)
       assert (regions = []);
       let tys = List.map translate tys in
       match type_id with
-      | T.AdtId adt_id -> Adt (AdtId adt_id, tys)
+      | T.AdtId adt_id -> Adt (AdtId adt_id, tys, cgs)
       | T.Tuple -> mk_simpl_tuple_ty tys
       | T.Assumed aty -> (
           match aty with
-          | T.Vec -> Adt (Assumed Vec, tys)
-          | T.Option -> Adt (Assumed Option, tys)
+          | T.Vec -> Adt (Assumed Vec, tys, cgs)
+          | T.Option -> Adt (Assumed Option, tys, cgs)
           | T.Box -> (
               (* Eliminate the boxes *)
               match tys with
@@ -399,15 +412,13 @@ let rec translate_sty (ty : T.sty) : ty =
                   raise
                     (Failure
                        "Box/vec/option type with incorrect number of arguments")
-              )))
+              )
+          | T.Array -> Adt (Assumed Array, tys, cgs)
+          | T.Slice -> Adt (Assumed Slice, tys, cgs)
+          | T.Str -> Adt (Assumed Str, tys, cgs)))
   | TypeVar vid -> TypeVar vid
-  | Bool -> Bool
-  | Char -> Char
+  | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
-  | Integer int_ty -> Integer int_ty
-  | Str -> Str
-  | Array ty -> Array (translate ty)
-  | Slice ty -> Slice (translate ty)
   | Ref (_, rty, _) -> translate rty
 
 let translate_field (f : T.field) : field =
@@ -445,8 +456,9 @@ let translate_type_decl (def : T.type_decl) : type_decl =
   (* Can't translate types with regions for now *)
   assert (def.region_params = []);
   let type_params = def.type_params in
+  let const_generic_params = def.const_generic_params in
   let kind = translate_type_decl_kind def.T.kind in
-  { def_id; name; type_params; kind }
+  { def_id; name; type_params; const_generic_params; kind }
 
 (** Translate a type, seen as an input/output of a forward function
     (preserve all borrows, etc.)
@@ -455,7 +467,7 @@ let translate_type_decl (def : T.type_decl) : type_decl =
 let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
-  | T.Adt (type_id, regions, tys) -> (
+  | T.Adt (type_id, regions, tys, cgs) -> (
       (* Can't translate types with regions for now *)
       assert (regions = []);
       (* Translate the type parameters *)
-- 
cgit v1.3.1


From 59ec03d37d2ad51cf77e456622703c4c84780f48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 11:46:09 +0200
Subject: Make progress

---
 compiler/InterpreterPaths.ml      |  21 ++--
 compiler/InterpreterStatements.ml |  92 ++++++++------
 compiler/PrintPure.ml             |   1 +
 compiler/Pure.ml                  |  10 +-
 compiler/SymbolicAst.ml           |   3 +
 compiler/SymbolicToPure.ml        | 249 ++++++++++++++++++++++----------------
 compiler/SynthesizeSymbolic.ml    |  20 +--
 7 files changed, 232 insertions(+), 164 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 4a439250..04dc8892 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -359,7 +359,8 @@ let write_place (access : access_kind) (p : E.place) (nv : V.typed_value)
 
 let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
     (def_id : T.TypeDeclId.id) (opt_variant_id : T.VariantId.id option)
-    (regions : T.erased_region list) (types : T.ety list) : V.typed_value =
+    (regions : T.erased_region list) (types : T.ety list)
+    (cgs : T.const_generic list) : V.typed_value =
   (* Lookup the definition and check if it is an enumeration - it
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
@@ -368,12 +369,12 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
   assert (List.length regions = List.length def.T.region_params);
   (* Compute the field types *)
   let field_types =
-    Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types
+    Subst.type_decl_get_instantiated_field_etypes def opt_variant_id types cgs
   in
   (* Initialize the expanded value *)
   let fields = List.map mk_bottom field_types in
   let av = V.Adt { variant_id = opt_variant_id; field_values = fields } in
-  let ty = T.Adt (T.AdtId def_id, regions, types) in
+  let ty = T.Adt (T.AdtId def_id, regions, types, cgs) in
   { V.value = av; V.ty }
 
 let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
@@ -386,7 +387,7 @@ let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
     else raise (Failure "Unreachable")
   in
   let av = V.Adt { variant_id = Some variant_id; field_values } in
-  let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ]) in
+  let ty = T.Adt (T.Assumed T.Option, [], [ param_ty ], []) in
   { V.value = av; ty }
 
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
@@ -394,7 +395,7 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
   (* Generate the field values *)
   let fields = List.map mk_bottom field_types in
   let v = V.Adt { variant_id = None; field_values = fields } in
-  let ty = T.Adt (T.Tuple, [], field_types) in
+  let ty = T.Adt (T.Tuple, [], field_types, []) in
   { V.value = v; V.ty }
 
 (** Auxiliary helper to expand {!V.Bottom} values.
@@ -446,16 +447,16 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
     match (pe, ty) with
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
-        T.Adt (T.AdtId def_id', regions, types) ) ->
+        T.Adt (T.AdtId def_id', regions, types, cgs) ) ->
         assert (def_id = def_id');
         compute_expanded_bottom_adt_value ctx.type_context.type_decls def_id
-          opt_variant_id regions types
+          opt_variant_id regions types cgs
     (* Option *)
-    | Field (ProjOption variant_id, _), T.Adt (T.Assumed T.Option, [], [ ty ])
-      ->
+    | ( Field (ProjOption variant_id, _),
+        T.Adt (T.Assumed T.Option, [], [ ty ], []) ) ->
         compute_expanded_bottom_option_value variant_id ty
     (* Tuples *)
-    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
+    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys, []) ->
         assert (arity = List.length tys);
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value tys
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index d181ca4b..cd5f8c3e 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -420,18 +420,20 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_replace_concrete (_config : C.config)
-    (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
-    =
+    (_region_params : T.erased_region list) (_type_params : T.ety list)
+    (_cg_params : T.const_generic list) : cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_new_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (cg_params : T.const_generic list) : cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
-  match (region_params, type_params, ctx.env) with
+  match (region_params, type_params, cg_params, ctx.env) with
   | ( [],
       [ boxed_ty ],
+      [],
       Var (VarBinder input_var, input_value)
       :: Var (_ret_var, _)
       :: C.Frame :: _ ) ->
@@ -468,12 +470,13 @@ let eval_box_new_concrete (config : C.config)
     and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *)
 let eval_box_deref_mut_or_shared_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
-    (is_mut : bool) : cm_fun =
+    (cg_params : T.const_generic list) (is_mut : bool) : cm_fun =
  fun cf ctx ->
   (* Check the arguments *)
-  match (region_params, type_params, ctx.env) with
+  match (region_params, type_params, cg_params, ctx.env) with
   | ( [],
       [ boxed_ty ],
+      [],
       Var (VarBinder input_var, input_value)
       :: Var (_ret_var, _)
       :: C.Frame :: _ ) ->
@@ -513,15 +516,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (cg_params : T.const_generic list) : cm_fun =
   let is_mut = false in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
+  eval_box_deref_mut_or_shared_concrete config region_params type_params
+    cg_params is_mut
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_mut_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (cg_params : T.const_generic list) : cm_fun =
   let is_mut = true in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
+  eval_box_deref_mut_or_shared_concrete config region_params type_params
+    cg_params is_mut
 
 (** Auxiliary function - see {!eval_non_local_function_call}.
 
@@ -543,11 +550,11 @@ let eval_box_deref_mut_concrete (config : C.config)
     the destination (by setting it to [()]).
 *)
 let eval_box_free (config : C.config) (region_params : T.erased_region list)
-    (type_params : T.ety list) (args : E.operand list) (dest : E.place) : cm_fun
-    =
+    (type_params : T.ety list) (cg_params : T.const_generic list)
+    (args : E.operand list) (dest : E.place) : cm_fun =
  fun cf ctx ->
-  match (region_params, type_params, args) with
-  | [], [ boxed_ty ], [ E.Move input_box_place ] ->
+  match (region_params, type_params, cg_params, args) with
+  | [], [ boxed_ty ], [], [ E.Move input_box_place ] ->
       (* Required type checking *)
       let input_box = InterpreterPaths.read_place Write input_box_place ctx in
       (let input_ty = ty_get_box input_box.V.ty in
@@ -565,15 +572,15 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
 
 (** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
-    (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
-    =
+    (_region_params : T.erased_region list) (_type_params : T.ety list)
+    (_cg_params : T.const_generic list) : cm_fun =
  fun _cf _ctx -> raise Unimplemented
 
 (** Evaluate a non-local function call in concrete mode *)
 let eval_non_local_function_call_concrete (config : C.config)
     (fid : A.assumed_fun_id) (region_params : T.erased_region list)
-    (type_params : T.ety list) (args : E.operand list) (dest : E.place) : cm_fun
-    =
+    (type_params : T.ety list) (cg_params : T.const_generic list)
+    (args : E.operand list) (dest : E.place) : cm_fun =
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
@@ -582,7 +589,7 @@ let eval_non_local_function_call_concrete (config : C.config)
   match fid with
   | A.BoxFree ->
       (* Degenerate case: box_free *)
-      eval_box_free config region_params type_params args dest
+      eval_box_free config region_params type_params cg_params args dest
   | _ ->
       (* "Normal" case: not box_free *)
       (* Evaluate the operands *)
@@ -605,6 +612,7 @@ let eval_non_local_function_call_concrete (config : C.config)
         let ret_vid = E.VarId.zero in
         let ret_ty =
           get_non_local_function_return_type fid region_params type_params
+            cg_params
         in
         let ret_var = mk_var ret_vid (Some "@return") ret_ty in
         let cc = comp cc (push_uninitialized_var ret_var) in
@@ -622,15 +630,25 @@ let eval_non_local_function_call_concrete (config : C.config)
          * access to a body. *)
         let cf_eval_body : cm_fun =
           match fid with
-          | A.Replace -> eval_replace_concrete config region_params type_params
-          | BoxNew -> eval_box_new_concrete config region_params type_params
-          | BoxDeref -> eval_box_deref_concrete config region_params type_params
+          | A.Replace ->
+              eval_replace_concrete config region_params type_params cg_params
+          | BoxNew ->
+              eval_box_new_concrete config region_params type_params cg_params
+          | BoxDeref ->
+              eval_box_deref_concrete config region_params type_params cg_params
           | BoxDerefMut ->
               eval_box_deref_mut_concrete config region_params type_params
+                cg_params
           | BoxFree ->
               (* Should have been treated above *) raise (Failure "Unreachable")
           | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
               eval_vec_function_concrete config fid region_params type_params
+                cg_params
+          | ArraySharedIndex | ArrayMutIndex | ArrayToSharedSlice
+          | ArrayToMutSlice | ArraySharedSubslice | ArrayMutSubslice
+          | SliceSharedIndex | SliceMutIndex | SliceSharedSubslice
+          | SliceMutSubslice ->
+              raise (Failure "Unimplemented")
         in
 
         let cc = comp cc cf_eval_body in
@@ -644,8 +662,8 @@ let eval_non_local_function_call_concrete (config : C.config)
       (* Compose and apply *)
       comp cf_eval_ops cf_eval_call
 
-let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
-    A.inst_fun_sig =
+let instantiate_fun_sig (type_params : T.ety list)
+    (cg_params : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
   (* Generate fresh abstraction ids and create a substitution from region
    * group ids to abstraction ids *)
   let rg_abs_ids_bindings =
@@ -674,13 +692,12 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
    * work to do to properly handle full type parametrization.
    * *)
   let rtype_params = List.map ety_no_regions_to_rty type_params in
-  let tsubst =
-    Subst.make_type_subst
-      (List.map (fun v -> v.T.index) sg.type_params)
-      rtype_params
+  let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in
+  let cgsubst =
+    Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_params
   in
   (* Substitute the signature *)
-  let inst_sig = Subst.substitute_signature asubst rsubst tsubst sg in
+  let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in
   (* Return *)
   inst_sig
 
@@ -912,7 +929,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         let cf_if (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Primitive (PV.Bool b) ->
+          | V.Literal (PV.Bool b) ->
               (* Evaluate the if and the branch body *)
               let cf_branch cf : m_fun =
                 (* Branch *)
@@ -940,7 +957,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         let cf_switch (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Primitive (PV.Scalar sv) ->
+          | V.Literal (PV.Scalar sv) ->
               (* Evaluate the branch *)
               let cf_eval_branch cf =
                 (* Sanity check *)
@@ -1035,7 +1052,8 @@ 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)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+    st_cm_fun =
  fun cf ctx ->
   assert (region_args = []);
 
@@ -1052,11 +1070,13 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
     | Some body -> body
   in
   let tsubst =
-    Subst.make_type_subst
-      (List.map (fun v -> v.T.index) def.A.signature.type_params)
-      type_args
+    Subst.make_type_subst_from_vars def.A.signature.type_params type_args
+  in
+  let cgsubst =
+    Subst.make_const_generic_subst_from_vars
+      def.A.signature.const_generic_params cg_args
   in
-  let locals, body_st = Subst.fun_body_substitute_in_body tsubst body in
+  let locals, body_st = Subst.fun_body_substitute_in_body tsubst cgsubst body in
 
   (* Evaluate the input operands *)
   assert (List.length args = body.A.arg_count);
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 6f857b4f..33a86df5 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -532,6 +532,7 @@ let unop_to_string (unop : unop) : string =
   | Cast (src, tgt) ->
       "cast<" ^ integer_type_to_string src ^ "," ^ integer_type_to_string tgt
       ^ ">"
+  | SliceNew tgt_len -> "array_to_slice<" ^ scalar_value_to_string tgt_len ^ ">"
 
 let binop_to_string = Print.Expressions.binop_to_string
 
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 9b5d9236..b90ef60a 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -197,8 +197,8 @@ type type_decl = {
 }
 [@@deriving show]
 
-type scalar_value = V.scalar_value [@@deriving show]
-type literal = V.literal [@@deriving show]
+type scalar_value = V.scalar_value [@@deriving show, ord]
+type literal = V.literal [@@deriving show, ord]
 
 (** Because we introduce a lot of temporary variables, the list of variables
     is not fixed: we thus must carry all its information with the variable
@@ -343,7 +343,11 @@ and typed_pattern = { value : pattern; ty : ty }
         polymorphic = false;
       }]
 
-type unop = Not | Neg of integer_type | Cast of integer_type * integer_type
+type unop =
+  | Not
+  | Neg of integer_type
+  | Cast of integer_type * integer_type
+  | SliceNew of scalar_value
 [@@deriving show, ord]
 
 (** Identifiers of assumed functions that we use only in the pure translation *)
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 0e68d2fd..787fefc7 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -43,7 +43,10 @@ type call = {
           borrows (we need to perform lookups).
        *)
   abstractions : V.AbstractionId.id list;
+  (* TODO: rename to "...args" *)
   type_params : T.ety list;
+  (* TODO: rename to "...args" *)
+  const_generic_params : T.const_generic list;
   args : V.typed_value list;
   args_places : mplace option list;  (** Meta information *)
   dest : V.symbolic_value;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ba2a6525..a6d2784b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -107,6 +107,7 @@ type loop_info = {
   input_vars : var list;
   input_svl : V.symbolic_value list;
   type_args : ty list;
+  const_generic_args : const_generic list;
   forward_inputs : texpression list option;
       (** The forward inputs are initialized at [None] *)
   forward_output_no_state_no_result : var option;
@@ -460,10 +461,28 @@ let translate_type_decl (def : T.type_decl) : type_decl =
   let kind = translate_type_decl_kind def.T.kind in
   { def_id; name; type_params; const_generic_params; kind }
 
+let translate_type_id (id : T.type_id) : type_id =
+  match id with
+  | AdtId adt_id -> AdtId adt_id
+  | T.Assumed aty ->
+      let aty =
+        match aty with
+        | T.Vec -> Vec
+        | T.Option -> Option
+        | T.Array -> Array
+        | T.Slice -> Slice
+        | T.Str -> Str
+        | T.Box ->
+            (* Boxes have to be eliminated: this type id shouldn't
+               be translated *)
+            raise (Failure "Unreachable")
+      in
+      Assumed aty
+  | T.Tuple -> Tuple
+
 (** Translate a type, seen as an input/output of a forward function
     (preserve all borrows, etc.)
 *)
-
 let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
   let translate = translate_fwd_ty type_infos in
   match ty with
@@ -474,17 +493,11 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       let t_tys = List.map translate tys in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.Assumed (T.Vec | T.Option) ->
+      | AdtId _ | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
           (* No general parametricity for now *)
           assert (not (List.exists (TypesUtils.ty_has_borrows type_infos) tys));
-          let type_id =
-            match type_id with
-            | AdtId adt_id -> AdtId adt_id
-            | T.Assumed T.Vec -> Assumed Vec
-            | T.Assumed T.Option -> Assumed Option
-            | _ -> raise (Failure "Unreachable")
-          in
-          Adt (type_id, t_tys)
+          let type_id = translate_type_id type_id in
+          Adt (type_id, t_tys, cgs)
       | Tuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
@@ -501,17 +514,8 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
                    "Unreachable: box/vec/option receives exactly one type \
                     parameter")))
   | TypeVar vid -> TypeVar vid
-  | Bool -> Bool
-  | Char -> Char
   | Never -> raise (Failure "Unreachable")
-  | Integer int_ty -> Integer int_ty
-  | Str -> Str
-  | Array ty ->
-      assert (not (TypesUtils.ty_has_borrows type_infos ty));
-      Array (translate ty)
-  | Slice ty ->
-      assert (not (TypesUtils.ty_has_borrows type_infos ty));
-      Slice (translate ty)
+  | Literal lty -> Literal lty
   | Ref (_, rty, _) -> translate rty
 
 (** Simply calls [translate_fwd_ty] *)
@@ -531,21 +535,15 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   (* A small helper for "leave" types *)
   let wrap ty = if inside_mut then Some ty else None in
   match ty with
-  | T.Adt (type_id, _, tys) -> (
+  | T.Adt (type_id, _, tys, cgs) -> (
       match type_id with
-      | T.AdtId _ | Assumed (T.Vec | T.Option) ->
+      | T.AdtId _ | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
-          let type_id =
-            match type_id with
-            | T.AdtId id -> AdtId id
-            | T.Assumed T.Vec -> Assumed Vec
-            | T.Assumed T.Option -> Assumed Option
-            | T.Tuple | T.Assumed T.Box -> raise (Failure "Unreachable")
-          in
+          let type_id = translate_type_id type_id in
           if inside_mut then
             let tys_t = List.filter_map translate tys in
-            Some (Adt (type_id, tys_t))
+            Some (Adt (type_id, tys_t, cgs))
           else None
       | Assumed T.Box -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
@@ -567,17 +565,8 @@ let rec translate_back_ty (type_infos : TA.type_infos)
                * is the identity *)
               Some (mk_simpl_tuple_ty tys_t)))
   | TypeVar vid -> wrap (TypeVar vid)
-  | Bool -> wrap Bool
-  | Char -> wrap Char
   | Never -> raise (Failure "Unreachable")
-  | Integer int_ty -> wrap (Integer int_ty)
-  | Str -> wrap Str
-  | Array ty -> (
-      assert (not (TypesUtils.ty_has_borrows type_infos ty));
-      match translate ty with None -> None | Some ty -> Some (Array ty))
-  | Slice ty -> (
-      assert (not (TypesUtils.ty_has_borrows type_infos ty));
-      match translate ty with None -> None | Some ty -> Some (Slice ty))
+  | Literal lty -> wrap (Literal lty)
   | Ref (r, rty, rkind) -> (
       match rkind with
       | T.Shared ->
@@ -813,8 +802,9 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     (* Wrap in a result type *)
     if effect_info.can_fail then mk_result_ty output else output
   in
-  (* Type parameters *)
+  (* Type/const generic parameters *)
   let type_params = sg.type_params in
+  let const_generic_params = sg.const_generic_params in
   (* Return *)
   let has_fuel = fuel <> [] in
   let num_fwd_inputs_no_state = List.length fwd_inputs in
@@ -842,7 +832,9 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
       effect_info;
     }
   in
-  let sg = { type_params; inputs; output; doutputs; info } in
+  let sg =
+    { type_params; const_generic_params; inputs; output; doutputs; info }
+  in
   { sg; output_names }
 
 let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern =
@@ -921,7 +913,7 @@ let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
 (** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
   match (v.value, v.ty) with
-  | V.Adt av, T.Adt (T.Assumed T.Box, _, _) -> (
+  | V.Adt av, T.Adt (T.Assumed T.Box, _, _, _) -> (
       match av.field_values with
       | [ bv ] -> unbox_typed_value bv
       | _ -> raise (Failure "Unreachable"))
@@ -960,26 +952,22 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
   (* Translate the value *)
   let value =
     match v.value with
-    | V.Primitive cv -> { e = Const cv; ty }
+    | V.Literal cv -> { e = Const cv; ty }
     | Adt av -> (
         let variant_id = av.variant_id in
         let field_values = List.map translate av.field_values in
         (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
         match v.ty with
-        | T.Adt (T.Tuple, _, _) ->
+        | T.Adt (T.Tuple, _, _, _) ->
             assert (variant_id = None);
             mk_simpl_tuple_texpression field_values
         | _ ->
-            (* Retrieve the type and the translated type arguments from the
-             * translated type (simpler this way) *)
-            let adt_id, type_args =
-              match ty with
-              | Adt (type_id, tys) -> (type_id, tys)
-              | _ -> raise (Failure "Unreachable")
-            in
+            (* Retrieve the type, the translated type arguments and the
+             * const generic arguments from the translated type (simpler this way) *)
+            let adt_id, type_args, const_generic_args = ty_as_adt ty in
             (* Create the constructor *)
             let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
-            let qualif = { id = qualif_id; type_args } in
+            let qualif = { id = qualif_id; type_args; const_generic_args } in
             let cons_e = Qualif qualif in
             let field_tys =
               List.map (fun (v : texpression) -> v.ty) field_values
@@ -1046,9 +1034,10 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* Translate the field values *)
         let field_values = List.filter_map translate adt_v.field_values in
         (* For now, only tuples can contain borrows *)
-        let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
+        let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Vec | T.Option) ->
+        | T.AdtId _
+        | T.Assumed (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1189,11 +1178,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
         in
         let field_values = List.filter_map (fun x -> x) field_values in
         (* For now, only tuples can contain borrows - note that if we gave
-         * something like a [&mut Vec] to a function, we give give back the
+         * something like a [&mut Vec] to a function, we give back the
          * vector value upon visiting the "abstraction borrow" node *)
-        let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
+        let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _ | T.Assumed (T.Box | T.Vec | T.Option) ->
+        | T.AdtId _
+        | T.Assumed (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -1463,6 +1453,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   (* Translate the function call *)
   let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
+  let const_generic_args = call.const_generic_params in
   let args =
     let args = List.map (typed_value_to_texpression ctx call.ctx) call.args in
     let args_mplaces = List.map translate_opt_mplace call.args_places in
@@ -1540,6 +1531,19 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           }
         in
         (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
+    | S.Unop (E.SliceNew tgt_len) ->
+        (* The cast can fail if the length of the source array is not
+           big enough *)
+        let effect_info =
+          {
+            can_fail = true;
+            stateful_group = false;
+            stateful = false;
+            can_diverge = false;
+            is_rec = false;
+          }
+        in
+        (ctx, Unop (SliceNew tgt_len), effect_info, args, None)
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->
@@ -1564,7 +1568,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
     | None -> dest
     | Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
   in
-  let func = { id = FunOrOp fun_id; type_args } in
+  let func = { id = FunOrOp fun_id; type_args; const_generic_args } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
   let ret_ty =
     if effect_info.can_fail then mk_result_ty dest_v.ty else dest_v.ty
@@ -1625,13 +1629,13 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
    *   to the backward function, and which consumed the values [consumed_i],
    *   we introduce:
    *   {[
-         *   let v_i = consumed_i in
-         *   ...
-   *   ]}
+       *   let v_i = consumed_i in
+       *   ...
+         *   ]}
    *   Then, when we reach the [Return] node, we introduce:
    *   {[
-         *   (v_i)
-   *   ]}
+       *   (v_i)
+       *   ]}
    * *)
   (* First, get the given back variables.
 
@@ -1696,6 +1700,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     get_fun_effect_info ctx.fun_context.fun_infos fun_id None (Some rg_id)
   in
   let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
+  let const_generic_args = call.const_generic_params in
   (* Retrieve the original call and the parent abstractions *)
   let _forward, backwards = get_abs_ancestors ctx abs call_id in
   (* Retrieve the values consumed when we called the forward function and
@@ -1744,7 +1749,10 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
   in
   (* Sanity check: there is the proper number of inputs and outputs, and they have the proper type *)
   let _ =
-    let inst_sg = get_instantiated_fun_sig fun_id (Some rg_id) type_args ctx in
+    let inst_sg =
+      get_instantiated_fun_sig fun_id (Some rg_id) type_args const_generic_args
+        ctx
+    in
     log#ldebug
       (lazy
         ("\n- fun_id: " ^ A.show_fun_id fun_id ^ "\n- inputs ("
@@ -1787,7 +1795,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
     if effect_info.can_fail then mk_result_ty output.ty else output.ty
   in
   let func_ty = mk_arrows input_tys ret_ty in
-  let func = { id = FunOrOp func; type_args } in
+  let func = { id = FunOrOp func; type_args; const_generic_args } in
   let func = { e = Qualif func; ty = func_ty } in
   let call = mk_apps func args in
   (* **Optimization**:
@@ -1850,7 +1858,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
      {[
        let id_back x nx =
          let s = nx in // the name [s] is not important (only collision matters)
-         ...
+                                                        ...
      ]}
 
      This let-binding later gets inlined, during a micro-pass.
@@ -1911,6 +1919,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       in
       let loop_info = LoopId.Map.find loop_id ctx.loops in
       let type_args = loop_info.type_args in
+      let const_generic_args = loop_info.const_generic_args in
       let fwd_inputs = Option.get loop_info.forward_inputs in
       (* Retrieve the additional backward inputs. Note that those are actually
          the backward inputs of the function we are synthesizing (and that we
@@ -1959,7 +1968,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
       in
       let func_ty = mk_arrows input_tys ret_ty in
       let func = Fun (FromLlbc (fun_id, Some loop_id, Some rg_id)) in
-      let func = { id = FunOrOp func; type_args } in
+      let func = { id = FunOrOp func; type_args; const_generic_args } in
       let func = { e = Qualif func; ty = func_ty } in
       let call = mk_apps func args in
       (* **Optimization**:
@@ -2019,7 +2028,9 @@ and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
     (e : S.expression) (ctx : bs_ctx) : texpression =
   let ctx, var = fresh_var_for_symbolic_value sval ctx in
   let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
-  let global_expr = { id = Global gid; type_args = [] } in
+  let global_expr =
+    { id = Global gid; type_args = []; const_generic_args = [] }
+  in
   (* We use translate_fwd_ty to translate the global type *)
   let ty = ctx_translate_fwd_ty ctx decl.ty in
   let gval = { e = Qualif global_expr; ty } in
@@ -2032,8 +2043,14 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   let monadic = true in
   let v = typed_value_to_texpression ctx ectx v in
   let args = [ v ] in
-  let func = { id = FunOrOp (Fun (Pure Assert)); type_args = [] } in
-  let func_ty = mk_arrow Bool mk_unit_ty in
+  let func =
+    {
+      id = FunOrOp (Fun (Pure Assert));
+      type_args = [];
+      const_generic_args = [];
+    }
+  in
+  let func_ty = mk_arrow (Literal Bool) mk_unit_ty in
   let func = { e = Qualif func; ty = func_ty } in
   let assertion = mk_apps func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e
@@ -2048,13 +2065,13 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
   match exp with
   | ExpandNoBranch (sexp, e) -> (
       match sexp with
-      | V.SePrimitive _ ->
-          (* Actually, we don't *register* symbolic expansions to constant
-           * values in the symbolic ADT *)
+      | V.SeLiteral _ ->
+          (* We do not *register* symbolic expansions to literal
+                   * values in the symbolic ADT *)
           raise (Failure "Unreachable")
       | SeMutRef (_, nsv) | SeSharedRef (_, nsv) ->
           (* The (mut/shared) borrow type is extracted to identity: we thus simply
-           * introduce an reassignment *)
+                   * introduce an reassignment *)
           let ctx, var = fresh_var_for_symbolic_value nsv ctx in
           let next_e = translate_expression e ctx in
           let monadic = false in
@@ -2075,10 +2092,10 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
                && !Config.always_deconstruct_adts_with_matches) ->
           (* There is exactly one branch: no branching.
 
-             We can decompose the ADT value with a let-binding, unless
-             the backend doesn't support this (see {!Config.always_deconstruct_adts_with_matches}):
-             we *ignore* this branch (and go to the next one) if the ADT is a custom
-             adt, and [always_deconstruct_adts_with_matches] is true.
+                     We can decompose the ADT value with a let-binding, unless
+                     the backend doesn't support this (see {!Config.always_deconstruct_adts_with_matches}):
+                     we *ignore* this branch (and go to the next one) if the ADT is a custom
+                     adt, and [always_deconstruct_adts_with_matches] is true.
           *)
           translate_ExpandAdt_one_branch sv scrutinee scrutinee_mplace
             variant_id svl branch ctx
@@ -2127,14 +2144,14 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
       let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
           match_branch =
         (* We don't need to update the context: we don't introduce any
-         * new values/variables *)
+           * new values/variables *)
         let branch = translate_expression branch_e ctx in
-        let pat = mk_typed_pattern_from_primitive_value (PV.Scalar v) in
+        let pat = mk_typed_pattern_from_literal (PV.Scalar v) in
         { pat; branch }
       in
       let branches = List.map translate_branch branches in
       let otherwise = translate_expression otherwise ctx in
-      let pat_ty = Integer int_ty in
+      let pat_ty = Literal (Integer int_ty) in
       let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in
       let otherwise : match_branch =
         { pat = otherwise_pat; branch = otherwise }
@@ -2154,18 +2171,18 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
 
    There are several possibilities:
    - if the ADT is an enumeration, we attempt to deconstruct it with a let-binding:
-     {[
-       let Cons x0 ... xn = y in
-       ...
-     ]}
+   {[
+     let Cons x0 ... xn = y in
+     ...
+   ]}
 
    - if the ADT is a structure, we attempt to introduce one let-binding per field:
-     {[
-       let x0 = y.f0 in
-       ...
+   {[
+     let x0 = y.f0 in
+     ...
        let xn = y.fn in
        ...
-     ]}
+   ]}
 
    Of course, this is not always possible depending on the backend.
    Also, recursive structures, and more specifically structures mutually recursive
@@ -2179,14 +2196,14 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
     (branch : S.expression) (ctx : bs_ctx) : texpression =
   (* TODO: always introduce a match, and use micro-passes to turn the
      the match into a let? *)
-  let type_id, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
+  let type_id, _, _, _ = TypesUtils.ty_as_adt sv.V.sv_ty in
   let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
   let branch = translate_expression branch ctx in
   match type_id with
   | T.AdtId adt_id ->
       (* Detect if this is an enumeration or not *)
       let tdef = bs_ctx_lookup_llbc_type_decl adt_id ctx in
-      let is_enum = type_decl_is_enum tdef in
+      let is_enum = TypesUtils.type_decl_is_enum tdef in
       (* We deconstruct the ADT with a let-binding in two situations:
          - if the ADT is an enumeration (which must have exactly one branch)
          - if we forbid using field projectors.
@@ -2214,14 +2231,10 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          * field.
          * We use the [dest] variable in order not to have to recompute
          * the type of the result of the projection... *)
-        let adt_id, type_args =
-          match scrutinee.ty with
-          | Adt (adt_id, tys) -> (adt_id, tys)
-          | _ -> raise (Failure "Unreachable")
-        in
+        let adt_id, type_args, const_generic_args = ty_as_adt scrutinee.ty in
         let gen_field_proj (field_id : FieldId.id) (dest : var) : texpression =
           let proj_kind = { adt_id; field_id } in
-          let qualif = { id = Proj proj_kind; type_args } in
+          let qualif = { id = Proj proj_kind; type_args; const_generic_args } in
           let proj_e = Qualif qualif in
           let proj_ty = mk_arrow scrutinee.ty dest.ty in
           let proj = { e = proj_e; ty = proj_ty } in
@@ -2253,12 +2266,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed T.Vec ->
-      (* We can't expand vector values: we can access the fields only
+  | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) ->
+      (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
-       * know how to expand a vector, because it has a variable number
+       * know how to expand values like vectors or arrays, because they have a variable number
        * of fields!) *)
-      raise (Failure "Can't expand a vector value")
+      raise (Failure "Attempt to expand a non-expandable value")
   | T.Assumed T.Option ->
       (* We shouldn't get there in the "one-branch" case: options have
        * two variants *)
@@ -2394,7 +2407,13 @@ and translate_forward_end (ectx : C.eval_ctx)
 
       let loop_call =
         let fun_id = Fun (FromLlbc (fid, Some loop_id, None)) in
-        let func = { id = FunOrOp fun_id; type_args = loop_info.type_args } in
+        let func =
+          {
+            id = FunOrOp fun_id;
+            type_args = loop_info.type_args;
+            const_generic_args = loop_info.const_generic_args;
+          }
+        in
         let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
         let ret_ty =
           if effect_info.can_fail then mk_result_ty out_pat.ty else out_pat.ty
@@ -2515,7 +2534,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
        (and will introduce the outputs at that moment, together with the actual
        call to the loop forward function *)
     let type_args =
-      List.map (fun ty -> TypeVar ty.T.index) ctx.sg.type_params
+      List.map (fun (ty : T.type_var) -> TypeVar ty.T.index) ctx.sg.type_params
+    in
+    let const_generic_args =
+      List.map
+        (fun (cg : T.const_generic_var) -> T.ConstGenericVar cg.T.index)
+        ctx.sg.const_generic_params
     in
 
     let loop_info =
@@ -2524,6 +2548,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         input_vars = inputs;
         input_svl = loop.input_svalues;
         type_args;
+        const_generic_args;
         forward_inputs = None;
         forward_output_no_state_no_result = None;
       }
@@ -2611,14 +2636,26 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression)
       *)
       (* Create the expression: [fuel0 = 0] *)
       let check_fuel =
-        let func = { id = FunOrOp (Fun (Pure FuelEqZero)); type_args = [] } in
+        let func =
+          {
+            id = FunOrOp (Fun (Pure FuelEqZero));
+            type_args = [];
+            const_generic_args = [];
+          }
+        in
         let func_ty = mk_arrow mk_fuel_ty mk_bool_ty in
         let func = { e = Qualif func; ty = func_ty } in
         mk_app func fuel0
       in
       (* Create the expression: [decrease fuel0] *)
       let decrease_fuel =
-        let func = { id = FunOrOp (Fun (Pure FuelDecrease)); type_args = [] } in
+        let func =
+          {
+            id = FunOrOp (Fun (Pure FuelDecrease));
+            type_args = [];
+            const_generic_args = [];
+          }
+        in
         let func_ty = mk_arrow mk_fuel_ty mk_fuel_ty in
         let func = { e = Qualif func; ty = func_ty } in
         mk_app func fuel0
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index e2cdc726..857fea97 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -98,9 +98,9 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
 
 let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
     (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
-    (args : V.typed_value list) (args_places : mplace option list)
-    (dest : V.symbolic_value) (dest_place : mplace option)
-    (e : expression option) : expression option =
+    (const_generic_params : T.const_generic list) (args : V.typed_value list)
+    (args_places : mplace option list) (dest : V.symbolic_value)
+    (dest_place : mplace option) (e : expression option) : expression option =
   Option.map
     (fun e ->
       let call =
@@ -109,6 +109,7 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
           ctx;
           abstractions;
           type_params;
+          const_generic_params;
           args;
           dest;
           args_places;
@@ -125,24 +126,25 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
 let synthesize_regular_function_call (fun_id : A.fun_id)
     (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx)
     (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
-    (args : V.typed_value list) (args_places : mplace option list)
-    (dest : V.symbolic_value) (dest_place : mplace option)
-    (e : expression option) : expression option =
+    (const_generic_params : T.const_generic list) (args : V.typed_value list)
+    (args_places : mplace option list) (dest : V.symbolic_value)
+    (dest_place : mplace option) (e : expression option) : expression option =
   synthesize_function_call
     (Fun (fun_id, call_id))
-    ctx abstractions type_params args args_places dest dest_place e
+    ctx abstractions type_params const_generic_params args args_places dest
+    dest_place e
 
 let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop)
     (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
-  synthesize_function_call (Unop unop) ctx [] [] [ arg ] [ arg_place ] dest
+  synthesize_function_call (Unop unop) ctx [] [] [] [ arg ] [ arg_place ] dest
     dest_place e
 
 let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop)
     (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value)
     (arg1_place : mplace option) (dest : V.symbolic_value)
     (dest_place : mplace option) (e : expression option) : expression option =
-  synthesize_function_call (Binop binop) ctx [] [] [ arg0; arg1 ]
+  synthesize_function_call (Binop binop) ctx [] [] [] [ arg0; arg1 ]
     [ arg0_place; arg1_place ] dest dest_place e
 
 let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs)
-- 
cgit v1.3.1


From a1e24c2a13713b015abc9a93e6915b6d4a6f22fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 14:10:15 +0200
Subject: Make progress

---
 compiler/ExtractBase.ml            | 13 +++---
 compiler/InterpreterExpansion.ml   |  3 +-
 compiler/InterpreterExpressions.ml | 86 ++++++++++++++++++++++++++------------
 compiler/InterpreterStatements.ml  | 49 ++++++++++++----------
 compiler/PrimitiveValuesUtils.ml   |  1 +
 compiler/PrintPure.ml              | 15 ++++++-
 compiler/Pure.ml                   |  1 +
 compiler/PureMicroPasses.ml        | 46 ++++++++++++++++----
 compiler/PureTypeCheck.ml          |  6 ++-
 compiler/Substitute.ml             |  5 +++
 compiler/SymbolicToPure.ml         | 17 +++++---
 compiler/TypesAnalysis.ml          |  6 ++-
 compiler/ValuesUtils.ml            |  1 +
 compiler/dune                      |  5 ++-
 14 files changed, 178 insertions(+), 76 deletions(-)
 create mode 100644 compiler/PrimitiveValuesUtils.ml

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 655bb033..bff6a360 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -292,7 +292,7 @@ type formatter = {
           indices to names, the responsability of finding a proper index is
           delegated to helper functions.
        *)
-  extract_primitive_value : F.formatter -> bool -> primitive_value -> unit;
+  extract_literal : F.formatter -> bool -> literal -> unit;
       (** Format a constant value.
 
           Inputs:
@@ -674,7 +674,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             if variant_id = option_some_id then "@option::Some"
             else if variant_id = option_none_id then "@option::None"
             else raise (Failure "Unreachable")
-        | Assumed (State | Vec | Fuel) -> raise (Failure "Unreachable")
+        | Assumed (State | Vec | Fuel | Array | Slice | Str | Range) ->
+            raise (Failure "Unreachable")
         | AdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
             match def.kind with
@@ -688,10 +689,10 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let field_name =
         match id with
         | Tuple -> raise (Failure "Unreachable")
-        | Assumed (State | Result | Error | Fuel | Option) ->
-            raise (Failure "Unreachable")
-        | Assumed Vec ->
-            (* We can't directly have access to the fields of a vector *)
+        | Assumed
+            ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str
+            | Range ) ->
+            (* We can't directly have access to the fields of those types *)
             raise (Failure "Unreachable")
         | AdtId id -> (
             let def = TypeDeclId.Map.find id type_decls in
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 3b196571..81e73e3e 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -707,7 +707,8 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
         | T.Adt ((Tuple | Assumed Box), _, _, _) | T.Ref (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config sv None
-        | T.Adt (Assumed (Vec | Option | Array | Slice | Str), _, _, _) ->
+        | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _, _, _)
+          ->
             (* We can't expand those *)
             raise
               (Failure
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index bb159f05..c3ff8d4f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -232,7 +232,7 @@ let prepare_eval_operand_reorganize (config : C.config) (op : E.operand) :
     match op with
     | Expressions.Constant (ty, cv) ->
         (* No need to reorganize the context *)
-        literal_to_typed_value ty cv |> ignore;
+        literal_to_typed_value (TypesUtils.ty_as_literal ty) cv |> ignore;
         cf ctx
     | Expressions.Copy p ->
         (* Access the value *)
@@ -260,7 +260,8 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
      ^ "\n- ctx:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Evaluate *)
   match op with
-  | Expressions.Constant (ty, cv) -> cf (literal_to_typed_value ty cv) ctx
+  | Expressions.Constant (ty, cv) ->
+      cf (literal_to_typed_value (TypesUtils.ty_as_literal ty) cv) ctx
   | Expressions.Copy p ->
       (* Access the value *)
       let access = Read in
@@ -350,21 +351,21 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
   (* Apply the unop *)
   let apply cf (v : V.typed_value) : m_fun =
     match (unop, v.V.value) with
-    | E.Not, V.Primitive (Bool b) ->
-        cf (Ok { v with V.value = V.Primitive (Bool (not b)) })
-    | E.Neg, V.Primitive (PV.Scalar sv) -> (
+    | E.Not, V.Literal (Bool b) ->
+        cf (Ok { v with V.value = V.Literal (Bool (not b)) })
+    | E.Neg, V.Literal (PV.Scalar sv) -> (
         let i = Z.neg sv.PV.value in
         match mk_scalar sv.int_ty i with
         | Error _ -> cf (Error EPanic)
-        | Ok sv -> cf (Ok { v with V.value = V.Primitive (PV.Scalar sv) }))
-    | E.Cast (src_ty, tgt_ty), V.Primitive (PV.Scalar sv) -> (
+        | Ok sv -> cf (Ok { v with V.value = V.Literal (PV.Scalar sv) }))
+    | E.Cast (src_ty, tgt_ty), V.Literal (PV.Scalar sv) -> (
         assert (src_ty = sv.int_ty);
         let i = sv.PV.value in
         match mk_scalar tgt_ty i with
         | Error _ -> cf (Error EPanic)
         | Ok sv ->
-            let ty = T.Integer tgt_ty in
-            let value = V.Primitive (PV.Scalar sv) in
+            let ty = T.Literal (Integer tgt_ty) in
+            let value = V.Literal (PV.Scalar sv) in
             cf (Ok { V.ty; value }))
     | _ -> raise (Failure "Invalid input for unop")
   in
@@ -381,9 +382,9 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
     let res_sv_id = C.fresh_symbolic_value_id () in
     let res_sv_ty =
       match (unop, v.V.ty) with
-      | E.Not, T.Bool -> T.Bool
-      | E.Neg, T.Integer int_ty -> T.Integer int_ty
-      | E.Cast (_, tgt_ty), _ -> T.Integer tgt_ty
+      | E.Not, (T.Literal Bool as lty) -> lty
+      | E.Neg, (T.Literal (Integer _) as lty) -> lty
+      | E.Cast (_, tgt_ty), _ -> T.Literal (Integer tgt_ty)
       | _ -> raise (Failure "Invalid input for unop")
     in
     let res_sv =
@@ -418,11 +419,11 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
     (* Equality/inequality check is primitive only for a subset of types *)
     assert (ty_is_primitively_copyable v1.ty);
     let b = v1 = v2 in
-    Ok { V.value = V.Primitive (Bool b); ty = T.Bool })
+    Ok { V.value = V.Literal (Bool b); ty = T.Literal Bool })
   else
     (* For the non-equality operations, the input values are necessarily scalars *)
     match (v1.V.value, v2.V.value) with
-    | V.Primitive (PV.Scalar sv1), V.Primitive (PV.Scalar sv2) -> (
+    | V.Literal (PV.Scalar sv1), V.Literal (PV.Scalar sv2) -> (
         (* There are binops which require the two operands to have the same
            type, and binops for which it is not the case.
            There are also binops which return booleans, and binops which
@@ -442,7 +443,9 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
               | E.BitOr | E.Shl | E.Shr | E.Ne | E.Eq ->
                   raise (Failure "Unreachable")
             in
-            Ok ({ V.value = V.Primitive (Bool b); ty = T.Bool } : V.typed_value)
+            Ok
+              ({ V.value = V.Literal (Bool b); ty = T.Literal Bool }
+                : V.typed_value)
         | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd | E.BitOr
           -> (
             (* The two operands must have the same type and the result is an integer *)
@@ -470,8 +473,8 @@ let eval_binary_op_concrete_compute (binop : E.binop) (v1 : V.typed_value)
             | Ok sv ->
                 Ok
                   {
-                    V.value = V.Primitive (PV.Scalar sv);
-                    ty = Integer sv1.int_ty;
+                    V.value = V.Literal (PV.Scalar sv);
+                    ty = T.Literal (Integer sv1.int_ty);
                   })
         | E.Shl | E.Shr -> raise Unimplemented
         | E.Ne | E.Eq -> raise (Failure "Unreachable"))
@@ -507,19 +510,19 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
         assert (v1.ty = v2.ty);
         (* Equality/inequality check is primitive only for a subset of types *)
         assert (ty_is_primitively_copyable v1.ty);
-        T.Bool)
+        T.Literal Bool)
       else
         (* Other operations: input types are integers *)
         match (v1.V.ty, v2.V.ty) with
-        | T.Integer int_ty1, T.Integer int_ty2 -> (
+        | T.Literal (Integer int_ty1), T.Literal (Integer int_ty2) -> (
             match binop with
             | E.Lt | E.Le | E.Ge | E.Gt ->
                 assert (int_ty1 = int_ty2);
-                T.Bool
+                T.Literal Bool
             | E.Div | E.Rem | E.Add | E.Sub | E.Mul | E.BitXor | E.BitAnd
             | E.BitOr ->
                 assert (int_ty1 = int_ty2);
-                T.Integer int_ty1
+                T.Literal (Integer int_ty1)
             | E.Shl | E.Shr -> raise Unimplemented
             | E.Ne | E.Eq -> raise (Failure "Unreachable"))
         | _ -> raise (Failure "Invalid inputs for binop")
@@ -653,7 +656,7 @@ let eval_rvalue_aggregate (config : C.config)
     | E.AggregatedTuple ->
         let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
         let v = V.Adt { variant_id = None; field_values = values } in
-        let ty = T.Adt (T.Tuple, [], tys) in
+        let ty = T.Adt (T.Tuple, [], tys, []) in
         let aggregated : V.typed_value = { V.value = v; ty } in
         (* Call the continuation *)
         cf aggregated ctx
@@ -664,20 +667,20 @@ let eval_rvalue_aggregate (config : C.config)
           assert (List.length values = 1)
         else raise (Failure "Unreachable");
         (* Construt the value *)
-        let aty = T.Adt (T.Assumed T.Option, [], [ ty ]) in
+        let aty = T.Adt (T.Assumed T.Option, [], [ ty ], []) in
         let av : V.adt_value =
           { V.variant_id = Some variant_id; V.field_values = values }
         in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
-    | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
+    | E.AggregatedAdt (def_id, opt_variant_id, regions, types, cgs) ->
         (* Sanity checks *)
         let type_decl = C.ctx_lookup_type_decl ctx def_id in
         assert (List.length type_decl.region_params = List.length regions);
         let expected_field_types =
           Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
-            types
+            types cgs
         in
         assert (
           expected_field_types
@@ -686,10 +689,41 @@ let eval_rvalue_aggregate (config : C.config)
         let av : V.adt_value =
           { V.variant_id = opt_variant_id; V.field_values = values }
         in
-        let aty = T.Adt (T.AdtId def_id, regions, types) in
+        let aty = T.Adt (T.AdtId def_id, regions, types, cgs) in
         let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
         (* Call the continuation *)
         cf aggregated ctx
+    | E.AggregatedRange ety ->
+        (* There should be two fields exactly *)
+        let v0, v1 =
+          match values with
+          | [ v0; v1 ] -> (v0, v1)
+          | _ -> raise (Failure "Unreachable")
+        in
+        (* Ranges are parametric over the type of indices. For now we only
+           support scalars, which can be of any type *)
+        assert (literal_type_is_integer (ty_as_literal ety));
+        assert (v0.ty = ety);
+        assert (v1.ty = ety);
+        (* Construct the value *)
+        let av : V.adt_value =
+          { V.variant_id = None; V.field_values = values }
+        in
+        let aty = T.Adt (T.Assumed T.Range, [], [ ety ], []) in
+        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+        (* Call the continuation *)
+        cf aggregated ctx
+    | 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);
+        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
+        (* Call the continuation *)
+        cf aggregated ctx
   in
   (* Compose and apply *)
   comp eval_ops compute cf
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index cd5f8c3e..79fe79e7 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -893,7 +893,7 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      (eval_local_function_call_concrete config global.body_id [] [] [] dest)
+      (eval_local_function_call_concrete config global.body_id [] [] [] [] dest)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
@@ -1044,10 +1044,10 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
   match call.func with
   | A.Regular fid ->
       eval_local_function_call config fid call.region_args call.type_args
-        call.args call.dest
+        call.const_generic_args call.args call.dest
   | A.Assumed fid ->
       eval_non_local_function_call config fid call.region_args call.type_args
-        call.args call.dest
+        call.const_generic_args call.args call.dest
 
 (** 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)
@@ -1135,19 +1135,20 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
 and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+    st_cm_fun =
  fun cf ctx ->
   (* Retrieve the (correctly instantiated) signature *)
   let def = C.ctx_lookup_fun_decl ctx fid in
   let sg = def.A.signature in
   (* Instantiate the signature and introduce fresh abstraction and region ids
    * while doing so *)
-  let inst_sg = instantiate_fun_sig type_args sg in
+  let inst_sg = instantiate_fun_sig type_args cg_args sg in
   (* Sanity check *)
   assert (List.length args = List.length def.A.signature.inputs);
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
-    region_args type_args args dest cf ctx
+    region_args type_args cg_args args dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1157,7 +1158,8 @@ 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)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (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 *)
@@ -1225,8 +1227,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     let expr = cf ctx in
 
     (* Synthesize the symbolic AST *)
-    S.synthesize_regular_function_call fid call_id ctx abs_ids type_args args
-      args_places ret_spc dest_place expr
+    S.synthesize_regular_function_call fid call_id ctx abs_ids type_args cg_args
+      args args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
 
@@ -1289,8 +1291,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
 (** Evaluate a non-local function call in symbolic mode *)
 and eval_non_local_function_call_symbolic (config : C.config)
     (fid : A.assumed_fun_id) (region_args : T.erased_region list)
-    (type_args : T.ety list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+    (type_args : T.ety list) (cg_args : T.const_generic list)
+    (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Sanity check: make sure the type parameters don't contain regions -
    * this is a current limitation of our synthesis *)
@@ -1308,7 +1310,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   | A.BoxFree ->
       (* Degenerate case: box_free - note that this is not really a function
        * call: no need to call a "synthesize_..." function *)
-      eval_box_free config region_args type_args args dest (cf Unit) ctx
+      eval_box_free config region_args type_args cg_args args dest (cf Unit) ctx
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1319,18 +1321,20 @@ and eval_non_local_function_call_symbolic (config : C.config)
         | A.BoxFree ->
             (* should have been treated above *)
             raise (Failure "Unreachable")
-        | _ -> instantiate_fun_sig type_args (Assumed.get_assumed_sig fid)
+        | _ ->
+            instantiate_fun_sig type_args cg_args (Assumed.get_assumed_sig fid)
       in
 
       (* Evaluate the function call *)
       eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
-        region_args type_args args dest cf ctx
+        region_args type_args cg_args args dest cf ctx
 
 (** Evaluate a non-local (i.e, assumed) function call such as [Box::deref]
     (auxiliary helper for [eval_statement]) *)
 and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
     (region_args : T.erased_region list) (type_args : T.ety list)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+    st_cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
@@ -1349,23 +1353,24 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
   match config.mode with
   | C.ConcreteMode ->
       eval_non_local_function_call_concrete config fid region_args type_args
-        args dest (cf Unit) ctx
+        cg_args args dest (cf Unit) ctx
   | C.SymbolicMode ->
       eval_non_local_function_call_symbolic config fid region_args type_args
-        args dest cf ctx
+        cg_args args dest cf ctx
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
 and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
     (region_args : T.erased_region list) (type_args : T.ety list)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+    st_cm_fun =
   match config.mode with
   | ConcreteMode ->
-      eval_local_function_call_concrete config fid region_args type_args args
-        dest
+      eval_local_function_call_concrete config fid region_args type_args cg_args
+        args dest
   | SymbolicMode ->
-      eval_local_function_call_symbolic config fid region_args type_args args
-        dest
+      eval_local_function_call_symbolic config fid region_args type_args cg_args
+        args dest
 
 (** Evaluate a statement seen as a function body *)
 and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
diff --git a/compiler/PrimitiveValuesUtils.ml b/compiler/PrimitiveValuesUtils.ml
new file mode 100644
index 00000000..0000916d
--- /dev/null
+++ b/compiler/PrimitiveValuesUtils.ml
@@ -0,0 +1 @@
+include Charon.PrimitiveValuesUtils
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 33a86df5..8fb6d644 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let assumed_ty_to_string (aty : assumed_ty) : string =
   | Array -> "Array"
   | Slice -> "Slice"
   | Str -> "Str"
+  | Range -> "Range"
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
@@ -293,9 +294,11 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
   | Assumed aty -> (
       (* Assumed type *)
       match aty with
-      | State | Vec | Array | Slice | Str ->
+      | State | Array | Slice | Str ->
           (* Those types are opaque: we can't get there *)
           raise (Failure "Unreachable")
+      | Vec -> "@Vec"
+      | Range -> "@Range"
       | Result ->
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then "@Result::Return"
@@ -334,6 +337,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
   | Assumed aty -> (
       (* Assumed type *)
       match aty with
+      | Range -> FieldId.to_string field_id
       | State | Fuel | Vec | Array | Slice | Str ->
           (* Opaque types: we can't get there *)
           raise (Failure "Unreachable")
@@ -425,7 +429,14 @@ let adt_g_value_to_string (fmt : value_formatter)
             List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
           in
           let id = assumed_ty_to_string aty in
-          id ^ " [" ^ String.concat "; " field_values ^ "]")
+          id ^ " [" ^ String.concat "; " field_values ^ "]"
+      | Range ->
+          assert (variant_id = None);
+          let field_values =
+            List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
+          in
+          let id = assumed_ty_to_string aty in
+          id ^ " {" ^ String.concat "; " field_values ^ "}")
   | _ ->
       let fmt = value_to_type_formatter fmt in
       raise
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index b90ef60a..551ebf7b 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,6 +64,7 @@ type assumed_ty =
   | Array
   | Slice
   | Str
+  | Range
 [@@deriving show, ord]
 
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 74f3c576..00620c58 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -585,6 +585,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 {
                   id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
                   type_args = _;
+                  const_generic_args = _;
                 } ->
                 (* Lookup the def *)
                 let decl =
@@ -1086,6 +1087,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 {
                   id = AdtCons { adt_id = AdtId adt_id; variant_id = None };
                   type_args;
+                  const_generic_args;
                 } ->
                 (* This is a struct *)
                 (* Retrieve the definiton, to find how many fields there are *)
@@ -1106,7 +1108,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                    * [x.field] for some variable [x], and where the projection
                    * is for the proper ADT *)
                   let to_var_proj (i : int) (arg : texpression) :
-                      (ty list * var_id) option =
+                      (ty list * const_generic list * var_id) option =
                     match arg.e with
                     | App (proj, x) -> (
                         match (proj.e, x.e) with
@@ -1115,13 +1117,15 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                                 id =
                                   Proj { adt_id = AdtId proj_adt_id; field_id };
                                 type_args = proj_type_args;
+                                const_generic_args = proj_const_generic_args;
                               },
                             Var v ) ->
                             (* We check that this is the proper ADT, and the proper field *)
                             if
                               proj_adt_id = adt_id
                               && FieldId.to_int field_id = i
-                            then Some (proj_type_args, v)
+                            then
+                              Some (proj_type_args, proj_const_generic_args, v)
                             else None
                         | _ -> None)
                     | _ -> None
@@ -1132,12 +1136,15 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                   if List.length args = num_fields then
                     (* Check that this is the same variable we project from -
                      * note that we checked above that there is at least one field *)
-                    let (_, x), end_args = Collections.List.pop args in
-                    if List.for_all (fun (_, y) -> y = x) end_args then (
+                    let (_, _, x), end_args = Collections.List.pop args in
+                    if List.for_all (fun (_, _, y) -> y = x) end_args then (
                       (* We can substitute *)
                       (* Sanity check: all types correct *)
                       assert (
-                        List.for_all (fun (tys, _) -> tys = type_args) args);
+                        List.for_all
+                          (fun (tys, cgs, _) ->
+                            tys = type_args && cgs = const_generic_args)
+                          args);
                       { e with e = Var x })
                     else super#visit_texpression env e
                   else super#visit_texpression env e
@@ -1156,6 +1163,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                         {
                           id = Proj { adt_id = AdtId proj_adt_id; field_id };
                           type_args = _;
+                          const_generic_args = _;
                         },
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
@@ -1354,6 +1362,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
             let loop_sig =
               {
                 type_params = fun_sig.type_params;
+                const_generic_params = fun_sig.const_generic_params;
                 inputs = inputs_tys;
                 output;
                 doutputs;
@@ -1554,8 +1563,11 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 | A.BoxFree, _ ->
                     assert (args = []);
                     mk_unit_rvalue
-                | ( ( A.Replace | A.VecNew | A.VecPush | A.VecInsert | A.VecLen
-                    | A.VecIndex | A.VecIndexMut ),
+                | ( ( A.Replace | VecNew | VecPush | VecInsert | VecLen
+                    | VecIndex | VecIndexMut | ArraySharedSubslice
+                    | ArrayMutSubslice | SliceSharedIndex | SliceMutIndex
+                    | SliceSharedSubslice | SliceMutSubslice | ArraySharedIndex
+                    | ArrayMutIndex | ArrayToSharedSlice | ArrayToMutSlice ),
                     _ ) ->
                     super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
@@ -2130,7 +2142,14 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
           let num_filtered =
             List.length (List.filter (fun b -> not b) used_info)
           in
-          let { type_params; inputs; output; doutputs; info } =
+          let {
+            type_params;
+            const_generic_params;
+            inputs;
+            output;
+            doutputs;
+            info;
+          } =
             decl.signature
           in
           let {
@@ -2158,7 +2177,16 @@ let filter_loop_inputs (transl : (bool * pure_fun_translation) list) :
               effect_info;
             }
           in
-          let signature = { type_params; inputs; output; doutputs; info } in
+          let signature =
+            {
+              type_params;
+              const_generic_params;
+              inputs;
+              output;
+              doutputs;
+              info;
+            }
+          in
 
           { decl with signature }
     in
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index ef8bac37..0f64720e 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -46,7 +46,11 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           if variant_id = option_some_id then [ ty ]
           else if variant_id = option_none_id then []
           else
-            raise (Failure "Unreachable: improper variant id for result type")
+            raise (Failure "Unreachable: improper variant id for option type")
+      | Range ->
+          let ty = Collections.List.to_cons_nil tys in
+          assert (variant_id = None);
+          [ ty; ty ]
       | Vec | Array | Slice | Str ->
           raise
             (Failure
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index a1b1572e..38850243 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -230,6 +230,11 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
           if adt.V.variant_id = Some T.option_some_id then type_params
           else if adt.V.variant_id = Some T.option_none_id then []
           else raise (Failure "Unreachable")
+      | T.Range ->
+          assert (List.length region_params = 0);
+          assert (List.length type_params = 1);
+          assert (List.length cg_params = 0);
+          type_params
       | T.Array | T.Slice | T.Str ->
           (* Those types don't have fields *)
           raise (Failure "Unreachable"))
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index a6d2784b..958c1bc8 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -416,7 +416,8 @@ let rec translate_sty (ty : T.sty) : ty =
               )
           | T.Array -> Adt (Assumed Array, tys, cgs)
           | T.Slice -> Adt (Assumed Slice, tys, cgs)
-          | T.Str -> Adt (Assumed Str, tys, cgs)))
+          | T.Str -> Adt (Assumed Str, tys, cgs)
+          | T.Range -> Adt (Assumed Range, tys, cgs)))
   | TypeVar vid -> TypeVar vid
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
@@ -472,6 +473,7 @@ let translate_type_id (id : T.type_id) : type_id =
         | T.Array -> Array
         | T.Slice -> Slice
         | T.Str -> Str
+        | T.Range -> Range
         | T.Box ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
@@ -493,7 +495,8 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       let t_tys = List.map translate tys in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _ | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
+      | AdtId _
+      | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
           (* No general parametricity for now *)
           assert (not (List.exists (TypesUtils.ty_has_borrows type_infos) tys));
           let type_id = translate_type_id type_id in
@@ -537,7 +540,8 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.Adt (type_id, _, tys, cgs) -> (
       match type_id with
-      | T.AdtId _ | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
+      | T.AdtId _
+      | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           let type_id = translate_type_id type_id in
@@ -1037,7 +1041,8 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | T.AdtId _
-        | T.Assumed (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
+        | T.Assumed
+            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1183,7 +1188,8 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
         let adt_id, _, _, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
         | T.AdtId _
-        | T.Assumed (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str) ->
+        | T.Assumed
+            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -2272,6 +2278,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
        * know how to expand values like vectors or arrays, because they have a variable number
        * of fields!) *)
       raise (Failure "Attempt to expand a non-expandable value")
+  | T.Assumed Range -> raise (Failure "Unimplemented")
   | T.Assumed T.Option ->
       (* We shouldn't get there in the "one-branch" case: options have
        * two variants *)
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index b4bb0386..925f6d39 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -170,8 +170,10 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         (* Continue exploring *)
         analyze expl_info ty_info rty
     | Adt
-        ((Tuple | Assumed (Box | Vec | Option | Slice | Array | Str)), _, tys, _)
-      ->
+        ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)),
+          _,
+          tys,
+          _ ) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
           (fun ty_info ty -> analyze expl_info ty_info ty)
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index abbfad31..d748cc2e 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -3,6 +3,7 @@ open TypesUtils
 open Types
 open Values
 module TA = TypesAnalysis
+include PrimitiveValuesUtils
 
 (** Utility exception *)
 exception FoundSymbolicValue of symbolic_value
diff --git a/compiler/dune b/compiler/dune
index b74b65fa..6785cad4 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -48,6 +48,8 @@
   PrePasses
   Print
   PrintPure
+  PrimitiveValues
+  PrimitiveValuesUtils
   PureMicroPasses
   Pure
   PureTypeCheck
@@ -67,8 +69,7 @@
   TypesUtils
   Utils
   Values
-  ValuesUtils
-  PrimitiveValues))
+  ValuesUtils))
 
 (documentation
  (package aeneas))
-- 
cgit v1.3.1


From 56aa15e45e8cbc32eec6ec07221d93cbe56fad59 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 2 Aug 2023 14:57:55 +0200
Subject: Make progress

---
 compiler/Extract.ml        | 90 ++++++++++++++++++++++++++++------------------
 compiler/ExtractBase.ml    | 23 ++++++++++++
 compiler/PrintPure.ml      |  1 -
 compiler/Pure.ml           |  6 +---
 compiler/SymbolicToPure.ml | 13 -------
 5 files changed, 80 insertions(+), 53 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b16f9639..3cb2be2c 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -41,7 +41,9 @@ let unop_name (unop : unop) : string =
       match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
   | Neg (int_ty : integer_type) -> (
       match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
-  | Cast _ -> raise (Failure "Unsupported")
+  | Cast _ ->
+      (* We never directly use the unop name in this case *)
+      raise (Failure "Unsupported")
 
 (** Small helper to compute the name of a binary operation (note that many
     binary operations like "less than" are extracted to primitive operations,
@@ -722,7 +724,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | None -> (
         (* No basename: we use the first letter of the type *)
         match ty with
-        | Adt (type_id, tys) -> (
+        | Adt (type_id, tys, _) -> (
             match type_id with
             | Tuple ->
                 (* The "pair" case is frequent enough to have its special treatment *)
@@ -732,6 +734,10 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             | Assumed Fuel -> ConstStrings.fuel_basename
             | Assumed Option -> "opt"
             | Assumed Vec -> "v"
+            | Assumed Array -> "a"
+            | Assumed Slice -> "s"
+            | Assumed Str -> "s"
+            | Assumed Range -> "r"
             | Assumed State -> ConstStrings.state_basename
             | AdtId adt_id ->
                 let def =
@@ -757,12 +763,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             match !backend with
             | FStar -> "x" (* lacking inspiration here... *)
             | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
-        | Bool -> "b"
-        | Char -> "c"
-        | Integer _ -> "i"
-        | Str -> "s"
-        | Arrow _ -> "f"
-        | Array _ | Slice _ -> raise Unimplemented)
+        | Literal lty -> (
+            match lty with Bool -> "b" | Char -> "c" | Integer _ -> "i")
+        | Arrow _ -> "f")
   in
   let type_var_basename (_varset : StringSet.t) (basename : string) : string =
     (* Rust type variables are snake-case and start with a capital letter *)
@@ -775,12 +778,21 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         "'" ^ to_snake_case basename
     | Coq | Lean -> basename
   in
+  let const_generic_var_basename (_varset : StringSet.t) (basename : string) :
+      string =
+    (* Rust type variables are snake-case and start with a capital letter *)
+    match !backend with
+    | FStar | HOL4 ->
+        (* This is *not* a no-op: this removes the capital letter *)
+        to_snake_case basename
+    | Coq | Lean -> basename
+  in
   let append_index (basename : string) (i : int) : string =
     basename ^ string_of_int i
   in
 
-  let extract_primitive_value (fmt : F.formatter) (inside : bool)
-      (cv : primitive_value) : unit =
+  let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit
+      =
     match cv with
     | Scalar sv -> (
         match !backend with
@@ -847,14 +859,6 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             in
             F.pp_print_string fmt c;
             if inside then F.pp_print_string fmt ")")
-    | String s ->
-        (* We need to replace all the line breaks *)
-        let s =
-          StringUtils.map
-            (fun c -> if c = '\n' then "\n" else String.make 1 c)
-            s
-        in
-        F.pp_print_string fmt ("\"" ^ s ^ "\"")
   in
   let bool_name = if !backend = Lean then "Bool" else "bool" in
   let char_name = if !backend = Lean then "Char" else "char" in
@@ -877,8 +881,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     opaque_pre;
     var_basename;
     type_var_basename;
+    const_generic_var_basename;
     append_index;
-    extract_primitive_value;
+    extract_literal;
     extract_unop;
     extract_binop;
   }
@@ -1043,6 +1048,17 @@ let extract_arrow (fmt : F.formatter) () : unit =
   if !Config.backend = Lean then F.pp_print_string fmt "→"
   else F.pp_print_string fmt "->"
 
+let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
+    (inside : bool) (cg : const_generic) : unit =
+  match cg with
+  | ConstGenericGlobal id ->
+      let s = ctx_get_global ctx.use_opaque_pre id ctx in
+      F.pp_print_string fmt s
+  | ConstGenericValue v -> ctx.fmt.extract_literal fmt inside v
+  | ConstGenericVar id ->
+      let s = ctx_get_const_generic_var id ctx in
+      F.pp_print_string fmt s
+
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
 
@@ -1067,7 +1083,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
   let extract_rec = extract_ty ctx fmt no_params_tys in
   match ty with
-  | Adt (type_id, tys) -> (
+  | Adt (type_id, tys, cgs) -> (
+      let has_params = tys <> [] || cgs <> [] in
       match type_id with
       | Tuple ->
           (* This is a bit annoying, but in F*/Coq/HOL4 [()] is not the unit type:
@@ -1099,7 +1116,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
           let with_opaque_pre = false in
           match !backend with
           | FStar | Coq | Lean ->
-              let print_paren = inside && tys <> [] in
+              let print_paren = inside && has_params in
               if print_paren then F.pp_print_string fmt "(";
               (* TODO: for now, only the opaque *functions* are extracted in the
                  opaque module. The opaque *types* are assumed. *)
@@ -1108,6 +1125,11 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                 F.pp_print_space fmt ();
                 Collections.List.iter_link (F.pp_print_space fmt)
                   (extract_rec true) tys);
+              if cgs <> [] then (
+                F.pp_print_space fmt ();
+                Collections.List.iter_link (F.pp_print_space fmt)
+                  (extract_const_generic ctx fmt true)
+                  cgs);
               if print_paren then F.pp_print_string fmt ")"
           | HOL4 ->
               let print_tys =
@@ -1128,10 +1150,9 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
                 F.pp_print_space fmt ());
               F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx)))
   | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
-  | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
-  | Char -> F.pp_print_string fmt ctx.fmt.char_name
-  | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
-  | Str -> F.pp_print_string fmt ctx.fmt.str_name
+  | Literal Bool -> F.pp_print_string fmt ctx.fmt.bool_name
+  | Literal Char -> F.pp_print_string fmt ctx.fmt.char_name
+  | Literal (Integer int_ty) -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
   | Arrow (arg_ty, ret_ty) ->
       if inside then F.pp_print_string fmt "(";
       extract_rec false arg_ty;
@@ -1140,7 +1161,6 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       extract_rec false ret_ty;
       if inside then F.pp_print_string fmt ")"
-  | Array _ | Slice _ -> raise Unimplemented
 
 (** Compute the names for all the top-level identifiers used in a type
     definition (type name, variant names, field names, etc. but not type
@@ -2016,10 +2036,11 @@ let extract_adt_g_value
     (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
     (ty : ty) : extraction_ctx =
   match ty with
-  | Adt (Tuple, type_args) ->
+  | Adt (Tuple, type_args, cg_args) ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
       assert (List.length type_args = List.length field_values);
+      assert (cg_args = []);
       (* This is very annoying: in Coq, we can't write [()] for the value of
          type [unit], we have to write [tt]. *)
       if !backend = Coq && field_values = [] then (
@@ -2037,7 +2058,7 @@ let extract_adt_g_value
         in
         F.pp_print_string fmt ")";
         ctx)
-  | Adt (adt_id, _) ->
+  | Adt (adt_id, _, _) ->
       (* "Regular" ADT *)
 
       (* If we are generating a pattern for a let-binding and we target Lean,
@@ -2107,7 +2128,7 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
     (is_let : bool) (inside : bool) (v : typed_pattern) : extraction_ctx =
   match v.value with
   | PatConstant cv ->
-      ctx.fmt.extract_primitive_value fmt inside cv;
+      ctx.fmt.extract_literal fmt inside cv;
       ctx
   | PatVar (v, _) ->
       let vname =
@@ -2142,7 +2163,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
   | Var var_id ->
       let var_name = ctx_get_var var_id ctx in
       F.pp_print_string fmt var_name
-  | Const cv -> ctx.fmt.extract_primitive_value fmt inside cv
+  | Const cv -> ctx.fmt.extract_literal fmt inside cv
   | App _ ->
       let app, args = destruct_apps e in
       extract_App ctx fmt inside app args
@@ -2175,7 +2196,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
           extract_function_call ctx fmt inside fun_id qualif.type_args args
       | Global global_id -> extract_global ctx fmt global_id
       | AdtCons adt_cons_id ->
-          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
+          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args
+            qualif.const_generic_args args
       | Proj proj ->
           extract_field_projector ctx fmt inside app proj qualif.type_args args)
   | _ ->
@@ -2250,9 +2272,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
 
 (** Subcase of the app case: ADT constructor *)
 and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (adt_cons : adt_cons_id) (type_args : ty list) (args : texpression list) :
-    unit =
-  let e_ty = Adt (adt_cons.adt_id, type_args) in
+    (adt_cons : adt_cons_id) (type_args : ty list)
+    (cg_args : const_generic list) (args : texpression list) : unit =
+  let e_ty = Adt (adt_cons.adt_id, type_args, cg_args) in
   let is_single_pat = false in
   let _ =
     extract_adt_g_value
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index bff6a360..3ba507a6 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -286,6 +286,8 @@ type formatter = {
        *)
   type_var_basename : StringSet.t -> string -> string;
       (** Generates a type variable basename. *)
+  const_generic_var_basename : StringSet.t -> string -> string;
+      (** Generates a const generic variable basename. *)
   append_index : string -> int -> string;
       (** Appends an index to a name - we use this to generate unique
           names: when doing so, the role of the formatter is just to concatenate
@@ -392,6 +394,7 @@ type id =
           them here.
        *)
   | TypeVarId of TypeVarId.id
+  | ConstGenericVarId of ConstGenericVarId.id
   | VarId of VarId.id
   | UnknownId
       (** Used for stored various strings like keywords, definitions which
@@ -710,6 +713,8 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       "field name: " ^ field_name
   | UnknownId -> "keyword"
   | TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
+  | ConstGenericVarId id ->
+      "const_generic_var_id: " ^ ConstGenericVarId.to_string id
   | VarId id -> "var_id: " ^ VarId.to_string id
 
 (** We might not check for collisions for some specific ids (ex.: field names) *)
@@ -788,6 +793,11 @@ let ctx_get_type_var (id : TypeVarId.id) (ctx : extraction_ctx) : string =
   let is_opaque = false in
   ctx_get is_opaque (TypeVarId id) ctx
 
+let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx)
+    : string =
+  let is_opaque = false in
+  ctx_get is_opaque (ConstGenericVarId id) ctx
+
 let ctx_get_field (type_id : type_id) (field_id : FieldId.id)
     (ctx : extraction_ctx) : string =
   let is_opaque = false in
@@ -823,6 +833,19 @@ let ctx_add_type_var (basename : string) (id : TypeVarId.id)
   let ctx = ctx_add is_opaque (TypeVarId id) name ctx in
   (ctx, name)
 
+(** Generate a unique const generic variable name and add it to the context *)
+let ctx_add_const_generic_var (basename : string) (id : ConstGenericVarId.id)
+    (ctx : extraction_ctx) : extraction_ctx * string =
+  let is_opaque = false in
+  let name =
+    ctx.fmt.const_generic_var_basename ctx.names_map.names_set basename
+  in
+  let name =
+    basename_to_unique ctx.names_map.names_set ctx.fmt.append_index name
+  in
+  let ctx = ctx_add is_opaque (ConstGenericVarId id) name ctx in
+  (ctx, name)
+
 (** See {!ctx_add_type_var} *)
 let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 8fb6d644..211fb2c2 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -543,7 +543,6 @@ let unop_to_string (unop : unop) : string =
   | Cast (src, tgt) ->
       "cast<" ^ integer_type_to_string src ^ "," ^ integer_type_to_string tgt
       ^ ">"
-  | SliceNew tgt_len -> "array_to_slice<" ^ scalar_value_to_string tgt_len ^ ">"
 
 let binop_to_string = Print.Expressions.binop_to_string
 
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 551ebf7b..e202b170 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -344,11 +344,7 @@ and typed_pattern = { value : pattern; ty : ty }
         polymorphic = false;
       }]
 
-type unop =
-  | Not
-  | Neg of integer_type
-  | Cast of integer_type * integer_type
-  | SliceNew of scalar_value
+type unop = Not | Neg of integer_type | Cast of integer_type * integer_type
 [@@deriving show, ord]
 
 (** Identifiers of assumed functions that we use only in the pure translation *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 958c1bc8..5e47459d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1537,19 +1537,6 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
           }
         in
         (ctx, Unop (Cast (src_ty, tgt_ty)), effect_info, args, None)
-    | S.Unop (E.SliceNew tgt_len) ->
-        (* The cast can fail if the length of the source array is not
-           big enough *)
-        let effect_info =
-          {
-            can_fail = true;
-            stateful_group = false;
-            stateful = false;
-            can_diverge = false;
-            is_rec = false;
-          }
-        in
-        (ctx, Unop (SliceNew tgt_len), effect_info, args, None)
     | S.Binop binop -> (
         match args with
         | [ arg0; arg1 ] ->
-- 
cgit v1.3.1


From 931fabe3e8590815548d606b33fc8db31e9f6010 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Aug 2023 16:21:43 +0200
Subject: Fix an issue with the extraction of aggregated arrays

---
 compiler/Extract.ml                    | 218 ++++++++++++++++++++-------------
 compiler/InterpreterExpressions.ml     |   4 +-
 compiler/InterpreterLoopsFixedPoint.ml |   2 +-
 compiler/InterpreterLoopsMatchCtxs.mli |   6 +-
 compiler/PrintPure.ml                  |  38 ++++--
 compiler/Pure.ml                       | 139 ++++++++++++++-------
 compiler/PureMicroPasses.ml            |   6 +-
 compiler/PureTypeCheck.ml              |  55 +++++----
 compiler/SymbolicAst.ml                |   9 +-
 compiler/SymbolicToPure.ml             |  23 +++-
 10 files changed, 320 insertions(+), 180 deletions(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 9ee94db2..f161cc13 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2260,7 +2260,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
   | Let (_, _, _, _) -> extract_lets ctx fmt inside e
   | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body
   | Meta (_, e) -> extract_texpression ctx fmt inside e
-  | StructUpdate supd -> extract_StructUpdate ctx fmt inside supd
+  | StructUpdate supd -> extract_StructUpdate ctx fmt inside e.ty supd
   | Loop _ ->
       (* The loop nodes should have been eliminated in {!PureMicroPasses} *)
       raise (Failure "Unreachable")
@@ -2723,104 +2723,152 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
   F.pp_close_box fmt ()
 
 and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
-    (inside : bool) (supd : struct_update) : unit =
+    (inside : bool) (e_ty : ty) (supd : struct_update) : unit =
   (* We can't update a subset of the fields in Coq (i.e., we can do
      [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
   assert (!backend <> Coq || supd.init = None);
   (* In the case of HOL4, records with no fields are not supported and are
      thus extracted to unit. We need to check that by looking up the definition *)
   let extract_as_unit =
-    if !backend = HOL4 then
-      let d =
-        TypeDeclId.Map.find supd.struct_id ctx.trans_ctx.type_context.type_decls
-      in
-      d.kind = Struct []
-    else false
+    match (!backend, supd.struct_id) with
+    | HOL4, AdtId adt_id ->
+        let d =
+          TypeDeclId.Map.find adt_id ctx.trans_ctx.type_context.type_decls
+        in
+        d.kind = Struct []
+    | _ -> false
   in
   if extract_as_unit then
     (* Remark: this is only valid for HOL4 (for instance the Coq unit value is [tt]) *)
     F.pp_print_string fmt "()"
-  else (
-    F.pp_open_hvbox fmt 0;
-    F.pp_open_hvbox fmt ctx.indent_incr;
-    (* Inner/outer brackets: there are several syntaxes for the field updates.
-
-       For instance, in F*:
-       {[
-         { x with f = ..., ... }
-       ]}
-
-       In HOL4:
-       {[
-         x with <| f = ..., ... |>
-       ]}
-
-       In the above examples:
-       - in F*, the { } brackets are "outer" brackets
-       - in HOL4, the <| |> brackets are "inner" brackets
+  else
+    (* There are two cases:
+       - this is a regular struct
+       - this is an array
     *)
-    (* Outer brackets *)
-    let olb, orb =
-      match !backend with
-      | Lean | FStar -> (Some "{", Some "}")
-      | Coq -> (Some "{|", Some "|}")
-      | HOL4 -> (None, None)
-    in
-    (* Inner brackets *)
-    let ilb, irb =
-      match !backend with
-      | Lean | FStar | Coq -> (None, None)
-      | HOL4 -> (Some "<|", Some "|>")
-    in
-    (* Helper *)
-    let print_bracket (is_left : bool) b =
-      match b with
-      | Some b ->
-          if not is_left then F.pp_print_space fmt ();
-          F.pp_print_string fmt b;
-          if is_left then F.pp_print_space fmt ()
-      | None -> ()
-    in
-    print_bracket true olb;
-    let need_paren = inside && !backend = HOL4 in
-    if need_paren then F.pp_print_string fmt "(";
-    F.pp_open_hvbox fmt ctx.indent_incr;
-    if supd.init <> None then (
-      let var_name = ctx_get_var (Option.get supd.init) ctx in
-      F.pp_print_string fmt var_name;
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt "with";
-      F.pp_print_space fmt ());
-    print_bracket true ilb;
-    F.pp_open_hvbox fmt 0;
-    let delimiter =
-      match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
-    in
-    let assign =
-      match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "="
-    in
-    Collections.List.iter_link
-      (fun () ->
-        F.pp_print_string fmt delimiter;
-        F.pp_print_space fmt ())
-      (fun (fid, fe) ->
+    match supd.struct_id with
+    | AdtId _ ->
+        F.pp_open_hvbox fmt 0;
         F.pp_open_hvbox fmt ctx.indent_incr;
-        let f = ctx_get_field (AdtId supd.struct_id) fid ctx in
-        F.pp_print_string fmt f;
-        F.pp_print_string fmt (" " ^ assign);
-        F.pp_print_space fmt ();
+        (* Inner/outer brackets: there are several syntaxes for the field updates.
+
+           For instance, in F*:
+           {[
+             { x with f = ..., ... }
+           ]}
+
+           In HOL4:
+           {[
+             x with <| f = ..., ... |>
+           ]}
+
+           In the above examples:
+           - in F*, the { } brackets are "outer" brackets
+           - in HOL4, the <| |> brackets are "inner" brackets
+        *)
+        (* Outer brackets *)
+        let olb, orb =
+          match !backend with
+          | Lean | FStar -> (Some "{", Some "}")
+          | Coq -> (Some "{|", Some "|}")
+          | HOL4 -> (None, None)
+        in
+        (* Inner brackets *)
+        let ilb, irb =
+          match !backend with
+          | Lean | FStar | Coq -> (None, None)
+          | HOL4 -> (Some "<|", Some "|>")
+        in
+        (* Helper *)
+        let print_bracket (is_left : bool) b =
+          match b with
+          | Some b ->
+              if not is_left then F.pp_print_space fmt ();
+              F.pp_print_string fmt b;
+              if is_left then F.pp_print_space fmt ()
+          | None -> ()
+        in
+        print_bracket true olb;
+        let need_paren = inside && !backend = HOL4 in
+        if need_paren then F.pp_print_string fmt "(";
         F.pp_open_hvbox fmt ctx.indent_incr;
-        extract_texpression ctx fmt true fe;
+        if supd.init <> None then (
+          let var_name = ctx_get_var (Option.get supd.init) ctx in
+          F.pp_print_string fmt var_name;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "with";
+          F.pp_print_space fmt ());
+        print_bracket true ilb;
+        F.pp_open_hvbox fmt 0;
+        let delimiter =
+          match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+        in
+        let assign =
+          match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+        in
+        Collections.List.iter_link
+          (fun () ->
+            F.pp_print_string fmt delimiter;
+            F.pp_print_space fmt ())
+          (fun (fid, fe) ->
+            F.pp_open_hvbox fmt ctx.indent_incr;
+            let f = ctx_get_field supd.struct_id fid ctx in
+            F.pp_print_string fmt f;
+            F.pp_print_string fmt (" " ^ assign);
+            F.pp_print_space fmt ();
+            F.pp_open_hvbox fmt ctx.indent_incr;
+            extract_texpression ctx fmt true fe;
+            F.pp_close_box fmt ();
+            F.pp_close_box fmt ())
+          supd.updates;
         F.pp_close_box fmt ();
-        F.pp_close_box fmt ())
-      supd.updates;
-    F.pp_close_box fmt ();
-    print_bracket false irb;
-    F.pp_close_box fmt ();
-    F.pp_close_box fmt ();
-    if need_paren then F.pp_print_string fmt ")";
-    print_bracket false orb;
-    F.pp_close_box fmt ())
+        print_bracket false irb;
+        F.pp_close_box fmt ();
+        F.pp_close_box fmt ();
+        if need_paren then F.pp_print_string fmt ")";
+        print_bracket false orb;
+        F.pp_close_box fmt ()
+    | Assumed Array ->
+        (* Open the boxes *)
+        F.pp_open_hvbox fmt ctx.indent_incr;
+        let need_paren = inside in
+        if need_paren then F.pp_print_string fmt "(";
+        (* Open the box for `Array.mk T N [` *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Print the array constructor *)
+        let cs = ctx_get_struct false (Assumed Array) ctx in
+        F.pp_print_string fmt cs;
+        (* Print the parameters *)
+        let _, tys, cgs = ty_as_adt e_ty in
+        let ty = Collections.List.to_cons_nil tys in
+        F.pp_print_space fmt ();
+        extract_ty ctx fmt TypeDeclId.Set.empty true ty;
+        let cg = Collections.List.to_cons_nil cgs in
+        F.pp_print_space fmt ();
+        extract_const_generic ctx fmt true cg;
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "[";
+        (* Close the box for `Array.mk T N [` *)
+        F.pp_close_box fmt ();
+        (* Print the values *)
+        let delimiter =
+          match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+        in
+        F.pp_print_space fmt ();
+        F.pp_open_hovbox fmt 0;
+        Collections.List.iter_link
+          (fun () ->
+            F.pp_print_string fmt delimiter;
+            F.pp_print_space fmt ())
+          (fun (_, fe) -> extract_texpression ctx fmt false fe)
+          supd.updates;
+        (* Close the boxes *)
+        F.pp_close_box fmt ();
+        if supd.updates <> [] then F.pp_print_space fmt ();
+        F.pp_print_string fmt "]";
+        if need_paren then F.pp_print_string fmt ")";
+        F.pp_close_box fmt ()
+    | _ -> raise (Failure "Unreachable")
 
 (** Insert a space, if necessary *)
 let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 0834cfe2..8b2070c6 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -719,9 +719,7 @@ let eval_rvalue_aggregate (config : C.config)
         (* Sanity check: the number of values is consistent with the length *)
         let len = (literal_as_scalar (const_generic_as_literal cg)).value in
         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
@@ -736,7 +734,7 @@ let eval_rvalue_aggregate (config : C.config)
         | 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)))
+            Some (SymbolicAst.IntroSymbolic (ctx, None, sv, Array values, e)))
   in
   (* Compose and apply *)
   comp eval_ops compute cf
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index a9ec9ecf..4310f017 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -322,7 +322,7 @@ let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun =
              let sv =
                V.SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values
              in
-             SymbolicAst.IntroSymbolic (ctx, None, sv, v, e))
+             SymbolicAst.IntroSymbolic (ctx, None, sv, SingleValue v, e))
            e !sid_subst)
 
 let prepare_ashared_loans_no_synth (loop_id : V.LoopId.id) (ctx : C.eval_ctx) :
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index d0f57f32..20b997ce 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -34,13 +34,13 @@ val compute_abs_borrows_loans_maps :
     We use it for joins, to check if two environments are convertible, etc.
     See for instance {!MakeJoinMatcher} and {!MakeCheckEquivMatcher}.
 
-    The functor is parameterized by a {!InterpreterLoopsCore.PrimMatcher}, which implements the
-    non-generic part of the match. More precisely, the role of {!InterpreterLoopsCore.PrimMatcher} is two
+    The functor is parameterized by a {!PrimMatcher}, which implements the
+    non-generic part of the match. More precisely, the role of {!PrimMatcher} is two
     provide generic functions which recursively match two values (by recursively
     matching the fields of ADT values for instance). When it does need to match
     values in a non-trivial manner (if two ADT values don't have the same
     variant for instance) it calls the corresponding specialized function from
-    {!InterpreterLoopsCore.PrimMatcher}.
+    {!PrimMatcher}.
  *)
 module MakeMatcher : functor (_ : PrimMatcher) -> Matcher
 
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 211fb2c2..43b11aa5 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -583,25 +583,39 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
   | Loop loop ->
       let e = loop_to_string fmt indent indent_incr loop in
       if inside then "(" ^ e ^ ")" else e
-  | StructUpdate supd ->
+  | StructUpdate supd -> (
       let s =
         match supd.init with
         | None -> ""
         | Some vid -> " " ^ fmt.var_id_to_string vid ^ " with"
       in
-      let field_names = Option.get (fmt.adt_field_names supd.struct_id None) in
       let indent1 = indent ^ indent_incr in
       let indent2 = indent1 ^ indent_incr in
-      let fields =
-        List.map
-          (fun (fid, fe) ->
-            let field = FieldId.nth field_names fid in
-            let fe = texpression_to_string fmt false indent2 indent_incr fe in
-            "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";")
-          supd.updates
-      in
-      let bl = if fields = [] then "" else "\n" ^ indent in
-      "{" ^ s ^ String.concat "" fields ^ bl ^ "}"
+      (* The id should be a custom type decl id or an array *)
+      match supd.struct_id with
+      | AdtId aid ->
+          let field_names = Option.get (fmt.adt_field_names aid None) in
+          let fields =
+            List.map
+              (fun (fid, fe) ->
+                let field = FieldId.nth field_names fid in
+                let fe =
+                  texpression_to_string fmt false indent2 indent_incr fe
+                in
+                "\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";")
+              supd.updates
+          in
+          let bl = if fields = [] then "" else "\n" ^ indent in
+          "{" ^ s ^ String.concat "" fields ^ bl ^ "}"
+      | Assumed Array ->
+          let fields =
+            List.map
+              (fun (_, fe) ->
+                texpression_to_string fmt false indent2 indent_incr fe)
+              supd.updates
+          in
+          "[ " ^ String.concat ", " fields ^ " ]"
+      | _ -> raise (Failure "Unexpected"))
   | Meta (meta, e) -> (
       let meta_s = meta_to_string fmt meta in
       let e = texpression_to_string fmt inside indent indent_incr e in
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index e202b170..ac4ca081 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -105,6 +105,29 @@ class ['self] map_type_id_base =
     method visit_assumed_ty : 'env -> assumed_ty -> assumed_ty = fun _ x -> x
   end
 
+(** Ancestor for reduce visitor for [ty] *)
+class virtual ['self] reduce_type_id_base =
+  object (self : 'self)
+    inherit [_] VisitorsRuntime.reduce
+
+    method visit_type_decl_id : 'env -> type_decl_id -> 'a =
+      fun _ _ -> self#zero
+
+    method visit_assumed_ty : 'env -> assumed_ty -> 'a = fun _ _ -> self#zero
+  end
+
+(** Ancestor for mapreduce visitor for [ty] *)
+class virtual ['self] mapreduce_type_id_base =
+  object (self : 'self)
+    inherit [_] VisitorsRuntime.mapreduce
+
+    method visit_type_decl_id : 'env -> type_decl_id -> type_decl_id * 'a =
+      fun _ x -> (x, self#zero)
+
+    method visit_assumed_ty : 'env -> assumed_ty -> assumed_ty * 'a =
+      fun _ x -> (x, self#zero)
+  end
+
 type type_id = AdtId of type_decl_id | Tuple | Assumed of assumed_ty
 [@@deriving
   show,
@@ -126,6 +149,22 @@ type type_id = AdtId of type_decl_id | Tuple | Assumed of assumed_ty
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
+      },
+    visitors
+      {
+        name = "reduce_type_id";
+        variety = "reduce";
+        ancestors = [ "reduce_type_id_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        polymorphic = false;
+      },
+    visitors
+      {
+        name = "mapreduce_type_id";
+        variety = "mapreduce";
+        ancestors = [ "mapreduce_type_id_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        polymorphic = false;
       }]
 
 type literal_type = T.literal_type [@@deriving show, ord]
@@ -148,6 +187,26 @@ class ['self] map_ty_base =
     method visit_type_var_id : 'env -> type_var_id -> type_var_id = fun _ x -> x
   end
 
+(** Ancestor for reduce visitor for [ty] *)
+class virtual ['self] reduce_ty_base =
+  object (self : 'self)
+    inherit [_] reduce_type_id
+    inherit! [_] T.reduce_const_generic
+    inherit! [_] PV.reduce_literal_type
+    method visit_type_var_id : 'env -> type_var_id -> 'a = fun _ _ -> self#zero
+  end
+
+(** Ancestor for mapreduce visitor for [ty] *)
+class virtual ['self] mapreduce_ty_base =
+  object (self : 'self)
+    inherit [_] mapreduce_type_id
+    inherit! [_] T.mapreduce_const_generic
+    inherit! [_] PV.mapreduce_literal_type
+
+    method visit_type_var_id : 'env -> type_var_id -> type_var_id * 'a =
+      fun _ x -> (x, self#zero)
+  end
+
 type ty =
   | Adt of type_id * ty list * const_generic list
       (** {!Adt} encodes ADTs and tuples and assumed types.
@@ -176,9 +235,25 @@ type ty =
         name = "map_ty";
         variety = "map";
         ancestors = [ "map_ty_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+        nude = true (* Don't inherit {!VisitorsRuntime.map} *);
         concrete = true;
         polymorphic = false;
+      },
+    visitors
+      {
+        name = "reduce_ty";
+        variety = "reduce";
+        ancestors = [ "reduce_ty_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.reduce} *);
+        polymorphic = false;
+      },
+    visitors
+      {
+        name = "mapreduce_ty";
+        variety = "mapreduce";
+        ancestors = [ "mapreduce_ty_base" ];
+        nude = true (* Don't inherit {!VisitorsRuntime.mapreduce} *);
+        polymorphic = false;
       }]
 
 type field = { field_name : string option; field_ty : ty } [@@deriving show]
@@ -243,51 +318,39 @@ type variant_id = VariantId.id [@@deriving show]
 (** Ancestor for {!iter_typed_pattern} visitor *)
 class ['self] iter_typed_pattern_base =
   object (_self : 'self)
-    inherit [_] VisitorsRuntime.iter
-    method visit_literal : 'env -> literal -> unit = fun _ _ -> ()
+    inherit [_] iter_ty
     method visit_var : 'env -> var -> unit = fun _ _ -> ()
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
-    method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
     method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
   end
 
 (** Ancestor for {!map_typed_pattern} visitor *)
 class ['self] map_typed_pattern_base =
   object (_self : 'self)
-    inherit [_] VisitorsRuntime.map
-    method visit_literal : 'env -> literal -> literal = fun _ x -> x
+    inherit [_] map_ty
     method visit_var : 'env -> var -> var = fun _ x -> x
     method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
-    method visit_ty : 'env -> ty -> ty = fun _ x -> x
     method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
   end
 
 (** Ancestor for {!reduce_typed_pattern} visitor *)
 class virtual ['self] reduce_typed_pattern_base =
   object (self : 'self)
-    inherit [_] VisitorsRuntime.reduce
-    method visit_literal : 'env -> literal -> 'a = fun _ _ -> self#zero
+    inherit [_] reduce_ty
     method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
     method visit_mplace : 'env -> mplace -> 'a = fun _ _ -> self#zero
-    method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
     method visit_variant_id : 'env -> variant_id -> 'a = fun _ _ -> self#zero
   end
 
 (** Ancestor for {!mapreduce_typed_pattern} visitor *)
 class virtual ['self] mapreduce_typed_pattern_base =
   object (self : 'self)
-    inherit [_] VisitorsRuntime.mapreduce
-
-    method visit_literal : 'env -> literal -> literal * 'a =
-      fun _ x -> (x, self#zero)
-
+    inherit [_] mapreduce_ty
     method visit_var : 'env -> var -> var * 'a = fun _ x -> (x, self#zero)
 
     method visit_mplace : 'env -> mplace -> mplace * 'a =
       fun _ x -> (x, self#zero)
 
-    method visit_ty : 'env -> ty -> ty * 'a = fun _ x -> (x, self#zero)
-
     method visit_variant_id : 'env -> variant_id -> variant_id * 'a =
       fun _ x -> (x, self#zero)
   end
@@ -419,11 +482,10 @@ type var_id = VarId.id [@@deriving show, ord]
 class ['self] iter_expression_base =
   object (_self : 'self)
     inherit [_] iter_typed_pattern
-    method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
+    inherit! [_] iter_type_id
     method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
     method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
     method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
-    method visit_type_decl_id : 'env -> type_decl_id -> unit = fun _ _ -> ()
     method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
   end
 
@@ -431,17 +493,10 @@ class ['self] iter_expression_base =
 class ['self] map_expression_base =
   object (_self : 'self)
     inherit [_] map_typed_pattern
-
-    method visit_integer_type : 'env -> integer_type -> integer_type =
-      fun _ x -> x
-
+    inherit! [_] map_type_id
     method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x
     method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
     method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x
-
-    method visit_type_decl_id : 'env -> type_decl_id -> type_decl_id =
-      fun _ x -> x
-
     method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
   end
 
@@ -449,17 +504,10 @@ class ['self] map_expression_base =
 class virtual ['self] reduce_expression_base =
   object (self : 'self)
     inherit [_] reduce_typed_pattern
-
-    method visit_integer_type : 'env -> integer_type -> 'a =
-      fun _ _ -> self#zero
-
+    inherit! [_] reduce_type_id
     method visit_var_id : 'env -> var_id -> 'a = fun _ _ -> self#zero
     method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
     method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero
-
-    method visit_type_decl_id : 'env -> type_decl_id -> 'a =
-      fun _ _ -> self#zero
-
     method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero
   end
 
@@ -467,9 +515,7 @@ class virtual ['self] reduce_expression_base =
 class virtual ['self] mapreduce_expression_base =
   object (self : 'self)
     inherit [_] mapreduce_typed_pattern
-
-    method visit_integer_type : 'env -> integer_type -> integer_type * 'a =
-      fun _ x -> (x, self#zero)
+    inherit! [_] mapreduce_type_id
 
     method visit_var_id : 'env -> var_id -> var_id * 'a =
       fun _ x -> (x, self#zero)
@@ -480,9 +526,6 @@ class virtual ['self] mapreduce_expression_base =
     method visit_loop_id : 'env -> loop_id -> loop_id * 'a =
       fun _ x -> (x, self#zero)
 
-    method visit_type_decl_id : 'env -> type_decl_id -> type_decl_id * 'a =
-      fun _ x -> (x, self#zero)
-
     method visit_field_id : 'env -> field_id -> field_id * 'a =
       fun _ x -> (x, self#zero)
   end
@@ -592,9 +635,21 @@ and loop = {
     {[
       { s with x := 3 }
     ]}
+
+    We also use struct updates to encode array aggregates, so that whenever
+    the user writes code like:
+    {[
+      let a : [u32; 2] = [0, 1];
+      ...
+    ]}
+    this gets encoded to:
+    {[
+      let a : Array u32 2 = Array.mk [0, 1] in
+      ...
+    ]}
  *)
 and struct_update = {
-  struct_id : type_decl_id;
+  struct_id : type_id;
   init : var_id option;
   updates : (field_id * texpression) list;
 }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 00620c58..58a5f9e2 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -611,7 +611,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     (!Config.backend <> Lean && !Config.backend <> Coq)
                     || not is_rec
                   then
-                    let struct_id = adt_id in
+                    let struct_id = AdtId adt_id in
                     let init = None in
                     let updates =
                       FieldId.mapi
@@ -1168,8 +1168,8 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       Var v ) ->
                       (* We check that this is the proper ADT, and the proper field *)
                       if
-                        proj_adt_id = struct_id && field_id = fid
-                        && x.ty = adt_ty
+                        AdtId proj_adt_id = struct_id
+                        && field_id = fid && x.ty = adt_ty
                       then Some v
                       else None
                   | _ -> None)
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 8f5b5df4..8d28bb8a 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -5,8 +5,8 @@ open PureUtils
 
 (** Utility function, used for type checking.
 
-    We need the number of fields for cases like `Slice`, when the number of fields
-    varies.
+    This function should only be used for "regular" ADTs, where the number
+    of fields is fixed: it shouldn't be used for arrays, slices, etc.
  *)
 let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
     (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list)
@@ -55,17 +55,9 @@ 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 ]
-      | 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 ->
+      | Vec | Array | Slice | Str ->
+          (* Array: when not symbolic values (for instance, because of aggregates),
+             the array expressions are introduced as struct updates *)
           raise (Failure "Attempting to access the fields of an opaque type"))
 
 type tc_ctx = {
@@ -207,7 +199,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       assert (Option.is_some loop.back_output_tys || loop.loop_body.ty = e.ty);
       check_texpression ctx loop.fun_end;
       check_texpression ctx loop.loop_body
-  | StructUpdate supd ->
+  | StructUpdate supd -> (
       (* Check the init value *)
       (if Option.is_some supd.init then
          match VarId.Map.find_opt (Option.get supd.init) ctx.env with
@@ -216,18 +208,29 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
       (* Check the fields *)
       (* Retrieve and check the expected field type *)
       let adt_id, adt_type_args, adt_cg_args = ty_as_adt e.ty in
-      assert (adt_id = AdtId supd.struct_id);
-      let variant_id = None in
-      let expected_field_tys =
-        get_adt_field_types ctx.type_decls adt_id variant_id adt_type_args
-          adt_cg_args
-      in
-      List.iter
-        (fun (fid, fe) ->
-          let expected_field_ty = FieldId.nth expected_field_tys fid in
-          assert (expected_field_ty = fe.ty);
-          check_texpression ctx fe)
-        supd.updates
+      assert (adt_id = supd.struct_id);
+      (* The id can only be: a custom type decl or an array *)
+      match adt_id with
+      | AdtId _ ->
+          let variant_id = None in
+          let expected_field_tys =
+            get_adt_field_types ctx.type_decls adt_id variant_id adt_type_args
+              adt_cg_args
+          in
+          List.iter
+            (fun (fid, fe) ->
+              let expected_field_ty = FieldId.nth expected_field_tys fid in
+              assert (expected_field_ty = fe.ty);
+              check_texpression ctx fe)
+            supd.updates
+      | Assumed Array ->
+          let expected_field_ty = Collections.List.to_cons_nil adt_type_args in
+          List.iter
+            (fun (_, fe) ->
+              assert (expected_field_ty = fe.ty);
+              check_texpression ctx fe)
+            supd.updates
+      | _ -> raise (Failure "Unexpected"))
   | Meta (_, e_next) ->
       assert (e_next.ty = e.ty);
       check_texpression ctx e_next
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 787fefc7..7dc94dcd 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -167,7 +167,7 @@ type expression =
       Contexts.eval_ctx
       * mplace option
       * V.symbolic_value
-      * V.typed_value
+      * value_aggregate
       * expression
       (** We introduce a new symbolic value, equal to some other value.
 
@@ -246,6 +246,13 @@ and expansion =
       T.integer_type * (V.scalar_value * expression) list * expression
       (** An integer expansion (i.e, a switch over an integer). The last
           expression is for the "otherwise" branch. *)
+
+(* Remark: this type doesn't have to be mutually recursive with the other
+   types, but it makes it easy to generate the visitors *)
+and value_aggregate =
+  | SingleValue of V.typed_value  (** Regular case *)
+  | Array of V.typed_value list
+      (** This is used when introducing array aggregates *)
 [@@deriving
   show,
     visitors
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5e47459d..3512270a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2272,19 +2272,34 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
       raise (Failure "Unreachable")
 
 and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
-    (sv : V.symbolic_value) (v : V.typed_value) (e : S.expression)
+    (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
     (ctx : bs_ctx) : texpression =
   let mplace = translate_opt_mplace p in
 
   (* Introduce a fresh variable for the symbolic value *)
   let ctx, var = fresh_var_for_symbolic_value sv ctx in
 
-  (* Translate the value *)
-  let v = typed_value_to_texpression ctx ectx v in
-
   (* Translate the next expression *)
   let next_e = translate_expression e ctx in
 
+  (* Translate the value: there are two cases, depending on whether this
+     is a "regular" let-binding or an array aggregate.
+  *)
+  let v =
+    match v with
+    | SingleValue v -> typed_value_to_texpression ctx ectx v
+    | Array values ->
+        (* We use a struct update to encode the array aggregate, in order
+           to preserve the structure and allow generating code of the shape
+           `[x0, ...., xn]` *)
+        let values = List.map (typed_value_to_texpression ctx ectx) values in
+        let values = FieldId.mapi (fun fid v -> (fid, v)) values in
+        let su : struct_update =
+          { struct_id = Assumed Array; init = None; updates = values }
+        in
+        { e = StructUpdate su; ty = var.ty }
+  in
+
   (* Make the let-binding *)
   let monadic = false in
   let var = mk_typed_pattern_from_var var mplace in
-- 
cgit v1.3.1