From e4043e51ed4b4dcee7096df2d55ac049033b1d68 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 15 Nov 2022 11:43:13 +0100
Subject: Make minor modifications to the extraction

---
 compiler/Extract.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'compiler')

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 ();
-- 
cgit v1.2.3