Supporting "(@foo) args" in patterns, where "@foo" has no arguments.

9 files changed, 35 insertions, 30 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9c577034e..c5730e626 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
       eq_reference c1 c2 &&
-      List.equal cases_pattern_expr_eq a1 a2 &&
+      Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
   | CPatAtom(_,r1), CPatAtom(_,r2) ->
       Option.equal eq_reference r1 r2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2da8e0f6f..49892bec4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -266,7 +266,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args =
 
 let mkPat loc qid l =
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
-  if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
+  if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -286,7 +286,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+      CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
     | _ ->
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -329,13 +329,13 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
                   let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
 		  if !Topconstr.asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
-		    then CPatCstr (loc, c, [], args)
-		    else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+		    then CPatCstr (loc, c, None, args)
+		    else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
-		      |Some true_args -> CPatCstr (loc, c, [], true_args)
-		      |None -> CPatCstr (loc, c, full_args, [])
+		      |Some true_args -> CPatCstr (loc, c, None, true_args)
+		      |None -> CPatCstr (loc, c, Some full_args, [])
 	  in insert_pat_alias loc p na
 and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
@@ -413,7 +413,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
     let c = extern_reference Loc.ghost vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-    CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
+    CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -431,8 +431,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       let c = extern_reference Loc.ghost vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
-	   |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args)
-	   |None -> CPatCstr (Loc.ghost, c, args, [])
+	   |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
+	   |None -> CPatCstr (Loc.ghost, c, Some args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f46217dec..b62df8dff 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1095,7 +1095,7 @@ let drop_notations_pattern looked_for =
     let (loc,qid) = qualid_of_reference re in
     try
       match locate_extended qid with
-      |SynDef sp ->
+      | SynDef sp ->
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
 	| NRef g ->
@@ -1118,7 +1118,7 @@ let drop_notations_pattern looked_for =
 	      let (_,argscs) = find_remaining_scopes pats1 pats2 g in
 	      Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2)
 	| _ -> raise Not_found)
-      |TrueGlobal g ->
+      | TrueGlobal g ->
 	  test_kind top g;
 	  Dumpglob.add_glob loc g;
 	  let (_,argscs) = find_remaining_scopes [] pats g in
@@ -1140,16 +1140,15 @@ let drop_notations_pattern looked_for =
 	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, head, [], pl) ->
+    | CPatCstr (loc, head, None, pl) ->
       begin
 	match drop_syndef top env head pl with
 	  | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, r, expl_pl, pl) ->
-      let g = try
-		      (locate (snd (qualid_of_reference r)))
-	    with Not_found ->
+    | CPatCstr (loc, r, Some expl_pl, pl) ->
+      let g = try locate (snd (qualid_of_reference r))
+	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in
       RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cde72fd93..e569f543b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -52,7 +52,7 @@ let rec cases_pattern_fold_names f a = function
       List.fold_left (cases_pattern_fold_names f) a patl
   | CPatCstr (_,_,patl1,patl2) ->
     List.fold_left (cases_pattern_fold_names f)
-      (List.fold_left (cases_pattern_fold_names f) a patl1) patl2
+      (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
   | CPatNotation (_,_,(patl,patll),patl') ->
       List.fold_left (cases_pattern_fold_names f)
 	(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 40812a3d8..f5855a971 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -40,15 +40,15 @@ type raw_cases_pattern_expr =
   | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
   | RCPatCstr of Loc.t * Globnames.global_reference
     * raw_cases_pattern_expr list * raw_cases_pattern_expr list
-  (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
+  (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *)
   | RCPatAtom of Loc.t * Id.t option
   | RCPatOr of Loc.t * raw_cases_pattern_expr list
 
 type cases_pattern_expr =
   | CPatAlias of Loc.t * cases_pattern_expr * Id.t
   | CPatCstr of Loc.t * reference
-    * cases_pattern_expr list * cases_pattern_expr list
-  (** [CPatCstr (_, Inl c, l1, l2)] represents (@c l1) l2 *)
+    * cases_pattern_expr list option * cases_pattern_expr list
+  (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
   | CPatAtom of Loc.t * reference option
   | CPatOr of Loc.t * cases_pattern_expr list
   | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6eeae925a..b11204cbc 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -379,14 +379,14 @@ GEXTEND Gram
     | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
-	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
+	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
           | _ -> Errors.user_err_loc
               (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Such pattern cannot have arguments."))
-      |"@"; r = Prim.reference; lp = LIST1 NEXT ->
-        CPatCstr (!@loc, r, lp, []) ]
+      |"@"; r = Prim.reference; lp = LIST0 NEXT ->
+        CPatCstr (!@loc, r, Some lp, []) ]
     | "1" LEFTA
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 4874552d6..34307a358 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -96,7 +96,7 @@ let rec add_vars_of_simple_pattern globs = function
       add_vars_of_simple_pattern globs p
   | CPatCstr (_,_,pl1,pl2) ->
     List.fold_left add_vars_of_simple_pattern
-      (List.fold_left add_vars_of_simple_pattern globs pl1) pl2
+      (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2
   | CPatNotation(_,_,(pl,pll),pl') ->
       List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll))
   | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8a0df18ca..1866ca504 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -244,16 +244,16 @@ end) = struct
       | CPatAlias (_, p, id) ->
         pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
 
-      | CPatCstr (_,c, [], []) ->
+      | CPatCstr (_,c, None, []) ->
         pr_reference c, latom
 
-      | CPatCstr (_, c, [], args) ->
+      | CPatCstr (_, c, None, args) ->
         pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, args, []) ->
+      | CPatCstr (_, c, Some args, []) ->
         str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, expl_args, extra_args) ->
+      | CPatCstr (_, c, Some expl_args, extra_args) ->
         surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
         ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
 
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 5bd1569ce..3c4b8cb71 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -304,7 +304,13 @@ and pp_cases_pattern_expr cpe =
       xmlApply loc
         (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
           [pp_cases_pattern_expr cpe])
-  | CPatCstr (loc, ref, cpel1, cpel2) ->
+  | CPatCstr (loc, ref, None, cpel2) ->
+      xmlApply loc
+        (xmlOperator "reference"
+           ~attr:["name", Libnames.string_of_reference ref] loc ::
+         [Element ("impargs", [], []);
+          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+  | CPatCstr (loc, ref, Some cpel1, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::