Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 123 insertions, 100 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 214e19fe..97aa82e4 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  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
@@ -11,6 +13,7 @@ open Util
 open Names
 open Univ
 open Term
+open Constr
 open Vars
 open Termops
 open Declarations
@@ -24,14 +27,14 @@ open Context.Rel.Declaration
 
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps;
  Inductive.type_of_inductive env (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
  let (mib,_ as specif) =
    Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps;
  Inductive.type_of_constructor (cstr,u) specif
 
 (* Return constructor types in user form *)
@@ -58,21 +61,24 @@ let lift_inductive_family n = liftn_inductive_family n 1
 let substnl_ind_family l n = map_ind_family (substnl l n)
 
 
-type inductive_type = IndType of inductive_family * constr list
+type inductive_type = IndType of inductive_family * EConstr.constr list
 
 let make_ind_type (indf, realargs) = IndType (indf,realargs)
 let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
 
 let map_inductive_type f (IndType (indf, realargs)) =
-  IndType (map_ind_family f indf, List.map f realargs)
+  let f' c = EConstr.Unsafe.to_constr (f (EConstr.of_constr c)) in
+  IndType (map_ind_family f' indf, List.map f realargs)
 
-let liftn_inductive_type n d = map_inductive_type (liftn n d)
+let liftn_inductive_type n d = map_inductive_type (EConstr.Vars.liftn n d)
 let lift_inductive_type n = liftn_inductive_type n 1
 
-let substnl_ind_type l n = map_inductive_type (substnl l n)
+let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n)
 
 let mkAppliedInd (IndType ((ind,params), realargs)) =
-  applist (mkIndU ind,params@realargs)
+  let open EConstr in
+  let ind = on_snd EInstance.make ind in
+  applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs)
 
 (* Does not consider imbricated or mutually recursive types *)
 let mis_is_recursive_subset listind rarg =
@@ -80,7 +86,7 @@ let mis_is_recursive_subset listind rarg =
     List.exists
       (fun ra ->
         match dest_recarg ra with
-	  | Mrec (_,i) -> Int.List.mem i listind
+          | Mrec (_,i) -> Int.List.mem i listind
           | _ -> false) rvec
   in
   Array.exists one_is_rec (dest_subterms rarg)
@@ -94,7 +100,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   and ntypes = mib.mind_ntypes
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
-  if j > nconstr then error "Not enough constructors in the type.";
+  if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
     substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
 
 (* Number of constructors *)
@@ -271,7 +277,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | Some (Some _) -> mib.mind_finite == BiFinite
   | _ -> true
 
 (* Annotation for cases *)
@@ -343,34 +349,35 @@ let get_projections env (ind,params) =
     | Some (Some (id, projs, pbs)) -> Some projs
     | _ -> None
 
-let make_case_or_project env indf ci pred c branches =
+let make_case_or_project env sigma indf ci pred c branches =
+  let open EConstr in
   let projs = get_projections env indf in
   match projs with
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
      assert(Array.length branches == 1);
      let () =
-       let _, _, t = destLambda pred in
+       let _, _, t = destLambda sigma pred in
        let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
-       if (* dependent *) not (noccurn 1 t) &&
+       if (* dependent *) not (Vars.noccurn sigma 1 t) &&
           not (has_dependent_elim mib) then
-       errorlabstrm "make_case_or_project"
-		    Pp.(str"Dependent case analysis not allowed" ++
-		     str" on inductive type " ++ Names.MutInd.print (fst ind))
+       user_err ~hdr:"make_case_or_project"
+                    Pp.(str"Dependent case analysis not allowed" ++
+                     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
-     let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
+     let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
-	  match decl with
-	  | LocalAssum (na, t) ->
-	     let t = mkProj (Projection.make ps.(i) true, c) in
-	     (i + 1, t :: subst)
-	  | LocalDef (na, b, t) -> (i, substl subst b :: subst))
-	 ctx (0, [])
-     in substl subst br
+          match decl with
+          | LocalAssum (na, t) ->
+             let t = mkProj (Projection.make ps.(i) true, c) in
+             (i + 1, t :: subst)
+          | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
+         ctx (0, [])
+     in Vars.substl subst br
 
 (* substitution in a signature *)
 
@@ -393,8 +400,8 @@ let get_arity env ((ind,u),params) =
       mib.mind_params_ctxt
     else begin
       assert (Int.equal nparams mib.mind_nparams_rec);
-      let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in
-      snd (List.chop nnonrecparamdecls mib.mind_params_ctxt)
+      let nnonrecparamdecls = mib.mind_nparams - mib.mind_nparams_rec in
+      snd (Termops.context_chop nnonrecparamdecls mib.mind_params_ctxt)
     end in
   let parsign = Vars.subst_instance_context u parsign in
   let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
@@ -408,51 +415,55 @@ let build_dependent_constructor cs =
   applist
     (mkConstructU cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)
