module Make:
type int
type
| |
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 rules Vector.t
type
|
mutable join : var list; |
|
mutable fct : sem list; |
}
type D.t -> D.t
type D.t -> D.t -> D.t
type 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
|
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 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.