module Partitioning: sig
.. end
type
partition = {
|
mutable color : Lang.F.var Lang.F.Vmap.t ; |
|
mutable depend : Lang.F.Vars.t Lang.F.Vmap.t ; |
|
mutable mem : Lang.F.var Lang.F.Tmap.t ; |
}
val zero : Lang.F.Var.t
val create : unit -> partition
val color : partition -> Lang.F.Vmap.key -> Lang.F.var
val depend : partition -> Lang.F.Vmap.key -> Lang.F.Vars.t
val merge : partition -> Lang.F.var -> Lang.F.Vmap.key -> unit
val unify : partition ->
Lang.F.Vmap.key -> Lang.F.Vmap.key -> Lang.F.Vmap.key
val add_depend : partition -> Lang.F.Vmap.key -> Lang.F.Vars.t -> unit
val is_varray : Lang.F.Var.t -> bool
val color_of : partition ->
Lang.F.Vars.t -> Lang.F.Vmap.key -> Lang.F.pred -> Lang.F.Vmap.key
val walk : partition -> Lang.F.Vars.t -> Lang.F.pred -> unit
val collect : partition -> Lang.F.pred -> unit
type
classeq = partition * Lang.F.Vars.t
val closure : partition -> Lang.F.Vars.elt -> Lang.F.Vars.t -> Lang.F.Vars.t
val classes : partition -> (partition * Lang.F.Vars.t) list
val filter : partition -> bool -> Lang.F.Vars.t -> Lang.F.pred -> Lang.F.pred
val filter_hyp : partition * Lang.F.Vars.t -> Lang.F.pred -> Lang.F.pred
val filter_goal : partition * Lang.F.Vars.t -> Lang.F.pred -> Lang.F.pred