zelus 2.2 · OCaml Package

val find_value : 
  Zlocation.location ->
  Lident.t ->
  Global.value_desc Global.info

val find_type : Zlocation.location -> Lident.t -> Global.type_desc Global.info

val find_constr : 
  Zlocation.location ->
  Lident.t ->
  Global.constr_desc Global.info

val find_label : 
  Zlocation.location ->
  Lident.t ->
  Global.label_desc Global.info

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 lift : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.kind ->
  Deftypes.kind

val sort_less_than : 
  Zlocation.location ->
  Deftypes.tsort ->
  Deftypes.kind ->
  unit

val check_is_vec : 
  Zlocation.location ->
  Deftypes.typ ->
  Deftypes.typ * Deftypes.size

val expansive : Zelus.exp -> bool

val check_statefull : Zlocation.location -> Deftypes.kind -> unit

type state = {

mutable s_reset : bool option;
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

val turn_vars_into_memories : 
  Deftypes.tentry Zident.Env.t ->
  Deftypes.defnames ->
  Deftypes.tentry Zident.Env.t * Deftypes.tentry Zident.Env.t

val immediate : Deftypes.immediate -> Deftypes.typ_desc Deftypes.loc

Typing immediate values

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

val vars : Zelus.pattern -> Zident.S.t

Variables in a pattern

val var : Zlocation.location -> 'a Zident.Env.t -> Zident.Env.key -> 'a

Types for local identifiers

val typ_of_var : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val last : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val derivative : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val pluseq : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val init : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val next : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  Deftypes.typ

val def : 
  Zlocation.location ->
  Deftypes.tentry Zident.Env.t ->
  Zident.Env.key ->
  unit

val global : 
  Zlocation.location ->
  Deftypes.kind ->
  Lident.t ->
  Lident.qualident * Deftypes.typ

Types for global identifiers

val global_with_instance : 
  Zlocation.location ->
  Deftypes.kind ->
  Lident.t ->
  Lident.qualident * Deftypes.typ_instance * Deftypes.typ

val label : 
  Zlocation.location ->
  Lident.t ->
  Lident.qualident * Global.label_desc

val constr : 
  Zlocation.location ->
  Lident.t ->
  Lident.qualident * Global.constr_desc

val get_all_labels : 
  Zlocation.location ->
  Deftypes.typ ->
  Global.label_desc Global.info list

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

val constant : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.typ ->
  Deftypes.constant ->
  unit

val vardec_list : 
  Deftypes.kind ->
  Zelus.vardec list ->
  Zident.S.t ->
  Deftypes.tentry Zident.Env.t

val build : (Zident.S.t * Zident.S.t) -> Zelus.eq -> Zident.S.t * Zident.S.t

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

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

val env_of_statepat : 
  Deftypes.kind ->
  Zelus.statepatdesc Zelus.localized ->
  Deftypes.tentry Zident.Env.t

val env_of_pattern_list : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.pattern list ->
  Deftypes.tentry Zident.Env.t

val env_of_pattern : 
  Deftypes.kind ->
  Zelus.pattern ->
  Deftypes.tentry Zident.Env.t

val pattern : 
  Deftypes.tentry Zident.Env.t ->
  Zelus.pattern ->
  Deftypes.typ ->
  unit

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

val match_handlers : 
  (Deftypes.kind ->
    Deftypes.tentry Zident.Env.t ->
    'a ->
    'b ->
    Deftypes.defnames) ->
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  bool ref ->
  'a Zelus.match_handler list ->
  Deftypes.typ ->
  'b ->
  Deftypes.defnames

Typing a pattern matching. Returns defined names

val present_handlers : 
  (Deftypes.kind ->
    bool ->
    Deftypes.tentry Zident.Env.t ->
    Zelus.scondpat ->
    'a) ->
  (Deftypes.kind ->
    Deftypes.tentry Zident.Env.t ->
    'b ->
    'c ->
    Deftypes.defnames) ->
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  'b Zelus.present_handler list ->
  'b option ->
  'c ->
  Deftypes.defnames

it is the kind of the context.

val expression : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.exp ->
  Deftypes.typ

val size : Deftypes.tentry Zident.Env.t -> Zelus.size -> Deftypes.size

Typing a size expression

val size_of_exp : Zelus.exp -> Deftypes.size

Convert an expression into a size expression

val operator : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zlocation.location ->
  Zelus.op ->
  Zelus.exp list ->
  Deftypes.typ

The type of primitives and imported functions

val period : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.exp Zelus.period ->
  unit

val expect : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.exp ->
  Deftypes.typ ->
  unit

Typing an expression with expected type expected_type

val apply : 
  Zlocation.location ->
  bool ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.exp ->
  Zelus.exp list ->
  Deftypes.typ

val equation : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.eq ->
  Deftypes.defnames

Typing an equation. Returns the set of defined names

val equation_list : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.eq list ->
  Deftypes.defnames

val present_handler_exp_list : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.exp Zelus.present_handler list ->
  Zelus.exp option ->
  Deftypes.typ ->
  Deftypes.defnames

Type a present handler when the body is an expression

val present_handler_block_eq_list : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.eq list Zelus.block Zelus.present_handler list ->
  Zelus.eq list Zelus.block option ->
  Deftypes.defnames

val match_handler_block_eq_list : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.total ref ->
  Zelus.eq list Zelus.block Zelus.match_handler list ->
  Deftypes.typ ->
  Deftypes.defnames

val match_handler_exp_list : 
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.total ref ->
  Zelus.exp Zelus.match_handler list ->
  Deftypes.typ ->
  Deftypes.typ ->
  Deftypes.defnames

val block_eq_list : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.eq list Zelus.block ->
  Deftypes.tentry Zident.Env.t * Deftypes.defnames

val local : 
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.local ->
  Deftypes.tentry Zident.Env.t

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

val automaton_handlers : 
  Zelus.is_weak ->
  Zlocation.location ->
  Deftypes.kind ->
  Deftypes.tentry Zident.Env.t ->
  Zelus.state_handler list ->
  Zelus.state_exp option ->
  Deftypes.defnames

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 funtype : 
  Zlocation.location ->
  Deftypes.kind ->
  Zelus.pattern list ->
  Deftypes.typ list ->
  Deftypes.typ ->
  Deftypes.typ

val constdecl : 'a -> bool -> Zelus.exp -> Deftypes.typ_scheme

val fundecl : Zlocation.location -> 'a -> Zelus.funexp -> Deftypes.typ_scheme

val implementation : 
  Format.formatter ->
  bool ->
  Zelus.implementation_desc Zelus.localized ->
  unit

val implementation_list : 
  Format.formatter ->
  bool ->
  Zelus.implementation_desc Zelus.localized list ->
  Zelus.implementation_desc Zelus.localized list

package zelus