Timide tentative de clarification du statut de l'opérateur de filtrage

PCase dans le type pattern: le type pattern est utilisé
essentiellement dans ltac, il est normalement obtenu sans typage, et
ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est
obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à
part car sans le type, il est impossible de savoir le nombre
d'arguments du constructeur puisque par définition du "if", ceux-ci ne
sont pas liants et ne laissent pas dans la syntaxe concrète
(résolution au passage du bug #1070, dû à un filtrage incomplet dans
le passage de pattern à rawconstr permettant l'affichage des pattern).


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

1 files changed, 78 insertions, 24 deletions

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 634f0b5915..9029578cd2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -38,8 +38,9 @@ type constr_pattern =
   | PLetIn of name * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of patvar option
-  | PCase of (inductive option * case_style)
-      * constr_pattern option * constr_pattern * constr_pattern array
+  | PIf of constr_pattern * constr_pattern * constr_pattern
+  | PCase of (case_style * int array * inductive option * int option)
+      * constr_pattern * constr_pattern * constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -49,9 +50,10 @@ let rec occur_meta_pattern = function
   | PLambda (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PLetIn (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
-  | PCase(_,None,c,br)   ->
-      (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
-  | PCase(_,Some p,c,br) ->
+  | PIf (c,c1,c2)  ->
+      (occur_meta_pattern c) or
+      (occur_meta_pattern c1) or (occur_meta_pattern c2)
+  | PCase(_,p,c,br) ->
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PMeta _ | PSoApp _ -> true
@@ -70,6 +72,7 @@ let rec head_pattern_bound t =
     | PProd (_,_,b)  -> head_pattern_bound b 
     | PLetIn (_,_,b) -> head_pattern_bound b 
     | PApp (c,args)  -> head_pattern_bound c
+    | PIf (c,_,_)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
     | PVar id        -> VarRef id
@@ -103,14 +106,44 @@ let rec pattern_of_constr t =
     | Construct sp -> PRef (ConstructRef sp)
     | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
-	PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
-	       Some (pattern_of_constr p),pattern_of_constr a,
+	let cip = ci.ci_pp_info in
+	PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,Some cip.ind_nargs),
+	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
     | CoFix f -> PCoFix f
 
 (* To process patterns, we need a translation without typing at all. *)
 
+let map_pattern_with_binders g f l = function
+  | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
+  | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
+  | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
+  | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
+  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+  | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
+  | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
+  (* Non recursive *)
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
+  (* Bound to terms *)
+  | PFix _ | PCoFix _ as x) -> x
+
+let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+
+let rec instantiate_pattern lvar = function
+  | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
+  | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+  | c -> map_pattern (instantiate_pattern lvar) c
+
+let rec liftn_pattern k n = function
+  | PRel i as x -> if i >= n then PRel (i+k) else x
+  | PFix x -> PFix (destFix (liftn k n (mkFix x)))
+  | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
+  | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+
+let lift_pattern k = liftn_pattern k 1
+
+(*
 let rec inst lvar = function
   | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
   | PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
@@ -125,6 +158,7 @@ let rec inst lvar = function
   (* Bound to terms *)
   | (PFix _ | PCoFix _) ->
       error ("Not instantiable pattern")
+*)
 
 let rec subst_pattern subst pat = match pat with
   | PRef ref ->
@@ -160,12 +194,20 @@ let rec subst_pattern subst pat = match pat with
 	  PLetIn (name,c1',c2')
   | PSort _ 
   | PMeta _ -> pat
-  | PCase (cs,typ, c, branches) -> 
-      let typ' = option_smartmap (subst_pattern subst) typ in 
+  | PIf (c,c1,c2) ->
+      let c' = subst_pattern subst c in
+      let c1' = subst_pattern subst c1 in
+      let c2' = subst_pattern subst c2 in
+	if c' == c && c1' == c1 && c2' == c2 then pat else
+	  PIf (c',c1',c2')
+  | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+      let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+      let typ' = subst_pattern subst typ in 
       let c' = subst_pattern subst c in
       let branches' = array_smartmap (subst_pattern subst) branches in
+      let cs' = if ind == ind' then cs else (a,b,ind',n) in
 	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs,typ', c', branches') 
+	  PCase(cs',typ', c', branches') 
   | PFix fixpoint ->
       let cstr = mkFix fixpoint in
       let fixpoint' = destFix (subst_mps subst cstr) in
@@ -177,8 +219,8 @@ let rec subst_pattern subst pat = match pat with
 	if cofixpoint' == cofixpoint then pat else
 	  PCoFix cofixpoint'
 
-
-let instantiate_pattern = inst
+let mkPLambda na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambda = List.fold_right mkPLambda 
 
 let rec pat_of_raw metas vars = function
   | RVar (_,id) ->
@@ -212,17 +254,30 @@ let rec pat_of_raw metas vars = function
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
   | RIf (_,c,(_,None),b1,b2) ->
-      PCase ((None,IfStyle),None, pat_of_raw metas vars c,
-             [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
-  | RCases (loc,None,[c,_],brs) ->
-      let sp =
+      PIf (pat_of_raw metas vars c,
+           pat_of_raw metas vars b1,pat_of_raw metas vars b2)
+  | RLetTuple (loc,nal,(_,None),b,c) ->
+      let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in
+      let c = List.fold_left mkRLambda c nal in
+      PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
+             [|pat_of_raw metas vars c|])
+  | RCases (loc,p,[c,(na,indnames)],brs) ->
+      let pred,ind_nargs, ind = match p,indnames with
+	| Some p, Some (_,ind,nal) ->
+	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
+	    Some (List.length nal),Some ind
+	| _ -> PMeta None, None, None in
+      let ind = match ind with Some _ -> ind | None ->
 	match brs with
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
-      PCase ((sp,Term.RegularStyle),None,
-             pat_of_raw metas vars c,
-             Array.init (List.length brs)
-	       (pat_of_raw_branch loc metas vars sp brs))
+      let cbrs =
+	Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
+      in
+      let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
+      PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+             pat_of_raw metas vars c, brs)
+             
   | r ->
       let loc = loc_of_rawconstr r in
       user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
@@ -230,12 +285,12 @@ let rec pat_of_raw metas vars = function
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
     (function
-        (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
+        (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
           user_err_loc (loc,"pattern_of_rawconstr",
                         Pp.str "Not supported pattern")) brs in
   match bri with
-      [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
+    | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
           user_err_loc (loc,"pattern_of_rawconstr",
             Pp.str "All constructors must be in the same inductive type");
@@ -246,8 +301,7 @@ and pat_of_raw_branch loc metas vars ind brs i =
                   user_err_loc (loc,"pattern_of_rawconstr",
                                 Pp.str "Not supported pattern")) lv in
         let vars' = List.rev lna @ vars in 
-        List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna
-          (pat_of_raw metas vars' br)
+	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
     | _ -> user_err_loc (loc,"pattern_of_rawconstr",
                          str "No unique branch for " ++ int (i+1) ++
                          str"-th constructor")