From 08189431706298d599cffea2e41dd51290305ba3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jan 2020 13:36:34 +0100 Subject: Centralizing all kinds of numeral string management in numTok.ml. Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him. --- interp/constrexpr.ml | 20 +--- interp/constrexpr_ops.ml | 5 +- interp/constrextern.ml | 29 ++--- interp/constrintern.ml | 11 +- interp/notation.ml | 140 ++++++++--------------- interp/notation.mli | 6 +- interp/numTok.ml | 287 ++++++++++++++++++++++++++++++++++++++--------- interp/numTok.mli | 130 ++++++++++++++++++--- 8 files changed, 420 insertions(+), 208 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 8732b0e2c6..21f682ac0e 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -57,26 +57,8 @@ type abstraction_kind = AbsLambda | AbsPi type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) -(** Representation of decimal literals that appear in Coq scripts. - We now use raw strings following the format defined by - [NumTok.t] and a separate sign flag. - - Note that this representation is not unique, due to possible - multiple leading or trailing zeros, and -0 = +0, for instances. - The reason to keep the numeral exactly as it was parsed is that - specific notations can be declared for specific numerals - (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or - [Notation "2e1" := ...]). Those notations, which override the - generic interpretation as numeral, use the same representation of - numeral using the Numeral constructor. So the latter should be able - to record the form of the numeral which exactly matches the - notation. *) - -type sign = SPlus | SMinus -type raw_numeral = NumTok.t - type prim_token = - | Numeral of sign * raw_numeral + | Numeral of NumTok.Signed.t | String of string type instance_expr = Glob_term.glob_level list diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index da5b8d9132..d4369e9bd1 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -48,10 +48,9 @@ let names_of_local_binders bl = are considered different here. *) let prim_token_eq t1 t2 = match t1, t2 with -| Numeral (SPlus,n1), Numeral (SPlus,n2) -| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2 +| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2 | String s1, String s2 -> String.equal s1 s2 -| (Numeral ((SPlus|SMinus),_) | String _), _ -> false +| (Numeral _ | String _), _ -> false let explicitation_eq ex1 ex2 = match ex1, ex2 with | ExplByPos (i1, id1), ExplByPos (i2, id2) -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a16825b5c9..7a14ca3e48 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -354,27 +354,21 @@ let drop_implicits_in_patt cst nb_expl args = let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None -let is_zero s = - let rec aux i = - Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) - in aux 0 -let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac - let make_notation_gen loc ntn mknot mkprim destprim l bl = match snd ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) - | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) -> + | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) -> assert (bl=[]); mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[]) | _ -> match decompose_notation_key ntn, l with | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] -> - begin match NumTok.of_string x with - | Some n -> mkprim (loc, Numeral (SMinus,n)) + begin match NumTok.Unsigned.parse_string x with + | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n)) | None -> mknot (loc,ntn,l,bl) end | (InConstrEntrySomeLevel,[Terminal x]), [] -> - begin match NumTok.of_string x with - | Some n -> mkprim (loc, Numeral (SPlus,n)) + begin match NumTok.Unsigned.parse_string x with + | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n)) | None -> mknot (loc,ntn,l,bl) end | _ -> mknot (loc,ntn,l,bl) @@ -899,13 +893,10 @@ let extern_float f scopes = else if Float64.is_infinity f then CRef(q_infinity (), None) else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None) else - let sign = if Float64.sign f then SMinus else SPlus in - let s = Float64.(to_string (abs f)) in - match NumTok.of_string s with - | None -> assert false - | Some n -> - extern_prim_token_delimiter_if_required (Numeral (sign, n)) - "float" "float_scope" scopes + let s = Float64.(to_string f) in + let n = NumTok.Signed.of_string s in + extern_prim_token_delimiter_if_required (Numeral n) + "float" "float_scope" scopes (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -1085,7 +1076,7 @@ let rec extern inctx ?impargs scopes vars r = | GInt i -> extern_prim_token_delimiter_if_required - (Numeral (SPlus, NumTok.int (Uint63.to_string i))) + (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i))) "int63" "int63_scope" (snd scopes) | GFloat f -> extern_float f (snd scopes) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index abacadc43a..a071ba7ec9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -32,6 +32,7 @@ open Notation_ops open Notation open Inductiveops open Context.Rel.Declaration +open NumTok (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -1585,12 +1586,6 @@ let alias_of als = match als.alias_ids with *) -let is_zero s = - let rec aux i = - Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1)) - in aux 0 -let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac - let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1614,11 +1609,11 @@ let rec subst_pat_iterator y t = DAst.(map (function | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) let is_non_zero c = match c with -| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let is_non_zero_pat c = match c with -| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p) +| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p) | _ -> false let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref diff --git a/interp/notation.ml b/interp/notation.ml index 4b73189ad3..6291a88bb0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -21,6 +21,7 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration +open NumTok (*i*) @@ -335,7 +336,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_numeral +type rawnum = NumTok.Signed.t type prim_token_uid = string @@ -358,17 +359,13 @@ module InnerPrimToken = struct | StringInterp f, StringInterp f' -> f == f' | _ -> false - 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) - let do_interp ?loc interp primtok = match primtok, interp with - | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n) - | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }), - BigNumInterp interp -> interp ?loc (ofNumeral s n) + | Numeral n, RawNumInterp interp -> interp ?loc n + | Numeral n, BigNumInterp interp -> + (match NumTok.Signed.to_bigint n with + | Some n -> interp ?loc n + | None -> raise Not_found) | String s, StringInterp interp -> interp ?loc s | (Numeral _ | String _), (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found @@ -385,10 +382,7 @@ module InnerPrimToken = struct | _ -> false let mkNumeral 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))) + Numeral (NumTok.Signed.of_bigint n) let mkString = function | None -> None @@ -425,8 +419,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; @@ -567,7 +561,7 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) = Some (to_raw (fst o.of_kind, c)) with | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) - | NotAValidPrimToken -> None (* all other functions except big2raw *) + | NotAValidPrimToken -> None (* all other functions except NumTok.Signed.of_bigint *) end @@ -600,26 +594,6 @@ let warn_abstract_large_num = pr_qualid ty ++ strbrk " are interpreted as applications of " ++ Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") -(** Comparing two raw numbers (base 10, big-endian, non-negative). - A bit nasty, but not critical: only used to decide when a - number is considered as large (see warnings above). *) - -exception Comp of int - -let rec rawnum_compare s s' = - let l = String.length s and l' = String.length s' in - if l < l' then - rawnum_compare s' s - else - let d = l-l' in - try - for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; - for i = d to l-1 do - let c = pervasives_compare s.[i] s'.[i-d] in - if c != 0 then raise (Comp c) - done; - 0 - with Comp c -> c - (***********************************************************************) (** ** Conversion between Coq [Decimal.int] and internal raw string *) @@ -634,32 +608,31 @@ let char_of_digit n = assert (2<=n && n<=11); Char.chr (n-2 + Char.code '0') -let coquint_of_rawnum uint str = +let coquint_of_rawnum uint n = let nil = mkConstruct (uint,1) in + match n with None -> nil | Some n -> + let str = NumTok.UnsignedNat.to_string n in let rec do_chars s i acc = if i < 0 then acc - else if s.[i] == '_' then do_chars s (i-1) acc else + else let dg = mkConstruct (uint, digit_of_char s.[i]) in do_chars s (i-1) (mkApp(dg,[|acc|])) in do_chars str (String.length str - 1) nil -let coqint_of_rawnum inds sign str = - let uint = coquint_of_rawnum inds.uint str in +let coqint_of_rawnum inds (sign,n) = + let uint = coquint_of_rawnum inds.uint (Some n) 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 coqdecimal_of_rawnum inds n = + let i, f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = coqint_of_rawnum inds.int 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 + match e with + | None -> mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *) + | Some e -> + let e = coqint_of_rawnum inds.int e in mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *) let rawnum_of_coquint c = @@ -680,26 +653,23 @@ 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 NumTok.int (Buffer.contents buf) + else NumTok.UnsignedNat.of_string (Buffer.contents buf) let rawnum_of_coqint c = match Constr.kind c with | App (c,[|c'|]) -> (match Constr.kind c with - | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c') - | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c') + | Construct ((_,1), _) (* Pos *) -> (SPlus,rawnum_of_coquint c') + | Construct ((_,2), _) (* Neg *) -> (SMinus,rawnum_of_coquint 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 + let n = rawnum_of_coqint i in + let f = try Some (rawnum_of_coquint f) with NotAValidPrimToken -> None in + let e = match e with None -> None | Some e -> Some (rawnum_of_coqint e) in + NumTok.Signed.of_decimal_and_exponent n f 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) @@ -789,43 +759,31 @@ let bigint_of_int63 c = | Int i -> Bigint.of_string (Uint63.to_string i) | _ -> raise NotAValidPrimToken -let big2raw 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 - | 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, { NumTok.int = n; frac = ""; exp = "" }) - when rawnum_compare n threshold >= 0 -> + | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> warn_large_num o.ty_name | _ -> () end; - 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) + let c = match fst o.to_kind, NumTok.Signed.to_int n with + | Int int_ty, Some n -> + coqint_of_rawnum int_ty n + | UInt uint_ty, Some (SPlus, n) -> + coquint_of_rawnum uint_ty (Some n) + | Z z_pos_ty, Some n -> + z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) + | Int63, Some n -> + interp_int63 ?loc (NumTok.SignedNat.to_bigint 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 + | Decimal decimal_ty, _ -> coqdecimal_of_rawnum decimal_ty 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).NumTok.int threshold >= 0 -> + | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold -> warn_abstract_large_num (o.ty_name,o.to_ty); glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|])) | _ -> @@ -837,10 +795,10 @@ let interp o ?loc n = let uninterp o n = PrimTokenNotation.uninterp begin function - | (Int _, c) -> rawnum_of_coqint c - | (UInt _, c) -> (SPlus, rawnum_of_coquint c) - | (Z _, c) -> big2raw (bigint_of_z c) - | (Int63, c) -> big2raw (bigint_of_int63 c) + | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) + | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) + | (Z _, c) -> NumTok.Signed.of_bigint (bigint_of_z c) + | (Int63, c) -> NumTok.Signed.of_bigint (bigint_of_int63 c) | (Decimal _, c) -> rawnum_of_decimal c end o n end @@ -1162,8 +1120,8 @@ let find_notation ntn sc = NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function - | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n - | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n + | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n + | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = diff --git a/interp/notation.mli b/interp/notation.mli index 8fcf9dc5dc..892eba8d11 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -81,7 +81,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_numeral +type rawnum = NumTok.Signed.t (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -116,8 +116,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; diff --git a/interp/numTok.ml b/interp/numTok.ml index c11acdc8bd..0d0f17f358 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -8,55 +8,238 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type t = { - int : string; - frac : string; - exp : string -} - -let equal n1 n2 = - String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp) - -let int s = { int = s; frac = ""; exp = "" } - -let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp - -let parse = - let buff = ref (Bytes.create 80) in - let store len x = - let open Bytes in - if len >= length !buff then - buff := cat !buff (create (length !buff)); - set !buff len x; - succ len in - let get_buff len = Bytes.sub_string !buff 0 len in - (* reads [0-9_]* *) - let rec number len s = match Stream.peek s with - | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s - | _ -> len in - fun s -> - let i = get_buff (number 0 s) in - let f = - match Stream.npeek 2 s with - | '.' :: (('0'..'9' | '_') as c) :: _ -> - Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) - | _ -> "" in - let e = - match (Stream.npeek 2 s) with - | (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> - Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) - | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> - begin match Stream.npeek 3 s with - | _ :: _ :: ('0'..'9' as c) :: _ -> - Stream.junk s; Stream.junk s; Stream.junk s; - get_buff (number (store (store (store 0 e) sign) c) s) - | _ -> "" - end - | _ -> "" in - { int = i; frac = f; exp = e } - -let of_string s = - if s = "" || s.[0] < '0' || s.[0] > '9' then None else - let strm = Stream.of_string (s ^ " ") in - let n = parse strm in - if Stream.count strm >= String.length s then Some n else None +(** We keep the string to preserve the user representation, + e.g. "e"/"E" or the presence of leading 0s, or the presence of a + + in the exponent *) + +module UnsignedNat = +struct + type t = string + let of_string s = + assert (String.length s > 0); + assert (s.[0] <> '-'); + s + let to_string s = + String.(concat "" (split_on_char '_' s)) + + let sprint s = s + let print s = Pp.str (sprint s) + + (** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: used e.g. to decide when a number + is considered as large (see threshold warnings in notation.ml). *) + + exception Comp of int + + let rec compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Util.pervasives_compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + + let is_zero s = + compare s "0" = 0 +end + +type sign = SPlus | SMinus + +module SignedNat = +struct + type t = sign * UnsignedNat.t + let of_string n = + let sign,n = + if String.length n > 0 && n.[0] = '-' + then (SMinus,String.sub n 1 (String.length n - 1)) + else (SPlus,n) in + (sign,UnsignedNat.of_string n) + let to_string (s,n) = + (match s with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n + let to_bigint s = Bigint.of_string (to_string s) + let of_bigint n = + let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in + (sign, Bigint.to_string n) +end + +module Unsigned = +struct + + type t = { + int : string; (** \[0-9\]\[0-9_\]* *) + frac : string; (** empty or \[0-9_\]+ *) + exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + } + + let equal n1 n2 = + String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp) + + let parse = + let buff = ref (Bytes.create 80) in + let store len x = + let open Bytes in + if len >= length !buff then + buff := cat !buff (create (length !buff)); + set !buff len x; + succ len in + let get_buff len = Bytes.sub_string !buff 0 len in + (* reads [0-9_]* *) + let rec number len s = match Stream.peek s with + | Some ('0'..'9' as c) -> Stream.junk s; number (store len c) s + | Some ('_' as c) when len > 0 -> Stream.junk s; number (store len c) s + | _ -> len in + fun s -> + let i = get_buff (number 0 s) in + assert (i <> ""); + let f = + match Stream.npeek 2 s with + | '.' :: (('0'..'9' | '_') as c) :: _ -> + Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s) + | _ -> "" in + let e = + match (Stream.npeek 2 s) with + | (('e'|'E') as e) :: ('0'..'9' as c) :: _ -> + Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s) + | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ -> + begin match Stream.npeek 3 s with + | _ :: _ :: ('0'..'9' as c) :: _ -> + Stream.junk s; Stream.junk s; Stream.junk s; + get_buff (number (store (store (store 0 e) sign) c) s) + | _ -> "" + end + | _ -> "" in + { int = i; frac = f; exp = e } + + let sprint n = + n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp + + let print n = + Pp.str (sprint n) + + let parse_string s = + if s = "" || s.[0] < '0' || s.[0] > '9' then None else + let strm = Stream.of_string (s ^ " ") in + let n = parse strm in + if Stream.count strm >= String.length s then Some n else None + + let of_string s = + match parse_string s with + | None -> assert false + | Some s -> s + + let to_string = + sprint (* We could remove the '_' but not necessary for float_of_string *) + + let to_nat = function + | { int = i; frac = ""; exp = "" } -> Some i + | _ -> None + + let is_nat = function + | { int = _; frac = ""; exp = "" } -> true + | _ -> false + +end + +open Unsigned + +module Signed = +struct + + type t = sign * Unsigned.t + + let equal (s1,n1) (s2,n2) = + s1 = s2 && equal n1 n2 + + let is_zero = function + | (SPlus,{int;frac;exp}) -> UnsignedNat.is_zero int && UnsignedNat.is_zero frac + | _ -> false + + let of_decimal_and_exponent (sign,int) f e = + let exp = match e with Some e -> "e" ^ SignedNat.to_string e | None -> "" in + let frac = match f with Some f -> UnsignedNat.to_string f | None -> "" in + sign, { int; frac; exp } + + let to_decimal_and_exponent (sign, { int; frac; exp }) = + let e = + if exp = "" then None else + Some (match exp.[1] with + | '-' -> SMinus, String.sub exp 2 (String.length exp - 2) + | '+' -> SPlus, String.sub exp 2 (String.length exp - 2) + | _ -> SPlus, String.sub exp 1 (String.length exp - 1)) in + let f = if frac = "" then None else Some frac in + (sign, int), f, e + + let of_nat i = + (SPlus,{ int = i; frac = ""; exp = "" }) + + let of_int (s,i) = + (s,{ int = i; frac = ""; exp = "" }) + + let of_int_string s = of_int (SignedNat.of_string s) + + let to_int = function + | (s, { int = i; frac = ""; exp = "" }) -> Some (s,i) + | _ -> None + + let is_int n = match to_int n with None -> false | Some _ -> true + + let sprint (s,i) = + (match s with SPlus -> "" | SMinus -> "-") ^ Unsigned.sprint i + + let print i = + Pp.str (sprint i) + + let parse_string s = + if s = "" || s = "-" || + (s.[0] < '0' || s.[0] > '9') && (s.[0] <> '-' || s.[1] < '0' || s.[1] > '9') then None else + let strm = Stream.of_string (s ^ " ") in + let sign = if s.[0] = '-' then (Stream.junk strm; SMinus) else SPlus in + let n = parse strm in + if Stream.count strm >= String.length s then Some (sign,n) else None + + let of_string s = + assert (s <> ""); + let sign,u = match s.[0] with + | '-' -> (SMinus, String.sub s 1 (String.length s - 1)) + | '+' -> (SPlus, String.sub s 1 (String.length s - 1)) + | _ -> (SPlus, s) in + (sign, Unsigned.of_string u) + + let to_string (sign,u) = + (match sign with SPlus -> "" | SMinus -> "-") ^ Unsigned.to_string u + + let to_bigint = function + | (sign, { int = n; frac = ""; exp = "" }) -> + Some (SignedNat.to_bigint (sign,UnsignedNat.to_string n)) + | _ -> None + + let of_bigint n = + let sign, int = SignedNat.of_bigint n in + (sign, { int; frac = ""; exp = "" }) + + let to_bigint_and_exponent (s, { int; frac; exp }) = + let s = match s with SPlus -> "" | SMinus -> "-" in + let int = UnsignedNat.to_string int in + let frac = UnsignedNat.to_string frac in + let i = Bigint.of_string (s ^ int ^ frac) in + let e = + let e = if exp = "" then Bigint.zero else match exp.[1] with + | '+' -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2))) + | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (String.sub exp 2 (String.length exp - 2))))) + | _ -> Bigint.of_string (UnsignedNat.to_string (String.sub exp 1 (String.length exp - 1))) in + Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' frac))))) in + (i,e) + + let of_bigint_and_exponent i e = + of_decimal_and_exponent (SignedNat.of_bigint i) None (Some (SignedNat.of_bigint e)) + + let is_bigger_int_than (s, { int; frac; exp }) i = + frac = "" && exp = "" && UnsignedNat.compare int i >= 0 + +end diff --git a/interp/numTok.mli b/interp/numTok.mli index 141f1be889..ea289df237 100644 --- a/interp/numTok.mli +++ b/interp/numTok.mli @@ -8,21 +8,125 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -type t = { - int : string; (** \[0-9\]\[0-9_\]* *) - frac : string; (** empty or \[0-9_\]+ *) - exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) -} +(** Numerals in different forms: signed or unsigned, possibly with + fractional part and exponent. -val equal : t -> t -> bool + Numerals are represented using raw strings of decimal + literals and a separate sign flag. -(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *) -val int : string -> t + Note that this representation is not unique, due to possible + multiple leading or trailing zeros, and -0 = +0, for instances. + The reason to keep the numeral exactly as it was parsed is that + specific notations can be declared for specific numerals + (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or + [Notation "2e1" := ...]). Those notations override the generic + interpretation as numeral. So, one has to record the form of the + numeral which exactly matches the notation. *) -val to_string : t -> string +type sign = SPlus | SMinus -val of_string : string -> t option +(** {6 String representation of a natural number } *) -(** Precondition: the first char on the stream is a digit (\[0-9\]). - Precondition: at least two extra chars after the numeral to parse. *) -val parse : char Stream.t -> t +module UnsignedNat : +sig + type t + val of_string : string -> t + (** Convert from a non-empty sequence of digits (which may contain "_") *) + + val to_string : t -> string + (** Convert to a non-empty sequence of digit that does not contain "_" *) + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val compare : t -> t -> int +end + +(** {6 String representation of a signed natural number } *) + +module SignedNat : +sig + type t = sign * UnsignedNat.t + val of_string : string -> t + (** Convert from a non-empty sequence of digits which may contain "_" *) + + val to_string : t -> string + (** Convert to a non-empty sequence of digit that does not contain "_" *) + + val to_bigint : t -> Bigint.bigint + val of_bigint : Bigint.bigint -> t +end + +(** {6 Unsigned decimal numerals } *) + +module Unsigned : +sig + type t + val equal : t -> t -> bool + val is_nat : t -> bool + val to_nat : t -> string option + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val parse : char Stream.t -> t + (** Parse a positive Coq numeral. + Precondition: the first char on the stream is already known to be a digit (\[0-9\]). + Precondition: at least two extra chars after the numeral to parse. + + The recognized syntax is: + - integer part: \[0-9\]\[0-9_\]* + - decimal part: empty or .\[0-9_\]+ + - exponent part: empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) + + val parse_string : string -> t option + (** Parse the string as a positive Coq numeral, if possible *) + +end + +(** {6 Signed decimal numerals } *) + +module Signed : +sig + type t = sign * Unsigned.t + val equal : t -> t -> bool + val is_zero : t -> bool + val of_nat : UnsignedNat.t -> t + val of_int : SignedNat.t -> t + val to_int : t -> SignedNat.t option + val is_int : t -> bool + + val sprint : t -> string + val print : t -> Pp.t + (** [sprint] and [print] returns the numeral as it was parsed, for printing *) + + val parse_string : string -> t option + (** Parse the string as a signed Coq numeral, if possible *) + + val of_int_string : string -> t + (** Convert from a string in the syntax of OCaml's int/int64 *) + + val of_string : string -> t + (** Convert from a string in the syntax of OCaml's string_of_float *) + + val to_string : t -> string + (** Returns a string in the syntax of OCaml's float_of_string *) + + val of_bigint : Bigint.bigint -> t + val to_bigint : t -> Bigint.bigint option + (** Convert from and to bigint when the denotation of a bigint *) + + val of_decimal_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t + val to_decimal_and_exponent : t -> SignedNat.t * UnsignedNat.t option * SignedNat.t option + (** n, p and q such that the number is n.p*10^q *) + + val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint + val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint -> t + (** n and p such that the number is n*10^p *) + + val is_bigger_int_than : t -> UnsignedNat.t -> bool + (** Test if an integer whose absolute value is bounded *) + +end -- cgit v1.2.3 From f7687371270e0b3fd3b61db3f25128c567aa7033 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Mar 2020 21:09:22 +0100 Subject: Adding support for parsing "+" sig in NumTok. Support in the parser needs yet to be added though. --- interp/numTok.ml | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) (limited to 'interp') diff --git a/interp/numTok.ml b/interp/numTok.ml index 0d0f17f358..e254e9e972 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -17,7 +17,7 @@ struct type t = string let of_string s = assert (String.length s > 0); - assert (s.[0] <> '-'); + assert (s.[0] >= '0' && s.[0] <= '9'); s let to_string s = String.(concat "" (split_on_char '_' s)) @@ -54,15 +54,17 @@ type sign = SPlus | SMinus module SignedNat = struct type t = sign * UnsignedNat.t - let of_string n = + let of_string s = + assert (String.length s > 0); let sign,n = - if String.length n > 0 && n.[0] = '-' - then (SMinus,String.sub n 1 (String.length n - 1)) - else (SPlus,n) in + match s.[0] with + | '-' -> (SMinus,String.sub s 1 (String.length s - 1)) + | '+' -> (SPlus,String.sub s 1 (String.length s - 1)) + | _ -> (SPlus,s) in (sign,UnsignedNat.of_string n) - let to_string (s,n) = - (match s with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n - let to_bigint s = Bigint.of_string (to_string s) + let to_string (sign,n) = + (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n + let to_bigint n = Bigint.of_string (to_string n) let of_bigint n = let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in (sign, Bigint.to_string n) @@ -196,10 +198,13 @@ struct Pp.str (sprint i) let parse_string s = - if s = "" || s = "-" || - (s.[0] < '0' || s.[0] > '9') && (s.[0] <> '-' || s.[1] < '0' || s.[1] > '9') then None else + if s = "" || s = "-" || s = "+" || + (s.[0] < '0' || s.[0] > '9') && ((s.[0] <> '-' && s.[0] <> '+') || s.[1] < '0' || s.[1] > '9') then None else let strm = Stream.of_string (s ^ " ") in - let sign = if s.[0] = '-' then (Stream.junk strm; SMinus) else SPlus in + let sign = match s.[0] with + | '-' -> (Stream.junk strm; SMinus) + | '+' -> (Stream.junk strm; SPlus) + | _ -> SPlus in let n = parse strm in if Stream.count strm >= String.length s then Some (sign,n) else None -- cgit v1.2.3