gospel 0.1.0 · OCaml Package

module Preid = Identifier.Preid

type qualid =

| Qpreid of Preid.t
| Qdot of qualid * Preid.t

type pty =

| PTtyvar of Preid.t
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTarrow of labelled_arg * pty * pty

and labelled_arg =

| Lunit
| Lnone of Preid.t
| Loptional of Preid.t
| Lnamed of Preid.t
| Lghost of Preid.t * pty

type ghost = bool

type pattern = {

pat_desc : pat_desc;
pat_loc : Ppxlib.Location.t;

}

and pat_desc =

| Pwild
| Pvar of Preid.t
| Papp of qualid * pattern list
| Prec of (qualid * pattern) list
| Ptuple of pattern list
| Pas of pattern * Preid.t
| Por of pattern * pattern
| Pcast of pattern * pty

type binder = Preid.t * pty option

type param = Ppxlib.Location.t * Preid.t * pty

type binop =

| Tand
| Tand_asym
| Tor
| Tor_asym
| Timplies
| Tiff

type quant =

| Tforall
| Texists
| Tlambda

type term = {

term_desc : term_desc;
term_loc : Ppxlib.Location.t;

}

and term_desc =

| Ttrue
| Tfalse
| Tconst of Ppxlib.Parsetree.constant
| Tpreid of qualid
| Tidapp of qualid * term list
| Tfield of term * qualid
| Tapply of term * term
| Tinfix of term * Preid.t * term
| Tbinop of term * binop * term
| Tnot of term
| Tif of term * term * term
| Tquant of quant * binder list * term
| Tattr of string * term
| Tlet of Preid.t * term * term
| Tcase of term * (pattern * term) list
| Tcast of term * pty
| Ttuple of term list
| Trecord of (qualid * term) list
| Tupdate of term * (qualid * term) list
| Tscope of qualid * term
| Told of term

type xpost = Ppxlib.Location.t * (qualid * (pattern * term) option) list

type spec_header = {

sp_hd_nm : Preid.t;
sp_hd_ret : labelled_arg list;
sp_hd_args : labelled_arg list;

}

type val_spec = {

sp_header : spec_header option;
sp_pre : term list;
sp_checks : term list;
sp_post : term list;
sp_xpost : xpost list;
sp_writes : term list;
sp_consumes : term list;
sp_diverge : bool;
sp_pure : bool;
sp_equiv : string list;
sp_text : string;
sp_loc : Ppxlib.Location.t;

}

type field = {

f_loc : Ppxlib.Location.t;
f_preid : Preid.t;
f_pty : pty;
f_mutable : bool;

}

type type_spec = {

ty_ephemeral : bool;
ty_field : field list;
ty_invariant : term list;
ty_text : string;
ty_loc : Ppxlib.Location.t;

}

type fun_spec = {

fun_req : term list;
fun_ens : term list;
fun_variant : term list;
fun_coer : bool;
fun_text : string;
fun_loc : Ppxlib.Location.t;

}

type function_ = {

fun_name : Preid.t;
fun_rec : bool;
fun_type : pty option;
fun_params : param list;
fun_def : term option;
fun_spec : fun_spec option;
fun_loc : Ppxlib.Location.t;
fun_text : string;

}

type axiom = {

ax_name : Preid.t;
ax_term : term;
ax_loc : Ppxlib.Location.t;
ax_text : string;

}

type s_val_description = {

vname : string Ppxlib.Asttypes.loc;
vtype : Ppxlib.Parsetree.core_type;
vprim : string list;
vattributes : Ppxlib.Parsetree.attributes;
vspec : val_spec option;
vloc : Ppxlib.Location.t;

}

type s_type_declaration = {

tname : string Ppxlib.Asttypes.loc;
tparams : (Ppxlib.Parsetree.core_type * (Ppxlib.Asttypes.variance * Ppxlib.Asttypes.injectivity)) list;
tcstrs : (Ppxlib.Parsetree.core_type * Ppxlib.Parsetree.core_type * Ppxlib.Location.t) list;
tkind : Ppxlib.Parsetree.type_kind;
tprivate : Ppxlib.Asttypes.private_flag;
tmanifest : Ppxlib.Parsetree.core_type option;
tattributes : Ppxlib.Parsetree.attributes;
tspec : type_spec option;
tloc : Ppxlib.Location.t;

}

type s_with_constraint =

| Wtype of Ppxlib.Longident.t Ppxlib.Asttypes.loc * s_type_declaration
| Wmodule of Ppxlib.Longident.t Ppxlib.Asttypes.loc * Ppxlib.Longident.t Ppxlib.Asttypes.loc
| Wtypesubst of Ppxlib.Longident.t Ppxlib.Asttypes.loc * s_type_declaration
| Wmodsubst of Ppxlib.Longident.t Ppxlib.Asttypes.loc * Ppxlib.Longident.t Ppxlib.Asttypes.loc

type s_signature_item_desc =

| Sig_val of s_val_description
| Sig_type of Ppxlib.Asttypes.rec_flag * s_type_declaration list
| Sig_typext of Ppxlib.Parsetree.type_extension
| Sig_module of s_module_declaration
| Sig_recmodule of s_module_declaration list
| Sig_modtype of s_module_type_declaration
| Sig_exception of Ppxlib.Parsetree.type_exception
| Sig_open of Ppxlib.Parsetree.open_description
| Sig_include of Ppxlib.Parsetree.include_description
| Sig_class of Ppxlib.Parsetree.class_description list
| Sig_class_type of Ppxlib.Parsetree.class_type_declaration list
| Sig_attribute of Ppxlib.Parsetree.attribute
| Sig_extension of Ppxlib.Parsetree.extension * Ppxlib.Parsetree.attributes
| Sig_function of function_
| Sig_axiom of axiom
| Sig_ghost_type of Ppxlib.Asttypes.rec_flag * s_type_declaration list
| Sig_ghost_val of s_val_description
| Sig_ghost_open of Ppxlib.Parsetree.open_description

and s_signature_item = {

sdesc : s_signature_item_desc;
sloc : Ppxlib.Location.t;

}

and s_signature = s_signature_item list

and s_module_type_desc =

| Mod_ident of Ppxlib.Longident.t Ppxlib.Asttypes.loc
| Mod_signature of s_signature
| Mod_functor of s_functor_parameter * s_module_type
| Mod_with of s_module_type * s_with_constraint list
| Mod_typeof of Ppxlib.Parsetree.module_expr
| Mod_extension of Ppxlib.Parsetree.extension
| Mod_alias of Ppxlib.Longident.t Ppxlib.Asttypes.loc

and s_functor_parameter =

| Unit
| Named of string option Ppxlib.Asttypes.loc * s_module_type

and s_module_type = {

mdesc : s_module_type_desc;
mloc : Ppxlib.Location.t;
mattributes : Ppxlib.Parsetree.attributes;

}

and s_module_declaration = {

mdname : string option Ppxlib.Asttypes.loc;
mdtype : s_module_type;
mdattributes : Ppxlib.Parsetree.attributes;
mdloc : Ppxlib.Location.t;

}

and s_module_type_declaration = {

mtdname : string Ppxlib.Asttypes.loc;
mtdtype : s_module_type option;
mtdattributes : Ppxlib.Parsetree.attributes;
mtdloc : Ppxlib.Location.t;

}

package gospel