petit nettoyage de kernel/inductive

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

3 files changed, 110 insertions, 167 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b4a74061f..b45e501eb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -18,69 +18,45 @@ open Environ
 open Reduction
 open Type_errors
 
-exception Induc
-
-(* raise Induc if not an inductive type *)
+(* raise Not_found if not an inductive type *)
 let lookup_mind_specif env (sp,tyi) =
-  let mib =
-    try Environ.lookup_mind sp env
-    with Not_found -> raise Induc in
+  let mib = Environ.lookup_mind sp env in
   if tyi >= Array.length mib.mind_packets then
     error "Inductive.lookup_mind_specif: invalid inductive index";
   (mib, mib.mind_packets.(tyi))
 
-let lookup_recargs env ind =
-  let (mib,mip) = lookup_mind_specif env ind in
-  Array.map (fun mip -> mip.mind_listrec) mib.mind_packets
-
-let lookup_subterms env (_,i as ind) =
-  (lookup_recargs env ind).(i)
-
 let find_rectype env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
         when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
     | Ind ind
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
-    | _ -> raise Induc
+    | _ -> raise Not_found
 
 (***********************************************************************)
 
-type inductive_instance = {
-  mis_sp : section_path;
-  mis_mib : mutual_inductive_body;
-  mis_tyi : int;
-  mis_mip : one_inductive_body }
-
-let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_inductive mis = (mis.mis_sp,mis.mis_tyi)
-
-let lookup_mind_instance (sp,tyi) env =
-  let (mib,mip) = lookup_mind_specif env (sp,tyi) in
-  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_mip = mip }
-
 (* Build the substitution that replaces Rels by the appropriate *)
 (* inductives *)
-let ind_subst mispec =
-  let ntypes = mispec.mis_mib.mind_ntypes in
-  let make_Ik k = mkInd (mispec.mis_sp,ntypes-k-1) in 
+let ind_subst mind mib =
+  let ntypes = mib.mind_ntypes in
+  let make_Ik k = mkInd (mind,ntypes-k-1) in 
   list_tabulate make_Ik ntypes
 
-(* Instantiate both section variables and inductives *)
-let constructor_instantiate mispec c =
-  let s = ind_subst mispec in
+(* Instantiate inductives in constructor type *)
+let constructor_instantiate mind mib c =
+  let s = ind_subst mind mib in
   type_app (substl s) c
 
 (* Instantiate the parameters of the inductive type *)
@@ -102,13 +78,13 @@ let instantiate_params t args sign =
   if rem_args <> [] then fail();
   type_app (substl subs) ty
 
-let full_inductive_instantiate (mispec,params) t =
-  instantiate_params t params mispec.mis_mip.mind_params_ctxt
+let full_inductive_instantiate mip params t =
+  instantiate_params t params mip.mind_params_ctxt
 
-let full_constructor_instantiate (mispec,params) =
-  let inst_ind = constructor_instantiate mispec in
+let full_constructor_instantiate (((mind,_),mib,mip),params) =
+  let inst_ind = constructor_instantiate mind mib in
   (fun t ->
-    instantiate_params (inst_ind t) params mispec.mis_mip.mind_params_ctxt)
+    instantiate_params (inst_ind t) params mip.mind_params_ctxt)
 
 (***********************************************************************)
 (***********************************************************************)
@@ -118,71 +94,47 @@ let full_constructor_instantiate (mispec,params) =
 (* Type of an inductive type *)
 
 let type_of_inductive env i =
-  let mis = lookup_mind_instance i env in
-  let hyps = mis.mis_mib.mind_hyps in
-  mis.mis_mip.mind_user_arity
-
-(* The same, with parameters instantiated *)
-let get_arity (mispec,params as indf) =
-  let arity = mispec.mis_mip.mind_nf_arity in
-  destArity (full_inductive_instantiate indf arity)
+  let (_,mip) = lookup_mind_specif env i in
+  mip.mind_user_arity
 
 (***********************************************************************)
 (* Type of a constructor *)
 
 let type_of_constructor env cstr =
   let ind = inductive_of_constructor cstr in
-  let mispec = lookup_mind_instance ind env in
-  let specif = mispec.mis_mip.mind_user_lc 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 = mis_nconstr mispec in
+  let nconstr = Array.length mip.mind_consnames in
   if i > nconstr then error "Not enough constructors in the type";
