Make minor modifications

3 files changed, 16 insertions, 75 deletions

diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 0e36f6df..64151a48 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -10,8 +10,8 @@ type var = {
   name : string option;
   var_ty : ety;
       (** The variable type - erased type, because variables are not used
-       ** in function signatures - TODO: useless? TODO: binder type for
-          function definitions *)
+       ** in function signatures: they are only used to declare the list of
+       ** variables manipulated by a function body *)
 }
 [@@deriving show]
 (** A variable, as used in a function definition *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5ffc0908..d34c20dc 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -90,23 +90,6 @@ let borrows_in_value (v : V.typed_value) : bool =
     false
   with Found -> true
 
-(** Check a predicate on all the loans in a value - TODO: remove? *)
-let forall_borrows_in_value (pred : V.borrow_content -> bool)
-    (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value as super
-
-      method! visit_borrow_content env lc =
-        if not (pred lc) then raise Found else super#visit_borrow_content env lc
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    true
-  with Found -> false
-
 (** Check if a value contains inactivated mutable borrows *)
 let inactivated_in_value (v : V.typed_value) : bool =
   let obj =
@@ -137,43 +120,6 @@ let loans_in_value (v : V.typed_value) : bool =
     false
   with Found -> true
 
-(** Check a predicate on all the loans in a value - TODO: remove?*)
-let forall_loans_in_value (pred : V.loan_content -> bool) (v : V.typed_value) :
-    bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value as super
-
-      method! visit_loan_content env lc =
-        if not (pred lc) then raise Found else super#visit_loan_content env lc
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    true
-  with Found -> false
-
-(** Return true if there are mutable borrows/loans or inactivated mut borrows
-    in the value - TODO: remove? *)
-let mut_inactivated_borrows_loans_in_value (v : V.typed_value) : bool =
-  let obj =
-    object
-      inherit [_] V.iter_typed_value
-
-      method! visit_MutLoan _ _ = raise Found
-
-      method! visit_MutBorrow _ _ = raise Found
-
-      method! visit_InactivatedMutBorrow _ _ = raise Found
-    end
-  in
-  (* We use exceptions *)
-  try
-    obj#visit_typed_value () v;
-    false
-  with Found -> true
-
 (** Lookup a loan content.
 
     The loan is referred to by a borrow id.
@@ -821,11 +767,13 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id) (ctx : C.eval_ctx) :
       (* Check that there is only one borrow id (l) and update the loan *)
       assert (V.BorrowId.Set.mem l bids && V.BorrowId.Set.cardinal bids = 1);
       (* We need to check that there aren't any loans in the value:
-           we should have gotten rid of those already, but it is better
-           to do a sanity check. *)
+         we should have gotten rid of those already, but it is better
+         to do a sanity check. *)
       assert (not (loans_in_value sv));
-      (* Also need to check there isn't [Bottom] (this is actually an invariant *)
+      (* Check there isn't [Bottom] (this is actually an invariant *)
       assert (not (bottom_in_value sv));
+      (* Check there aren't inactivated borrows *)
+      assert (not (inactivated_in_value sv));
       (* Update the loan content *)
       let env = update_loan ek l (V.MutLoan l) ctx.env in
       let ctx = { ctx with env } in
@@ -1878,7 +1826,7 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
           let aty = T.Adt (T.AdtId def_id, regions, types) in
           Ok (ctx, { V.value = Adt av; ty = aty }))
 
-(** Result of evaluating a statement - TODO: add prefix *)
+(** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return
 
 (** Small utility.
diff --git a/src/Values.ml b/src/Values.ml
index aabd41c2..78923e5e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -1,12 +1,6 @@
 open Identifiers
 open Types
 
-(** TODO: do we put the type variable/variable/region names everywhere
-    (to not have to perform lookups by using the ids?)
-    No: it is good not to duplicate and to use ids. This allows to split/
-    make very explicit the role of variables/identifiers/binders/etc.
- *)
-
 module VarId = IdGen ()
 
 module BorrowId = IdGen ()
@@ -199,22 +193,21 @@ class ['self] map_typed_avalue_base =
     method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
   end
 
+(** Abstraction values are used inside of abstractions to properly model
+    borrowing relations introduced by function calls.
+
+    When calling a function, we lose information about the borrow graph:
+    part of it is thus "abstracted" away.
+*)
 type avalue =
   | AConcrete of constant_value
-  | AAdt of aadt_value
+  | AAdt of adt_avalue
   | ABottom
   | ALoan of aloan_content
   | ABorrow of aborrow_content
   | ASymbolic of aproj
-      (** Abstraction values are used inside of abstractions to properly model
-    borrowing relations introduced by function calls.
-
-    When calling a function, we lose information about the borrow graph:
-    part of it is thus "abstracted" away.
-*)
 
-(* TODO: rename to adt_avalue? *)
-and aadt_value = {
+and adt_avalue = {
   variant_id : (VariantId.id option[@opaque]);
   field_values : typed_avalue list;
 }