package gospel

  1. Overview
  2. Docs
module Preid = Identifier.Preid
type qualid =
  1. | Qpreid of Preid.t
  2. | Qdot of qualid * Preid.t
type pty =
  1. | PTtyvar of Preid.t
  2. | PTtyapp of qualid * pty list
  3. | PTtuple of pty list
  4. | PTarrow of labelled_arg * pty * pty
and labelled_arg =
  1. | Lunit
  2. | Lnone of Preid.t
  3. | Loptional of Preid.t
  4. | Lnamed of Preid.t
  5. | Lghost of Preid.t * pty
type ghost = bool
type pattern = {
  1. pat_desc : pat_desc;
  2. pat_loc : Ppxlib.Location.t;
}
and pat_desc =
  1. | Pwild
  2. | Pvar of Preid.t
  3. | Papp of qualid * pattern list
  4. | Prec of (qualid * pattern) list
  5. | Ptuple of pattern list
  6. | Pas of pattern * Preid.t
  7. | Por of pattern * pattern
  8. | Pcast of pattern * pty
type binder = Preid.t * pty option
type param = Ppxlib.Location.t * Preid.t * pty
type binop =
  1. | Tand
  2. | Tand_asym
  3. | Tor
  4. | Tor_asym
  5. | Timplies
  6. | Tiff
type quant =
  1. | Tforall
  2. | Texists
  3. | Tlambda
type term = {
  1. term_desc : term_desc;
  2. term_loc : Ppxlib.Location.t;
}
and term_desc =
  1. | Ttrue
  2. | Tfalse
  3. | Tconst of Ppxlib.Parsetree.constant
  4. | Tpreid of qualid
  5. | Tidapp of qualid * term list
  6. | Tfield of term * qualid
  7. | Tapply of term * term
  8. | Tinfix of term * Preid.t * term
  9. | Tbinop of term * binop * term
  10. | Tnot of term
  11. | Tif of term * term * term
  12. | Tquant of quant * binder list * term
  13. | Tattr of string * term
  14. | Tlet of Preid.t * term * term
  15. | Tcase of term * (pattern * term) list
  16. | Tcast of term * pty
  17. | Ttuple of term list
  18. | Trecord of (qualid * term) list
  19. | Tupdate of term * (qualid * term) list
  20. | Tscope of qualid * term
  21. | Told of term
type xpost = Ppxlib.Location.t * (qualid * (pattern * term) option) list
type spec_header = {
  1. sp_hd_nm : Preid.t;
  2. sp_hd_ret : labelled_arg list;
  3. sp_hd_args : labelled_arg list;
}
type val_spec = {
  1. sp_header : spec_header option;
  2. sp_pre : term list;
  3. sp_checks : term list;
  4. sp_post : term list;
  5. sp_xpost : xpost list;
  6. sp_writes : term list;
  7. sp_consumes : term list;
  8. sp_diverge : bool;
  9. sp_pure : bool;
  10. sp_equiv : string list;
  11. sp_text : string;
  12. sp_loc : Ppxlib.Location.t;
}
type field = {
  1. f_loc : Ppxlib.Location.t;
  2. f_preid : Preid.t;
  3. f_pty : pty;
  4. f_mutable : bool;
}
type type_spec = {
  1. ty_ephemeral : bool;
  2. ty_field : field list;
  3. ty_invariant : term list;
  4. ty_text : string;
  5. ty_loc : Ppxlib.Location.t;
}
type fun_spec = {
  1. fun_req : term list;
  2. fun_ens : term list;
  3. fun_variant : term list;
  4. fun_coer : bool;
  5. fun_text : string;
  6. fun_loc : Ppxlib.Location.t;
}
type function_ = {
  1. fun_name : Preid.t;
  2. fun_rec : bool;
  3. fun_type : pty option;
  4. fun_params : param list;
  5. fun_def : term option;
  6. fun_spec : fun_spec option;
  7. fun_loc : Ppxlib.Location.t;
  8. fun_text : string;
}
type axiom = {
  1. ax_name : Preid.t;
  2. ax_term : term;
  3. ax_loc : Ppxlib.Location.t;
  4. ax_text : string;
}
type s_val_description = {
  1. vname : string Ppxlib.Asttypes.loc;
  2. vtype : Ppxlib.Parsetree.core_type;
  3. vprim : string list;
  4. vattributes : Ppxlib.Parsetree.attributes;
  5. vspec : val_spec option;
  6. vloc : Ppxlib.Location.t;
}
type s_signature_item_desc =
  1. | Sig_val of s_val_description
  2. | Sig_type of Ppxlib.Asttypes.rec_flag * s_type_declaration list
  3. | Sig_typext of Ppxlib.Parsetree.type_extension
  4. | Sig_module of s_module_declaration
  5. | Sig_recmodule of s_module_declaration list
  6. | Sig_modtype of s_module_type_declaration
  7. | Sig_exception of Ppxlib.Parsetree.type_exception
  8. | Sig_open of Ppxlib.Parsetree.open_description
  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_function of function_
  15. | Sig_axiom of axiom
  16. | Sig_ghost_type of Ppxlib.Asttypes.rec_flag * s_type_declaration list
  17. | Sig_ghost_val of s_val_description
  18. | Sig_ghost_open of Ppxlib.Parsetree.open_description
and s_signature_item = {
  1. sdesc : s_signature_item_desc;
  2. sloc : Ppxlib.Location.t;
}
and s_signature = s_signature_item list
and s_module_type_desc =
  1. | Mod_ident of Ppxlib.Longident.t Ppxlib.Asttypes.loc
  2. | Mod_signature of s_signature
  3. | Mod_functor of s_functor_parameter * s_module_type
  4. | Mod_with of s_module_type * s_with_constraint list
  5. | Mod_typeof of Ppxlib.Parsetree.module_expr
  6. | Mod_extension of Ppxlib.Parsetree.extension
  7. | Mod_alias of Ppxlib.Longident.t Ppxlib.Asttypes.loc
and s_functor_parameter =
  1. | Unit
  2. | Named of string option Ppxlib.Asttypes.loc * s_module_type
and s_module_type = {
  1. mdesc : s_module_type_desc;
  2. mloc : Ppxlib.Location.t;
  3. mattributes : Ppxlib.Parsetree.attributes;
}
and s_module_declaration = {
  1. mdname : string option Ppxlib.Asttypes.loc;
  2. mdtype : s_module_type;
  3. mdattributes : Ppxlib.Parsetree.attributes;
  4. mdloc : Ppxlib.Location.t;
}
and s_module_type_declaration = {
  1. mtdname : string Ppxlib.Asttypes.loc;
  2. mtdtype : s_module_type option;
  3. mtdattributes : Ppxlib.Parsetree.attributes;
  4. mtdloc : Ppxlib.Location.t;
}