forked from caterinaurban/function
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbanal_int.ml
59 lines (41 loc) · 1.26 KB
/
banal_int.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
(*
Mathematical integers.
Copyright (C) 2011 Antoine Miné
*)
open Apron
include Z
let to_float_up (x:t) =
to_float x
let to_float_down (x:t) =
-. (to_float (neg x))
let of_float_up (x:float) : t =
of_float (ceil x)
let of_float_down (x:float) : t =
of_float (floor x)
(* apron and mlgmpidl *)
(* ****************** *)
external mpz_set: Mpz.t -> t -> unit = "ml_z_mlgmpidl_set_mpz"
external of_mpz: Mpz.t -> t = "ml_z_mlgmpidl_of_mpz"
let to_mpz (x:t) : Mpz.t = let z = Mpz.init () in mpz_set z x; z
let of_mpzf (x:Mpzf.t) : t = of_mpz (Mpzf._mpz x)
let to_mpzf (x:t) : Mpzf.t = Mpzf._mpzf (to_mpz x)
let of_mpqf_up x =
let n,d = of_mpzf (Mpqf.get_num x), of_mpzf (Mpqf.get_den x) in
if sign d = 0 then raise Overflow;
cdiv n d
let of_mpqf_down x =
let n,d = of_mpzf (Mpqf.get_num x), of_mpzf (Mpqf.get_den x) in
if sign d = 0 then raise Overflow;
fdiv n d
let to_mpqf x =
Mpqf.of_mpz (to_mpz x)
let to_apron x =
Scalar.Mpqf (to_mpqf x)
let of_apron_up = function
| Scalar.Float x -> of_float_up x
| Scalar.Mpqf x -> of_mpqf_up x
| _ -> invalid_arg "Int: unsupported Scalar type"
let of_apron_down = function
| Scalar.Float x -> of_float_down x
| Scalar.Mpqf x -> of_mpqf_down x
| _ -> invalid_arg "Int: unsupported Scalar type"