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

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

quote(MLI,"(** APRON Expressions of level 1 *)")

quote(C, "\n\
#include <limits.h>\n\
#include \"ap_texpr1.h\"\n\
#include \"apron_caml.h\"\n\
")


import "scalar.idl";
import "interval.idl";
import "coeff.idl";
import "texpr0.idl";
import "environment.idl";

struct ap_texpr1_t {
  [mlname(mutable_texpr0)] ap_texpr0_ptr texpr0;
  [mlname(mutable_env)] ap_environment_ptr env;
};
quote(MLMLI,"\n\
(** Unary operators *) \n\
type unop = Texpr0.unop = \n\
  | Neg\n\
  | Cast\n\
  | Sqrt\n\
\n\
(** Binary operators *) \n\
type binop = Texpr0.binop = \n\
  | Add\n\
  | Sub\n\
  | Mul\n\
  | Div\n\
  | Mod\n\
\n\
(** Destination type for rounding *) \n\
type typ = Texpr0.typ = \n\
  | Real\n\
  | Int\n\
  | Single\n\
  | Double\n\
  | Extended\n\
  | Quad\n\
\n\
(** Rounding direction *) \n\
type round = Texpr0.round = \n\
  | Near\n\
  | Zero\n\
  | Up\n\
  | Down\n\
  | Rnd\n\
\n\
(** User type for tree expressions *) \n\
type expr = \n\
  | Cst of Coeff.t \n\
  | Var of Var.t \n\
  | Unop of unop * expr * typ * round \n\
  | Binop of binop * expr * expr * typ * round \n\
")

