From a64fdc8b1be70de43afe35ff788ba3240318daac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 15:02:17 +0100
Subject: WIP Beginning working on better errors: began replacing raise
 (Failure) and assert by craise and cassert. Does not compile yet, still need
 to propagate the meta variable where it's relevant

---
 compiler/InterpreterPaths.ml | 123 ++++++++++++++++++++++---------------------
 1 file changed, 62 insertions(+), 61 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 999b8ab0..e411db9b 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -8,6 +8,7 @@ open InterpreterUtils
 open InterpreterBorrowsCore
 open InterpreterBorrows
 open InterpreterExpansion
+open Errors
 module Synth = SynthesizeSymbolic
 
 (** The local logger *)
@@ -68,7 +69,7 @@ type projection_access = {
     
     TODO: use exceptions?
  *)
-let rec access_projection (access : projection_access) (ctx : eval_ctx)
+let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx : eval_ctx)
     (* Function to (eventually) update the value we find *)
       (update : typed_value -> typed_value) (p : projection) (v : typed_value) :
     (eval_ctx * updated_read_value) path_access_result =
@@ -85,10 +86,10 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
-        raise
-          (Failure
+        craise
+          meta
              "Assertion failed: new value doesn't have the same type as its \
-              destination"));
+              destination");
       Ok (ctx, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
@@ -101,10 +102,10 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
               assert (def_id = def_id');
               assert (opt_variant_id = adt.variant_id)
-          | _ -> raise (Failure "Unreachable"));
+          | _ -> craise meta "Unreachable");
           (* Actually project *)
           let fv = FieldId.nth adt.field_values field_id in
-          match access_projection access ctx update p' fv with
+          match access_projection meta access ctx update p' fv with
           | Error err -> Error err
           | Ok (ctx, res) ->
               (* Update the field value *)
@@ -119,7 +120,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           assert (arity = List.length adt.field_values);
           let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
-          match access_projection access ctx update p' fv with
+          match access_projection meta access ctx update p' fv with
           | Error err -> Error err
           | Ok (ctx, res) ->
               (* Update the field value *)
@@ -146,7 +147,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
            * it shouldn't happen due to user code, and we leverage it
            * when implementing box dereferencement for the concrete
            * interpreter *)
-          match access_projection access ctx update p' bv with
+          match access_projection meta access ctx update p' bv with
           | Error err -> Error err
           | Ok (ctx, res) ->
               let nv =
@@ -163,18 +164,18 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           | VSharedBorrow bid ->
               (* Lookup the loan content, and explore from there *)
               if access.lookup_shared_borrows then
-                match lookup_loan ek bid ctx with
+                match lookup_loan meta ek bid ctx with
                 | _, Concrete (VMutLoan _) ->
-                    raise (Failure "Expected a shared loan")
+                    craise meta "Expected a shared loan"
                 | _, Concrete (VSharedLoan (bids, sv)) -> (
                     (* Explore the shared value *)
-                    match access_projection access ctx update p' sv with
+                    match access_projection meta access ctx update p' sv with
                     | Error err -> Error err
                     | Ok (ctx, res) ->
                         (* Update the shared loan with the new value returned
                            by {!access_projection} *)
                         let ctx =
-                          update_loan ek bid
+                          update_loan meta ek bid
                             (VSharedLoan (bids, res.updated))
                             ctx
                         in
@@ -190,22 +191,22 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
                       | AEndedIgnoredMutLoan
                           { given_back = _; child = _; given_back_meta = _ }
                       | AIgnoredSharedLoan _ ) ) ->
-                    raise (Failure "Expected a shared (abstraction) loan")
+                    craise meta "Expected a shared (abstraction) loan"
                 | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
                     (* Explore the shared value *)
-                    match access_projection access ctx update p' sv with
+                    match access_projection meta access ctx update p' sv with
                     | Error err -> Error err
                     | Ok (ctx, res) ->
                         (* Relookup the child avalue *)
                         let av =
-                          match lookup_loan ek bid ctx with
+                          match lookup_loan meta ek bid ctx with
                           | _, Abstract (ASharedLoan (_, _, av)) -> av
-                          | _ -> raise (Failure "Unexpected")
+                          | _ -> craise meta "Unexpected"
                         in
                         (* Update the shared loan with the new value returned
                              by {!access_projection} *)
                         let ctx =
-                          update_aloan ek bid
+                          update_aloan meta ek bid
                             (ASharedLoan (bids, res.updated, av))
                             ctx
                         in
@@ -215,7 +216,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           | VReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
           | VMutBorrow (bid, bv) ->
               if access.enter_mut_borrows then
-                match access_projection access ctx update p' bv with
+                match access_projection meta access ctx update p' bv with
                 | Error err -> Error err
                 | Ok (ctx, res) ->
                     let nv =
@@ -231,7 +232,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
                  to the fact that we need to reexplore the *whole* place (i.e,
                  we mustn't ignore the current projection element *)
               if access.enter_shared_loans then
-                match access_projection access ctx update (pe :: p') sv with
+                match access_projection meta access ctx update (pe :: p') sv with
                 | Error err -> Error err
                 | Ok (ctx, res) ->
                     let nv =
@@ -245,7 +246,7 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
           let v = "- v:\n" ^ show_value v in
           let ty = "- ty:\n" ^ show_ety ty in
           log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          raise (Failure "Inconsistent projection"))
+          craise meta "Inconsistent projection")
 
 (** Generic function to access (read/write) the value at a given place.
 
@@ -253,14 +254,14 @@ let rec access_projection (access : projection_access) (ctx : eval_ctx)
     environment, if we managed to access the place, or the precise reason
     why we failed.
  *)
-let access_place (access : projection_access)
+let access_place (meta : Meta.meta) (access : projection_access)
     (* Function to (eventually) update the value we find *)
       (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
     (eval_ctx * typed_value) path_access_result =
   (* Lookup the variable's value *)
   let value = ctx_lookup_var_value ctx p.var_id in
   (* Apply the projection *)
-  match access_projection access ctx update p.projection value with
+  match access_projection meta access ctx update p.projection value with
   | Error err -> Error err
   | Ok (ctx, res) ->
       (* Update the value *)
@@ -300,12 +301,12 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
+let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx : eval_ctx) :
     typed_value path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
   let update v = v in
-  match access_place access update p ctx with
+  match access_place meta access update p ctx with
   | Error err -> Error err
   | Ok (ctx1, read_value) ->
       (* Note that we ignore the new environment: it should be the same as the
@@ -318,31 +319,31 @@ let try_read_place (access : access_kind) (p : place) (ctx : eval_ctx) :
             ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
           in
           log#serror msg;
-          raise (Failure "Unexpected environment update"));
+          craise meta "Unexpected environment update");
       Ok read_value
 
-let read_place (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value
+let read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value
     =
-  match try_read_place access p ctx with
-  | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
+  match try_read_place meta access p ctx with
+  | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
-let try_write_place (access : access_kind) (p : place) (nv : typed_value)
+let try_write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
   let update _ = nv in
-  match access_place access update p ctx with
+  match access_place meta access update p ctx with
   | Error err -> Error err
   | Ok (ctx, _) ->
       (* We ignore the read value *)
       Ok ctx
 
-let write_place (access : access_kind) (p : place) (nv : typed_value)
+let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : typed_value)
     (ctx : eval_ctx) : eval_ctx =
-  match try_write_place access p nv ctx with
-  | Error e -> raise (Failure ("Unreachable: " ^ show_path_fail_kind e))
+  match try_write_place meta access p nv ctx with
+  | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok ctx -> ctx
 
 let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id)
@@ -395,7 +396,7 @@ let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value =
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
 *)
-let expand_bottom_value_from_projection (access : access_kind) (p : place)
+let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind) (p : place)
     (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) :
     eval_ctx =
   (* Debugging *)
@@ -435,20 +436,20 @@ let expand_bottom_value_from_projection (access : access_kind) (p : place)
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value types
     | _ ->
-        raise
-          (Failure
-             ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty))
+        craise
+          meta
+             ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)
   in
   (* Update the context by inserting the expanded value at the proper place *)
-  match try_write_place access p' nv ctx with
+  match try_write_place meta access p' nv ctx with
   | Ok ctx -> ctx
-  | Error _ -> raise (Failure "Unreachable")
+  | Error _ -> craise meta "Unreachable"
 
-let rec update_ctx_along_read_place (config : config) (access : access_kind)
+let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
-  match try_read_place access p ctx with
+  match try_read_place meta access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       let cc =
@@ -467,17 +468,17 @@ let rec update_ctx_along_read_place (config : config) (access : access_kind)
               (Some (Synth.mk_mplace prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
-            raise (Failure "Found [Bottom] while reading a place")
-        | FailBorrow _ -> raise (Failure "Could not read a borrow")
+            craise meta "Found [Bottom] while reading a place"
+        | FailBorrow _ -> craise meta "Could not read a borrow"
       in
-      comp cc (update_ctx_along_read_place config access p) cf ctx
+      comp cc (update_ctx_along_read_place meta config access p) cf ctx
 
-let rec update_ctx_along_write_place (config : config) (access : access_kind)
+let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
-  match try_read_place access p ctx with
+  match try_read_place meta access p ctx with
   | Ok _ -> cf ctx
   | Error err ->
       (* Update the context *)
@@ -494,19 +495,19 @@ let rec update_ctx_along_write_place (config : config) (access : access_kind)
             (* Expand the {!Bottom} value *)
             fun cf ctx ->
              let ctx =
-               expand_bottom_value_from_projection access p remaining_pes pe ty
+               expand_bottom_value_from_projection meta access p remaining_pes pe ty
                  ctx
              in
              cf ctx
-        | FailBorrow _ -> raise (Failure "Could not write to a borrow")
+        | FailBorrow _ -> craise meta "Could not write to a borrow"
       in
       (* Retry *)
-      comp cc (update_ctx_along_write_place config access p) cf ctx
+      comp cc (update_ctx_along_write_place meta config access p) cf ctx
 
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-let rec end_loans_at_place (config : config) (access : access_kind) (p : place)
+let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access_kind) (p : place)
     : cm_fun =
  fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
@@ -545,7 +546,7 @@ let rec end_loans_at_place (config : config) (access : access_kind) (p : place)
   in
 
   (* First, retrieve the value *)
-  let v = read_place access p ctx in
+  let v = read_place meta access p ctx in
   (* Inspect the value and update the context while doing so.
      If the context gets updated: perform a recursive call (many things
      may have been updated in the context: we need to re-read the value
@@ -559,15 +560,15 @@ let rec end_loans_at_place (config : config) (access : access_kind) (p : place)
   with UpdateCtx cc ->
     (* We need to update the context: compose the caugth continuation with
      * a recursive call to reinspect the value *)
-    comp cc (end_loans_at_place config access p) cf ctx
+    comp cc (end_loans_at_place meta config access p) cf ctx
 
-let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
+let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
   let access = Write in
-  let v = read_place access p ctx in
-  let ctx = write_place access p (mk_bottom v.ty) ctx in
+  let v = read_place meta access p ctx in
+  let ctx = write_place meta access p (mk_bottom v.ty) ctx in
   let dummy_id = fresh_dummy_var_id () in
   let ctx = ctx_push_dummy_var ctx dummy_id v in
   (* Auxiliary function *)
@@ -587,7 +588,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
           match c with
           | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids
           | LoanContent (VMutLoan bid) -> end_borrow config bid
-          | BorrowContent _ -> raise (Failure "Unreachable")
+          | BorrowContent _ -> craise meta "Unreachable"
         in
         (* Retry *)
         comp cc drop cf ctx
@@ -600,7 +601,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
         (* Pop *)
         let ctx, v = ctx_remove_dummy_var ctx dummy_id in
         (* Reinsert *)
-        let ctx = write_place access p v ctx in
+        let ctx = write_place meta access p v ctx in
         (* Sanity check *)
         assert (not (outer_loans_in_value v));
         (* Continue *)
@@ -609,7 +610,7 @@ let drop_outer_loans_at_lplace (config : config) (p : place) : cm_fun =
   (* Continue *)
   cc cf ctx
 
-let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) :
+let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   log#ldebug
@@ -618,13 +619,13 @@ let prepare_lplace (config : config) (p : place) (cf : typed_value -> m_fun) :
      ^ "\n- Initial context:\n" ^ eval_ctx_to_string ctx));
   (* Access the place *)
   let access = Write in
-  let cc = update_ctx_along_write_place config access p in
+  let cc = update_ctx_along_write_place meta config access p in
   (* End the borrows and loans, starting with the borrows *)
