Change the way primitive projections are declared to the kernel.

Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.

11 files changed, 104 insertions, 94 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6dacb7818..fcbe939a9 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -866,22 +866,19 @@ let rec get_parameters depth n argstk =
 let eta_expand_ind_stacks env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (exp,projs) when Array.length projs > 0 
+    | Some (projs,pbs) when Array.length projs > 0 
       && mib.Declarations.mind_finite -> 
-      let primitive = Environ.is_projection projs.(0) env in
-	if primitive then
-	  (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	     arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-	  let pars = mib.Declarations.mind_nparams in
-	  let right = fapp_stack (f, s') in
-	  let (depth, args, s) = strip_update_shift_app m s in
-	  (** Try to drop the params, might fail on partially applied constructors. *)
-	  let argss = try_drop_parameters depth pars args in
-	  let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					     term = FProj (p, right) }) projs in
-	    argss, [Zapp hstack]
-	else raise Not_found (* disallow eta-exp for non-primitive records *)
-    | _ -> raise Not_found
+	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+      let pars = mib.Declarations.mind_nparams in
+      let right = fapp_stack (f, s') in
+      let (depth, args, s) = strip_update_shift_app m s in
+      (** Try to drop the params, might fail on partially applied constructors. *)
+      let argss = try_drop_parameters depth pars args in
+      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+					 term = FProj (p, right) }) projs in
+	argss, [Zapp hstack]	
+    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3dd782342..2d316fc1d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -215,6 +215,8 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
   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
+    let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in
     let ((mind, _), _), n' =
       try 
 	let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in
@@ -229,6 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
     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;
 	proj_type = ty'; proj_body = c' }
   in
   let univs = UContext.union abs_ctx univs in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index f76f401b4..2c516cafd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -53,7 +53,8 @@ type projection_body = {
   proj_npars : int;
   proj_arg : int;
   proj_type : types; (* Type under params *)
-  proj_body : constr; (* For compatibility, the match version *)
+  proj_eta : constr * types; (* Eta-expanded term and type *)
+  proj_body : constr; (* For compatibility with VMs only, the match version *)
 }
 
 type constant_def =
