From 63b530234e0b19323a50c52434a7439518565c81 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 03:15:17 +0200 Subject: [notations] Split interpretation and parsing of notations Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries. --- printing/genprint.ml | 8 ++++---- printing/genprint.mli | 8 ++++---- printing/ppconstr.ml | 4 +--- printing/ppconstr.mli | 2 +- printing/printer.mli | 6 +++--- 5 files changed, 13 insertions(+), 15 deletions(-) (limited to 'printing') diff --git a/printing/genprint.ml b/printing/genprint.ml index 1bb7838a4..fa53a8794 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -19,15 +19,15 @@ open Geninterp (* Printing generic values *) type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { default_already_surrounded : Notation_gram.tolerability; + default_ensure_surrounded : Notation_gram.tolerability; printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/genprint.mli b/printing/genprint.mli index fd5dd7259..1a31025a9 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -13,15 +13,15 @@ open Genarg type 'a with_level = - { default_already_surrounded : Notation_term.tolerability; - default_ensure_surrounded : Notation_term.tolerability; + { default_already_surrounded : Notation_gram.tolerability; + default_ensure_surrounded : Notation_gram.tolerability; printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level +| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level -type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t type top_printer_result = | TopPrinterBasic of (unit -> Pp.t) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2a5f38697..e877b3c63 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -19,7 +19,7 @@ open Constr open Libnames open Pputils open Ppextend -open Notation_term +open Notation_gram open Constrexpr open Constrexpr_ops open Decl_kinds @@ -88,8 +88,6 @@ let tag_var = tag Tag.variable | Numeral (_,b) -> if b then lposint else lnegint | String _ -> latom - open Notation - let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 127c4471c..05f48ec79 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -16,7 +16,7 @@ open Libnames open Constrexpr open Names open Misctypes -open Notation_term +open Notation_gram val prec_less : precedence -> tolerability -> bool diff --git a/printing/printer.mli b/printing/printer.mli index ac0e12979..7a8b963d2 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -36,7 +36,7 @@ val pr_constr : constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_n_env : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t +val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" @@ -57,7 +57,7 @@ val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t val pr_leconstr : EConstr.t -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_econstr_n_env : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t +val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t @@ -87,7 +87,7 @@ val pr_type_env : env -> evar_map -> types -> Pp.t val pr_type : types -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -val pr_closed_glob_n_env : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t +val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t val pr_closed_glob : closed_glob_constr -> Pp.t [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] -- cgit v1.2.3