package zelus

  1. Overview
  2. Docs
type table = cont Zident.Env.t

horizons are considered to be useful

and cont = {
  1. mutable c_vars : Zident.S.t;
  2. mutable c_useful : bool;
  3. mutable c_visited : bool;
}
val print : Format.formatter -> cont Zident.Env.t -> unit

Useful function. For debugging purpose.

is marked to also depend on names in names

Fusion of two tables

val build_equation : cont Zident.Env.t -> Zelus.eq -> cont Zident.Env.t

Build the association table yk -> { x1,..., xn}

val build_block : cont Zident.Env.t -> Zelus.eq list Zelus.block -> cont Zident.Env.t
val build_equation_list : cont Zident.Env.t -> Zelus.eq list -> cont Zident.Env.t

read is a set of variables

val is_empty_block : 'a list Zelus.block -> bool

Empty block

remove useless names in write names

val remove_equation : Zident.S.t -> Zelus.eq -> Zelus.eq list -> Zelus.eq list

Remove useless equations. useful is the set of useful names

val remove_equation_list : Zident.S.t -> Zelus.eq list -> Zelus.eq list
val remove_block : Zident.S.t -> Zelus.eq list Zelus.block -> Zelus.eq list Zelus.block
val remove_local : Zident.S.t -> Zelus.local -> Zelus.local
val horizon : Zident.S.t -> Zelus.local -> Zident.S.t

Compute the set of horizons

val exp : Zelus.exp -> Zelus.exp

the main entry for expressions. Warning: e must be in normal form

OCaml

Innovation. Community. Security.