1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 Vernacexpr
open Notation
open Constrexpr
open Notation_term
open Environ
type notation_main_data
type syntax_rules
type notation_interpretation_decl
(** This data type packages all the necessary information to declare a notation
interpretation, once the syntax is declared or recovered from a previous
declaration. *)
val add_notation_syntax :
local:bool ->
infix:bool ->
UserWarn.t option ->
notation_declaration ->
notation_interpretation_decl
(** Add syntax rules for a (constr) notation in the environment *)
val add_notation_interpretation :
local:bool -> env -> notation_interpretation_decl -> unit
(** Declare the interpretation of a notation *)
(** Declaring scopes, delimiter keys and default scopes *)
val declare_scope : locality_flag -> scope_name -> unit
val add_delimiters : locality_flag -> scope_name -> string -> unit
val remove_delimiters : locality_flag -> scope_name -> unit
val add_class_scope : locality_flag -> scope_name -> add_scope_where option -> scope_class list -> unit
(** Scope opening *)
val open_close_scope : locality_flag -> to_open:bool -> scope_name -> unit
(** Add a notation interpretation associated to a "where" clause (already has pa/pp rules) *)
val prepare_where_notation :
notation_declaration -> notation_interpretation_decl
(** Interpret the modifiers of a where-notation *)
val set_notation_for_interpretation :
env -> Constrintern.internalization_env -> notation_interpretation_decl -> unit
(** Set the interpretation of the where-notation for interpreting a mutual block *)
(** Add only the parsing/printing rule of a notation *)
val add_reserved_notation :
local:bool -> infix:bool -> (lstring * syntax_modifier CAst.t list) -> unit
(** Add a syntactic definition (as in "Notation f := ...") *)
val add_abbreviation : local:bool -> UserWarn.t option -> env ->
Id.t -> Id.t list * constr_expr -> syntax_modifier CAst.t list -> unit
(** Print the Camlp5 state of a grammar *)
val pr_grammar : string list -> Pp.t
val pr_custom_grammar : string -> Pp.t
val pr_keywords : unit -> Pp.t
val with_syntax_protection : ('a -> 'b) -> 'a -> 'b
val declare_notation_toggle : locality_flag -> on:bool -> all:bool -> Notation.notation_query_pattern -> unit
val declare_custom_entry : locality_flag -> string -> unit
(** Declare given string as a custom grammar entry *)
val check_custom_entry : string -> unit
(** Check that the given string is a valid custom entry that has been declared *)
val pr_level : Constrexpr.notation -> Notationextern.level -> Extend.constr_entry_key list -> Pp.t
(** Pretty print level information of a notation and all of its arguments *)
|
