package zelus

  1. Overview
  2. Docs
package zelus
Legend:
Library
Module
Module type
Parameter
Class
Class type
type kind =
  1. | S
  2. | A
  3. | C
  4. | D
  5. | AD
  6. | AS
  7. | P
type name = string
type 'a localized = {
  1. desc : 'a;
  2. loc : Zlocation.location;
}
type type_expression = type_expression_desc localized

Types

and type_expression_desc =
  1. | Etypevar of string
  2. | Etypeconstr of Lident.t * type_expression list
  3. | Etypetuple of type_expression list
  4. | Etypevec of type_expression * size
  5. | Etypefun of kind * Zident.t option * type_expression * type_expression
and size = size_desc localized
and size_desc =
  1. | Sconst of int
  2. | Sglobal of Lident.t
  3. | Sname of Zident.t
  4. | Sop of size_op * size * size
and size_op =
  1. | Splus
  2. | Sminus
type interface = interface_desc localized

Declarations and expressions

and interface_desc =
  1. | Einter_open of name
  2. | Einter_typedecl of name * name list * type_decl
  3. | Einter_constdecl of name * type_expression
and type_decl = type_decl_desc localized
and type_decl_desc =
  1. | Eabstract_type
  2. | Eabbrev of type_expression
  3. | Evariant_type of constr_decl list
  4. | Erecord_type of (name * type_expression) list
and constr_decl = constr_decl_desc localized
and constr_decl_desc =
  1. | Econstr0decl of name
  2. | Econstr1decl of name * type_expression list
and implementation = implementation_desc localized
and implementation_desc =
  1. | Eopen of name
  2. | Etypedecl of name * name list * type_decl
  3. | Econstdecl of name * is_static * exp
  4. | Efundecl of name * funexp
and funexp = {
  1. f_kind : kind;
  2. f_atomic : is_atomic;
  3. f_args : pattern list;
  4. f_body : exp;
  5. mutable f_env : Deftypes.tentry Zident.Env.t;
  6. f_loc : Zlocation.location;
}
and is_atomic = bool
and is_static = bool
and exp = {
  1. mutable e_desc : desc;
  2. e_loc : Zlocation.location;
  3. mutable e_typ : Deftypes.typ;
  4. mutable e_caus : Defcaus.tc;
  5. mutable e_init : Definit.ti;
}
and desc =
  1. | Elocal of Zident.t
  2. | Eglobal of {
    1. lname : Lident.t;
    2. typ_instance : Deftypes.typ_instance;
    }
  3. | Econst of immediate
  4. | Econstr0 of Lident.t
  5. | Econstr1 of Lident.t * exp list
  6. | Elast of Zident.t
  7. | Eapp of app * exp * exp list
  8. | Eop of op * exp list
  9. | Etuple of exp list
  10. | Erecord_access of exp * Lident.t
  11. | Erecord of (Lident.t * exp) list
  12. | Erecord_with of exp * (Lident.t * exp) list
  13. | Etypeconstraint of exp * type_expression
  14. | Epresent of exp present_handler list * exp option
  15. | Ematch of total Stdlib.ref * exp * exp match_handler list
  16. | Elet of local * exp
  17. | Eseq of exp * exp
  18. | Eperiod of exp period
  19. | Eblock of eq list block * exp
and is_rec = bool
and op =
  1. | Efby
  2. | Eunarypre
  3. | Eifthenelse
  4. | Eminusgreater
  5. | Eup
  6. | Einitial
  7. | Edisc
  8. | Ehorizon
  9. | Etest
  10. | Eaccess
  11. | Eupdate
  12. | Eslice of size * size
  13. | Econcat
  14. | Eatomic
and immediate = Deftypes.immediate
and app = {
  1. app_inline : bool;
  2. app_statefull : bool;
}
and 'a period = {
  1. p_phase : 'a option;
  2. p_period : 'a;
}
and pattern = {
  1. mutable p_desc : pdesc;
  2. p_loc : Zlocation.location;
  3. mutable p_typ : Deftypes.typ;
  4. mutable p_caus : Defcaus.tc;
  5. mutable p_init : Definit.ti;
}
and pdesc =
  1. | Ewildpat
  2. | Econstpat of immediate
  3. | Econstr0pat of Lident.t
  4. | Econstr1pat of Lident.t * pattern list
  5. | Etuplepat of pattern list
  6. | Evarpat of Zident.t
  7. | Ealiaspat of pattern * Zident.t
  8. | Eorpat of pattern * pattern
  9. | Erecordpat of (Lident.t * pattern) list
  10. | Etypeconstraintpat of pattern * type_expression
