summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-03-08 23:53:50 +0100
committerSon Ho2024-03-08 23:53:50 +0100
commit8f1972dddbd25ff2153bdf3dabd743256fec03a4 (patch)
tree6eca36d3269b08c2a922e29290cd1d4d9f456d26
parent457888a031c870edc4576068ec647987800f0fb7 (diff)
Add some comments
Diffstat (limited to '')
-rw-r--r--compiler/SymbolicAst.ml14
-rw-r--r--compiler/SymbolicToPure.ml7
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