-  constructor_instantiate mispec specif.(i-1)
+  constructor_instantiate (fst ind) mib specif.(i-1)
 
 let arities_of_constructors env ind = 
-  let mispec = lookup_mind_instance ind env in
-  let specif = mispec.mis_mip.mind_user_lc in
-  Array.map (constructor_instantiate mispec) specif
+  let (mib,mip) = lookup_mind_specif env ind in
+  let specif = mip.mind_nf_lc in
+  Array.map (constructor_instantiate (fst ind) mib) specif
 
 
 
-(* gives the vector of constructors and of 
-   types of constructors of an inductive definition 
-   correctly instanciated *)
+(***********************************************************************)
 
-let mis_nf_constructor_type i mispec =
-  let nconstr = mis_nconstr mispec in
-  if i > nconstr then error "Not enough constructors in the type";
-  constructor_instantiate mispec mispec.mis_mip.mind_nf_lc.(i-1)
-   
-(*s Useful functions *)
-
-type constructor_summary = {
-  cs_cstr : constructor;
-  cs_params : constr list;
-  cs_nargs : int;
-  cs_args : rel_context;
-  cs_concl_realargs : constr array
-}
-
-let process_constructor ((mispec,params) as indf) j typi =
-  let typi = full_constructor_instantiate indf typi in
-  let (args,ccl) = decompose_prod_assum typi in
-  let (_,allargs) = decompose_app ccl in
-  let (_,vargs) = list_chop mispec.mis_mip.mind_nparams allargs in
-  { cs_cstr = ith_constructor_of_inductive (mis_inductive mispec) (j+1);
-    cs_params = params;
-    cs_nargs = rel_context_length args;
-    cs_args = args;
-    cs_concl_realargs = Array.of_list vargs }
-
-let get_constructors ((mispec,params) as indf) =
-  let constr_tys = mispec.mis_mip.mind_nf_lc in
-  Array.mapi (process_constructor indf) constr_tys
+let is_info_arity env c =
+  match dest_arity env c with
+    | (_,Prop Null) -> false 
+    | (_,Prop Pos)  -> true 
+    | (_,Type _)    -> true
 
-(***********************************************************************)
+let error_elim_expln env kp ki =
+  if is_info_arity env kp && not (is_info_arity env ki) then
+    NonInformativeToInformative
+  else 
+    match (kind_of_term kp,kind_of_term ki) with 
+      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
+      | _ -> WrongArity
 
-(* Type of case branches *)
+exception Arity of (constr * constr * arity_error) option
+
+(* Type of case predicates *)
 
 let local_rels ctxt =
   let (rels,_) =
@@ -196,48 +148,23 @@ let local_rels ctxt =
   in
   rels
 
-let build_dependent_constructor cs =
-  applist
-    (mkConstruct cs.cs_cstr,
-     (List.map (lift cs.cs_nargs) cs.cs_params)@(local_rels cs.cs_args))
+(* Get type of inductive, with parameters instantiated *)
+let get_arity mip params =
+  let arity = mip.mind_nf_arity in
+  destArity (full_inductive_instantiate mip params arity)
 
-let build_dependent_inductive ((mis, params) as indf) =
-  let arsign,_ = get_arity indf in
-  let nrealargs = mis.mis_mip.mind_nrealargs in
+let build_dependent_inductive ind mip params =
+  let arsign,_ = get_arity mip params in
+  let nrealargs = mip.mind_nrealargs in
   applist 