-  let cc = comp cc (drop_outer_loans_at_lplace config p) in
+  let cc = comp cc (drop_outer_loans_at_lplace meta config p) in
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
-    let v = read_place access p ctx in
+    let v = read_place meta access p ctx in
     (* Sanity checks *)
     assert (not (outer_loans_in_value v));
     (* Continue *)
-- 
cgit v1.2.3


From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 17:19:14 +0100
Subject: WIP: does not compile yet because we need to propagate the meta
 variable.

---
 compiler/InterpreterPaths.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index e411db9b..cc1e3208 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -259,13 +259,13 @@ let access_place (meta : Meta.meta) (access : projection_access)
       (update : typed_value -> typed_value) (p : place) (ctx : eval_ctx) :
     (eval_ctx * typed_value) path_access_result =
   (* Lookup the variable's value *)
-  let value = ctx_lookup_var_value ctx p.var_id in
+  let value = ctx_lookup_var_value meta ctx p.var_id in
   (* Apply the projection *)
   match access_projection meta access ctx update p.projection value with
   | Error err -> Error err
   | Ok (ctx, res) ->
       (* Update the value *)
-      let ctx = ctx_update_var_value ctx p.var_id res.updated in
+      let ctx = ctx_update_var_value meta ctx p.var_id res.updated in
       (* Return *)
       Ok (ctx, res.read)
 
@@ -465,7 +465,7 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
             in
             let prefix = { p with projection = proj } in
             expand_symbolic_value_no_branching config sp
-              (Some (Synth.mk_mplace prefix ctx))
+              (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
             craise meta "Found [Bottom] while reading a place"
@@ -490,7 +490,7 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config sp
-              (Some (Synth.mk_mplace p ctx))
+              (Some (Synth.mk_mplace meta p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the {!Bottom} value *)
             fun cf ctx ->
@@ -575,7 +575,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   let rec drop : cm_fun =
    fun cf ctx ->
     (* Read the value *)
-    let v = ctx_lookup_dummy_var ctx dummy_id in
+    let v = ctx_lookup_dummy_var meta ctx dummy_id in
     (* Check if there are loans or borrows to end *)
     let with_borrows = false in
     match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -599,7 +599,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   let cc =
     comp cc (fun cf ctx ->
         (* Pop *)
-        let ctx, v = ctx_remove_dummy_var ctx dummy_id in
+        let ctx, v = ctx_remove_dummy_var meta ctx dummy_id in
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/InterpreterPaths.ml | 64 ++++++++++++++++++++++----------------------
 1 file changed, 32 insertions(+), 32 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index cc1e3208..c6db7f2e 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -100,8 +100,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
           (* Check consistency *)
           (match (proj_kind, type_id) with
           | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
-              assert (def_id = def_id');
-              assert (opt_variant_id = adt.variant_id)
+              cassert (def_id = def_id') meta "TODO: Error message";
+              cassert (opt_variant_id = adt.variant_id) meta "TODO: Error message"
           | _ -> craise meta "Unreachable");
           (* Actually project *)
           let fv = FieldId.nth adt.field_values field_id in
@@ -117,7 +117,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
               Ok (ctx, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
-          assert (arity = List.length adt.field_values);
+          cassert (arity = List.length adt.field_values) meta "TODO: Error message";
           let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
           match access_projection meta access ctx update p' fv with
@@ -346,30 +346,30 @@ let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : type
   | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok ctx -> ctx
 
-let compute_expanded_bottom_adt_value (ctx : eval_ctx) (def_id : TypeDeclId.id)
+let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id)
     (opt_variant_id : VariantId.id option) (generics : generic_args) :
-    typed_value =
-  assert (TypesUtils.generic_args_only_erased_regions generics);
+    typed_value = 
+  cassert (TypesUtils.generic_args_only_erased_regions generics) meta "TODO: Error message";
   (* 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
      of fields at the same time. *)
-  let def = ctx_lookup_type_decl ctx def_id in
-  assert (List.length generics.regions = List.length def.generics.regions);
+  let def = ctx_lookup_type_decl ctx def_id in (*TODO: check if can be moved before assert ?*)
+  cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
   (* Compute the field types *)
   let field_types =
     AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id
       generics
   in
   (* Initialize the expanded value *)
-  let fields = List.map mk_bottom field_types in
+  let fields = List.map (mk_bottom meta) field_types in
   let av = VAdt { variant_id = opt_variant_id; field_values = fields } in
   let ty = TAdt (TAdtId def_id, generics) in
   { value = av; ty }
 
-let compute_expanded_bottom_tuple_value (field_types : ety list) : typed_value =
+let compute_expanded_bottom_tuple_value (meta : Meta.meta) (field_types : ety list) : typed_value =
   (* Generate the field values *)
-  let fields = List.map mk_bottom field_types in
+  let fields = List.map (mk_bottom meta) field_types in
   let v = VAdt { variant_id = None; field_values = fields } in
   let generics = TypesUtils.mk_generic_args [] field_types [] [] in
   let ty = TAdt (TTuple, generics) in
@@ -425,16 +425,16 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         TAdt (TAdtId def_id', generics) ) ->
-        assert (def_id = def_id');
-        compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
+        cassert (def_id = def_id') meta "TODO: Error message";
+        compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id generics
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
         TAdt
           (TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
       ) ->
-        assert (arity = List.length types);
+        cassert (arity = List.length types) meta "TODO: Error message";
         (* Generate the field values *)
-        compute_expanded_bottom_tuple_value types
+        compute_expanded_bottom_tuple_value meta types
     | _ ->
         craise
           meta
@@ -454,9 +454,9 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
   | Error err ->
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows config bids
-        | FailMutLoan bid -> end_borrow config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid
+        | FailSharedLoan bids -> end_borrows meta config bids
+        | FailMutLoan bid -> end_borrow meta config bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
         | FailSymbolic (i, sp) ->
             (* Expand the symbolic value *)
             let proj, _ =
@@ -464,7 +464,7 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
                 (List.length p.projection - i)
             in
             let prefix = { p with projection = proj } in
-            expand_symbolic_value_no_branching config sp
+            expand_symbolic_value_no_branching meta config sp
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
@@ -484,12 +484,12 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
       (* Update the context *)
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows config bids
-        | FailMutLoan bid -> end_borrow config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config bid
+        | FailSharedLoan bids -> end_borrows meta config bids
+        | FailMutLoan bid -> end_borrow meta config bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching config sp
+            expand_symbolic_value_no_branching meta config sp
               (Some (Synth.mk_mplace meta p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the {!Bottom} value *)
@@ -525,7 +525,7 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             (* Nothing special to do *) super#visit_borrow_content env bc
         | VReservedMutBorrow bid ->
             (* We need to activate reserved borrows *)
-            let cc = promote_reserved_mut_borrow config bid in
+            let cc = promote_reserved_mut_borrow meta config bid in
             raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
@@ -536,11 +536,11 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             match access with
             | Read -> super#visit_VSharedLoan env bids v
             | Write | Move ->
-                let cc = end_borrows config bids in
+                let cc = end_borrows meta config bids in
                 raise (UpdateCtx cc))
         | VMutLoan bid ->
             (* We always need to end mutable borrows *)
-            let cc = end_borrow config bid in
+            let cc = end_borrow meta config bid in
             raise (UpdateCtx cc)
     end
   in
@@ -568,7 +568,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
    * a dummy variable *)
   let access = Write in
   let v = read_place meta access p ctx in
-  let ctx = write_place meta access p (mk_bottom v.ty) ctx in
+  let ctx = write_place meta access p (mk_bottom meta v.ty) ctx in
   let dummy_id = fresh_dummy_var_id () in
   let ctx = ctx_push_dummy_var ctx dummy_id v in
   (* Auxiliary function *)
@@ -586,8 +586,8 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
         (* There are: end them then retry *)
         let cc =
           match c with
-          | LoanContent (VSharedLoan (bids, _)) -> end_borrows config bids
-          | LoanContent (VMutLoan bid) -> end_borrow config bid
+          | LoanContent (VSharedLoan (bids, _)) -> end_borrows meta config bids
+          | LoanContent (VMutLoan bid) -> end_borrow meta config bid
           | BorrowContent _ -> craise meta "Unreachable"
         in
         (* Retry *)
@@ -603,7 +603,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
-        assert (not (outer_loans_in_value v));
+        cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
         (* Continue *)
         cf ctx)
   in
@@ -616,7 +616,7 @@ let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_
   log#ldebug
     (lazy
       ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
-     ^ "\n- Initial context:\n" ^ eval_ctx_to_string ctx));
+     ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx));
   (* Access the place *)
   let access = Write in
   let cc = update_ctx_along_write_place meta config access p in
@@ -627,7 +627,7 @@ let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_
    fun ctx ->
     let v = read_place meta access p ctx in
     (* Sanity checks *)
-    assert (not (outer_loans_in_value v));
+    cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
     (* Continue *)
     cf v ctx
   in
-- 
cgit v1.2.3


From 76fda6b5d205a4422c2360b676227690714c9ac5 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 22 Mar 2024 15:59:22 +0100
Subject: Still need to fill the TODO: error message and check some meta but it
 builds

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

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index c6db7f2e..c7141064 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -354,7 +354,7 @@ let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_i
      should be an enumeration if and only if the projection element
      is a field projection with *some* variant id. Retrieve the list
      of fields at the same time. *)
-  let def = ctx_lookup_type_decl ctx def_id in (*TODO: check if can be moved before assert ?*)
+  let def = ctx_lookup_type_decl ctx def_id in
   cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
   (* Compute the field types *)
   let field_types =
-- 
cgit v1.2.3


From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Mon, 25 Mar 2024 12:06:05 +0100
Subject: Inverted meta and config argument orders (from meta -> config to
 config -> meta)

---
 compiler/InterpreterPaths.ml | 46 ++++++++++++++++++++++----------------------
 1 file changed, 23 insertions(+), 23 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index c7141064..6ec12d6f 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -445,7 +445,7 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
   | Ok ctx -> ctx
   | Error _ -> craise meta "Unreachable"
 
-let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access : access_kind)
+let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
@@ -454,9 +454,9 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
   | Error err ->
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows meta config bids
-        | FailMutLoan bid -> end_borrow meta config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
+        | FailSharedLoan bids -> end_borrows config meta bids
+        | FailMutLoan bid -> end_borrow config meta bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
         | FailSymbolic (i, sp) ->
             (* Expand the symbolic value *)
             let proj, _ =
@@ -464,16 +464,16 @@ let rec update_ctx_along_read_place (meta : Meta.meta) (config : config) (access
                 (List.length p.projection - i)
             in
             let prefix = { p with projection = proj } in
-            expand_symbolic_value_no_branching meta config sp
+            expand_symbolic_value_no_branching config meta sp
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
             craise meta "Found [Bottom] while reading a place"
         | FailBorrow _ -> craise meta "Could not read a borrow"
       in
-      comp cc (update_ctx_along_read_place meta config access p) cf ctx
+      comp cc (update_ctx_along_read_place config meta access p) cf ctx
 
-let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (access : access_kind)
+let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (access : access_kind)
     (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
@@ -484,12 +484,12 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
       (* Update the context *)
       let cc =
         match err with
-        | FailSharedLoan bids -> end_borrows meta config bids
-        | FailMutLoan bid -> end_borrow meta config bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow meta config bid
+        | FailSharedLoan bids -> end_borrows config meta bids
+        | FailMutLoan bid -> end_borrow config meta bid
+        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
-            expand_symbolic_value_no_branching meta config sp
+            expand_symbolic_value_no_branching config meta sp
               (Some (Synth.mk_mplace meta p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
             (* Expand the {!Bottom} value *)
@@ -502,12 +502,12 @@ let rec update_ctx_along_write_place (meta : Meta.meta) (config : config) (acces
         | FailBorrow _ -> craise meta "Could not write to a borrow"
       in
       (* Retry *)
-      comp cc (update_ctx_along_write_place meta config access p) cf ctx
+      comp cc (update_ctx_along_write_place config meta access p) cf ctx
 
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access_kind) (p : place)
+let rec end_loans_at_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place)
     : cm_fun =
  fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
@@ -525,7 +525,7 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             (* Nothing special to do *) super#visit_borrow_content env bc
         | VReservedMutBorrow bid ->
             (* We need to activate reserved borrows *)
-            let cc = promote_reserved_mut_borrow meta config bid in
+            let cc = promote_reserved_mut_borrow config meta bid in
             raise (UpdateCtx cc)
 
       method! visit_loan_content env lc =
@@ -536,11 +536,11 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
             match access with
             | Read -> super#visit_VSharedLoan env bids v
             | Write | Move ->
-                let cc = end_borrows meta config bids in
+                let cc = end_borrows config meta bids in
                 raise (UpdateCtx cc))
         | VMutLoan bid ->
             (* We always need to end mutable borrows *)
-            let cc = end_borrow meta config bid in
+            let cc = end_borrow config meta bid in
             raise (UpdateCtx cc)
     end
   in
@@ -560,9 +560,9 @@ let rec end_loans_at_place (meta : Meta.meta) (config : config) (access : access
   with UpdateCtx cc ->
     (* We need to update the context: compose the caugth continuation with
      * a recursive call to reinspect the value *)
-    comp cc (end_loans_at_place meta config access p) cf ctx
+    comp cc (end_loans_at_place config meta access p) cf ctx
 
-let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place) : cm_fun =
+let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
@@ -586,8 +586,8 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
         (* There are: end them then retry *)
         let cc =
           match c with
-          | LoanContent (VSharedLoan (bids, _)) -> end_borrows meta config bids
-          | LoanContent (VMutLoan bid) -> end_borrow meta config bid
+          | LoanContent (VSharedLoan (bids, _)) -> end_borrows config meta bids
+          | LoanContent (VMutLoan bid) -> end_borrow config meta bid
           | BorrowContent _ -> craise meta "Unreachable"
         in
         (* Retry *)
@@ -610,7 +610,7 @@ let drop_outer_loans_at_lplace (meta : Meta.meta) (config : config) (p : place)
   (* Continue *)
   cc cf ctx
 
-let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_value -> m_fun) :
+let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_value -> m_fun) :
     m_fun =
  fun ctx ->
   log#ldebug
@@ -619,9 +619,9 @@ let prepare_lplace (meta : Meta.meta) (config : config) (p : place) (cf : typed_
      ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx));
   (* Access the place *)
   let access = Write in
-  let cc = update_ctx_along_write_place meta config access p in
+  let cc = update_ctx_along_write_place config meta access p in
   (* End the borrows and loans, starting with the borrows *)
-  let cc = comp cc (drop_outer_loans_at_lplace meta config p) in
+  let cc = comp cc (drop_outer_loans_at_lplace config meta p) in
   (* Read the value and check it *)
   let read_check cf : m_fun =
    fun ctx ->
-- 
cgit v1.2.3


From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 27 Mar 2024 10:22:06 +0100
Subject: Added sanity_check and sanity_check_opt_meta helpers and changed
 sanity checks related cassert to these helpers to have a proper error message

---
 compiler/InterpreterPaths.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 6ec12d6f..3733c06d 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -603,7 +603,7 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
-        cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
+        sanity_check (not (outer_loans_in_value v)) meta;
         (* Continue *)
         cf ctx)
   in
