From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 pretyping/inductiveops.ml | 59 ++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 46 insertions(+), 13 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 57d966f1..e0cdeeee 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductiveops.ml 8653 2006-03-22 09:41:17Z herbelin $ *)
+(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Util
 open Names
@@ -116,11 +116,15 @@ let constructor_nrealhyps env (ind,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls.(j-1)
 
+let get_full_arity_sign env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_arity_ctxt
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt
+  mib.mind_nparams, mip.mind_nrealargs
 
 (* Annotation for cases *)
 let make_case_info env ind style pats_source =
@@ -196,10 +200,40 @@ let rec instantiate args c = match kind_of_term c, args with
   | _, [] -> c
   | _ -> anomaly "too short arity"
 
+(* substitution in a signature *)
+
+let substnl_rel_context subst n sign =
+  let rec aux n = function
+  | d::sign -> substnl_decl subst n d :: aux (n+1) sign
+  | [] -> []
+  in List.rev (aux n (List.rev sign))
+
+let substl_rel_context subst = substnl_rel_context subst 0
+
+let rec instantiate_context sign args =
+  let rec aux subst = function
+  | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args)
+  | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args)
+  | [], [] -> subst
+  | _ -> anomaly "Signature/instance mismatch in inductive family"
+  in aux [] (List.rev sign,args)
+
 let get_arity env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let arity = mip.mind_nf_arity in
-  destArity (instantiate params arity)
+  let parsign =
+    (* Dynamically detect if called with an instance of recursively
+       uniform parameter only or also of non recursively uniform
+       parameters *)
+    let parsign = mib.mind_params_ctxt in
+    let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
+    if List.length params = rel_context_nhyps parsign - nnonrecparams then
+      snd (list_chop nnonrecparams mib.mind_params_ctxt)
+    else
+      parsign in
+  let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
+  let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in
+  let subst = instantiate_context parsign params in
+  (substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
 
 (* Functions to build standard types related to inductive *)
 let build_dependent_constructor cs =
@@ -284,12 +318,12 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the Case
    and Inversion (case_then_using et case_nodep_then_using) tactics. *)
 
-let is_predicate_explicitly_dep env pred nodep_ar = 
-  let rec srec env pval nodep_ar =
+let is_predicate_explicitly_dep env pred arsign = 
+  let rec srec env pval arsign =
     let pv' = whd_betadeltaiota env Evd.empty pval in
-    match kind_of_term pv', kind_of_term nodep_ar with
-      | Lambda (na,t,b), Prod (_,_,a') ->
-	  srec (push_rel_assum (na,t) env) b a'
+    match kind_of_term pv', arsign with
+      | Lambda (na,t,b), (_,None,_)::arsign ->
+	  srec (push_rel_assum (na,t) env) b arsign
       | Lambda (na,_,_), _ ->
 
        (* The following code has impact on the introduction names
@@ -317,12 +351,11 @@ let is_predicate_explicitly_dep env pred nodep_ar =
 
       | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate"
   in
-  srec env pred nodep_ar
+  srec env pred arsign
 
 let is_elim_predicate_explicitly_dependent env pred indf =
-  let arsign,s = get_arity env indf in
-  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
-  is_predicate_explicitly_dep env pred glob_t
+  let arsign,_ = get_arity env indf in
+  is_predicate_explicitly_dep env pred arsign
 
 let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
-- 
cgit v1.2.3