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. --- printing/ppvernac.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 950246c531..a7e73c91f4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -102,7 +102,6 @@ open Decl_kinds | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" let pr_comment pr_c = function | CommentConstr c -> pr_c c -- 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. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a7e73c91f4..ae73640525 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -96,7 +96,7 @@ open Decl_kinds let pr_set_entry_type = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern -> str"pattern" + | ETPattern _ -> str"pattern" | ETConstr _ -> str"constr" | ETOther (_,e) -> str e | ETBigint -> str "bigint" -- 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 --- printing/ppvernac.ml | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ae73640525..42329d03a7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -93,16 +93,28 @@ open Decl_kinds let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() - let pr_set_entry_type = function + let pr_at_level = function + | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n + | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + + let pr_set_entry_type pr = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern _ -> str"pattern" - | ETConstr _ -> str"constr" + | ETPattern None -> str"pattern" + | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETConstr lev -> str"constr" ++ pr lev | ETOther (_,e) -> str e | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" + let pr_at_level_opt = function + | None -> mt () + | Some n -> spc () ++ pr_at_level n + + let pr_set_simple_entry_type = + pr_set_entry_type pr_at_level_opt + let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s @@ -359,17 +371,13 @@ open Decl_kinds let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) let pr_syntax_modifier = function - | SetItemLevel (l,NextLevel) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ keyword "at next level" - | SetItemLevel (l,NumLevel n) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ keyword "at level" ++ spc() ++ int n - | SetLevel n -> keyword "at level" ++ spc() ++ int n + | SetItemLevel (l,n) -> + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n + | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" - | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing -> keyword "only parsing" | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") -- 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}. --- printing/ppvernac.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 42329d03a7..2fc7843eda 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -97,13 +97,21 @@ open Decl_kinds | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + let pr_constr_as_binder_kind = function + | AsIdent -> keyword "as ident" + | AsIdentOrPattern -> keyword "as pattern" + | AsStrictPattern -> keyword "as strict pattern" + + let pr_strict b = if b then str "strict " else mt () + let pr_set_entry_type pr = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern None -> str"pattern" - | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETPattern (b,None) -> pr_strict b ++ str"pattern" + | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) | ETConstr lev -> str"constr" ++ pr lev | ETOther (_,e) -> str e + | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" @@ -373,6 +381,9 @@ open Decl_kinds let pr_syntax_modifier = function | SetItemLevel (l,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n + | SetItemLevelAsBinder (l,bk,n) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" -- 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. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppvernac.ml') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2fc7843eda..31c0d20f32 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -383,7 +383,7 @@ open Decl_kinds prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n | SetItemLevelAsBinder (l,bk,n) -> prlist_with_sep sep_v2 str l ++ - spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk + spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" -- cgit v1.2.3