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 pattern = {
  1. pat_desc : pat_desc;
  2. pat_loc : Ppxlib.Location.t;
}
and pat_desc =
  1. | Pwild
  2. | Pvar of Preid.t
  3. | Ptrue
  4. | Pfalse
  5. | Papp of qualid * pattern list
  6. | Prec of (qualid * pattern) list
  7. | Ptuple of pattern list
  8. | Pas of pattern * Preid.t
  9. | Por of pattern * pattern
  10. | Pcast of pattern * pty
  11. | Pconst of Ppxlib.constant
  12. | Pinterval of char * char
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
type term = {
  1. term_desc : term_desc;
  2. term_loc : Ppxlib.Location.t;
}
and term_desc =
  1. | Ttrue
  2. | Tfalse
  3. | Tconst of Ppxlib.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. | Tlambda of pattern list * term * pty option
  14. | Tattr of string * term
  15. | Tlet of Preid.t * term * term
  16. | Tcase of term * (pattern * term option * term) list
  17. | Tcast of term * pty
  18. | Ttuple of term list
  19. | Trecord of (qualid * term) list
  20. | Tupdate of term * (qualid * term) list
  21. | Tscope of qualid * term
  22. | 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 : Preid.t option * 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.loc;
  2. vtype : Ppxlib.core_type;
  3. vprim : string list;
  4. vattributes : Ppxlib.attributes;
  5. vspec : val_spec option;
  6. vloc : Ppxlib.Location.t;
}
type s_type_declaration = {
  1. tname : string Ppxlib.loc;
  2. tparams : (Ppxlib.core_type * (Ppxlib.variance * Ppxlib.injectivity)) list;
  3. tcstrs : (Ppxlib.core_type * Ppxlib.core_type * Ppxlib.Location.t) list;
  4. tkind : Ppxlib.type_kind;
  5. tprivate : Ppxlib.private_flag;
  6. tmanifest : Ppxlib.core_type option;
  7. tattributes : Ppxlib.attributes;
  8. tspec : type_spec option;
  9. tloc : Ppxlib.Location.t;
}
type s_signature_item_desc =
  1. | Sig_val of s_val_description
  2. | Sig_type of Ppxlib.rec_flag * s_type_declaration list
  3. | Sig_typesubst of s_type_declaration list
  4. | Sig_typext of Ppxlib.type_extension
  5. | Sig_module of s_module_declaration
  6. | Sig_recmodule of s_module_declaration list
  7. | Sig_modtype of s_module_type_declaration
  8. | Sig_modtypesubst of s_module_type_declaration
  9. | Sig_modsubst of Ppxlib.module_substitution
  10. | Sig_exception of Ppxlib.type_exception
  11. | Sig_open of Ppxlib.open_description
  12. | Sig_include of Ppxlib.include_description
  13. | Sig_class of Ppxlib.class_description list
  14. | Sig_class_type of Ppxlib.class_type_declaration list
  15. | Sig_attribute of Ppxlib.attribute
  16. | Sig_extension of Ppxlib.extension * Ppxlib.attributes
  17. | Sig_function of function_
  18. | Sig_axiom of axiom
  19. | Sig_ghost_type of Ppxlib.rec_flag * s_type_declaration list
  20. | Sig_ghost_val of s_val_description
  21. | Sig_ghost_open of Ppxlib.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.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.module_expr
  6. | Mod_extension of Ppxlib.extension
  7. | Mod_alias of Ppxlib.Longident.t Ppxlib.loc
and s_functor_parameter =
  1. | Unit
  2. | Named of string option Ppxlib.loc * s_module_type
and s_module_type = {
  1. mdesc : s_module_type_desc;
  2. mloc : Ppxlib.Location.t;
  3. mattributes : Ppxlib.attributes;
}
and s_module_declaration = {
  1. mdname : string option Ppxlib.loc;
  2. mdtype : s_module_type;
  3. mdattributes : Ppxlib.attributes;
  4. mdloc : Ppxlib.Location.t;
}
and s_module_type_declaration = {
  1. mtdname : string Ppxlib.loc;
  2. mtdtype : s_module_type option;
  3. mtdattributes : Ppxlib.attributes;
  4. mtdloc : Ppxlib.Location.t;
}
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