From 581d5c0cb8e618382fa41e5a42175560283ff0a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 7 Apr 2024 14:27:14 +0200
Subject: Cleanup a bit and improve the error messages

---
 compiler/Invariants.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'compiler/Invariants.ml')

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..2ccf3ad4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
           "find_info: could not find the representant of borrow "
           ^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
         in
-        log#serror err;
         craise __FILE__ __LINE__ meta err
   in
 
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
             | AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
         | AIgnored, _ -> ()
         | _ ->
-            log#lerror
+            log#ltrace
               (lazy
                 ("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
                ^ "\n- value: "
                 ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
                 ^ "\n- type: " ^ ty_to_string ctx atv.ty));
-            craise __FILE__ __LINE__ meta "Erroneous typing");
+            internal_error __FILE__ __LINE__ meta);
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_avalue info atv
     end
-- 
cgit v1.2.3


From 143a68b2c43c4302abbbd39c28cac3f9c5f52f4a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 10 Apr 2024 16:46:24 +0200
Subject: Trust rustc regarding `Copy` bounds

---
 compiler/Invariants.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Invariants.ml')

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 2ccf3ad4..6e448cc4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -827,7 +827,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
     (* A duplicated symbolic value is necessarily primitively copyable *)
     sanity_check __FILE__ __LINE__
-      (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+      (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
 
     sanity_check __FILE__ __LINE__
-- 
cgit v1.2.3


From c63284e3f9d7723b24f2d226355747e91ebb06aa Mon Sep 17 00:00:00 2001
From: Son HO
Date: Thu, 11 Apr 2024 10:54:12 +0200
Subject: Update a comment

---
 compiler/Invariants.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/Invariants.ml')

diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 6e448cc4..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -825,7 +825,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
      * it must be expanded first *)
     if ty_has_borrows ctx.type_ctx.type_infos info.ty then
       sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
-    (* A duplicated symbolic value is necessarily primitively copyable *)
+    (* A duplicated symbolic value is necessarily copyable *)
     sanity_check __FILE__ __LINE__
       (info.env_count <= 1 || ty_is_copyable info.ty)
       meta;
-- 
cgit v1.2.3