-      @(Context.Rel.to_extended_list 0 cs.cs_args))
+      @(Context.Rel.to_extended_list mkRel 0 cs.cs_args))
 
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let nrealargs = List.length arsign in
   applist
     (mkIndU ind,
-     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
+     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list mkRel 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
-let make_arity_signature env dep indf =
+let make_arity_signature env sigma dep indf =
   let (arsign,_) = get_arity env indf in
+  let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in
   if dep then
     (* We need names everywhere *)
-    Namegen.name_context env
-      ((LocalAssum (Anonymous,build_dependent_inductive env indf))::arsign)
+    Namegen.name_context env sigma
+      ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign)
       (* Costly: would be better to name once for all at definition time *)
   else
     (* No need to enforce names *)
     arsign
 
-let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
+let make_arity env sigma dep indf s =
+  let open EConstr in
+  it_mkProd_or_LetIn (mkSort s) (make_arity_signature env sigma dep indf)
 
 (* [p] is the predicate and [cs] a constructor summary *)
-let build_branch_type env dep p cs =
+let build_branch_type env sigma dep p cs =
   let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
   if dep then
-    Namegen.it_mkProd_or_LetIn_name env
-      (applist (base,[build_dependent_constructor cs]))
-      cs.cs_args
+    EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma
+      (EConstr.of_constr (applist (base,[build_dependent_constructor cs])))
+      (List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) cs.cs_args))
   else
-    it_mkProd_or_LetIn base cs.cs_args
+    Term.it_mkProd_or_LetIn base cs.cs_args
 
 (**************************************************)
 
-let extract_mrectype t =
-  let (t, l) = decompose_app t in
-  match kind_of_term t with
+let extract_mrectype sigma t =
+  let open EConstr in
+  let (t, l) = decompose_app sigma t in
+  match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
 let find_mrectype_vect env sigma c =
-  let (t, l) = decompose_appvect (whd_all env sigma c) in
-  match kind_of_term t with
+  let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in
+  match EConstr.kind sigma t with
     | Ind ind -> (ind, l)
     | _ -> raise Not_found
 
@@ -460,28 +471,35 @@ let find_mrectype env sigma c =
   let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v)
 
 let find_rectype env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
-    | Ind (ind,u as indu) ->
+  let open EConstr in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
+  match EConstr.kind sigma t with
+    | Ind (ind,u) ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
         if mib.mind_nparams > List.length l then raise Not_found;
+        let l = List.map EConstr.Unsafe.to_constr l in
         let (par,rargs) = List.chop mib.mind_nparams l in
-        IndType((indu, par),rargs)
+        let indu = (ind, EInstance.kind sigma u) in
+        IndType((indu, par),List.map EConstr.of_constr rargs)
     | _ -> raise Not_found
 
 let find_inductive env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
+  match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite ->
+        let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env sigma c =
-  let (t, l) = decompose_app (whd_all env sigma c) in
-  match kind_of_term t with
+  let open EConstr in
+  let (t, l) = decompose_app sigma (whd_all env sigma c) in
+  match EConstr.kind sigma t with
     | Ind ind
-        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+        when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite ->
+        let l = List.map EConstr.Unsafe.to_constr l in
         (ind, l)
     | _ -> raise Not_found
 
@@ -490,32 +508,32 @@ 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 arsign =
+let is_predicate_explicitly_dep env sigma pred arsign =
   let rec srec env pval arsign =
-    let pv' = whd_all env Evd.empty pval in
-    match kind_of_term pv', arsign with
+    let pv' = whd_all env sigma pval in
+    match EConstr.kind sigma pv', arsign with
       | Lambda (na,t,b), (LocalAssum _)::arsign ->
-	  srec (push_rel_assum (na,t) env) b arsign
+          srec (push_rel_assum (na, t) env) b arsign
       | Lambda (na,_,t), _ ->
 
        (* The following code has an impact on the introduction names
-	  given by the tactics "case" and "inversion": when the
-	  elimination is not dependent, "case" uses Anonymous for
-	  inductive types in Prop and names created by mkProd_name for
-	  inductive types in Set/Type while "inversion" uses anonymous
-	  for inductive types both in Prop and Set/Type !!
-
-	  Previously, whether names were created or not relied on
-	  whether the predicate created in Indrec.make_case_com had a
-	  dependent arity or not. To avoid different predicates
-	  printed the same in v8, all predicates built in indrec.ml
-	  got a dependent arity (Aug 2004). The new way to decide
-	  whether names have to be created or not is to use an
-	  Anonymous or Named variable to enforce the expected
-	  dependency status (of course, Anonymous implies non
-	  dependent, but not conversely).
-
-          From Coq > 8.2, using or not the the effective dependency of
+          given by the tactics "case" and "inversion": when the
+          elimination is not dependent, "case" uses Anonymous for
+          inductive types in Prop and names created by mkProd_name for
+          inductive types in Set/Type while "inversion" uses anonymous
+          for inductive types both in Prop and Set/Type !!
+
+          Previously, whether names were created or not relied on
+          whether the predicate created in Indrec.make_case_com had a
+          dependent arity or not. To avoid different predicates
+          printed the same in v8, all predicates built in indrec.ml
+          got a dependent arity (Aug 2004). The new way to decide
+          whether names have to be created or not is to use an
+          Anonymous or Named variable to enforce the expected
+          dependency status (of course, Anonymous implies non
+          dependent, but not conversely).
+
+          From Coq > 8.2, using or not the effective dependency of
           the predicate is parametrable! *)
 
           begin match na with
