module Cleaning: sig
.. end
type 'a
occur =
| |
TOP |
| |
TRUE |
| |
FALSE |
| |
EQ of 'a |
val cup : ('a -> 'b -> bool) -> 'a occur -> 'b -> 'a occur
val cup_true : 'a occur -> 'b occur
val cup_false : 'a occur -> 'b occur
val set_top : 'a occur Lang.F.Vmap.t ->
Lang.F.pred -> 'a occur Lang.F.Vmap.t
val add : ('a -> 'a -> bool) ->
Lang.F.Vmap.key ->
'a -> 'a occur Lang.F.Vmap.t -> 'a occur Lang.F.Vmap.t
val add_true : 'a occur Lang.F.Vmap.t ->
Lang.F.Vmap.key -> 'a occur Lang.F.Vmap.t
val add_false : 'a occur Lang.F.Vmap.t ->
Lang.F.Vmap.key -> 'a occur Lang.F.Vmap.t
val add_var : Lang.F.Vmap.key ->
Lang.F.var ->
Lang.F.var occur Lang.F.Vmap.t ->
Lang.F.var occur Lang.F.Vmap.t
val add_fun : Lang.F.Vmap.key ->
Lang.F.Fun.t ->
Lang.F.Fun.t occur Lang.F.Vmap.t ->
Lang.F.Fun.t occur Lang.F.Vmap.t
val add_pred : Lang.F.var occur Lang.F.Vmap.t ->
Lang.F.pred -> Lang.F.var occur Lang.F.Vmap.t
val add_type : Lang.F.Fun.t occur Lang.F.Vmap.t ->
Lang.F.pred -> Lang.F.Fun.t occur Lang.F.Vmap.t
type
usage = {
|
mutable eq_var : Lang.F.var occur Lang.F.Vmap.t ; |
|
mutable eq_fun : Lang.lfun occur Lang.F.Vmap.t ; |
}
val create : unit -> usage
val as_atom : usage -> Lang.F.pred -> unit
val as_have : usage -> Lang.F.pred -> unit
val as_type : usage -> Lang.F.pred -> unit
val get : Lang.F.Vmap.key -> 'a Lang.F.Vmap.t -> 'a option
val is_true : Lang.F.Vmap.key -> 'a occur Lang.F.Vmap.t -> bool
val is_false : Lang.F.Vmap.key -> 'a occur Lang.F.Vmap.t -> bool
val is_var : Lang.F.Vmap.key -> usage -> bool
val filter_pred : usage -> Lang.F.pred -> Lang.F.pred
val filter_type : usage -> Lang.F.pred -> Lang.F.pred