Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed

to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body)
instead of looking it up in the environment. A version of the same functions
with the old type is put in Inductiveops (outside the kernel).


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

4 files changed, 19 insertions, 17 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5f9f907f52..5aee04f7d7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -317,9 +317,10 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) =
 
 let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   let auxntyp = 1 in
+  let specif = lookup_mind_specif env mi in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive env mi) lpar) env in
+              hnf_prod_applist env (type_of_inductive specif) lpar) env in
   let ra_env' = 
     (Imbr mi,Rtree.mk_param 0) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 545b5b83a1..ab2177f75c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,6 +18,8 @@ open Environ
 open Reduction
 open Type_errors
 
+type mind_specif = mutual_inductive_body * one_inductive_body
+
 (* raise Not_found if not an inductive type *)
 let lookup_mind_specif env (kn,tyi) =
   let mib = Environ.lookup_mind kn env in
@@ -93,16 +95,13 @@ let full_constructor_instantiate (((mind,_),mib,mip),params) =
 
 (* Type of an inductive type *)
 
-let type_of_inductive env i =
-  let (_,mip) = lookup_mind_specif env i in
-  mip.mind_user_arity
+let type_of_inductive (_,mip) = mip.mind_user_arity
 
 (************************************************************************)
 (* Type of a constructor *)
 
-let type_of_constructor env cstr =
+let type_of_constructor cstr (mib,mip) =
   let ind = inductive_of_constructor cstr in
-  let (mib,mip) = lookup_mind_specif env ind in
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
@@ -113,8 +112,8 @@ let arities_of_specif kn (mib,mip) =
   let specif = mip.mind_nf_lc in
   Array.map (constructor_instantiate kn mib) specif
 
-let arities_of_constructors env ind = 
-  arities_of_specif (fst ind) (lookup_mind_specif env ind)
+let arities_of_constructors ind specif = 
+  arities_of_specif (fst ind) specif
 
 
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 0ecfe2a8c4..0174b80201 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -28,24 +28,24 @@ val find_rectype     : env -> types -> inductive * constr list
 val find_inductive   : env -> types -> inductive * constr list
 val find_coinductive : env -> types -> inductive * constr list
 
+type mind_specif = mutual_inductive_body * one_inductive_body
+
 (*s Fetching information in the environment about an inductive type.
     Raises [Not_found] if the inductive type is not found. *)
-val lookup_mind_specif :
-  env -> inductive -> mutual_inductive_body * one_inductive_body
+val lookup_mind_specif : env -> inductive -> mind_specif
 
 (*s Functions to build standard types related to inductive *)
 
-val type_of_inductive    : env -> inductive -> types
+val type_of_inductive : mind_specif -> types
 
 (* Return type as quoted by the user *)
-val type_of_constructor  : env -> constructor -> types
+val type_of_constructor : constructor -> mind_specif -> types
 
 (* Return constructor types in normal form *)
-val arities_of_constructors : env -> inductive -> types array
+val arities_of_constructors : inductive -> mind_specif -> types array
 
 (* Transforms inductive specification into types (in nf) *)
-val arities_of_specif : mutual_inductive -> 
-  mutual_inductive_body * one_inductive_body -> types array 
+val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 05b7619e52..1a3dd19f88 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,7 +252,8 @@ let judge_of_inductive env i =
     let (kn,_) = i in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_inductive env i)
+  let specif = lookup_mind_specif env i in
+  make_judge constr (type_of_inductive specif)
 
 (*
 let toikey = Profile.declare_profile "judge_of_inductive";;
@@ -268,7 +269,8 @@ let judge_of_constructor env c =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
     check_args env constr mib.mind_hyps in 
-  make_judge constr (type_of_constructor env c)
+  let specif = lookup_mind_specif env (inductive_of_constructor c) in
+  make_judge constr (type_of_constructor c specif)
 
 (*
 let tockey = Profile.declare_profile "judge_of_constructor";;