-    (mkInd (mis_inductive mis),
-     (List.map (lift nrealargs) params)@(local_rels arsign))
-
-(* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type dep p cs =
-  let args =
-    if dep then
-      Array.append cs.cs_concl_realargs [|build_dependent_constructor cs|]
-    else
-      cs.cs_concl_realargs in
-  let base = beta_appvect (lift cs.cs_nargs p) args in
-  it_mkProd_or_LetIn base cs.cs_args
-
-
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
+    (mkInd ind, (List.map (lift nrealargs) params)@(local_rels arsign))
 
-let error_elim_expln env kp ki =
-  if is_info_arity env kp && not (is_info_arity env ki) then
-    NonInformativeToInformative
-  else 
-    match (kind_of_term kp,kind_of_term ki) with 
-      | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
-      | _ -> WrongArity
 
-exception Arity of (constr * constr * arity_error) option
-
-
-let is_correct_arity env kelim (c,pj) indf t = 
-  let rec srec (pt,t) u =
+let is_correct_arity env c pj ind mip params = 
+  let kelim = mip.mind_kelim in
+  let arsign,s = get_arity mip params in
+  let nodep_ar = it_mkProd_or_LetIn (mkSort s) arsign in
+  let rec srec pt t u =
     let pt' = whd_betadeltaiota env pt in
     let t' = whd_betadeltaiota env t in
     match kind_of_term pt', kind_of_term t' with
@@ -245,18 +172,18 @@ let is_correct_arity env kelim (c,pj) indf t =
           let univ =
             try conv env a1 a1'
             with NotConvertible -> raise (Arity None) in
-          srec (a2,a2') (Constraint.union u univ)
+          srec a2 a2' (Constraint.union u univ)
       | Prod (_,a1,a2), _ -> 
           let k = whd_betadeltaiota env a2 in 
           let ksort = match kind_of_term k with
             | Sort s -> family_of_sort s 
 	    | _ -> raise (Arity None) in
-	  let ind = build_dependent_inductive indf in
+	  let dep_ind = build_dependent_inductive ind mip params in
           let univ =
-            try conv env a1 ind
+            try conv env a1 dep_ind
             with NotConvertible -> raise (Arity None) in
           if List.exists ((=) ksort) kelim then
-	    ((true,k), Constraint.union u univ)
+	    (true, Constraint.union u univ)
           else 
 	    raise (Arity (Some(k,t',error_elim_expln env k t')))
       | k, Prod (_,_,_) ->
@@ -266,11 +193,11 @@ let is_correct_arity env kelim (c,pj) indf t =
             | Sort s -> family_of_sort s 
             | _ ->  raise (Arity None) in
           if List.exists ((=) ksort) kelim then 
-	    (false, pt'), u
+	    (false, u)
           else 
 	    raise (Arity (Some(pt',t',error_elim_expln env pt' t')))
   in 
-  try srec (pj.uj_type,t) Constraint.empty
+  try srec pj.uj_type nodep_ar Constraint.empty
   with Arity kinds ->
     let create_sort = function 
       | InProp -> mkProp
@@ -281,33 +208,52 @@ let is_correct_arity env kelim (c,pj) indf t =
       (List.map (fun s -> make_arity env true indf (create_sort s)) kelim)
       @(List.map (fun s -> make_arity env false indf (create_sort s)) kelim)*)
     in 
-    let ind = mis_inductive (fst indf) in
     error_elim_arity env ind listarity c pj kinds
 
 
-let find_case_dep_nparams env (c,pj) (ind,params) =
-  let indf = lookup_mind_instance ind env in
-  let kelim = indf.mis_mip.mind_kelim in
-  let arsign,s = get_arity (indf,params) in
-  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
-  let ((dep,_),univ) =
-    is_correct_arity env kelim (c,pj) (indf,params) glob_t in
-  (dep,univ)
+(***********************************************************************)
+(* Type of case branches *)
 
+(* [p] is the predicate, [i] is the constructor number (starting from 0),
+   and [cty] is the type of the constructor (params not instantiated) *)
+let build_branches_type ind mib mip params dep p =
+  let build_one_branch i cty =
+    let typi = full_constructor_instantiate ((ind,mib,mip),params) cty in
+    let (args,ccl) = decompose_prod_assum typi in
+    let nargs = rel_context_length args in
+    let (_,allargs) = decompose_app ccl in
+    let (lparams,vargs) = list_chop mip.mind_nparams allargs in
+    let cargs =
+      if dep then
+        let cstr = ith_constructor_of_inductive ind (i+1) in
+        let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
+        vargs @ [dep_cstr]
+      else
+        vargs in
+    let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+    it_mkProd_or_LetIn base args in
+  Array.mapi build_one_branch mip.mind_nf_lc
+
+(* [p] is the predicate, [c] is the match object, [realargs] is the
+   list of real args of the inductive type *)
+let build_case_type dep p c realargs =
+  let args = if dep then realargs@[c] else realargs in
+  beta_appvect p (Array.of_list args)
 
-let type_case_branches env (mind,largs) pj c =
-  let mispec = lookup_mind_instance mind env in 
-  let nparams = mispec.mis_mip.mind_nparams in
+let type_case_branches env (ind,largs) pj c =
+  let (mib,mip) = lookup_mind_specif env ind in 
+  let nparams = mip.mind_nparams in
   let (params,realargs) = list_chop nparams largs in
-  let indf = (mispec,params) in
   let p = pj.uj_val in
-  let (dep,univ) = find_case_dep_nparams env (c,pj) (mind,params) in
-  let constructs = get_constructors indf in
-  let lc = Array.map (build_branch_type dep p) constructs in
-  let args = if dep then realargs@[c] else realargs in
-  (lc, beta_appvect p (Array.of_list args), univ)
+  let (dep,univ) = is_correct_arity env c pj ind mip params in
+  let lc = build_branches_type ind mib mip params dep p in
+  let ty = build_case_type dep p c realargs in
+  (lc, ty, univ)
 
 
+(***********************************************************************)
+(* Checking the case annotation is relevent *)
+
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
@@ -363,6 +309,10 @@ type guard_env =
     lst     : (int * (size * recarg list array)) list;
   }
 
+let lookup_recargs env ind =
+  let (mib,mip) = lookup_mind_specif env ind in
+  Array.map (fun mip -> mip.mind_listrec) mib.mind_packets
+
 let make_renv env minds recarg (_,tyi as ind) =
   let mind_recvec = lookup_recargs env ind in 
   let lcx = mind_recvec.(tyi)  in
@@ -423,6 +373,8 @@ let subterm_var p renv =
    correct envs and decreasing args.
 *)
 
