aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-24 03:15:17 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-31 11:16:47 +0200
commit63b530234e0b19323a50c52434a7439518565c81 (patch)
tree12c19a5ffbbb08fade444b7ec495e44090dfad14
parent2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f (diff)
[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.
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml99
-rw-r--r--interp/notation.mli23
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--interp/notation_term.ml37
-rw-r--r--parsing/extend.ml7
-rw-r--r--parsing/notation_gram.ml42
-rw-r--r--parsing/notgram_ops.ml65
-rw-r--r--parsing/notgram_ops.mli (renamed from interp/ppextend.ml)37
-rw-r--r--parsing/parsing.mllib3
-rw-r--r--parsing/ppextend.ml76
-rw-r--r--parsing/ppextend.mli (renamed from interp/ppextend.mli)18
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extraargs.mli2
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/pptactic.mli4
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--printing/genprint.ml8
-rw-r--r--printing/genprint.mli8
-rw-r--r--printing/ppconstr.ml4
-rw-r--r--printing/ppconstr.mli2
-rw-r--r--printing/printer.mli6
-rw-r--r--vernac/egramcoq.ml10
-rw-r--r--vernac/egramcoq.mli2
-rw-r--r--vernac/g_vernac.ml46
-rw-r--r--vernac/metasyntax.ml27
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/vernacexpr.ml2
30 files changed, 269 insertions, 238 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3a88284e4..45c0e9c42 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -820,11 +820,11 @@ let split_by_type ids subst =
| NtnTypeConstr ->
let terms,terms' = bind id scl terms terms' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
+ | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 8ed2b9fad..3668455ae 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -10,7 +10,6 @@ Notation
Syntax_def
Smartlocate
Constrexpr_ops
-Ppextend
Dumpglob
Reserve
Impargs
diff --git a/interp/notation.ml b/interp/notation.ml
index 192c477be..05fcd0e7f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -20,7 +20,6 @@ open Constrexpr
open Notation_term
open Glob_term
open Glob_ops
-open Ppextend
open Context.Named.Declaration
(*i*)
@@ -56,9 +55,6 @@ type scope = {
delimiters: delimiters option
}
-(* Uninterpreted notation map: notation -> level * DirPath.t *)
-let notation_level_map = ref String.Map.empty
-
(* Scopes table: scope_name -> symbol_interpretation *)
let scope_map = ref String.Map.empty
@@ -75,44 +71,6 @@ let default_scope = "" (* empty name, not available from outside *)
let init_scope_map () =
scope_map := String.Map.add default_scope empty_scope !scope_map
-(**********************************************************************)
-(* Operations on scopes *)
-
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
-
-open Extend
-
-let production_level_eq l1 l2 = true (* (l1 = l2) *)
-
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
-
-let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETName, ETName -> true
-| ETReference, ETReference -> true
-| ETBigint, ETBigint -> true
-| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
-| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
-
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
- let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
- let prod_eq (l1,pp1) (l2,pp2) =
- if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
- else production_level_eq l1 l2 in
- Int.equal l1 l2 && List.equal tolerability_eq t1 t2
- && List.equal (constr_entry_key_eq prod_eq) u1 u2
-
-let level_eq = level_eq_gen false
-
let declare_scope scope =
try let _ = String.Map.find scope !scope_map in ()
with Not_found ->
@@ -427,18 +385,6 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Can we switch to [scope]? Yes if it has defined delimiters *)
find_with_delimiters ntn_scope
-(* Uninterpreted notation levels *)
-
-let declare_notation_level ?(onlyprint=false) ntn level =
- if String.Map.mem ntn !notation_level_map then
- anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
- notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
- let (level,onlyprint') = String.Map.find ntn !notation_level_map in
- if onlyprint' && not onlyprint then raise Not_found;
- level
-
(* The mapping between notations and their interpretation *)
let warn_notation_overridden =
@@ -1113,63 +1059,24 @@ let pr_visibility prglob = function
| None -> pr_scope_stack prglob !scope_stack
(**********************************************************************)
-(* Mapping notations to concrete syntax *)
-
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-(* Concrete syntax for symbolic-extension table *)
-let notation_rules =
- ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
-
-let declare_notation_rule ntn ~extra unpl gram =
- notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
-
-let find_notation_printing_rule ntn =
- try pi1 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
- try pi2 (String.Map.find ntn !notation_rules)
- with Not_found -> []
-let find_notation_parsing_rules ntn =
- try pi3 (String.Map.find ntn !notation_rules)
- with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
-
-let get_defined_notations () =
- String.Set.elements @@ String.Map.domain !notation_rules
-
-let add_notation_extra_printing_rule ntn k v =
- try
- notation_rules :=
- let p, pp, gr = String.Map.find ntn !notation_rules in
- String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
- with Not_found ->
- user_err ~hdr:"add_notation_extra_printing_rule"
- (str "No such Notation.")
-
-(**********************************************************************)
(* Synchronisation with reset *)
let freeze _ =
- (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
- !delimiters_map, !notations_key_table, !notation_rules,
- !scope_class_map)
+ (!scope_map, !scope_stack, !arguments_scope,
+ !delimiters_map, !notations_key_table, !scope_class_map)
-let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc) =
scope_map := scm;
- notation_level_map := nlm;
scope_stack := scs;
delimiters_map := dlm;
arguments_scope := asc;
notations_key_table := fkm;
- notation_rules := pprules;
scope_class_map := clsc
let init () =
init_scope_map ();
- notation_level_map := String.Map.empty;
delimiters_map := String.Map.empty;
notations_key_table := KeyMap.empty;
- notation_rules := String.Map.empty;
scope_class_map := initial_scope_class_map
let _ =
diff --git a/interp/notation.mli b/interp/notation.mli
index ccc67fe49..b177b7f1e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -14,7 +14,6 @@ open Libnames
open Constrexpr
open Glob_term
open Notation_term
-open Ppextend
(** Notations *)
@@ -32,8 +31,6 @@ val declare_scope : scope_name -> unit
val current_scopes : unit -> scopes
-val level_eq : level -> level -> bool
-
(** Check where a scope is opened or not in a scope list, or in
* the current opened scopes *)
val scope_is_open_in_scopes : scope_name -> scopes -> bool
@@ -135,11 +132,6 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
val availability_of_notation : scope_name option * notation -> local_scopes ->
(scope_name option * delimiters option) option
-(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
-
(** {6 Miscellaneous} *)
val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
@@ -200,21 +192,6 @@ val locate_notation : (glob_constr -> Pp.t) -> notation ->
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
-(** {6 Printing rules for notations} *)
-
-(** Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-val declare_notation_rule :
- notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
-
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
-
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b0480aa70..f208b23fb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -687,7 +687,7 @@ let is_onlybinding_meta id metas =
let is_onlybinding_pattern_like_meta isvar id metas =
try match Id.List.assoc id metas with
| _,NtnTypeBinder (NtnBinderParsedAsConstr
- (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ (AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
| _ -> false
with Not_found -> false
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 1a46746cc..52a6354a0 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -62,6 +62,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 constr_as_binder_kind =
+ | AsIdent
+ | AsIdentOrPattern
+ | AsStrictPattern
+
type notation_binder_source =
(* This accepts only pattern *)
(* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
@@ -69,7 +74,7 @@ type notation_binder_source =
(* This accepts only ident *)
| NtnParsedAsIdent
(* This accepts ident, or pattern, or both *)
- | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
+ | NtnBinderParsedAsConstr of constr_as_binder_kind
type notation_var_instance_type =
| NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
@@ -91,33 +96,3 @@ type notation_interp_env = {
ninterp_var_type : notation_var_internalization_type Id.Map.t;
ninterp_rec_vars : Id.t Id.Map.t;
}
-
-type grammar_constr_prod_item =
- | GramConstrTerminal of Tok.t
- | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
- | GramConstrListMark of int * bool * int
- (* tells action rule to make a list of the n previous parsed items;
- concat with last parsed list when true; additionally release
- the p last items as if they were parsed autonomously *)
-
-(** Dealing with precedences *)
-
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = precedence * tolerability list * Extend.constr_entry_key list
-
-(** Grammar rules for a notation *)
-
-type one_notation_grammar = {
- notgram_level : level;
- notgram_assoc : Extend.gram_assoc option;
- notgram_notation : Constrexpr.notation;
- notgram_prods : grammar_constr_prod_item list list;
-}
-
-type notation_grammar = {
- notgram_onlyprinting : bool;
- notgram_rules : one_notation_grammar list
-}
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 734b859f6..f2af594ef 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -31,11 +31,6 @@ 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 =
@@ -44,7 +39,7 @@ type 'a constr_entry_key_gen =
| ETBigint
| ETBinder of bool (* open list of binders if true, closed list of binders otherwise *)
| ETConstr of 'a
- | ETConstrAsBinder of constr_as_binder_kind * 'a
+ | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
| ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
| ETOther of string * string
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
new file mode 100644
index 000000000..346350641
--- /dev/null
+++ b/parsing/notation_gram.ml
@@ -0,0 +1,42 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Extend
+
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * constr_entry_key list
+
+type grammar_constr_prod_item =
+ | GramConstrTerminal of Tok.t
+ | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+ | GramConstrListMark of int * bool * int
+ (* tells action rule to make a list of the n previous parsed items;
+ concat with last parsed list when true; additionally release
+ the p last items as if they were parsed autonomously *)
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+ notgram_level : level;
+ notgram_assoc : Extend.gram_assoc option;
+ notgram_notation : Constrexpr.notation;
+ notgram_prods : grammar_constr_prod_item list list;
+}
+
+type notation_grammar = {
+ notgram_onlyprinting : bool;
+ notgram_rules : one_notation_grammar list
+}
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
new file mode 100644
index 000000000..071e6db20
--- /dev/null
+++ b/parsing/notgram_ops.ml
@@ -0,0 +1,65 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Extend
+open Notation_gram
+
+(* Uninterpreted notation levels *)
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+
+let declare_notation_level ?(onlyprint=false) ntn level =
+ if String.Map.mem ntn !notation_level_map then
+ anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
+ notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+ let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+ if onlyprint' && not onlyprint then raise Not_found;
+ level
+
+(**********************************************************************)
+(* Operations on scopes *)
+
+let parenRelation_eq t1 t2 = match t1, t2 with
+| L, L | E, E | Any, Any -> true
+| Prec l1, Prec l2 -> Int.equal l1 l2
+| _ -> false
+
+let production_level_eq l1 l2 = true (* (l1 = l2) *)
+
+let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| (NextLevel | NumLevel _), _ -> false *)
+
+let constr_entry_key_eq eq v1 v2 = match v1, v2 with
+| ETName, ETName -> true
+| ETReference, ETReference -> true
+| ETBigint, ETBigint -> true
+| ETBinder b1, ETBinder b2 -> b1 == b2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
+| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+
+let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+ let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
+ let prod_eq (l1,pp1) (l2,pp2) =
+ if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
+ else production_level_eq l1 l2 in
+ Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+ && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
diff --git a/interp/ppextend.ml b/parsing/notgram_ops.mli
index c75d9e12f..f427a607b 100644
--- a/interp/ppextend.ml
+++ b/parsing/notgram_ops.mli
@@ -8,36 +8,13 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Pp
-open Notation_term
+(* Merge with metasyntax? *)
+open Constrexpr
+open Notation_gram
-(*s Pretty-print. *)
+val level_eq : level -> level -> bool
-type ppbox =
- | PpHB of int
- | PpHOVB of int
- | PpHVB of int
- | PpVB of int
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-type ppcut =
- | PpBrk of int * int
- | PpFnl
-
-let ppcmd_of_box = function
- | PpHB n -> h n
- | PpHOVB n -> hov n
- | PpHVB n -> hv n
- | PpVB n -> v n
-
-let ppcmd_of_cut = function
- | PpFnl -> fnl ()
- | PpBrk(n1,n2) -> brk(n1,n2)
-
-type unparsing =
- | UnpMetaVar of int * parenRelation
- | UnpBinderMetaVar of int * parenRelation
- | UnpListMetaVar of int * parenRelation * unparsing list
- | UnpBinderListMetaVar of int * bool * unparsing list
- | UnpTerminal of string
- | UnpBox of ppbox * unparsing Loc.located list
- | UnpCut of ppcut
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index da4a0421b..2154f2f88 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,9 @@
Tok
CLexer
Extend
+Notation_gram
+Ppextend
+Notgram_ops
Pcoq
G_constr
G_prim
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
new file mode 100644
index 000000000..d2b50fa83
--- /dev/null
+++ b/parsing/ppextend.ml
@@ -0,0 +1,76 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+open Notation_gram
+
+(*s Pretty-print. *)
+
+type ppbox =
+ | PpHB of int
+ | PpHOVB of int
+ | PpHVB of int
+ | PpVB of int
+
+type ppcut =
+ | PpBrk of int * int
+ | PpFnl
+
+let ppcmd_of_box = function
+ | PpHB n -> h n
+ | PpHOVB n -> hov n
+ | PpHVB n -> hv n
+ | PpVB n -> v n
+
+let ppcmd_of_cut = function
+ | PpFnl -> fnl ()
+ | PpBrk(n1,n2) -> brk(n1,n2)
+
+type unparsing =
+ | UnpMetaVar of int * parenRelation
+ | UnpBinderMetaVar of int * parenRelation
+ | UnpListMetaVar of int * parenRelation * unparsing list
+ | UnpBinderListMetaVar of int * bool * unparsing list
+ | UnpTerminal of string
+ | UnpBox of ppbox * unparsing Loc.located list
+ | UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+(* Concrete syntax for symbolic-extension table *)
+let notation_rules =
+ Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+
+let declare_notation_rule ntn ~extra unpl gram =
+ notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+
+let find_notation_printing_rule ntn =
+ try pi1 (String.Map.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+let find_notation_extra_printing_rules ntn =
+ try pi2 (String.Map.find ntn !notation_rules)
+ with Not_found -> []
+let find_notation_parsing_rules ntn =
+ try pi3 (String.Map.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+
+let get_defined_notations () =
+ String.Set.elements @@ String.Map.domain !notation_rules
+
+let add_notation_extra_printing_rule ntn k v =
+ try
+ notation_rules :=
+ let p, pp, gr = String.Map.find ntn !notation_rules in
+ String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+ with Not_found ->
+ user_err ~hdr:"add_notation_extra_printing_rule"
+ (str "No such Notation.")
diff --git a/interp/ppextend.mli b/parsing/ppextend.mli
index c81058e72..9f61e121a 100644
--- a/interp/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -8,7 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Notation_term
+open Constrexpr
+open Notation_gram
(** {6 Pretty-print. } *)
@@ -26,6 +27,9 @@ val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
val ppcmd_of_cut : ppcut -> Pp.t
+(** {6 Printing rules for notations} *)
+
+(** Declare and look for the printing rule for symbolic notations *)
type unparsing =
| UnpMetaVar of int * parenRelation
| UnpBinderMetaVar of int * parenRelation
@@ -34,3 +38,15 @@ type unparsing =
| UnpTerminal of string
| UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+
+val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b83034..4e7c8b754 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,7 @@ END
let pr_by_arg_tac _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a4f090e..ff697e3c7 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -66,7 +66,7 @@ val wit_by_arg_tac :
Geninterp.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
- (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3dfe308a5..b29af6680 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
open Geninterp
open Stdarg
open Libnames
-open Notation_term
+open Notation_gram
open Misctypes
open Locus
open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 799a52cc8..5d2a99618 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,7 +17,7 @@ open Names
open Misctypes
open Environ
open Constrexpr
-open Notation_term
+open Notation_gram
open Tacexpr
type 'a grammar_tactic_prod_item_expr =
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
val ltop : tolerability
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
'a Genprint.top_printer
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 138b42e54..fbfbdb110 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -64,7 +64,7 @@ DECLARE PLUGIN "ssreflect_plugin"
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
-let tacltop = (5,Notation_term.E)
+let tacltop = (5,Notation_gram.E)
let pr_ssrtacarg _ _ prt = prt tacltop
ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 2ac7c7e26..7cd3751ce 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,11 +14,11 @@ open Ltac_plugin
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
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"]
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5f63d21c4..e7a308dda 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -8,14 +8,14 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open CErrors
open Util
-open Pcoq
+open CErrors
+open Names
+open Libnames
open Constrexpr
-open Notation_term
open Extend
-open Libnames
-open Names
+open Notation_gram
+open Pcoq
(**********************************************************************)
(* This determines (depending on the associativity of the current
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index e15add10f..b0341e6a1 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -15,5 +15,5 @@
(** {5 Adding notations} *)
-val extend_constr_grammar : Notation_term.one_notation_grammar -> unit
+val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 0964d46ac..dd8149d0a 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -1148,8 +1148,8 @@ GEXTEND Gram
[ [ "at"; n = level -> n ] ]
;
constr_as_binder_kind:
- [ [ "as"; IDENT "ident" -> AsIdent
- | "as"; IDENT "pattern" -> AsIdentOrPattern
- | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+ [ [ "as"; IDENT "ident" -> Notation_term.AsIdent
+ | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern
+ | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ]
;
END
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e038f54dd..2245e762f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -15,6 +15,7 @@ open Names
open Constrexpr
open Constrexpr_ops
open Notation_term
+open Notation_gram
open Notation_ops
open Ppextend
open Extend
@@ -709,7 +710,7 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec =
pr_level ntn prec ++ str ".")
type syntax_extension = {
- synext_level : Notation_term.level;
+ synext_level : Notation_gram.level;
synext_notation : notation;
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
@@ -728,8 +729,8 @@ let check_and_extend_constr_grammar ntn rule =
let ntn_for_grammar = rule.notgram_notation in
if String.equal ntn ntn_for_grammar then raise Not_found;
let prec = rule.notgram_level in
- let oldprec = Notation.level_of_notation ntn_for_grammar in
- if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+ let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+ if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
with Not_found ->
Egramcoq.extend_constr_grammar rule
@@ -738,16 +739,16 @@ let cache_one_syntax_extension se =
let prec = se.synext_level in
let onlyprint = se.synext_notgram.notgram_onlyprinting in
try
- let oldprec = Notation.level_of_notation ~onlyprint ntn in
- if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
+ let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
+ if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
with Not_found ->
if is_active_compat se.synext_compat then begin
(* Reserve the notation level *)
- Notation.declare_notation_level ntn prec ~onlyprint;
+ Notgram_ops.declare_notation_level ntn prec ~onlyprint;
(* Declare the parsing rule *)
if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
(* Declare the notation rule *)
- Notation.declare_notation_rule ntn
+ declare_notation_rule ntn
~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
end
@@ -1061,7 +1062,7 @@ let find_precedence lev etyps symbols onlyprint =
[],Option.get lev
let check_curly_brackets_notation_exists () =
- try let _ = Notation.level_of_notation "{ _ }" in ()
+ try let _ = Notgram_ops.level_of_notation "{ _ }" in ()
with Not_found ->
user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1274,10 +1275,10 @@ exception NoSyntaxRule
let recover_notation_syntax ntn =
try
- let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
- let pp_rule,_ = Notation.find_notation_printing_rule ntn in
- let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
- let pa_rule = Notation.find_notation_parsing_rules ntn in
+ let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
+ let pp_rule,_ = find_notation_printing_rule ntn in
+ let pp_extra_rules = find_notation_extra_printing_rules ntn in
+ let pa_rule = find_notation_parsing_rules ntn in
{ synext_level = prec;
synext_notation = ntn;
synext_notgram = pa_rule;
@@ -1444,7 +1445,7 @@ let add_notation_extra_printing_rule df k v =
let notk =
let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
make_notation_key symbs in
- Notation.add_notation_extra_printing_rule notk k v
+ add_notation_extra_printing_rule notk k v
(* Infix notations *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7e67e12cb..7aff758e9 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -102,7 +102,7 @@ open Pputils
| 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
+ let pr_constr_as_binder_kind = let open Notation_term in function
| AsIdent -> keyword "as ident"
| AsIdentOrPattern -> keyword "as pattern"
| AsStrictPattern -> keyword "as strict pattern"
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 4ff9d105b..74355e1a7 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -207,7 +207,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 option
+ | SetItemLevelAsBinder of string list * Notation_term.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