aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml45
-rw-r--r--interp/constrintern.mli14
-rw-r--r--interp/declare.ml48
-rw-r--r--interp/declare.mli4
-rw-r--r--interp/discharge.ml17
-rw-r--r--interp/dumpglob.ml1
-rw-r--r--interp/impargs.ml13
-rw-r--r--interp/impargs.mli1
-rw-r--r--interp/modintern.ml4
-rw-r--r--interp/notation.ml41
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/notation_ops.ml15
-rw-r--r--interp/notation_term.ml1
14 files changed, 132 insertions, 88 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 444ac5ab6d..8e49800982 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -625,8 +625,13 @@ let explicitize inctx impl (cf,f) args =
CApp ((ip,f),args1@args2)
| None ->
let args = exprec 1 (args,impl) in
- if List.is_empty args then f.CAst.v else CApp ((None, f), args)
- in
+ if List.is_empty args then f.CAst.v else
+ match f.CAst.v with
+ | CApp (g,args') ->
+ (* may happen with notations for a prefix of an n-ary
+ application *)
+ CApp (g,args'@args)
+ | _ -> CApp ((None, f), args) in
try expl ()
with Expl ->
let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
@@ -962,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)
@@ -1307,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/constrintern.ml b/interp/constrintern.ml
index c8c38ffe05..24894fc9f5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2328,36 +2328,38 @@ let interp_open_constr env sigma c =
(* Not all evars expected to be resolved and computation of implicit args *)
-let interp_constr_evars_gen_impls env sigma
+let interp_constr_evars_gen_impls ?(program_mode=false) env sigma
?(impls=empty_internalization_env) expected_type c =
let c = intern_gen expected_type ~impls env sigma c in
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
- let sigma, c = understand_tcc env sigma ~expected_type c in
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
+ let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
sigma, (c, imps)
-let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c
-let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ =
+ interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c
-let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen_impls env sigma ~impls IsType c
+let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c
(* Not all evars expected to be resolved, with side-effect on evars *)
-let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen ?(program_mode=false) env sigma ?(impls=empty_internalization_env) expected_type c =
let c = intern_gen expected_type ~impls env sigma c in
- understand_tcc env sigma ~expected_type c
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
+ understand_tcc ~flags env sigma ~expected_type c
-let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
+let interp_constr_evars ?program_mode env evdref ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen ?program_mode env evdref WithoutTypeConstraint ~impls c
-let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
- interp_constr_evars_gen env sigma ~impls (OfType typ) c
+let interp_casted_constr_evars ?program_mode env sigma ?(impls=empty_internalization_env) c typ =
+ interp_constr_evars_gen ?program_mode env sigma ~impls (OfType typ) c
-let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
- interp_constr_evars_gen env sigma IsType ~impls c
+let interp_type_evars ?program_mode env sigma ?(impls=empty_internalization_env) c =
+ interp_constr_evars_gen ?program_mode env sigma IsType ~impls c
(* Miscellaneous *)
@@ -2419,8 +2421,9 @@ let intern_context global_level env impl_env binders =
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
-let interp_glob_context_evars env sigma k bl =
+let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let open EConstr in
+ let flags = { Pretyping.all_no_fail_flags with program_mode } in
let env, sigma, par, _, impls =
List.fold_left
(fun (env,sigma,params,n,impls) (na, k, b, t) ->
@@ -2428,7 +2431,7 @@ let interp_glob_context_evars env sigma k bl =
if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
else t
in
- let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
+ let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
match b with
None ->
let d = LocalAssum (na,t) in
@@ -2440,13 +2443,13 @@ let interp_glob_context_evars env sigma k bl =
in
(push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
- let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
+ let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
let d = LocalDef (na, c, t) in
(push_rel d env, sigma, d::params, n, impls))
(env,sigma,[],k+1,[]) (List.rev bl)
in sigma, ((env, par), impls)
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
let int_env,bl = intern_context global_level env impl_env params in
- let sigma, x = interp_glob_context_evars env sigma shift bl in
+ let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 61acd09d65..2d14a0d0a7 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -113,26 +113,26 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
(** Accepting unresolved evars *)
-val interp_constr_evars : env -> evar_map ->
+val interp_constr_evars : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr -> evar_map * constr
-val interp_casted_constr_evars : env -> evar_map ->
+val interp_casted_constr_evars : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr -> types -> evar_map * constr
-val interp_type_evars : env -> evar_map ->
+val interp_type_evars : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr -> evar_map * types
(** Accepting unresolved evars and giving back the manual implicit arguments *)
-val interp_constr_evars_impls : env -> evar_map ->
+val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr ->
evar_map * (constr * Impargs.manual_implicits)
-val interp_casted_constr_evars_impls : env -> evar_map ->
+val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr -> types ->
evar_map * (constr * Impargs.manual_implicits)
-val interp_type_evars_impls : env -> evar_map ->
+val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map ->
?impls:internalization_env -> constr_expr ->
evar_map * (types * Impargs.manual_implicits)
@@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
(** Interpret contexts: returns extended env and context *)
val interp_context_evars :
- ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
+ ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
env -> evar_map -> local_binder_expr list ->
evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
diff --git a/interp/declare.ml b/interp/declare.ml
index 6778fa1e7a..4371b15c82 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -143,7 +143,7 @@ let declare_constant_common id cst =
update_tables c;
c
-let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
+let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
{ const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
@@ -156,8 +156,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
let is_poly de = match de.const_entry_universes with
- | Monomorphic_const_entry _ -> false
- | Polymorphic_const_entry _ -> true
+ | Monomorphic_entry _ -> false
+ | Polymorphic_entry _ -> true
in
let in_section = Lib.sections_are_opened () in
let export, decl = (* We deal with side effects *)
@@ -217,8 +217,8 @@ let cache_variable ((sp,_),o) =
section-local definition, but it's not enforced by typing *)
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
- | Monomorphic_const_entry uctx -> false, uctx
- | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+ | Monomorphic_entry uctx -> false, uctx
+ | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
(* We must declare the universe constraints before type-checking the
@@ -328,21 +328,15 @@ let dummy_inductive_entry m = {
mind_entry_record = None;
mind_entry_finite = Declarations.BiFinite;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
- mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
+ mind_entry_universes = default_univ_entry;
+ mind_entry_variance = None;
mind_entry_private = None;
}
(* reinfer subtyping constraints for inductive after section is dischared. *)
-let infer_inductive_subtyping mind_ent =
- match mind_ent.mind_entry_universes with
- | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
- mind_ent
- | Cumulative_ind_entry (_, cumi) ->
- begin
- let env = Global.env () in
- (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
- InferCumulativity.infer_inductive env mind_ent
- end
+let rebuild_inductive mind_ent =
+ let env = Global.env () in
+ InferCumulativity.infer_inductive env mind_ent
let inInductive : mutual_inductive_entry -> obj =
declare_object {(default_object "INDUCTIVE") with
@@ -352,25 +346,19 @@ let inInductive : mutual_inductive_entry -> obj =
classify_function = (fun a -> Substitute (dummy_inductive_entry a));
subst_function = ident_subst_function;
discharge_function = discharge_inductive;
- rebuild_function = infer_inductive_subtyping }
+ rebuild_function = rebuild_inductive }
let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
let id = Label.to_id label in
- let univs = match univs with
- | Monomorphic_ind_entry _ ->
+ let univs, u = match univs with
+ | Monomorphic_entry _ ->
(* Global constraints already defined through the inductive *)
- Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry (nas, ctx) ->
- Polymorphic_const_entry (nas, ctx)
- | Cumulative_ind_entry (nas, ctx) ->
- Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
- in
- let term, types = match univs with
- | Monomorphic_const_entry _ -> term, types
- | Polymorphic_const_entry (_, ctx) ->
- let u = Univ.UContext.instance ctx in
- Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+ default_univ_entry, Univ.Instance.empty
+ | Polymorphic_entry (nas, ctx) ->
+ Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
in
+ let term = Vars.subst_instance_constr u term in
+ let types = Vars.subst_instance_constr u types in
let entry = definition_entry ~types ~univs term in
let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
diff --git a/interp/declare.mli b/interp/declare.mli
index 468e056909..8f1e73c88c 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -43,7 +43,7 @@ type internal_flag =
(* Defaut definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
- ?univs:Entries.constant_universes_entry ->
+ ?univs:Entries.universes_entry ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
(** [declare_constant id cd] declares a global declaration
@@ -58,7 +58,7 @@ val declare_constant :
val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
?local:bool -> Id.t -> ?types:constr ->
- constr Entries.in_constant_universes_entry -> Constant.t
+ constr Entries.in_universes_entry -> Constant.t
(** Since transparent constants' side effects are globally declared, we
* need that *)
diff --git a/interp/discharge.ml b/interp/discharge.ml
index eeda5a6867..353b0f6057 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -76,18 +76,16 @@ let process_inductive info modlist mib =
let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
let subst, ind_univs =
match mib.mind_universes with
- | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
- | Polymorphic_ind auctx ->
+ | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
+ | Polymorphic auctx ->
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
let nas = Univ.AUContext.names auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Polymorphic_ind_entry (nas, auctx)
- | Cumulative_ind cumi ->
- let auctx = Univ.ACumulativityInfo.univ_context cumi in
- let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
- let nas = Univ.AUContext.names auctx in
- let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx)
+ subst, Polymorphic_entry (nas, auctx)
+ in
+ let variance = match mib.mind_variance with
+ | None -> None
+ | Some _ -> Some (InferCumulativity.dummy_variance ind_univs)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
@@ -114,6 +112,7 @@ let process_inductive info modlist mib =
mind_entry_params = params';
mind_entry_inds = inds';
mind_entry_private = mib.mind_private;
+ mind_entry_variance = variance;
mind_entry_universes = ind_univs
}
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..6fd52d98dd 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,12 +120,7 @@ let argument_position_eq p1 p2 = match p1, p2 with
| Hyp h1, Hyp h2 -> Int.equal h1 h2
| _ -> false
-let explicitation_eq ex1 ex2 = match ex1, ex2 with
-| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
- Int.equal i1 i2 && Option.equal Id.equal id1 id2
-| ExplByName id1, ExplByName id2 ->
- Id.equal id1 id2
-| _ -> false
+let explicitation_eq = Constrexpr_ops.explicitation_eq
type implicit_explanation =
| DepRigid of argument_position
@@ -200,7 +195,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
| App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
if strict then () else
iter_with_full_binders sigma push_lift (frec false) ed c
- | Proj (p,c) when rig ->
+ | Proj (p, _) when rig ->
if strict then () else
iter_with_full_binders sigma push_lift (frec false) ed c
| Case _ when rig ->
@@ -225,7 +220,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
@@ -380,7 +375,7 @@ let flatten_explicitations l autoimps =
| (Name id,_)::imps ->
let value, l' =
try
- let eq = explicitation_eq in
+ let eq = Constrexpr_ops.explicitation_eq in
let flags = List.assoc_f eq (ExplByName id) l in
Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
with Not_found -> assoc_by_pos k l
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 4afc2af5e9..43c26b024f 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -138,4 +138,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
val select_stronger_impargs : implicits_list list -> implicit_status list
val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
+ [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"]
(** Equality on [explicitation]. *)
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 60056dfd90..2f516f4f3c 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,12 +107,12 @@ let transl_with_decl env base kind = function
let c, ectx = interp_constr env sigma c in
let poly = lookup_polymorphism env base kind fqid in
begin match UState.check_univ_decl ~poly ectx udecl with
- | Entries.Polymorphic_const_entry (nas, ctx) ->
+ | Entries.Polymorphic_entry (nas, ctx) ->
let inst, ctx = Univ.abstract_universes nas ctx in
let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let c = EConstr.to_constr sigma c in
WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty
- | Entries.Monomorphic_const_entry ctx ->
+ | Entries.Monomorphic_entry ctx ->
let c = EConstr.to_constr sigma c in
WithDef (fqid,(c, None)), ctx
end
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..7d7e10a05b 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
@@ -903,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
(* TODO: look at the consequences for alp *)
alp, add_env alp sigma var (DAst.make @@ GVar id)
-let force_cases_pattern c =
- DAst.make ?loc:c.CAst.loc (DAst.get c)
-
let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
- let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
+ let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
try
(* If already bound to a binder, unify the term and the binder *)
let patl' = Id.List.assoc var binders in
@@ -1189,6 +1191,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 +1219,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-05-04 00:59:56 +0000