package gospel

  1. Overview
  2. Docs
module Ident = Identifier.Ident
type lb_arg =
  1. | Lunit
    (*

    ()

    *)
  2. | Lnone of Symbols.vsymbol
    (*

    x

    *)
  3. | Loptional of Symbols.vsymbol
    (*

    ?x

    *)
  4. | Lnamed of Symbols.vsymbol
    (*

    ~x

    *)
  5. | Lghost of Symbols.vsymbol
    (*

    [x: t]

    *)
val pp_lb_arg : Ppx_deriving_runtime.Format.formatter -> lb_arg -> Ppx_deriving_runtime.unit
val show_lb_arg : lb_arg -> Ppx_deriving_runtime.string
type val_spec = {
  1. sp_args : lb_arg list;
    (*

    Arguments

    *)
  2. sp_ret : lb_arg list;
    (*

    Return values. This is a list because of tuple destruction.

    *)
  3. sp_pre : Tterm.term list;
    (*

    Preconditions

    *)
  4. sp_checks : Tterm.term list;
    (*

    Checks preconditions

    *)
  5. sp_post : Tterm.term list;
    (*

    Postconditions

    *)
  6. sp_xpost : (Ttypes.xsymbol * (Tterm.pattern * Tterm.term) list) list;
    (*

    Exceptional postconditions.

    *)
  7. sp_wr : Tterm.term list;
    (*

    Writes

    *)
  8. sp_cs : Tterm.term list;
    (*

    Consumes

    *)
  9. sp_diverge : bool;
    (*

    Diverges

    *)
  10. sp_pure : bool;
    (*

    Pure

    *)
  11. sp_equiv : string list;
    (*

    Equivalent

    *)
  12. sp_text : string;
    (*

    String containing the original specificaion as written by the user

    *)
  13. sp_loc : Ppxlib.Location.t;
    (*

    Specification location

    *)
}
val pp_val_spec : Ppx_deriving_runtime.Format.formatter -> val_spec -> Ppx_deriving_runtime.unit
val show_val_spec : val_spec -> Ppx_deriving_runtime.string
type val_description = {
  1. vd_name : Ident.t;
  2. vd_type : Ppxlib.core_type;
  3. vd_prim : string list;
    (*

    primitive declaration

    *)
  4. vd_attrs : Ppxlib.attributes;
  5. vd_args : lb_arg list;
  6. vd_ret : lb_arg list;
  7. vd_spec : val_spec option;
  8. vd_loc : Ppxlib.Location.t;
}
val pp_val_description : Ppx_deriving_runtime.Format.formatter -> val_description -> Ppx_deriving_runtime.unit
val show_val_description : val_description -> Ppx_deriving_runtime.string
type type_spec = {
  1. ty_ephemeral : bool;
    (*

    Ephemeral

    *)
  2. ty_fields : (Symbols.lsymbol * bool) list;
    (*

    Models (field symbol * mutable)

    *)
  3. ty_invariants : (Symbols.vsymbol * Tterm.term list) option;
    (*

    Invariants

    *)
  4. ty_text : string;
    (*

    String containing the original specificaion as written by the user

    *)
  5. ty_loc : Ppxlib.Location.t;
    (*

    Specification location

    *)
}
val pp_type_spec : Ppx_deriving_runtime.Format.formatter -> type_spec -> Ppx_deriving_runtime.unit
val show_type_spec : type_spec -> Ppx_deriving_runtime.string
type mutable_flag =
  1. | Immutable
  2. | Mutable
val pp_mutable_flag : Ppx_deriving_runtime.Format.formatter -> mutable_flag -> Ppx_deriving_runtime.unit
val show_mutable_flag : mutable_flag -> Ppx_deriving_runtime.string
type 'a label_declaration = {
  1. ld_field : 'a;
  2. ld_mut : mutable_flag;
  3. ld_loc : Ppxlib.Location.t;
  4. ld_attrs : Ppxlib.attributes;
}
val pp_label_declaration : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'a label_declaration -> Ppx_deriving_runtime.unit
val show_label_declaration : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> 'a label_declaration -> Ppx_deriving_runtime.string
type rec_declaration = {
  1. rd_cs : Symbols.lsymbol;
  2. rd_ldl : Symbols.lsymbol label_declaration list;
}
val pp_rec_declaration : Ppx_deriving_runtime.Format.formatter -> rec_declaration -> Ppx_deriving_runtime.unit
val show_rec_declaration : rec_declaration -> Ppx_deriving_runtime.string
type constructor_decl = {
  1. cd_cs : Symbols.lsymbol;
  2. cd_ld : (Ident.t * Ttypes.ty) label_declaration list;
  3. cd_loc : Ppxlib.Location.t;
  4. cd_attrs : Ppxlib.attributes;
}
val pp_constructor_decl : Ppx_deriving_runtime.Format.formatter -> constructor_decl -> Ppx_deriving_runtime.unit
val show_constructor_decl : constructor_decl -> Ppx_deriving_runtime.string
type type_kind =
  1. | Pty_abstract
  2. | Pty_variant of constructor_decl list
    (*

    Invariant: non-empty list

    *)
  3. | Pty_record of rec_declaration
