Quelle metasyntax.mli Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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 -> Globnames.extended_global_reference UserWarn.with_qf 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 *)

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.