higher-order application syntax in patterns

src/parser/parser.mly

@@ -460,12 +460,19 @@ list1_pat_sep_comma:
 | pattern                           { [$1] }
 | pattern COMMA list1_pat_sep_comma { $1::$3 }
 
+list1_pat_arg:
+| pat_arg               { [$1] }
+| pat_arg list1_pat_arg { $1::$2 }
+
 pattern:
+| pat_arg               { $1 }
+| uqualid list1_pat_arg { mk_pat (PPpapp ($1, $2)) }
+| pattern AS lident     { mk_pat (PPpas ($1,$3)) }
+
+pat_arg:
 | UNDERSCORE                                    { mk_pat (PPpwild) }
 | lident                                        { mk_pat (PPpvar $1) }
 | uqualid                                       { mk_pat (PPpapp ($1, [])) }
-| uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR  { mk_pat (PPpapp ($1, $3)) }
-| pattern AS lident                             { mk_pat (PPpas ($1,$3)) }
 | LEFTPAR pattern RIGHTPAR                      { $2 }
 | LEFTPAR RIGHTPAR                              { mk_pat (PPptuple []) }
 | LEFTPAR pattern COMMA list1_pat_sep_comma RIGHTPAR 

theories/list.why

@@ -11,8 +11,8 @@ theory Length
 
   logic length(l : 'a list) : int = 
     match l with
-    | Nil        -> 0
-    | Cons(_, r) -> 1 + length(r)
+    | Nil      -> 0
+    | Cons _ r -> 1 + length(r)
     end
 
   lemma Length_nonnegative : forall l:'a list. length(l) >= 0
@@ -23,8 +23,8 @@ theory Mem
   use export List
  
   logic mem(x: 'a, l : 'a list) = match l with
-    | Nil -> false
-    | Cons(y, r) -> x = y or mem(x, r)
+    | Nil      -> false
+    | Cons y r -> x = y or mem(x, r)
     end
 
 end
@@ -54,8 +54,8 @@ theory Map
 
   logic map(l : a list) : b list = 
     match l with
-    | Nil        -> Nil
-    | Cons(x, r) -> Cons(f(x), map(r))
+    | Nil      -> Nil
+    | Cons x r -> Cons(f(x), map(r))
     end
 
 end