zelus 2.2 (latest) · OCaml Package

val print : Zident.t -> 'a

type error = {

kind : kind;
cycle : Causal.cycle;
env : Causal.tentry Zident.Env.t;

}

and kind =

| Cless_than of Defcaus.tc * Defcaus.tc
| Cless_than_name of Zident.t * Defcaus.tc * Defcaus.tc

exception Error of Zlocation.location * error

val error : Zlocation.location -> error -> 'a

val message : Zlocation.location -> error -> 'a

val less_than : 
  Zlocation.location ->
  Causal.tentry Zident.Env.t ->
  Defcaus.tc ->
  Defcaus.tc ->
  unit

val less_than_name : 
  Zlocation.location ->
  Causal.tentry Zident.Env.t ->
  Zident.t ->
  Defcaus.tc ->
  Defcaus.tc ->
  unit

val less_than_c : 
  Zlocation.location ->
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Defcaus.t ->
  unit

val pattern : Causal.tentry Zident.Env.t -> Zelus.pattern -> Defcaus.tc

Typing a pattern. pattern env p = tc where tc is the type

val build_env : 
  Deftypes.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t

Build an environment from a typing environment.

val build_env_on_c : 
  Defcaus.t ->
  Deftypes.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t

Build an environment with all entries synchronised on c

val def_env : 
  Zlocation.location ->
  Deftypes.defnames ->
  Causal.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t

Build an environment for a set of written variables

val def_env_on_c : 
  Zlocation.location ->
  Deftypes.defnames ->
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zident.S.t * Causal.tentry Zident.Env.t

Build an environment for a set of written variables

val last_env : 
  Zident.S.t ->
  Deftypes.defnames ->
  Causal.tentry Zident.Env.t ->
  Causal.tentry Zident.Env.t

Build an environment from env by replacing the causality

val match_handlers : 
  (Causal.tentry Zident.Env.t -> 'a -> 'b -> 'c) ->
  Causal.tentry Zident.Env.t ->
  'a ->
  Defcaus.t ->
  'b Zelus.match_handler list ->
  'c list

Causality analysis of a match handler.

val present_handlers : 
  (Causal.tentry Zident.Env.t -> 'a -> Zelus.scondpat -> Defcaus.t) ->
  (Causal.tentry Zident.Env.t -> 'b -> 'c -> 'd) ->
  Causal.tentry Zident.Env.t ->
  'a ->
  Defcaus.t ->
  'b ->
  'c Zelus.present_handler list ->
  'c option ->
  'd list

Causality analysis of a present handler

val exp : Causal.tentry Zident.Env.t -> Defcaus.t -> Zelus.exp -> Defcaus.tc

causality of an expression. C | H |-cfree e: ct

val app : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Defcaus.tc ->
  Zelus.exp list ->
  Defcaus.tc

Typing an application

val operator : 
  Causal.tentry Zident.Env.t ->
  Zelus.op ->
  Defcaus.t ->
  Deftypes.typ ->
  Zelus.exp list ->
  Defcaus.tc

Typing an operator

val exp_less_than_on_c : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.exp ->
  Defcaus.t ->
  unit

Typing an expression with an expected causality

val exp_less_than : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.exp ->
  Defcaus.tc ->
  unit

val equation_list : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.eq list ->
  unit

Typing a list of equations env |-c eq list

val equation : Causal.tentry Zident.Env.t -> Defcaus.t -> Zelus.eq -> unit

Typing of an equation. env |-cfree eq

val present_handler_exp_list : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Defcaus.t ->
  Defcaus.t ->
  Zelus.exp Zelus.present_handler list ->
  Zelus.exp option ->
  Defcaus.tc

val present_handler_block_eq_list : 
  Causal.tentry Zident.Env.t ->
  Zident.S.t ->
  Defcaus.t ->
  Defcaus.t ->
  Defcaus.t ->
  Zelus.eq list Zelus.block Zelus.present_handler list ->
  Zelus.eq list Zelus.block option ->
  unit

val match_handler_exp_list : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Defcaus.t ->
  Zelus.exp Zelus.match_handler list ->
  Defcaus.tc

val match_handler_block_eq_list : 
  Causal.tentry Zident.Env.t ->
  Zident.S.t ->
  Defcaus.t ->
  Defcaus.t ->
  Zelus.eq list Zelus.block Zelus.match_handler list ->
  unit

val block_eq_list : 
  Zident.S.t ->
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.eq list Zelus.block ->
  Causal.tentry Zident.Env.t

val local : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.local ->
  Causal.tentry Zident.Env.t

val scondpat : 
  Causal.tentry Zident.Env.t ->
  Defcaus.t ->
  Zelus.scondpat ->
  Defcaus.t

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

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

package zelus