Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 10 insertions, 10 deletions

diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 9487df84..faed066b 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -23,12 +23,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
   if not (ty_has_regions_in_set regions ty) then []
   else
     match (v.V.value, ty) with
-    | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> []
-    | V.Adt adt, T.Adt (id, region_params, tys) ->
+    | V.Literal _, T.Literal _ -> []
+    | V.Adt adt, T.Adt (id, region_params, tys, cgs) ->
         (* Retrieve the types of the fields *)
         let field_types =
           Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-            region_params tys
+            region_params tys cgs
         in
         (* Project over the field values *)
         let fields_types = List.combine adt.V.field_values field_types in
@@ -102,12 +102,12 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
   else
     let value : V.avalue =
       match (v.V.value, ty) with
-      | V.Primitive _, (T.Bool | T.Char | T.Integer _ | T.Str) -> V.AIgnored
-      | V.Adt adt, T.Adt (id, region_params, tys) ->
+      | V.Literal _, T.Literal _ -> V.AIgnored
+      | V.Adt adt, T.Adt (id, region_params, tys, cgs) ->
           (* Retrieve the types of the fields *)
           let field_types =
             Subst.ctx_adt_value_get_instantiated_field_rtypes ctx adt id
-              region_params tys
+              region_params tys cgs
           in
           (* Project over the field values *)
           let fields_types = List.combine adt.V.field_values field_types in
@@ -231,7 +231,7 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
   let ty = Subst.erase_regions sv.V.sv_ty in
   let value =
     match see with
-    | SePrimitive cv -> V.Primitive cv
+    | SeLiteral cv -> V.Literal cv
     | SeAdt (variant_id, field_values) ->
         let field_values =
           List.map mk_typed_value_from_symbolic_value field_values
@@ -267,9 +267,9 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
   (* Match *)
   let (value, ty) : V.avalue * T.rty =
     match (see, original_sv_ty) with
-    | SePrimitive _, (T.Bool | T.Char | T.Integer _ | T.Str) ->
-        (V.AIgnored, original_sv_ty)
-    | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys) ->
+    | SeLiteral _, T.Literal _ -> (V.AIgnored, original_sv_ty)
+    | SeAdt (variant_id, field_values), T.Adt (_id, _region_params, _tys, _cgs)
+      ->
         (* Project over the field values *)
         let field_values =
           List.map