quote(C, "\n\
value camlidl_texpr1_ap_texpr1_to_expr_c2ml(ap_environment_t* env, ap_texpr0_t* expr, camlidl_ctx _ctx)\n\
{\n\
  value _v_res ;\n\
\n\
  switch(expr->discr){\n\
  case AP_TEXPR_CST:\n\
    {\n\
      value v0 = Val_unit;\n\
      Begin_root(v0);\n\
      v0 = camlidl_c2ml_coeff_struct_ap_coeff_t(&expr->val.cst, _ctx);\n\
      _v_res = caml_alloc_small(1,0);\n\
       Field(_v_res,0) = v0;\n\
      End_roots();\n\
    }\n\
    break;\n\
  case AP_TEXPR_DIM:\n\
    {\n\
      ap_var_t var;\n\
      value v0 = Val_unit;\n\
      var = ap_environment_var_of_dim(env,expr->val.dim);\n\
      assert(var!=NULL);\n\
      var = ap_var_copy(var);\n\
      Begin_root(v0);\n\
      v0 = camlidl_apron_var_ptr_c2ml(&var);\n\
      _v_res = caml_alloc_small(1,1);\n\
       Field(_v_res,0) = v0;\n\
      End_roots();\n\
    }\n\
    break;\n\
  case AP_TEXPR_NODE:\n\
    {\n\
      value v0,v1,v2,v3,v4;\n\
      v0 = v1 = v2 = v3 = v4 = Val_unit;\n\
      Begin_roots5(v0,v1,v2,v3,v4);\n\
      ap_texpr0_node_t* node = expr->val.node;\n\
      v1 = camlidl_texpr1_ap_texpr1_to_expr_c2ml(env,node->exprA,_ctx);\n\
      v3 = camlidl_apron_texpr_rtype_t_c2ml(&node->type);\n\
      v4 = camlidl_apron_texpr_rdir_t_c2ml(&node->dir);\n\
      if (ap_texpr_is_unop(node->op)){\n\
	v0 = camlidl_apron_texpr_unop_t_c2ml(&node->op);\n\
	_v_res = caml_alloc_small(4,2);\n\
	Field(_v_res,0) = v0;\n\
	Field(_v_res,1) = v1;\n\
	Field(_v_res,2) = v3;\n\
	Field(_v_res,3) = v4;\n\
      }\n\
      else {\n\
	v0 = camlidl_apron_texpr_binop_t_c2ml(&node->op);\n\
	v2 = camlidl_texpr1_ap_texpr1_to_expr_c2ml(env,node->exprB,_ctx);\n\
	_v_res = caml_alloc_small(5,3);\n\
	Field(_v_res,0) = v0;\n\
	Field(_v_res,1) = v1;\n\
	Field(_v_res,2) = v2;\n\
	Field(_v_res,3) = v3;\n\
	Field(_v_res,4) = v4;\n\
      }\n\
      End_roots();\n\
    }\n\
    break;\n\
  default:\n\
    abort();\n\
  }\n\
  return _v_res;\n\
}\n\
value camlidl_texpr1_ap_texpr1_to_expr(value _v_texpr)\n\
{\n\
  CAMLparam1(_v_texpr);\n\
  CAMLlocal1(_v_res);\n\
  ap_environment_t* env;\n\
  ap_texpr1_t texpr1;\n\
\n\
  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };\n\
  camlidl_ctx _ctx = &_ctxs;\n\
\n\
  camlidl_ml2c_texpr1_struct_ap_texpr1_t(_v_texpr,&texpr1,_ctx);\n\
  _v_res = camlidl_texpr1_ap_texpr1_to_expr_c2ml(texpr1.env,texpr1.texpr0,_ctx);\n\
  camlidl_free(_ctx);\n\
\n\
  CAMLreturn(_v_res);\n\
}\n\
\n\
void camlidl_texpr1_ap_texpr0_of_expr_ml2c(value v, ap_environment_t* env, ap_texpr0_t** res, camlidl_ctx _ctx)\n\
{\n\
  ap_texpr0_t* texpr;\n\
  ap_texpr0_node_t* node;\n\
  ap_coeff_t coeff;\n\
  ap_var_t var;\n\
  ap_dim_t dim;\n\
  ap_texpr0_t* exprA;\n\
  ap_texpr0_t* exprB;\n\
  value v0,v1,v2,v3,v4;\n\
\n\
  texpr = malloc(sizeof(ap_texpr0_t));\n \
\n\
  assert (Is_block(v));\n\
  switch (Tag_val(v)){\n\
  case 0: /* Constant */\n\
    assert(Wosize_val(v)==1);\n\
    v0 = Field(v,0);\n\
    texpr->discr = AP_TEXPR_CST;\n\
    camlidl_ml2c_coeff_struct_ap_coeff_t(v0,&coeff,_ctx);\n\
    ap_coeff_init_set(&texpr->val.cst,&coeff);\n\
    break;\n\
  case 1: /* Variable */\n\
    assert(Wosize_val(v)==1);\n\
    v0 = Field(v,0);\n\
    camlidl_apron_var_ptr_ml2c(v0,&var);\n\
    texpr->discr = AP_TEXPR_DIM;\n\
    texpr->val.dim = ap_environment_dim_of_var(env,var);\n\
    if (texpr->val.dim == AP_DIM_MAX){\n\
      free(texpr);\n\
      texpr = NULL;\n\
    }\n\
    break;\n\
  case 2: /* Unary node */\n\
    v0 = Field(v,0);\n\
    v1 = Field(v,1);\n\
    v2 = Field(v,2);\n\
    v3 = Field(v,3);\n\
    \n\
    camlidl_texpr1_ap_texpr0_of_expr_ml2c(v1,env,&exprA,_ctx);\n\
    if (exprA==NULL){\n\
      free(texpr);\n\
      texpr = NULL;\n\
    }\n\
    else {\n\
      node = malloc(sizeof(ap_texpr0_node_t));\n\
      camlidl_apron_texpr_unop_t_ml2c      (v0,&node->op);\n\
      camlidl_apron_texpr_rtype_t_ml2c     (v2,&node->type);\n\
      camlidl_apron_texpr_rdir_t_ml2c      (v3,&node->dir);\n\
      node->exprA = exprA; \n\
      node->exprB = NULL;\n\
      texpr->discr = AP_TEXPR_NODE;\n\
      texpr->val.node = node;\n\
    }\n\
    break;\n\
  case 3: /* Binary node */\n\
    v0 = Field(v,0);\n\
    v1 = Field(v,1);\n\
    v2 = Field(v,2);\n\
    v3 = Field(v,3);\n\
    v4 = Field(v,4);\n\
    camlidl_texpr1_ap_texpr0_of_expr_ml2c(v1,env,&exprA,_ctx);\n\
    if (exprA==NULL){\n\
      free(texpr);\n\
      texpr = NULL;\n\
    }\n\
    else {\n\
      camlidl_texpr1_ap_texpr0_of_expr_ml2c(v2,env,&exprB,_ctx);\n\
      if (exprB==NULL){\n\
	ap_texpr0_free(exprA);\n\
	free(texpr);\n\
	texpr = NULL;\n\
      }\n\
      else {\n\
	node = malloc(sizeof(ap_texpr0_node_t));\n\
	camlidl_apron_texpr_binop_t_ml2c     (v0,&node->op);\n\
	camlidl_apron_texpr_rtype_t_ml2c     (v3,&node->type);\n\
	camlidl_apron_texpr_rdir_t_ml2c      (v4,&node->dir);\n\
	node->exprA = exprA; \n\
	node->exprB = exprB; \n\
	texpr->discr = AP_TEXPR_NODE;\n\
	texpr->val.node = node;\n\
      }\n\
    }\n\
    break;\n\
  default:\n\
    assert(false);\n\
  }\n\
  *res = texpr;\n\
}\n\
value camlidl_texpr1_ap_texpr0_of_expr(value _v_env, value _v_expr)\n\
{\n\
  CAMLparam2(_v_env,_v_expr);\n\
  CAMLlocal1(_v_res);\n\
  ap_texpr0_t* texpr0;\n\
  ap_environment_t* env;\n\
\n\
  struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };\n\
  camlidl_ctx _ctx = &_ctxs;\n\
\n\
  camlidl_apron_environment_ptr_ml2c(_v_env,&env);\n\
  camlidl_texpr1_ap_texpr0_of_expr_ml2c(_v_expr,env,&texpr0,_ctx);\n\
  camlidl_free(_ctx);\n\
  if (texpr0==NULL){\n\
    caml_failwith(\"Texpr1.texpr0_of_expr: unknown variable in the environment\");\n\
  }\n\
  _v_res = camlidl_apron_texpr0_ptr_c2ml(&texpr0);\n\
  CAMLreturn(_v_res);\n\
}\n\
")