val pp_type_kind : Ppx_deriving_runtime.Format.formatter -> type_kind -> Ppx_deriving_runtime.unit
val show_type_kind : type_kind -> Ppx_deriving_runtime.string
type private_flag =
  1. | Private
  2. | Public
val pp_private_flag : Ppx_deriving_runtime.Format.formatter -> private_flag -> Ppx_deriving_runtime.unit
val show_private_flag : private_flag -> Ppx_deriving_runtime.string
type type_declaration = {
  1. td_ts : Ttypes.tysymbol;
  2. td_params : (Ttypes.tvsymbol * (Ppxlib.variance * Ppxlib.injectivity)) list;
  3. td_cstrs : (Ttypes.ty * Ttypes.ty * Ppxlib.Location.t) list;
  4. td_kind : type_kind;
  5. td_private : private_flag;
  6. td_manifest : Ttypes.ty option;
  7. td_attrs : Ppxlib.attributes;
  8. td_spec : type_spec option;
  9. td_loc : Ppxlib.Location.t;
}
val pp_type_declaration : Ppx_deriving_runtime.Format.formatter -> type_declaration -> Ppx_deriving_runtime.unit
val show_type_declaration : type_declaration -> Ppx_deriving_runtime.string
type axiom = {
  1. ax_name : Ident.t;
    (*

    Name

    *)
  2. ax_term : Tterm.term;
    (*

    Definition

    *)
  3. ax_loc : Ppxlib.Location.t;
    (*

    Location

    *)
  4. ax_text : string;
    (*

    String containing the original specificaion as written by the user

    *)
}
val pp_axiom : Ppx_deriving_runtime.Format.formatter -> axiom -> Ppx_deriving_runtime.unit
type fun_spec = {
  1. fun_req : Tterm.term list;
    (*

    Preconditions

    *)
  2. fun_ens : Tterm.term list;
    (*

    Postconditions

    *)
  3. fun_variant : Tterm.term list;
    (*

    Variant

    *)
  4. fun_coer : bool;
    (*

    Coercion

    *)
  5. fun_text : string;
    (*

    String containing the original specificaion as written by the user

    *)
  6. fun_loc : Ppxlib.Location.t;
    (*

    Specification location

    *)
}
val pp_fun_spec : Ppx_deriving_runtime.Format.formatter -> fun_spec -> Ppx_deriving_runtime.unit
val show_fun_spec : fun_spec -> Ppx_deriving_runtime.string
type function_ = {
  1. fun_ls : Symbols.lsymbol;
    (*

    Function symbol

    *)
  2. fun_rec : bool;
    (*

    Recursive

    *)
  3. fun_params : Symbols.vsymbol list;
    (*

    Arguments

    *)
  4. fun_def : Tterm.term option;
    (*

    Definition

    *)
  5. fun_spec : fun_spec option;
    (*

    Specification

    *)
  6. fun_text : string;
    (*

    String containing the original specificaion as written by the user

    *)
  7. fun_loc : Ppxlib.Location.t;
    (*

    Location

    *)
}
val pp_function_ : Ppx_deriving_runtime.Format.formatter -> function_ -> Ppx_deriving_runtime.unit
val show_function_ : function_ -> Ppx_deriving_runtime.string
type extension_constructor = {
  1. ext_ident : Ident.t;
  2. ext_xs : Ttypes.xsymbol;
  3. ext_kind : Ppxlib.extension_constructor_kind;
  4. ext_loc : Ppxlib.Location.t;
  5. ext_attributes : Ppxlib.attributes;
}
val pp_extension_constructor : Ppx_deriving_runtime.Format.formatter -> extension_constructor -> Ppx_deriving_runtime.unit
val show_extension_constructor : extension_constructor -> Ppx_deriving_runtime.string
type type_exception = {
  1. exn_constructor : extension_constructor;
  2. exn_loc : Ppxlib.Location.t;
  3. exn_attributes : Ppxlib.attributes;
}
val pp_type_exception : Ppx_deriving_runtime.Format.formatter -> type_exception -> Ppx_deriving_runtime.unit
val show_type_exception : type_exception -> Ppx_deriving_runtime.string
type rec_flag =
  1. | Nonrecursive
  2. | Recursive
