zelus 2.1 · OCaml Package

module Error : sig ... end

module S : sig ... end

type defnames = S.t

module Rename : sig ... end

val emake : Location.location -> Zelus.desc -> Zelus.exp

val eqmake : Location.location -> Zelus.eqdesc -> Zelus.eq

val pmake : Location.location -> Zelus.pdesc -> Zelus.pattern

val var : Location.location -> Ident.t -> Zelus.exp

val varpat : Location.location -> Ident.t -> Zelus.pattern

val eblock : 'a -> 'a Zelus.block

val block_with_emit : (Zelus.exp -> 'a) -> Zelus.exp -> 'a list Zelus.block

val block_with_result : Ident.t -> Zelus.eq list -> Zelus.eq list Zelus.block

val name_with_sort : 
  bool ->
  Location.location ->
  Rename.value Rename.t ->
  Rename.key ->
  Ident.t

val name : Location.location -> Rename.value Rename.t -> Rename.key -> Ident.t

val shortname : Parsetree.longname -> Parsetree.name

val longname : Parsetree.longname -> Lident.t

val immediate : Parsetree.immediate -> Deftypes.immediate

val constant : Parsetree.constant -> Deftypes.constant

val default : 
  Parsetree.constant Parsetree.default ->
  Deftypes.constant Zelus.default

val kind : Parsetree.kind -> Zelus.kind

val types : 
  Rename.value Rename.t ->
  Parsetree.type_expression ->
  Zelus.type_expression

val size : Rename.value Rename.t -> Parsetree.size -> Zelus.size

val operator : 'a -> Rename.value Rename.t -> Parsetree.op -> Zelus.op

val build : bool -> S.t -> Parsetree.pattern -> S.t

if check_linear = true, stop when the same name appears twice

val build_list : bool -> S.t -> Parsetree.pattern list -> S.t

val build_equation_list : S.t -> Parsetree.eq list -> S.t

Builds the set of names defined in a list of equations

val build_equation : S.t -> Parsetree.eq -> S.t

val build_block_equation_list : 
  S.t ->
  Parsetree.eq list Parsetree.block ->
  S.t * S.t

val build_automaton_handler : 
  S.t ->
  Parsetree.eq list Parsetree.block ->
  Parsetree.escape list ->
  Parsetree.escape list ->
  S.t

val check_pattern : Rename.value Rename.t -> Parsetree.pattern -> Zelus.pattern

Renaming of a pattern

val check_pattern_list : 
  Rename.value Rename.t ->
  Parsetree.pattern list ->
  Zelus.pattern list

val pattern : 
  Rename.value Rename.t ->
  Parsetree.pattern ->
  Rename.value Rename.t * Rename.value Rename.t * Zelus.pattern

val pattern_list : 
  Rename.value Rename.t ->
  Parsetree.pattern list ->
  Rename.value Rename.t * Rename.value Rename.t * Zelus.pattern list

val match_handler_list : 
  ('a -> Rename.value Rename.t -> 'b -> 'c) ->
  'a ->
  Rename.value Rename.t ->
  'b Parsetree.match_handler list ->
  'c Zelus.match_handler list

Two generic functions for control blocks (present/match)

val present_handler_list : 
  ('a -> Parsetree.scondpat -> Rename.value Rename.t * 'b * Zelus.scondpat) ->
  ('c -> 'b -> 'd -> 'e) ->
  'c ->
  'a ->
  'd Parsetree.present_handler list ->
  'e Zelus.present_handler list

val state_handler_list : 
  Location.location ->
  (Rename.value Rename.t ->
    Parsetree.scondpat ->
    Rename.value Rename.t * Rename.value Rename.t * Zelus.scondpat) ->
  ('a ->
    Rename.value Rename.t ->
    'b Parsetree.block ->
    Rename.value Rename.t * Zelus.eq list Zelus.block) ->
  ('a ->
    Rename.value Rename.t ->
    Parsetree.eq list Parsetree.block ->
    Rename.value Rename.t * Zelus.eq list Zelus.block) ->
  (Rename.value Rename.t -> Parsetree.exp -> Zelus.exp) ->
  'a ->
  Rename.value Rename.t ->
  'b Parsetree.state_handler_desc Parsetree.localized list ->
  Parsetree.state_exp_desc Parsetree.localized option ->
  bool * Zelus.state_handler list * Zelus.state_exdesc Zelus.localized option

Translate automata

val vardec : 
  (Rename.value Rename.t * Zelus.vardec list) ->
  Parsetree.vardecdesc Parsetree.localized ->
  Rename.value Rename.t * Zelus.vardec list

val block : 
  (Rename.value Rename.t -> Parsetree.local list -> 'a * Zelus.local list) ->
  (Rename.value Rename.t -> 'a -> 'b -> 'c) ->
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  'b Parsetree.block_desc Parsetree.localized ->
  'a * 'c Zelus.block

val expression : Rename.value Rename.t -> Parsetree.exp -> Zelus.exp

Scoping an expression

val recordrec : 
  Location.location ->
  Rename.value Rename.t ->
  (Parsetree.longname * Parsetree.exp) list ->
  (Lident.t * Zelus.exp) list

val period : 
  Rename.value Rename.t ->
  Parsetree.period ->
  Zelus.exp Zelus.period

val equation : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Zelus.eq list ->
  Parsetree.eq ->
  Zelus.eq list

val equation_list : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.eq list ->
  Zelus.eq list

val local : 
  Rename.value Rename.t ->
  Parsetree.local ->
  Rename.value Rename.t * Zelus.local

Translating a sequence of local declarations

val locals : 
  Rename.value Rename.t ->
  Parsetree.local list ->
  Rename.value Rename.t * Zelus.local list

val letin : 
  Parsetree.is_rec ->
  Rename.value Rename.t ->
  Parsetree.eq list ->
  Rename.value Rename.t * Rename.value Rename.t * Zelus.eq list

val present_handler_exp_list : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.exp Parsetree.present_handler list ->
  Zelus.exp Zelus.present_handler list

Translate a present and match when handlers are expressions or equations

val present_handler_block_eq_list : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.eq list Parsetree.block Parsetree.present_handler list ->
  Zelus.eq list Zelus.block Zelus.present_handler list

val match_handler_block_eq_list : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.eq list Parsetree.block Parsetree.match_handler list ->
  Zelus.eq list Zelus.block Zelus.match_handler list

val block_eq_list : 
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.eq list Parsetree.block ->
  Rename.value Rename.t * Zelus.eq list Zelus.block

Translate a block when the body is a list of equations

val state_handler_eq_list : 
  Location.location ->
  Rename.value Rename.t ->
  Rename.value Rename.t ->
  Parsetree.eq list Parsetree.state_handler list ->
  Parsetree.state_exp option ->
  Zelus.is_weak * Zelus.state_handler list * Zelus.state_exp option

Translate an automaton

val scondpat : 
  Rename.value Rename.t ->
  Parsetree.scondpat ->
  Rename.value Rename.t * Rename.value Rename.t * Zelus.scondpat

val type_decl : 
  Parsetree.type_decl_desc Parsetree.localized ->
  Zelus.type_decl_desc Zelus.localized

val constr_decl : Parsetree.constr_decl -> Zelus.constr_decl

val type_decls : 
  ('a * 'b * Parsetree.type_decl_desc Parsetree.localized) list ->
  ('a * 'b * Zelus.type_decl_desc Zelus.localized) list

val implementation : 
  Parsetree.implementation_desc Parsetree.localized ->
  Zelus.implementation_desc Zelus.localized

val implementation_list : 
  Parsetree.implementation_desc Parsetree.localized list ->
  Zelus.implementation_desc Zelus.localized list

val interface : 
  Parsetree.interface_desc Parsetree.localized ->
  Zelus.interface_desc Zelus.localized

val interface_list : 
  Parsetree.interface_desc Parsetree.localized list ->
  Zelus.interface_desc Zelus.localized list

package zelus