quote(MLMLI,"(** {2 Constructors and Destructor} *)")

quote(MLI,"(** General constructor (actually the most efficient) *)")
quote(MLI,"val of_expr : Environment.t -> expr -> t\n")
/* quote(ML,"external texpr0_of_expr : Environment.t -> expr -> Texpr0.t = \"camlidl_texpr1_ap_texpr0_of_expr\")
*/
quote(ML,"\
let rec expr0_of_expr1 env expr =\n\
  match expr with\n\
  | Cst x -> Texpr0.Cst x\n\
  | Var var -> Texpr0.Dim (Environment.dim_of_var env var)\n\
  | Unop(op,e,t,r) -> \n\
      Texpr0.Unop(\n\
	op,\n\
	(expr0_of_expr1 env e),\n\
	t,r\n\
      )\n\
  | Binop(op,e1,e2,t,r) -> \n\
      Texpr0.Binop(\n\
	op,\n\
	(expr0_of_expr1 env e1),\n\
	(expr0_of_expr1 env e2),\n\
	t,r\n\
      )\n\
let texpr0_of_expr env expr =\n\
  Texpr0.of_expr (expr0_of_expr1 env expr)\n\
let of_expr env expr = {\n\
  texpr0 = texpr0_of_expr env expr;\n\
  env = env;\n\
}\n\
")