@@ -627,7 +627,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_
    fun ctx ->
     let v = read_place meta access p ctx in
     (* Sanity checks *)
-    cassert (not (outer_loans_in_value v)) meta "TODO: Error message";
+    sanity_check (not (outer_loans_in_value v)) meta;
     (* Continue *)
     cf v ctx
   in
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/InterpreterPaths.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 3733c06d..93ce0515 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -100,8 +100,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
           (* Check consistency *)
           (match (proj_kind, type_id) with
           | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
-              cassert (def_id = def_id') meta "TODO: Error message";
-              cassert (opt_variant_id = adt.variant_id) meta "TODO: Error message"
+              sanity_check (def_id = def_id') meta;
+              sanity_check (opt_variant_id = adt.variant_id) meta
           | _ -> craise meta "Unreachable");
           (* Actually project *)
           let fv = FieldId.nth adt.field_values field_id in
@@ -117,7 +117,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
               Ok (ctx, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
-          cassert (arity = List.length adt.field_values) meta "TODO: Error message";
+          sanity_check (arity = List.length adt.field_values) meta;
           let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
           match access_projection meta access ctx update p' fv with
@@ -349,16 +349,16 @@ let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : type
 let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id)
     (opt_variant_id : VariantId.id option) (generics : generic_args) :
     typed_value = 
-  cassert (TypesUtils.generic_args_only_erased_regions generics) meta "TODO: Error message";
+  sanity_check (TypesUtils.generic_args_only_erased_regions generics) meta;
   (* 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
      of fields at the same time. *)
   let def = ctx_lookup_type_decl ctx def_id in
-  cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
+  sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
   (* Compute the field types *)
   let field_types =
-    AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id
+    AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def opt_variant_id
       generics
   in
   (* Initialize the expanded value *)
@@ -425,14 +425,14 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         TAdt (TAdtId def_id', generics) ) ->
-        cassert (def_id = def_id') meta "TODO: Error message";
+        sanity_check (def_id = def_id') meta;
         compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id generics
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
         TAdt
           (TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
       ) ->
-        cassert (arity = List.length types) meta "TODO: Error message";
+        sanity_check (arity = List.length types) meta;
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value meta types
     | _ ->
@@ -616,7 +616,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_
   log#ldebug
     (lazy
       ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
-     ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx));
+     ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Access the place *)
   let access = Write in
   let cc = update_ctx_along_write_place config meta access p in
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/InterpreterPaths.ml | 93 ++++++++++++++++++++++++--------------------
 1 file changed, 51 insertions(+), 42 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 93ce0515..c386c2db 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -69,7 +69,8 @@ type projection_access = {
     
     TODO: use exceptions?
  *)
-let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx : eval_ctx)
+let rec access_projection (meta : Meta.meta) (access : projection_access)
+    (ctx : eval_ctx)
     (* Function to (eventually) update the value we find *)
       (update : typed_value -> typed_value) (p : projection) (v : typed_value) :
     (eval_ctx * updated_read_value) path_access_result =
@@ -86,10 +87,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
-        craise
-          meta
-             "Assertion failed: new value doesn't have the same type as its \
-              destination");
+        craise meta
+          "Assertion failed: new value doesn't have the same type as its \
+           destination");
       Ok (ctx, { read = v; updated = nv })
   | pe :: p' -> (
       (* Match on the projection element and the value *)
