Skip to content

Commit

Permalink
Debug printing for relevance marks
Browse files Browse the repository at this point in the history
  • Loading branch information
@SkySkimmer
SkySkimmer committed Nov 20, 2023
1 parent 2f3e6c2 commit cd5b388
Show file tree
Hide file tree
Showing 36 changed files with 661 additions and 471 deletions.
26 changes: 22 additions & 4 deletions doc/sphinx/addendum/sprop.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -241,15 +241,33 @@ The term :g:`c (top -> top) (fun x => x) c` infinitely reduces to itself.
Lack of tactic support
----------------------

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.

Relevance marks are invisible to the user, but 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.
17 changes: 12 additions & 5 deletions interp/constrexpr.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down
69 changes: 38 additions & 31 deletions interp/constrexpr_ops.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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 *)
Expand Down Expand Up @@ -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 &&
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 (_,_) ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 _
Expand Down Expand Up @@ -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
Expand All @@ -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.")
Expand All @@ -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
Expand Down
1 change: 1 addition & 0 deletions interp/constrexpr_ops.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]. *)
Expand Down
Loading

0 comments on commit cd5b388

Please sign in to comment.