support multiple variants in WhyML syntax

src/parser/parser.mly

@@ -1437,9 +1437,18 @@ effect:
 ;
 
 opt_variant:
-| /* epsilon */                   { None }
-| VARIANT annotation              { Some ($2, None) }
-| VARIANT annotation WITH lqualid { Some ($2, Some $4) }
+| /* epsilon */         { [] }
+| VARIANT list1_variant { $2 }
+;
+
+list1_variant:
+| variant                     { [$1] }
+| variant COMMA list1_variant { $1::$3 }
+;
+
+variant:
+| annotation              { $1, None }
+| annotation WITH lqualid { $1, Some $3 }
 ;
 
 opt_cast:

src/parser/ptree.ml

@@ -181,7 +181,7 @@ type variant = lexpr * qualid option
 
 type loop_annotation = {
   loop_invariant : lexpr option;
-  loop_variant   : variant option;
+  loop_variant   : variant list;
 }
 
 type for_direction = To | Downto
@@ -248,7 +248,7 @@ and expr_desc =
   | Eabstract of expr * post
   | Enamed of label * expr
 
-and letrec = loc * ident * ghost * binder list * variant option * triple
+and letrec = loc * ident * ghost * binder list * variant list * triple
 
 and triple = pre * expr * post
 

src/programs/pgm_typing.ml

@@ -342,9 +342,14 @@ let dvariant env (l, p) =
   in
   l, option_map relation p
 
+let dvariants env = function
+  | [] -> None
+  | [v] -> Some (dvariant env v)
+  | _ -> errorm "multiple variants are not supported"
+
 let dloop_annotation env a =
   { dloop_invariant = a.Ptree.loop_invariant;
-    dloop_variant   = option_map (dvariant env) a.Ptree.loop_variant; }
+    dloop_variant   = dvariants env a.Ptree.loop_variant; }
 
 (***
 let is_ps_ghost e = match e.dexpr_desc with
@@ -741,7 +746,7 @@ and dletrec ~ghost ~userloc env dl =
   (* then type-check all of them and unify *)
   let type_one ((id, tyres), bl, v, t) =
     let env, bl = map_fold_left dubinder env bl in
-    let v = option_map (dvariant env) v in
+    let v = dvariants env v in
     let (_,e,_) as t = dtriple ~ghost ~userloc env t in
     let tyl = List.map (fun (_,ty) -> ty) bl in
     let ty = dcurrying tyl e.dexpr_type in

src/whyml/mlw_typing.ml

@@ -388,13 +388,8 @@ and dtype_v denv = function
       let tyc,(argl,res) = dtype_c denv tyc in
       DSpecA (bl,tyc), (tyl @ argl,res)
 
-let dvariant uc = function
-  | Some (le, Some q) -> [le, Some (find_variant_ls uc q)]
-  | Some (le, None) -> [le, None]
-  | None -> []
-(* TODO: accept a list of variants in the surface language
+let dvariant uc var =
   List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var
-*)
 
 (* expressions *)
 
@@ -454,7 +449,7 @@ and de_desc denv loc = function
       DEletrec (rdl, e1), e1.de_type
   | Ptree.Efun (bl, tr) ->
       let denv, bl, tyl = dbinders denv bl in
-      let lam, (argl, res) = dlambda denv bl None tr in
+      let lam, (argl, res) = dlambda denv bl [] tr in
       DEfun lam, (tyl @ argl, res)
   | Ptree.Ecast (e1, pty) ->
       let e1 = dexpr denv e1 in