@@ -152,9 +153,10 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : (constr * constant array) option;  
+    mind_record : (constant array * projection_body array) option;  
     (** Whether the inductive type has been declared as a record, 
-	In that case we get its canonical eta-expansion and list of projections. *)
+	In the case it is primitive we get its projection names and checked
+	projection bodies, otherwise both arrays are empty. *)
 
     mind_finite : bool;  (** Whether the type is inductive or coinductive *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f583bff64..5b937207f 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -237,11 +237,11 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
-let subst_mind_record sub (c, ps as r) =
-  let c' = subst_mps sub c in
+let subst_mind_record sub (ps, pb as r) =
   let ps' = Array.smartmap (subst_constant sub) ps in
-    if c' == c && ps' == ps then r
-    else (c', ps')
+  let pb' = Array.smartmap (subst_const_proj sub) pb in
+    if ps' == ps && pb' == pb then r
+    else (ps', pb')
 
 let subst_mind_body sub mib =
   { mind_record = Option.smartmap (subst_mind_record sub) mib.mind_record ;
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 244637acd..5fa0527ef 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -63,7 +63,7 @@ type definition_entry = {
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
   const_entry_universes   : Univ.universe_context;
-  const_entry_proj        : bool;
+  const_entry_proj        : (mutual_inductive * int) option;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 18ebc2aa0..715bdb5da 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -661,24 +661,50 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_expansion ((kn, _ as ind), u) params ctx =
+let compute_projections ((kn, _ as ind), u as indsp) nparamargs params
+    mind_consnrealdecls mind_consnrealargs ctx =
   let mp, dp, l = repr_mind kn in
-  let make_proj id = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
-  let projections acc (na, b, t) =
+  let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+  let ci = 
+    let print_info = { ind_nargs = 0; style = LetStyle } in
+      { ci_ind     = ind;
+	ci_npar    = nparamargs;
+	ci_cstr_ndecls = mind_consnrealdecls;
+	ci_cstr_nargs = mind_consnrealargs;
+	ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let x = Name (id_of_string "r") in
+  let compat_body ccl i = 
+    (* [ccl] is defined in context [params;x:rp] *)
+    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 rp, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+  in
+  let projections (na, b, t) (i, j, kns, pbs, subst) =
     match b with
-    | Some c -> acc
-    | None -> 
+    | Some c -> (i, j+1, kns, pbs, c :: subst)
+    | None ->
       match na with
-      | Name id -> make_proj id :: acc
+      | Name id ->
+	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+	let ty = substl subst (liftn 1 j t) in
+	let term = mkProj (kn, mkRel 1) in
+	let compat = compat_body ty i in
+	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
+	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+	let body = { proj_ind = fst ind; proj_npars = nparamargs;
+		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
+		     proj_body = compat } in
+	  (i + 1, j + 1, kn :: kns, body :: pbs, term :: subst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let projs = List.fold_left projections [] ctx in
-  let projarr = Array.of_list projs in
-  let exp = 
-    mkApp (mkConstructU ((ind, 1),u),
-	   Array.append (rel_appvect 1 params)
- 	     (Array.map (fun p -> mkProj (p, mkRel 1)) projarr))
-   in exp, projarr
+  let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+    Array.of_list (List.rev kns),
+    Array.of_list (List.rev pbs)
 
 let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
@@ -750,18 +776,21 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
+  let pkt = packets.(0) in	  
   let isrecord = 
     match isrecord with
-    | Some true -> (* || (Array.length pkt.mind_consnames = 1 &&  *)
-      let pkt = packets.(0) in	  
+    | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
+      (** The elimination criterion ensures that all projections can be defined. *)
       let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
       let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in
 	(try 
-	 let exp = compute_expansion ((kn, 0), u) params 
-	   (List.firstn pkt.mind_consnrealdecls.(0) rctx) 
-	 in Some exp
-	 with UndefinableExpansion -> (Some (mkProp, [||])))
-    | Some false -> Some (mkProp, [||])
+	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+	   let kns, projs = 
+	     compute_projections ((kn, 0), u) nparamargs params
+	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+	   in Some (kns, projs)
+	 with UndefinableExpansion -> Some ([||], [||]))
+    | Some _ -> Some ([||], [||])
     | None -> None
   in
     (* Build the mutual inductive *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8730a3045..85e6a6327 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -41,5 +41,6 @@ val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutua
 val enforce_indices_matter : unit -> unit
 val is_indices_matter : unit -> bool
 
-val compute_expansion : pinductive -> 
-  Context.rel_context -> Context.rel_context -> (constr * constant array)
+val compute_projections : pinductive -> int -> Context.rel_context -> int array -> int array -> 
+  Context.rel_context -> 
+  (constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6ddddeb05..189c2f4d2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -294,6 +294,12 @@ let get_instantiated_arity (ind,u) (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
+let is_private (mib,_) = mib.mind_private = Some true
+let is_primitive_record (mib,_) = 
+  match mib.mind_record with
+  | Some (projs, _) when Array.length projs > 0 -> true
+  | _ -> false
+
 let extended_rel_list n hyps =
   let rec reln l p = function
     | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
@@ -391,12 +397,13 @@ let type_case_branches env (pind,largs) pj c =
 (* Checking the case annotation is relevent *)
 
 let check_case_info env (indsp,u) ci =
-  let (mib,mip) = lookup_mind_specif env indsp in
+  let (mib,mip as spec) = lookup_mind_specif env indsp in
   if
     not (eq_ind indsp ci.ci_ind) ||
     not (Int.equal mib.mind_nparams ci.ci_npar) ||
     not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
-    not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs)
+    not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) ||
+    is_primitive_record spec
   then raise (TypeError(env,WrongCaseInfo((indsp,u),ci)))
 
 (************************************************************************)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index bac242f82..55236700d 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -53,6 +53,9 @@ val type_of_inductive_knowing_parameters :
 
 val elim_sorts : mind_specif -> sorts_family list
 
+val is_private : mind_specif -> bool
+val is_primitive_record : mind_specif -> bool
+
 (** Return type as quoted by the user *)
 
 val constrained_type_of_constructor : pconstructor -> mind_specif -> types constrained
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 843d8f8a3..b603610ce 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -107,39 +107,6 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
-let check_projection env kn usubst body =
-  let cannot_recognize () = error ("Cannot recognize a projection") in
-  let ctx, m = decompose_lam_assum body in
-  let () = if not (isCase m) then cannot_recognize () in
-  let ci, p, c, b = destCase m in
-  let (mib, oib as _specif) = Inductive.lookup_mind_specif env ci.ci_ind in
-  let recinfo = match mib.mind_record with
-    | None -> 
-      error ("Trying to declare a primitive projection for a non-record inductive type")
-    | Some (_, r) -> r
-  in
-  let n = mib.mind_nparams in
-  let () = 
-    if n + 1 != List.length ctx ||
-      not (isRel c) || destRel c != 1 || Array.length b != 1 ||
-      not (isLambda p)
-    then cannot_recognize ()
-  in
-  let (na, t, ty) = destLambda (Vars.subst1 mkProp p) in 
-  let argctx, p = decompose_lam_assum b.(0) in
-  (* No need to check the lambdas as the case is well-formed *)
-  let () = if not (isRel p) then cannot_recognize () in
-  let var = destRel p in
-  let () = if not (var <= Array.length recinfo) then cannot_recognize () in
-  let arg = Array.length recinfo - var in
-  let () = if not (eq_con_chk recinfo.(arg) kn) then cannot_recognize () in
-  let pb = { proj_ind = fst ci.ci_ind;
-	     proj_npars = n;
-	     proj_arg = arg;
-	     proj_type = Vars.subst_univs_level_constr usubst ty;
-	     proj_body = Vars.subst_univs_level_constr usubst body }
-  in pb
   
 let subst_instance_j s j =
   { uj_val = Vars.subst_univs_level_constr s j.uj_val;
@@ -186,19 +153,21 @@ let infer_declaration env kn dcl =
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
       let def, typ, proj = 
-	if c.const_entry_proj then
-	  (** This should be the projection defined as a match. *)
-	  let j = infer env body in
-	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
-	  (** We check it does indeed have the shape of a projection. *)
-	  let pb = check_projection env (Option.get kn) usubst body in
-	  (** We build the eta-expanded form. *)
-	  let context, m = decompose_lam_n_assum (pb.proj_npars + 1) body in 
-	  let body' = mkProj (Option.get kn, mkRel 1) in
-	  let body = it_mkLambda_or_LetIn body' context in
-	    Def (Mod_subst.from_val (hcons_constr (Vars.subst_univs_level_constr usubst body))),
-	    typ, Some pb
-	else
+	match c.const_entry_proj with
+	| Some (ind, i) -> (* Bind c to a checked primitive projection *)
+	  let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
+	  let kn, pb = 
+	    match mib.mind_record with
+	    | Some (kns, pbs) -> 
+	      if i < Array.length pbs then
+		kns.(i), pbs.(i)
+	      else assert false
+	    | None -> assert false
+	  in
+	  let term = Vars.subst_univs_level_constr usubst (fst pb.proj_eta) in
+	  let typ = Vars.subst_univs_level_constr usubst (snd pb.proj_eta) in
+	    Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb 
+	| None ->
 	  let j = infer env body in
 	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
 	  let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index cb0c429a9..fa7dd105c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -388,7 +388,6 @@ let judge_of_projection env p cj =
     assert(eq_mind pb.proj_ind (fst ind));
     let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in
     let ty = substl (cj.uj_val :: List.rev args) ty in
-      (* TODO: Universe polymorphism for projections *)
       {uj_val = mkProj (p,cj.uj_val);
        uj_type = ty}