Merge PR #889: Removing template polymorphism for definitions.

11 files changed, 30 insertions, 165 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 63614e20f7..80d41847cd 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -18,7 +18,6 @@ open Util
 open Names
 open Term
 open Declarations
-open Environ
 open Univ
 
 module NamedDecl = Context.Named.Declaration
@@ -153,7 +152,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
@@ -167,11 +166,6 @@ let on_body ml hy f = function
     OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f
                  { Opaqueproof.modlist = ml; abstract = hy } o)
 
-let constr_of_def otab = function
-  | Undef _ -> assert false
-  | Def cs -> Mod_subst.force_constr cs
-  | OpaqueDef lc -> Opaqueproof.force_proof otab lc
-
 let expmod_constr_subst cache modlist subst c =
   let c = expmod_constr cache modlist c in
     Vars.subst_univs_level_constr subst c
@@ -220,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } =
       List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
       hyps ~init:cb.const_hyps in
-  let typ = match cb.const_type with
-    | RegularArity t ->
-  	let typ =
-          abstract_constant_type (expmod t) hyps in
-  	RegularArity typ
-    | TemplateArity (ctx,s) ->
-  	let t = mkArity (ctx,Type s.template_level) in
-  	let typ = abstract_constant_type (expmod t) hyps in
-  	let j = make_judge (constr_of_def (opaque_tables env) body) typ in
-  	Typeops.make_polymorphic_if_constant_for_ind env j
-  in
+  let typ = abstract_constant_type (expmod cb.const_type) hyps in
   let projection pb =
     let c' = abstract_constant_body (expmod pb.proj_body) hyps in
     let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in
@@ -244,9 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
 	  | _ -> assert false 
       with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0)
     in 
