Extension des motifs disjonctifs au cas de disjonction de motifs multiples

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

7 files changed, 31 insertions, 17 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e8fd52dba..2a11f55c9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -336,8 +336,8 @@ and
   | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
                                      List.map xlate_match_pattern l)
 and  translate_one_equation = function
-    (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp,
-	     xlate_formula a)
+    (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+  | _ -> xlate_error "TODO: disjunctive multiple patterns"
 and 
   xlate_binder_ne_list = function
     [] -> assert false
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a81ca599c..44f4baee6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -186,7 +186,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 check_same_pattern pl1 pl2;
+        List.iter2 (List.iter2 check_same_pattern) pl1 pl2;
         check_same_type r1 r2) brl1 brl2
   | CHole _, CHole _ -> ()
   | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -797,7 +797,7 @@ and extern_local_binder scopes vars = function
              LocalRawAssum([(dummy_loc,na)],ty) :: l))
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
-  (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
+  (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 deb7abbde..aa9a379db 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -81,9 +81,8 @@ let explain_non_linear_pattern id =
   str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
 
 let explain_bad_patterns_number n1 n2 =
-  let s = if n1 > 1 then "s" else "" in
-  str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found "
-    ++ int n2
+  str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
+  str " but found " ++ int n2
 
 let explain_bad_explicitation_number n po =
   match n with
@@ -357,7 +356,8 @@ 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_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs))
+ join_loc (cases_pattern_loc (List.hd (List.hd lhs)))
+          (cases_pattern_loc (list_last (list_last lhs)))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -929,11 +929,24 @@ let internalise sigma globalenv env allow_soapp lvar c =
         ((name_fold Idset.add na ids,ts,sc),
          (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
-  and intern_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) =
+  (* Expands a multiple pattern into a disjunction of multiple patterns *)
+  and intern_multiple_pattern scopes pl =
     let idsl_pll = 
-      List.map (intern_cases_pattern globalenv scopes ([],[]) None) lhs in
-
-    let eqn_ids,pll = product_of_cases_patterns [] idsl_pll in
+      List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+    product_of_cases_patterns [] idsl_pll
+
+  (* Expands a disjunction of multiple pattern *)
+  and intern_disjunctive_multiple_pattern scopes loc mpl =
+    assert (mpl <> []);
+    let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+    let (idsl,mpl') = List.split mpl' in
+    let ids = List.hd idsl in
+    check_or_pat_variables loc ids (List.tl idsl);
+    (ids,List.flatten mpl')
+
+  (* 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
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
     check_number_of_pattern loc n (snd (List.hd pll));
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6e7ea0f9c..855fcb329 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -515,7 +515,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 * constr_expr) list
+      (loc * cases_pattern_expr list 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/interp/topconstr.mli b/interp/topconstr.mli
index 57a2c976c..e06a48215 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -98,7 +98,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 * constr_expr) list
+      (loc * cases_pattern_expr list 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/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 2a975a964..443a10511 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -274,7 +274,8 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   eqn:
-    [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
+    [ [ pll = LIST0 LIST1 pattern LEVEL "99" SEP "," SEP "|"; 
+        "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
   ;
   pattern:
     [ "200" RIGHTA [ ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 613fbfe78..92b07e08b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -186,12 +186,12 @@ let rec pr_patt sep inh p =
 
 let pr_patt = pr_patt mt
 
-
 let pr_eqn pr (loc,pl,rhs) =
   spc() ++ hov 4
     (pr_with_comments loc
       (str "| " ++
-      hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
+      hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl 
+             ++ str " =>") ++
       pr_sep_com spc (pr ltop) rhs))
 
 let begin_of_binder = function