- 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

5 files changed, 70 insertions, 47 deletions

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