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).
look for the shape:
\forall x:integer. (csta <= x /\ x <= cstb) => t1=t2
and return Some(csta,cstb)
< on integer are always normalized to <=
module Ground:sig
..end
module Sigma:sig
..end
module Defs:sig
..end
val bind : Sigma.t -> Defs.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 add_definitions : Sigma.t ->
Defs.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