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/InterpreterProjectors.mli | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'compiler/InterpreterProjectors.mli')

diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 9e4ebc20..7ffe4917 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -15,11 +15,11 @@ open Contexts
     [original_sv_ty]: shouldn't have erased regions
 *)
 val apply_proj_loans_on_symbolic_expansion :
-  RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> rty -> typed_avalue
+  Meta.meta -> RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> rty -> typed_avalue
 
 (** Convert a symbolic expansion *which is not a borrow* to a value *)
 val symbolic_expansion_non_borrow_to_value :
-  symbolic_value -> symbolic_expansion -> typed_value
+  Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
 
 (** Convert a symbolic expansion *which is not a shared borrow* to a value.
 
@@ -28,7 +28,7 @@ val symbolic_expansion_non_borrow_to_value :
     during a symbolic expansion.
   *)
 val symbolic_expansion_non_shared_borrow_to_value :
-  symbolic_value -> symbolic_expansion -> typed_value
+ Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
 
 (** Auxiliary function to prepare reborrowing operations (used when
     applying projectors).
@@ -43,7 +43,7 @@ val symbolic_expansion_non_shared_borrow_to_value :
     - [allow_reborrows]
  *)
 val prepare_reborrows :
-  config -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
+  Meta.meta -> config -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
 
 (** Apply (and reduce) a projector over borrows to an avalue.
     We use this for instance to spread the borrows present in the inputs
@@ -96,6 +96,7 @@ val prepare_reborrows :
       then we interpret the borrow [l] as belonging to region [r]
 *)
 val apply_proj_borrows :
+  Meta.meta ->
   bool ->
   eval_ctx ->
   (BorrowId.id -> BorrowId.id) ->
@@ -115,6 +116,7 @@ val apply_proj_borrows :
       erased regions)
  *)
 val apply_proj_borrows_on_input_value :
+  Meta.meta ->
   config ->
   eval_ctx ->
   RegionId.Set.t ->
-- 
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/InterpreterProjectors.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterProjectors.mli')

diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 7ffe4917..64ad1b29 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -43,7 +43,7 @@ val symbolic_expansion_non_shared_borrow_to_value :
     - [allow_reborrows]
  *)
 val prepare_reborrows :
-  Meta.meta -> config -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
+  config -> Meta.meta -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
 
 (** Apply (and reduce) a projector over borrows to an avalue.
     We use this for instance to spread the borrows present in the inputs
@@ -116,8 +116,8 @@ val apply_proj_borrows :
       erased regions)
  *)
 val apply_proj_borrows_on_input_value :
-  Meta.meta ->
   config ->
+  Meta.meta ->
   eval_ctx ->
   RegionId.Set.t ->
   RegionId.Set.t ->
-- 
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/InterpreterProjectors.mli | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'compiler/InterpreterProjectors.mli')

diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
index 64ad1b29..17569ac8 100644
--- a/compiler/InterpreterProjectors.mli
+++ b/compiler/InterpreterProjectors.mli
@@ -15,7 +15,12 @@ open Contexts
     [original_sv_ty]: shouldn't have erased regions
 *)
 val apply_proj_loans_on_symbolic_expansion :
-  Meta.meta -> RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> rty -> typed_avalue
+  Meta.meta ->
+  RegionId.Set.t ->
+  RegionId.Set.t ->
+  symbolic_expansion ->
+  rty ->
+  typed_avalue
 
 (** Convert a symbolic expansion *which is not a borrow* to a value *)
 val symbolic_expansion_non_borrow_to_value :
@@ -28,7 +33,7 @@ val symbolic_expansion_non_borrow_to_value :
     during a symbolic expansion.
   *)
 val symbolic_expansion_non_shared_borrow_to_value :
- Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
+  Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value
 
 (** Auxiliary function to prepare reborrowing operations (used when
     applying projectors).
@@ -43,7 +48,10 @@ val symbolic_expansion_non_shared_borrow_to_value :
     - [allow_reborrows]
  *)
 val prepare_reborrows :
-  config -> Meta.meta -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
+  config ->
+  Meta.meta ->
+  bool ->
+  (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx)
 
 (** Apply (and reduce) a projector over borrows to an avalue.
     We use this for instance to spread the borrows present in the inputs
-- 
cgit v1.2.3