aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/declare.ml3
-rw-r--r--interp/declare.mli1
-rw-r--r--interp/dumpglob.ml1
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/notation.ml41
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/notation_ops.ml10
-rw-r--r--interp/notation_term.ml1
9 files changed, 63 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 13078840ef..8e49800982 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -967,6 +967,8 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
map_cast_type (extern_typ scopes vars) c')
+ | GInt i ->
+ CPrim(Numeral (Uint63.to_string i,true))
in insert_coercion coercion (CAst.make ?loc c)
@@ -1312,6 +1314,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
| PSort s -> GSort s
+ | PInt i -> GInt i
let extern_constr_pattern env sigma pat =
extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
diff --git a/interp/declare.ml b/interp/declare.ml
index 6778fa1e7a..ea6ed8321d 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -442,6 +442,9 @@ let assumption_message id =
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
+let register_message id =
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered")
+
(** Monomorphic universes need to survive sections. *)
let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
diff --git a/interp/declare.mli b/interp/declare.mli
index 468e056909..669657af6f 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -74,6 +74,7 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool
val definition_message : Id.t -> unit
val assumption_message : Id.t -> unit
+val register_message : Id.t -> unit
val fixpoint_message : int array option -> Id.t list -> unit
val cofixpoint_message : Id.t list -> unit
val recursive_message : bool (** true = fixpoint *) ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index f5be0ddbae..a537b4848c 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -101,6 +101,7 @@ let type_of_logical_kind = function
| Property
| Proposition
| Corollary -> "thm")
+ | IsPrimitive -> "prim"
let type_of_global_ref gr =
if Typeclasses.is_class gr then
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 8a89bcdf26..959455dfd2 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -225,7 +225,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
| Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
| _ -> is_rigid_head sigma f)
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
- | Prod _ | Meta _ | Cast _ -> assert false
+ | Prod _ | Meta _ | Cast _ | Int _ -> assert false
let is_rigid env sigma t =
let open Context.Rel.Declaration in
diff --git a/interp/notation.ml b/interp/notation.ml
index ca27d439fb..bc68d97bb8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -574,6 +574,7 @@ 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 *)
type string_target_kind =
| ListByte
@@ -637,6 +638,7 @@ let rec constr_of_glob env sigma g = match DAst.get g with
let sigma,c = constr_of_glob env sigma gc in
let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
sigma,mkApp (c, Array.of_list cl)
+ | Glob_term.GInt i -> sigma, mkInt i
| _ ->
raise NotAValidPrimToken
@@ -649,6 +651,7 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
| Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
| Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
| Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+ | Int i -> DAst.make ?loc (Glob_term.GInt i)
| _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
let no_such_prim_token uninterpreted_token_kind ?loc ty =
@@ -683,6 +686,16 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
end
+(** Conversion from bigint to int63 *)
+let rec int63_of_pos_bigint i =
+ let open Bigint in
+ if equal i zero then Uint63.of_int 0
+ else
+ let (quo,rem) = div2_with_rest i in
+ if rem then Uint63.add (Uint63.of_int 1)
+ (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
+ else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
+
module Numeral = struct
(** * Numeral notation *)
open PrimTokenNotation
@@ -838,6 +851,32 @@ let bigint_of_z z = match Constr.kind z with
end
| _ -> raise NotAValidPrimToken
+(** Now, [Int63] from/to bigint *)
+
+let int63_of_pos_bigint ?loc n =
+ let i = int63_of_pos_bigint n in
+ mkInt i
+
+let error_negative ?loc =
+ CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.")
+
+let error_overflow ?loc n =
+ CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n))
+
+let interp_int63 ?loc n =
+ let open Bigint in
+ if is_pos_or_zero n
+ then
+ if less_than n (pow two 63)
+ then int63_of_pos_bigint ?loc n
+ else error_overflow ?loc n
+ else error_negative ?loc
+
+let bigint_of_int63 c =
+ match Constr.kind c with
+ | Int i -> Bigint.of_string (Uint63.to_string i)
+ | _ -> raise NotAValidPrimToken
+
let big2raw n =
if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
else (Bigint.to_string (Bigint.neg n), false)
@@ -856,6 +895,7 @@ let interp o ?loc n =
| UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst 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)
in
let env = Global.env () in
let sigma = Evd.from_env env in
@@ -877,6 +917,7 @@ let uninterp o n =
| (Int _, c) -> rawnum_of_coqint c
| (UInt _, c) -> (rawnum_of_coquint c, true)
| (Z _, c) -> big2raw (bigint_of_z c)
+ | (Int63, c) -> big2raw (bigint_of_int63 c)
end o n
end
diff --git a/interp/notation.mli b/interp/notation.mli
index a482e00e81..5dcc96dc29 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -127,6 +127,7 @@ 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 *)
type string_target_kind =
| ListByte
@@ -320,3 +321,6 @@ val entry_has_ident : notation_entry_level -> bool
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
+
+(** Conversion from bigint to int63 *)
+val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8d225fe683..890c24e633 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -89,9 +89,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
+| NInt i1, NInt i2 ->
+ Uint63.equal i1 i2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ ), _ -> false
+ | NRec _ | NSort _ | NCast _ | NInt _), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -220,6 +222,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
+ | NInt i -> GInt i
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -435,6 +438,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| GCast (c,k) -> NCast (aux c,map_cast_type aux k)
| GSort s -> NSort s
+ | GInt i -> NInt i
| GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
NHole (w, naming, arg)
@@ -623,6 +627,7 @@ let rec subst_notation_constr subst bound raw =
NRec (fk,idl,dll',tl',bl')
| NSort _ -> raw
+ | NInt _ -> raw
| NHole (knd, naming, solve) ->
let nknd = match knd with
@@ -1189,6 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
| GSort (GType _), NSort (GType _) when not u -> sigma
| GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
+ | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -1216,7 +1222,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _ ), _ -> raise No_match
+ | GCast _ | GInt _ ), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 0ef1f267f6..6fe20486dc 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -43,6 +43,7 @@ type notation_constr =
notation_constr array * notation_constr array
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
+ | NInt of Uint63.t
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:35:11 +0000