Automataval eblock : 'a -> 'a Zelus.blockval eq_present :
Zelus.eq list Zelus.block Zelus.present_handler list ->
Zelus.eq list ->
Zelus.eq listval extend_block : 'a list -> 'a list Zelus.block option -> 'a list Zelus.blockmodule TableOfTypes : sig ... endval constr : string -> Deftypes.typ list -> Deftypes.typ_desc Deftypes.locval intro_type :
Zelus.state_handler list ->
Deftypes.typ_desc Deftypes.loc * Ident.t list Ident.Env.tval state_value : Deftypes.typ -> Deftypes.tentryval state_parameter : bool -> Deftypes.typ -> Deftypes.tentryval 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 listp = ..., ...p..., ...last p...
val block :
(Zelus.local list -> Zelus.local list) ->
('a -> 'b) ->
'a Zelus.block ->
'b Zelus.blockval present_handlers :
(Zelus.scondpat -> Zelus.scondpat) ->
('a -> 'b) ->
'a Zelus.present_handler list ->
'b Zelus.present_handler listTranslating an equation. lnames defines names x that must be
val block_eq_list :
Ident.S.t ->
Zelus.eq list Zelus.block ->
Zelus.eq list Zelus.blockval present_handler_exp_list :
Ident.S.t ->
Zelus.exp Zelus.present_handler list ->
Zelus.exp Zelus.present_handler listval 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 listval match_handler_exp_list :
Ident.S.t ->
Zelus.exp Zelus.match_handler list ->
Zelus.exp Zelus.match_handler listval 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 listval local : Ident.S.t -> Zelus.local -> Zelus.localval scondpat : Ident.S.t -> Zelus.scondpat -> Zelus.scondpatval automaton :
Ident.S.t ->
Zelus.is_weak ->
Zelus.state_handler list ->
Zelus.state_exp option ->
Zelus.eqan extended list containing eq_list and new equations
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