package zelus

  1. Overview
  2. Docs
type error =
  1. | Iless_than of Definit.ti * Definit.ti
  2. | Iless_than_i of Definit.t * Definit.t
  3. | Ilast of Zident.t
  4. | Ivar of Zident.t
  5. | Ider of Zident.t
exception Error of Zlocation.location * error
val error : Zlocation.location -> error -> 'a
val message : Zlocation.location -> error -> 'a
val less_than : Zlocation.location -> Definit.ti -> Definit.ti -> unit
val less_for_last : Zlocation.location -> Zident.t -> Definit.t -> Definit.t -> unit
val less_for_var : Zlocation.location -> Zident.t -> Definit.ti -> Definit.ti -> unit

Build an environment from a typing environment

Build an environment from env by replacing the initialization

val add_last_to_env : bool -> Init.tentry Zident.Env.t -> Zident.S.t -> Init.tentry Zident.Env.t
val print : Zident.t -> 'a
val initialized : Zlocation.location -> Init.tentry Zident.Env.t -> Zident.S.t -> unit

Check that partially defined names have a last value which is initialized

val pattern : bool -> Init.tentry Zident.Env.t -> Zelus.pattern -> Definit.ti -> unit

Patterns

val pattern_less_than_on_i : bool -> Init.tentry Zident.Env.t -> Zelus.pattern -> Definit.t -> unit
val match_handlers : bool -> (bool -> Init.tentry Zident.Env.t -> 'a -> 'b) -> Init.tentry Zident.Env.t -> 'c Zelus.match_handler list -> unit

Match handler

val present_handlers : bool -> (bool -> Init.tentry Zident.Env.t -> Zelus.scondpat -> 'a) -> (bool -> Init.tentry Zident.Env.t -> 'b -> 'c) -> Init.tentry Zident.Env.t -> 'd Zelus.present_handler list -> unit

Present handler

Initialization of an expression

val operator : bool -> Init.tentry Zident.Env.t -> Zelus.op -> Deftypes.typ -> Zelus.exp list -> Definit.ti

Typing an operator

val app : bool -> Init.tentry Zident.Env.t -> Definit.ti -> Zelus.exp list -> Definit.ti

Typing an application

val exp_less_than_on_i : bool -> Init.tentry Zident.Env.t -> Zelus.exp -> Definit.t -> unit
val opt_exp_less_than_on_i : bool -> Init.tentry Zident.Env.t -> Zelus.exp option -> Definit.t -> unit
val exp_less_than : bool -> Init.tentry Zident.Env.t -> Zelus.exp -> Definit.ti -> unit
val equation_list : bool -> Init.tentry Zident.Env.t -> Zelus.eq list -> unit

Checking equations

val equation : bool -> Init.tentry Zident.Env.t -> Zelus.eq -> unit
val present_handler_exp_list : bool -> Init.tentry Zident.Env.t -> Zelus.exp Zelus.present_handler list -> Definit.ti -> unit
val present_handler_block_eq_list : bool -> Zident.S.t -> Init.tentry Zident.Env.t -> Deftypes.defnames -> Zelus.eq list Zelus.block Zelus.present_handler list -> unit
val match_handler_block_eq_list : bool -> Zident.S.t -> Init.tentry Zident.Env.t -> Deftypes.defnames -> Zelus.eq list Zelus.block Zelus.match_handler list -> unit
val match_handler_exp_list : bool -> Init.tentry Zident.Env.t -> Zelus.exp Zelus.match_handler list -> Definit.ti -> unit
val scondpat : bool -> Init.tentry Zident.Env.t -> Zelus.scondpat -> unit
val implementation : Stdlib.Format.formatter -> Zelus.implementation_desc Zelus.localized -> unit
val implementation_list : Stdlib.Format.formatter -> Zelus.implementation_desc Zelus.localized list -> Zelus.implementation_desc Zelus.localized list