gospel 0.2.0 · OCaml Package

module Ident = Identifier.Ident

type lb_arg =

| Lunit
(*
()
*)
| Lnone of Symbols.vsymbol
(*
x
*)
| Loptional of Symbols.vsymbol
(*
?x
*)
| Lnamed of Symbols.vsymbol
(*
~x
*)
| 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 = {

sp_args : lb_arg list;
(*
Arguments
*)
sp_ret : lb_arg list;
(*
Return values. This is a list because of tuple destruction.
*)
sp_pre : Tterm.term list;
(*
Preconditions
*)
sp_checks : Tterm.term list;
(*
Checks preconditions
*)
sp_post : Tterm.term list;
(*
Postconditions
*)
sp_xpost : (Ttypes.xsymbol * (Tterm.pattern * Tterm.term) list) list;
(*
Exceptional postconditions.
*)
sp_wr : Tterm.term list;
(*
Writes
*)
sp_cs : Tterm.term list;
(*
Consumes
*)
sp_diverge : bool;
(*
Diverges
*)
sp_pure : bool;
(*
Pure
*)
sp_equiv : string list;
(*
Equivalent
*)
sp_text : string;
(*
String containing the original specificaion as written by the user
*)
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 = {

vd_name : Ident.t;
vd_type : Ppxlib.core_type;
vd_prim : string list;
(*
primitive declaration
*)
vd_attrs : Ppxlib.attributes;
vd_args : lb_arg list;
vd_ret : lb_arg list;
vd_spec : val_spec option;
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 = {

ty_ephemeral : bool;
(*
Ephemeral
*)
ty_fields : (Symbols.lsymbol * bool) list;
(*
Models (field symbol * mutable)
*)
ty_invariants : Symbols.vsymbol option * Tterm.term list;
(*
Invariants
*)
ty_text : string;
(*
String containing the original specificaion as written by the user
*)
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 =

| Immutable
| 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 = {

ld_field : 'a;
ld_mut : mutable_flag;
ld_loc : Ppxlib.Location.t;
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 = {

rd_cs : Symbols.lsymbol;
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 = {

cd_cs : Symbols.lsymbol;
cd_ld : (Ident.t * Ttypes.ty) label_declaration list;
cd_loc : Ppxlib.Location.t;
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 =

| Pty_abstract
| Pty_variant of constructor_decl list
(*
Invariant: non-empty list
*)
| 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 =

| Private
| 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 = {

td_ts : Ttypes.tysymbol;
td_params : (Ttypes.tvsymbol * (Ppxlib.variance * Ppxlib.injectivity)) list;
td_cstrs : (Ttypes.ty * Ttypes.ty * Ppxlib.Location.t) list;
td_kind : type_kind;
td_private : private_flag;
td_manifest : Ttypes.ty option;
td_attrs : Ppxlib.attributes;
td_spec : type_spec option;
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 = {

ax_name : Ident.t;
(*
Name
*)
ax_term : Tterm.term;
(*
Definition
*)
ax_loc : Ppxlib.Location.t;
(*
Location
*)
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

val show_axiom : axiom -> Ppx_deriving_runtime.string

type fun_spec = {

fun_req : Tterm.term list;
(*
Preconditions
*)
fun_ens : Tterm.term list;
(*
Postconditions
*)
fun_variant : Tterm.term list;
(*
Variant
*)
fun_coer : bool;
(*
Coercion
*)
fun_text : string;
(*
String containing the original specificaion as written by the user
*)
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_ = {

fun_ls : Symbols.lsymbol;
(*
Function symbol
*)
fun_rec : bool;
(*
Recursive
*)
fun_params : Symbols.vsymbol list;
(*
Arguments
*)
fun_def : Tterm.term option;
(*
Definition
*)
fun_spec : fun_spec option;
(*
Specification
*)
fun_text : string;
(*
String containing the original specificaion as written by the user
*)
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 = {

ext_ident : Ident.t;
ext_xs : Ttypes.xsymbol;
ext_kind : Ppxlib.extension_constructor_kind;
ext_loc : Ppxlib.Location.t;
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 = {

exn_constructor : extension_constructor;
exn_loc : Ppxlib.Location.t;
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 =

| Nonrecursive
| 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 =

| Nonghost
| Ghost

val pp_ghost : 
  Ppx_deriving_runtime.Format.formatter ->
  ghost ->
  Ppx_deriving_runtime.unit

val show_ghost : ghost -> Ppx_deriving_runtime.string

type with_constraint =

| Wty of Ident.t * type_declaration
| Wmod of Ident.t * Ident.t
| Wtysubs of Ident.t * type_declaration
| 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 = {

opn_id : string list;
opn_override : Ppxlib.Asttypes.override_flag;
opn_loc : Ppxlib.Location.t;
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 = {

sig_desc : signature_item_desc;
sig_loc : Ppxlib.Location.t;

}

and signature_item_desc =

| Sig_val of val_description * ghost
| Sig_type of rec_flag * type_declaration list * ghost
| Sig_typext of Ppxlib.type_extension
| Sig_module of module_declaration
| Sig_recmodule of module_declaration list
| Sig_modtype of module_type_declaration
| Sig_exception of type_exception
| Sig_open of open_description * ghost
| Sig_include of Ppxlib.include_description
| Sig_class of Ppxlib.class_description list
| Sig_class_type of Ppxlib.class_type_declaration list
| Sig_attribute of Ppxlib.attribute
| Sig_extension of Ppxlib.extension * Ppxlib.attributes
| Sig_use of string
| Sig_function of function_
| Sig_axiom of axiom

and module_declaration = {

md_name : Ident.t;
md_type : module_type;
md_attrs : Ppxlib.attributes;
md_loc : Ppxlib.Location.t;

}

and module_type_declaration = {

mtd_name : Ident.t;
mtd_type : module_type option;
mtd_attrs : Ppxlib.attributes;
mtd_loc : Ppxlib.Location.t;

}

and module_type = {

mt_desc : module_type_desc;
mt_loc : Ppxlib.Location.t;
mt_attrs : Ppxlib.attributes;

}

and module_type_desc =

| Mod_ident of string list
| Mod_signature of signature
| Mod_functor of Ident.t * module_type option * module_type
| Mod_with of module_type * with_constraint list
| Mod_typeof of Ppxlib.module_expr
| Mod_extension of Ppxlib.extension
| 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

package gospel