1 files changed, 62 insertions, 0 deletions
diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli
new file mode 100644
index 00000000..7395739b
--- /dev/null
+++ b/compiler/InterpreterLoops.mli
@@ -0,0 +1,62 @@
+(** This module implements support for loops.
+
+    Throughout the module, we will use the following code as example to
+    illustrate what the functions do (this function simply returns a mutable
+    borrow to the nth element of a list):
+    {[
+      pub fn list_nth_mut<'a, T>(mut ls: &'a mut List<T>, mut i: u32) -> &'a mut T {
+          loop {
+              match ls {
+                  List::Nil => {
+                      panic!()
+                  }
+                  List::Cons(x, tl) => {
+                      if i == 0 {
+                          return x;
+                      } else {
+                          ls = tl;
+                          i -= 1;
+                      }
+                  }
+              }
+          }
+      }
+    ]}
+
+    Upon reaching the loop entry, the environment is as follows (ignoring the
+    dummy variables):
+    {[
+      abs@0 { ML l0 }
+      ls -> MB l0 (s2 : loops::List<T>)
+      i -> s1 : u32
+    ]}
+
+    Upon reaching the [continue] at the end of the first iteration, the environment
+    is as follows:
+    {[
+      abs@0 { ML l0 }
+      ls -> MB l4 (s@6 : loops::List<T>)
+      i -> s@7 : u32
+      _@1 -> MB l0 (loops::List::Cons (ML l1, ML l2))
+      _@2 -> MB l2 (@Box (ML l4))                      // tail
+      _@3 -> MB l1 (s@3 : T)                           // hd
+    ]}
+
+    The fixed point we compute is:
+    {[
+      abs@0 { ML l0 }
+      ls -> MB l1 (s@3 : loops::List<T>)
+      i -> s@4 : u32
+      abs@fp { // fp: fixed-point
+        MB l0
+        ML l1
+      }
+    ]}
+
+    From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction.
+  *)
+
+module C = Contexts
+
+(** Evaluate a loop *)
+val eval_loop : C.config -> Cps.st_cm_fun -> Cps.st_cm_fun