zelus 2.2 · OCaml Package

type table = cont Zident.Env.t

horizons are considered to be useful

and cont = {

}

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

Useful function. For debugging purpose.

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

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

is marked to also depend on names in names

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

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_local : cont Zident.Env.t -> Zelus.local -> cont Zident.Env.t

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

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

read is a set of variables

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

Empty block

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

remove useless names in write names

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

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

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