Peaufinement nouveaux types inductive_summary et constructor_summary en vue

de remplacer mispec


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

1 files changed, 30 insertions, 9 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 41342e6d4e..d235245e64 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -51,16 +51,27 @@ let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
 let mis_consnames mis = mis.mis_mip.mind_consnames
 
+type constructor_summary = {
+  cs_cstr : constructor;
+  cs_params : constr list;
+  cs_nargs : int;
+  cs_args : (name * constr) list;
+  cs_concl_realargs : constr array
+}
+
 (* A light version of mind_specif_of_mind with pre-splitted args *)
-type inductive_summary =
-    {fullmind : constr;
-     mind : inductive;
-     nparams : int;
-     nrealargs : int;
-     nconstr : int;
-     params : constr list;
-     realargs : constr list;
-     arity : constr}
+(* and a receipt to build a summary of constructors *)
+type inductive_summary = {
+  fullmind : constr;
+  mind : inductive;
+  params : constr list;
+  realargs : constr list;
+  nparams : int;
+  nrealargs : int;
+  nconstr : int;
+  make_arity : inductive -> constr list -> (name * constr) list * sorts;
+  make_constrs : inductive -> constr list -> constructor_summary array
+}
 
 let is_recursive listind = 
   let rec one_is_rec rvec = 
@@ -174,3 +185,13 @@ let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
 
 let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
 let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
+
+let build_dependent_constructor cs =
+  applist
+    (mkMutConstruct cs.cs_cstr,
+     (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
+
+let build_dependent_inductive is =
+  applist 
+    (mkMutInd is.mind,
+     (List.map (lift is.nparams) is.params)@(rel_list 0 is.nrealargs))