@@ -523,19 +541,20 @@ let is_predicate_explicitly_dep env pred arsign =
           | Name _ -> true
           end
 
-      | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
+      | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.")
   in
-  srec env pred arsign
+  srec env (EConstr.of_constr pred) arsign
 
-let is_elim_predicate_explicitly_dependent env pred indf =
+let is_elim_predicate_explicitly_dependent env sigma pred indf =
   let arsign,_ = get_arity env indf in
-  is_predicate_explicitly_dep env pred arsign
+  is_predicate_explicitly_dep env sigma pred arsign
 
-let set_names env n brty =
-  let (ctxt,cl) = decompose_prod_n_assum n brty in
-  Namegen.it_mkProd_or_LetIn_name env cl ctxt
+let set_names env sigma n brty =
+  let open EConstr in
+  let (ctxt,cl) = decompose_prod_n_assum sigma n brty in
+  EConstr.Unsafe.to_constr (Namegen.it_mkProd_or_LetIn_name env sigma cl ctxt)
 
-let set_pattern_names env ind brv =
+let set_pattern_names env sigma ind brv =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let arities =
     Array.map
@@ -543,10 +562,11 @@ let set_pattern_names env ind brv =
         Context.Rel.length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
-  Array.map2 (set_names env) arities brv
+  Array.map2 (set_names env sigma) arities brv
 
-let type_case_branches_with_names env indspec p c =
+let type_case_branches_with_names env sigma indspec p c =
   let (ind,args) = indspec in
+  let args = List.map EConstr.Unsafe.to_constr args in
   let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
   let nparams = mib.mind_nparams in
   let (params,realargs) = List.chop nparams args in
@@ -554,8 +574,8 @@ let type_case_branches_with_names env indspec p c =
   (* Build case type *)
   let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
-  if is_elim_predicate_explicitly_dependent env p (ind,params) then
-    (set_pattern_names env (fst ind) lbrty, conclty)
+  if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
+    (set_pattern_names env sigma (fst ind) (Array.map EConstr.of_constr lbrty), conclty)
   else (lbrty, conclty)
 
 (* Type of Case predicates *)
@@ -563,7 +583,7 @@ let arity_of_case_predicate env (ind,params) dep k =
   let arsign,_ = get_arity env (ind,params) in
   let mind = build_dependent_inductive env (ind,params) in
   let concl = if dep then mkArrow mind (mkSort k) else mkSort k in
-  it_mkProd_or_LetIn concl arsign
+  Term.it_mkProd_or_LetIn concl arsign
 
 (***********************************************)
 (* Inferring the sort of parameters of a polymorphic inductive type
@@ -582,15 +602,15 @@ let rec instantiate_universes env evdref scl is = function
       let ctx,_ = Reduction.dest_arity env ty in
       let u = Univ.Universe.make l in
       let s =
-	(* Does the sort of parameter [u] appear in (or equal)
+        (* Does the sort of parameter [u] appear in (or equal)
            the sort of inductive [is] ? *)
         if univ_level_mem l is then
           scl (* constrained sort: replace by scl *)
         else
           (* unconstrained sort: replace by fresh universe *)
           let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
-	  let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
-	    evdref := evm; s
+          let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
+            evdref := evm; s
       in
       (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp)
   | sign, [] -> sign (* Uniform parameters are exhausted *)
@@ -598,24 +618,26 @@ let rec instantiate_universes env evdref scl is = function
 
 let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
-  | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
+  | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
-    let _,scl = Reduction.dest_arity env conclty in
+    let _,scl = splay_arity env sigma conclty in
+    let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
       instantiate_universes
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
-      !evdref, mkArity (List.rev ctx,scl)
+      !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_knowing_arg env sigma p c ty =
+  let c = EConstr.Unsafe.to_constr c in
   let IndType(pars,realargs) =
     try find_rectype env sigma ty
     with Not_found ->
       raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
   in
   let (_,u), pars = dest_ind_family pars in
-  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+  substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u))
 
 (***********************************************)
 (* Guard condition *)
@@ -623,8 +645,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 (* A function which checks that a term well typed verifies both
    syntactic conditions *)
 
-let control_only_guard env c =
-  let check_fix_cofix e c = match kind_of_term c with
+let control_only_guard env sigma c =
+  let check_fix_cofix e c =
+    match kind (EConstr.to_constr sigma c) with
     | CoFix (_,(_,_,_) as cofix) ->
       Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
@@ -633,6 +656,6 @@ let control_only_guard env c =
   in
   let rec iter env c =
     check_fix_cofix env c;
-    iter_constr_with_full_binders push_rel iter env c
+    iter_constr_with_full_binders sigma EConstr.push_rel iter env c
   in
   iter env c