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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct