- Utilisation d'abbréviations pour les types intervenant dans RCases

- Factorisation du procédé de transformation Cases -> RCases dans Detyping
- Rebranchement de la traduction XML pour Cases (interrompue depuis
  suppression traducteur)


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

7 files changed, 108 insertions, 75 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2cbbfca02..5efa68e2d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -27,6 +27,7 @@ open Pattern
 open Nametab
 open Notation
 open Reserve
+open Detyping
 (*i*)
 
 (* Translation from rawconstr to front constr *)
@@ -908,26 +909,20 @@ let rec raw_of_pat env = function
       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 =
+      let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
+      RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+  | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
+      let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
+      let brns = Array.to_list cstr_nargs in
+        (* ind is None only if no branch and no return type *)
+      let ind = out_some indo in
+      let mat = simple_cases_matrix_of_branches ind brns brs in
+      let indnames,rtn =
 	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)
+	else 
+	  let n = out_some ind_nargs in
+	  return_type_of_predicate ind n (raw_of_pat env p) in
+      RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 8b3661dbe..23fdfdaa2 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -19,6 +19,7 @@ open Tacexpr
 open Libnames
 
 open Nametab
+open Detyping
 
 (* Generic xml parser without raw data *)
 
@@ -95,7 +96,9 @@ let sort_of_cdata (loc,a) = match a with
 
 let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
 
-let get_xml_inductive_kn al = inductive_of_cdata (get_xml_attr "uri" al)
+let get_xml_inductive_kn al =
+  inductive_of_cdata (* uriType apparent synonym of uri *)
+    (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
 
 let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
 
@@ -113,6 +116,16 @@ let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
 
 let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
 
+(* A leak in the xml dtd: arities of constructor need to know global env *)
+
+let compute_branches_lengths ind =
+  let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  mip.Declarations.mind_consnrealdecls
+
+let compute_predicate_length ind =
+  let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  mip.Declarations.mind_nrealargs
+
 (* Interpreting constr as a rawconstr *)
 
 let rec interp_xml_constr = function
@@ -134,14 +147,16 @@ let rec interp_xml_constr = function
       failwith "META: TODO"
   | XmlTag (loc,"CONST",al,[]) ->
       RRef (loc, ConstRef (get_xml_constant al))
-  | XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *)
-      failwith "XML MUTCASE TO DO";
-(*
-      ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x),
-      interp_xml_inductiveTerm y,
-      Array.of_list (List.map interp_xml_pattern yl),
-      ref None)
-*)
+  | XmlTag (loc,"MUTCASE",al,x::y::yl) ->
+      let ind = get_xml_inductive al in
+      let p = interp_xml_patternsType x in
+      let tm = interp_xml_inductiveTerm y in
+      let brs = List.map interp_xml_pattern yl in
+      let brns = Array.to_list (compute_branches_lengths ind) in
+      let mat = simple_cases_matrix_of_branches ind brns brs in
+      let n = compute_predicate_length ind in
+      let nal,rtn = return_type_of_predicate ind n p in
+      RCases (loc,rtn,[tm,nal],mat)
   | XmlTag (loc,"MUTIND",al,[]) ->
       RRef (loc, IndRef (get_xml_inductive al))
   | XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index e9fba44d2..17d74a9fd 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -41,13 +41,9 @@ val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
 module type S = sig
   val compile_cases :
     loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
-      evar_defs ref ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
-    env ->
-    rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list *
-      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index edbbbb329..6789459e8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -277,6 +277,25 @@ let extract_nondep_branches test c b n =
       | _ -> assert false in
   if test c n then Some (strip n b) else None
 
+let it_destRLambda_or_LetIn_names n c =
+  let rec aux n nal c =
+    if n=0 then (List.rev nal,c) else match c with
+      | RLambda (_,na,_,c) -> aux (n-1) (na::nal) c
+      | RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
+      | _ ->
+          (* eta-expansion *)
+	  let rec next l =
+	    let x = Nameops.next_ident_away (id_of_string "x") l in
+	    (* Not efficient but unusual and no function to get free rawvars *)
+	    if occur_rawconstr x c then next (x::l) else x in
+	  let x = next [] in 
+	  let a = RVar (dl,x) in
+	  aux (n-1) (Name x :: nal) 
+            (match c with
+              | RApp (loc,p,l) -> RApp (loc,c,l@[a])
+              | _ -> (RApp (dl,c,[a])))
+  in aux n [] c
+
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
   let (indsp,st,nparams,consnargsl,k) = data in
   let synth_type = synthetize_type () in
