Module Automata

val moduleident : Ident.t -> Ident.t
val eblock : 'a -> 'a Zelus.block
val eq_present : Zelus.eq list Zelus.block Zelus.present_handler list -> Zelus.eq list -> Zelus.eq list
val extend_block : 'a list -> 'a list Zelus.block option -> 'a list Zelus.block
module TableOfTypes : sig ... end
val constr : string -> Deftypes.typ list -> Deftypes.typ_desc Deftypes.loc
val intro_type : Zelus.state_handler list -> Deftypes.typ_desc Deftypes.loc * Ident.t list Ident.Env.t
val state_value : Deftypes.typ -> Deftypes.tentry
val state_parameter : bool -> Deftypes.typ -> Deftypes.tentry
val env_of_parameters : Ident.t list Ident.Env.t -> Zelus.state_handler list -> Zelus.state_exdesc Zelus.localized option -> Deftypes.tentry Ident.Env.t * Zelus.eq list

p = ..., ...p..., ...last p...

val block : (Zelus.local list -> Zelus.local list) -> ('a -> 'b) -> 'a Zelus.block -> 'b Zelus.block
val present_handlers : (Zelus.scondpat -> Zelus.scondpat) -> ('a -> 'b) -> 'a Zelus.present_handler list -> 'b Zelus.present_handler list
val exp : Ident.S.t -> Zelus.exp -> Zelus.exp
val equation : Ident.S.t -> Zelus.eq -> Zelus.eq

Translating an equation. lnames defines names x that must be

val equation_list : Ident.S.t -> Zelus.eq list -> Zelus.eq list
val block_eq_list : Ident.S.t -> Zelus.eq list Zelus.block -> Zelus.eq list Zelus.block
val present_handler_exp_list : Ident.S.t -> Zelus.exp Zelus.present_handler list -> Zelus.exp Zelus.present_handler list
val present_handler_block_eq_list : Ident.S.t -> Zelus.eq list Zelus.block Zelus.present_handler list -> Zelus.eq list Zelus.block Zelus.present_handler list
val match_handler_exp_list : Ident.S.t -> Zelus.exp Zelus.match_handler list -> Zelus.exp Zelus.match_handler list
val match_handler_block_eq_list : Ident.S.t -> Zelus.eq list Zelus.block Zelus.match_handler list -> Zelus.eq list Zelus.block Zelus.match_handler list
val local : Ident.S.t -> Zelus.local -> Zelus.local
val scondpat : Ident.S.t -> Zelus.scondpat -> Zelus.scondpat
val automaton : Ident.S.t -> Zelus.is_weak -> Zelus.state_handler list -> Zelus.state_exp option -> Zelus.eq

an extended list containing eq_list and new equations

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