functor (D : Domain) ->
sig
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 = Fixpoint.Make.rules Vector.t
and rules = {
mutable join : Fixpoint.Make.var list;
mutable fct : Fixpoint.Make.sem list;
}
type f1 = D.t -> D.t
type f2 = D.t -> D.t -> D.t
type fn = D.t list -> D.t
val map : ('a -> 'b) -> 'a list -> 'b list
val create : unit -> 'a Vector.t
val var : Fixpoint.Make.rules Vector.t -> int
val add :
Fixpoint.Make.rules Vector.t -> int -> Fixpoint.Make.var -> unit
val adds :
Fixpoint.Make.rules Vector.t -> int -> Fixpoint.Make.sem -> unit
val add0 : Fixpoint.Make.rules Vector.t -> int -> D.t -> unit
val add1 :
Fixpoint.Make.rules Vector.t -> int -> (D.t -> D.t) -> int -> unit
val add2 :
Fixpoint.Make.rules Vector.t ->
int -> (D.t -> D.t -> D.t) -> int -> int -> unit
val addn :
Fixpoint.Make.rules Vector.t ->
int -> (D.t list -> D.t) -> int list -> unit
type strategy = {
root : int;
sys : Fixpoint.Make.system;
var : int array;
dom : D.t array;
}
val visit :
Fixpoint.Make.rules Vector.t ->
Fixpoint.Make.var array -> Fixpoint.Make.var -> Fixpoint.Make.var
val visit_k :
Fixpoint.Make.rules Vector.t ->
Fixpoint.Make.var array ->
Fixpoint.Make.var -> Fixpoint.Make.rules -> unit
val visit_r :
Fixpoint.Make.rules Vector.t ->
Fixpoint.Make.var array ->
Fixpoint.Make.var -> Fixpoint.Make.rules -> Fixpoint.Make.var
val id : int array -> int -> int
val depend : int array -> 'a list array -> 'a -> int -> int
val fmap : (int -> int) -> Fixpoint.Make.sem -> Fixpoint.Make.sem
val sem : D.t array -> Fixpoint.Make.sem -> D.t
val update : Fixpoint.Make.rules Vector.t * D.t array * 'a -> int -> unit
val widen :
Fixpoint.Make.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:Fixpoint.Make.rules Vector.t ->
root:Fixpoint.Make.var -> timeout:int -> D.t array
end