diff options
| author | Hugo Herbelin | 2018-12-12 14:07:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-12 14:07:12 +0100 |
| commit | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (patch) | |
| tree | 2e7d4477c2effb1975f7964e2a82a497b28cb3bc /interp/notation.mli | |
| parent | 84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff) | |
| parent | cac9811632834b0135f4408a32b4a2d391d09a0d (diff) | |
Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index ab0501a1e1..75034cad70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -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 @@ -128,20 +128,28 @@ type target_kind = | UInt of Names.inductive (* Coq.Init.Decimal.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) +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? *) |