diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 80 |
1 files changed, 45 insertions, 35 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 2e92a00a..18671feb 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 Bigint open Names open Libnames @@ -22,7 +23,6 @@ open Ppextend (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) -type level = precedence * tolerability list type delimiters = string type scope type scopes (** = [scope_name list] *) @@ -55,7 +55,7 @@ val find_scope : scope_name -> scope val declare_delimiters : scope_name -> delimiters -> unit val remove_delimiters : scope_name -> unit -val find_delimiters_scope : Loc.t -> delimiters -> scope_name +val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) @@ -69,10 +69,15 @@ type required_module = full_path * string list type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - Loc.t -> 'a -> glob_constr + ?loc:Loc.t -> 'a -> glob_constr type 'a prim_token_uninterpreter = - glob_constr list * (glob_constr -> 'a option) * cases_pattern_status + glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status + +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + +val declare_rawnumeral_interpreter : scope_name -> required_module -> + rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit val declare_numeral_interpreter : scope_name -> required_module -> bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit @@ -83,18 +88,19 @@ val declare_string_interpreter : scope_name -> required_module -> (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -val interp_prim_token : Loc.t -> prim_token -> local_scopes -> +val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token -> - local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option) +(* This function returns a glob_const representing a pattern *) +val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token -> + local_scopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) val uninterp_prim_token : - glob_constr -> scope_name * prim_token + 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : - cases_pattern -> Name.t * scope_name * prim_token + 'a cases_pattern_g -> Name.t * scope_name * prim_token val uninterp_prim_token_ind_pattern : inductive -> cases_pattern list -> scope_name * prim_token @@ -106,7 +112,7 @@ val availability_of_prim_token : (** Binds a notation in a given scope to an interpretation *) type interp_rule = | NotationRule of scope_name option * notation - | SynDefRule of kernel_name + | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit @@ -114,14 +120,14 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit (** Return the interpretation bound to a notation *) -val interp_notation : Loc.t -> notation -> local_scopes -> +val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : glob_constr -> notation_rule list -val uninterp_cases_pattern_notations : cases_pattern -> notation_rule list +val uninterp_notations : 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes @@ -132,17 +138,17 @@ val availability_of_notation : scope_name option * notation -> local_scopes -> (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) +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.t -> (global_reference -> bool) -> +val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) -> notation -> delimiters option -> global_reference (** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> - interpretation -> bool + bool -> interpretation -> bool (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : @@ -159,10 +165,10 @@ val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit -val declare_ref_arguments_scope : global_reference -> unit +val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit -val compute_arguments_scope : Term.types -> scope_name option list -val compute_type_scope : Term.types -> scope_name option +val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list +val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option @@ -172,24 +178,28 @@ val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) type symbol = - | Terminal of string - | NonTerminal of Id.t - | SProdList of Id.t * symbol list - | Break of int + | Terminal of string (* an expression including symbols or a simply-quoted ident, e.g. "'U'" or "!" *) + | NonTerminal of Id.t (* an identifier "x" *) + | SProdList of Id.t * symbol list (* an expression "x sep .. sep y", remembering x (or y) and sep *) + | Break of int (* a sequence of blanks > 1, e.g. " " *) val symbol_eq : symbol -> symbol -> bool +(** Make/decompose a notation of the form "_ U _" *) val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list +(** Decompose a notation of the form "a 'U' b" *) +val decompose_raw_notation : string -> symbol list + (** Prints scopes (expects a pure aconstr printer) *) -val pr_scope_class : scope_class -> std_ppcmds -val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds -val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds -val locate_notation : (glob_constr -> std_ppcmds) -> notation -> - scope_name option -> std_ppcmds +val pr_scope_class : scope_class -> Pp.t +val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t +val pr_scopes : (glob_constr -> Pp.t) -> Pp.t +val locate_notation : (glob_constr -> Pp.t) -> notation -> + scope_name option -> Pp.t -val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds +val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t (** {6 Printing rules for notations} *) |