package gospel

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

    ()

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

    x

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

    ?x

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

    ~x

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

    [x: t]

    *)
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

    *)
}
type val_description = {
  1. vd_name : Ident.t;
  2. vd_type : Ppxlib.Parsetree.core_type;
  3. vd_prim : string list;
    (*

    primitive declaration

    *)
  4. vd_attrs : Ppxlib.Parsetree.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;
}
type type_spec = {
  1. ty_ephemeral : bool;
    (*

    Ephemeral

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

    Models (field symbol * mutable)

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

    Invariants

    *)
  4. ty_text : string;
    (*

    String containing the original specificaion as written by the user

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

    Specification location

    *)
}
type mutable_flag =
  1. | Immutable
  2. | Mutable
type 'a label_declaration = {
  1. ld_field : 'a;
  2. ld_mut : mutable_flag;
  3. ld_loc : Ppxlib.Location.t;
  4. ld_attrs : Ppxlib.Parsetree.attributes;
}
type rec_declaration = {
  1. rd_cs : Tterm.lsymbol;
  2. rd_ldl : Tterm.lsymbol label_declaration list;
}
type constructor_decl = {
  1. cd_cs : Tterm.lsymbol;
  2. cd_ld : (Ident.t * Ttypes.ty) label_declaration list;
  3. cd_loc : Ppxlib.Location.t;
  4. cd_attrs : Ppxlib.Parsetree.attributes;
}
type type_kind =
  1. | Pty_abstract
  2. | Pty_variant of constructor_decl list
  3. | Pty_record of rec_declaration
  4. | Pty_open
type private_flag =
  1. | Private
  2. | Public
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.Parsetree.attributes;
  8. td_spec : type_spec option;
  9. td_loc : Ppxlib.Location.t;
}
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

    *)
}
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

    *)
}
type function_ = {
  1. fun_ls : Tterm.lsymbol;
    (*

    Function symbol

    *)
  2. fun_rec : bool;
    (*

    Recursive

    *)
  3. fun_params : Tterm.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

    *)
}
type extension_constructor = {
  1. ext_ident : Ident.t;
  2. ext_xs : Ttypes.xsymbol;
  3. ext_kind : Ppxlib.Parsetree.extension_constructor_kind;
  4. ext_loc : Ppxlib.Location.t;
  5. ext_attributes : Ppxlib.Parsetree.attributes;
}
type type_exception = {
  1. exn_constructor : extension_constructor;
  2. exn_loc : Ppxlib.Location.t;
  3. exn_attributes : Ppxlib.Parsetree.attributes;
}
type rec_flag =
  1. | Nonrecursive
  2. | Recursive
type ghost = bool
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
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.Parsetree.attributes;
}
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.Parsetree.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.Parsetree.include_description
  10. | Sig_class of Ppxlib.Parsetree.class_description list
  11. | Sig_class_type of Ppxlib.Parsetree.class_type_declaration list
  12. | Sig_attribute of Ppxlib.Parsetree.attribute
  13. | Sig_extension of Ppxlib.Parsetree.extension * Ppxlib.Parsetree.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.Parsetree.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.Parsetree.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.Parsetree.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.Parsetree.module_expr
  6. | Mod_extension of Ppxlib.Parsetree.extension
  7. | Mod_alias of string list