diff options
| author | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-05 01:28:47 +0200 |
| commit | be6f3a6234ee809dd3c290621d80c3280a41355e (patch) | |
| tree | 8fed697f726193b765c8a2faeedd34ad60b541cb /interp/notation.mli | |
| parent | 2e1aa5c15ad524cffd03c7979992af44ab2bb715 (diff) | |
| parent | 6af420bb384af0acf94028fc44ef44fd5a6fd841 (diff) | |
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 5dcc96dc29..57e2be16b9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -70,14 +70,14 @@ 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 -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number + | 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 |