summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2022-11-15 11:43:13 +0100
committerSon HO2022-11-16 15:45:32 +0100
commite4043e51ed4b4dcee7096df2d55ac049033b1d68 (patch)
tree94febfe1778ecaa3fb78eb5d40786f0f2c267581 /compiler
parent6232c2bfda2d3bbb4de8b536d8b03fe26255a864 (diff)
Make minor modifications to the extraction
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml17
1 files changed, 13 insertions, 4 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 950e4026..9daea15b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1432,10 +1432,19 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(re : texpression) : extraction_ctx =
(* Open a box for the let-binding *)
F.pp_open_hovbox fmt ctx.indent_incr;
+ let is_fstar_monadic = monadic && !backend = FStar in
let ctx =
- if monadic then (
- (* Note that in F*, the left value of a monadic let-binding can only be
- * a variable *)
+ (* There are two cases:
+ * - do we use a notation like [x <-- y;]
+ * - do we use notation with let-bindings
+ * Note that both notations can be used for monadic let-bindings.
+ * For instance, in F*, you can write:
+ * {[
+ * let* x = y in // monadic
+ * ...
+ * ]}
+ * *)
+ if monadic && !backend = Coq then (
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
let arrow = match !backend with FStar -> "<--" | Coq -> "<-" in
@@ -1445,7 +1454,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_string fmt ";";
ctx)
else (
- F.pp_print_string fmt "let";
+ F.pp_print_string fmt (if is_fstar_monadic then "let*" else "let");
F.pp_print_space fmt ();
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();