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

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 7c3f6199..d727e9bd 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -60,7 +60,7 @@ val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun
 
     we only introduce a fresh abstraction for [l1].
   *)
-val prepare_ashared_loans : loop_id option -> Cps.cm_fun
+val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
 
 (** Compute a fixed-point for the context at the entry of the loop.
     We also return:
@@ -77,6 +77,7 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun
     the values which are read or modified (some symbolic values may be ignored).
  *)
 val compute_loop_entry_fixed_point :
+  Meta.meta -> 
   config ->
   loop_id ->
   Cps.st_cm_fun ->
@@ -160,7 +161,7 @@ val compute_loop_entry_fixed_point :
     through the loan [l1] is actually the value which has to be given back to [l0].
  *)
 val compute_fixed_point_id_correspondance :
-  ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp
+  Meta.meta -> ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp
 
 (** Compute the set of "quantified" symbolic value ids in a fixed-point context.
 
@@ -169,4 +170,4 @@ val compute_fixed_point_id_correspondance :
     - the list of input symbolic values
  *)
 val compute_fp_ctx_symbolic_values :
-  eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list
+  Meta.meta -> eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list
-- 
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/InterpreterLoopsFixedPoint.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index d727e9bd..4568bf79 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -77,8 +77,8 @@ val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
     the values which are read or modified (some symbolic values may be ignored).
  *)
 val compute_loop_entry_fixed_point :
-  Meta.meta -> 
-  config ->
+  config -> 
+  Meta.meta ->
   loop_id ->
   Cps.st_cm_fun ->
   eval_ctx ->
-- 
cgit v1.2.3


From 53347ecc40b308b0b75a620453bfa8bd520a2c70 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 16:31:24 +0100
Subject: changes after git rebase main

---
 compiler/InterpreterLoopsFixedPoint.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 4568bf79..54e4d780 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -13,7 +13,7 @@ open InterpreterLoopsCore
    - config
    - fixed ids (the fixeds ids are the ids we consider as non-fresh)
  *)
-val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun
+val cleanup_fresh_values_and_abs : config -> Meta.meta -> ids_sets -> Cps.cm_fun
 
 (** Prepare the shared loans in the abstractions by moving them to fresh
     abstractions.
-- 
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/InterpreterLoopsFixedPoint.mli | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 54e4d780..4fc36598 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -77,7 +77,7 @@ val prepare_ashared_loans : Meta.meta -> loop_id option -> Cps.cm_fun
     the values which are read or modified (some symbolic values may be ignored).
  *)
 val compute_loop_entry_fixed_point :
-  config -> 
+  config ->
   Meta.meta ->
   loop_id ->
   Cps.st_cm_fun ->
@@ -170,4 +170,7 @@ val compute_fixed_point_id_correspondance :
     - the list of input symbolic values
  *)
 val compute_fp_ctx_symbolic_values :
-  Meta.meta -> eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list
+  Meta.meta ->
+  eval_ctx ->
+  eval_ctx ->
+  symbolic_value_id_set * symbolic_value list
-- 
cgit v1.2.3