1 files changed, 91 insertions, 78 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 3c4c2796..9bed598b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1,16 +1,18 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open CErrors
 open Util
 open Names
 open Univ
-open Term
+open Constr
 open Vars
 open Declarations
 open Declareops
@@ -25,27 +27,27 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 let lookup_mind_specif env (kn,tyi) =
   let mib = Environ.lookup_mind kn env in
   if tyi >= Array.length mib.mind_packets then
-    error "Inductive.lookup_mind_specif: invalid inductive index";
+    user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index");
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
   let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  match kind t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 let find_inductive env c =
   let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
   let (t, l) = decompose_app (whd_all env c) in
-  match kind_of_term t with
+  match kind t with
     | Ind ind
-        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+        when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let inductive_params (mib,_) = mib.mind_nparams
@@ -54,9 +56,11 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  if mib.mind_polymorphic then
-    Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes)
-  else Univ.Constraint.empty
+  let process auctx =  Univ.AUContext.instantiate u auctx in
+  match mib.mind_universes with
+  | Monomorphic_ind _ -> Univ.Constraint.empty
+  | Polymorphic_ind auctx -> process auctx
+  | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
 
 
 (************************************************************************)
@@ -75,11 +79,11 @@ let constructor_instantiate mind u mib c =
 
 let instantiate_params full t u args sign =
   let fail () =
-    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
+    anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
   let (rem_args, subs, ty) =
     Context.Rel.fold_outside
       (fun decl (largs,subs,ty) ->
-        match (decl, largs, kind_of_term ty) with
+        match (decl, largs, kind ty) with
           | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
           | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
 	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
@@ -92,9 +96,9 @@ let instantiate_params full t u args sign =
   substl subs ty
 
 let full_inductive_instantiate mib u params sign =
-  let dummy = prop_sort in
-  let t = mkArity (Vars.subst_instance_context u sign,dummy) in
-    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+  let dummy = Sorts.prop in
+  let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in
+    fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
   let inst_ind = constructor_instantiate mind u mib t in
@@ -126,7 +130,7 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let sort_as_univ = function
+let sort_as_univ = let open Sorts in function
 | Type u -> u
 | Prop Null -> Universe.type0m
 | Prop Pos -> Universe.type0
@@ -190,11 +194,11 @@ let instantiate_universes env ctx ar argsorts =
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-    if is_type0m_univ level then prop_sort
+    if is_type0m_univ level then Sorts.prop
     (* Non singleton type not containing types are interpretable in Set *)
-    else if is_type0_univ level then set_sort
+    else if is_type0_univ level then Sorts.set
     (* This is a Type with constraints *)
-    else Type level
+    else Sorts.Type level
   in
     (ctx, ty)
 
@@ -209,9 +213,9 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+      if not polyprop && not (is_type0m_univ ar.template_level) && Sorts.is_prop s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s)
+      Term.mkArity (List.rev ctx,s)
 
 let type_of_inductive env pind = 
   type_of_inductive_gen env pind [||]
@@ -231,7 +235,7 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
 
 (* The max of an array of universes *)
 
-let cumulate_constructor_univ u = function
+let cumulate_constructor_univ u = let open Sorts in function
   | Prop Null -> u
   | Prop Pos -> Universe.sup Universe.type0 u
   | Type u' -> Universe.sup u u'
@@ -247,7 +251,7 @@ let type_of_constructor (cstr, u) (mib,mip) =
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
-  if i > nconstr then error "Not enough constructors in the type.";
+  if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
   constructor_instantiate (fst ind) u mib specif.(i-1)
 
 let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
@@ -274,8 +278,8 @@ let type_of_constructors (ind,u) (mib,mip) =
 
 let inductive_sort_family mip =
   match mip.mind_arity with
-  | RegularArity s -> family_of_sort s.mind_sort
-  | TemplateArity _ -> InType
+  | RegularArity s -> Sorts.family s.mind_sort
+  | TemplateArity _ -> Sorts.InType
 
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
@@ -294,19 +298,20 @@ let is_primitive_record (mib,_) =
 
 let build_dependent_inductive ind (_,mip) params =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
-  applist
+  Term.applist
     (mkIndU ind,
        List.map (lift mip.mind_nrealdecls) params
-       @ Context.Rel.to_extended_list 0 realargs)
+       @ Context.Rel.to_extended_list mkRel 0 realargs)
 
 (* This exception is local *)
-exception LocalArity of (sorts_family * sorts_family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * arity_error) option
 
 let check_allowed_sort ksort specif =
+  let open Sorts in
   let eq_ksort s = match ksort, s with
   | InProp, InProp | InSet, InSet | InType, InType -> true
   | _ -> false in
