A tiny extension of frontend syntax.

ANNOTATIONS.md

@@ -269,7 +269,7 @@ Coq import to bring theorem `thm` in scope: `From x.y Require Import z.`.
 This annotation can appear either on functions and on structures. It should be
 given at least one argument of the following form.
 ```
-<ident (as variable name)> ":" <coq_expr (as Coq type)>
+<ident (as variable)> {"," <ident (as variable)>}* ":" <coq_expr (as Coq type)>
 ```
 It corresponds to an universally quantified variable with the given type. When
 on a function, such a variable is bound in the whole specification. Similarly,

examples/bff_paper_example.c

@@ -78,7 +78,7 @@ static bool pte_valid(pte_t pte) {
 //@rc::end
 
 [[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
-[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "lvl : Z")]]
+[[rc::parameters("p : loc", "old, pa, attr : Pte", "lvl : Z")]]
 [[rc::args("p @ &own<old @ pte_t>", "pa @ pte_t", "attr @ pte_t", "lvl @ int<u32>")]]
 [[rc::requires("{old.(pte_valid) = false}")]]
 [[rc::returns("{true} @ boolean<bool_it>")]]

frontend/rc_annot.ml

@@ -226,8 +226,8 @@ let type_expr = type_expr `Full
 
 (** {4 Annotations on type definitions} *)
 
-let parser annot_parameter : (ident * coq_expr) Earley.grammar =
-  | id:ident ":" s:coq_expr
+let parser annot_parameter : (ident list * coq_expr) Earley.grammar =
+  | id:ident ids:{"," ident}* ":" s:coq_expr -> (id :: ids, s)
 
 let parser annot_refine : (ident * coq_expr) Earley.grammar =
   | id:ident ":" s:coq_expr
@@ -436,8 +436,12 @@ let parse_attr : rc_attr -> annot = fun attr ->
     | _  -> error "should not have arguments"
   in
 
+  let mk_annot_parameters l =
+    let fn (ids, ty) = List.map (fun id -> (id, ty)) ids in
+    Annot_parameters(List.concat (List.map fn l))
+  in
   match id.elt with
-  | "parameters"   -> many_args annot_parameter (fun l -> Annot_parameters(l))
+  | "parameters"   -> many_args annot_parameter mk_annot_parameters
   | "refined_by"   -> many_args annot_refine (fun l -> Annot_refined_by(l))
   | "ptr_type"     -> single_arg annot_ptr_type (fun e -> Annot_ptr_type(e))
   | "size"         -> single_arg annot_size (fun e -> Annot_size(e))