aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/07-commands-and-options/10747-canonical-better-message.rst5
-rw-r--r--doc/sphinx/language/gallina-extensions.rst15
-rw-r--r--pretyping/recordops.ml11
-rw-r--r--pretyping/recordops.mli1
-rw-r--r--test-suite/output/PrintCanonicalProjections.out18
-rw-r--r--test-suite/output/PrintCanonicalProjections.v46
-rw-r--r--vernac/g_vernac.mlg3
-rw-r--r--vernac/ppvernac.ml4
-rw-r--r--vernac/prettyp.ml18
-rw-r--r--vernac/prettyp.mli2
-rw-r--r--vernac/vernacentries.ml4
-rw-r--r--vernac/vernacexpr.ml2
12 files changed, 113 insertions, 16 deletions
diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
new file mode 100644
index 0000000000..e73be9c642
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ The :cmd:`Print Canonical Projections` command now can take constants and
+ prints only the unification rules that involve or are synthesized from given
+ constants (`#10747 <https://github.com/coq/coq/pull/10747>`_,
+ by Kazuhiko Sakaguchi).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8caa289a47..4ca20ce313 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2075,11 +2075,13 @@ in :ref:`canonicalstructures`; here only a simple example is given.
This is equivalent to a regular definition of :token:`ident` followed by the
declaration :n:`Canonical @ident`.
-.. cmd:: Print Canonical Projections
+.. cmd:: Print Canonical Projections {* @ident}
This displays the list of global names that are components of some
canonical structure. For each of them, the canonical structure of
- which it is a projection is indicated.
+ which it is a projection is indicated. If constants are given as
+ its arguments, only the unification rules that involve or are
+ synthesized from given constants will be shown.
.. example::
@@ -2089,10 +2091,15 @@ in :ref:`canonicalstructures`; here only a simple example is given.
Print Canonical Projections.
+ .. coqtop:: all
+
+ Print Canonical Projections nat.
+
.. note::
- The last line would not show up if the corresponding projection (namely
- :g:`Prf_equiv`) were annotated as not canonical, as described above.
+ The last line in the first example would not show up if the
+ corresponding projection (namely :g:`Prf_equiv`) were annotated as not
+ canonical, as described above.
Implicit types of variables
~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5b416a99f9..35e182840b 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,7 +114,7 @@ let find_primitive_projection c =
(* the effective components of a structure and the projections of the *)
(* structure *)
-(* Table des definitions "object" : pour chaque object c,
+(* Table of "object" definitions: for each object c,
c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
@@ -127,16 +127,19 @@ let find_primitive_projection c =
that maps the pair (Li,ci) to the following data
+ o_ORIGIN = c (the constant name which this conversion rule is
+ synthesized from)
o_DEF = c
o_TABS = B1...Bk
o_INJ = Some n (when ci is a reference to the parameter xi)
- o_PARAMS = a1...am
- o_NARAMS = m
+ o_TPARAMS = a1...am
+ o_NPARAMS = m
o_TCOMP = ui1...uir
*)
type obj_typ = {
+ o_ORIGIN : Constant.t;
o_DEF : constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option; (* position of trivial argument if any *)
@@ -224,7 +227,7 @@ let compute_canonical_projections env ~warn (con,ind) =
match cs_pattern_of_constr nenv t with
| patt, o_INJ, o_TCOMPS ->
((GlobRef.ConstRef proji_sp, (patt, t)),
- { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
+ { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
| exception Not_found ->
if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e8b0d771aa..aaba7cc3e5 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -73,6 +73,7 @@ type cs_pattern =
| Default_cs
type obj_typ = {
+ o_ORIGIN : Constant.t;
o_DEF : constr;
o_CTX : Univ.AUContext.t;
o_INJ : int option; (** position of trivial argument *)
diff --git a/test-suite/output/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out
new file mode 100644
index 0000000000..a4e2251440
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.out
@@ -0,0 +1,18 @@
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+nat <- sort_eq ( nat_eqType )
+nat <- sort_TYPE ( nat_TYPE )
+prod <- sort_eq ( prod_eqType )
+prod <- sort_TYPE ( prod_TYPE )
+sum <- sort_eq ( sum_eqType )
+sum <- sort_TYPE ( sum_TYPE )
+sum <- sort_TYPE ( sum_TYPE )
+prod <- sort_TYPE ( prod_TYPE )
+nat <- sort_TYPE ( nat_TYPE )
+bool <- sort_TYPE ( bool_TYPE )
+sum <- sort_eq ( sum_eqType )
+prod <- sort_eq ( prod_eqType )
+nat <- sort_eq ( nat_eqType )
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+bool <- sort_eq ( bool_eqType )
diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v
new file mode 100644
index 0000000000..808cdffe39
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.v
@@ -0,0 +1,46 @@
+Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
+Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.
+
+Definition eq_op (T : eqType) : T -> T -> bool :=
+ match T with Pack_eq _ op => op end.
+
+Definition bool_eqb b1 b2 :=
+ match b1, b2 with
+ | false, false => true
+ | true, true => true
+ | _, _ => false
+ end.
+
+Canonical bool_TYPE := Pack_TYPE bool.
+Canonical bool_eqType := Pack_eq bool bool_eqb.
+
+Canonical nat_TYPE := Pack_TYPE nat.
+Canonical nat_eqType := Pack_eq nat Nat.eqb.
+
+Definition prod_eqb (T U : eqType) (x y : T * U) :=
+ match x, y with
+ | (x1, x2), (y1, y2) =>
+ andb (eq_op _ x1 y1) (eq_op _ x2 y2)
+ end.
+
+Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
+Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).
+
+Definition sum_eqb (T U : eqType) (x y : T + U) :=
+ match x, y with
+ | inl x, inl y => eq_op _ x y
+ | inr x, inr y => eq_op _ x y
+ | _, _ => false
+ end.
+
+Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
+Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).
+
+Print Canonical Projections bool.
+Print Canonical Projections nat.
+Print Canonical Projections prod.
+Print Canonical Projections sum.
+Print Canonical Projections sort_TYPE.
+Print Canonical Projections sort_eq.
+Print Canonical Projections sort_TYPE bool.
+Print Canonical Projections bool_eqType.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 436648c163..69ab0fafe9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1026,7 +1026,8 @@ GRAMMAR EXTEND Gram
| IDENT "Coercions" -> { PrintCoercions }
| IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
-> { PrintCoercionPaths (s,t) }
- | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+ | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global
+ -> { PrintCanonicalConversions qids }
| IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
| IDENT "Tables" -> { PrintTables }
| IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1742027076..a1bd99c237 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -513,8 +513,8 @@ let string_of_theorem_kind = let open Decls in function
keyword "Print Coercion Paths" ++ spc()
++ pr_class_rawexpr s ++ spc()
++ pr_class_rawexpr t
- | PrintCanonicalConversions ->
- keyword "Print Canonical Structures"
+ | PrintCanonicalConversions qids ->
+ keyword "Print Canonical Structures" ++ prlist pr_smart_global qids
| PrintTypingFlags ->
keyword "Print Typing Flags"
| PrintTables ->
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index d04a02febc..8ced35c3be 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -996,12 +996,26 @@ let print_path_between cls clt =
in
print_path ((i,j),p)
-let print_canonical_projections env sigma =
+let print_canonical_projections env sigma grefs =
+ let match_proj_gref ((x,y),c) gr =
+ GlobRef.equal x gr ||
+ begin match y with
+ | Const_cs y -> GlobRef.equal y gr
+ | _ -> false
+ end ||
+ match gr with
+ | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con
+ | _ -> false
+ in
+ let projs =
+ List.filter (fun p -> List.for_all (match_proj_gref p) grefs)
+ (canonical_projections ())
+ in
prlist_with_sep fnl
(fun ((r1,r2),o) -> pr_cs_pattern r2 ++
str " <- " ++
pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
- (canonical_projections ())
+ projs
(*************************************************************************)
diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli
index 2ee9c4ed33..ac41f30c5d 100644
--- a/vernac/prettyp.mli
+++ b/vernac/prettyp.mli
@@ -53,7 +53,7 @@ val print_graph : unit -> Pp.t
val print_classes : unit -> Pp.t
val print_coercions : unit -> Pp.t
val print_path_between : Coercionops.cl_typ -> Coercionops.cl_typ -> Pp.t
-val print_canonical_projections : env -> Evd.evar_map -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> GlobRef.t list -> Pp.t
(** Pretty-printing functions for type classes and instances *)
val print_typeclasses : unit -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 604d1b28ff..04f3e0d7b2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1701,7 +1701,9 @@ let vernac_print ~pstate ~atts =
| PrintCoercions -> Prettyp.print_coercions ()
| PrintCoercionPaths (cls,clt) ->
Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)
- | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma
+ | PrintCanonicalConversions qids ->
+ let grefs = List.map Smartlocate.smart_global qids in
+ Prettyp.print_canonical_projections env sigma grefs
| PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst
| PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r)
| PrintHintGoal ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 32ff8b8fb2..1daa244986 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -46,7 +46,7 @@ type printable =
| PrintInstances of qualid or_by_notation
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
- | PrintCanonicalConversions
+ | PrintCanonicalConversions of qualid or_by_notation list
| PrintUniverses of bool * qualid list option * string option
| PrintHint of qualid or_by_notation
| PrintHintGoal
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:29:16 +0000