From cd99485fa2493697b2b3775a5cae80bf9bf58a99 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 19:33:08 +0100
Subject: Make progress on fixing the loops

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

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 65a76359..c0e5dca5 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -56,6 +56,8 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun
     - the map from region group id to the corresponding abstraction appearing
       in the fixed point (this is useful to compute the return type of the loop
       backward functions for instance).
+      Note that this is a partial map: the loop doesn't necessarily introduce
+      an abstraction for each input region of the function.
 
     Rem.: the list of symbolic values should be computable by simply exploring
     the fixed point environment and listing all the symbolic values we find.
-- 
cgit v1.2.3


From 4f6def2f36227f0e58687729574ec5caa9f9004b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 22:52:31 +0100
Subject: Simplify the contexts before symbolically evaluating loops

---
 compiler/InterpreterLoopsFixedPoint.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'compiler/InterpreterLoopsFixedPoint.mli')

diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index c0e5dca5..7c3f6199 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -3,6 +3,18 @@ open Contexts
 open InterpreterUtils
 open InterpreterLoopsCore
 
+(** Repeat until we can't simplify the context anymore:
+   - explore the fresh anonymous values and replace all the values which are not
+     borrows/loans with ⊥
+   - also end the borrows which appear in fresh anonymous values and don't contain loans
+   - end the fresh region abstractions which can be ended (no loans)
+
+   Inputs:
+   - 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
+
 (** Prepare the shared loans in the abstractions by moving them to fresh
     abstractions.
 
-- 
cgit v1.2.3