diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 53 |
1 files changed, 40 insertions, 13 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 734198bbf6..5dcc96dc29 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool (** Open scope *) val open_close_scope : - (** locality *) bool * (* open *) bool * scope_name -> unit + (* locality *) bool * (* open *) bool * scope_name -> unit (** Extend a list of scopes *) val empty_scope_stack : scopes @@ -104,11 +104,11 @@ val register_string_interpretation : (** * Numeral notation *) -type numeral_notation_error = +type prim_token_notation_error = | UnexpectedTerm of Constr.t | UnexpectedNonOptionTerm of Constr.t -exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error +exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error type numnot_option = | Nop @@ -127,21 +127,30 @@ type target_kind = | Int of int_ty (* Coq.Init.Decimal.int + uint *) | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + +type string_target_kind = + | ListByte + | Byte type option_kind = Option | Direct -type conversion_kind = target_kind * option_kind +type 'target conversion_kind = 'target * option_kind -type numeral_notation_obj = - { to_kind : conversion_kind; +type ('target, 'warning) prim_token_notation_obj = + { to_kind : 'target conversion_kind; to_ty : GlobRef.t; - of_kind : conversion_kind; + of_kind : 'target conversion_kind; of_ty : GlobRef.t; - num_ty : Libnames.qualid; (* for warnings / error messages *) - warning : numnot_option } + ty_name : Libnames.qualid; (* for warnings / error messages *) + warning : 'warning } + +type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj +type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj type prim_token_interp_info = Uid of prim_token_uid | NumeralNotation of numeral_notation_obj + | StringNotation of string_notation_obj type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) @@ -202,6 +211,8 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t +module InterpRuleSet : Set.S with type elt = interp_rule + val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit @@ -211,18 +222,28 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_rule_core = + interp_rule (* kind of notation *) + * interpretation (* pattern associated to the notation *) + * int option (* number of expected arguments *) + +type notation_rule = + notation_rule_core + * delimiters option (* delimiter to possibly add *) + * bool (* true if the delimiter is mandatory *) (** Return the possible notations for a given term *) -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 +val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option + *) (** {6 Miscellaneous} *) @@ -233,6 +254,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool +(** Checks for already existing notations *) +val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool + (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit @@ -297,3 +321,6 @@ val entry_has_ident : notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b + +(** Conversion from bigint to int63 *) +val int63_of_pos_bigint : Bigint.bigint -> Uint63.t |