Debug printing for relevance marks

doc/sphinx/addendum/sprop.rst

@@ -238,18 +238,37 @@ breaks termination of reduction
 
 The term :g:`c (top -> top) (fun x => x) c` infinitely reduces to itself.
 
-Lack of tactic support
-----------------------
+Debugging |SProp| issues
+------------------------
 
-Some tactics do not handle |SProp| as they were not correctly ported. While in
-most of the cases they will just fail, in some cases this can result in sending
-ill-typed terms to the kernel, which will fail with anomalies at `Qed`.
+Every binder in a term (such as `fun x` or `forall x`) caches
+information called the :gdef:`relevance mark` indicating whether its type is
+in |SProp| or not. This is used to efficiently implement proof
+irrelevance.
+
+The user should usually not be concerned with relevance marks, so by
+default they are not displayed. However code outside the kernel may
+generate incorrect marks resulting in bugs. Typically this means a
+conversion will incorrectly fail as a variable was incorrectly marked
+proof relevant.
 
 .. warn:: Bad relevance
 
   This is a developer warning, which is treated as an error by default. It is
   emitted by the kernel when it is passed a term with incorrect relevance marks.
-  This is always caused by a bug in Coq, which should thus be reported and
+  This is always caused by a bug in Coq (or a plugin), which should thus be reported and
   fixed. In order to allow the user to work around such bugs, we leave the
   ability to unset the ``bad-relevance`` warning for the time being, so that the
   kernel will silently repair the proof term instead of failing.
+
+.. flag:: Printing Relevance Marks
+
+   This :term:`flag` enables debug printing of relevance marks. It is off by default.
+   Note that :flag:`Printing All` does not affect printing of relevance marks.
+
+   .. coqtop:: all
+
+      Set Printing Relevance Marks.
+
+      Check fun x : nat => x.
+      Check fun (P:SProp) (p:P) => p.

interp/constrexpr.mli

@@ -30,6 +30,12 @@ type quality_expr =
   | CQConstant of Sorts.Quality.constant
   | CQualVar of qvar_expr
 
+type relevance_expr =
+  | CRelevant | CIrrelevant
+  | CRelevanceVar of qvar_expr
+
+type relevance_info_expr = relevance_expr option
+
 type sort_expr = (qvar_expr option * (sort_name_expr * int) list) Glob_term.glob_sort_gen
 
 type instance_expr = quality_expr list * univ_level_expr list
@@ -176,11 +182,12 @@ and branch_expr =
   (cases_pattern_expr list list * constr_expr) CAst.t
 
 and fix_expr =
-    lident * recursion_order_expr option *
-      local_binder_expr list * constr_expr * constr_expr
+  lident * relevance_info_expr
+  * recursion_order_expr option *
+  local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
-    lident * local_binder_expr list * constr_expr * constr_expr
+    lident * relevance_info_expr * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr_r =
   | CStructRec of lident
@@ -190,8 +197,8 @@ and recursion_order_expr = recursion_order_expr_r CAst.t
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =
-  | CLocalAssum   of lname list * binder_kind * constr_expr
-  | CLocalDef     of lname * constr_expr * constr_expr option
+  | CLocalAssum   of lname list * relevance_info_expr * binder_kind * constr_expr
+  | CLocalDef     of lname * relevance_info_expr * constr_expr * constr_expr option
   | CLocalPattern of cases_pattern_expr
 
 and constr_notation_substitution =

interp/constrexpr_ops.ml

@@ -34,6 +34,13 @@ let qvar_expr_eq c1 c2 = match c1, c2 with
   | CRawQVar q1, CRawQVar q2 -> Sorts.QVar.equal q1 q2
   | (CQVar _ | CQAnon _ | CRawQVar _), _ -> false
 
+let relevance_expr_eq a b = match a, b with
+  | CRelevant, CRelevant | CIrrelevant, CIrrelevant -> true
+  | CRelevanceVar q1, CRelevanceVar q2 -> qvar_expr_eq q1 q2
+  | (CRelevant | CIrrelevant | CRelevanceVar _), _ -> false
+
+let relevance_info_expr_eq = Option.equal relevance_expr_eq
+
 let univ_level_expr_eq u1 u2 =
   Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2
 
@@ -57,10 +64,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with
 let default_binder_kind = Default Explicit
 
 let names_of_local_assums bl =
-  List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|_->[]) bl)
 
 let names_of_local_binders bl =
-  List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl)
+  List.flatten (List.map (function CLocalAssum(l,_,_,_)->l|CLocalDef(l,_,_,_)->[l]|CLocalPattern _ -> assert false) bl)
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -150,21 +157,21 @@ module EqGen (A:sig val constr_expr_eq : constr_expr -> constr_expr -> bool end)
   let recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2
 
   let local_binder_eq l1 l2 = match l1, l2 with
-    | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
+    | CLocalDef (n1, _, e1, t1), CLocalDef (n2, _, e2, t2) ->
       CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