quote(MLI,"\
(** Copy *)\n\
val copy : t -> t\n\
\n\
(** Conversion *)\n\
val of_linexpr : Linexpr1.t -> t\n\
")
quote(ML,"\n\
let copy e = { texpr0 = Texpr0.copy e.texpr0; env = e.env }\n\
let of_linexpr e = { texpr0 = Texpr0.of_linexpr e.Linexpr1.linexpr0; env = e.Linexpr1.env }\n\
")
quote(MLI,"(** General destructor *)")
/* quote(MLMLI,"external to_expr : t -> expr = \"camlidl_texpr1_ap_texpr1_to_expr\"\n") */
quote(MLI,"val to_expr : t -> expr\n")
quote(ML,"\
let rec expr1_of_expr0 env expr =\n\
  match expr with\n\
  | Texpr0.Cst x -> Cst x\n\
  | Texpr0.Dim dim -> Var (Environment.var_of_dim env dim)\n\
  | Texpr0.Unop(op,e,t,r) -> \n\
      Unop(\n\
	op,\n\
	(expr1_of_expr0 env e),\n\
	t,r\n\
      )\n\
  | Texpr0.Binop(op,e1,e2,t,r) -> \n\
      Binop(\n\
	op,\n\
	(expr1_of_expr0 env e1),\n\
	(expr1_of_expr0 env e2),\n\
	t,r\n\
      )\n\
let to_expr texpr1 =\n\
  let expr0 = Texpr0.to_expr texpr1.texpr0 in\n\
  expr1_of_expr0 texpr1.env expr0\n\
")
quote(MLI,"\n(** {3 Incremental constructors} *)\n")
[ref]struct ap_texpr1_t* ap_texpr1_cst(ap_environment_ptr env, [ref]struct ap_coeff_t* coeff);
[ref]struct ap_texpr1_t* ap_texpr1_var(ap_environment_ptr env, ap_var_t var);
[ref]struct ap_texpr1_t* ap_texpr1_unop(ap_texpr_unop_t op,
			     [ref]struct ap_texpr1_t* expr,
			     ap_texpr_rtype_t type, ap_texpr_rdir_t dir)
quote(call,"_res = ap_texpr1_unop(op,ap_texpr1_copy(expr),type,dir);");
[ref]struct ap_texpr1_t* ap_texpr1_binop(ap_texpr_binop_t op,
			      [ref]struct ap_texpr1_t* exprA, [ref]struct ap_texpr1_t* exprB,
			      ap_texpr_rtype_t type, ap_texpr_rdir_t dir)
quote(call,"_res = ap_texpr1_binop(op,ap_texpr1_copy(exprA),ap_texpr1_copy(exprB),type,dir);");


quote(MLMLI,"\n(** {2 Tests} *)\n")

quote(MLI,"\
val is_interval_cst : t -> bool \n\
val is_interval_linear : t -> bool \n\
val is_interval_polynomial : t -> bool \n\
val is_interval_polyfrac : t -> bool \n\
val is_scalar : t -> bool \n\
")
quote(ML,"\
let is_interval_cst x = Texpr0.is_interval_cst x.texpr0 \n\
let is_interval_linear x = Texpr0.is_interval_linear x.texpr0 \n\
let is_interval_polynomial x = Texpr0.is_interval_polynomial x.texpr0 \n\
let is_interval_polyfrac x = Texpr0.is_interval_polyfrac x.texpr0 \n\
let is_scalar x = Texpr0.is_scalar x.texpr0 \n\
")

quote(MLMLI,"\n(** {2 Operations} *)\n")
quote(MLI,"(** Change the environment of the expression for a super-environement. Raise [Failure] if it is not the case *)")
[ref]struct ap_texpr1_t* ap_texpr1_extend_environment([ref]struct ap_texpr1_t* texpr,
						      ap_environment_ptr env)
     quote(call,"\n\
{\n\
  bool b;\n\
  _res = ap_texpr1_extend_environment(texpr,env);\n\
  if (!_res) caml_failwith(\"Texpr1.extend_environment: new environment is not a superenvironment\");\n\
}\n\
")
;
quote(MLI,"(** Side-effet version of the previous function *)")
void ap_texpr1_extend_environment_with([ref]struct ap_texpr1_t* texpr,
				       ap_environment_ptr env)
     quote(call,"\n\
{\n\
  if (texpr->env!=env){ \n\
    bool b;\n\
    ap_environment_copy(texpr->env); /* to protect it */ \n\
    b = ap_texpr1_extend_environment_with(texpr,env);\n\
    if (b){ \n\
      ap_environment_free(texpr->env); \n\
      caml_failwith(\"Texpr1.extend_environment_with: new environment is not a superenvironment\");\n\
    }\n\
    Store_field(_v_texpr,1,_v_env);\n\
    ap_environment_free(env);\n\
  }\n\
}\n\
")
;

