aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml44
-rw-r--r--interp/constrintern.ml3
-rw-r--r--interp/dune2
-rw-r--r--interp/impargs.ml40
-rw-r--r--interp/impargs.mli2
-rw-r--r--interp/notation.ml48
-rw-r--r--interp/notation.mli8
-rw-r--r--interp/numTok.ml67
-rw-r--r--interp/numTok.mli12
-rw-r--r--interp/stdarg.ml4
-rw-r--r--interp/stdarg.mli3
11 files changed, 91 insertions, 142 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3667757a2f..43fef8685d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -636,10 +636,10 @@ exception Expl
(* If the removal of implicit arguments is not possible, raise [Expl] *)
(* [inctx] tells if the term is in a context which will enforce the external type *)
(* [n] is the total number of arguments block to which the [args] belong *)
-let adjust_implicit_arguments inctx n q args impl =
- let rec exprec q = function
+let adjust_implicit_arguments inctx n args impl =
+ let rec exprec = function
| a::args, imp::impl when is_status_implicit imp ->
- let tail = exprec (q+1) (args,impl) in
+ let tail = exprec (args,impl) in
let visible =
!Flags.raw_print ||
(!print_implicits && !print_implicits_explicit_args) ||
@@ -652,13 +652,13 @@ let adjust_implicit_arguments inctx n q args impl =
(Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
else
tail
- | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
+ | a::args, _::impl -> (Lazy.force a,None) :: exprec (args,impl)
| args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
| [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
(* The non-explicit application cannot be parsed back with the same type *)
raise Expl
| [], _ -> []
- in exprec q (args,impl)
+ in exprec (args,impl)
let extern_projection (cf,f) args impl =
let ip = is_projection (List.length args) cf in
@@ -750,14 +750,14 @@ let extern_applied_ref inctx impl (cf,f) us args =
match extern_projection (cf,f) args impl with
(* Try a [t.(f args1) args2] projection-style notation *)
| Some (i,(args1,impl1),(args2,impl2)) ->
- let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in
- let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in
+ let args1 = adjust_implicit_arguments inctx n args1 impl1 in
+ let args2 = adjust_implicit_arguments inctx n args2 impl2 in
let ip = Some (List.length args1) in
CApp ((ip,f),args1@args2)
(* A normal application node with each individual implicit
arguments either dropped or made explicit *)
| None ->
- let args = adjust_implicit_arguments inctx n 1 args impl in
+ let args = adjust_implicit_arguments inctx n args impl in
if args = [] then ref else CApp ((None, f), args)
with Expl ->
(* A [@f args] node *)
@@ -765,10 +765,10 @@ let extern_applied_ref inctx impl (cf,f) us args =
let isproj = if !print_projections then isproj else None in
CAppExpl ((isproj,f,us), args)
-let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
+let extern_applied_syntactic_definition inctx n extraimpl (cf,f) syndefargs extraargs =
try
let syndefargs = List.map (fun a -> (a,None)) syndefargs in
- let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in
+ let extraargs = adjust_implicit_arguments inctx n extraargs extraimpl in
let args = syndefargs @ extraargs in
if args = [] then cf else CApp ((None, CAst.make cf), args)
with Expl ->
@@ -784,12 +784,12 @@ let mkFlattenedCApp (head,args) =
| _ ->
CApp ((None, head), args)
-let extern_applied_notation n impl f args =
+let extern_applied_notation inctx n impl f args =
if List.is_empty args then
f.CAst.v
else
try
- let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in
+ let args = adjust_implicit_arguments inctx n args impl in
mkFlattenedCApp (f,args)
with Expl -> raise No_match
@@ -940,11 +940,11 @@ let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
let rec extern inctx ?impargs scopes vars r =
match remove_one_coercion inctx (flatten_application r) with
| Some (nargs,inctx,r') ->
- (try extern_notations scopes vars (Some nargs) r
+ (try extern_notations inctx scopes vars (Some nargs) r
with No_match -> extern inctx scopes vars r')
| None ->
- try extern_notations scopes vars None r
+ try extern_notations inctx scopes vars None r
with No_match ->
let loc = r.CAst.loc in
@@ -1000,7 +1000,7 @@ let rec extern inctx ?impargs scopes vars r =
mkFlattenedCApp (head,args))
| GLetIn (na,b,t,c) ->
- CLetIn (make ?loc na,sub_extern false scopes vars b,
+ CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
Option.map (extern_typ scopes vars) t,
extern inctx ?impargs scopes (add_vname vars na) c)
@@ -1197,7 +1197,7 @@ and extern_local_binder scopes vars = function
extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
(assums,na::ids,
CLocalDef(CAst.make na, extern false scopes vars bd,
- Option.map (extern false scopes vars) ty) :: l)
+ Option.map (extern_typ scopes vars) ty) :: l)
| GLocalAssum (na,bk,ty) ->
let implicit_type = is_reserved_type na ty in
@@ -1225,14 +1225,14 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
make ?loc (pll,extern inctx scopes vars c)
-and extern_notations scopes vars nargs t =
+and extern_notations inctx scopes vars nargs t =
if !Flags.raw_print || !print_no_symbol then raise No_match;
try extern_possible_prim_token scopes t
with No_match ->
let t = flatten_application t in
- extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+ extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
-and extern_notation (custom,scopes as allscopes) vars t rules =
+and extern_notation inctx (custom,scopes as allscopes) vars t rules =
match rules with
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
@@ -1313,7 +1313,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
let c = insert_entry_coercion coercion (insert_delimiters c key) in
let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
- CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
+ CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args)
| SynDefRule kn ->
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -1323,13 +1323,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
let a = CRef (cf,None) in
let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
- let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
+ let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in
if isCRef_no_univ c.CAst.v && entry_has_global custom then c
else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion -> insert_entry_coercion coercion c
with
- No_match -> extern_notation allscopes vars t rules
+ No_match -> extern_notation inctx allscopes vars t rules
let extern_glob_constr vars c =
extern false (InConstrEntrySomeLevel,(None,[])) vars c
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6d4ab8b4d6..1d3b1bbb24 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1724,8 +1724,7 @@ let drop_notations_pattern looked_for genv =
the domains of lambdas in the encoding of match in constr.
This check is here and not in the parser because it would require
duplicating the levels of the [pattern] rule. *)
- CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
- (Pp.strbrk "Casts are not supported in this pattern.")
+ CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
diff --git a/interp/dune b/interp/dune
index e9ef7ba99a..6d73d5724c 100644
--- a/interp/dune
+++ b/interp/dune
@@ -3,4 +3,4 @@
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
(public_name coq.interp)
(wrapped false)
- (libraries pretyping))
+ (libraries zarith pretyping))
diff --git a/interp/impargs.ml b/interp/impargs.ml
index db102470b0..7742f985de 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -20,7 +20,6 @@ open Lib
open Libobject
open EConstr
open Reductionops
-open Namegen
open Constrexpr
module NamedDecl = Context.Named.Declaration
@@ -247,24 +246,15 @@ let is_rigid env sigma t =
is_rigid_head sigma t
| _ -> true
-let find_displayed_name_in sigma all avoid na (env, b) =
- let envnames_b = (env, b) in
- let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in sigma flag avoid na b
- else compute_displayed_name_in sigma flag avoid na b
-
-let compute_implicits_names_gen all env sigma t =
+let compute_implicits_names env sigma t =
let open Context.Rel.Declaration in
- let rec aux env avoid names t =
+ let rec aux env names t =
let t = whd_all env sigma t in
match kind sigma t with
| Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in
- aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+ aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b
| _ -> List.rev names
- in aux env Id.Set.empty [] t
-
-let compute_implicits_names = compute_implicits_names_gen true
+ in aux env [] t
let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
let open Context.Rel.Declaration in
@@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t =
(f.strict || f.strongly_strict) f.strongly_strict
f.reversible_pattern f.contextual env sigma t
-let compute_implicits_flags env sigma f all t =
+let compute_implicits_flags env sigma f t =
List.combine
- (compute_implicits_names_gen all env sigma t)
+ (compute_implicits_names env sigma t)
(compute_implicits_explanation_flags env sigma f t)
let compute_auto_implicits env sigma flags enriching t =
@@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) =
let rec prepare_implicits i f = function
| [] -> []
- | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
- | (Name id, Some imp)::imps ->
+ | (na, Some imp)::imps ->
let imps' = prepare_implicits (i+1) f imps in
- Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+ let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in
+ Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits (i+1) f imps
let set_manual_implicits silent flags enriching autoimps l =
@@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l =
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
- else let l = compute_implicits_flags env sigma f false t in
+ else let l = compute_implicits_flags env sigma f t in
[DefaultImpArgs, prepare_implicits 1 f l]
(*s Constants. *)
@@ -677,10 +667,12 @@ let explicit_kind i = function
let compute_implicit_statuses autoimps l =
let rec aux i = function
- | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
- | na :: autoimps, MaxImplicit :: manualimps ->
+ | _ :: autoimps, (_, Explicit) :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+ | na :: autoimps, (Anonymous, MaxImplicit) :: manualimps
+ | _ :: autoimps, (na, MaxImplicit) :: manualimps ->
Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
- | na :: autoimps, NonMaxImplicit :: manualimps ->
+ | na :: autoimps, (Anonymous, NonMaxImplicit) :: manualimps
+ | _ :: autoimps, (na, NonMaxImplicit) :: manualimps ->
let imps' = aux (i+1) (autoimps, manualimps) in
let max = set_maximality Error na i imps' false in
Some (explicit_kind i na, Manual, (max, true)) :: imps'
@@ -703,7 +695,7 @@ let set_implicits local ref l =
check_rigidity (is_rigid env sigma t);
(* Sort by number of implicits, decreasing *)
let is_implicit = function
- | Explicit -> false
+ | _, Explicit -> false
| _ -> true in
let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 97841b37f2..c8bcef19c8 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -117,7 +117,7 @@ val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
(** [set_implicits local ref l]
Manual declaration of implicit arguments.
`l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> (Name.t * Glob_term.binding_kind) list list -> unit
val implicits_of_global : GlobRef.t -> implicits_list list
diff --git a/interp/notation.ml b/interp/notation.ml
index c4e9496b95..17ae045187 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -388,7 +388,7 @@ module InnerPrimToken = struct
type interpreter =
| RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr)
- | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr)
+ | BigNumInterp of (?loc:Loc.t -> Z.t -> glob_constr)
| StringInterp of (?loc:Loc.t -> string -> glob_constr)
let interp_eq f f' = match f,f' with
@@ -410,7 +410,7 @@ module InnerPrimToken = struct
type uninterpreter =
| RawNumUninterp of (any_glob_constr -> rawnum option)
- | BigNumUninterp of (any_glob_constr -> Bigint.bigint option)
+ | BigNumUninterp of (any_glob_constr -> Z.t option)
| StringUninterp of (any_glob_constr -> string option)
let uninterp_eq f f' = match f,f' with
@@ -612,13 +612,14 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
end
+let z_two = Z.of_int 2
+
(** 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
+ if Z.(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)
+ let quo, remi = Z.div_rem i z_two in
+ if Z.(equal remi one) 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)
@@ -800,24 +801,24 @@ let rawnum_of_coqint c =
(** First, [positive] from/to bigint *)
let rec pos_of_bigint posty n =
- match Bigint.div2_with_rest n with
- | (q, false) ->
+ match Z.div_rem n z_two with
+ | (q, rem) when rem = Z.zero ->
let c = mkConstruct (posty, 2) in (* xO *)
mkApp (c, [| pos_of_bigint posty q |])
- | (q, true) when not (Bigint.equal q Bigint.zero) ->
+ | (q, _) when not (Z.equal q Z.zero) ->
let c = mkConstruct (posty, 1) in (* xI *)
mkApp (c, [| pos_of_bigint posty q |])
- | (q, true) ->
+ | (q, _) ->
mkConstruct (posty, 3) (* xH *)
let rec bigint_of_pos c = match Constr.kind c with
- | Construct ((_, 3), _) -> (* xH *) Bigint.one
+ | Construct ((_, 3), _) -> (* xH *) Z.one
| App (c, [| d |]) ->
begin match Constr.kind c with
| Construct ((_, n), _) ->
begin match n with
- | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
- | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
+ | 1 -> (* xI *) Z.add Z.one (Z.mul z_two (bigint_of_pos d))
+ | 2 -> (* xO *) Z.mul z_two (bigint_of_pos d)
| n -> assert false (* no other constructor of type positive *)
end
| x -> raise NotAValidPrimToken
@@ -827,24 +828,24 @@ let rec bigint_of_pos c = match Constr.kind c with
(** Now, [Z] from/to bigint *)
let z_of_bigint { z_ty; pos_ty } n =
- if Bigint.equal n Bigint.zero then
+ if Z.(equal n zero) then
mkConstruct (z_ty, 1) (* Z0 *)
else
let (s, n) =
- if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
- else (3, Bigint.neg n) (* Zneg *)
+ if Z.(leq zero n) then (2, n) (* Zpos *)
+ else (3, Z.neg n) (* Zneg *)
in
let c = mkConstruct (z_ty, s) in
mkApp (c, [| pos_of_bigint pos_ty n |])
let bigint_of_z z = match Constr.kind z with
- | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
+ | Construct ((_, 1), _) -> (* Z0 *) Z.zero
| App (c, [| d |]) ->
begin match Constr.kind c with
| Construct ((_, n), _) ->
begin match n with
| 2 -> (* Zpos *) bigint_of_pos d
- | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
+ | 3 -> (* Zneg *) Z.neg (bigint_of_pos d)
| n -> assert false (* no other constructor of type Z *)
end
| _ -> raise NotAValidPrimToken
@@ -861,20 +862,19 @@ 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))
+ CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n))
let interp_int63 ?loc n =
- let open Bigint in
- if is_pos_or_zero n
+ if Z.(leq zero n)
then
- if less_than n (pow two 63)
+ if Z.(lt n (pow z_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)
+ | Int i -> Z.of_string (Uint63.to_string i)
| _ -> raise NotAValidPrimToken
let interp o ?loc n =
@@ -1429,7 +1429,7 @@ let declare_entry_coercion (scope,(entry,key)) lev entry' =
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
- if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
+ if entry' = entry'' && level_ord lev'' lev' && entry <> entry'''
then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
diff --git a/interp/notation.mli b/interp/notation.mli
index 05ddd25a62..948831b317 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -101,7 +101,7 @@ val register_rawnumeral_interpretation :
?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
val register_bignumeral_interpretation :
- ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit
+ ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
val register_string_interpretation :
?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
@@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit
*)
val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module ->
- Bigint.bigint prim_token_interpreter ->
- glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit
+ Z.t prim_token_interpreter ->
+ glob_constr list * Z.t prim_token_uninterpreter * bool -> unit
val declare_string_interpreter : ?local:bool -> scope_name -> required_module ->
string prim_token_interpreter ->
glob_constr list * string prim_token_uninterpreter * bool -> unit
@@ -349,4 +349,4 @@ val level_of_notation : notation -> level
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
(** Conversion from bigint to int63 *)
-val int63_of_pos_bigint : Bigint.bigint -> Uint63.t
+val int63_of_pos_bigint : Z.t -> Uint63.t
diff --git a/interp/numTok.ml b/interp/numTok.ml
index bb14649b91..124a6cd249 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -80,63 +80,14 @@ struct
let to_string (sign,n) =
(match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n
let classify (_,n) = UnsignedNat.classify n
- let bigint_of_string (sign,n) =
- (* nasty code to remove when switching to zarith
- since zarith's of_string handles hexadecimal *)
- match UnsignedNat.classify n with
- | CDec -> Bigint.of_string (to_string (sign,n))
- | CHex ->
- let int_of_char c = match c with
- | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a'
- | _ -> int_of_char c - int_of_char '0' in
- let c16 = Bigint.of_int 16 in
- let s = UnsignedNat.to_string n in
- let n = ref Bigint.zero in
- let len = String.length s in
- for d = 2 to len - 1 do
- n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d])))
- done;
- match sign with SPlus -> !n | SMinus -> Bigint.neg !n
+ let bigint_of_string (sign,n) = Z.of_string (to_string (sign,n))
let to_bigint n = bigint_of_string n
let string_of_nonneg_bigint c n =
- (* nasty code to remove when switching to zarith
- since zarith's format handles hexadecimal *)
match c with
- | CDec -> Bigint.to_string n
- | CHex ->
- let div16 n =
- let n, r0 = Bigint.div2_with_rest n in
- let n, r1 = Bigint.div2_with_rest n in
- let n, r2 = Bigint.div2_with_rest n in
- let n, r3 = Bigint.div2_with_rest n in
- let r = match r3, r2, r1, r0 with
- | false, false, false, false -> "0"
- | false, false, false, true -> "1"
- | false, false, true, false -> "2"
- | false, false, true, true -> "3"
- | false, true, false, false -> "4"
- | false, true, false, true -> "5"
- | false, true, true, false -> "6"
- | false, true, true, true -> "7"
- | true, false, false, false -> "8"
- | true, false, false, true -> "9"
- | true, false, true, false -> "a"
- | true, false, true, true -> "b"
- | true, true, false, false -> "c"
- | true, true, false, true -> "d"
- | true, true, true, false -> "e"
- | true, true, true, true -> "f" in
- n, r in
- let n = ref n in
- let l = ref [] in
- while Bigint.is_strictly_pos !n do
- let n', r = div16 !n in
- n := n';
- l := r :: !l
- done;
- "0x" ^ String.concat "" (List.rev !l)
+ | CDec -> Z.format "%d" n
+ | CHex -> Z.format "0x%x" n
let of_bigint c n =
- let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in
+ 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)
end
@@ -339,13 +290,13 @@ struct
let frac = UnsignedNat.to_string frac in
let i = SignedNat.to_bigint (s, int ^ frac) in
let e =
- let e = if exp = "" then Bigint.zero else match exp.[1] with
- | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp))
- | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
- | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
+ let e = if exp = "" then Z.zero else match exp.[1] with
+ | '+' -> Z.of_string (UnsignedNat.to_string (string_del_head 2 exp))
+ | '-' -> Z.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp))))
+ | _ -> Z.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in
let l = String.length frac in
let l = match c with CDec -> l | CHex -> 4 * l in
- Bigint.(sub e (of_int l)) in
+ Z.(sub e (of_int l)) in
(i, match c with CDec -> EDec e | CHex -> EBin e)
let of_bigint_and_exponent i e =
diff --git a/interp/numTok.mli b/interp/numTok.mli
index 11d5a0f980..bcfe663dd2 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -65,8 +65,8 @@ sig
val classify : t -> num_class
- val of_bigint : num_class -> Bigint.bigint -> t
- val to_bigint : t -> Bigint.bigint
+ val of_bigint : num_class -> Z.t -> t
+ val to_bigint : t -> Z.t
end
(** {6 Unsigned decimal numerals } *)
@@ -131,8 +131,8 @@ sig
val to_string : t -> string
(** Returns a string in the syntax of OCaml's float_of_string *)
- val of_bigint : num_class -> Bigint.bigint -> t
- val to_bigint : t -> Bigint.bigint option
+ val of_bigint : num_class -> Z.t -> t
+ val to_bigint : t -> Z.t option
(** Convert from and to bigint when the denotation of a bigint *)
val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t
@@ -140,8 +140,8 @@ sig
(** n, p and q such that the number is n.p*10^q or n.p*2^q
pre/postcondition: classify n = classify p, classify q = CDec *)
- val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t
- val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp
+ val of_bigint_and_exponent : Z.t -> Z.t exp -> t
+ val to_bigint_and_exponent : t -> Z.t * Z.t exp
(** n and p such that the number is n*10^p or n*2^p *)
val classify : t -> num_class
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index d5f104b7f8..343f85be03 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -25,6 +25,9 @@ let wit_bool : bool uniform_genarg_type =
let wit_int : int uniform_genarg_type =
make0 "int"
+let wit_nat : int uniform_genarg_type =
+ make0 "nat"
+
let wit_string : string uniform_genarg_type =
make0 "string"
@@ -59,6 +62,7 @@ let wit_clause_dft_concl =
(** Aliases for compatibility *)
let wit_integer = wit_int
+let wit_natural = wit_nat
let wit_preident = wit_pre_ident
let wit_reference = wit_ref
let wit_global = wit_ref
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 89bdd78c70..3ae8b7d73f 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -23,6 +23,8 @@ val wit_unit : unit uniform_genarg_type
val wit_bool : bool uniform_genarg_type
+val wit_nat : int uniform_genarg_type
+
val wit_int : int uniform_genarg_type
val wit_string : string uniform_genarg_type
@@ -54,6 +56,7 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr,
(** Aliases for compatibility *)
+val wit_natural : int uniform_genarg_type
val wit_integer : int uniform_genarg_type
val wit_preident : string uniform_genarg_type
val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:10:32 +0000