diff options
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 4 | ||||
| -rw-r--r-- | plugins/syntax/numbers_syntax.ml | 94 |
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 |