/usr/lib/ocaml/apron/dim.idl is in libapron-ocaml-dev 0.9.10-7.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 | /* -*- 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, "\n\
#include <limits.h>\n\
#include \"ap_dimension.h\"\n\
#include \"caml/mlvalues.h\"\n\
#include \"apron_caml.h\"\n\
")
typedef unsigned int ap_dim_t;
typedef [mltype("{\n dim : int array;\n intdim : int;\n realdim : int;\n}"),
c2ml(camlidl_apron_dimchange_c2ml),
ml2c(camlidl_apron_dimchange_ml2c)]
struct ap_dimchange_t ap_dimchange_t;
struct ap_dimchange2_t {
ap_dimchange_t* add;
ap_dimchange_t* remove;
};
struct ap_dimperm_t {
[size_is(size)]unsigned int* dim;
unsigned int size;
};
struct ap_dimension_t {
[mlname(intd)]unsigned int intdim;
[mlname(reald)]unsigned int realdim;
};
quote(MLMLI,"(** APRON Dimensions and related types *)")
quote(MLI,"\n(**
{ul
{- [t=int] is the type of dimensions.}
{- The semantics of an object [(change:change)] is the following one:
{ul
{- [change.intdim] and [change.realdim] indicate the number of integer and
real dimensions to add or to remove}
{- In case of the addition of dimensions,
[change.dim[i]=k] means: add one dimension at dimension k and shift the
already existing dimensions greater than or equal to k one step on the
right (or increment them).
if k is equal to the size of the vector, then it means: add a dimension at
the end.
Repetition are allowed, and means that one inserts more than one dimensions.
Example:
[add_dimensions [i0 i1 r0 r1] { dim=[0 1 2 2 4]; intdim=3; realdim=1 }]
returns [0 i0 0 i1 0 0 r0 r1 0], considered as a vector with 6 integer
dimensions and 3 real dimensions.}
{- In case of the removal of dimensions,
dimchange.dim[i]=k means: remove the dimension k and shift the dimensions
greater than k one step on the left (or decrement them).
Repetitions are meaningless (and are not correct specification)
Example: [remove_dimensions [i0 i1 i2 r0 r1 r2] { dim=[0 2 4]; intdim=2;
realdim=1 }] returns [i1 r0 r2], considered as a vector with 1 integer
dimensions and 2 real dimensions.
}}}
{- The semantics of an object [(change2:change2)] is the combination of the
two following transformations:
{ul
{- [change2.add] indicates an optional addition of dimensions.}
{- [change2.remove] indicates an optional removal of dimensions.}
}}
{- [perm] defines a permutation.}
{- [dimension] defines the dimensionality of an abstract value (number of
integer and real dimensions).
}}
*)
")
quote(MLI,"
(** Assuming a transformation for add_dimensions, invert it in-place to
obtain the inverse transformation using remove_dimensions *)
val change_add_invert : change -> unit
(** [perm_compose perm1 perm2] composes the 2 permutations perm1 and perm2
(in this order). The sizes of permutations are supposed to be equal. *)
val perm_compose : perm -> perm -> perm
(** Invert a permutation *)
val perm_invert : perm -> perm
")
quote(ML,"
let change_add_invert change =
let dim = change.dim in
for i=0 to (Array.length dim)-1 do
dim.(i) <- dim.(i) + i;
done
let perm_compose perm1 perm2 =
let length = Array.length perm1 in
assert(length==(Array.length perm2));
Array.init length (fun i -> perm2.(perm1.(i)))
let perm_invert perm =
let length = Array.length perm in
let res = Array.make length 0 in
for i=0 to length-1 do
res.(perm.(i)) <- i;
done;
res
")
|