libapron-ocaml-dev 0.9.10-6 / usr / lib / ocaml / apron / polka.idl

/* -*- mode: c -*- */

/* This file is part of the APRON Library, released under LGPL license.  Please
   read the COPYING file packaged in the distribution */

quote(C,"#include \"pk.h\"")
quote(C,"#include \"pkeq.h\"")
quote(C,"#include \"ap_manager.h\"")
quote(C,"#include \"apron_caml.h\"")

quote(C,"typedef struct pk_internal_t* internal_ptr;")

import "manager.idl";

typedef [abstract] struct pk_internal_t* internal_ptr;

quote(MLMLI,"(** Convex Polyhedra and Linear Equalities abstract domains *)")

quote(MLMLI,"
type loose
type strict
  (** Two flavors for convex polyhedra: loose or strict.

      Loose polyhedra cannot have strict inequality constraints like [x>0].
      They are algorithmically more efficient
      (less generators, simpler normalization).

      Convex polyhedra are defined by the conjunction of a set of linear
      constraints of the form [a_0*x_0 + ... + a_n*x_n + b >= 0] or
      [a_0*x_0 + ... + a_n*x_n + b > 0]
      where [a_0, ..., a_n, b, c] are constants and [x_0, ..., x_n] variables.
  *)
type equalities
  (** Linear equalities.

      Linear equalities are conjunctions of linear
      equalities of the form [a_0*x_0 + ... + a_n*x_n + b = 0].
  *)
type 'a t
(** Type of convex polyhedra/linear equalities, where ['a] is [loose], [strict] or [equalities].

    Abstract values which are convex polyhedra have the type
    [(loose t) Apron.Abstract0.t] or [(loose t) Apron.Abstract1.t] or
    [(strict t) Apron.Abstract0.t] or [(strict t) Apron.Abstract1.t].

    Abstract values which are conjunction of linear equalities have the type
    [(equalities t) Apron.Abstract0.t] or [(equalities t) Apron.Abstract1.t].

    Managers allocated by NewPolka have the type ['a t Apron.Manager.t].
*)
")

quote(MLI,"(** Create a NewPolka manager for loose convex polyhedra. *)")
ap_manager_ptr pk_manager_alloc_loose()
quote(call,"
_res = pk_manager_alloc(false);
{ ap_exc_t i;
for (i=1; i<AP_EXC_SIZE; i++){
ap_manager_set_abort_if_exception(_res,i,false);
}}
");

quote(MLI,"(** Create a NewPolka manager for strict convex polyhedra. *)")
ap_manager_ptr pk_manager_alloc_strict()
quote(call,"_res = pk_manager_alloc(true);
{ ap_exc_t i;
for (i=1; i<AP_EXC_SIZE; i++){
ap_manager_set_abort_if_exception(_res,i,false);
}}
");

quote(MLI,"(** Create a NewPolka manager for conjunctions of linear equalities. *)")
ap_manager_ptr pk_manager_alloc_equalities()
quote(call,"_res = pkeq_manager_alloc();
{ ap_exc_t i;
for (i=1; i<AP_EXC_SIZE; i++){
ap_manager_set_abort_if_exception(_res,i,false);
}}
");

quote(MLI,"(** Get the internal submanager of a NewPolka manager. *)")
internal_ptr manager_get_internal(ap_manager_ptr man)
  quote(call,"_res = (internal_ptr)man->internal;");

quote(MLI,"(** Various options. See the C documentation *)\n")
void pk_set_max_coeff_size(internal_ptr pk, unsigned int size);
void pk_set_approximate_max_coeff_size(internal_ptr pk, unsigned int size);
int pk_get_max_coeff_size(internal_ptr pk);
int pk_get_approximate_max_coeff_size(internal_ptr pk);

quote(MLI,"(** {2 Type conversions} *)

val manager_is_polka : 'a Apron.Manager.t -> bool
val manager_is_polka_loose : 'a Apron.Manager.t -> bool
val manager_is_polka_strict : 'a Apron.Manager.t -> bool
val manager_is_polka_equalities : 'a Apron.Manager.t -> bool
  (** Return [true] iff the argument manager is a polka manager *)
val manager_of_polka : 'a t Apron.Manager.t -> 'b Apron.Manager.t
val manager_of_polka_loose : loose t Apron.Manager.t -> 'a Apron.Manager.t
val manager_of_polka_strict : strict t Apron.Manager.t -> 'a Apron.Manager.t
val manager_of_polka_equalities : equalities t Apron.Manager.t -> 'a Apron.Manager.t
  (** Makes a polka manager generic *)
val manager_to_polka : 'a Apron.Manager.t -> 'b t Apron.Manager.t
val manager_to_polka_loose : 'a Apron.Manager.t -> loose t Apron.Manager.t
val manager_to_polka_strict : 'a Apron.Manager.t -> strict t Apron.Manager.t
val manager_to_polka_equalities : 'a Apron.Manager.t -> equalities t Apron.Manager.t
  (** Instanciate the type of a polka manager. 
      Raises [Failure] if the argument manager is not a polka manager *)

module Abstract0 : sig
  val is_polka : 'a Apron.Abstract0.t -> bool
  val is_polka_loose : 'a Apron.Abstract0.t -> bool
  val is_polka_strict : 'a Apron.Abstract0.t -> bool
  val is_polka_equalities : 'a Apron.Abstract0.t -> bool
    (** Return [true] iff the argument manager is a polka value *)
  val of_polka : 'a t Apron.Abstract0.t -> 'b Apron.Abstract0.t
  val of_polka_loose : loose t Apron.Abstract0.t -> 'a Apron.Abstract0.t
  val of_polka_strict : strict t Apron.Abstract0.t -> 'a Apron.Abstract0.t
  val of_polka_equalities : equalities t Apron.Abstract0.t -> 'a Apron.Abstract0.t
    (** Makes a polka value generic *)
  val to_polka : 'a Apron.Abstract0.t -> 'b t Apron.Abstract0.t
  val to_polka_loose : 'a Apron.Abstract0.t -> loose t Apron.Abstract0.t
  val to_polka_strict : 'a Apron.Abstract0.t -> strict t Apron.Abstract0.t
  val to_polka_equalities : 'a Apron.Abstract0.t -> equalities t Apron.Abstract0.t
    (** Instanciate the type of a polka value.
	Raises [Failure] if the argument manager is not a polka manager *)
end

module Abstract1 : sig
  val is_polka : 'a Apron.Abstract1.t -> bool
  val is_polka_loose : 'a Apron.Abstract1.t -> bool
  val is_polka_strict : 'a Apron.Abstract1.t -> bool
  val is_polka_equalities : 'a Apron.Abstract1.t -> bool
    (** Return [true] iff the argument manager is a polka value *)
  val of_polka : 'a t Apron.Abstract1.t -> 'b Apron.Abstract1.t
  val of_polka_loose : loose t Apron.Abstract1.t -> 'a Apron.Abstract1.t
  val of_polka_strict : strict t Apron.Abstract1.t -> 'a Apron.Abstract1.t
  val of_polka_equalities : equalities t Apron.Abstract1.t -> 'a Apron.Abstract1.t
    (** Makes a polka value generic *)
  val to_polka : 'a Apron.Abstract1.t -> 'b t Apron.Abstract1.t
  val to_polka_loose : 'a Apron.Abstract1.t -> loose t Apron.Abstract1.t
  val to_polka_strict : 'a Apron.Abstract1.t -> strict t Apron.Abstract1.t
  val to_polka_equalities : 'a Apron.Abstract1.t -> equalities t Apron.Abstract1.t
    (** Instanciate the type of a polka value.
	Raises [Failure] if the argument manager is not a polka manager *)
end
")

quote(ML,"
let manager_is_polka man =
  let str = Apron.Manager.get_library man in
  let str =
    try String.sub str 0 5
    with Invalid_argument _ -> \"\"
  in
  (String.compare str \"polka\")==0
let manager_of_polka (man:'a t Apron.Manager.t) : 'b Apron.Manager.t = Obj.magic man
let manager_to_polka (man:'a Apron.Manager.t) : 'b t Apron.Manager.t =
  if manager_is_polka man then
    Obj.magic man
  else
    failwith \"Polka.to_polka: the argument manager is not a Polka manager\"

let manager_is_polka_loose man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"polka, loose mode\")==0
let manager_of_polka_loose (man:loose t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_polka_loose (man:'a Apron.Manager.t) : loose t Apron.Manager.t =
  if manager_is_polka_loose man then
    Obj.magic man
  else
    failwith \"Polka.to_polka_loose: the argument manager is not a loose Polka manager\"

let manager_is_polka_strict man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"polka, strict mode\")==0
let manager_of_polka_strict (man:strict t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_polka_strict (man:'a Apron.Manager.t) : strict t Apron.Manager.t =
  if manager_is_polka_strict man then
    Obj.magic man
  else
    failwith \"Polka.to_polka_strict: the argument manager is not a strict Polka manager\"

let manager_is_polka_equalities man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"polka, equalities mode\")==0
let manager_of_polka_equalities (man:equalities t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_polka_equalities (man:'a Apron.Manager.t) : equalities t Apron.Manager.t =
  if manager_is_polka_equalities man then
    Obj.magic man
  else
    failwith \"Polka.to_polka_equalities: the argument manager is not an equalities Polka manager\"

module Abstract0 = struct
  let is_polka abs =
    manager_is_polka (Apron.Abstract0.manager abs)
  let is_polka_loose abs =
    manager_is_polka_loose (Apron.Abstract0.manager abs)
  let is_polka_strict abs =
    manager_is_polka (Apron.Abstract0.manager abs)
  let is_polka_equalities abs =
    manager_is_polka_equalities (Apron.Abstract0.manager abs)
  let of_polka (abs: 'a t Apron.Abstract0.t) : 'b Apron.Abstract0.t = Obj.magic abs
  let of_polka_loose (abs: loose t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let of_polka_strict (abs: strict t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let of_polka_equalities (abs: equalities t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let to_polka (abs:'a Apron.Abstract0.t) : 'b t Apron.Abstract0.t =
    if is_polka abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract0.to_polka: the argument value is not a polka value\"
  let to_polka_loose (abs:'a Apron.Abstract0.t) : loose t Apron.Abstract0.t =
    if is_polka_loose abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract0.to_polka_loose: the argument value is not a loose polka value\"
  let to_polka_strict (abs:'a Apron.Abstract0.t) : strict t Apron.Abstract0.t =
    if is_polka_strict abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract0.to_polka_strict: the argument value is not a strict polka value\"
  let to_polka_equalities (abs:'a Apron.Abstract0.t) : equalities t Apron.Abstract0.t =
    if is_polka_equalities abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract0.to_polka_equalities: the argument value is not an equalities polka value\"
end

module Abstract1 = struct
  let is_polka abs =
    manager_is_polka (Apron.Abstract1.manager abs)
  let is_polka_loose abs =
    manager_is_polka_loose (Apron.Abstract1.manager abs)
  let is_polka_strict abs =
    manager_is_polka (Apron.Abstract1.manager abs)
  let is_polka_equalities abs =
    manager_is_polka_equalities (Apron.Abstract1.manager abs)
  let of_polka (abs: 'a t Apron.Abstract1.t) : 'b Apron.Abstract1.t = Obj.magic abs
  let of_polka_loose (abs: loose t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let of_polka_strict (abs: strict t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let of_polka_equalities (abs: equalities t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let to_polka (abs:'a Apron.Abstract1.t) : 'b t Apron.Abstract1.t =
    if is_polka abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract1.to_polka: the argument value is not a polka value\"
  let to_polka_loose (abs:'a Apron.Abstract1.t) : loose t Apron.Abstract1.t =
    if is_polka_loose abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract1.to_polka_loose: the argument value is not a loose polka value\"
  let to_polka_strict (abs:'a Apron.Abstract1.t) : strict t Apron.Abstract1.t =
    if is_polka_strict abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract1.to_polka_strict: the argument value is not a strict polka value\"
  let to_polka_equalities (abs:'a Apron.Abstract1.t) : equalities t Apron.Abstract1.t =
    if is_polka_equalities abs then
      Obj.magic abs
    else
      failwith \"Polka.Abstract1.to_polka_equalities: the argument value is not an equalities polka value\"
end
")

quote(MLI,"\n(**
{2 Compilation information}

See {!Introduction.compilation} for complete explanations. 
We just show examples with the file [mlexample.ml].

{3 Bytecode compilation}

{[ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.byte \\
  bigarray.cma gmp.cma apron.cma polkaMPQ.cma mlexample.ml]}

{[ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \\
  bigarray.cma gmp.cma apron.cma polkaMPQ.cma

ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \\
  bigarray.cma gmp.cma apron.cma polkaMPQ.cma mlexample.ml ]}

{3 Native-code compilation}

{[ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \\
  bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa mlexample.ml ]}

{3 Without auto-linking feature}

{[ocamlopt -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \\
  bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa mlexample.ml \\
  -cclib \"-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib \\
	  -lpolkaMPQ_caml_debug -lpolkaMPQ_debug \\
	  -lapron_caml_debug -lapron_debug \\
	  -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \\
	  -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \\
	  -lbigarray\" ]}

*)")