@@ -232,7 +232,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
                  to the fact that we need to reexplore the *whole* place (i.e,
                  we mustn't ignore the current projection element *)
               if access.enter_shared_loans then
-                match access_projection meta access ctx update (pe :: p') sv with
+                match
+                  access_projection meta access ctx update (pe :: p') sv
+                with
                 | Error err -> Error err
                 | Ok (ctx, res) ->
                     let nv =
@@ -301,8 +303,8 @@ let access_kind_to_projection_access (access : access_kind) : projection_access
     Note that we only access the value at the place, and do not check that
     the value is "well-formed" (for instance that it doesn't contain bottoms).
  *)
-let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx : eval_ctx) :
-    typed_value path_access_result =
+let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
+    (ctx : eval_ctx) : typed_value path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function is the identity *)
   let update v = v in
@@ -322,15 +324,15 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx :
           craise meta "Unexpected environment update");
       Ok read_value
 
-let read_place (meta : Meta.meta) (access : access_kind) (p : place) (ctx : eval_ctx) : typed_value
-    =
+let read_place (meta : Meta.meta) (access : access_kind) (p : place)
+    (ctx : eval_ctx) : typed_value =
   match try_read_place meta access p ctx with
   | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
-let try_write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : typed_value)
-    (ctx : eval_ctx) : eval_ctx path_access_result =
+let try_write_place (meta : Meta.meta) (access : access_kind) (p : place)
+    (nv : typed_value) (ctx : eval_ctx) : eval_ctx path_access_result =
   let access = access_kind_to_projection_access access in
   (* The update function substitutes the value with the new value *)
   let update _ = nv in
