Merge pull request antoinemine#108 from antoinemine/fix/compare

Fix and document comparisons in OCaml bindings

apron/ap_linexpr0.h

@@ -292,7 +292,9 @@ long ap_linexpr0_hash(ap_linexpr0_t* expr);
 bool ap_linexpr0_equal(ap_linexpr0_t* expr1,
 		    ap_linexpr0_t* expr2);
 
-/* Lexicographic ordering, terminating by constant coefficients */
+/* Lexicographic partial ordering, terminating by constant coefficients.
+  Returns a value between -3 and 3 (as ap_coeff_cmp).
+*/
 int ap_linexpr0_compare(ap_linexpr0_t* expr1,
 		     ap_linexpr0_t* expr2);
 

apron/apron.texi

@@ -3666,9 +3666,10 @@ Equality test.
 @end deftypefun
 
 @deftypefun int ap_linexpr0_compare (ap_linexpr0_t* @var{e1}, ap_linexpr0_t* @var{e2})
-Lexicographic ordering, terminating by constant coefficients.
+Lexicographic partial ordering, terminating by constant coefficients.
+Returns a value between -3 and 3 (as ap_coeff_cmp).
 
-Use the (partial order) comparison function on coefficients
+Use the partial order comparison function on coefficients
 @code{coeff_cmp}.
 @end deftypefun
 

mlapronidl/abstract0.idl

@@ -33,7 +33,6 @@ struct ap_abstract0_ptr ap_abstract0_ptr;
 quote(MLMLI,"(** APRON Abstract value of level 0 *)")
 quote(MLMLI,"(** The type parameter ['a] allows to distinguish abstract values with different underlying abstract domains. *)\n")
 
-quote(MLI,"\n(** TO BE DOCUMENTED *)")
 void ap_abstract0_set_gc(int size)
      quote(call,"camlidl_apron_heap = size;");
 
@@ -132,6 +131,14 @@ quote(MLMLI,"(* ============================================================ *)"
 quote(MLMLI,"(** {3 Tests} *)")
 quote(MLMLI,"(* ============================================================ *)")
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Abstract elements are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [is_eq] and [is_leq] instead.\n\
+*)\n\n");
+
 quote(MLI,"\n(** Emptiness test *)")
 boolean ap_abstract0_is_bottom(ap_manager_ptr man, ap_abstract0_ptr a)
      quote(dealloc,"I0_CHECK_EXC(man)");

mlapronidl/abstract1.idl