val pp_rec_flag : Ppx_deriving_runtime.Format.formatter -> rec_flag -> Ppx_deriving_runtime.unit
val show_rec_flag : rec_flag -> Ppx_deriving_runtime.string
type ghost =
  1. | Nonghost
  2. | Ghost
val pp_ghost : Ppx_deriving_runtime.Format.formatter -> ghost -> Ppx_deriving_runtime.unit
type with_constraint =
  1. | Wty of Ident.t * type_declaration
  2. | Wmod of Ident.t * Ident.t
  3. | Wtysubs of Ident.t * type_declaration
  4. | Wmodsubs of Ident.t * Ident.t
val pp_with_constraint : Ppx_deriving_runtime.Format.formatter -> with_constraint -> Ppx_deriving_runtime.unit
val show_with_constraint : with_constraint -> Ppx_deriving_runtime.string
type open_description = {
  1. opn_id : string list;
  2. opn_override : Ppxlib.Asttypes.override_flag;
  3. opn_loc : Ppxlib.Location.t;
  4. opn_attrs : Ppxlib.attributes;
}
val pp_open_description : Ppx_deriving_runtime.Format.formatter -> open_description -> Ppx_deriving_runtime.unit
val show_open_description : open_description -> Ppx_deriving_runtime.string
type signature = signature_item list
and signature_item = {
  1. sig_desc : signature_item_desc;
  2. sig_loc : Ppxlib.Location.t;
}
and signature_item_desc =
  1. | Sig_val of val_description * ghost
  2. | Sig_type of rec_flag * type_declaration list * ghost
  3. | Sig_typext of Ppxlib.type_extension
  4. | Sig_module of module_declaration
  5. | Sig_recmodule of module_declaration list
  6. | Sig_modtype of module_type_declaration
  7. | Sig_exception of type_exception
  8. | Sig_open of open_description * ghost
  9. | Sig_include of Ppxlib.include_description
  10. | Sig_class of Ppxlib.class_description list
  11. | Sig_class_type of Ppxlib.class_type_declaration list
  12. | Sig_attribute of Ppxlib.attribute
  13. | Sig_extension of Ppxlib.extension * Ppxlib.attributes
  14. | Sig_use of string
  15. | Sig_function of function_
  16. | Sig_axiom of axiom
and module_declaration = {
  1. md_name : Ident.t;
  2. md_type : module_type;
  3. md_attrs : Ppxlib.attributes;
  4. md_loc : Ppxlib.Location.t;
}
and module_type_declaration = {
  1. mtd_name : Ident.t;
  2. mtd_type : module_type option;
  3. mtd_attrs : Ppxlib.attributes;
  4. mtd_loc : Ppxlib.Location.t;
}
and module_type = {
  1. mt_desc : module_type_desc;
  2. mt_loc : Ppxlib.Location.t;
  3. mt_attrs : Ppxlib.attributes;
}
and module_type_desc =
  1. | Mod_ident of string list
  2. | Mod_signature of signature
  3. | Mod_functor of Ident.t * module_type option * module_type
  4. | Mod_with of module_type * with_constraint list
  5. | Mod_typeof of Ppxlib.module_expr
  6. | Mod_extension of Ppxlib.extension
  7. | Mod_alias of string list
val pp_signature : Ppx_deriving_runtime.Format.formatter -> signature -> Ppx_deriving_runtime.unit
val show_signature : signature -> Ppx_deriving_runtime.string
val pp_signature_item : Ppx_deriving_runtime.Format.formatter -> signature_item -> Ppx_deriving_runtime.unit
val show_signature_item : signature_item -> Ppx_deriving_runtime.string
val pp_signature_item_desc : Ppx_deriving_runtime.Format.formatter -> signature_item_desc -> Ppx_deriving_runtime.unit
val show_signature_item_desc : signature_item_desc -> Ppx_deriving_runtime.string
val pp_module_declaration : Ppx_deriving_runtime.Format.formatter -> module_declaration -> Ppx_deriving_runtime.unit
val show_module_declaration : module_declaration -> Ppx_deriving_runtime.string
val pp_module_type_declaration : Ppx_deriving_runtime.Format.formatter -> module_type_declaration -> Ppx_deriving_runtime.unit
val show_module_type_declaration : module_type_declaration -> Ppx_deriving_runtime.string
val pp_module_type : Ppx_deriving_runtime.Format.formatter -> module_type -> Ppx_deriving_runtime.unit
val show_module_type : module_type -> Ppx_deriving_runtime.string
val pp_module_type_desc : Ppx_deriving_runtime.Format.formatter -> module_type_desc -> Ppx_deriving_runtime.unit
val show_module_type_desc : module_type_desc -> Ppx_deriving_runtime.string
OCaml

Innovation. Community. Security.