Zdeadcodetype table = cont Zident.Env.thorizons are considered to be useful
val print : Format.formatter -> cont Zident.Env.t -> unitUseful function. For debugging purpose.
val add :
bool ->
Zident.S.t ->
Zident.S.t ->
cont Zident.Env.t ->
cont Zident.Env.tval extend : cont Zident.Env.t -> Zident.S.t -> cont Zident.Env.tis marked to also depend on names in names
val merge : cont Zident.Env.t -> cont Zident.Env.t -> cont Zident.Env.tFusion of two tables
val build_equation : cont Zident.Env.t -> Zelus.eq -> cont Zident.Env.tBuild the association table yk -> { x1,..., xn}
val build_block :
cont Zident.Env.t ->
Zelus.eq list Zelus.block ->
cont Zident.Env.tval build_local : cont Zident.Env.t -> Zelus.local -> cont Zident.Env.tval build_equation_list :
cont Zident.Env.t ->
Zelus.eq list ->
cont Zident.Env.tval visit : Zident.S.t -> cont Zident.Env.t -> Zident.S.tread is a set of variables
val is_empty_block : 'a list Zelus.block -> boolEmpty block
val writes : Zident.S.t -> Deftypes.defnames -> Deftypes.defnamesremove useless names in write names
val pattern : Zident.S.t -> Zelus.pattern -> Zelus.patternval remove_equation : Zident.S.t -> Zelus.eq -> Zelus.eq list -> Zelus.eq listRemove useless equations. useful is the set of useful names
val remove_equation_list : Zident.S.t -> Zelus.eq list -> Zelus.eq listval remove_block :
Zident.S.t ->
Zelus.eq list Zelus.block ->
Zelus.eq list Zelus.blockval remove_local : Zident.S.t -> Zelus.local -> Zelus.localval horizon : Zident.S.t -> Zelus.local -> Zident.S.tCompute the set of horizons
val implementation :
Zelus.implementation_desc Zelus.localized ->
Zelus.implementation_desc Zelus.localizedval implementation_list :
Zelus.implementation_desc Zelus.localized list ->
Zelus.implementation_desc Zelus.localized list