aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml25
-rw-r--r--interp/constrextern.mli1
-rw-r--r--interp/dune2
-rw-r--r--interp/notation.ml76
-rw-r--r--interp/notation.mli8
-rw-r--r--interp/numTok.ml2
-rw-r--r--interp/reserve.ml10
7 files changed, 57 insertions, 67 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8138b4c6d9..3cabf52197 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -64,7 +64,7 @@ let print_parentheses = Notation_ops.print_parentheses
(* This forces printing universe names of Type{.} *)
let print_universes = Detyping.print_universes
-(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
+(* This suppresses printing of notations *)
let print_no_symbol = ref false
(* This tells to skip types if a variable has this type by default *)
@@ -74,6 +74,9 @@ let print_use_implicit_types =
~key:["Printing";"Use";"Implicit";"Types"]
~value:true
+(* Print primitive tokens, like strings *)
+let print_raw_literal = ref false
+
(**********************************************************************)
let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
@@ -434,7 +437,7 @@ let extern_record_pattern cstrsp args =
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
- if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
@@ -853,6 +856,7 @@ let same_binder_type ty nal c =
(* one with no delimiter if possible) *)
let extern_possible_prim_token (custom,scopes) r =
+ if !print_raw_literal then raise No_match;
let (n,key) = uninterp_prim_token r scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
@@ -969,7 +973,13 @@ let rec extern inctx ?impargs scopes vars r =
with No_match -> extern inctx scopes vars r')
| None ->
- try extern_notations inctx scopes vars None r
+ let r' = match DAst.get r with
+ | GInt i when Coqlib.has_ref "num.int63.wrap_int" ->
+ let wrap = Coqlib.lib_ref "num.int63.wrap_int" in
+ DAst.make (GApp (DAst.make (GRef (wrap, None)), [r]))
+ | _ -> r in
+
+ try extern_notations inctx scopes vars None r'
with No_match ->
let loc = r.CAst.loc in
@@ -1123,7 +1133,7 @@ let rec extern inctx ?impargs scopes vars r =
| GInt i ->
extern_prim_token_delimiter_if_required
- (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
+ (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i))))
"int63" "int63_scope" (snd scopes)
| GFloat f -> extern_float f (snd scopes)
@@ -1255,11 +1265,12 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
make ?loc (pll,extern inctx scopes vars c)
and extern_notations inctx scopes vars nargs t =
- if !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.raw_print then raise No_match;
try extern_possible_prim_token scopes t
with No_match ->
- let t = flatten_application t in
- extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+ if !print_no_symbol then raise No_match;
+ let t = flatten_application t in
+ extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
and extern_notation inctx (custom,scopes as allscopes) vars t rules =
match rules with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 298b52f0be..bb49c8697d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -60,6 +60,7 @@ val print_parentheses : bool ref
val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
+val print_raw_literal : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
diff --git a/interp/dune b/interp/dune
index 6d73d5724c..793ce48ea3 100644
--- a/interp/dune
+++ b/interp/dune
@@ -1,6 +1,6 @@
(library
(name interp)
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
- (public_name coq.interp)
+ (public_name coq-core.interp)
(wrapped false)
(libraries zarith pretyping))
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
diff --git a/interp/notation.mli b/interp/notation.mli
index 97955bf92e..195f2a4416 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -137,15 +137,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
diff --git a/interp/numTok.ml b/interp/numTok.ml
index 124a6cd249..12ef33717a 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -85,7 +85,7 @@ struct
let string_of_nonneg_bigint c n =
match c with
| CDec -> Z.format "%d" n
- | CHex -> Z.format "0x%x" n
+ | CHex -> Z.format "%#x" n
let of_bigint c n =
let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
(sign, string_of_nonneg_bigint c n)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 07160dcf6f..cdc95285fe 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -15,8 +15,6 @@ open Util
open Pp
open Names
open Nameops
-open Libobject
-open Lib
open Notation_term
open Notation_ops
open Globnames
@@ -77,15 +75,11 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NRef (ref,_) -> RefKey(canonical_gr ref), None
| _ -> Oth, None
-let cache_reserved_type (_,(id,t)) =
+let add_reserved_type (id,t) =
let key = fst (notation_constr_key t) in
reserve_table := Id.Map.add id t !reserve_table;
reserve_revtable := keymap_add key (id, t) !reserve_revtable
-let in_reserved : Id.t * notation_constr -> obj =
- declare_object {(default_object "RESERVED-TYPE") with
- cache_function = cache_reserved_type }
-
let declare_reserved_type_binding {CAst.loc;v=id} t =
if not (Id.equal id (root_of_id id)) then
user_err ?loc ~hdr:"declare_reserved_type"
@@ -96,7 +90,7 @@ let declare_reserved_type_binding {CAst.loc;v=id} t =
user_err ?loc ~hdr:"declare_reserved_type"
((Id.print id++str" is already bound to a type"))
with Not_found -> () end;
- add_anonymous_leaf (in_reserved (id,t))
+ add_reserved_type (id,t)
let declare_reserved_type idl t =
List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:37:21 +0000