diff options
| author | Pierre Roux | 2018-10-20 14:40:23 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:21 +0200 |
| commit | 552bb5aba750785d8f19aa7b333baa59e9199369 (patch) | |
| tree | df349e57ff8c34e2da48d8c786d2466426822511 /interp/notation.mli | |
| parent | 4dc3d04d0812005f221e88744c587de8ef0f38ee (diff) | |
Add parsing of decimal constants (e.g., 1.02e+01)
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 5423655229..57e2be16b9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -70,10 +70,10 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name (** {6 Declare and uses back and forth an interpretation of primitive token } *) -(** A numeral interpreter is the pair of an interpreter for **integer** +(** A numeral interpreter is the pair of an interpreter for **decimal** numbers in terms and an optional interpreter in pattern, if - negative numbers are not supported, the interpreter must fail with - an appropriate error message *) + non integer or negative numbers are not supported, the interpreter + must fail with an appropriate error message *) type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list @@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_numeral - | Abstract of raw_numeral + | Warning of string + | Abstract of string type int_ty = { uint : Names.inductive; @@ -123,11 +123,16 @@ type z_pos_ty = { z_ty : Names.inductive; pos_ty : Names.inductive } +type decimal_ty = + { int : int_ty; + decimal : Names.inductive } + 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 *) + | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *) type string_target_kind = | ListByte |