Add relevance marks on binders.

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

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

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 ->

checker/values.ml

@@ -119,14 +119,17 @@ 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  
 
 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;

clib/cArray.ml

@@ -52,6 +52,8 @@ sig
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+  val map3_i :
+    (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
@@ -358,6 +360,21 @@ let map3 f v1 v2 v3 =
     res
   end
 
+let map3_i f v1 v2 v3 =
+  let len1 = Array.length v1 in
+  let len2 = Array.length v2 in
+  let len3 = Array.length v3 in
+  let () = if not (Int.equal len1 len2 && Int.equal len1 len3) then invalid_arg "Array.map3_i" in
+  if Int.equal len1 0 then
+    [| |]
+  else begin
+    let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0) (uget v3 0)) in
+    for i = 1 to pred len1 do
+      Array.unsafe_set res i (f i (uget v1 i) (uget v2 i) (uget v3 i))
+    done;
+    res
+  end
+
 let map_left f a = (* Ocaml does not guarantee Array.map is LR *)
   let l = Array.length a in (* (even if so), then we rewrite it *)
   if Int.equal l 0 then [||] else begin

clib/cArray.mli

@@ -83,6 +83,8 @@ sig
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+  val map3_i :
+    (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
 
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   (** As [map] but guaranteed to be left-to-right. *)

clib/cList.ml

@@ -98,6 +98,7 @@ sig
   val split : ('a * 'b) list -> 'a list * 'b list
   val combine : 'a list -> 'b list -> ('a * 'b) list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   val add_set : 'a eq -> 'a -> 'a list -> 'a list
   val eq_set : 'a eq -> 'a list -> 'a list -> bool
@@ -846,6 +847,12 @@ let split3 = function
     split3_loop cp cq cr l;
     (cast cp, cast cq, cast cr)
 
+(** XXX TODO tailrec *)
+let rec split4 = function
+  | [] -> ([], [], [], [])
+  | (a,b,c,d)::l ->
+      let (ra, rb, rc, rd) = split4 l in (a::ra, b::rb, c::rc, d::rd)
+
 let rec combine3_loop p l1 l2 l3 = match l1, l2, l3 with
   | [], [], [] -> ()
   | x :: l1, y :: l2, z :: l3 ->

clib/cList.mli

@@ -308,6 +308,9 @@ sig
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
   (** Like [split] but for triples *)
 
+  val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
+  (** Like [split] but for quads *)
+
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   (** Like [combine] but for triples *)
 

dev/top_printers.ml

@@ -20,6 +20,7 @@ open Univ
 open Environ
 open Printer
 open Constr
+open Context
 open Genarg
 open Clenv
 
@@ -316,7 +317,7 @@ let constr_display csr =
     Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
         then (" "^i) else "")) (Instance.to_array l) ""
 
-  and name_display = function
+  and name_display x = match x.binder_name with
     | Name id -> "Name("^(Id.to_string id)^")"
     | Anonymous -> "Anonymous"
 
@@ -336,13 +337,13 @@ let print_pure_constr csr =
   | Cast (c,_, t) -> open_hovbox 1;
       print_string "("; (term_display c); print_cut();
       print_string "::"; (term_display t); print_string ")"; close_box()
-  | Prod (Name(id),t,c) ->
+  | Prod ({binder_name=Name(id)},t,c) ->
       open_hovbox 1;
       print_string"("; print_string (Id.to_string id);
       print_string ":"; box_display t;
       print_string ")"; print_cut();
       box_display c; close_box()
-  | Prod (Anonymous,t,c) ->
+  | Prod ({binder_name=Anonymous},t,c) ->
       print_string"("; box_display t; print_cut(); print_string "->";
       box_display c; print_string ")";
   | Lambda (na,t,c) ->
@@ -437,7 +438,7 @@ let print_pure_constr csr =
     | Type u -> open_hbox();
 	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
 
-  and name_display = function
+  and name_display x = match x.binder_name with
     | Name id -> print_string (Id.to_string id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)

doc/plugin_tutorial/tuto3/src/construction_game.ml

@@ -1,4 +1,5 @@
 open Pp
+open Context
 
 let find_reference = Coqlib.find_reference [@ocaml.warning "-3"]
 
@@ -32,15 +33,15 @@ let dangling_identity env evd =
   let evd, arg_type = Evarutil.new_evar env evd type_type in
 (* Notice the use of a De Bruijn index for the inner occurrence of the
   bound variable. *)
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let dangling_identity2 env evd =
 (* This example uses directly a function that produces an evar that
   is meant to be a type. *)
   let evd, (arg_type, type_type) =
     Evarutil.new_type_evar env evd Evd.univ_rigid in
-  evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+  evd, EConstr.mkLambda(nameR (Names.Id.of_string "x"), arg_type,
           EConstr.mkRel 1)
 
 let example_sort_app_lambda () =

doc/plugin_tutorial/tuto3/src/tuto_tactic.ml

@@ -116,11 +116,11 @@ let repackage i h_hyps_id = Goal.enter begin fun gl ->
           mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
     Refine.refine ~typecheck:true begin fun evd ->
       let evd, new_goal = Evarutil.new_evar env evd
