WhyML: allow return types with names: f (a:int) : (x: int, ghost y: int)

These names are only visible under "ensures" but not under "returns".
If the result is named, the special variable "result" is not used.
In a tuple, either each component should be named, or none at all.
Underscores are allowed. Parentheses around the return type are required.
Each name must be given its own type: "f () : (x y: int)" is rejected.
Identifiers without cast are treated as types, not as names.
To name the result without giving its type, use "returns".

examples/add_list.mlw

@@ -29,9 +29,9 @@ module AddListRec
 
 use import SumList
 
-let rec sum (l: list or_integer_float) : (int, real) =
+let rec sum (l: list or_integer_float) : (si: int, sf: real) =
     variant { l }
-    returns { si, sf -> si = add_int l /\ sf = add_real l }
+    ensures { si = add_int l /\ sf = add_real l }
   match l with
   | Nil -> 0, 0.0
   | Cons h t ->
@@ -59,8 +59,8 @@ module AddListImp
 use import SumList
 use import ref.Ref
 
-let sum (l: list or_integer_float) : (int, real) =
-    returns { si, sf -> si = add_int l /\ sf = add_real l }
+let sum (l: list or_integer_float) : (si: int, sf: real) =
+    ensures { si = add_int l /\ sf = add_real l }
   let si = ref 0 in
   let sf = ref 0.0 in
   let ll = ref l in

examples/add_list_vc_sp.mlw

@@ -29,9 +29,9 @@ module AddListRec
 
 use import SumList
 
-let rec sum (l: list or_integer_float) : (int, real) =
+let rec sum (l: list or_integer_float) : (si: int, sf: real) =
     variant { l }
-    returns { si, sf -> si = add_int l /\ sf = add_real l }
+    ensures { si = add_int l /\ sf = add_real l }
   [@vc:sp]
   match l with
   | Nil -> 0, 0.0
@@ -61,8 +61,8 @@ module AddListImp
 use import SumList
 use import ref.Ref
 
-let sum (l: list or_integer_float) : (int, real) =
-    returns { si, sf -> si = add_int l /\ sf = add_real l }
+let sum (l: list or_integer_float) : (si: int, sf: real) =
+    ensures { si = add_int l /\ sf = add_real l }
   [@vc:sp]
   let si = ref 0 in
   let sf = ref 0.0 in

examples/fibonacci.mlw

@@ -239,12 +239,12 @@ module Zeckendorf
     requires { sum l1 = sum l2 }
     ensures { l1 = l2 }
     variant { sum l1 }
-  = let rec decomp (k acc:int) (lc lb:list int) : (int,list int)
+  = let rec decomp (k acc:int) (lc lb:list int) : (x: int, p: list int)
       requires { wf k lc }
       requires { k >= 2 /\ lc <> Nil }
       requires { 0 <= acc = sum lb - sum lc < fib (k-1) }
-      returns { x,p -> fib x <= sum lb = acc + fib x + sum p < fib (x+1) }
-      returns { x,p -> wf k p /\ x >= k /\ lc = snoc p x }
+      ensures { fib x <= sum lb = acc + fib x + sum p < fib (x+1) }
+      ensures { wf k p /\ x >= k /\ lc = snoc p x }
       variant { lc }
     = match lc with
       | Nil -> absurd

examples/finger_trees.mlw

@@ -48,8 +48,8 @@ module FingerTrees
     | Deep l m r -> d_m l ++ flatten (t_m m) ++ d_m r
     end
 
-  let d_cons (x:'a) (d:digit 'a) : (digit 'a,list (node 'a))
-    returns { b,o -> Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 }
+  let d_cons (x:'a) (d:digit 'a) : (b: digit 'a, o: list (node 'a))
+    ensures { Cons x (d_m d) = d_m b ++ flatten o /\ length o <= 1 }
   = match d with
     | One y -> Two x y , Nil
     | Two y z -> Three x y z , Nil

examples/linked_list_rev.mlw

