diff options
author | Son Ho | 2022-01-20 21:25:08 +0100 |
---|---|---|
committer | Son Ho | 2022-01-20 21:25:08 +0100 |
commit | 582b23d6eb2d772a11e1b86db5f6f3868d6dc44c (patch) | |
tree | e4525e8b5c04743803de52def9973ab9046194cb | |
parent | 108dfc94b7f634d5624bfb7ef0865c2b2a5ee18c (diff) |
Update a comment
-rw-r--r-- | src/Contexts.ml | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 15256cda..70c7a399 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -18,11 +18,11 @@ module M = Modules * objects * * ============= - * **WARNNING**: + * **WARNING**: * ============= - * Pay attention when playing with the function type abbreviations, - * as they may make you not always generate fresh identifiers. For - * instance, consider the following: + * Pay attention when playing with closures, as you may not always generate + * fresh identifiers without noticing it, especially when using type abbreviations. + * For instance, consider the following: * ``` * type fun_type = unit -> ... * fn f x : fun_type = @@ -43,6 +43,17 @@ module M = Modules * let id = fresh_id () in * ... * ``` + * + * Note that in practice, we never reuse closures, except when evaluating + * a branching in the execution (which is fine, because the branches evaluate + * independentely of each other). Still, it is always a good idea to be + * defensive. + * + * Also, a more defensive way would be to not use global references, and + * store the counters in the evaluation context. This is actually what was + * originally done, before we updated the code to use global counters because + * it proved more convenient (and even before updating the code of the + * interpreter to use CPS). *) let symbolic_value_id_counter, fresh_symbolic_value_id = |