-    let typ = (* By invariant, a regular arity *)
-      match typ with RegularArity t -> t | TemplateArity _ -> assert false 
-    in
     let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in
       { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg;
 	proj_eta = etab, etat;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index f386fd9362..6d1b776c05 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,7 +18,7 @@ type inline = bool
 
 type result = {
   cook_body : constant_def;
-  cook_type : constant_type;
+  cook_type : types;
   cook_proj : projection_body option;
   cook_universes : constant_universes;
   cook_inline : inline;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f35438dfc4..9697b0b8b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
-type constant_type = (types, Context.Rel.t * template_arity) declaration_arity
-
 (** Inlining level of parameters at functor applications.
     None means no inlining *)
 
@@ -83,7 +81,7 @@ type typing_flags = {
 type constant_body = {
     const_hyps : Context.Named.t; (** New: younger hyp at top *)
     const_body : constant_def;
-    const_type : constant_type;
+    const_type : types;
     const_body_code : Cemitcodes.to_patch_substituted option;
     const_universes : constant_universes;
     const_proj : projection_body option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index efce219826..85dd1e66db 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -69,10 +69,6 @@ let subst_rel_declaration sub =
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
-let subst_template_cst_arity sub (ctx,s as arity) =
-  let ctx' = subst_rel_context sub ctx in
-    if ctx==ctx' then arity else (ctx',s)
-      
 let subst_const_type sub arity =
   if is_empty_subst sub then arity
   else subst_mps sub arity
@@ -94,7 +90,7 @@ let subst_const_body sub cb =
   if is_empty_subst sub then cb
   else
     let body' = subst_const_def sub cb.const_body in
-    let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in
+    let type' = subst_const_type sub cb.const_type in
     let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
     if body' == cb.const_body && type' == cb.const_type
       && proj' == cb.const_proj then cb
@@ -120,14 +116,6 @@ let hcons_rel_decl =
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
-let hcons_regular_const_arity t = Term.hcons_constr t
-
-let hcons_template_const_arity (ctx, ar) = 
-  (hcons_rel_context ctx, hcons_template_arity ar)
-
-let hcons_const_type = 
-  map_decl_arity hcons_regular_const_arity hcons_template_const_arity
-
 let hcons_const_def = function
   | Undef inl -> Undef inl
   | Def l_constr ->
@@ -145,7 +133,7 @@ let hcons_const_universes cbu =
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
-    const_type = hcons_const_type cb.const_type;
+    const_type = Term.hcons_constr cb.const_type;
     const_universes = hcons_const_universes cb.const_universes }
 
 (** {6 Inductive types } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b01b652001..d2c737ab0c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,12 +232,6 @@ let constraints_of cb u =
   | Monomorphic_const _ -> Univ.Constraint.empty
   | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
 
-let map_regular_arity f = function
-  | RegularArity a as ar -> 
-    let a' = f a in 
-      if a' == a then ar else RegularArity a'
-  | TemplateArity _ -> assert false
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
@@ -245,7 +239,7 @@ let constant_type env (kn,u) =
   | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
   | Polymorphic_const ctx -> 
     let csts = constraints_of cb u in
-    (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+    (subst_instance_constr u cb.const_type, csts)
 
 let constant_context env kn =
   let cb = lookup_constant kn env in
@@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) =
 	| OpaqueDef _ -> None
 	| Undef _ -> None
       in
-	b', map_regular_arity (subst_instance_constr u) cb.const_type, cst
+	b', subst_instance_constr u cb.const_type, cst
     else 
       let b' = match cb.const_body with
 	| Def l_body -> Some (Mod_subst.force_constr l_body)
@@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) =
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
     if Declareops.constant_is_polymorphic cb then
-      map_regular_arity (subst_instance_constr u) cb.const_type
+      subst_instance_constr u cb.const_type
     else cb.const_type
 
 let constant_value_in env (kn,u) =
@@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env =
 let type_in_type_constant cst env =
   not (lookup_constant cst env).const_typing_flags.check_universes
 
-let template_polymorphic_constant cst env =
-  match (lookup_constant cst env).const_type with 
-  | TemplateArity _ -> true
-  | RegularArity _ -> false
-
-let template_polymorphic_pconstant (cst,u) env =
-  if not (Univ.Instance.is_empty u) then false
-  else template_polymorphic_constant cst env
-
 let lookup_projection cst env =
   match (lookup_constant (Projection.constant cst) env).const_proj with 
   | Some pb -> pb
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cd7a9d2791..377c61de2c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -139,10 +139,6 @@ val polymorphic_constant  : constant -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
 val type_in_type_constant : constant -> env -> bool
 
-(** Old-style polymorphism *)
-val template_polymorphic_constant  : constant -> env -> bool
-val template_polymorphic_pconstant : pconstant -> env -> bool
-
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
@@ -153,11 +149,11 @@ type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> constant_type constrained
+val constant_type : env -> constant puniverses -> types constrained
 
 val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
 val constant_value_and_type : env -> constant puniverses -> 
-  constr option * constant_type * Univ.constraints
+  constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
 val constant_context : env -> constant -> Univ.abstract_universe_context
@@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_universe_context
    already contains the constraints corresponding to the constant 
    application. *)
 val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> constant_type
+val constant_type_in : env -> constant puniverses -> types
 val constant_opt_value_in : env -> constant puniverses -> constr option
 
 (** {6 Primitive projections} *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index c7f3e5c51b..0888ccc109 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -83,7 +83,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let c',cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      j.uj_val, cst'
@@ -103,7 +103,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	  let cst = match cb.const_body with
 	    | Undef _ | OpaqueDef _ ->
 	      let j = Typeops.infer env' c in
-	      let typ = Typeops.type_of_constant_type env' cb.const_type in
+	      let typ = cb.const_type in
 	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 						j.uj_type typ in
 	      cst'
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bd82dd465b..b311165f10 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -313,8 +313,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
           error (PolymorphicStatusExpected false)
       in
       (* Now check types *)
-      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let typ1 = cb1.const_type in
+      let typ2 = cb2.const_type in
       let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
 	 - A transparent constant can only be implemented by a compatible
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 43c099712a..3f42c348fc 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -21,7 +21,6 @@ open Environ
 open Entries
 open Typeops
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
@@ -128,7 +127,7 @@ let inline_side_effects env body ctx side_eff =
       match cb.const_universes with
       | Monomorphic_const cnstctx ->
         (** Abstract over the term at the top of the proof *)
-        let ty = Typeops.type_of_constant_type env cb.const_type in
+        let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
         let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
@@ -249,7 +248,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
       {
         Cooking.cook_body = Undef nl;
-        cook_type = RegularArity t;
+        cook_type = t;
         cook_proj = None;
         cook_universes = univs;
         cook_inline = false;
@@ -290,7 +289,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       {
         Cooking.cook_body = def;
-        cook_type = RegularArity typ;
+        cook_type = typ;
         cook_proj = None;
         cook_universes = Monomorphic_const univs;
         cook_inline = c.const_entry_inline_code;
@@ -320,13 +319,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not poly then (* Old-style polymorphism *)
-             make_polymorphic_if_constant_for_ind env j
-           else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
+          Vars.subst_univs_level_constr usubst j.uj_type
         | Some t ->
            let tj = infer_type env t in
            let _ = judge_of_cast env j DEFAULTcast tj in
-           RegularArity (Vars.subst_univs_level_constr usubst t)
+           Vars.subst_univs_level_constr usubst t
       in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
@@ -363,21 +360,13 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
     let term, typ = pb.proj_eta in
     {
       Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term));
-      cook_type = RegularArity typ;
+      cook_type = typ;
       cook_proj = Some pb;
       cook_universes = univs;
       cook_inline = false;
       cook_context = None;
     }
 
-let global_vars_set_constant_type env = function
-  | RegularArity t -> global_vars_set env t
-  | TemplateArity (ctx,_) ->
-      Context.Rel.fold_outside
-        (RelDecl.fold_constr
-	  (fun t c -> Id.Set.union (global_vars_set env t) c))
-      ctx ~init:Id.Set.empty
-
 let record_aux env s_ty s_bo suggested_expr =
   let in_ty = keep_hyps env s_ty in
   let v =
@@ -426,7 +415,7 @@ let build_constant_declaration kn env result =
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
            we must look at the body NOW, if any *)
-        let ids_typ = global_vars_set_constant_type env typ in
+        let ids_typ = global_vars_set env typ in
         let ids_def = match def with
         | Undef _ -> Idset.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
@@ -454,14 +443,14 @@ let build_constant_declaration kn env result =
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
-            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
             let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
-              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
@@ -524,8 +513,7 @@ let constant_entry_of_side_effect cb u =
     const_entry_body = Future.from_val (pt, ());
     const_entry_secctx = None;
     const_entry_feedback = None;
-    const_entry_type =
-      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_type = Some cb.const_type;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -625,7 +613,7 @@ let translate_recipe env kn r =
 let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
-  let typ = type_of_constant_type env decl.cook_type in
+  let typ = decl.cook_type in
   if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
     match decl.cook_body with
     | Undef _ -> ()
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index b814deb6eb..044877e82a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign =
 (* Type of constants *)
 
 
-let type_of_constant_type_knowing_parameters env t paramtyps =
-  match t with
-  | RegularArity t -> t
-  | TemplateArity (sign,ar) ->
-      let ctx = List.rev sign in
-      let ctx,s = instantiate_universes env ctx ar paramtyps in
-      mkArity (List.rev ctx,s)
-
-let type_of_constant_knowing_parameters env (kn,u as cst) args =
+let type_of_constant env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   let ty, cu = constant_type env cst in
-  let ty = type_of_constant_type_knowing_parameters env ty args in
   let () = check_constraints cu env in
     ty
 
-let type_of_constant_knowing_parameters_in env (kn,u as cst) args =
+let type_of_constant_in env (kn,u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
-  let ty = constant_type_in env cst in
-  type_of_constant_type_knowing_parameters env ty args
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
-  type_of_constant_knowing_parameters_in env cst [||]
-
-let type_of_constant_type env t =
-  type_of_constant_type_knowing_parameters env t [||]
+  constant_type_in env cst
 
 (* Type of a lambda-abstraction. *)
 
@@ -369,9 +350,6 @@ let rec execute env cstr =
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
 	    let args = Array.map (fun t -> lazy t) argst in
               type_of_inductive_knowing_parameters env ind args
-	  | Const cst when Environ.template_polymorphic_pconstant cst env ->
-	    let args = Array.map (fun t -> lazy t) argst in
-              type_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* No template polymorphism *)
             execute env f
@@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k)
 let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x)
 
 let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst)
-let judge_of_constant_knowing_parameters env cst args =
-  make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args)
 
 let judge_of_projection env p cj =
   make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type)
@@ -559,34 +535,3 @@ let type_of_projection_constant env (p,u) =
       Vars.subst_instance_constr u pb.proj_type
     else pb.proj_type
   | None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-(* Instantiation of terms on real arguments. *)
-
-(* Make a type polymorphic if an arity *)
-
-let extract_level env p =
-  let _,c = dest_prod_assum env p in
-  match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None
-
-let extract_context_levels env l =
-  let fold l = function
-    | RelDecl.LocalAssum (_,p) -> extract_level env p :: l
-    | RelDecl.LocalDef _ -> l
-  in
-  List.fold_left fold [] l
-
-let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
-  let params, ccl = dest_prod_assum env t in
-  match kind_of_term ccl with
-  | Sort (Type u) ->
-     let ind, l = decompose_app (whd_all env c) in
-     if isInd ind && List.is_empty l then
-       let mis = lookup_mind_specif env (fst (destInd ind)) in
-       let nparams = Inductive.inductive_params mis in
-       let paramsl = CList.lastn nparams params in
-       let param_ccls = extract_context_levels env paramsl in
-       let s = { template_param_levels = param_ccls; template_level = u} in
-       TemplateArity (params,s)
-     else RegularArity t
-  | _ ->
-      RegularArity t
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 24521070e2..a8f7fba9a0 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -11,7 +11,6 @@ open Univ
 open Term
 open Environ
 open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
 
@@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 
 val judge_of_constant : env -> pconstant -> unsafe_judgment
 
-val judge_of_constant_knowing_parameters :
-  env -> pconstant -> types Lazy.t array -> unsafe_judgment
-
 (** {6 type of an applied projection } *)
 
 val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
@@ -98,21 +94,9 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_constant_type : env -> constant_type -> types
-
 val type_of_projection_constant : env -> Names.projection puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types
 
-val type_of_constant_type_knowing_parameters :
-  env -> constant_type -> types Lazy.t array -> types
-
-val type_of_constant_knowing_parameters_in :
-  env -> pconstant -> types Lazy.t array -> types
-
-(** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
-  constant_type
-
 (** Check that hyps are included in env and fails with error otherwise *)
 val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit