summaryrefslogtreecommitdiff
path: root/plugins/syntax/numbers_syntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/numbers_syntax.ml')
-rw-r--r--plugins/syntax/numbers_syntax.ml158
1 files changed, 67 insertions, 91 deletions
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index a540a7d0..b8636a74 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -1,18 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: numbers_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* digit-based syntax for int31, bigN bigZ and bigQ *)
open Bigint
open Libnames
-open Rawterm
+open Glob_term
(*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
@@ -48,30 +46,14 @@ let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)
let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ]
let bigN_path = make_path (bigN_module@["BigN"]) "t"
-let bigN_t = make_mind_mpdot bigN_module "BigN" "t_"
+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" ]
@@ -100,9 +82,9 @@ exception Non_closed
(* parses a *non-negative* integer (from bigint.ml) into an int31
wraps modulo 2^31 *)
let int31_of_pos_bigint dloc n =
- let ref_construct = RRef (dloc, int31_construct) in
- let ref_0 = RRef (dloc, int31_0) in
- let ref_1 = RRef (dloc, int31_1) in
+ let ref_construct = GRef (dloc, int31_construct) in
+ let ref_0 = GRef (dloc, int31_0) in
+ let ref_1 = GRef (dloc, int31_1) in
let rec args counter n =
if counter <= 0 then
[]
@@ -110,7 +92,7 @@ let int31_of_pos_bigint dloc n =
let (q,r) = div2_with_rest n in
(if r then ref_1 else ref_0)::(args (counter-1) q)
in
- RApp (dloc, ref_construct, List.rev (args 31 n))
+ GApp (dloc, ref_construct, List.rev (args 31 n))
let error_negative dloc =
Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
@@ -127,12 +109,12 @@ let bigint_of_int31 =
let rec args_parsing args cur =
match args with
| [] -> cur
- | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
- | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
+ | (GRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur)
+ | (GRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur))
| _ -> raise Non_closed
in
function
- | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero
+ | GApp (_, GRef (_, c), args) when c=int31_construct -> args_parsing args zero
| _ -> raise Non_closed
let uninterp_int31 i =
@@ -145,62 +127,61 @@ let uninterp_int31 i =
let _ = Notation.declare_numeral_interpreter int31_scope
(int31_path, int31_module)
interp_int31
- ([RRef (Util.dummy_loc, int31_construct)],
+ ([GRef (Util.dummy_loc, int31_construct)],
uninterp_int31,
true)
(*** 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 = RRef (dloc, zn2z_W0) in
- let ref_WW = RRef (dloc, zn2z_WW) in
+ 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
- RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)])
+ GApp (dloc, ref_W0, [GHole (dloc, Evd.InternalHole)])
else
let (h,l) = split_at hgt n in
- RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole);
- decomp (sub_1 hgt) h;
- decomp (sub_1 hgt) l])
+ GApp (dloc, ref_WW, [GHole (dloc, Evd.InternalHole);
+ decomp (hgt-1) h;
+ decomp (hgt-1) l])
in
decomp hght n
let bigN_of_pos_bigint dloc n =
- let ref_constructor i = RRef (dloc, bigN_constructor i) in
- let result h word = RApp (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 =
Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
@@ -217,23 +198,18 @@ let interp_bigN dloc n =
let bigint_of_word =
let rec get_height rc =
match rc with
- | RApp (_,RRef(_,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
+ | GApp (_,GRef(_,c), [_;lft;rght]) when c = zn2z_WW ->
+ 1+max (get_height lft) (get_height rght)
+ | _ -> 0
in
let rec transform hght rc =
match rc with
- | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero
- | RApp (_,RRef(_,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),_) when c = zn2z_W0-> zero
+ | 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 ->
@@ -242,8 +218,8 @@ let bigint_of_word =
let bigint_of_bigN rc =
match rc with
- | RApp (_,_,[one_arg]) -> bigint_of_word one_arg
- | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
+ | GApp (_,_,[one_arg]) -> bigint_of_word one_arg
+ | GApp (_,_,[_;second_arg]) -> bigint_of_word second_arg
| _ -> raise Non_closed
let uninterp_bigN rc =
@@ -258,12 +234,12 @@ let uninterp_bigN rc =
let bigN_list_of_constructors =
let rec build i =
- if less_than i (add_1 n_inlined) then
- RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i))
+ if i < n_inlined+1 then
+ GRef (Util.dummy_loc, 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
@@ -276,17 +252,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
(*** Parsing for bigZ in digital notation ***)
let interp_bigZ dloc n =
- let ref_pos = RRef (dloc, bigZ_pos) in
- let ref_neg = RRef (dloc, bigZ_neg) in
+ let ref_pos = GRef (dloc, bigZ_pos) in
+ let ref_neg = GRef (dloc, bigZ_neg) in
if is_pos_or_zero n then
- RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
+ GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])
else
- RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
+ GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])
(* pretty printing functions for bigZ *)
let bigint_of_bigZ = function
- | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
- | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg ->
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigZ_neg ->
let opp_val = bigint_of_bigN one_arg in
if equal opp_val zero then
raise Non_closed
@@ -305,19 +281,19 @@ let uninterp_bigZ rc =
let _ = Notation.declare_numeral_interpreter bigZ_scope
(bigZ_path, bigZ_module)
interp_bigZ
- ([RRef (Util.dummy_loc, bigZ_pos);
- RRef (Util.dummy_loc, bigZ_neg)],
+ ([GRef (Util.dummy_loc, bigZ_pos);
+ GRef (Util.dummy_loc, bigZ_neg)],
uninterp_bigZ,
true)
(*** Parsing for bigQ in digital notation ***)
let interp_bigQ dloc n =
- let ref_z = RRef (dloc, bigQ_z) in
- RApp (dloc, ref_z, [interp_bigZ dloc n])
+ let ref_z = GRef (dloc, bigQ_z) in
+ GApp (dloc, ref_z, [interp_bigZ dloc n])
let uninterp_bigQ rc =
try match rc with
- | RApp (_, RRef(_,c), [one_arg]) when c = bigQ_z ->
+ | GApp (_, GRef(_,c), [one_arg]) when c = bigQ_z ->
Some (bigint_of_bigZ one_arg)
| _ -> None (* we don't pretty-print yet fractions *)
with Non_closed -> None
@@ -326,5 +302,5 @@ let uninterp_bigQ rc =
let _ = Notation.declare_numeral_interpreter bigQ_scope
(bigQ_path, bigQ_module)
interp_bigQ
- ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+ ([GRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
true)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:10:51 +0000