Add some comments

2 files changed, 12 insertions, 9 deletions

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index e1f0ad38..7252a020 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -197,16 +197,16 @@ type expression =
           The evaluation context is the context at the moment we introduce the
           [ForwardEnd], and is used to translate the input values (see the
           comments for the {!Return} variant).
+
+          This case also handles the case where we (re-)enter a loop (once
+          we enter a loop in symbolic mode, we don't get out: the loop is
+          responsible for the end of the function).
        *)
   | Loop of loop  (** Loop *)
   | ReturnWithLoop of loop_id * bool
-      (** End the function with a call to a loop function.
-
-          This encompasses the cases when we synthesize a function body
-          and enter a loop for the first time, or when we synthesize a
-          loop body and reach a [Continue].
-
-          The boolean is [is_continue].
+      (** We reach a return while inside a loop.
+          The boolean is [true].
+          TODO: merge this with Return.
        *)
   | Meta of emeta * expression  (** Meta information *)
 
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 8e53f18a..8b4362a2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1890,7 +1890,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
          Remark: we can't get there if we are inside a loop. *)
       translate_return ectx opt_v ctx
   | ReturnWithLoop (loop_id, is_continue) ->
-      (* We end the function with a call to a loop function. *)
+      (* We reached a return and are inside a loop. *)
       translate_return_with_loop loop_id is_continue ctx
   | Panic -> translate_panic ctx
   | FunCall (call, e) -> translate_function_call call e ctx
@@ -1902,7 +1902,10 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
       translate_intro_symbolic ectx p sv v e ctx
   | Meta (meta, e) -> translate_emeta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
-      (* Translate the end of a function, or the end of a loop *)
+      (* Translate the end of a function, or the end of a loop.
+
+         The case where we (re-)enter a loop is handled here.
+      *)
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx