Correction bug #1749 (datant de l'implantation des or-patterns) +

amélioration message d'erreur si nombre de pattern incorrect.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 25 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7e288f3117..06edeaed20 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -198,7 +198,7 @@ let rec check_same_type ty1 ty2 =
   | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
-        List.iter2 (List.iter2 check_same_pattern) pl1 pl2;
+        List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
         check_same_type r1 r2) brl1 brl2
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -817,7 +817,7 @@ and extern_local_binder scopes vars = function
              LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
-  (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
+  (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
 and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3214ca6c45..033052325a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -368,8 +368,7 @@ let rec has_duplicate = function
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let loc_of_lhs lhs = 
- join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs)))
-          (cases_pattern_expr_loc (list_last (list_last lhs)))
+ join_loc (fst (List.hd lhs)) (fst (list_last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -960,15 +959,16 @@ let internalise sigma globalenv env allow_patvar lvar c =
          (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
-  and intern_multiple_pattern scopes pl =
+  and intern_multiple_pattern scopes n (loc,pl) =
     let idsl_pll = 
       List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+    check_number_of_pattern loc n pl;
     product_of_cases_patterns [] idsl_pll
 
   (* Expands a disjunction of multiple pattern *)
-  and intern_disjunctive_multiple_pattern scopes loc mpl =
+  and intern_disjunctive_multiple_pattern scopes loc n mpl =
     assert (mpl <> []);
-    let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+    let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
     let (idsl,mpl') = List.split mpl' in
     let ids = List.hd idsl in
     check_or_pat_variables loc ids (List.tl idsl);
@@ -976,10 +976,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
   and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
-    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in
+    let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-    check_number_of_pattern loc n (snd (List.hd pll));
     let env_ids = List.fold_right Idset.add eqn_ids ids in
     List.map (fun (subst,pl) ->
       let rhs = replace_vars_constr_expr subst rhs in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2994bc3aea..aa3c923ebf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -560,7 +560,7 @@ type constr_expr =
       (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list list * constr_expr) list
+      (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
@@ -688,7 +688,9 @@ let rec cases_pattern_fold_names f a = function
   | CPatPrim _ | CPatAtom _ -> a
 
 let ids_of_pattern_list =
-  List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add))
+  List.fold_left
+    (located_fold_left 
+      (List.fold_left (cases_pattern_fold_names Idset.add)))
     Idset.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 608cedb3c1..fa7940faa8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -120,7 +120,7 @@ type constr_expr =
         (constr_expr * explicitation located option) list
   | CCases of loc * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
-      (loc * cases_pattern_expr list list * constr_expr) list
+      (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
diff --git a/lib/util.ml b/lib/util.ml
index 6dd0a792b2..32ede2fb24 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -34,6 +34,9 @@ let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
 
+let located_fold_left f x (_,a) = f x a 
+let located_iter2 f (_,a) (_,b) = f a b
+
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
 
diff --git a/lib/util.mli b/lib/util.mli
index d52db650ac..8e3ec2cb40 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -43,6 +43,8 @@ val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
 val join_loc : loc -> loc -> loc
+val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 
 (* Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index c649b58466..a7d905032b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -203,8 +203,9 @@ GEXTEND Gram
           CLetTuple (loc,List.map snd lb,po,c1,c2)
       | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern;
           "in"; c2 = operconstr LEVEL "200" ->
+	 let loc' = cases_pattern_expr_loc p in
          CCases (loc, None, [(c1, (None, None))],
-                 [loc, [[p]], c2])
+                 [loc, [loc',[p]], c2])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -274,8 +275,11 @@ GEXTEND Gram
   branches:
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
+  mult_pattern:
+    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (loc,pl) ] ]
+  ;
   eqn:
-    [ [ pll = LIST1 LIST1 pattern LEVEL "99" SEP "," SEP "|"; 
+    [ [ pll = LIST1 mult_pattern SEP "|";
         "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
   ;
   pattern:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 85bf11806e..ed4386ada0 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -197,6 +197,7 @@ let rec pr_patt sep inh p =
 let pr_patt = pr_patt mt
 
 let pr_eqn pr (loc,pl,rhs) =
+  let pl = List.map snd pl in
   spc() ++ hov 4
     (pr_with_comments loc
       (str "| " ++