+let lookup_subterms env (_,i as ind) =
+  (lookup_recargs env ind).(i)
 
 let imbr_recarg_expand env (sp,i as ind_sp) lrc =
   let recargs = lookup_subterms env ind_sp in
@@ -719,7 +671,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) = 
                   try find_inductive env a 
-                  with Induc -> raise_err i RecursionNotOnInductiveType in
+                  with Not_found -> raise_err i RecursionNotOnInductiveType in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
             else anomaly "check_one_fix: Bad occurrence of recursive call"
@@ -763,10 +715,9 @@ let check_one_cofix env nbfix def deftype =
       | Prod (x,a,b) ->
 	  codomain_is_coind (push_rel (x, None, a) env) b 
       | _ -> 
-	  try
-	    find_coinductive env b
-          with Induc ->
-	    raise (CoFixGuardError (CodomainNotInductiveType b))
+	  (try find_coinductive env b
+           with Not_found ->
+	     raise (CoFixGuardError (CodomainNotInductiveType b)))
   in
   let (mind, _) = codomain_is_coind env deftype in
   let (sp,tyi) = mind in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 720ae3e4a..719205331 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -16,22 +16,20 @@ open Declarations
 open Environ
 (*i*)
 
-exception Induc
-
 (*s Extracting an inductive type from a construction *)
 
 (* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
    [find_rectype], [find_inductive] and [find_coinductive]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
-   They raise [Induc] if not convertible to a recursive type. *)
+   They raise [Not_found] if not convertible to a recursive type. *)
 
 val find_rectype     : env -> types -> inductive * constr list
 val find_inductive   : env -> types -> inductive * constr list
 val find_coinductive : env -> types -> inductive * constr list
 
 (*s Fetching information in the environment about an inductive type.
-    Raises Induc if the inductive type is not found. *)
+    Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif :
   env -> inductive -> mutual_inductive_body * one_inductive_body
 
@@ -66,9 +64,3 @@ val check_case_info : env -> inductive -> case_info -> unit
 (*s Guard conditions for fix and cofix-points. *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
-
-(********************)
-(* TODO: remove (used in pretyping only...) *)
-val find_case_dep_nparams :
-  env -> constr * unsafe_judgment -> inductive * constr list ->
-    bool * constraints
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index ce62acdf8..9d63dc7dd 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -282,7 +282,7 @@ let check_branch_types env cj (lft,explft) =
 let judge_of_case env ci pj cj lfj =
   let indspec =
     try find_rectype env cj.uj_type
-    with Induc -> error_case_not_inductive env cj in
+    with Not_found -> error_case_not_inductive env cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in