Précalcul de la forme canonique des constructeurs et arités pour traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois

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

4 files changed, 48 insertions, 23 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index a48384389d..510e1f12b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -47,8 +47,11 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : typed_type array;
-  mind_arity : typed_type;
+  mind_nf_lc : typed_type array;
+  mind_nf_arity : typed_type;
+  (* lc and arity as given by user if not in nf; useful e.g. for Ensemble.v *)
+  mind_user_lc : constr array option;
+  mind_user_arity : constr option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -66,6 +69,14 @@ type mutual_inductive_body = {
 
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
+let mind_user_lc mip = match mip.mind_user_lc with
+  | None -> Array.map body_of_type mip.mind_nf_lc
+  | Some lc -> lc
+
+let mind_user_arity mip = match mip.mind_user_arity with
+  | None -> body_of_type mip.mind_nf_arity
+  | Some a -> a
+
 (*s Declaration. *)
 
 type mutual_inductive_entry = {
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 93a84c7c7b..7853a2ce1e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -53,8 +53,10 @@ type recarg =
 type one_inductive_body = {
   mind_consnames : identifier array;
   mind_typename : identifier;
-  mind_lc : typed_type array;
-  mind_arity : typed_type;
+  mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
+  mind_nf_arity : typed_type;
+  mind_user_lc : constr array option;
+  mind_user_arity : constr option;
   mind_sort : sorts;
   mind_nrealargs : int;
   mind_kelim : sorts list;
@@ -71,9 +73,9 @@ type mutual_inductive_body = {
   mind_nparams : int }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
-
-val mind_nth_type_packet : 
-  mutual_inductive_body -> int -> one_inductive_body
+val mind_user_lc : one_inductive_body -> constr array
+val mind_user_arity : one_inductive_body -> constr
+val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
 
 (*s Declaration of inductive types. *)
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 16139abfeb..cdfd27cd0a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -39,7 +39,7 @@ let mis_typed_lc mis =
   let ids = ids_of_sign mis.mis_mib.mind_hyps in
   let args = Array.to_list mis.mis_args in
   Array.map (fun t -> Instantiate.instantiate_type ids t args)
-    mis.mis_mip.mind_lc
+    mis.mis_mip.mind_nf_lc
 
 let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
 
@@ -58,7 +58,15 @@ let mis_type_mconstructs mispec =
   (Array.init nconstr make_Ck, 
    Array.map (substl (list_tabulate make_Ik ntypes)) specif)
 
-let mis_type_mconstruct i mispec =
+let mis_type_nf_mconstruct i mispec =
+  let specif = mis_lc mispec
+  and ntypes = mis_ntypes mispec
+  and nconstr = mis_nconstr mispec in
+  let make_Ik k = DOPN(MutInd(mispec.mis_sp,ntypes-k-1),mispec.mis_args) in 
+  if i > nconstr then error "Not enough constructors in the type";
+  substl (list_tabulate make_Ik ntypes) specif.(i-1)
+
+let mis_type_mconstruct i mispec = 
   let specif = mis_typed_lc mispec
   and ntypes = mis_ntypes mispec
   and nconstr = mis_nconstr mispec in
@@ -69,9 +77,13 @@ let mis_type_mconstruct i mispec =
 let mis_typed_arity mis =
   let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
   and largs = Array.to_list mis.mis_args in
-  Instantiate.instantiate_type idhyps mis.mis_mip.mind_arity largs
+  Instantiate.instantiate_type idhyps mis.mis_mip.mind_nf_arity largs
 
+(*
 let mis_arity mispec = incast_type (mis_typed_arity mispec)
+*)
+
+let mis_arity mis = body_of_type (mis_typed_arity mis)
 
 let mis_params_ctxt mispec =
   let paramsign,_ =
@@ -221,7 +233,7 @@ let lift_constructor n cs = {
 
 let get_constructor (IndFamily (mispec,params)) j =
   assert (j <= mis_nconstr mispec);
-  let typi = body_of_type (mis_type_mconstruct j mispec) in
+  let typi = mis_type_nf_mconstruct j mispec in
   let (args,ccl) = decompose_prod (prod_applist typi params) in
   let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
   { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) j;
@@ -233,9 +245,9 @@ let get_constructor (IndFamily (mispec,params)) j =
 let get_constructors (IndFamily (mispec,params) as indf) =
   Array.init (mis_nconstr mispec) (fun j -> get_constructor indf (j+1))
 
-let get_arity env sigma (IndFamily (mispec,params)) =
+let get_arity (IndFamily (mispec,params)) =
   let arity = mis_arity mispec in
-  splay_arity env sigma (prod_applist arity params)
+  destArity (prod_applist arity params)
 
 (* Functions to build standard types related to inductive *)
 
@@ -251,8 +263,8 @@ let build_dependent_inductive (IndFamily (mis, params)) =
      (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
 
 (* builds the arity of an elimination predicate in sort [s] *)
-let make_arity env sigma dep indf s =
-  let (arsign,_) = get_arity env sigma indf in
+let make_arity env dep indf s =
+  let (arsign,_) = get_arity indf in
   if dep then
     (* We need names everywhere *)
     it_prod_name env
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3033c09a9c..97118a5171 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -43,11 +43,13 @@ val mis_consnames : inductive_instance -> identifier array
 val mis_typed_arity : inductive_instance -> typed_type
 val mis_inductive : inductive_instance -> inductive
 val mis_arity : inductive_instance -> constr
-val mis_lc : inductive_instance -> constr array
-val mis_type_mconstructs : inductive_instance -> constr array * constr array
-val mis_type_mconstruct : int -> inductive_instance -> typed_type
 val mis_params_ctxt : inductive_instance -> (name * constr) list
 val mis_sort : inductive_instance -> sorts
+val mis_type_mconstruct : int -> inductive_instance -> typed_type
+
+(* The ccl of constructor is pre-normalised in the following functions *)
+val mis_lc : inductive_instance -> constr array
+val mis_type_mconstructs : inductive_instance -> constr array * constr array
 
 (*s [inductive_family] = [inductive_instance] applied to global parameters *)
 type inductive_family = IndFamily of inductive_instance * constr list
@@ -117,8 +119,7 @@ val build_dependent_inductive : inductive_family -> constr
    indf k] builds [(x1:A1)...(xn:An)sort] which is the arity of an
    elimination predicate on sort [k]; if [dep=true] then it rather
    builds [(x1:A1)...(xn:An)(I params x1...xn)->sort] *)
-val make_arity : env -> 'a evar_map -> bool -> inductive_family ->
-  sorts -> constr
+val make_arity : env -> bool -> inductive_family -> sorts -> constr
 
 (* [build_branch_type env dep p cs] builds the type of the branch
    associated to constructor [cs] in a Case with elimination predicate
@@ -162,15 +163,14 @@ val find_rectype : env -> 'a evar_map -> constr -> inductive_type
 
 val get_constructors : inductive_family -> constructor_summary array
 
-(* [get_arity env sigma inf] returns the product and the sort of the
+(* [get_arity inf] returns the product and the sort of the
    arity of the inductive family described by [is]; global parameters are
    already instanciated; [indf] must be defined w.r.t. [env] and [sigma];
    the products signature is relative to [env] and [sigma]; the names
    of the products of the constructors types are not renamed when
    [Anonymous] *)
 
-val get_arity : env -> 'a evar_map -> inductive_family ->
-      (name * constr) list * sorts
+val get_arity : inductive_family -> flat_arity
 
 (* Examples: assume