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, 31 insertions, 14 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)