libapron-ocaml-dev 0.9.10-7 / usr / lib / ocaml / apron / ppl.idl

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

/*
 * ppl.idl
 *
 * OCaml interface specification for camlidl
 *
 * APRON Library / PPL library wrapper
 *
 * Copyright (C) Antoine Mine' 2006
 *
 */

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

quote(C,"/*\n This file is part of the APRON Library, released under GPL license.\n Please read the COPYING file packaged in the distribution.\n*/")
quote(MLMLI,"(*\n This file is part of the APRON Library, released under GPL license.\n Please read the COPYING file packaged in the distribution.\n*)\n")


quote(C,"#include \"ap_ppl.h\"")
quote(C,"#include \"apron_caml.h\"")

quote(C,"#define I0_CHECK_EXC(man) if (man->result.exn!=AP_EXC_NONE){ value v = camlidl_c2ml_manager_struct_ap_exclog_t(man->result.exclog,_ctx); caml_raise_with_arg(*caml_named_value(\"apron exception\"),v); } ")

import "manager.idl";

quote(MLMLI,"(** Convex Polyhedra and Linear Congruences abstract domains (PPL wrapper) *)\n")

quote(MLMLI,"(** This module is a wrapper around the Parma Polyhedra Library. *)\n\n")


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 grid
  (** Linear congruences.

      Linear congruences are defined by the conjunction of equality constraints
      modulo a rational number, of the form [a_0*x_0 + ... + a_n*x_n = b mod c],
      where [a_0, ..., a_n, b, c] are constants and [x_0, ..., x_n] variables.
  *)

