Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

1 files changed, 26 insertions, 17 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 457c17907e..545c0fe7b7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) =
   let specif = (lookup_mind_specif env mi, u) in
   let ty = type_of_inductive env specif in
   let env' =
-    let decl = LocalAssum (Anonymous, hnf_prod_applist env ty lrecparams) in
+    let r = (snd (fst specif)).mind_relevant in
+    let anon = Context.make_annot Anonymous r in
+    let decl = LocalAssum (anon, hnf_prod_applist env ty lrecparams) in
     push_rel decl env in
   let ra_env' =
     (Imbr mi,(Rtree.mk_rec_calls 1).(0)) ::
@@ -186,8 +188,8 @@ 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 c' with
-	Prod(na,a,b) ->
-	  let ienv' = ienv_push_var ienv (na,a,mk_norec) in
+        Prod(na,a,b) ->
+          let ienv' = ienv_push_var ienv (na,a,mk_norec) in
 	  ienv_decompose_prod ienv' (n-1) b
       | _ -> assert false
 
@@ -215,7 +217,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
   let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c =
     let x,largs = decompose_app (whd_all env c) in
       match kind x with
-	| Prod (na,b,d) ->
+        | Prod (na,b,d) ->
 	    let () = assert (List.is_empty largs) in
             (** If one of the inductives of the mutually inductive
                 block occurs in the left-hand side of a product, then
@@ -433,7 +435,7 @@ let compute_projections (kn, i as ind) mib =
       mkRel 1 :: List.map (lift 1) subst in
     subst
   in
-  let projections decl (i, j, labs, pbs, letsubst) =
+  let projections decl (i, j, labs, rs, pbs, letsubst) =
     match decl with
     | LocalDef (_na,c,_t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
@@ -445,10 +447,11 @@ let compute_projections (kn, i as ind) mib =
         (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
            to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
         let letsubst = c2 :: letsubst in
-        (i, j+1, labs, pbs, letsubst)
+        (i, j+1, labs, rs, pbs, letsubst)
     | LocalAssum (na,t) ->
-      match na with
+      match na.Context.binder_name with
       | Name id ->
+        let r = na.Context.binder_relevance in
         let lab = Label.of_id id in
         let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:i lab in
         (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
@@ -460,14 +463,15 @@ let compute_projections (kn, i as ind) mib =
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
-        (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst)
+        (i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, labs, pbs, _letsubst) =
-    List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
+  let (_, _, labs, rs, pbs, _letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
   in
-    Array.of_list (List.rev labs),
-    Array.of_list (List.rev pbs)
+  Array.of_list (List.rev labs),
+  Array.of_list (List.rev rs),
+  Array.of_list (List.rev pbs)
 
 let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
@@ -483,7 +487,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 	splayed_lc in
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d)
-	splayed_lc in
+        splayed_lc in
+    let mind_relevant = match arity with
+      | RegularArity { mind_sort;_ } -> Sorts.relevance_of_sort mind_sort
+      | TemplateArity _ -> Sorts.Relevant
+    in
     (* Assigning VM tags to constructors *)
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
@@ -510,8 +518,9 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 	mind_consnrealargs = consnrealargs;
 	mind_user_lc = lc;
 	mind_nf_lc = nf_lc;
-	mind_recargs = recarg;
-	mind_nb_constant = !nconst;
+        mind_recargs = recarg;
+        mind_relevant;
+        mind_nb_constant = !nconst;
 	mind_nb_args = !nblock;
 	mind_reloc_tbl = rtbl;
       } in
@@ -546,8 +555,8 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     (** The elimination criterion ensures that all projections can be defined. *)
     if Array.for_all is_record packets then
       let map i id =
-        let labs, projs = compute_projections (kn, i) mib in
-        (id, labs, projs)
+        let labs, rs, projs = compute_projections (kn, i) mib in
+        (id, labs, rs, projs)
       in
       try PrimRecord (Array.mapi map rid)
       with UndefinableExpansion -> FakeRecord