Fix some mistakes in the type conversion to pure

4 files changed, 53 insertions, 14 deletions

diff --git a/src/Logging.ml b/src/Logging.ml
index f4fa9309..55b07ed4 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -15,6 +15,9 @@ let pre_passes_log = L.get_logger "MainLogger.PrePasses"
 (** Logger for Translate *)
 let translate_log = L.get_logger "MainLogger.Translate"
 
+(** Logger for PureUtils *)
+let pure_utils_log = L.get_logger "MainLogger.PureUtils"
+
 (** Logger for SymbolicToPure *)
 let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 662902e6..1ed072e9 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -1,5 +1,8 @@
 open Pure
 
+(** Default logger *)
+let log = Logging.pure_utils_log
+
 type regular_fun_id = A.fun_id * T.RegionGroupId.id option
 [@@deriving show, ord]
 (** We use this type as a key for lookups *)
@@ -270,7 +273,6 @@ module TypeCheck = struct
   let check_adt_g_value (ctx : tc_ctx) (check_value : ty -> 'v -> unit)
       (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) :
       unit =
-    (*    let field_values = List.map value_to_string field_values in *)
     (* Retrieve the field types *)
     let field_tys =
       match ty with
@@ -312,17 +314,23 @@ module TypeCheck = struct
       (List.combine field_tys field_values)
 
   let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : unit =
+    log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v));
     match v.value with
     | LvConcrete cv -> check_constant_value v.ty cv
     | LvVar _ -> ()
     | LvAdt av ->
         check_adt_g_value ctx
           (fun ty (v : typed_lvalue) ->
-            assert (ty = v.ty);
+            if ty <> v.ty then (
+              log#serror
+                ("check_typed_lvalue: not the same types:" ^ "\n- ty: "
+               ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
+              raise (Failure "Inconsistent types"));
             check_typed_lvalue ctx v)
           av.variant_id av.field_values v.ty
 
   let rec check_typed_rvalue (ctx : tc_ctx) (v : typed_rvalue) : unit =
+    log#ldebug (lazy ("check_typed_rvalue: " ^ show_typed_rvalue v));
     match v.value with
     | RvConcrete cv -> check_constant_value v.ty cv
     | RvPlace _ ->
@@ -331,7 +339,11 @@ module TypeCheck = struct
     | RvAdt av ->
         check_adt_g_value ctx
           (fun ty (v : typed_rvalue) ->
-            assert (ty = v.ty);
+            if ty <> v.ty then (
+              log#serror
+                ("check_typed_rvalue: not the same types:" ^ "\n- ty: "
+               ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
+              raise (Failure "Inconsistent types"));
             check_typed_rvalue ctx v)
           av.variant_id av.field_values v.ty
 end
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 0a4d0176..1967732d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -200,7 +200,10 @@ let rec translate_sty (ty : T.sty) : ty =
       | T.Tuple -> mk_simpl_tuple_ty tys
       | T.Assumed aty -> (
           match aty with
-          | T.Box | T.Vec | T.Option -> (
+          | T.Vec -> Adt (Assumed Vec, tys)
+          | T.Option -> Adt (Assumed Option, tys)
+          | T.Box -> (
+              (* Eliminate the boxes *)
               match tys with
               | [ ty ] -> ty
               | _ ->
@@ -265,17 +268,25 @@ let rec translate_fwd_ty (types_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       assert (regions = []);
       (* Translate the type parameters *)
       let t_tys = List.map translate tys in
-      (* Eliminate boxes *)
+      (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId adt_id ->
+      | AdtId _ | T.Assumed (T.Vec | T.Option) ->
           (* No general parametricity for now *)
           assert (not (List.exists (TypesUtils.ty_has_borrows types_infos) tys));
-          Adt (AdtId adt_id, t_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)
       | Tuple ->
           (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the
              identity *)
           mk_simpl_tuple_ty t_tys
-      | T.Assumed (T.Box | T.Vec | T.Option) -> (
+      | T.Assumed T.Box -> (
+          (* We eliminate boxes *)
           (* No general parametricity for now *)
           assert (not (List.exists (TypesUtils.ty_has_borrows types_infos) tys));
           match t_tys with
@@ -317,20 +328,21 @@ let rec translate_back_ty (types_infos : TA.type_infos)
   match ty with
   | T.Adt (type_id, _, tys) -> (
       match type_id with
-      | T.AdtId _ ->
+      | T.AdtId _ | Assumed (T.Vec | T.Option) ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows types_infos ty));
           let type_id =
             match type_id with
             | T.AdtId id -> AdtId id
-            | T.Tuple | T.Assumed (T.Box | T.Vec | T.Option) ->
-                failwith "Unreachable"
+            | T.Assumed T.Vec -> Assumed Vec
+            | T.Assumed T.Option -> Assumed Option
+            | T.Tuple | T.Assumed T.Box -> failwith "Unreachable"
           in
           if inside_mut then
             let tys_t = List.filter_map translate tys in
             Some (Adt (type_id, tys_t))
           else None
-      | Assumed (T.Box | T.Vec | T.Option) -> (
+      | Assumed T.Box -> (
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows types_infos ty));
           (* Eliminate the box *)
@@ -576,10 +588,15 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
   let value =
     match v.value with
     | V.Concrete cv -> RvConcrete cv
-    | Adt av ->
+    | Adt av -> (
         let variant_id = av.variant_id in
         let field_values = List.map translate av.field_values in
-        RvAdt { variant_id; field_values }
+        (* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
+        match v.ty with
+        | T.Adt (T.Tuple, _, _) ->
+            assert (variant_id = None);
+            (mk_simpl_tuple_rvalue field_values).value
+        | _ -> RvAdt { variant_id; field_values })
     | Bottom -> failwith "Unreachable"
     | Loan lc -> (
         match lc with
@@ -601,6 +618,11 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
   in
   let ty = ctx_translate_fwd_ty ctx v.ty in
   let value = { value; ty } in
+  (* Debugging *)
+  log#ldebug
+    (lazy
+      ("typed_value_to_rvalue: result:" ^ "\n- input:\n" ^ V.show_typed_value v
+     ^ "\n- typed rvalue:\n" ^ show_typed_rvalue value));
   (* Sanity check *)
   type_check_rvalue ctx value;
   (* Return *)
diff --git a/src/main.ml b/src/main.ml
index ca05ba78..193b20c2 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -92,6 +92,7 @@ let () =
    * command-line arguments *)
   Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
   main_log#set_level EL.Debug;
+  pre_passes_log#set_level EL.Debug;
   interpreter_log#set_level EL.Debug;
   statements_log#set_level EL.Debug;
   paths_log#set_level EL.Debug;
@@ -99,6 +100,7 @@ let () =
   expansion_log#set_level EL.Debug;
   borrows_log#set_level EL.Debug;
   invariants_log#set_level EL.Warning;
+  pure_utils_log#set_level EL.Debug;
   symbolic_to_pure_log#set_level EL.Debug;
   pure_micro_passes_log#set_level EL.Debug;
   pure_to_extract_log#set_level EL.Debug;