Safer entry point of primitive projections in the kernel, now it does recognize

a projection constant only of the form
 λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).

8 files changed, 54 insertions, 30 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 07c18d5e3..c672ba731 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -53,8 +53,6 @@ type mutual_inductive_entry = {
 type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
 type const_entry_body = proof_output Future.computation
 
-type projection = mutual_inductive * int * int * types
-
 type definition_entry = {
   const_entry_body   : const_entry_body;
   (* List of sectoin variables *)
@@ -64,7 +62,7 @@ type definition_entry = {
   const_entry_type        : types option;
   const_entry_polymorphic : bool;
   const_entry_universes   : Univ.universe_context;
-  const_entry_proj        : projection option;
+  const_entry_proj        : bool;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 770c720d8..d6df6366c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -119,6 +119,38 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
+
+let check_projection env kn inst 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 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 arg = destRel p - 1 in
+  let () = if not (arg < Array.length recinfo) then cannot_recognize () in
+  let () = if not (eq_con_chk recinfo.(Array.length recinfo - (arg + 1)) kn) then cannot_recognize () in
+  let pb = { proj_ind = fst ci.ci_ind;
+	     proj_npars = n;
+	     proj_arg = arg;
+	     proj_type = ty;
+	     proj_body = body }
+  in pb
   
 let infer_declaration env kn dcl =
   match dcl with
@@ -153,23 +185,20 @@ let infer_declaration env kn dcl =
       assert(Univ.ContextSet.is_empty ctx);
       let body = handle_side_effects env body side_eff in
       let def, typ, proj = 
-	match c.const_entry_proj with
-	| Some (ind, n, m, ty) ->
-            (* FIXME: check projection *)
-	  let pb = { proj_ind = ind;
-		     proj_npars = n;
-		     proj_arg = m;
-		     proj_type = ty;
-		     proj_body = body }
-	  in 
+	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 (map_option_typ typ) in
+	  (** We check it does indeed have the shape of a projection. *)
+	  let inst = Univ.UContext.instance c.const_entry_universes in
+	  let pb = check_projection env (Option.get kn) inst 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
-	    (* TODO: recognize projection *)
-	  let context, m = decompose_lam_n_assum (n + 1) body in 
 	  let body = it_mkLambda_or_LetIn body' context in
-
 	    Def (Mod_subst.from_val (hcons_constr body)),
-	    RegularArity (hcons_constr (Option.get typ)), Some pb
-	| None ->
+	    typ, Some pb
+	else
 	  let j = infer env body in
 	  let j = hcons_j j in
 	  let typ = constrain_type env j c.const_entry_polymorphic (map_option_typ typ) in
diff --git a/library/declare.ml b/library/declare.ml
index dce346782..7a80d103d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -199,7 +199,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
   { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_proj = None;
+    const_entry_proj = false;
     const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
@@ -237,7 +237,7 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = cb.const_universes;
-	const_entry_proj = None;
+	const_entry_proj = false;
     });
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 89939b864..7c44f1500 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -327,7 +327,7 @@ let close_proof ?feedback_id ~now fpl =
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
 	  const_entry_polymorphic = poly;
-	  const_entry_proj = None})
+	  const_entry_proj = false})
       fpl initial_goals in
   { id = pid; entries = entries; persistence = strength; universes = univsubst },
   Ephemeron.get terminator
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 1f09d7620..6f3f5cc49 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -126,7 +126,7 @@ let define internal id c p univs =
     const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff);
     const_entry_secctx = None;
     const_entry_type = None;
-    const_entry_proj = None;
+    const_entry_proj = false;
     const_entry_polymorphic = p;
     const_entry_universes = Evd.evar_context_universe_context ctx;
     const_entry_opaque = false;
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a5e30b210..d17136f1c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -120,7 +120,7 @@ let define id internal ctx c t =
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_proj = None;
+	const_entry_proj = false;
 	const_entry_polymorphic = true;
 	const_entry_universes = Evd.universe_context ctx;
         const_entry_opaque = false;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 1543c5e87..067b92554 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -636,7 +636,7 @@ let declare_obligation prg obl body uctx =
         { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then Some ty else None;
-	  const_entry_proj = None;
+	  const_entry_proj = false;
 	  const_entry_polymorphic = poly;
 	  const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 71f017598..4b8a4fa0d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -247,12 +247,9 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                 it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	      let kn =
 	        try
-		  let projinfo = 
-		    (fst indsp, mib.mind_nparams, nfields - nfi, ccl)
-		  in
-		  let projinfo =
-		    if !primitive_flag && optci = None then Some projinfo 
-		    else None
+		  let makeprim =
+		    if !primitive_flag && optci = None then true
+		    else false
 		  in
 		  let cie = {
                     const_entry_body =
@@ -261,7 +258,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
                     const_entry_type = Some projtyp;
 		    const_entry_polymorphic = poly;
 		    const_entry_universes = ctx;
-		    const_entry_proj = projinfo;
+		    const_entry_proj = makeprim;
                     const_entry_opaque = false;
                     const_entry_inline_code = false;
                     const_entry_feedback = None;