zelus 2.2 (latest) · OCaml Package

val moduleident : Zident.t -> Zident.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 * Zident.t list Zident.Env.t

val state_value : Deftypes.typ -> Deftypes.tentry

val state_parameter : bool -> Deftypes.typ -> Deftypes.tentry

val env_of_parameters : 
  Zident.t list Zident.Env.t ->
  Zelus.state_handler list ->
  Zelus.state_exdesc Zelus.localized option ->
  Deftypes.tentry Zident.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 : Zident.S.t -> Zelus.exp -> Zelus.exp

val equation : Zident.S.t -> Zelus.eq -> Zelus.eq

Translating an equation. lnames defines names x that must be

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

val block_eq_list : 
  Zident.S.t ->
  Zelus.eq list Zelus.block ->
  Zelus.eq list Zelus.block

val present_handler_exp_list : 
  Zident.S.t ->
  Zelus.exp Zelus.present_handler list ->
  Zelus.exp Zelus.present_handler list

val present_handler_block_eq_list : 
  Zident.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 : 
  Zident.S.t ->
  Zelus.exp Zelus.match_handler list ->
  Zelus.exp Zelus.match_handler list

val match_handler_block_eq_list : 
  Zident.S.t ->
  Zelus.eq list Zelus.block Zelus.match_handler list ->
  Zelus.eq list Zelus.block Zelus.match_handler list

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

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

val automaton : 
  Zident.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

package zelus