zelus 2.1 · OCaml Package

type table = cont Ident.Env.t

horizons are considered to be useful

and cont = {

}

val print : Format.formatter -> cont Ident.Env.t -> unit

Useful function. For debugging purpose.

val add : 
  bool ->
  Ident.S.t ->
  Ident.S.t ->
  cont Ident.Env.t ->
  cont Ident.Env.t

val extend : cont Ident.Env.t -> Ident.S.t -> cont Ident.Env.t

is marked to also depend on names in names

val merge : cont Ident.Env.t -> cont Ident.Env.t -> cont Ident.Env.t

Fusion of two tables

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

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

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

val build_local : cont Ident.Env.t -> Zelus.local -> cont Ident.Env.t

val build_equation_list : cont Ident.Env.t -> Zelus.eq list -> cont Ident.Env.t

val visit : Ident.S.t -> cont Ident.Env.t -> Ident.S.t

read is a set of variables

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

Empty block

val writes : Ident.S.t -> Deftypes.defnames -> Deftypes.defnames

remove useless names in write names

val pattern : Ident.S.t -> Zelus.pattern -> Zelus.pattern

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

Remove useless equations. useful is the set of useful names

val remove_equation_list : Ident.S.t -> Zelus.eq list -> Zelus.eq list

val remove_block : 
  Ident.S.t ->
  Zelus.eq list Zelus.block ->
  Zelus.eq list Zelus.block

val remove_local : Ident.S.t -> Zelus.local -> Zelus.local

val horizon : Ident.S.t -> Zelus.local -> Ident.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

val implementation : 
  Zelus.implementation_desc Zelus.localized ->
  Zelus.implementation_desc Zelus.localized

val implementation_list : 
  Zelus.implementation_desc Zelus.localized list ->
  Zelus.implementation_desc Zelus.localized list

package zelus