package zelus

  1. Overview
  2. Docs
val unify : Zlocation.location -> Deftypes.typ -> Deftypes.typ -> unit

The main unification functions

val equal_sizes : Zlocation.location -> Deftypes.size -> Deftypes.size -> unit
val unify_expr : Zelus.exp -> Deftypes.typ -> Deftypes.typ -> unit
val unify_pat : Zelus.pattern -> Deftypes.typ -> Deftypes.typ -> unit
val less_than : Zlocation.location -> Deftypes.kind -> Deftypes.kind -> unit
val type_is_in_kind : Zlocation.location -> Deftypes.kind -> Deftypes.typ -> unit
val sort_less_than : Zlocation.location -> Deftypes.tsort -> Deftypes.kind -> unit
val expansive : Zelus.exp -> bool
val check_statefull : Zlocation.location -> Deftypes.kind -> unit
type state = {
  1. mutable s_reset : bool option;
  2. s_parameters : Deftypes.typ list;
}

We emit a warning when a state is entered both by reset and history

val check_target_state : Zlocation.location -> bool option -> bool -> bool option

Typing immediate values

val incorporate_into_env : Deftypes.tentry Zident.Env.t -> Deftypes.tentry Zident.Env.t -> unit

Variables in a pattern

Types for local identifiers

Types for global identifiers

val check_definitions_for_every_name : Deftypes.defnames -> Zelus.vardec list -> Deftypes.defnames

have been removed

Typing a declaration

val combine : Zlocation.location -> 'a -> Lident.t -> unit

Computes the set of names defined in a list of definitions

val build_list : (Zident.S.t * Zident.S.t) -> Zelus.eq list -> Zident.S.t * Zident.S.t
val env_of_eq_list : Deftypes.kind -> Zelus.eq list -> Deftypes.tentry Zident.Env.t
val intro_sort_of_var : Deftypes.kind -> Deftypes.tsort

Typing patterns

val pattern_list : Deftypes.tentry Zident.Env.t -> Zelus.pattern list -> Deftypes.typ list -> unit
val check_total_pattern : Patternsig.LANG.pattern_ast -> unit
val check_total_pattern_list : Patternsig.LANG.pattern_ast list -> unit

Typing a pattern matching. Returns defined names

it is the kind of the context.

Typing a size expression

val size_of_exp : Zelus.exp -> Deftypes.size

Convert an expression into a size expression

The type of primitives and imported functions

Typing an expression with expected type expected_type

Typing an equation. Returns the set of defined names

Type a present handler when the body is an expression

val scondpat : Deftypes.kind -> bool -> Deftypes.tentry Zident.Env.t -> Zelus.scondpat -> unit

Typing a signal condition

val typing_state : Deftypes.tentry Zident.Env.t -> state Zident.Env.t -> bool -> Zelus.state_exp -> unit
val mark_reset_state : state Zident.Env.t -> Zelus.state_handler list -> unit

Typing an automaton. Returns defined names

val no_unbounded_name : Zlocation.location -> Zident.S.t -> Deftypes.typ -> Deftypes.typ

Check that size variables are all bounded

val constdecl : 'a -> bool -> Zelus.exp -> Deftypes.typ_scheme
val implementation : Format.formatter -> bool -> Zelus.implementation_desc Zelus.localized -> unit
OCaml

Innovation. Community. Security.