From c4945b0b834af16d2574945aebd9eb8dca9a9c24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 18 Feb 2019 16:29:59 +0100
Subject: [PATCH] [stdlib] Fixes some comments in ival and integer.mli.
---
src/kernel_services/abstract_interp/ival.ml | 6 +++---
src/kernel_services/abstract_interp/ival.mli | 12 ++++++------
src/libraries/stdlib/integer.mli | 4 ++--
3 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 94ff33306fc..eb88284cee5 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -751,7 +751,7 @@ let compute_r_common r1 m1 r2 m2 =
solutions (k1,k2) to (E2).
Let d = pgcd(m1,m2). There are solutions to (E2) only if d
- divides c (because d divides k1*m1 - k2*m2). Else we raise
+ divides r (because d divides k1*m1 - k2*m2). Else we raise
[Error_Bottom]. *)
let (x1,_,pgcd) = extended_euclidian_algorithm m1 m2 in
let r = Int.sub r2 r1 in
@@ -762,7 +762,7 @@ let compute_r_common r1 m1 r2 m2 =
(* The extended euclidian algorithm has provided solutions x1,x2 to
the Bezout identity x1*m1 + x2*m2 = d.
- x1*m1 + x2*m2 = d ==> x1*(c/d)*m1 + x2*(r/d)*m2 = d*(r/d).
+ x1*m1 + x2*m2 = d ==> x1*(r/d)*m1 + x2*(r/d)*m2 = d*(r/d).
Thus, k1 = x1*(r/d), k2=-x2*(r/d) are solutions to (E2)
Thus, x = r1 + x1*(r/d)*m1 is a particular solution to (E1). *)
@@ -1681,7 +1681,7 @@ let div x y =
elements [x mod f] for [x] in [v].
[scale_rem ~pos:true f v] is an over-approximation of the set of
- elements [x pos_rem f] for [x] in [v].
+ elements [x e_rem f] for [x] in [v].
*)
let scale_rem ~pos f v =
(* Format.printf "scale_rem %b %a %a@."
diff --git a/src/kernel_services/abstract_interp/ival.mli b/src/kernel_services/abstract_interp/ival.mli
index b4f3e5a485b..32218fd7746 100644
--- a/src/kernel_services/abstract_interp/ival.mli
+++ b/src/kernel_services/abstract_interp/ival.mli
@@ -237,25 +237,25 @@ val scale : Integer.t -> t -> t
val scale_div : pos:bool -> Integer.t -> t -> t
(** [scale_div ~pos:false f v] is an over-approximation of the set of
- elements [x / f] for [x] in [v].
+ elements [x c_div f] for [x] in [v].
[scale_div ~pos:true f v] is an over-approximation of the set of
- elements [x pos_div f] for [x] in [v]. *)
+ elements [x e_div f] for [x] in [v]. *)
val scale_div_under : pos:bool -> Integer.t -> t -> t
(** [scale_div_under ~pos:false f v] is an under-approximation of the
- set of elements [x / f] for [x] in [v].
+ set of elements [x c_div f] for [x] in [v].
[scale_div_under ~pos:true f v] is an under-approximation of the
- set of elements [x pos_div f] for [x] in [v]. *)
+ set of elements [x e_div f] for [x] in [v]. *)
val div : t -> t -> t (** Integer division *)
val scale_rem : pos:bool -> Integer.t -> t -> t
(** [scale_rem ~pos:false f v] is an over-approximation of the set of
- elements [x mod f] for [x] in [v].
+ elements [x c_rem f] for [x] in [v].
[scale_rem ~pos:true f v] is an over-approximation of the set of
- elements [x pos_rem f] for [x] in [v]. *)
+ elements [x e_rem f] for [x] in [v]. *)
val c_rem : t -> t -> t
val mul : t -> t -> t
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 8f6fffda546..58c641c2c80 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -61,7 +61,7 @@ val e_div : t -> t -> t
Equivalent to C division if both operands are positive.
Equivalent to a floored division if b > 0 (rounds downwards),
otherwise rounds upwards.
- Note: it is possible that pos_div (-a) b <> pos_div a (-b).
+ Note: it is possible that e_div (-a) b <> e_div a (-b).
*)
val e_rem : t -> t -> t
@@ -81,7 +81,7 @@ val c_rem : t -> t -> t
Implemented by [Z.rem] *)
val c_div_rem : t -> t -> t * t
-(** Remainder of the truncated division towards 0 (like in C99.
+(** [c_div_rem a b] returns [(c_div a b, c_rem a b)].
Implemented by [Z.div_rem] *)
val pgcd : t -> t -> t
--
GitLab