@@ -42,10 +42,10 @@ module InPlaceRev
     end
 
   let rec ghost mem_decomp (x: loc) (l: list loc)
-    : (list loc, list loc)
+    : (l1: list loc, l2: list loc)
     requires { mem x l }
     variant  { l }
-    returns { (l1,l2) -> l = l1 ++ Cons x l2 }
+    ensures  { l = l1 ++ Cons x l2 }
   = match l with
     | Nil -> absurd
     | Cons h t -> if eq_loc h x then (Nil,t) else
@@ -225,10 +225,10 @@ module InPlaceRevSeq
     forall s: seq 'a. length s > 0 ->
     s == cons s[0] s[1..]
 
-  let rec ghost mem_decomp (x: loc) (s: seq loc) : (seq loc, seq loc)
+  let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc)
     requires { mem x s }
     variant  { length s }
-    returns  { (s1,s2) -> s == s1 ++ cons x s2 }
+    ensures  { s == s1 ++ cons x s2 }
   =
     if eq_loc s[0] x then (empty, s[1..])
     else begin

examples/sieve.mlw

@@ -21,9 +21,9 @@ module Sieve
     ensures { !r = old !r + 1 }
   = r := !r + 1
 
-  let sieve (n:int) : array bool
+  let sieve (n:int) : (m: array bool)
     requires { n > 1 }
-    returns { m -> length m = n /\ forall i. 0 <= i < n -> m[i] <-> prime i }
+    ensures  { length m = n /\ forall i. 0 <= i < n -> m[i] <-> prime i }
   = let t = Array.make n true in
     t[0] <- false;
     t[1] <- false;

examples/sumrange.mlw

@@ -300,11 +300,12 @@ module CumulativeTree
 (** {3 update cumulative tree} *)
 
 
