Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package gospel
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module Ident = Identifier.Identtype lb_arg = | Lunit(*()
*)| Lnone of Tterm.vsymbol(*x
*)| Loptional of Tterm.vsymbol(*?x
*)| Lnamed of Tterm.vsymbol(*~x
*)| Lghost of Tterm.vsymbol(*[x: t]
*)
type val_spec = {sp_args : lb_arg list;(*Arguments
*)sp_ret : lb_arg list;(*Return values. This is a list because of tuple destruction.
*)sp_pre : Tterm.term list;(*Preconditions
*)sp_checks : Tterm.term list;(*Checks preconditions
*)sp_post : Tterm.term list;(*Postconditions
*)sp_xpost : (Ttypes.xsymbol * (Tterm.pattern * Tterm.term) list) list;(*Exceptional postconditions.
*)sp_wr : Tterm.term list;(*Writes
*)sp_cs : Tterm.term list;(*Consumes
*)sp_diverge : bool;(*Diverges
*)sp_pure : bool;(*Pure
*)sp_equiv : string list;(*Equivalent
*)sp_text : string;(*String containing the original specificaion as written by the user
*)sp_loc : Ppxlib.Location.t;(*Specification location
*)
}type val_description = {vd_name : Ident.t;vd_type : Ppxlib.Parsetree.core_type;vd_prim : string list;(*primitive declaration
*)vd_attrs : Ppxlib.Parsetree.attributes;vd_args : lb_arg list;vd_ret : lb_arg list;vd_spec : val_spec option;vd_loc : Ppxlib.Location.t;
}type type_spec = {ty_ephemeral : bool;(*Ephemeral
*)ty_fields : (Tterm.lsymbol * bool) list;(*Models (field symbol * mutable)
*)ty_invariants : Tterm.term list;(*Invariants
*)ty_text : string;(*String containing the original specificaion as written by the user
*)ty_loc : Ppxlib.Location.t;(*Specification location
*)
}type 'a label_declaration = {ld_field : 'a;ld_mut : mutable_flag;ld_loc : Ppxlib.Location.t;ld_attrs : Ppxlib.Parsetree.attributes;
}type constructor_decl = {cd_cs : Tterm.lsymbol;cd_ld : (Ident.t * Ttypes.ty) label_declaration list;cd_loc : Ppxlib.Location.t;cd_attrs : Ppxlib.Parsetree.attributes;
}type type_kind = | Pty_abstract| Pty_variant of constructor_decl list| Pty_record of rec_declaration| Pty_open
type type_declaration = {td_ts : Ttypes.tysymbol;td_params : (Ttypes.tvsymbol * (Ppxlib.variance * Ppxlib.injectivity)) list;td_cstrs : (Ttypes.ty * Ttypes.ty * Ppxlib.Location.t) list;td_kind : type_kind;td_private : private_flag;td_manifest : Ttypes.ty option;td_attrs : Ppxlib.Parsetree.attributes;td_spec : type_spec option;td_loc : Ppxlib.Location.t;
}type axiom = {ax_name : Ident.t;(*Name
*)ax_term : Tterm.term;(*Definition
*)ax_loc : Ppxlib.Location.t;(*Location
*)ax_text : string;(*String containing the original specificaion as written by the user
*)
}type fun_spec = {fun_req : Tterm.term list;(*Preconditions
*)fun_ens : Tterm.term list;(*Postconditions
*)fun_variant : Tterm.term list;(*Variant
*)fun_coer : bool;(*Coercion
*)fun_text : string;(*String containing the original specificaion as written by the user
*)fun_loc : Ppxlib.Location.t;(*Specification location
*)
}type function_ = {fun_ls : Tterm.lsymbol;(*Function symbol
*)fun_rec : bool;(*Recursive
*)fun_params : Tterm.vsymbol list;(*Arguments
*)fun_def : Tterm.term option;(*Definition
*)fun_spec : fun_spec option;(*Specification
*)fun_text : string;(*String containing the original specificaion as written by the user
*)fun_loc : Ppxlib.Location.t;(*Location
*)
}type extension_constructor = {ext_ident : Ident.t;ext_xs : Ttypes.xsymbol;ext_kind : Ppxlib.Parsetree.extension_constructor_kind;ext_loc : Ppxlib.Location.t;ext_attributes : Ppxlib.Parsetree.attributes;
}type type_exception = {exn_constructor : extension_constructor;exn_loc : Ppxlib.Location.t;exn_attributes : Ppxlib.Parsetree.attributes;
}type with_constraint = | Wty of Ident.t * type_declaration| Wmod of Ident.t * Ident.t| Wtysubs of Ident.t * type_declaration| Wmodsubs of Ident.t * Ident.t
type open_description = {opn_id : string list;opn_override : Ppxlib.Asttypes.override_flag;opn_loc : Ppxlib.Location.t;opn_attrs : Ppxlib.Parsetree.attributes;
}type signature = signature_item listand signature_item_desc = | Sig_val of val_description * ghost| Sig_type of rec_flag * type_declaration list * ghost| Sig_typext of Ppxlib.Parsetree.type_extension| Sig_module of module_declaration| Sig_recmodule of module_declaration list| Sig_modtype of module_type_declaration| Sig_exception of type_exception| Sig_open of open_description * ghost| Sig_include of Ppxlib.Parsetree.include_description| Sig_class of Ppxlib.Parsetree.class_description list| Sig_class_type of Ppxlib.Parsetree.class_type_declaration list| Sig_attribute of Ppxlib.Parsetree.attribute| Sig_extension of Ppxlib.Parsetree.extension * Ppxlib.Parsetree.attributes| Sig_use of string| Sig_function of function_| Sig_axiom of axiom
and module_declaration = {md_name : Ident.t;md_type : module_type;md_attrs : Ppxlib.Parsetree.attributes;md_loc : Ppxlib.Location.t;
}and module_type_declaration = {mtd_name : Ident.t;mtd_type : module_type option;mtd_attrs : Ppxlib.Parsetree.attributes;mtd_loc : Ppxlib.Location.t;
}and module_type = {mt_desc : module_type_desc;mt_loc : Ppxlib.Location.t;mt_attrs : Ppxlib.Parsetree.attributes;
}and module_type_desc = | Mod_ident of string list| Mod_signature of signature| Mod_functor of Ident.t * module_type option * module_type| Mod_with of module_type * with_constraint list| Mod_typeof of Ppxlib.Parsetree.module_expr| Mod_extension of Ppxlib.Parsetree.extension| Mod_alias of string list