package zelus

  1. Overview
  2. Docs
package zelus
Legend:
Library
Module
Module type
Parameter
Class
Class type
type name = string
type op =
  1. | Lunarypre
  2. | Lfby
  3. | Lminusgreater
  4. | Lifthenelse
  5. | Lsharp
  6. | Lop of Lident.t
type immediate =
  1. | Lint of int
  2. | Lfloat of float
  3. | Lbool of bool
  4. | Lchar of char
  5. | Lstring of string
  6. | Lvoid
type constr0pat =
  1. | Lconstr0pat of Lident.t
  2. | Lboolpat of bool
type exp =
  1. | Llocal of Zident.t
  2. | Llast of Zident.t
  3. | Lglobal of Lident.t
  4. | Lconst of immediate
  5. | Lconstr0 of Lident.t
  6. | Lapp of op * exp list
  7. | Lrecord_access of exp * Lident.t
  8. | Lrecord of (Lident.t * exp) list
  9. | Ltuple of exp list
  10. | Lget of exp * int
  11. | Lmerge of exp * (constr0pat * exp) list
  12. | Lwhen of exp * constr0pat * exp
type clock =
  1. | Ck_base
  2. | Ck_on of clock * constr0pat * exp
type reset =
  1. | Res_never
  2. | Res_else of reset * exp
type eq = {
  1. eq_kind : kind;
  2. eq_ident : Zident.t;
  3. eq_exp : exp;
  4. eq_clock : clock;
}
and kind =
  1. | Def
  2. | Init of reset
  3. | Next
type funexp = {
  1. f_inputs : Zident.t list;
  2. f_output : Zident.t;
  3. f_env : tentry Zident.Env.t;
  4. f_body : eq list;
  5. f_assert : exp list;
}
and tentry = {
  1. t_typ : typ;
}
and implementation =
  1. | Lconstdecl of name * exp
  2. | Lfundecl of name * funexp
  3. | Ltypedecl of name * type_decl
and type_decl =
  1. | Labstract_type
  2. | Lvariant_type of name list
  3. | Lrecord_type of (name * typ) list
and typ =
  1. | Tint
  2. | Tbool
  3. | Tfloat
  4. | Tchar
  5. | Tstring
  6. | Tunit
  7. | Tconstr of Lident.qualident
  8. | Tproduct of typ list