@@ -340,26 +342,28 @@ let try_write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv :
       (* We ignore the read value *)
       Ok ctx
 
-let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : typed_value)
-    (ctx : eval_ctx) : eval_ctx =
+let write_place (meta : Meta.meta) (access : access_kind) (p : place)
+    (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   match try_write_place meta access p nv ctx with
   | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok ctx -> ctx
 
-let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id)
-    (opt_variant_id : VariantId.id option) (generics : generic_args) :
-    typed_value = 
+let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx)
+    (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
+    (generics : generic_args) : typed_value =
   sanity_check (TypesUtils.generic_args_only_erased_regions generics) meta;
   (* 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
      of fields at the same time. *)
   let def = ctx_lookup_type_decl ctx def_id in
-  sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
+  sanity_check
+    (List.length generics.regions = List.length def.generics.regions)
+    meta;
   (* Compute the field types *)
   let field_types =
-    AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def opt_variant_id
-      generics
+    AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def
+      opt_variant_id generics
   in
   (* Initialize the expanded value *)
   let fields = List.map (mk_bottom meta) field_types in
@@ -367,7 +371,8 @@ let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_i
   let ty = TAdt (TAdtId def_id, generics) in
   { value = av; ty }
 
-let compute_expanded_bottom_tuple_value (meta : Meta.meta) (field_types : ety list) : typed_value =
+let compute_expanded_bottom_tuple_value (meta : Meta.meta)
+    (field_types : ety list) : typed_value =
   (* Generate the field values *)
   let fields = List.map (mk_bottom meta) field_types in
   let v = VAdt { variant_id = None; field_values = fields } in
@@ -396,9 +401,9 @@ let compute_expanded_bottom_tuple_value (meta : Meta.meta) (field_types : ety li
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
 *)
-let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind) (p : place)
-    (remaining_pes : int) (pe : projection_elem) (ty : ety) (ctx : eval_ctx) :
-    eval_ctx =
+let expand_bottom_value_from_projection (meta : Meta.meta)
+    (access : access_kind) (p : place) (remaining_pes : int)
+    (pe : projection_elem) (ty : ety) (ctx : eval_ctx) : eval_ctx =
   (* Debugging *)
   log#ldebug
     (lazy
@@ -426,7 +431,8 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         TAdt (TAdtId def_id', generics) ) ->
         sanity_check (def_id = def_id') meta;
-        compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id generics
+        compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id
+          generics
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
         TAdt
@@ -436,17 +442,16 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value meta types
     | _ ->
-        craise
-          meta
-             ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)
+        craise meta
+          ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)
   in
   (* Update the context by inserting the expanded value at the proper place *)
   match try_write_place meta access p' nv ctx with
   | Ok ctx -> ctx
   | Error _ -> craise meta "Unreachable"
 
-let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access : access_kind)
-    (p : place) : cm_fun =
+let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
+    (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to read the place: if it fails, update the environment and retry *)
   match try_read_place meta access p ctx with
@@ -456,7 +461,8 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access
         match err with
         | FailSharedLoan bids -> end_borrows config meta bids
         | FailMutLoan bid -> end_borrow config meta bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
+        | FailReservedMutBorrow bid ->
+            promote_reserved_mut_borrow config meta bid
         | FailSymbolic (i, sp) ->
             (* Expand the symbolic value *)
             let proj, _ =