type 'a t
(** Type of convex polyhedra/linear congruences, where ['a] is [loose], [strict] or [grid].

    Abstract values which are convex polyhedra have the type
    [loose t Apron.AbstractX.t] or [strict t Apron.AbstractX.t].
    Abstract values which are conjunction of linear congruences equalities have the type
    [grid t Apron.AbstractX.t].
    Managers allocated by PPL have the type ['a t Apron.Manager.t].
*)
")

quote(MLI,"(** Allocate a PPL manager for loose convex polyhedra. *)")
ap_manager_ptr ap_ppl_manager_alloc_loose()
quote(call,"_res = ap_ppl_poly_manager_alloc(false);");

quote(MLI,"(** Allocate a PPL manager for strict convex polyhedra. *)")
ap_manager_ptr ap_ppl_manager_alloc_strict()
quote(call,"_res = ap_ppl_poly_manager_alloc(true);");

quote(MLI,"(** Allocate a new manager for linear congruences (grids) *)")
ap_manager_ptr ap_ppl_manager_alloc_grid()
quote(call,"_res = ap_ppl_grid_manager_alloc();");

quote(MLI,"(** {2 Type conversions} *)
val manager_is_ppl : 'a Apron.Manager.t -> bool
val manager_is_ppl_loose : 'a Apron.Manager.t -> bool
val manager_is_ppl_strict : 'a Apron.Manager.t -> bool
val manager_is_ppl_grid : 'a Apron.Manager.t -> bool
  (** Return [true] iff the argument manager is a ppl manager *)
val manager_of_ppl : 'a t Apron.Manager.t -> 'b Apron.Manager.t
val manager_of_ppl_loose : loose t Apron.Manager.t -> 'a Apron.Manager.t
val manager_of_ppl_strict : strict t Apron.Manager.t -> 'a Apron.Manager.t
val manager_of_ppl_grid : grid t Apron.Manager.t -> 'a Apron.Manager.t
  (** Make a ppl manager generic *)
val manager_to_ppl : 'a Apron.Manager.t -> 'b t Apron.Manager.t
val manager_to_ppl_loose : 'a Apron.Manager.t -> loose t Apron.Manager.t
val manager_to_ppl_strict : 'a Apron.Manager.t -> strict t Apron.Manager.t
val manager_to_ppl_grid : 'a Apron.Manager.t -> grid t Apron.Manager.t
  (** Instanciate the type of a ppl manager.
      Raises [Failure] if the argument manager is not a ppl manager *)

module Abstract0 : sig
  val is_ppl : 'a Apron.Abstract0.t -> bool
  val is_ppl_loose : 'a Apron.Abstract0.t -> bool
  val is_ppl_strict : 'a Apron.Abstract0.t -> bool
  val is_ppl_grid : 'a Apron.Abstract0.t -> bool
    (** Return [true] iff the argument manager is a ppl value *)
  val of_ppl : 'a t Apron.Abstract0.t -> 'b Apron.Abstract0.t
  val of_ppl_loose : loose t Apron.Abstract0.t -> 'a Apron.Abstract0.t
  val of_ppl_strict : strict t Apron.Abstract0.t -> 'a Apron.Abstract0.t
  val of_ppl_grid : grid t Apron.Abstract0.t -> 'a Apron.Abstract0.t
    (** Make a ppl value generic *)
  val to_ppl : 'a Apron.Abstract0.t -> 'b t Apron.Abstract0.t
  val to_ppl_loose : 'a Apron.Abstract0.t -> loose t Apron.Abstract0.t
  val to_ppl_strict : 'a Apron.Abstract0.t -> strict t Apron.Abstract0.t
  val to_ppl_grid : 'a Apron.Abstract0.t -> grid t Apron.Abstract0.t
    (** Instanciate the type of a ppl value.
	Raises [Failure] if the argument manager is not a ppl manager *)
end

module Abstract1 : sig
  val is_ppl : 'a Apron.Abstract1.t -> bool
  val is_ppl_loose : 'a Apron.Abstract1.t -> bool
  val is_ppl_strict : 'a Apron.Abstract1.t -> bool
  val is_ppl_grid : 'a Apron.Abstract1.t -> bool
    (** Return [true] iff the argument manager is a ppl value *)
  val of_ppl : 'a t Apron.Abstract1.t -> 'b Apron.Abstract1.t
  val of_ppl_loose : loose t Apron.Abstract1.t -> 'a Apron.Abstract1.t
  val of_ppl_strict : strict t Apron.Abstract1.t -> 'a Apron.Abstract1.t
  val of_ppl_grid : grid t Apron.Abstract1.t -> 'a Apron.Abstract1.t
    (** Make a ppl value generic *)
  val to_ppl : 'a Apron.Abstract1.t -> 'b t Apron.Abstract1.t
  val to_ppl_loose : 'a Apron.Abstract1.t -> loose t Apron.Abstract1.t
  val to_ppl_strict : 'a Apron.Abstract1.t -> strict t Apron.Abstract1.t
  val to_ppl_grid : 'a Apron.Abstract1.t -> grid t Apron.Abstract1.t
    (** Instanciate the type of a ppl value.
	Raises [Failure] if the argument manager is not a ppl manager *)
end
")

quote(ML,"
let manager_is_ppl man =
  let str = Apron.Manager.get_library man in
  let str =
    try String.sub str 0 3
    with Invalid_argument _ -> \"\"
  in
  (String.compare str \"PPL\")==0
let manager_of_ppl (man:'a t Apron.Manager.t) : 'b Apron.Manager.t = Obj.magic man
let manager_to_ppl (man:'a Apron.Manager.t) : 'b t Apron.Manager.t =
  if manager_is_ppl man then
    Obj.magic man
  else
    failwith \"Ppl.to_ppl: the argument manager is not a Ppl manager\"

let manager_is_ppl_loose man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"PPL::Polyhedron, loose mode\")==0
let manager_of_ppl_loose (man:loose t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_ppl_loose (man:'a Apron.Manager.t) : loose t Apron.Manager.t =
  if manager_is_ppl_loose man then
    Obj.magic man
  else
    failwith \"Ppl.to_ppl_loose: the argument manager is not a loose Ppl manager\"

let manager_is_ppl_strict man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"PPL::Polyhedron, strict mode\")==0
let manager_of_ppl_strict (man:strict t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_ppl_strict (man:'a Apron.Manager.t) : strict t Apron.Manager.t =
  if manager_is_ppl_strict man then
    Obj.magic man
  else
    failwith \"Ppl.to_ppl_strict: the argument manager is not a strict Ppl manager\"

let manager_is_ppl_grid man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"PPL::Grid\")==0
let manager_of_ppl_grid (man:grid t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_ppl_grid (man:'a Apron.Manager.t) : grid t Apron.Manager.t =
  if manager_is_ppl_grid man then
    Obj.magic man
  else
    failwith \"Ppl.to_ppl_grid: the argument manager is not a grid Ppl manager\"

module Abstract0 = struct
  let is_ppl abs =
    manager_is_ppl (Apron.Abstract0.manager abs)
  let is_ppl_loose abs =
    manager_is_ppl_loose (Apron.Abstract0.manager abs)
  let is_ppl_strict abs =
    manager_is_ppl (Apron.Abstract0.manager abs)
  let is_ppl_grid abs =
    manager_is_ppl_grid (Apron.Abstract0.manager abs)
  let of_ppl (abs: 'a t Apron.Abstract0.t) : 'b Apron.Abstract0.t = Obj.magic abs
  let of_ppl_loose (abs: loose t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let of_ppl_strict (abs: strict t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let of_ppl_grid (abs: grid t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let to_ppl (abs:'a Apron.Abstract0.t) : 'b t Apron.Abstract0.t =
    if is_ppl abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract0.to_ppl: the argument value is not a ppl value\"
  let to_ppl_loose (abs:'a Apron.Abstract0.t) : loose t Apron.Abstract0.t =
    if is_ppl_loose abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract0.to_ppl_loose: the argument value is not a loose ppl value\"
  let to_ppl_strict (abs:'a Apron.Abstract0.t) : strict t Apron.Abstract0.t =
    if is_ppl_strict abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract0.to_ppl_strict: the argument value is not a strict ppl value\"
  let to_ppl_grid (abs:'a Apron.Abstract0.t) : grid t Apron.Abstract0.t =
    if is_ppl_grid abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract0.to_ppl_grid: the argument value is not a grid ppl value\"
end

module Abstract1 = struct
  let is_ppl abs =
    manager_is_ppl (Apron.Abstract1.manager abs)
  let is_ppl_loose abs =
    manager_is_ppl_loose (Apron.Abstract1.manager abs)
  let is_ppl_strict abs =
    manager_is_ppl (Apron.Abstract1.manager abs)
  let is_ppl_grid abs =
    manager_is_ppl_grid (Apron.Abstract1.manager abs)
  let of_ppl (abs: 'a t Apron.Abstract1.t) : 'b Apron.Abstract1.t = Obj.magic abs
  let of_ppl_loose (abs: loose t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let of_ppl_strict (abs: strict t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let of_ppl_grid (abs: grid t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let to_ppl (abs:'a Apron.Abstract1.t) : 'b t Apron.Abstract1.t =
    if is_ppl abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract1.to_ppl: the argument value is not a ppl value\"
  let to_ppl_loose (abs:'a Apron.Abstract1.t) : loose t Apron.Abstract1.t =
    if is_ppl_loose abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract1.to_ppl_loose: the argument value is not a loose ppl value\"
  let to_ppl_strict (abs:'a Apron.Abstract1.t) : strict t Apron.Abstract1.t =
    if is_ppl_strict abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract1.to_ppl_strict: the argument value is not a strict ppl value\"
  let to_ppl_grid (abs:'a Apron.Abstract1.t) : grid t Apron.Abstract1.t =
    if is_ppl_grid abs then
      Obj.magic abs
    else
      failwith \"Ppl.Abstract1.to_ppl_grid: the argument value is not a grid ppl value\"
end
")

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

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

Do not forget the [-cc \"g++\"] option: PPL is a C++ library which requires
a C++ linker.

{3 Bytecode compilation}

{[ocamlc -cc \"g++\"-I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.byte \\
  bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml]}

{[ocamlc -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -make-runtime -o myrun \\
  bigarray.cma gmp.cma apron.cma ppl.cma

ocamlc -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \\
  bigarray.cma gmp.cma apron.cma ppl.cma mlexample.ml ]}

{3 Native-code compilation}

{[ocamlopt -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -o mlexample.opt \\
  bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml ]}

{3 Without auto-linking feature}

{[ocamlopt -cc \"g++\" -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -noautolink -o mlexample.opt \\
  bigarray.cmxa gmp.cmxa apron.cmxa ppl.cmxa mlexample.ml \\
  -cclib \"-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib -L$PPL_PREFIX/lib\\
	  -lap_ppl_caml_debug -lap_ppl_debug -lppl -lgmpxx \\
	  -lapron_caml_debug -lapron_debug \\
	  -lgmp_caml -L$MPFR_PREFIX/lib -lmpfr -L$GMP_PREFIX/lib -lgmp \\
	  -L$CAMLIDL_PREFIX/lib/ocaml -lcamlidl \\
	  -lbigarray\" ]}

*)")