aboutsummaryrefslogtreecommitdiff
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml88
1 files changed, 67 insertions, 21 deletions
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:26:55 +0000