@@ -473,8 +479,8 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta) (access
       in
       comp cc (update_ctx_along_read_place config meta access p) cf ctx
 
-let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (access : access_kind)
-    (p : place) : cm_fun =
+let rec update_ctx_along_write_place (config : config) (meta : Meta.meta)
+    (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Attempt to *read* (yes, *read*: we check the access to the place, and
      write to it later) the place: if it fails, update the environment and retry *)
@@ -486,7 +492,8 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (acces
         match err with
         | FailSharedLoan bids -> end_borrows config meta bids
         | FailMutLoan bid -> end_borrow config meta bid
-        | FailReservedMutBorrow bid -> promote_reserved_mut_borrow config meta bid
+        | FailReservedMutBorrow bid ->
+            promote_reserved_mut_borrow config meta bid
         | FailSymbolic (_pe, sp) ->
             (* Expand the symbolic value *)
             expand_symbolic_value_no_branching config meta sp
@@ -495,8 +502,8 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (acces
             (* Expand the {!Bottom} value *)
             fun cf ctx ->
              let ctx =
-               expand_bottom_value_from_projection meta access p remaining_pes pe ty
-                 ctx
+               expand_bottom_value_from_projection meta access p remaining_pes
+                 pe ty ctx
              in
              cf ctx
         | FailBorrow _ -> craise meta "Could not write to a borrow"
@@ -507,8 +514,8 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta) (acces
 (** Small utility used to break control-flow *)
 exception UpdateCtx of cm_fun
 
-let rec end_loans_at_place (config : config) (meta : Meta.meta) (access : access_kind) (p : place)
-    : cm_fun =
+let rec end_loans_at_place (config : config) (meta : Meta.meta)
+    (access : access_kind) (p : place) : cm_fun =
  fun cf ctx ->
   (* Iterator to explore a value and update the context whenever we find
    * loans.
@@ -562,7 +569,8 @@ let rec end_loans_at_place (config : config) (meta : Meta.meta) (access : access
      * a recursive call to reinspect the value *)
     comp cc (end_loans_at_place config meta access p) cf ctx
 
-let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place) : cm_fun =
+let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
+    : cm_fun =
  fun cf ctx ->
   (* Move the current value in the place outside of this place and into
    * a dummy variable *)
@@ -610,13 +618,14 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
   (* Continue *)
   cc cf ctx
 
-let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_value -> m_fun) :
-    m_fun =
+let prepare_lplace (config : config) (meta : Meta.meta) (p : place)
+    (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug
     (lazy
       ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
-     ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
+     ^ "\n- Initial context:\n"
+      ^ eval_ctx_to_string ~meta:(Some meta) ctx));
   (* Access the place *)
   let access = Write in
   let cc = update_ctx_along_write_place config meta access p in
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/InterpreterPaths.ml | 48 ++++++++++++++++++++++----------------------
 1 file changed, 24 insertions(+), 24 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index c386c2db..26456acf 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -87,7 +87,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           (lazy
             ("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
            ^ show_ety v.ty));
-        craise meta
+        craise __FILE__ __LINE__ meta
           "Assertion failed: new value doesn't have the same type as its \
            destination");
       Ok (ctx, { read = v; updated = nv })
@@ -100,9 +100,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           (* Check consistency *)
           (match (proj_kind, type_id) with
           | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
-              sanity_check (def_id = def_id') meta;
-              sanity_check (opt_variant_id = adt.variant_id) meta
-          | _ -> craise meta "Unreachable");
+              sanity_check __FILE__ __LINE__ (def_id = def_id') meta;
+              sanity_check __FILE__ __LINE__ (opt_variant_id = adt.variant_id) meta
+          | _ -> craise __FILE__ __LINE__ meta "Unreachable");
           (* Actually project *)
           let fv = FieldId.nth adt.field_values field_id in
           match access_projection meta access ctx update p' fv with
@@ -117,7 +117,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
               Ok (ctx, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
-          sanity_check (arity = List.length adt.field_values) meta;
+          sanity_check __FILE__ __LINE__ (arity = List.length adt.field_values) meta;
           let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
           match access_projection meta access ctx update p' fv with
@@ -166,7 +166,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
               if access.lookup_shared_borrows then
                 match lookup_loan meta ek bid ctx with
                 | _, Concrete (VMutLoan _) ->
-                    craise meta "Expected a shared loan"
+                    craise __FILE__ __LINE__ meta "Expected a shared loan"
                 | _, Concrete (VSharedLoan (bids, sv)) -> (
                     (* Explore the shared value *)
                     match access_projection meta access ctx update p' sv with
@@ -191,7 +191,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
                       | AEndedIgnoredMutLoan
                           { given_back = _; child = _; given_back_meta = _ }
                       | AIgnoredSharedLoan _ ) ) ->
-                    craise meta "Expected a shared (abstraction) loan"
+                    craise __FILE__ __LINE__ meta "Expected a shared (abstraction) loan"
                 | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
                     (* Explore the shared value *)
                     match access_projection meta access ctx update p' sv with
@@ -201,7 +201,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
                         let av =
                           match lookup_loan meta ek bid ctx with
                           | _, Abstract (ASharedLoan (_, _, av)) -> av
-                          | _ -> craise meta "Unexpected"
+                          | _ -> craise __FILE__ __LINE__ meta "Unexpected"
                         in
                         (* Update the shared loan with the new value returned
                              by {!access_projection} *)
@@ -248,7 +248,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           let v = "- v:\n" ^ show_value v in
           let ty = "- ty:\n" ^ show_ety ty in
           log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
-          craise meta "Inconsistent projection")
+          craise __FILE__ __LINE__ meta "Inconsistent projection")
 
 (** Generic function to access (read/write) the value at a given place.
 
@@ -321,13 +321,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
             ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
           in
           log#serror msg;
-          craise meta "Unexpected environment update");
+          craise __FILE__ __LINE__ meta "Unexpected environment update");
       Ok read_value
 
 let read_place (meta : Meta.meta) (access : access_kind) (p : place)
     (ctx : eval_ctx) : typed_value =
   match try_read_place meta access p ctx with
