Add relevance marks on binders.

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

3 files changed, 22 insertions, 12 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index b681fb876e..0eacc24626 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -25,7 +25,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   let nparams = List.length mb.mind_params_ctxt in (* include letins *)
   let mind_entry_record = match mb.mind_record with
     | NotRecord -> None | FakeRecord -> Some None
-    | PrimRecord data -> Some (Some (Array.map pi1 data))
+    | PrimRecord data -> Some (Some (Array.map (fun (x,_,_,_) -> x) data))
   in
   let mind_entry_universes = match mb.mind_universes with
     | Monomorphic univs -> Monomorphic_entry univs
@@ -95,8 +95,8 @@ let eq_in_context (ctx1, t1) (ctx2, t2) =
 let check_packet env mind ind
     { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc;
       mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc;
-      mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_nb_constant;
-      mind_nb_args; mind_reloc_tbl } =
+      mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_relevant;
+      mind_nb_constant; mind_nb_args; mind_reloc_tbl } =
   let check = check mind in
 
   ignore mind_typename; (* passed through *)
@@ -117,6 +117,8 @@ let check_packet env mind ind
 
   check "mind_recargs" (Rtree.equal eq_recarg ind.mind_recargs mind_recargs);
 
+  check "mind_relevant" (Sorts.relevance_equal ind.mind_relevant mind_relevant);
+
   check "mind_nb_args" Int.(equal ind.mind_nb_args mind_nb_args);
   check "mind_nb_constant" Int.(equal ind.mind_nb_constant mind_nb_constant);
   check "mind_reloc_tbl" (eq_reloc_tbl ind.mind_reloc_tbl mind_reloc_tbl);
@@ -128,7 +130,8 @@ let check_same_record r1 r2 = match r1, r2 with
   | PrimRecord r1, PrimRecord r2 ->
     (* The kernel doesn't care about the names, we just need to check
        that the saved types are correct. *)
-    Array.for_all2 (fun (_,_,tys1) (_,_,tys2) ->
+    Array.for_all2 (fun (_,_,r1,tys1) (_,_,r2,tys2) ->
+        Array.equal Sorts.relevance_equal r1 r2 &&
         Array.equal Constr.equal tys1 tys2)
       r1 r2
   | (NotRecord | FakeRecord | PrimRecord _), _ -> false
diff --git a/checker/checker.ml b/checker/checker.ml
index 205a3984d5..9be88ee31e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -298,6 +298,7 @@ let explain_exn = function
       | IllTypedRecBody _ -> str"IllTypedRecBody"
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
+      | BadRelevance -> str"BadRelevance"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
   | InductiveError e ->
diff --git a/checker/values.ml b/checker/values.ml
index f2b961ef56..5cbf0ff298 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -119,6 +119,9 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 let v_sort = v_sum "sort" 3 (*SProp, Prop, Set*) [|[|v_univ(*Type*)|]|]
 let v_sortfam = v_enum "sorts_family" 4
 
+let v_relevance = v_sum "relevance" 2 [||]
+let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|]
+
 let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
 
 let v_boollist = List v_bool  
@@ -126,7 +129,7 @@ let v_boollist = List v_bool
 let v_caseinfo =
   let v_cstyle = v_enum "case_style" 5 in
   let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in
-  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
+  v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_relevance;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
 
@@ -141,9 +144,9 @@ let rec v_constr =
     [|Fail "Evar"|]; (* Evar *)
     [|v_sort|]; (* Sort *)
     [|v_constr;v_cast;v_constr|]; (* Cast *)
-    [|v_name;v_constr;v_constr|]; (* Prod *)
-    [|v_name;v_constr;v_constr|]; (* Lambda *)
-    [|v_name;v_constr;v_constr;v_constr|]; (* LetIn *)
+    [|v_binder_annot v_name;v_constr;v_constr|]; (* Prod *)
+    [|v_binder_annot v_name;v_constr;v_constr|]; (* Lambda *)
+    [|v_binder_annot v_name;v_constr;v_constr;v_constr|]; (* LetIn *)
     [|v_constr;Array v_constr|]; (* App *)
     [|v_puniverses v_cst|]; (* Const *)
     [|v_puniverses v_ind|]; (* Ind *)
@@ -156,12 +159,13 @@ let rec v_constr =
   |])
 
 and v_prec = Tuple ("prec_declaration",
-                    [|Array v_name; Array v_constr; Array v_constr|])
+                    [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
 
-let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|];               (* LocalAssum *)
-                                           [|v_name; v_constr; v_constr|] |]   (* LocalDef *)
+let v_rdecl = v_sum "rel_declaration" 0
+    [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)
+       [|v_binder_annot v_name; v_constr; v_constr|] |]   (* LocalDef *)
 let v_rctxt = List v_rdecl
 
 let v_section_ctxt = v_enum "emptylist" 1
@@ -231,6 +235,7 @@ let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_constr;
+    v_relevance;
     Any;
     v_univs;
     Opt v_context_set;
@@ -265,6 +270,7 @@ let v_one_ind = v_tuple "one_inductive_body"
     Array Int;
     Array Int;
     v_wfp;
+    v_relevance;
     Int;
     Int;
     Any|]
@@ -273,7 +279,7 @@ let v_finite = v_enum "recursivity_kind" 3
 
 let v_record_info =
   v_sum "record_info" 2
-    [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
+    [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_relevance; Array v_constr |]) |] |]
 
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;