diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 76 |
1 files changed, 30 insertions, 46 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index d6002d71b5..4010c3487e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -548,15 +548,15 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) - | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) - | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) - | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *) type string_target_kind = | ListByte @@ -869,30 +869,16 @@ let mkDecHex ind c n = match c with | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *) | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *) -exception NonDecimal - -let decimal_coqnumber_of_rawnum inds n = - if NumTok.Signed.classify n <> CDec then raise NonDecimal; - coqnumber_of_rawnum inds CDec n - let coqnumber_of_rawnum inds n = let c = NumTok.Signed.classify n in let n = coqnumber_of_rawnum inds c n in mkDecHex inds.number c n -let decimal_coquint_of_rawnum inds n = - if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal; - coquint_of_rawnum inds CDec (Some n) - let coquint_of_rawnum inds n = let c = NumTok.UnsignedNat.classify n in let n = coquint_of_rawnum inds c (Some n) in mkDecHex inds.uint c n -let decimal_coqint_of_rawnum inds n = - if NumTok.SignedNat.classify n <> CDec then raise NonDecimal; - coqint_of_rawnum inds CDec n - let coqint_of_rawnum inds n = let c = NumTok.SignedNat.classify n in let n = coqint_of_rawnum inds c n in @@ -947,23 +933,14 @@ let destDecHex c = match Constr.kind c with | _ -> raise NotAValidPrimToken) | _ -> raise NotAValidPrimToken -let decimal_rawnum_of_coqnumber c = - rawnum_of_coqnumber CDec c - let rawnum_of_coqnumber c = let cl, c = destDecHex c in rawnum_of_coqnumber cl c -let decimal_rawnum_of_coquint c = - rawnum_of_coquint CDec c - let rawnum_of_coquint c = let cl, c = destDecHex c in rawnum_of_coquint cl c -let decimal_rawnum_of_coqint c = - rawnum_of_coqint CDec c - let rawnum_of_coqint c = let cl, c = destDecHex c in rawnum_of_coqint cl c @@ -1038,12 +1015,22 @@ let error_negative ?loc = let error_overflow ?loc n = CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n)) -let interp_int63 ?loc n = +let error_underflow ?loc n = + CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "underflow in int63 literal: " ++ str (Z.to_string n)) + +let coqpos_neg_int63_of_bigint ?loc ind (sign,n) = + let uint = int63_of_pos_bigint ?loc n in + let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in + mkApp (mkConstruct (ind, pos_neg), [|uint|]) + +let interp_int63 ?loc ind n = + let sign = if Z.(compare n zero >= 0) then SPlus else SMinus in + let n = Z.abs n in if Z.(leq zero n) then if Z.(lt n (pow z_two 63)) - then int63_of_pos_bigint ?loc n - else error_overflow ?loc n + then coqpos_neg_int63_of_bigint ?loc ind (sign,n) + else match sign with SPlus -> error_overflow ?loc n | SMinus -> error_underflow ?loc n else error_negative ?loc let bigint_of_int63 c = @@ -1051,6 +1038,15 @@ let bigint_of_int63 c = | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken +let bigint_of_coqpos_neg_int63 c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> bigint_of_int63 c' + | Construct ((_,2), _) (* Neg *) -> Z.neg (bigint_of_int63 c') + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken + let interp o ?loc n = begin match o.warning, n with | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> @@ -1062,22 +1058,13 @@ let interp o ?loc n = coqint_of_rawnum int_ty n | UInt int_ty, Some (SPlus, n) -> coquint_of_rawnum int_ty n - | DecimalInt int_ty, Some n -> - (try decimal_coqint_of_rawnum int_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) - | DecimalUInt int_ty, Some (SPlus, n) -> - (try decimal_coquint_of_rawnum int_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) | 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 _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ -> + | Int63 pos_neg_int63_ty, Some n -> + interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n) + | (Int _ | UInt _ | Z _ | Int63 _), _ -> no_such_prim_token "number" ?loc o.ty_name | Number number_ty, _ -> coqnumber_of_rawnum number_ty n - | Decimal number_ty, _ -> - (try decimal_coqnumber_of_rawnum number_ty n - with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) in let env = Global.env () in let sigma = Evd.from_env env in @@ -1100,11 +1087,8 @@ let uninterp o n = | (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 CDec (bigint_of_z c) - | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c) + | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c) | (Number _, c) -> rawnum_of_coqnumber c - | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) - | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) - | (Decimal _, c) -> decimal_rawnum_of_coqnumber c end o n end |