-  let rec update_aux (t:tree) (i:int) (ghost a :array int) (v:int) : (tree,int)
+  let rec update_aux
+      (t:tree) (i:int) (ghost a :array int) (v:int) : (t': tree, delta: int)
     requires { is_tree_for t a t.indexes.low t.indexes.high }
     requires { t.indexes.low <= i < t.indexes.high }
     variant { t }
-    returns { (t',delta) ->
+    ensures {
         delta = v - a[i] /\
         t'.indexes.low = t.indexes.low /\
         t'.indexes.high = t.indexes.high /\
@@ -387,12 +388,14 @@ module CumulativeTree
 
   use import ref.Ref
 
-  let rec update_aux_complexity (t:tree) (i:int) (ghost a :array int) (v:int) (ghost c:ref int): (tree,int)
+  let rec update_aux_complexity
+        (t:tree) (i:int) (ghost a :array int)
+        (v:int) (ghost c:ref int) : (t': tree, delta: int)
      requires { is_tree_for t a t.indexes.low t.indexes.high }
      requires { t.indexes.low <= i < t.indexes.high }
      variant { t }
      ensures { !c - old !c <= depth t }
-     returns { (t',delta) ->
+     ensures {
         delta = v - a[i] /\
         t'.indexes.low = t.indexes.low /\
         t'.indexes.high = t.indexes.high /\
@@ -443,4 +446,4 @@ module CumulativeTree
     end
 
 
-end
\ No newline at end of file
+end

examples/swap.mlw

@@ -48,9 +48,9 @@ module SwapInt32
 
   (* purely applicative version first *)
 
-  let swap (a b: int32) : (int32, int32)
+  let swap (a b: int32) : (x: int32, y: int32)
     requires { in_bounds a /\ in_bounds b }
-    returns  { x,y -> int32'int x = b /\ int32'int y = a }
+    ensures  { int32'int x = b /\ int32'int y = a }
   =
     let a = a + b in
     let b = a - b in

examples/verifythis_2017_maximum_sum_submatrix.mlw

@@ -26,9 +26,8 @@ module Kadane2D
   function array_sum (a: A.array int) (l h: int) : int
     = sum (fun i -> a[i]) l h
 
-  val maximum_subarray (a: A.array int) : (int, int, int)
-    returns { s, lo, hi ->
-              0 <= lo <= hi <= A.length a /\ s = array_sum a lo hi /\
+  val maximum_subarray (a: A.array int) : (s: int, lo: int, hi: int)
+    ensures { 0 <= lo <= hi <= A.length a /\ s = array_sum a lo hi /\
               forall l h. 0 <= l <= h <= A.length a -> s >= array_sum a l h }
 
   (* sum of a submatrix *)
@@ -38,9 +37,9 @@ module Kadane2D
   function matrix_sum (m: matrix int) (rl rh cl ch: int) : int
     = sum (fun j -> sum (col m j) rl rh) cl ch
 
-  let maximum_submatrix (m: matrix int) : (int, int, int, int, int)
-    returns { s, rlo, rhi, clo, chi ->
-              (* this is a legal submatrix *)
+  let maximum_submatrix (m: matrix int) :
+      (s: int, rlo: int, rhi: int, clo: int, chi: int)
+    ensures { (* this is a legal submatrix *)
               0 <= rlo <= rhi <= rows m /\
               0 <= clo <= chi <= columns m /\
               (* s is its sum *)

examples/verifythis_2018_le_rouge_et_le_noir_1.mlw

@@ -226,9 +226,8 @@ let rec disjoint_union (s1 s2: set coloring) : set coloring
 
 use import array.Array
 
-let enum () : (array int, ghost array (set coloring))
-  returns { count, sets ->
-            Array.length count = 51 = Array.length sets
+let enum () : (count: array int, ghost sets: array (set coloring))
+  ensures { Array.length count = 51 = Array.length sets
             /\ (forall i. 0 <= i <= 50 ->
                (forall c: coloring. Seq.length c = i ->
                           (valid c <-> mem c (sets[i]))))
@@ -327,4 +326,4 @@ let enum () : (array int, ghost array (set coloring))
   done;
   count, sets
 
-end
\ No newline at end of file
+end

examples/vstte10_max_sum.mlw

@@ -12,10 +12,10 @@ module MaxAndSum
   use import ref.Ref
   use import array.Array
 
-  let max_sum (a: array int) (n: int) : (int, int)
+  let max_sum (a: array int) (n: int) : (sum: int, max: int)
     requires { n = length a }
     requires { forall i. 0 <= i < n -> a[i] >= 0 }
-    returns  { sum, max -> sum <= n * max }
+    ensures  { sum <= n * max }
   = let sum = ref 0 in
     let max = ref 0 in
     for i = 0 to n - 1 do

examples/vstte12_tree_reconstruction.mlw

@@ -81,9 +81,9 @@ module TreeReconstruction
   exception Failure
     (* used to signal the algorithm's failure i.e. there is no tree *)
 
-  let rec build_rec (d: int) (s: list int) : (tree, list int)
+  let rec build_rec (d: int) (s: list int) : (t: tree, s': list int)
     variant { length s, hd s - d }
-    returns { t, s' -> s = depths d t ++ s' }
+    ensures { s = depths d t ++ s' }
     raises  { Failure -> forall t: tree, s' : list int. depths d t ++ s' <> s }
   = match s with
     | Nil ->

examples/white_and_black_balls.mlw

@@ -33,7 +33,7 @@ module WhiteAndBlackBalls
       invariant { !b >= 0 && !w >= 0 && !b + !w >= 1 }
       invariant { odd !b <-> odd b0 }
       variant   { !b + !w }
-      let x, y = any (int, int) returns { x, y ->
+      let x, y = any (x: int, y: int) ensures {
         0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w } in
       if x = 0 || y = 0 then begin (* same color -> insert a white *)
         b := !b - x;

src/core/dterm.ml

@@ -559,8 +559,12 @@ let quant_vars ~strict env vl =
 let debug_ignore_unused_var = Debug.register_info_flag "ignore_unused_vars"
   ~desc:"Suppress@ warnings@ on@ unused@ variables"
 
+let attr_w_unused_var_no =
+  Ident.create_attribute "W:unused_variable:N"
+
 let check_used_var t vs =
-  if Debug.test_noflag debug_ignore_unused_var then
+  if not (Sattr.mem attr_w_unused_var_no vs.vs_name.id_attrs) &&
+      Debug.test_noflag debug_ignore_unused_var then
     begin
       let s = vs.vs_name.id_string in
       if (s = "" || s.[0] <> '_') && t_v_occurs vs t = 0 then

src/core/dterm.mli

@@ -118,6 +118,7 @@ val dterm : Coercion.t -> ?loc:Loc.position -> dterm_node -> dterm
 (** Final stage *)
 
 val debug_ignore_unused_var : Debug.flag
+val attr_w_unused_var_no : Ident.attribute
 
 val term : ?strict:bool -> ?keep_loc:bool -> dterm -> term
 

src/mlw/dexpr.ml

@@ -1107,16 +1107,15 @@ let cty_of_spec env bl mask dsp dity =
 
 (** Expressions *)
 
-let warn_unused s loc =
-  if Debug.test_noflag Dterm.debug_ignore_unused_var then
+let check_used_pv e pv =
+  if not (Sattr.mem Dterm.attr_w_unused_var_no pv.pv_vs.vs_name.id_attrs) &&
+      Debug.test_noflag Dterm.debug_ignore_unused_var then
     begin
-     if s = "" || s.[0] <> '_' then
-     Warning.emit ?loc "unused variable %s" s
+      let s = pv.pv_vs.vs_name.id_string in
+      if (s = "" || s.[0] <> '_') && not (Spv.mem pv e.e_effect.eff_reads) then
+        Warning.emit ?loc:pv.pv_vs.vs_name.id_loc "unused variable %s" s
     end
 
-let check_used_pv e pv = if not (Spv.mem pv e.e_effect.eff_reads) then
-  warn_unused pv.pv_vs.vs_name.id_string pv.pv_vs.vs_name.id_loc
-
 let e_let_check e ld = match ld with
   | LDvar (v,_) -> check_used_pv e v; e_let ld e
   | _           -> e_let ld e

src/parser/parser.mly

@@ -98,6 +98,15 @@
   let continue_id = "'Continue"
   let return_id   = "'Return"
 
+  let apply_return pat sp =
+    let apply = function
+      | loc, [{pat_desc = Pvar ({id_str = "result"; id_loc = l}, false)}, f]
+        when Loc.equal loc l -> loc, [pat, f]
+      | post -> post in
+    match pat.pat_desc with
+    | Pwild -> sp
+    | _ -> { sp with sp_post = List.map apply sp.sp_post }
+
   let error_param loc =
     Loc.errorm ~loc "cannot determine the type of the parameter"
 
@@ -431,15 +440,12 @@ binders: binder+ { List.concat $1 }
 param:
 | anon_binder
     { error_param (floc $startpos $endpos) }
+| lident_nq attr+
+    { error_param (floc $startpos $endpos) }
 | ty_arg
     { [floc $startpos $endpos, None, false, $1] }
 | LEFTPAR GHOST ty RIGHTPAR
     { [floc $startpos $endpos, None, true, $3] }
-| ty_arg attr attr*
-    { match $1 with
-      | PTtyapp (Qident _, []) ->
-             error_param (floc $startpos $endpos)
-      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
 | LEFTPAR binder_vars_rest RIGHTPAR
     { match $2 with [l,_] -> error_param l
       | _ -> error_loc (floc $startpos($3) $endpos($3)) }
@@ -454,6 +460,8 @@ param:
 binder:
 | anon_binder
     { let l,i = $1 in [l, i, false, None] }
+| lident_nq attr+
+    { [floc $startpos $endpos, Some (add_attr $1 $2), false, None] }
 | ty_arg
     { match $1 with
       | PTtyapp (Qident id, [])
@@ -465,12 +473,6 @@ binder:
       | PTtyapp (Qident id, []) ->
              [floc $startpos $endpos, Some id, true, None]
       | _ -> [floc $startpos $endpos, None, true, Some $3] }
-| ty_arg attr attr*
-    { match $1 with
-      | PTtyapp (Qident id, []) ->
-             let id = add_attr id ($2::$3) in
-             [floc $startpos $endpos, Some id, false, None]
-      | _ -> error_loc (floc $startpos($2) $endpos($2)) }
 | LEFTPAR binder_vars_rest RIGHTPAR
     { match $2 with [l,i] -> [l, i, false, None]
       | _ -> error_loc (floc $startpos($3) $endpos($3)) }
@@ -487,12 +489,12 @@ binder_vars:
 | binder_vars_rest  { $1 }
 
 binder_vars_rest:
-| binder_vars_head attr attr* binder_var*
+| binder_vars_head attr+ binder_var*
     { List.rev_append (match $1 with
         | (l, Some id) :: bl ->
-            let l3 = floc $startpos($3) $endpos($3) in
-            (Loc.join l l3, Some (add_attr id ($2::$3))) :: bl
-        | _ -> assert false) $4 }
+            let l2 = floc $startpos($2) $endpos($2) in
+            (Loc.join l l2, Some (add_attr id $2)) :: bl
+        | _ -> assert false) $3 }
 | binder_vars_head anon_binder binder_var*
     { List.rev_append $1 ($2 :: $3) }
 | anon_binder binder_var*
@@ -689,20 +691,25 @@ kind:
 (* Function definitions *)
 
 rec_defn:
-| ghost kind attrs(lident_rich) binders ret_opt spec EQUAL spec seq_expr
-    { let id = mk_id return_id $startpos($7) $endpos($7) in
-      let e = { $9 with expr_desc = Eoptexn (id, snd $5, $9) } in
-      $3, $1, $2, $4, fst $5, snd $5, spec_union $6 $8, e }
+| ghost kind attrs(lident_rich) binders return_opt spec EQUAL spec seq_expr
+    { let pat, ty, mask = $5 in
+      let spec = apply_return pat (spec_union $6 $8) in
+      let id = mk_id return_id $startpos($7) $endpos($7) in
+      let e = { $9 with expr_desc = Eoptexn (id, mask, $9) } in
+      $3, $1, $2, $4, ty, mask, spec, e }
 
 fun_defn:
-| binders ret_opt spec EQUAL spec seq_expr
-    { let id = mk_id return_id $startpos($4) $endpos($4) in
-      let e = { $6 with expr_desc = Eoptexn (id, snd $2, $6) } in
-      Efun (List.map add_model_attrs $1, fst $2, snd $2, spec_union $3 $5, e) }
+| binders return_opt spec EQUAL spec seq_expr
+    { let pat, ty, mask = $2 in
+      let spec = apply_return pat (spec_union $3 $5) in
+      let id = mk_id return_id $startpos($4) $endpos($4) in
+      let e = { $6 with expr_desc = Eoptexn (id, mask, $6) } in
+      Efun (List.map add_model_attrs $1, ty, mask, spec, e) }
 
 val_defn:
-| params ret_opt spec
-    { Eany ($1, Expr.RKnone, fst $2, snd $2, $3) }
+| params return_opt spec
+    { let pat, ty, mask = $2 in
+      Eany ($1, Expr.RKnone, ty, mask, apply_return pat $3) }
 
 const_defn:
 | cast EQUAL seq_expr   { { $3 with expr_desc = Ecast ($3, $1) } }
@@ -825,8 +832,9 @@ single_expr_:
     { let id = mk_id return_id $startpos($4) $endpos($4) in
       let e = { $6 with expr_desc = Eoptexn (id, Ity.MaskVisible, $6) } in
       Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, e) }
-| ANY return spec
-    { Eany ([], Expr.RKnone, Some (fst $2), snd $2, $3) }
+| ANY return_named spec
+    { let pat, ty, mask = $2 in
+      Eany ([], Expr.RKnone, Some ty, mask, apply_return pat $3) }
 | VAL ghost kind attrs(lident_rich) mk_expr(val_defn) IN seq_expr
     { Elet ($4, $2, $3, $5, $7) }
 | MATCH seq_expr WITH ext_match_cases END
@@ -1036,30 +1044,45 @@ variant:
 single_variant:
 | single_term preceded(WITH,lqualid)?  { $1, $2 }
 
-ret_opt:
-| (* epsilon *)     { None, Ity.MaskVisible }
-| COLON return      { Some (fst $2), snd $2 }
+return_opt:
+| (* epsilon *)       { mk_pat Pwild $startpos $endpos, None, Ity.MaskVisible }
+| COLON return_named  { let pat, ty, mask = $2 in pat, Some ty, mask }
+
+return_named:
+| LEFTPAR ret_cast RIGHTPAR
+    { $2 }
+| LEFTPAR comma_list2(ret_cast) RIGHTPAR
+    { mk_pat (Ptuple (List.map (fun (pat,_,_) -> pat) $2)) $startpos $endpos,
+      PTtuple (List.map (fun (_,ty,_) -> ty) $2),
+      Ity.MaskTuple (List.map (fun (_,_,mask) -> mask) $2) }
+| return
+    { let ty, mask = $1 in mk_pat Pwild $startpos $endpos, ty, mask }
+
+ret_cast:
+|       ret_ident cast  { $1, $2, Ity.MaskVisible }
+| GHOST ret_ident cast  { $2, $3, Ity.MaskGhost }
+
+ret_ident:
+| id = attrs(lident_nq)
+    { let ats = ATstr Dterm.attr_w_unused_var_no :: id.id_ats in
+      mk_pat (Pvar ({id with id_ats = ats}, false)) $startpos $endpos }
 
 return:
-| ret_arg           { $1 }
-| lqualid ty_arg+   { PTtyapp ($1, $2), Ity.MaskVisible }
-| ret_arg ARROW ty  { PTarrow (fst $1, $3),
-                      if Ity.mask_ghost (snd $1) then
-                        raise Error else Ity.MaskVisible }
-| GHOST ty          { $2, Ity.MaskGhost }
-
-ret_arg:
-| lqualid                               { PTtyapp ($1, []), Ity.MaskVisible }
-| quote_lident                          { PTtyvar $1, Ity.MaskVisible }
-| LEFTPAR RIGHTPAR                      { PTtuple [], Ity.MaskVisible }
-| LEFTBRC ty RIGHTBRC                   { PTpure  $2, Ity.MaskVisible }
-| LEFTPAR ret_sub RIGHTPAR              { PTparen (fst $2), snd $2 }
-| LEFTPAR comma_list2(ret_sub) RIGHTPAR { PTtuple (List.map fst $2),
-                                    Ity.MaskTuple (List.map snd $2) }
-
-ret_sub:
-| ty                { $1, Ity.MaskVisible }
-| GHOST ty          { $2, Ity.MaskGhost }
+|               ty            { $1, Ity.MaskVisible }
+|         GHOST ty            { $2, Ity.MaskGhost }
+| LEFTPAR GHOST ty RIGHTPAR   { $3, Ity.MaskGhost }
+| LEFTPAR ret_ghost RIGHTPAR  { PTtuple (fst $2), Ity.MaskTuple (snd $2) }
+
+ret_ghost:
+|       ty COMMA GHOST ty     { [$1; $4], [Ity.MaskVisible; Ity.MaskGhost] }
+|       ty COMMA ret_ghost    { $1::fst $3, Ity.MaskVisible::snd $3 }
+| GHOST ty COMMA ret_rest     { $2::fst $4, Ity.MaskGhost::snd $4 }
+
+ret_rest:
+|       ty COMMA ret_rest     { $1::fst $3, Ity.MaskVisible::snd $3 }
+| GHOST ty COMMA ret_rest     { $2::fst $4, Ity.MaskGhost::snd $4 }
+|       ty                    { [$1], [Ity.MaskVisible] }
+| GHOST ty                    { [$2], [Ity.MaskGhost] }
 
 (* Patterns *)