@@ -156,7 +156,15 @@ quote(MLMLI,"(** {3 Tests} *)\n")
 quote(MLMLI,"(* ============================================================ *)")
 
 quote(MLI,"\n\
-(** Emptiness test *)
+(**\n\
+  NOTE: Abstract elements are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [is_eq] and [is_leq] instead.\n\
+*)\n\n");
+
+quote(MLI,"\n\
+(** Emptiness test *)\n\
 val is_bottom : 'a Manager.t -> 'a t -> bool\n\
 \n\
 (** Universality test *)
@@ -167,11 +175,11 @@ let is_bottom man x = Abstract0.is_bottom man x.abstract0\n\
 let is_top man x = Abstract0.is_top man x.abstract0\n\
 ")
 
-quote(MLI,"\n(** Inclusion test. The 2 abstract values should be compatible. *)")
+quote(MLI,"\n(** Inclusion test. The two abstract values should be compatible. *)")
 boolean ap_abstract1_is_leq(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
     quote(dealloc,"I0_CHECK_EXC(man)");
 
-quote(MLI,"\n(** Equality test. The 2 abstract values should be compatible. *)")
+quote(MLI,"\n(** Equality test. The two abstract values should be compatible. *)")
 boolean ap_abstract1_is_eq(ap_manager_ptr man, [ref]struct ap_abstract1_t* a1, [ref]struct ap_abstract1_t* a2)
     quote(dealloc,"I0_CHECK_EXC(man)");
 
@@ -183,7 +191,7 @@ quote(MLI,"\n(** Does the abstract value satisfy the tree expression constraint
 boolean ap_abstract1_sat_tcons(ap_manager_ptr man, [ref]struct ap_abstract1_t* a, [ref]struct ap_tcons1_t* v)
     quote(dealloc,"I0_CHECK_EXC(man)");
 
-quote(MLI,"\n(** Does the abstract value satisfy the constraint [dim in interval] ? *)")
+quote(MLI,"\n(** Does the abstract value satisfy the constraint [dim] in [interval]? *)")
 boolean ap_abstract1_sat_interval(ap_manager_ptr man, [ref]struct ap_abstract1_t* a,
 				  ap_var_t v1,
 				  [ref]struct ap_interval_t* v2)

mlapronidl/apron_caml.c

@@ -72,18 +72,27 @@ long camlidl_apron_linexpr0_ptr_hash(value v)
   ap_linexpr0_t* p = *(ap_linexpr0_ptr *) Data_custom_val(v);
   return ap_linexpr0_hash(p);
 }
+
+/* We no longer implement the polymorphic comparison function as
+   we do not have a natural total order, which is assumed by
+   its semantic. The previous implementation led to inconsistent
+   behavior and was confusing.
+ */
+
+/*
 static
 int camlidl_apron_linexpr0_ptr_compare(value v1, value v2)
 {
   ap_linexpr0_t* p1 = *(ap_linexpr0_ptr *) Data_custom_val(v1);
   ap_linexpr0_t* p2 = *(ap_linexpr0_ptr *) Data_custom_val(v2);
   return ap_linexpr0_compare(p1,p2);
 }
+*/
 
 struct custom_operations camlidl_apron_custom_linexpr0_ptr = {
   "apl0",
   camlidl_apron_linexpr0_ptr_finalize,
-  camlidl_apron_linexpr0_ptr_compare,
+  custom_compare_default /*camlidl_apron_linexpr0_ptr_compare*/,
   camlidl_apron_linexpr0_ptr_hash,
   custom_serialize_default,
   custom_deserialize_default,
@@ -185,18 +194,21 @@ long camlidl_apron_texpr0_ptr_hash(value v)
   ap_texpr0_t* p = *(ap_texpr0_ptr *) Data_custom_val(v);
   return ap_texpr0_hash(p);
 }
+
+/*
 static
 int camlidl_apron_texpr0_ptr_compare(value v1, value v2)
 {
   ap_texpr0_t* p1 = *(ap_texpr0_ptr *) Data_custom_val(v1);
   ap_texpr0_t* p2 = *(ap_texpr0_ptr *) Data_custom_val(v2);
   return ap_texpr0_equal(p1,p2) ? 0 : (p1<p2 ? (-1) : 1);
 }
+*/
 
 struct custom_operations camlidl_apron_custom_texpr0_ptr = {
   "apl0",
   camlidl_apron_texpr0_ptr_finalize,
-  camlidl_apron_texpr0_ptr_compare,
+  custom_compare_default /*camlidl_apron_texpr0_ptr_compare*/,
   camlidl_apron_texpr0_ptr_hash,
   custom_serialize_default,
   custom_deserialize_default,
@@ -219,6 +231,7 @@ void camlidl_apron_manager_ptr_finalize(value v)
   ap_manager_free(p);
 }
 
+/*
 static
 int camlidl_apron_manager_ptr_compare(value v1, value v2)
 {
@@ -229,11 +242,12 @@ int camlidl_apron_manager_ptr_compare(value v1, value v2)
   res = (p1==p2 || p1->library==p2->library) ? 0 : ((p1<p2) ? (-1) : 1);
   CAMLreturn(res);
 }
+*/
 
 struct custom_operations camlidl_apron_custom_manager_ptr = {
   "apman",
   camlidl_apron_manager_ptr_finalize,
-  camlidl_apron_manager_ptr_compare,
+  custom_compare_default /*camlidl_apron_manager_ptr_compare*/,
   custom_hash_default,
   custom_serialize_default,
   custom_deserialize_default,
@@ -278,6 +292,8 @@ long camlidl_apron_abstract0_ptr_hash(value v)
   if (a->man->result.exn!=AP_EXC_NONE) camlidl_apron_manager_check_exception(a->man,NULL);
   return res;
 }
+
+/*
 static
 int camlidl_apron_abstract0_ptr_compare(value v1, value v2)
 {
@@ -306,6 +322,7 @@ int camlidl_apron_abstract0_ptr_compare(value v1, value v2)
   }
   return res;
 }
+*/
 
 /* global manager used for deserialization */
 static ap_manager_ptr deserialize_man = NULL;
@@ -352,7 +369,7 @@ unsigned long camlidl_apron_abstract0_deserialize(void * dst)
 struct custom_operations camlidl_apron_custom_abstract0_ptr = {
   "apa0",
   camlidl_apron_abstract0_ptr_finalize,
-  camlidl_apron_abstract0_ptr_compare,
+  custom_compare_default /*camlidl_apron_abstract0_ptr_compare*/,
   camlidl_apron_abstract0_ptr_hash,
   camlidl_apron_abstract0_serialize,
   camlidl_apron_abstract0_deserialize,
@@ -445,6 +462,8 @@ long camlidl_apron_environment_ptr_hash(value v)
   int res = ap_environment_hash(e);
   CAMLreturn(res);
 }
+
+/*
 static
 int camlidl_apron_environment_ptr_compare(value v1, value v2)
 {
@@ -455,11 +474,12 @@ int camlidl_apron_environment_ptr_compare(value v1, value v2)
   res = ap_environment_compare(env1,env2);
   CAMLreturn(res);
 }
+*/
 
 struct custom_operations camlidl_apron_custom_environment_ptr = {
   "ape",
   camlidl_apron_environment_ptr_finalize,
-  camlidl_apron_environment_ptr_compare,
+  custom_compare_default /*camlidl_apron_environment_ptr_compare*/,
   camlidl_apron_environment_ptr_hash,
   custom_serialize_default,
   custom_deserialize_default,
@@ -540,6 +560,7 @@ void camlidl_apron_policy_ptr_finalize(value v)
   ap_policy_free(a->pman,a);
 }
 
+/*
 static
 int camlidl_apron_policy_ptr_compare(value v1, value v2)
 {
@@ -554,6 +575,8 @@ int camlidl_apron_policy_ptr_compare(value v1, value v2)
     res = (int)(a1-a2);
   return res;
 }
+*/
+
 static
 long camlidl_apron_policy_ptr_hash(value v)
 {
@@ -568,7 +591,7 @@ long camlidl_apron_policy_ptr_hash(value v)
 struct custom_operations camlidl_apron_custom_policy_ptr = {
   "appolicy",
   camlidl_apron_policy_ptr_finalize,
-  camlidl_apron_policy_ptr_compare,
+  custom_compare_default /*camlidl_apron_policy_ptr_compare*/,
   camlidl_apron_policy_ptr_hash,
   custom_serialize_default,
   custom_deserialize_default,

mlapronidl/environment.idl

@@ -33,6 +33,14 @@ struct ap_environment_ptr ap_environment_ptr;
 
 quote(MLMLI,"(** APRON Environments binding dimensions to names *)")
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Environments are not totally ordered.
+  As of 0.9.15, environments do not implement the polymorphic [compare] function to avoid confusion.\n \
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [equal] and [cmp] to compare environments.\n\
+*)\n\n");
+
 quote(MLI,"\n(** Making an environment from a set of integer and real variables. Raise [Failure] in case of name conflict. *)")
 
 ap_environment_ptr ap_environment_make([size_is(intdim)]ap_var_t* name_of_intdim,
@@ -206,16 +214,17 @@ if (_res==NULL){\n\
 ")
 quote(dealloc,"ap_dimchange2_free(_res);")
 ;
-quote(MLI,"\n(** Test equality if two environments *)")
+quote(MLI,"\n(** Test the equality of two environments *)")
 boolean ap_environment_equal(ap_environment_ptr env1,
 			     ap_environment_ptr env2)
   quote(call,"\n\
 _res = ap_environment_is_eq(env1,env2);\n\
 ");
 
-quote(MLI,"\n(** Compare two environment. [compare env1 env2] return [-2] if the environments are not compatible (a variable has different types in the 2 environments), [-1] if [env1] is a subset of env2, [0] if equality,  [+1] if env1 is a superset of env2, and [+2] otherwise (the lce exists and is a strict superset of both) *)")
-int ap_environment_compare(ap_environment_ptr env1,
-			   ap_environment_ptr env2);
+quote(MLI,"\n(** Compare two environment. [cmp env1 env2] return [-2] if the environments are not compatible (a variable has different types in the 2 environments), [-1] if [env1] is a subset of env2, [0] if equality,  [+1] if env1 is a superset of env2, and [+2] otherwise (the lce exists and is a strict superset of both). This is not a total order, and cannot be used as comparison function when a total order is needed (e.g., in [Set.Make]). The function has been renamed from [compare] to avoid confusion. *)")
+int ap_environment_cmp(ap_environment_ptr env1,
+		       ap_environment_ptr env2)
+ quote(call, "_res = ap_environment_compare(env1, env2);");
 
 quote(MLI,"\n(** Hashing function for environments *)")
 int ap_environment_hash(ap_environment_ptr env);

mlapronidl/generator0.idl

@@ -42,6 +42,13 @@ struct ap_generator0_array_t {
   int size;
 };
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Generators are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+*)\n\n");
+
 quote(MLI,"\n\
 (** Making a generator. The constant coefficient of the linear expression is\n\
   ignored. Modifying later the linear expression modifies correspondingly the\n\

mlapronidl/generator1.idl

@@ -31,6 +31,13 @@ struct ap_generator1_array_t {
 };
 quote(MLMLI,"(** APRON Generators and array of generators of level 1 *)")
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Generators are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+*)\n\n");
+
 quote(MLMLI,"\n\
 type typ = Generator0.typ = \n\
   | LINE\n\

mlapronidl/linexpr0.idl

@@ -24,6 +24,14 @@ typedef [abstract,
 	 c2ml(camlidl_apron_linexpr0_ptr_c2ml)]
 struct ap_linexpr0_ptr* ap_linexpr0_ptr;
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Linear expressions are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [equal] and [cmp] instead.\n\
+*)\n\n");
+
 quote(MLI,"(** Create a linear expression. Its representation is sparse if [None] is provided, dense of size [size] if [Some size] is provided. *)")
 ap_linexpr0_ptr ap_linexpr0_make([unique]int* size)
      quote(call,"\n\
@@ -48,8 +56,12 @@ void ap_linexpr0_minimize(ap_linexpr0_ptr a);
 quote(MLI,"(** Copy *)")
 ap_linexpr0_ptr ap_linexpr0_copy(const ap_linexpr0_ptr a);
 
-quote(MLI,"(** Comparison with lexicographic ordering using Coeff.cmp, terminating by constant *)")
-int ap_linexpr0_compare(const ap_linexpr0_ptr a, const ap_linexpr0_ptr b);
+quote(MLI,"(** Comparison with lexicographic ordering using [Coeff.cmp], terminating by constant. This is a partial ordrer; as [Coeff.cmp] it returns an integer between -3 and 3. It cannot be used when a total order is required (e.g., in [Set.Make]).*)")
+int ap_linexpr0_cmp(const ap_linexpr0_ptr a, const ap_linexpr0_ptr b)
+  quote(call, "_res = ap_linexpr0_compare(a, b);");
+
+quote(MLI,"(** Equality comparison *)")
+boolean ap_linexpr0_equal(const ap_linexpr0_ptr a, const ap_linexpr0_ptr b);
 
 quote(MLI,"(** Hashing function *)")
 int ap_linexpr0_hash(const ap_linexpr0_ptr a);

mlapronidl/linexpr1.idl

@@ -19,6 +19,14 @@ struct ap_linexpr1_t {
   [mlname(mutable_env)] ap_environment_ptr env;
 };
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Linear expressions are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [Linexpr0.equal] and [Linexpr0.cmp] on the [linexpr0] field instead.\n\
+*)\n\n");
+
 quote(MLI,"\n\n\
 (** Build a linear expression defined on the given argument, which is sparse by\n\
   default. *)\n\

mlapronidl/manager.idl

@@ -163,7 +163,12 @@ quote(MLMLI,"(** Concerning the other types,\n\n\
 - [exclog] defines the exceptions raised by APRON functions.\n\n\
 *)\n")
 
-
+quote(MLI,"\n\
+(**\n\
+  NOTE: Managers are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+*)\n\n");
 
 quote(MLI,"(** Get the name of the effective library which allocated the manager *)")
 [string]const char* ap_manager_get_library(ap_manager_ptr man);

mlapronidl/scalar.idl

@@ -124,8 +124,8 @@ val sgn : t -> int\n\
 \n\
 val cmp : t -> t -> int\n\
   (** Compare two coefficients, possibly converting to [Mpqf.t].\n\
-    [compare x y] returns a negative number if [x] is less than [y], \n\
-    [0] if they ar equal, and a positive number if [x] is greater than [y].\n\
+    [cmp x y] returns a negative number if [x] is less than [y], \n\
+    [0] if they are equal, and a positive number if [x] is greater than [y].\n\
   *)\n\
 \n\
 val cmp_int : t -> int -> int\n\

mlapronidl/texpr0.idl

@@ -8,6 +8,14 @@
 
 quote(MLI,"(** APRON tree expressions of level 0 *)\n")
 
+quote(MLI,"\n\
+(**\n\
+  NOTE: Expressions are not totally ordered.\n\
+  As of 0.9.15, they do not implement the polymorphic [compare] function to avoid confusion.\n\
+  As a consequence, the polymorphic [=], [<=], etc. operators cannot be used.\n\
+  Use [equal] instead.\n\
+*)\n\n");
+
 quote(C, "\n\
 #include <limits.h>\n\
 #include \"ap_texpr0.h\"\n\
@@ -263,6 +271,12 @@ boolean ap_texpr0_is_interval_polynomial(ap_texpr0_ptr a);
 boolean ap_texpr0_is_interval_polyfrac(ap_texpr0_ptr a);
 boolean ap_texpr0_is_scalar(ap_texpr0_ptr a);
 
+quote(MLI,"(** Equality test *)")
+boolean ap_texpr0_equal(ap_texpr0_ptr a, ap_texpr0_ptr b);
+
+quote(MLI,"(** Hashing function *)")
+int ap_texpr0_hash(ap_texpr0_ptr a);
+
 quote(MLMLI,"\n(** {2 Printing} *)\n")
 
 quote(MLI,"\n\