and eq = {
  1. eq_desc : eqdesc;
  2. eq_loc : Zlocation.location;
  3. eq_index : int;
  4. eq_safe : bool;
  5. mutable eq_write : Deftypes.defnames;
}
and eqdesc =
  1. | EQeq of pattern * exp
  2. | EQder of Zident.t * exp * exp option * exp present_handler list
  3. | EQinit of Zident.t * exp
  4. | EQnext of Zident.t * exp * exp option
  5. | EQpluseq of Zident.t * exp
  6. | EQautomaton of is_weak * state_handler list * state_exp option
  7. | EQpresent of eq list block present_handler list * eq list block option
  8. | EQmatch of total Stdlib.ref * exp * eq list block match_handler list
  9. | EQreset of eq list * exp
  10. | EQemit of Zident.t * exp option
  11. | EQblock of eq list block
  12. | EQand of eq list
  13. | EQbefore of eq list
  14. | EQforall of forall_handler
and total = bool
and is_next = bool
and is_weak = bool
and 'a block = {
  1. b_vars : vardec list;
  2. b_locals : local list;
  3. b_body : 'a;
  4. b_loc : Zlocation.location;
  5. mutable b_env : Deftypes.tentry Zident.Env.t;
  6. mutable b_write : Deftypes.defnames;
}
and vardec = {
  1. vardec_name : Zident.t;
  2. vardec_default : Deftypes.constant default option;
  3. vardec_combine : Lident.t option;
  4. vardec_loc : Zlocation.location;
}
and 'a default =
  1. | Init of 'a
  2. | Default of 'a
and local = {
  1. l_rec : is_rec;
  2. l_eq : eq list;
  3. mutable l_env : Deftypes.tentry Zident.Env.t;
  4. l_loc : Zlocation.location;
}
and state_handler = {
  1. s_loc : Zlocation.location;
  2. s_state : statepat;
  3. s_body : eq list block;
  4. s_trans : escape list;
  5. mutable s_env : Deftypes.tentry Zident.Env.t;
  6. mutable s_reset : bool;
}
and statepat = statepatdesc localized
and statepatdesc =
  1. | Estate0pat of Zident.t
  2. | Estate1pat of Zident.t * Zident.t list
and state_exp = state_exdesc localized
and state_exdesc =
  1. | Estate0 of Zident.t
  2. | Estate1 of Zident.t * exp list
and escape = {
  1. e_cond : scondpat;
  2. e_reset : bool;
  3. e_block : eq list block option;
  4. e_next_state : state_exp;
  5. mutable e_env : Deftypes.tentry Zident.Env.t;
  6. mutable e_zero : bool;
}
and scondpat = scondpat_desc localized
and scondpat_desc =
  1. | Econdand of scondpat * scondpat
  2. | Econdor of scondpat * scondpat
  3. | Econdexp of exp
  4. | Econdpat of exp * pattern
  5. | Econdon of scondpat * exp
and 'a match_handler = {
  1. m_pat : pattern;
  2. m_body : 'a;
  3. mutable m_env : Deftypes.tentry Zident.Env.t;
  4. m_reset : bool;
  5. mutable m_zero : bool;
}
and 'a present_handler = {
  1. p_cond : scondpat;
  2. p_body : 'a;
  3. mutable p_env : Deftypes.tentry Zident.Env.t;
  4. mutable p_zero : bool;
}
and forall_handler = {
  1. for_index : indexes_desc localized list;
  2. for_init : init_desc localized list;
  3. for_body : eq list block;
  4. mutable for_in_env : Deftypes.tentry Zident.Env.t;
  5. mutable for_out_env : Deftypes.tentry Zident.Env.t;
  6. for_loc : Zlocation.location;
}
and indexes_desc =
  1. | Einput of Zident.t * exp
  2. | Eoutput of Zident.t * Zident.t
  3. | Eindex of Zident.t * exp * exp
and init_desc =
  1. | Einit_last of Zident.t * exp