@@ -289,21 +308,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       match option_app detype p with
         | None -> Anonymous, None, None
         | Some p ->
-            let decompose_lam k c =
-              let rec lamdec_rec l avoid k c =
-                if k = 0 then List.rev l,c else match c with
-                  | RLambda (_,x,t,c) -> 
-                      lamdec_rec (x::l) (name_cons x avoid) (k-1) c
-                  | c -> 
-                      let x = next_ident_away (id_of_string "x") avoid in
-                      lamdec_rec ((Name x)::l) (x::avoid) (k-1)
-                        (let a = RVar (dl,x) in
-                          match c with
-                          | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                          | _ -> (RApp (dl,c,[a])))
-              in 
-              lamdec_rec [] [] k c in
-            let nl,typ = decompose_lam k p in
+            let nl,typ = it_destRLambda_or_LetIn_names k p in
 	    let n,typ = match typ with 
               | RLambda (_,x,t,c) -> x, c
 	      | _ -> Anonymous, typ in
@@ -331,22 +336,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
   match tag with
   | LetStyle when aliastyp = None -> 
       let bl' = Array.map detype bl in
-      let rec decomp_lam_force n avoid l p =
-	if n = 0 then (List.rev l,p) else
-          match p with
-            | RLambda (_,na,_,c) -> 
-		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
-            | RLetIn (_,na,_,c) -> 
-		decomp_lam_force (n-1) (name_cons na avoid) (na::l) c
-            | _ ->
-		let x = Nameops.next_ident_away (id_of_string "x") avoid in
-		decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-                  (* eta-expansion *)
-                  (let a = RVar (dl,x) in
-                  match p with
-                    | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                    | _ -> (RApp (dl,p,[a]))) in
-      let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl'.(0) in
+      let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
       RLetTuple (dl,nal,(alias,pred),tomatch,d)
   | IfStyle when aliastyp = None ->
       let bl' = Array.map detype bl in
@@ -645,3 +635,18 @@ let rec subst_rawconstr subst raw =
 	  RCast (loc,r1',k,r2')
 
   | RDynamic _ -> raw
+
+(* Utilities to transform kernel cases to simple pattern-matching problem *)
+
+let simple_cases_matrix_of_branches ind brns brs =
+  list_map2_i (fun i n b ->
+      let nal,c = it_destRLambda_or_LetIn_names n b in
+      let mkPatVar na = PatVar (dummy_loc,na) in
+      let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in
+      let ids = map_succeed Nameops.out_name nal in
+      (dummy_loc,ids,[p],c))
+    0 brns brs
+
+let return_type_of_predicate ind n pred =
+  let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
+  (List.hd nal, Some (dummy_loc,ind,List.tl nal)), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 71aed9373..4b0adabbd 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -47,3 +47,12 @@ val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 val force_if : case_info -> bool
 val force_let : case_info -> bool
+
+(* Utilities to transform kernel cases to simple pattern-matching problem *)
+
+val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
+val simple_cases_matrix_of_branches : 
+  inductive -> int list -> rawconstr list -> cases_clauses
+val return_type_of_predicate :
+  inductive -> int -> rawconstr -> predicate_pattern * rawconstr option
+
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 36edf519b..86ed95106 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,6 +47,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type predicate_pattern = name * (loc * inductive * name list) option
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -56,9 +58,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -73,7 +73,14 @@ and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
+
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 8ef0cb939..d20b3fce4 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -44,6 +44,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type predicate_pattern = name * (loc * inductive * name list) option
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -53,9 +55,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -70,10 +70,16 @@ and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
+
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
 
-val cases_predicate_names : 
-  (rawconstr * (name * (loc * inductive * name list) option)) list -> name list
+val cases_predicate_names : tomatch_tuple -> name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the