From 6e1f26a075a48fb32bce32e07d6b58e2f38b97a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 14:23:11 +0200 Subject: More precise explanation when a notation is not reversible for printing. --- intf/notation_term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cad6f4b821..d1cbb6a33d 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -74,7 +74,7 @@ type interpretation = (Id.t * (subscopes * notation_var_instance_type)) list * notation_constr -type reversibility_flag = bool +type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; -- cgit v1.2.3 From 407e154baa44609dea9f6f1ade746e24d60e2513 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Aug 2017 14:00:26 +0200 Subject: Rephrasing ETBinderList with a self-documenting and invariant-carrying argument. --- intf/extend.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/extend.ml b/intf/extend.ml index 5552bed559..e4d014a09c 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,8 @@ type production_level = | NextLevel | NumLevel of int +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint | ETBinder of bool @@ -36,7 +38,7 @@ type ('lev,'pos) constr_entry_key_gen = | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of bool * Tok.t list + | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) -- cgit v1.2.3 From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 16:15:57 +0200 Subject: Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed. --- intf/constrexpr.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index fbf9e248ab..2575b71ea5 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -70,8 +70,8 @@ and constr_expr_r = | CRef of reference * instance_expr option | CFix of Id.t Loc.located * fix_expr list | CCoFix of Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * @@ -107,9 +107,6 @@ and case_expr = constr_expr (* expression that is being matched and branch_expr = (cases_pattern_expr list list * constr_expr) Loc.located -and binder_expr = - Name.t Loc.located list * binder_kind * constr_expr - and fix_expr = Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr -- cgit v1.2.3 From 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 11 Aug 2017 19:24:50 +0200 Subject: Introducing an intermediary type "constr_prod_entry_key" for grammar productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API. --- intf/extend.ml | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) (limited to 'intf') diff --git a/intf/extend.ml b/intf/extend.ml index e4d014a09c..79bbbd376e 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,32 +29,41 @@ type production_level = | NextLevel | NumLevel of int -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +(** User-level types used to tell how to parse or interpret of the non-terminal *) type ('lev,'pos) constr_entry_key_gen = - | ETName | ETReference | ETBigint - | ETBinder of bool + | ETName + | ETReference + | ETBigint + | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of ('lev * 'pos) | ETPattern | ETOther of string * string - | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) type constr_entry_key = (int,unit) constr_entry_key_gen -(** Entries used in productions (in right-hand-side of grammar rules) *) - -type constr_prod_entry_key = - (production_level,production_position) constr_entry_key_gen - (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = (production_level,unit) constr_entry_key_gen +(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) + +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + +type constr_prod_entry_key = + | ETProdName (* Parsed as a name (ident or _) *) + | ETProdReference (* Parsed as a global reference *) + | ETProdBigint (* Parsed as an (unbounded) integer *) + | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) + | ETProdPattern (* Parsed as pattern (as subpart of a constr) *) + | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) + | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) + (** {5 AST for user-provided entries} *) type 'a user_symbol = -- cgit v1.2.3 From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Aug 2017 13:58:59 +0200 Subject: A bit of miscellaneous code documentation around notations. --- intf/notation_term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/notation_term.ml b/intf/notation_term.ml index d1cbb6a33d..028d14ccfd 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -63,7 +63,7 @@ type subscopes = tmp_scope_name option * scope_name list type notation_var_instance_type = | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList -(** Type of variables when interpreting a constr_expr as an notation_constr: +(** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = -- cgit v1.2.3 From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Aug 2017 20:05:03 +0200 Subject: Allows recursive patterns for binders to be associative on the left. This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder). --- intf/notation_term.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 028d14ccfd..52fd0f368f 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -25,11 +25,11 @@ type notation_constr = | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Id.t * Id.t * notation_constr * notation_constr * bool + | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr - | NBinderList of Id.t * Id.t * notation_constr * notation_constr + | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * -- cgit v1.2.3 From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 09:15:40 +0200 Subject: Adding support for parsing subterms of a notation as "pattern". This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms. --- intf/constrexpr.ml | 5 +++-- intf/extend.ml | 10 ++++++---- intf/intf.mllib | 2 +- intf/notation_term.ml | 6 +++--- 4 files changed, 13 insertions(+), 10 deletions(-) (limited to 'intf') diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 2575b71ea5..c598287943 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -46,7 +46,7 @@ type prim_token = type instance_expr = Misctypes.glob_level list type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Id.t + | CPatAlias of cases_pattern_expr * Name.t Loc.located | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -128,7 +128,8 @@ and local_binder_expr = and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder_expr list list (** for binders subexpressions *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/intf/extend.ml b/intf/extend.ml index 79bbbd376e..5258ef56b8 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -37,13 +37,13 @@ type ('lev,'pos) constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of ('lev * 'pos) - | ETPattern + | ETPattern of int | ETOther of string * string -(** Entries level (left-hand-side of grammar rules) *) +(** Entries level (left-hand side of grammar rules) *) type constr_entry_key = - (int,unit) constr_entry_key_gen + (production_level,production_position) constr_entry_key_gen (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) @@ -54,12 +54,14 @@ type simple_constr_prod_entry_key = type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +type binder_target = ForBinder | ForTerm + type constr_prod_entry_key = | ETProdName (* Parsed as a name (ident or _) *) | ETProdReference (* Parsed as a global reference *) | ETProdBigint (* Parsed as an (unbounded) integer *) | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *) - | ETProdPattern (* Parsed as pattern (as subpart of a constr) *) + | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *) | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *) | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) diff --git a/intf/intf.mllib b/intf/intf.mllib index 38a2a71cc0..2b8960d3f2 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -2,9 +2,9 @@ Constrexpr Evar_kinds Genredexpr Locus +Extend Notation_term Decl_kinds -Extend Glob_term Misctypes Pattern diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 52fd0f368f..83cc454f43 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,13 +61,13 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) type notation_var_instance_type = - | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent + | NtnInternTypeAny | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = @@ -95,7 +95,7 @@ type precedence = int type parenRelation = L | E | Any | Prec of precedence type tolerability = precedence * parenRelation -type level = precedence * tolerability list * notation_var_internalization_type list +type level = precedence * tolerability list * Extend.constr_entry_key list (** Grammar rules for a notation *) -- cgit v1.2.3 From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 12:35:56 +0200 Subject: Respecting the ident/pattern distinction in notation modifiers. --- intf/notation_term.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 83cc454f43..0f4bfef600 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -60,8 +60,11 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) + +type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern + type notation_var_instance_type = - | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type -- cgit v1.2.3 From e4d93d1cef27d3a8c1e36139fc1e118730406f67 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 17 Aug 2017 20:12:55 +0200 Subject: Adding general support for irrefutable disjunctive patterns. This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing. --- intf/glob_term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 61bbe2c264..3f48fa5479 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -105,7 +105,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option - | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g + | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g -- cgit v1.2.3 From 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 17:09:21 +0100 Subject: Notations: A step in cleaning constr_entry_key. - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions --- intf/extend.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'intf') diff --git a/intf/extend.ml b/intf/extend.ml index 5258ef56b8..813ed6dc6c 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -31,24 +31,24 @@ type production_level = (** User-level types used to tell how to parse or interpret of the non-terminal *) -type ('lev,'pos) constr_entry_key_gen = +type 'a constr_entry_key_gen = | ETName | ETReference | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) - | ETConstr of ('lev * 'pos) - | ETPattern of int + | ETConstr of 'a + | ETPattern of int option | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) type constr_entry_key = - (production_level,production_position) constr_entry_key_gen + (production_level * production_position) constr_entry_key_gen (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = - (production_level,unit) constr_entry_key_gen + production_level option constr_entry_key_gen (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) -- cgit v1.2.3 From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 20:50:03 +0100 Subject: Notations: Adding modifiers to tell which kind of binder a constr can parse. Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}. --- intf/extend.ml | 8 +++++++- intf/notation_term.ml | 9 ++++++++- intf/vernacexpr.ml | 1 + 3 files changed, 16 insertions(+), 2 deletions(-) (limited to 'intf') diff --git a/intf/extend.ml b/intf/extend.ml index 813ed6dc6c..78f0aa1178 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,11 @@ type production_level = | NextLevel | NumLevel of int +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + (** User-level types used to tell how to parse or interpret of the non-terminal *) type 'a constr_entry_key_gen = @@ -37,7 +42,8 @@ type 'a constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of 'a - | ETPattern of int option + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0f4bfef600..86f5adbd78 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,7 +61,14 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) -type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern +type notation_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8e0fe54c55..0b5009e26b 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,6 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key -- cgit v1.2.3 From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 23 Nov 2017 13:30:36 +0100 Subject: Change default for notations with variables bound to both terms and binders. For compatibility, the default is to parse as ident and not as pattern. --- intf/vernacexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'intf') diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 0b5009e26b..d16c9bb802 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,7 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key -- cgit v1.2.3