Module Letify

module Letify: sig .. end
bind sigma defs xs select definitions in defs targeting variables xs. The result is a new substitution that potentially augment sigma with definitions for xs (and others).

val vmem : Lang.F.Vars.elt -> Lang.F.term -> bool
val occurs : Lang.F.Vars.t -> Lang.F.term -> bool
module Sigma: sig .. end
module Defs: sig .. end
module XS: FCSet.Make(Lang.F.Var)
val elements : Lang.F.Vars.t -> XS.t
val iter : (XS.elt -> unit) -> Lang.F.Vars.t -> unit
val extract : Lang.F.Tset.t Lang.F.Vmap.t ->
Sigma.t Pervasives.ref -> Lang.F.Vars.t -> XS.elt -> unit
val bind : Sigma.t ->
Lang.F.Tset.t Lang.F.Vmap.t -> Lang.F.Vars.t -> Sigma.t
bind sigma defs xs select definitions in defs targeting variables xs. The result is a new substitution that potentially augment sigma with definitions for xs (and others).
val get_class : Sigma.t -> Lang.F.Vars.t -> Lang.F.var -> Lang.F.Vars.elt list
val add_eq : Lang.F.pred list -> Lang.F.var -> Lang.F.var list -> Lang.F.pred list
val add_equals : Lang.F.var list -> Lang.F.pred list -> Lang.F.pred list
val add_definitions : Sigma.t ->
'a Lang.F.Vmap.t -> Lang.F.Vars.t -> Lang.F.pred list -> Lang.F.pred list
add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs. They are added to ps.
module Split: sig .. end
Pruning strategy ; selects most occuring literals to split cases.