aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/nat_syntax.ml4
-rw-r--r--plugins/syntax/numbers_syntax.ml94
2 files changed, 39 insertions, 59 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 2fb8ce451..34a6a1a74 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -30,9 +30,11 @@ open Names
(* Parsing via scopes *)
(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+let threshold = of_int 5000
+
let nat_of_int dloc n =
if is_pos_or_zero n then begin
- if less_than (of_string "5000") n then
+ if less_than threshold n then
Flags.if_warn msg_warning
(strbrk "Stack overflow or segmentation fault happens when " ++
strbrk "working with large numbers in nat (observed threshold " ++
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 97753951a..9fa166661 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -51,26 +51,10 @@ let bigN_t = make_mind_mpdot bigN_module "BigN" "t'"
let bigN_scope = "bigN_scope"
(* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *)
-let n_inlined = of_string "7"
-let bigN_constructor =
- (* converts a bigint into an int the ugly way *)
- let rec to_int i =
- if equal i zero then
- 0
- else
- let (quo,rem) = div2_with_rest i in
- if rem then
- 2*(to_int quo)+1
- else
- 2*(to_int quo)
- in
- fun i ->
- ConstructRef ((bigN_t,0),
- if less_than i n_inlined then
- (to_int i)+1
- else
- (to_int n_inlined)+1
- )
+let n_inlined = 7
+
+let bigN_constructor i =
+ ConstructRef ((bigN_t,0),(min i n_inlined)+1)
(*bigZ stuff*)
let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ]
@@ -151,55 +135,54 @@ let _ = Notation.declare_numeral_interpreter int31_scope
(*** Parsing for bigN in digital notation ***)
(* the base for bigN (in Coq) that is 2^31 in our case *)
-let base = pow two (of_string "31")
+let base = pow two 31
-(* base of the bigN of height N : *)
-let rank n = pow base (pow two n)
+(* base of the bigN of height N : (2^31)^(2^n) *)
+let rank n =
+ let rec rk n pow2 =
+ if n <= 0 then pow2
+ else rk (n-1) (mult pow2 pow2)
+ in rk n base
(* splits a number bi at height n, that is the rest needs 2^n int31 to be stored
it is expected to be used only when the quotient would also need 2^n int31 to be
stored *)
let split_at n bi =
- euclid bi (rank (sub_1 n))
+ euclid bi (rank (n-1))
(* search the height of the Coq bigint needed to represent the integer bi *)
let height bi =
- let rec height_aux n =
- if less_than bi (rank n) then
- n
- else
- height_aux (add_1 n)
- in
- height_aux zero
-
+ let rec hght n pow2 =
+ if less_than bi pow2 then n
+ else hght (n+1) (mult pow2 pow2)
+ in hght 0 base
(* n must be a non-negative integer (from bigint.ml) *)
let word_of_pos_bigint dloc hght n =
let ref_W0 = GRef (dloc, zn2z_W0) in
let ref_WW = GRef (dloc, zn2z_WW) in
let rec decomp hgt n =
- if is_neg_or_zero hgt then
+ if hgt <= 0 then
int31_of_pos_bigint dloc n
else if equal n zero then
GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole)])
else
let (h,l) = split_at hgt n in
GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole);
- decomp (sub_1 hgt) h;
- decomp (sub_1 hgt) l])
+ decomp (hgt-1) h;
+ decomp (hgt-1) l])
in
decomp hght n
let bigN_of_pos_bigint dloc n =
- let ref_constructor i = GRef (dloc, bigN_constructor i) in
- let result h word = GApp (dloc, ref_constructor h, if less_than h n_inlined then
- [word]
- else
- [Nat_syntax.nat_of_int dloc (sub h n_inlined);
- word])
+ let h = height n in
+ let ref_constructor = GRef (dloc, bigN_constructor h) in
+ let word = word_of_pos_bigint dloc h n in
+ let args =
+ if h < n_inlined then [word]
+ else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word]
in
- let hght = height n in
- result hght (word_of_pos_bigint dloc hght n)
+ GApp (dloc, ref_constructor, args)
let bigN_error_negative dloc =
Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
@@ -217,22 +200,17 @@ let bigint_of_word =
let rec get_height rc =
match rc with
| GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
- let hleft = get_height lft in
- let hright = get_height rght in
- add_1
- (if less_than hleft hright then
- hright
- else
- hleft)
- | _ -> zero
+ 1+max (get_height lft) (get_height rght)
+ | _ -> 0
in
let rec transform hght rc =
match rc with
| GApp (_,GRef(_,c),_) when c = zn2z_W0-> zero
- | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in
- add (mult (rank new_hght)
- (transform (new_hght) lft))
- (transform (new_hght) rght)
+ | GApp (_,GRef(_,c), [_;lft;rght]) when c=zn2z_WW->
+ let new_hght = hght-1 in
+ add (mult (rank new_hght)
+ (transform new_hght lft))
+ (transform new_hght rght)
| _ -> bigint_of_int31 rc
in
fun rc ->
@@ -257,12 +235,12 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
- if less_than i (add_1 n_inlined) then
- GRef (Loc.ghost, bigN_constructor i)::(build (add_1 i))
+ if i < n_inlined+1 then
+ GRef (Loc.ghost, bigN_constructor i)::(build (i+1))
else
[]
in
- build zero
+ build 0
(* Actually declares the interpreter for bigN *)
let _ = Notation.declare_numeral_interpreter bigN_scope