-  | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
+  | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
@@ -345,19 +345,19 @@ let try_write_place (meta : Meta.meta) (access : access_kind) (p : place)
 let write_place (meta : Meta.meta) (access : access_kind) (p : place)
     (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   match try_write_place meta access p nv ctx with
-  | Error e -> craise meta ("Unreachable: " ^ show_path_fail_kind e)
+  | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok ctx -> ctx
 
 let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx)
     (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
     (generics : generic_args) : typed_value =
-  sanity_check (TypesUtils.generic_args_only_erased_regions generics) meta;
+  sanity_check __FILE__ __LINE__ (TypesUtils.generic_args_only_erased_regions generics) meta;
   (* 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
      of fields at the same time. *)
   let def = ctx_lookup_type_decl ctx def_id in
-  sanity_check
+  sanity_check __FILE__ __LINE__
     (List.length generics.regions = List.length def.generics.regions)
     meta;
   (* Compute the field types *)
@@ -430,7 +430,7 @@ let expand_bottom_value_from_projection (meta : Meta.meta)
     (* "Regular" ADTs *)
     | ( Field (ProjAdt (def_id, opt_variant_id), _),
         TAdt (TAdtId def_id', generics) ) ->
-        sanity_check (def_id = def_id') meta;
+        sanity_check __FILE__ __LINE__ (def_id = def_id') meta;
         compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id
           generics
     (* Tuples *)
@@ -438,17 +438,17 @@ let expand_bottom_value_from_projection (meta : Meta.meta)
         TAdt
           (TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
       ) ->
-        sanity_check (arity = List.length types) meta;
+        sanity_check __FILE__ __LINE__ (arity = List.length types) meta;
         (* Generate the field values *)
         compute_expanded_bottom_tuple_value meta types
     | _ ->
-        craise meta
+        craise __FILE__ __LINE__ meta
           ("Unreachable: " ^ show_projection_elem pe ^ ", " ^ show_ety ty)
   in
   (* Update the context by inserting the expanded value at the proper place *)
   match try_write_place meta access p' nv ctx with
   | Ok ctx -> ctx
-  | Error _ -> craise meta "Unreachable"
+  | Error _ -> craise __FILE__ __LINE__ meta "Unreachable"
 
 let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
     (access : access_kind) (p : place) : cm_fun =
@@ -474,8 +474,8 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
-            craise meta "Found [Bottom] while reading a place"
-        | FailBorrow _ -> craise meta "Could not read a borrow"
+            craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place"
+        | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not read a borrow"
       in
       comp cc (update_ctx_along_read_place config meta access p) cf ctx
 
@@ -506,7 +506,7 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta)
                  pe ty ctx
              in
              cf ctx
-        | FailBorrow _ -> craise meta "Could not write to a borrow"
+        | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not write to a borrow"
       in
       (* Retry *)
       comp cc (update_ctx_along_write_place config meta access p) cf ctx
@@ -596,7 +596,7 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
           match c with
           | LoanContent (VSharedLoan (bids, _)) -> end_borrows config meta bids
           | LoanContent (VMutLoan bid) -> end_borrow config meta bid
-          | BorrowContent _ -> craise meta "Unreachable"
+          | BorrowContent _ -> craise __FILE__ __LINE__ meta "Unreachable"
         in
         (* Retry *)
         comp cc drop cf ctx
@@ -611,7 +611,7 @@ let drop_outer_loans_at_lplace (config : config) (meta : Meta.meta) (p : place)
         (* Reinsert *)
         let ctx = write_place meta access p v ctx in
         (* Sanity check *)
-        sanity_check (not (outer_loans_in_value v)) meta;
+        sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta;
         (* Continue *)
         cf ctx)
   in
@@ -636,7 +636,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place)
    fun ctx ->
     let v = read_place meta access p ctx in
     (* Sanity checks *)
-    sanity_check (not (outer_loans_in_value v)) meta;
+    sanity_check __FILE__ __LINE__ (not (outer_loans_in_value v)) meta;
     (* Continue *)
     cf v ctx
   in
-- 
cgit v1.2.3


From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 14:07:36 +0100
Subject: formatting and changed save_error condition for failing from b to not
 b

---
 compiler/InterpreterPaths.ml | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 26456acf..93e56106 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -101,7 +101,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
           (match (proj_kind, type_id) with
           | ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
               sanity_check __FILE__ __LINE__ (def_id = def_id') meta;
-              sanity_check __FILE__ __LINE__ (opt_variant_id = adt.variant_id) meta
+              sanity_check __FILE__ __LINE__
+                (opt_variant_id = adt.variant_id)
+                meta
           | _ -> craise __FILE__ __LINE__ meta "Unreachable");
           (* Actually project *)
           let fv = FieldId.nth adt.field_values field_id in
@@ -117,7 +119,9 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
               Ok (ctx, { res with updated }))
       (* Tuples *)
       | Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
-          sanity_check __FILE__ __LINE__ (arity = List.length adt.field_values) meta;
+          sanity_check __FILE__ __LINE__
+            (arity = List.length adt.field_values)
+            meta;
           let fv = FieldId.nth adt.field_values field_id in
           (* Project *)
           match access_projection meta access ctx update p' fv with
@@ -191,7 +195,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
                       | AEndedIgnoredMutLoan
                           { given_back = _; child = _; given_back_meta = _ }
                       | AIgnoredSharedLoan _ ) ) ->
-                    craise __FILE__ __LINE__ meta "Expected a shared (abstraction) loan"
+                    craise __FILE__ __LINE__ meta
+                      "Expected a shared (abstraction) loan"
                 | _, Abstract (ASharedLoan (bids, sv, _av)) -> (
                     (* Explore the shared value *)
                     match access_projection meta access ctx update p' sv with
@@ -327,7 +332,8 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
 let read_place (meta : Meta.meta) (access : access_kind) (p : place)
     (ctx : eval_ctx) : typed_value =
   match try_read_place meta access p ctx with
-  | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
+  | Error e ->
+      craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok v -> v
 
 (** Attempt to update the value at a given place *)
@@ -345,13 +351,16 @@ let try_write_place (meta : Meta.meta) (access : access_kind) (p : place)
 let write_place (meta : Meta.meta) (access : access_kind) (p : place)
     (nv : typed_value) (ctx : eval_ctx) : eval_ctx =
   match try_write_place meta access p nv ctx with
-  | Error e -> craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
+  | Error e ->
+      craise __FILE__ __LINE__ meta ("Unreachable: " ^ show_path_fail_kind e)
   | Ok ctx -> ctx
 
 let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx)
     (def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
     (generics : generic_args) : typed_value =
-  sanity_check __FILE__ __LINE__ (TypesUtils.generic_args_only_erased_regions generics) meta;
+  sanity_check __FILE__ __LINE__
+    (TypesUtils.generic_args_only_erased_regions generics)
+    meta;
   (* 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
@@ -475,7 +484,8 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
             craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place"
-        | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not read a borrow"
+        | FailBorrow _ ->
+            craise __FILE__ __LINE__ meta "Could not read a borrow"
       in
       comp cc (update_ctx_along_read_place config meta access p) cf ctx
 
@@ -506,7 +516,8 @@ let rec update_ctx_along_write_place (config : config) (meta : Meta.meta)
                  pe ty ctx
              in
              cf ctx
-        | FailBorrow _ -> craise __FILE__ __LINE__ meta "Could not write to a borrow"
+        | FailBorrow _ ->
+            craise __FILE__ __LINE__ meta "Could not write to a borrow"
       in
       (* Retry *)
       comp cc (update_ctx_along_write_place config meta access p) cf ctx
-- 
cgit v1.2.3


From 1a86cac476c1f5c0d64d5a12db267d3ac651561b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 17:49:46 +0100
Subject: Cleanup and fix a mistake

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

(limited to 'compiler/InterpreterPaths.ml')

diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 93e56106..f2c0bcb1 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -483,7 +483,7 @@ let rec update_ctx_along_read_place (config : config) (meta : Meta.meta)
               (Some (Synth.mk_mplace meta prefix ctx))
         | FailBottom (_, _, _) ->
             (* We can't expand {!Bottom} values while reading them *)
-            craise __FILE__ __LINE__ meta "Found [Bottom] while reading a place"
+            craise __FILE__ __LINE__ meta "Found bottom while reading a place"
         | FailBorrow _ ->
             craise __FILE__ __LINE__ meta "Could not read a borrow"
       in
-- 
cgit v1.2.3