zelus 2.2 · OCaml Package

type error =

| Iless_than of Definit.ti * Definit.ti
| Iless_than_i of Definit.t * Definit.t
| Ilast of Zident.t
| Ivar of Zident.t
| 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

val build_env : 
  Zlocation.location ->
  bool ->
  Deftypes.tentry Zident.Env.t ->
  Init.tentry Zident.Env.t ->
  Init.tentry Zident.Env.t

Build an environment from a typing environment

val half : Init.tentry Zident.Env.t -> Init.tentry Zident.Env.t

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

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 split : 
  Zelus.state_exdesc Zelus.localized option ->
  Zelus.state_handler list ->
  Zelus.state_handler * Zelus.state_handler list

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 ->
  'a 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 ->
  'b Zelus.present_handler list ->
  unit

Present handler

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

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 block_eq_list : 
  Zident.S.t ->
  bool ->
  Init.tentry Zident.Env.t ->
  Zelus.eq list Zelus.block ->
  Init.tentry Zident.Env.t

val local : 
  bool ->
  Init.tentry Zident.Env.t ->
  Zelus.local ->
  Init.tentry Zident.Env.t

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

package zelus