diff options
Diffstat (limited to '')
-rw-r--r-- | backends/coq/Primitives.v | 2 | ||||
-rw-r--r-- | backends/fstar/Primitives.fst | 24 | ||||
-rw-r--r-- | compiler/Extract.ml | 17 | ||||
-rw-r--r-- | tests/coq/betree/Primitives.v | 2 | ||||
-rw-r--r-- | tests/coq/hashmap/Primitives.v | 2 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/Primitives.v | 2 | ||||
-rw-r--r-- | tests/coq/misc/Primitives.v | 2 | ||||
-rw-r--r-- | tests/fstar/betree/Primitives.fst | 24 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 24 | ||||
-rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 24 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 24 | ||||
-rw-r--r-- | tests/fstar/misc/Primitives.fst | 24 |
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 - |