-    | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
-      (* Don't care about the [binder_kind] *)
+    | CLocalAssum (n1, _, _, e1), CLocalAssum (n2, _, _, e2) ->
+      (* Don't care about the metadata *)
       List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2
     | _ -> false
 
-  let fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
+  let fix_expr_eq (id1,_,r1,bl1,a1,b1) (id2,_,r2,bl2,a2,b2) =
     (lident_eq id1 id2) &&
     Option.equal recursion_order_expr_eq r1 r2 &&
     List.equal local_binder_eq bl1 bl2 &&
     constr_expr_eq a1 a2 &&
     constr_expr_eq b1 b2
 
-  let cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
+  let cofix_expr_eq (id1,_,bl1,a1,b1) (id2,_,bl2,a2,b2) =
     (lident_eq id1 id2) &&
     List.equal local_binder_eq bl1 bl2 &&
     constr_expr_eq a1 a2 &&
@@ -283,10 +290,10 @@ let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
 let local_binder_loc = let open CAst in function
-  | CLocalAssum ({ loc } ::_,_,t)
-  | CLocalDef ( { loc },t,None) -> Loc.merge_opt loc (constr_loc t)
-  | CLocalDef ( { loc },b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
-  | CLocalAssum ([],_,_) -> assert false
+  | CLocalAssum ({ loc } ::_,_,_,t)
+  | CLocalDef ( { loc },_,t,None) -> Loc.merge_opt loc (constr_loc t)
+  | CLocalDef ( { loc },_,b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
+  | CLocalAssum ([],_,_,_) -> assert false
   | CLocalPattern { loc } -> loc
 
 let local_binders_loc bll = match bll with
@@ -340,11 +347,11 @@ let ids_of_cases_tomatch tms =
     tms Id.Set.empty
 
 let rec fold_local_binders g f n acc b = let open CAst in function
-  | CLocalAssum (nal,bk,t)::l ->
+  | CLocalAssum (nal,_,bk,t)::l ->
     let nal = List.(map (fun {v} -> v) nal) in
     let n' = List.fold_right (Name.fold_right g) nal n in
     f n (fold_local_binders g f n' acc b l) t
-  | CLocalDef ( { v = na },c,t)::l ->
+  | CLocalDef ( { v = na },_,c,t)::l ->
     Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
   | CLocalPattern pat :: l ->
     let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
@@ -383,8 +390,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
       Option.fold_left
         (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
     | CFix (_,l) ->
-      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
-      List.fold_right (fun (_,ro,lb,t,c) acc ->
+      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_,_) -> g id) l n in
+      List.fold_right (fun (_,_,ro,lb,t,c) acc ->
           fold_local_binders g f n'
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->
@@ -452,10 +459,10 @@ let fold_map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
   let open CAst in
   let h (e,bl) = function
-      CLocalAssum(nal,k,ty) ->
-      (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
-    | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
-      (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
+      CLocalAssum(nal,r,k,ty) ->
+      (map_binder g e nal, CLocalAssum(nal,r,k,f e ty)::bl)
+    | CLocalDef( { loc ; v = na } as cna ,r,c,ty) ->
+      (Name.fold_right g na e, CLocalDef(cna,r,f e c,Option.map (f e) ty)::bl)
     | CLocalPattern pat ->
       let e, pat = fold_map_cases_pattern g f e pat in
       (e, CLocalPattern pat::bl) in
@@ -497,20 +504,20 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
     | CFix (id,dl) ->
-      CFix (id,List.map (fun (id,n,bl,t,d) ->
+      CFix (id,List.map (fun (id,r,n,bl,t,d) ->
           let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
           (* Note: fix names should be inserted before the arguments... *)
-          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
-          (id,n,bl',t',d')) dl)
+          (id,r,n,bl',t',d')) dl)
     | CCoFix (id,dl) ->
-      CCoFix (id,List.map (fun (id,bl,t,d) ->
+      CCoFix (id,List.map (fun (id,r,bl,t,d) ->
           let (e',bl') = fold_map_local_binders f g e bl in
           let t' = f e' t in
-          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
-          (id,bl',t',d')) dl)
+          (id,r,bl',t',d')) dl)
     | CArray (u, t, def, ty) ->
       CArray (u, Array.map (f e) t, f e def, f e ty)
     | CHole _ | CGenarg _ | CGenargGlob _ | CEvar _ | CPatVar _ | CSort _
@@ -563,7 +570,7 @@ let split_at_annot bl na =
     end
   | Some { loc; v = id } ->
     let rec aux acc = function
-      | CLocalAssum (bls, k, t) as x :: rest ->
+      | CLocalAssum (bls, rinfo, k, t) as x :: rest ->
         let test { CAst.v = na } = match na with
           | Name id' -> Id.equal id id'
           | Anonymous -> false
@@ -574,11 +581,11 @@ let split_at_annot bl na =
           | _ ->
             let ans = match l with
               | [] -> acc
-              | _ -> CLocalAssum (l, k, t) :: acc
+              | _ -> CLocalAssum (l, rinfo, k, t) :: acc
             in
-            (List.rev ans, CLocalAssum (r, k, t) :: rest)
+            (List.rev ans, CLocalAssum (r, rinfo, k, t) :: rest)
         end
-      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
+      | CLocalDef ({ CAst.v = na },_,_,_) as x :: rest ->
         if Name.equal (Name id) na then
           CErrors.user_err ?loc
             (Id.print id ++ str" must be a proper parameter and not a local definition.")
@@ -596,9 +603,9 @@ let split_at_annot bl na =
 let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k,t) = CAst.make @@ CCast (a,k,t)
-let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,None,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,None,bk,a)],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in

interp/constrexpr_ops.mli

@@ -19,6 +19,7 @@ open Constrexpr
 val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool
 val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool
 val sort_expr_eq : sort_expr -> sort_expr -> bool
+val relevance_info_expr_eq : relevance_info_expr -> relevance_info_expr -> bool
 
 val explicitation_eq : explicitation -> explicitation -> bool
 (** Equality on [explicitation]. *)