From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Oct 2018 13:16:25 +0200 Subject: Replace type sign = bool with SPlus | SMinus --- interp/notation.ml | 49 ++++++++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 23 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 2765661749..2c8f5e3a96 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -476,7 +476,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type rawnum = Constrexpr.sign * Constrexpr.raw_natural_number type prim_token_uid = string @@ -499,13 +499,14 @@ module InnerPrimToken = struct | StringInterp f, StringInterp f' -> f == f' | _ -> false - let ofNumeral n s = - if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + let ofNumeral s n = match s with + | SPlus -> Bigint.of_string n + | SMinus -> Bigint.neg (Bigint.of_string n) let do_interp ?loc interp primtok = match primtok, interp with - | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s) - | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s) + | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n) + | Numeral (s,n), BigNumInterp interp -> interp ?loc (ofNumeral s n) | String s, StringInterp interp -> interp ?loc s | _ -> raise Not_found @@ -521,15 +522,15 @@ module InnerPrimToken = struct | _ -> false let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) - else Numeral (Bigint.to_string (Bigint.neg n), false) + if Bigint.is_pos_or_zero n then Numeral (SPlus,Bigint.to_string n) + else Numeral (SMinus,Bigint.to_string (Bigint.neg n)) let mkString = function | None -> None | Some s -> if Unicode.is_utf8 s then Some (String s) else None let do_uninterp uninterp g = match uninterp with - | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g) + | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g) | BigNumUninterp u -> Option.map mkNumeral (u g) | StringUninterp u -> mkString (u g) @@ -766,9 +767,10 @@ let coquint_of_rawnum uint str = in do_chars str (String.length str - 1) nil -let coqint_of_rawnum inds (str,sign) = +let coqint_of_rawnum inds (sign,str) = let uint = coquint_of_rawnum inds.uint str in - mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in + mkApp (mkConstruct (inds.int, pos_neg), [|uint|]) let rawnum_of_coquint c = let rec of_uint_loop c buf = @@ -794,8 +796,8 @@ let rawnum_of_coqint c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) - | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c') + | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c') | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken @@ -885,21 +887,22 @@ let bigint_of_int63 c = | _ -> raise NotAValidPrimToken let big2raw n = - if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) - else (Bigint.to_string (Bigint.neg n), false) + if Bigint.is_pos_or_zero n then (SPlus, Bigint.to_string n) + else (SMinus, Bigint.to_string (Bigint.neg n)) -let raw2big (n,s) = - if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) +let raw2big (s,n) = match s with + | SPlus -> Bigint.of_string n + | SMinus -> Bigint.neg (Bigint.of_string n) let interp o ?loc n = - begin match o.warning with - | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + begin match o.warning, n with + | Warning threshold, (SPlus, n) when rawnum_compare n threshold >= 0 -> warn_large_num o.ty_name | _ -> () end; let c = match fst o.to_kind with | Int int_ty -> coqint_of_rawnum int_ty n - | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt uint_ty when fst n == SPlus -> coquint_of_rawnum uint_ty (snd n) | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) | Int63 -> interp_int63 ?loc (raw2big n) @@ -909,7 +912,7 @@ let interp o ?loc n = let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in let to_ty = EConstr.Unsafe.to_constr to_ty in match o.warning, snd o.to_kind with - | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + | Abstract threshold, Direct when rawnum_compare (snd n) threshold >= 0 -> warn_abstract_large_num (o.ty_name,o.to_ty); glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> @@ -922,7 +925,7 @@ let uninterp o n = PrimTokenNotation.uninterp begin function | (Int _, c) -> rawnum_of_coqint c - | (UInt _, c) -> (rawnum_of_coquint c, true) + | (UInt _, c) -> (SPlus, rawnum_of_coquint c) | (Z _, c) -> big2raw (bigint_of_z c) | (Int63, c) -> big2raw (bigint_of_int63 c) end o n @@ -1249,8 +1252,8 @@ let find_notation ntn sc = (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral (n,true) -> InConstrEntrySomeLevel, n - | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n + | Numeral (SPlus,n) -> InConstrEntrySomeLevel, n + | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = -- cgit v1.2.3 From 4dc3d04d0812005f221e88744c587de8ef0f38ee Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 15:10:54 +0200 Subject: Rename raw_natural_number to raw_numeral In anticipation of an extension from natural numbers to other numeral constants. --- interp/notation.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 2c8f5e3a96..6cb95db364 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -476,7 +476,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_natural_number +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral type prim_token_uid = string @@ -560,8 +560,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 raw_numeral + | Abstract of raw_numeral type int_ty = { uint : Names.inductive; -- cgit v1.2.3 From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 14:40:23 +0200 Subject: 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. --- interp/notation.ml | 88 +++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 67 insertions(+), 21 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 6cb95db364..df8f6eb4f8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -506,9 +506,11 @@ module InnerPrimToken = struct let do_interp ?loc interp primtok = match primtok, interp with | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n) - | Numeral (s,n), BigNumInterp interp -> interp ?loc (ofNumeral s n) + | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }), + BigNumInterp interp -> interp ?loc (ofNumeral s n) | String s, StringInterp interp -> interp ?loc s - | _ -> raise Not_found + | (Numeral _ | String _), + (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found type uninterpreter = | RawNumUninterp of (any_glob_constr -> rawnum option) @@ -522,8 +524,10 @@ module InnerPrimToken = struct | _ -> false let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (SPlus,Bigint.to_string n) - else Numeral (SMinus,Bigint.to_string (Bigint.neg n)) + if Bigint.is_pos_or_zero n then + Numeral (SPlus,NumTok.int (Bigint.to_string n)) + else + Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg n))) let mkString = function | None -> None @@ -560,8 +564,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; @@ -571,11 +575,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 @@ -767,11 +776,24 @@ let coquint_of_rawnum uint str = in do_chars str (String.length str - 1) nil -let coqint_of_rawnum inds (sign,str) = +let coqint_of_rawnum inds sign str = let uint = coquint_of_rawnum inds.uint str in let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in mkApp (mkConstruct (inds.int, pos_neg), [|uint|]) +let coqdecimal_of_rawnum inds sign n = + let i, f, e = NumTok.(n.int, n.frac, n.exp) in + let i = coqint_of_rawnum inds.int sign i in + let f = coquint_of_rawnum inds.int.uint f in + if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) + else + let sign, e = match e.[1] with + | '-' -> SMinus, String.sub e 2 (String.length e - 2) + | '+' -> SPlus, String.sub e 2 (String.length e - 2) + | _ -> SPlus, String.sub e 1 (String.length e - 1) in + let e = coqint_of_rawnum inds.int sign e in + mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *) + let rawnum_of_coquint c = let rec of_uint_loop c buf = match Constr.kind c with @@ -790,7 +812,7 @@ let rawnum_of_coquint c = (* To avoid ambiguities between Nil and (D0 Nil), we choose to not display Nil alone as "0" *) raise NotAValidPrimToken - else Buffer.contents buf + else NumTok.int (Buffer.contents buf) let rawnum_of_coqint c = match Constr.kind c with @@ -801,6 +823,19 @@ let rawnum_of_coqint c = | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken +let rawnum_of_decimal c = + let of_ife i f e = + let sign, n = rawnum_of_coqint i in + let f = + try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in + let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with + | SPlus, e -> "e+" ^ e.NumTok.int + | SMinus, e -> "e-" ^ e.NumTok.int in + sign,{ n with NumTok.frac = f; exp = e } in + match Constr.kind c with + | App (_,[|i; f|]) -> of_ife i f None + | App (_,[|i; f; e|]) -> of_ife i f (Some e) + | _ -> raise NotAValidPrimToken (***********************************************************************) @@ -887,32 +922,42 @@ let bigint_of_int63 c = | _ -> raise NotAValidPrimToken let big2raw n = - if Bigint.is_pos_or_zero n then (SPlus, Bigint.to_string n) - else (SMinus, Bigint.to_string (Bigint.neg n)) + if Bigint.is_pos_or_zero n then + (SPlus, NumTok.int (Bigint.to_string n)) + else + (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n))) -let raw2big (s,n) = match s with +let raw2big s n = match s with | SPlus -> Bigint.of_string n | SMinus -> Bigint.neg (Bigint.of_string n) let interp o ?loc n = begin match o.warning, n with - | Warning threshold, (SPlus, n) when rawnum_compare n threshold >= 0 -> + | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) + when rawnum_compare n threshold >= 0 -> warn_large_num o.ty_name | _ -> () end; - let c = match fst o.to_kind with - | Int int_ty -> coqint_of_rawnum int_ty n - | UInt uint_ty when fst n == SPlus -> coquint_of_rawnum uint_ty (snd n) - | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name - | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) - | Int63 -> interp_int63 ?loc (raw2big n) + let c = match fst o.to_kind, n with + | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> + coqint_of_rawnum int_ty s n + | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) -> + coquint_of_rawnum uint_ty n + | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) -> + z_of_bigint z_pos_ty (raw2big s n) + | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) -> + interp_int63 ?loc (raw2big s n) + | (Int _ | UInt _ | Z _ | Int63), _ -> + no_such_prim_token "number" ?loc o.ty_name + | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n in let env = Global.env () in let sigma = Evd.from_env env in let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in let to_ty = EConstr.Unsafe.to_constr to_ty in match o.warning, snd o.to_kind with - | Abstract threshold, Direct when rawnum_compare (snd n) threshold >= 0 -> + | Abstract threshold, Direct + when rawnum_compare (snd n).NumTok.int threshold >= 0 -> warn_abstract_large_num (o.ty_name,o.to_ty); glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> @@ -928,6 +973,7 @@ let uninterp o n = | (UInt _, c) -> (SPlus, rawnum_of_coquint c) | (Z _, c) -> big2raw (bigint_of_z c) | (Int63, c) -> big2raw (bigint_of_int63 c) + | (Decimal _, c) -> rawnum_of_decimal c end o n end @@ -1252,8 +1298,8 @@ let find_notation ntn sc = (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral (SPlus,n) -> InConstrEntrySomeLevel, n - | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^n + | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n + | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = -- cgit v1.2.3 From ab2597acf4245cff82f31fae105a8103a4b46268 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 3 Feb 2019 21:19:56 +0100 Subject: Allow underscores as comments in numeral constants. The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)? --- interp/notation.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index df8f6eb4f8..b9aca82cf4 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -499,7 +499,9 @@ module InnerPrimToken = struct | StringInterp f, StringInterp f' -> f == f' | _ -> false - let ofNumeral s n = match s with + let ofNumeral s n = + let n = String.(concat "" (split_on_char '_' n)) in + match s with | SPlus -> Bigint.of_string n | SMinus -> Bigint.neg (Bigint.of_string n) @@ -770,7 +772,7 @@ let coquint_of_rawnum uint str = let nil = mkConstruct (uint,1) in let rec do_chars s i acc = if i < 0 then acc - else + else if s.[i] == '_' then do_chars s (i-1) acc else let dg = mkConstruct (uint, digit_of_char s.[i]) in do_chars s (i-1) (mkApp(dg,[|acc|])) in -- cgit v1.2.3