diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-04-26 17:30:30 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-14 09:44:21 +0200 |
| commit | d038839a32978548051573286e22462d68d42ee6 (patch) | |
| tree | 14af8ed8354ef5ace1f685b1593529a2394f86d8 /interp/notation.ml | |
| parent | 7e63c300a3aa1e3befb29bab9094e8b1939824bb (diff) | |
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
This string contains the base-10 representation of the number (big endian)
Note that some inner parsing stuff still uses bigints, see egramcoq.ml
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 23332f7c4..f74e1d43b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -10,7 +10,6 @@ open CErrors open Util open Pp -open Bigint open Names open Term open Libnames @@ -319,7 +318,13 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) patl -let mkNumeral n = Numeral n +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) + +let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + let mkString = function | None -> None | Some s -> if Unicode.is_utf8 s then Some (String s) else None @@ -327,8 +332,10 @@ let mkString = function let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = + let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p) + (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) + | p -> cont ?loc p) (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = @@ -440,8 +447,8 @@ let find_notation ntn sc = (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral n when is_pos_or_zero n -> to_string n - | Numeral n -> "- "^(to_string (neg n)) + | Numeral (n,true) -> n + | Numeral (n,false) -> "- "^n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -466,7 +473,8 @@ let interp_prim_token_gen ?loc g p local_scopes = with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with - | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) + | Numeral _ -> + str "No interpretation for numeral " ++ str (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token ?loc = |