quote(MLI,"\n\
(** Get the underlying expression of level 0 (which is not a copy). *)\n\
val get_texpr0: t -> Texpr0.t\n\
\n\
(** Get the environement of the expression *)\n\
val get_env: t -> Environment.t\n\
\n\
")
quote(ML,"\n\
let get_texpr0 expr = expr.texpr0\n\
let get_env expr = expr.env\n\
")

quote(MLMLI,"\n(** {2 Printing} *)\n")

quote(MLI,"\n\
val string_of_unop  : unop  -> string\n\
val string_of_binop : binop -> string\n\
val string_of_typ   : typ   -> string\n\
val string_of_round : round -> string\n\
val print_unop  :  Format.formatter -> unop  -> unit\n\
val print_binop :  Format.formatter -> binop -> unit\n\
val print_typ   :  Format.formatter -> typ   -> unit\n\
val print_round :  Format.formatter -> round -> unit\n\
val print_expr : Format.formatter -> expr -> unit\n\
  (** Print a tree expression *)\n\
val print : Format.formatter -> t -> unit\n\
  (** Print an abstract tree expression *)\n\
")

quote(ML,"\n\
let string_of_unop = Texpr0.string_of_unop\n\
let string_of_binop = Texpr0.string_of_binop\n\
let string_of_typ = Texpr0.string_of_typ\n\
let string_of_round = Texpr0.string_of_round\n\
let print_unop = Texpr0.print_unop\n\
let print_binop = Texpr0.print_binop\n\
let print_typ = Texpr0.print_typ\n\
let print_round = Texpr0.print_round\n\
let rec print_expr fmt expr =\n\
  let precedence_of_expr = function\n\
    | Cst _\n\
    | Var _ -> 5\n\
    | Unop(op,_,_,_) -> Texpr0.print_precedence_of_unop op\n\
    | Binop(op,_,_,_,_) -> Texpr0.print_precedence_of_binop op\n\
  in\n\
  match expr with\n\
  | Cst x -> Coeff.print fmt x\n\
  | Var x -> Format.pp_print_string fmt (Var.to_string x)\n\
  | Unop(op,e,typ,round) ->\n\
      let prec = Texpr0.print_precedence_of_unop op in\n\
      let prec1 = precedence_of_expr e in\n\
      let par = prec1<=prec in\n\
      Format.fprintf fmt \"%s%s%a%s\"\n\
	(Texpr0.print_sprint_unop op typ round)\n\
	(if par then \"(\" else \"\")\n\
	print_expr e\n\
	(if par then \")\" else \"\")\n\
  | Binop(op,e1,e2,typ,round) ->\n\
      let prec = Texpr0.print_precedence_of_binop op in\n\
      let prec1 = precedence_of_expr e1 in\n\
      let prec2 = precedence_of_expr e2 in\n\
      let par1 = prec1<prec in\n\
      let par2 = prec2<=prec in\n\
      Format.fprintf fmt \"%s%a%s %s %s%a%s\"\n\
	(if par1 then \"(\" else \"\")\n\
	print_expr e1\n\
	(if par1 then \")\" else \"\")\n\
	(Texpr0.print_sprint_binop op typ round)\n\
	(if par2 then \"(\" else \"\")\n\
	print_expr e2\n\
	(if par2 then \")\" else \"\")\n\
\n\
let print fmt expr =\n\
  Texpr0.print\n\
   (fun dim -> Var.to_string (Environment.var_of_dim expr.env dim))\n\
   fmt expr.texpr0\n\
")