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

6 files changed, 152 insertions, 48 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2fe967153f..2cbbfca028 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -873,6 +873,13 @@ let extern_type at_top env t =
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
+let it_destPLambda n c =
+  let rec aux n nal c =
+    if n=0 then (nal,c) else match c with
+      | PLambda (na,_,c) -> aux (n-1) (na::nal) c
+      | _ -> anomaly "it_destPLambda" in
+  aux n [] c
+
 let rec raw_of_pat env = function
   | PRef ref -> RRef (loc,ref)
   | PVar id -> RVar (loc,id)
@@ -897,20 +904,30 @@ let rec raw_of_pat env = function
       RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PLambda (na,t,c) ->
       RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
-  | PCase ((_,cs),typopt,tm,[||]) ->
-      if typopt <> None then failwith "TODO: PCase to RCases";
-      RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None,
-         [raw_of_pat env tm,(Anonymous,None)],[])
-  | PCase ((Some ind,cs),typopt,tm,bv) ->
-      let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
-      let mib,mip = lookup_mind_specif (Global.env()) ind in
-      let k = mip.Declarations.mind_nrealargs in
-      let nparams = mib.Declarations.mind_nparams in
-      let cstrnargs = mip.Declarations.mind_consnrealdecls in
-      Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env)
-	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
-	avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
-  | PCase _ -> error "Unsupported case-analysis while printing pattern"
+  | PIf (c,b1,b2) ->
+      RIf (loc, raw_of_pat env c, (Anonymous,None), 
+           raw_of_pat env b1, raw_of_pat env b2)
+  | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
+      let nal,b = it_destPLambda n b in
+      RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,raw_of_pat env b)
+  | PCase ((_,cstr_nargs,ind,ind_nargs),p,tm,bv) ->
+      let brs =
+	array_map2_i (fun i n b ->
+	  let nal,c = it_destPLambda n b in
+	  let mkPatVar na = PatVar (loc,na) in
+             (* ind is None only if no branch and no return type *) 
+	  let cs = (out_some ind,i+1) in
+	  let p = PatCstr (loc,cs,List.map mkPatVar nal,Anonymous) in
+	  let ids = map_succeed out_name nal in
+	  (loc,ids,[p],raw_of_pat (nal@env) c)) cstr_nargs bv in
+      let decompose_pred n p =
+	let nal,p = it_destPLambda (n+1) p in
+	(List.hd nal, Some (loc,out_some ind,List.tl nal)),
+	Some (raw_of_pat env p) in
+      let indnames,pred =
+	if p = PMeta None then (Anonymous,None),None
+	else decompose_pred (out_some ind_nargs) p in
+      RCases (loc,pred,[raw_of_pat env tm,indnames],Array.to_list brs)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 462fe1eb1d..2b0a0ac7b2 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -17,6 +17,7 @@ open Termops
 open Reductionops
 open Term
 open Rawterm
+open Sign
 open Environ
 open Pattern
 (*i*)
@@ -70,6 +71,11 @@ let memb_metavars m n =
 
 let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
 
+let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
+  match ind with
+  | Some ind -> ind = ci2.ci_ind
+  | None -> cs1 = ci2.ci_cstr_nargs
+
 let matches_core convert allow_partial_app pat c = 
   let rec sorec stk sigma p t =
     let cT = strip_outer_cast t in
@@ -79,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
 	    List.map
 	      (function
 		 | PRel n -> n
-		 | _ -> error "Only bound indices are currently allowed in second order pattern matching")
+		 | _ -> error "Only bound indices allowed in second order pattern matching")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
@@ -150,15 +156,27 @@ let matches_core convert allow_partial_app pat c =
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
-      | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
-	  (* On ne teste pas le prédicat *)
-          if (Array.length br1) = (Array.length br2) then
-  	    array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
+      | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
+	  let ctx,b2 = decompose_prod_n_assum ci.ci_cstr_nargs.(0) b2 in
+	  let ctx',b2' = decompose_prod_n_assum ci.ci_cstr_nargs.(1) b2' in
+	  let n = List.length ctx and n' = List.length ctx' in
+	  if noccur_between 1 n b2 & noccur_between 1 n' b2' then
+	    let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
+	    let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+	    let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
+  	    sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
           else
             raise PatternMatchingFailure
-      (* À faire *)
-      |	PFix f0, Fix f1 when f0 = f1 -> sigma
-      |	PCoFix c0, CoFix c1 when c0 = c1 -> sigma
+
+      | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
+	  if same_case_structure ci1 ci2 br1 br2 then
+  	    array_fold_left2 (sorec stk) 
+	      (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+          else
+            raise PatternMatchingFailure
+
+      |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
+      |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
       | _ -> raise PatternMatchingFailure
 
   in 
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")
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 0815f87211..4093f5e110 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -39,8 +39,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
 
@@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr ->
 
 val instantiate_pattern :
   (identifier * constr_pattern) list -> constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e4327..8e8b8059f9 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1 +1,4 @@
 intro H; split; [  a H |  e H ].
+intros; match goal with
+        | |- context [if ?X then _ else _] => case X
+        end; trivial.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 24a33651cd..8fa9199408 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,3 +7,12 @@ Lemma test : True -> True /\ True.
 intro H; split; [a H|e H].
 Show Script.
 Qed.
+
+(* Test printing of match context *)
+(* Used to fail after translator removal (see bug #1070) *)
+
+Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
+Proof.
+intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
+Show Script.
+Qed.