summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/coq/Primitives.v2
-rw-r--r--backends/fstar/Primitives.fst24
-rw-r--r--compiler/Extract.ml17
-rw-r--r--tests/coq/betree/Primitives.v2
-rw-r--r--tests/coq/hashmap/Primitives.v2
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v2
-rw-r--r--tests/coq/misc/Primitives.v2
-rw-r--r--tests/fstar/betree/Primitives.fst24
-rw-r--r--tests/fstar/betree_back_stateful/Primitives.fst24
-rw-r--r--tests/fstar/hashmap/Primitives.fst24
-rw-r--r--tests/fstar/hashmap_on_disk/Primitives.fst24
-rw-r--r--tests/fstar/misc/Primitives.fst24
12 files changed, 97 insertions, 74 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 9a97d6c7..ae961ac2 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -259,8 +259,6 @@ Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result
mk_scalar tgt_ty (to_Z x).
(** Comparisons *)
-Print Z.leb .
-
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
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 ();
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 9a97d6c7..ae961ac2 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -259,8 +259,6 @@ Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result
mk_scalar tgt_ty (to_Z x).
(** Comparisons *)
-Print Z.leb .
-
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 9a97d6c7..ae961ac2 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -259,8 +259,6 @@ Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result
mk_scalar tgt_ty (to_Z x).
(** Comparisons *)
-Print Z.leb .
-
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 9a97d6c7..ae961ac2 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -259,8 +259,6 @@ Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result
mk_scalar tgt_ty (to_Z x).
(** Comparisons *)
-Print Z.leb .
-
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 9a97d6c7..ae961ac2 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -259,8 +259,6 @@ Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result
mk_scalar tgt_ty (to_Z x).
(** Comparisons *)
-Print Z.leb .
-
Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
Z.leb (to_Z x) (to_Z y) .
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 9a06b596..bf0f9078 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -26,14 +26,19 @@ type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a
-// Monadic bind and return.
-// Re-definining those allows us to customize the result of the monadic notations
-// like: `y <-- f x;`
-let return (#a : Type0) (x:a) : result a = Return x
-let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
- match m with
- | Return x -> f x
- | Fail e -> Fail e
+// Monadic return operator
+unfold let return (#a : Type0) (x : a) : result a = Return x
+
+// Monadic bind operator.
+// Allows to use the notation:
+// ```
+// let* x = y in
+// ...
+// ```
+unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b =
+ match m with
+ | Return x -> f x
+ | Fail e -> Fail e
// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure
@@ -52,7 +57,7 @@ let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
-/// Rk.: most of the following code was at least partially generated
+/// Rem.: most of the following code was partially generated
let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
@@ -291,4 +296,3 @@ let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
if i < length v then Return (list_update v i nx) else Fail Failure
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 19:27:49 +0000