-  if not (List.exists eq_ksort (elim_sorts specif)) then
+  if not (CList.exists eq_ksort (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
     raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
@@ -314,7 +319,7 @@ let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
     let pt' = whd_all env pt in
-    match kind_of_term pt', ar with
+    match kind pt', ar with
       | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
           let () =
             try conv env a1 a1'
@@ -323,8 +328,8 @@ let is_correct_arity env c pj ind specif params =
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (LocalAssum (na1,a1)) env in
-	 let ksort = match kind_of_term (whd_all env' a2) with
-	 | Sort s -> family_of_sort s
+	 let ksort = match kind (whd_all env' a2) with
+	 | Sort s -> Sorts.family s
 	 | _ -> raise (LocalArity None) in
 	 let dep_ind = build_dependent_inductive ind specif params in
 	 let _ =
@@ -349,22 +354,22 @@ let is_correct_arity env c pj ind specif params =
 let build_branches_type (ind,u) (_,mip as specif) params p =
   let build_one_branch i cty =
     let typi = full_constructor_instantiate (ind,u,specif,params) cty in
-    let (cstrsign,ccl) = decompose_prod_assum typi in
+    let (cstrsign,ccl) = Term.decompose_prod_assum typi in
     let nargs = Context.Rel.length cstrsign in
     let (_,allargs) = decompose_app ccl in
     let (lparams,vargs) = List.chop (inductive_params specif) allargs in
     let cargs =
       let cstr = ith_constructor_of_inductive ind (i+1) in
-      let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in
+      let dep_cstr = Term.applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in
       vargs @ [dep_cstr] in
-    let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
-    it_mkProd_or_LetIn base cstrsign in
+    let base = Term.lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
+    Term.it_mkProd_or_LetIn base cstrsign 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 env n p c realargs =
-  whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
+  whd_betaiota env (Term.lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
 
 let type_case_branches env (pind,largs) pj c =
   let specif = lookup_mind_specif env (fst pind) in
@@ -587,7 +592,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
 let rec ienv_decompose_prod (env,_ as ienv) n c =
  if Int.equal n 0 then (ienv,c) else
    let c' = whd_all env c in
-   match kind_of_term c' with
+   match kind c' with
    Prod(na,a,b) ->
      let ienv' = ienv_push_var ienv (na,a,mk_norec) in
      ienv_decompose_prod ienv' (n-1) b
@@ -619,7 +624,7 @@ compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
   let rec build_recargs (env, ra_env as ienv) tree c =
     let x,largs = decompose_app (whd_all env c) in
-    match kind_of_term x with
+    match kind x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
        build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d
@@ -678,7 +683,7 @@ let get_recargs_approx env tree ind args =
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
       let x,largs = decompose_app (whd_all env c) in
-	match kind_of_term x with
+	match kind x with
 
           | Prod (na,b,d) ->
 	     let () = assert (List.is_empty largs) in
@@ -707,7 +712,7 @@ let restrict_spec env spec p =
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
   let i,args = decompose_app (whd_all env s) in
-  match kind_of_term i with
+  match kind i with
   | Ind i ->
      begin match spec with
 	   | Dead_code -> spec
@@ -728,7 +733,7 @@ let restrict_spec env spec p =
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
   let f,l = decompose_app (whd_all renv.env t) in
-    match kind_of_term f with
+    match kind f with
     | Rel k -> subterm_var k renv
     | Case (ci,p,c,lbr) ->
        let stack' = push_stack_closures renv l stack in
@@ -771,7 +776,7 @@ let rec subterm_specif renv stack t =
 	let decrArg = recindxs.(i) in
 	let theBody = bodies.(i)   in
 	let nbOfAbst = decrArg+1 in
-	let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+	let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in
 		   (* pushing the fix parameters *)
 	let stack' = push_stack_closures renv l stack in
 	let renv'' = push_ctxt_renv renv' sign in
@@ -793,21 +798,24 @@ let rec subterm_specif renv stack t =
 
     | Proj (p, c) -> 
       let subt = subterm_specif renv stack c in
-	(match subt with
-	| Subterm (s, wf) ->
-	   (* We take the subterm specs of the constructor of the record *)
-	   let wf_args = (dest_subterms wf).(0) in
-	   (* We extract the tree of the projected argument *)
-	   let kn = Projection.constant p in
-	   let cb = lookup_constant kn renv.env in
-	   let pb = Option.get cb.const_proj in
-	   let n = pb.proj_arg in
-	   Subterm (Strict, List.nth wf_args n)
-	| Dead_code -> Dead_code
-	| Not_subterm -> Not_subterm)
+      (match subt with
+       | Subterm (s, wf) ->
+         (* We take the subterm specs of the constructor of the record *)
+         let wf_args = (dest_subterms wf).(0) in
+         (* We extract the tree of the projected argument *)
+         let kn = Projection.constant p in
+         let cb = lookup_constant kn renv.env in
+         let pb = Option.get cb.const_proj in
+         let n = pb.proj_arg in
+         spec_of_tree (List.nth wf_args n)
+       | Dead_code -> Dead_code
+       | Not_subterm -> Not_subterm)
+
+    | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+      | Construct _ | CoFix _ -> Not_subterm
+
 
       (* Other terms are not subterms *)
-    | _ -> Not_subterm
 
 and lazy_subterm_specif renv stack t =
   lazy (subterm_specif renv stack t)
@@ -855,11 +863,13 @@ let filter_stack_domain env ci p stack =
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
     let t = whd_all env ar in
-    match stack, kind_of_term t with
+    match stack, kind t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
+      let ctx, a = dest_prod_assum env a in
+      let env = push_rel_context ctx env in
       let ty, args = decompose_app (whd_all env a) in
-      let elt = match kind_of_term ty with
+      let elt = match kind ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
         (match (Lazy.force spec') with
@@ -890,7 +900,7 @@ let check_one_fix renv recpos trees def =
     if noccur_with_meta renv.rel_min nfi t then ()
     else
       let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
-      match kind_of_term f with
+      match kind f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p && p < renv.rel_min+nfi then
@@ -920,7 +930,7 @@ let check_one_fix renv recpos trees def =
                 | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
-                      check_rec_call renv stack (applist(lift p c,l))
+                      check_rec_call renv stack (Term.applist(lift p c,l))
               end
 		
         | Case (ci,p,c_0,lrest) ->
@@ -966,7 +976,7 @@ let check_one_fix renv recpos trees def =
             if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-		let value = (applist(constant_value_in renv.env cu, l)) in
+		let value = (Term.applist(constant_value_in renv.env cu, l)) in
 	        check_rec_call renv stack value
 	    else List.iter (check_rec_call renv []) l
 
@@ -1003,7 +1013,7 @@ let check_one_fix renv recpos trees def =
               | LocalDef (_,c,_) ->
                   try List.iter (check_rec_call renv []) l
                   with (FixGuardError _) -> 
-		    check_rec_call renv stack (applist(c,l))
+		    check_rec_call renv stack (Term.applist(c,l))
             end
 
 	| Sort _ ->
@@ -1018,12 +1028,12 @@ let check_one_fix renv recpos trees def =
     if Int.equal decr 0 then
       check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
     else
-      match kind_of_term body with
+      match kind body with
 	| Lambda (x,a,b) ->
 	    check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
 	      check_nested_fix_body renv' (decr-1) recArgsDecrArg b
-	| _ -> anomaly (Pp.str "Not enough abstractions in fix body")
+	| _ -> anomaly (Pp.str "Not enough abstractions in fix body.")
 	    
   in
   check_rec_call renv [] def
@@ -1039,7 +1049,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     || not (Int.equal (Array.length names) nbfix)
     || bodynum < 0
     || bodynum >= nbfix
-  then anomaly (Pp.str "Ill-formed fix term");
+  then anomaly (Pp.str "Ill-formed fix term.");
   let fixenv = push_rec_types recdef env in
   let vdefj = judgment_of_fixpoint recdef in
   let raise_err env i err =
@@ -1049,7 +1059,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def =
-      match kind_of_term (whd_all env def) with
+      match kind (whd_all env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (LocalAssum (x,a)) env in
@@ -1059,9 +1069,12 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                   try find_inductive env a
                   with Not_found ->
 		    raise_err env i (RecursionNotOnInductiveType a) in
+                let mib,_ = lookup_mind_specif env (out_punivs mind) in
+                if mib.mind_finite != Finite then
+                  raise_err env i (RecursionNotOnInductiveType a);
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
-            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
+            else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
@@ -1090,8 +1103,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
     ()
 
 (*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
 *)
 
 (************************************************************************)
@@ -1100,11 +1113,11 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 exception CoFixGuardError of env * guard_error
 
 let anomaly_ill_typed () =
-  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
+  anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.")
 
 let rec codomain_is_coind env c =
   let b = whd_all env c in
-  match kind_of_term b with
+  match kind b with
     | Prod (x,a,b) ->
 	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
@@ -1116,7 +1129,7 @@ let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
       let c,args = decompose_app (whd_all env t) in
-      match kind_of_term c with
+      match kind c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive
                call allowed *)
@@ -1188,8 +1201,8 @@ let check_one_cofix env nbfix def deftype =
 	| Meta _ -> ()
         | Evar _ ->
 	    List.iter (check_rec_call env alreadygrd n tree vlra) args
-
-	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+        | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
+          | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in