-          (mkProd (Names.Name.Anonymous,
-                     mkApp(c_H (), [| new_packed_type |]),
-                       Vars.lift 1 concl)) in
-        evd, mkApp (new_goal,
-                 [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+          (mkArrowR (mkApp(c_H (), [| new_packed_type |]))
+             (Vars.lift 1 concl))
+      in
+      evd, mkApp (new_goal,
+                  [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
       end
     end
 

engine/eConstr.ml

@@ -73,7 +73,8 @@ let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
-let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2))
+let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2
 let mkInt i = of_kind (Int i)
 
 let mkRef (gr,u) = let open GlobRef in match gr with
@@ -668,9 +669,9 @@ let mkLambda_or_LetIn decl c =
   | LocalAssum (na,t) -> mkLambda (na, t, c)
   | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
-let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
-let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
-let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
+let mkNamedProd id typ c = mkProd (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLambda id typ c = mkLambda (map_annot Name.mk_name id, typ, Vars.subst_var id.binder_name c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (map_annot Name.mk_name id, c1, t, Vars.subst_var id.binder_name c2)
 
 let mkNamedProd_or_LetIn decl c =
   let open Context.Named.Declaration in

engine/eConstr.mli

@@ -109,9 +109,9 @@ val mkProp : t
 val mkSet  : t
 val mkType : Univ.Universe.t -> t
 val mkCast : t * cast_kind * t -> t
-val mkProd : Name.t * t * t -> t
-val mkLambda : Name.t * t * t -> t
-val mkLetIn : Name.t * t * t * t -> t
+val mkProd : Name.t Context.binder_annot * t * t -> t
+val mkLambda : Name.t Context.binder_annot * t * t -> t
+val mkLetIn : Name.t Context.binder_annot * t * t * t -> t
 val mkApp : t * t array -> t
 val mkConst : Constant.t -> t
 val mkConstU : Constant.t * EInstance.t -> t
@@ -124,7 +124,8 @@ val mkConstructUi : (inductive * EInstance.t) * int -> t
 val mkCase : case_info * t * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
-val mkArrow : t -> t -> t
+val mkArrow : t -> Sorts.relevance  -> t -> t
+val mkArrowR : t -> t -> t
 val mkInt : Uint63.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
@@ -139,9 +140,9 @@ val mkLambda_or_LetIn : rel_declaration -> t -> t
 val it_mkProd_or_LetIn : t -> rel_context -> t
 val it_mkLambda_or_LetIn : t -> rel_context -> t
 
-val mkNamedLambda : Id.t -> types -> constr -> constr
-val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
-val mkNamedProd : Id.t -> types -> types -> types
+val mkNamedLambda : Id.t Context.binder_annot -> types -> constr -> constr
+val mkNamedLetIn : Id.t Context.binder_annot -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t Context.binder_annot -> types -> types -> types
 val mkNamedLambda_or_LetIn : named_declaration -> types -> types
 val mkNamedProd_or_LetIn : named_declaration -> types -> types
 
@@ -179,9 +180,9 @@ val destMeta : Evd.evar_map -> t -> metavariable
 val destVar : Evd.evar_map -> t -> Id.t
 val destSort : Evd.evar_map -> t -> ESorts.t
 val destCast : Evd.evar_map -> t -> t * cast_kind * t
-val destProd : Evd.evar_map -> t -> Name.t * types * types
-val destLambda : Evd.evar_map -> t -> Name.t * types * t
-val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t
+val destProd : Evd.evar_map -> t -> Name.t Context.binder_annot * types * types
+val destLambda : Evd.evar_map -> t -> Name.t Context.binder_annot * types * t
+val destLetIn : Evd.evar_map -> t -> Name.t Context.binder_annot * t * types * t
 val destApp : Evd.evar_map -> t -> t * t array
 val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
@@ -197,7 +198,7 @@ val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
 val decompose_app : Evd.evar_map -> t -> t * t list
 
 (** Pops lambda abstractions until there are no more, skipping casts. *)
-val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_lam : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t
 
 (** Pops lambda abstractions and letins until there are no more, skipping casts. *)
 val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
@@ -213,10 +214,10 @@ val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
      @raise UserError if the term doesn't have enough lambdas/letins. *)
 val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
 
-val compose_lam : (Name.t * t) list -> t -> t
+val compose_lam : (Name.t Context.binder_annot * t) list -> t -> t
 val to_lambda : Evd.evar_map -> int -> t -> t
 
-val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t
+val decompose_prod : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t
 val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t
 val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
 

engine/evarutil.ml

@@ -11,6 +11,7 @@
 open CErrors
 open Util
 open Names
+open Context
 open Constr
 open Environ
 open Evd
@@ -781,13 +782,13 @@ let cached_evar_of_hyp cache sigma decl accu = match cache with
   in
   NamedDecl.fold_constr fold decl accu
 | Some cache ->
-  let id = NamedDecl.get_id decl in
+  let id = NamedDecl.get_annot decl in
   let r =
-    try Id.Map.find id cache.cache
+    try Id.Map.find id.binder_name cache.cache
     with Not_found ->
       (* Dummy value *)
       let r = ref (NamedDecl.LocalAssum (id, EConstr.mkProp), Evar.Set.empty) in
-      let () = cache.cache <- Id.Map.add id r cache.cache in
+      let () = cache.cache <- Id.Map.add id.binder_name r cache.cache in
       r
   in
   let (decl', evs) = !r in