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/extend.ml') 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 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/extend.ml') 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 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/extend.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'intf/extend.ml') 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 *) -- 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/extend.ml') 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 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'intf/extend.ml') 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) *) -- cgit v1.2.3