module Make:
type
var = int
type
sem =
| |
F0 of D.t |
| |
F1 of int * (D.t -> D.t) |
| |
F2 of int * int * (D.t -> D.t -> D.t) |
| |
Fn of int list * (D.t list -> D.t) |
type
system = rules Vector.t
type
rules = {
|
mutable join : var list ; |
|
mutable fct : sem list ; |
}
type
f1 = D.t -> D.t
type
f2 = D.t -> D.t -> D.t
type
fn = D.t list -> D.t
val add : rules Vector.t -> int -> var -> unit
add x y
requires x >= y
val map : ('a -> 'b) -> 'a list -> 'b list
val create : unit -> 'a Vector.t
val var : rules Vector.t -> int
val add : rules Vector.t -> int -> var -> unit
add x y
requires x >= y
val adds : rules Vector.t -> int -> sem -> unit
val add0 : rules Vector.t -> int -> D.t -> unit
add0 x d
requires x >= d
val add1 : rules Vector.t -> int -> (D.t -> D.t) -> int -> unit
add x f y
requires x >= f(y)
val add2 : rules Vector.t ->
int -> (D.t -> D.t -> D.t) -> int -> int -> unit
add x f y z
requires x >= f(y,z)
val addn : rules Vector.t -> int -> (D.t list -> D.t) -> int list -> unit
add x f ys
requires x >= f(ys)
type
strategy = {
|
root : int ; |
|
sys : system ; |
|
var : int array ; |
|
dom : D.t array ; |
}
val visit : rules Vector.t ->
var array -> var -> var
val visit_k : rules Vector.t ->
var array -> var -> rules -> unit
val visit_r : rules Vector.t ->
var array ->
var -> rules -> var
val id : int array -> int -> int
val depend : int array -> 'a list array -> 'a -> int -> int
val fmap : (int -> int) -> sem -> sem
val sem : D.t array -> sem -> D.t
val update : rules Vector.t * D.t array * 'a -> int -> unit
val widen : rules Vector.t * D.t array * 'a -> level:'a -> int -> bool
type
fixpoint = D.t array
val get : 'a array -> int -> 'a
val fixpoint : system:rules Vector.t ->
root:var -> timeout:int -> D.t array
Computes the least fixpoint solution satifying all added
requirements. Chains of pure-copies (see add
) are detected and
optimized. Uses Bourdoncle's weak partial ordering to compute
the solution. For each component, after timeout
-steps of
non-stable iteration, the widening operator of D
is used to
stabilize the computation.