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

---
 tests/coq/betree/Primitives.v                   |  2 --
 tests/coq/hashmap/Primitives.v                  |  2 --
 tests/coq/hashmap_on_disk/Primitives.v          |  2 --
 tests/coq/misc/Primitives.v                     |  2 --
 tests/fstar/betree/Primitives.fst               | 24 ++++++++++++++----------
 tests/fstar/betree_back_stateful/Primitives.fst | 24 ++++++++++++++----------
 tests/fstar/hashmap/Primitives.fst              | 24 ++++++++++++++----------
 tests/fstar/hashmap_on_disk/Primitives.fst      | 24 ++++++++++++++----------
 tests/fstar/misc/Primitives.fst                 | 24 ++++++++++++++----------
 9 files changed, 70 insertions(+), 58 deletions(-)

(limited to 'tests')

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