Module Mlw_decl

module Mlw_decl: sig .. end

Program Declarations




Type declaration


type constructor = Mlw_expr.plsymbol * Mlw_expr.plsymbol option list 
type data_decl = Mlw_ty.T.itysymbol * constructor list * Mlw_ty.post 

Declaration type


type pdecl = private {
   pd_node : pdecl_node;
   pd_syms : Ident.Sid.t;
   pd_news : Ident.Sid.t;
   pd_tag : int;
}
type pdecl_node = private 
| PDtype of Mlw_ty.T.itysymbol
| PDdata of data_decl list
| PDval of Mlw_expr.let_sym
| PDlet of Mlw_expr.let_defn
| PDrec of Mlw_expr.fun_defn list
| PDexn of Mlw_ty.xsymbol

Marks


val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val ity_mark : Mlw_ty.T.ity
val pv_old : Mlw_ty.pvsymbol

Declaration constructors


type pre_field = Ident.preid option * Mlw_expr.field 
type pre_constructor = Ident.preid * pre_field list 
type pre_data_decl = Mlw_ty.T.itysymbol * pre_constructor list 
val create_data_decl : pre_data_decl list -> pdecl
val create_ty_decl : Mlw_ty.T.itysymbol -> pdecl
val create_val_decl : Mlw_expr.let_sym -> pdecl
val create_let_decl : Mlw_expr.let_defn -> pdecl
val create_rec_decl : Mlw_expr.fun_defn list -> pdecl
val create_exn_decl : Mlw_ty.xsymbol -> pdecl

Type invariants


val null_invariant : Mlw_ty.T.itysymbol -> Mlw_ty.post
val add_invariant : pdecl -> Mlw_ty.T.itysymbol -> Mlw_ty.post -> pdecl

Cloning


val clone_data_decl : Mlw_expr.symbol_map -> pdecl -> pdecl

Known identifiers


type known_map = pdecl Ident.Mid.t 
val known_id : known_map -> Ident.ident -> unit
val known_add_decl : Decl.known_map -> known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
val find_constructors : known_map -> Mlw_ty.T.itysymbol -> constructor list
val find_invariant : known_map -> Mlw_ty.T.itysymbol -> Mlw_ty.post
val find_definition : known_map -> Mlw_expr.psymbol -> Mlw_expr.fun_defn option
exception NonupdatableType of Mlw_ty.T.ity
val inst_constructors : Decl.known_map ->
known_map ->
Mlw_ty.T.ity -> (Term.lsymbol * Mlw_expr.field list) list