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

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

/*
 * oct.idl
 *
 * OCaml interface specification for camlidl
 *
 * APRON Library / Octagonal Domain
 *
 * Copyright (C) Antoine Mine' 2006
 *
 */

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

quote(C,"/*\n This file is part of the APRON Library, released under LGPL 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 LGPL license.\n Please read the COPYING file packaged in the distribution.\n*)")

quote(MLI,"\n \n(** Octagon abstract domain. *)\n \n")

quote(C,"#include \"oct.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); } ")


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

import "generator0.idl";
import "abstract0.idl";
import "scalar.idl";
import "manager.idl";

typedef [abstract] struct oct_internal_t* internal_ptr;

quote(MLMLI,"\n \n\
type t\n\
  (** Type of octagons.\n\n\
      Octagons are defined by conjunctions of inequalities of the form\n\
      [+/-x_i +/- x_j >= 0].\n\n\
    Abstract values which are octagons have the type [t Apron.AbstractX.t].\n\n\
    Managers allocated for octagons have the type [t Apron.manager.t].\n\
  *)\n\n \
")

quote(MLI,"(** Allocate a new manager to manipulate octagons. *)")
ap_manager_ptr oct_manager_alloc(void);

quote(MLI,"(** No internal parameters for now... *)")
internal_ptr manager_get_internal(ap_manager_ptr man)
  quote(call,"_res = (internal_ptr)man->internal;");

quote(MLI,"(** Approximate a set of generators to an abstract value, with best precision. *)")
ap_abstract0_ptr ap_abstract0_oct_of_generator_array(ap_manager_ptr man, int v1, int v2, [ref]struct ap_generator0_array_t* v3)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Widening with scalar thresholds. *)")
ap_abstract0_ptr ap_abstract0_oct_widening_thresholds(ap_manager_ptr man,ap_abstract0_ptr a1,ap_abstract0_ptr a2,struct ap_scalar_array_t array)
     quote(call,"_res = ap_abstract0_oct_widening_thresholds(man,a1,a2,(const ap_scalar_t**)array.p,array.size);")
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Standard narrowing. *)")
ap_abstract0_ptr ap_abstract0_oct_narrowing(ap_manager_ptr man, ap_abstract0_ptr a1,ap_abstract0_ptr a2)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Perturbation. *)")
ap_abstract0_ptr ap_abstract0_oct_add_epsilon(ap_manager_ptr man,ap_abstract0_ptr a,ap_scalar_ptr epsilon)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Perturbation. *)")
ap_abstract0_ptr ap_abstract0_oct_add_epsilon_bin(ap_manager_ptr man,ap_abstract0_ptr a1,ap_abstract0_ptr a2,ap_scalar_ptr epsilon)
     quote(dealloc,"I0_CHECK_EXC(man)");

quote(MLI,"(** Algorithms. *)")
const int pre_widening = 99;

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

val manager_is_oct : 'a Apron.Manager.t -> bool
  (** Return [true] iff the argument manager is an octagon manager *)
val manager_of_oct : t Apron.Manager.t -> 'a Apron.Manager.t
  (** Make an octagon manager generic *)
val manager_to_oct : 'a Apron.Manager.t -> t Apron.Manager.t
  (** Instanciate the type of an octagon manager.
      Raises [Failure] if the argument manager is not an octagon manager *)
module Abstract0 : sig
  val is_oct : 'a Apron.Abstract0.t -> bool
    (** Return [true] iff the argument value is an oct value *)
  val of_oct : t Apron.Abstract0.t -> 'a Apron.Abstract0.t
    (** Make an oct value generic *)
  val to_oct : 'a Apron.Abstract0.t -> t Apron.Abstract0.t
    (** Instanciate the type of an oct value. 
        Raises [Failure] if the argument value is not an oct value *)
end
module Abstract1 : sig
  val is_oct : 'a Apron.Abstract1.t -> bool
    (** Return [true] iff the argument value is an oct value *)
  val of_oct : t Apron.Abstract1.t -> 'a Apron.Abstract1.t
    (** Make an oct value generic *)
  val to_oct : 'a Apron.Abstract1.t -> t Apron.Abstract1.t
    (** Instanciate the type of an oct value. 
        Raises [Failure] if the argument value is not an oct value *)
end
")

quote(ML,"
let manager_is_oct man =
  let str = Apron.Manager.get_library man in
  (String.compare str \"oct\")==0
let manager_of_oct (man:t Apron.Manager.t) : 'a Apron.Manager.t = Obj.magic man
let manager_to_oct (man:'a Apron.Manager.t) : t Apron.Manager.t =
  if manager_is_oct man then 
    Obj.magic man
  else
    failwith \"Oct.manager_to_oct: the argument manager is not an Oct manager\"
module Abstract0 = struct
  let is_oct abs = 
    manager_is_oct (Apron.Abstract0.manager abs)
  let of_oct (abs: t Apron.Abstract0.t) : 'a Apron.Abstract0.t = Obj.magic abs
  let to_oct (abs:'a Apron.Abstract0.t) : t Apron.Abstract0.t =
  if is_oct abs then 
    Obj.magic abs
  else
    failwith \"Oct.Abstract0.to_oct: the argument value is not an oct value\"
end
module Abstract1 = struct
  let is_oct abs = 
    manager_is_oct (Apron.Abstract1.manager abs)
  let of_oct (abs: t Apron.Abstract1.t) : 'a Apron.Abstract1.t = Obj.magic abs
  let to_oct (abs:'a Apron.Abstract1.t) : t Apron.Abstract1.t =
  if is_oct abs then 
    Obj.magic abs
  else
    failwith \"Oct.Abstract1.to_oct: the argument value is not an oct 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 octD.cma mlexample.ml]}

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

ocamlc -I $MLGMPIDL_PREFIX/lib -I $APRON_PREFIX/lib -use-runtime myrun -o mlexample.byte \\
  bigarray.cma gmp.cma apron.cma octD.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 octD.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 octD.cmxa mlexample.ml \\
  -cclib \"-L$MLGMPIDL_PREFIX/lib -L$APRON_PREFIX/lib \\
	  -loctD_caml_debug -loctD_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\" ]}

*)")