package gospel

  1. Overview
  2. Docs
module Ident = Identifier.Ident
type vsymbol = {
  1. vs_name : Ident.t;
  2. vs_ty : Ttypes.ty;
}
val create_vsymbol : Gospel__Identifier.Preid.t -> Ttypes.ty -> vsymbol
module Vs : sig ... end
module Svs : sig ... end
type lsymbol = {
  1. ls_name : Ident.t;
  2. ls_args : Ttypes.ty list;
  3. ls_value : Ttypes.ty option;
  4. ls_constr : bool;
  5. ls_field : bool;
}
val ls_equal : lsymbol -> lsymbol -> bool
module LS : sig ... end
module Sls : sig ... end
module Mls : sig ... end
val lsymbol : ?constr:bool -> field:bool -> Ident.t -> Ttypes.ty list -> Ttypes.ty option -> lsymbol
val fsymbol : ?constr:bool -> field:bool -> Ident.t -> Ttypes.ty list -> Ttypes.ty -> lsymbol
val psymbol : Ident.t -> Ttypes.ty list -> lsymbol
val ls_subst_ts : Ttypes.tysymbol -> Ttypes.tysymbol -> lsymbol -> lsymbol

buil-in lsymbols

val ps_equ : lsymbol
val fs_unit : lsymbol
val fs_bool_true : lsymbol
val fs_bool_false : lsymbol
val fs_apply : lsymbol
val fs_tuple_ids : (Ident.t, lsymbol) Hashtbl.t
val fs_tuple : int -> lsymbol
val is_fs_tuple : lsymbol -> bool

terms

type pattern = {
  1. p_node : pattern_node;
  2. p_ty : Ttypes.ty;
  3. p_vars : Svs.t;
  4. p_loc : Ppxlib.Location.t;
}
and pattern_node =
  1. | Pwild
  2. | Pvar of vsymbol
  3. | Papp of lsymbol * pattern list
  4. | Por of pattern * pattern
  5. | Pas of pattern * vsymbol
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. t_node : term_node;
  2. t_ty : Ttypes.ty option;
  3. t_attrs : string list;
  4. t_loc : Ppxlib.Location.t;
}
and term_node =
  1. | Tvar of vsymbol
  2. | Tconst of Ppxlib.Parsetree.constant
  3. | Tapp of lsymbol * term list
  4. | Tfield of term * lsymbol
  5. | Tif of term * term * term
  6. | Tlet of vsymbol * term * term
  7. | Tcase of term * (pattern * term) list
  8. | Tquant of quant * vsymbol list * term
  9. | Tbinop of binop * term * term
  10. | Tnot of term
  11. | Told of term
  12. | Ttrue
  13. | Tfalse
val p_vars : pattern -> Svs.t
val t_free_vars : term -> Svs.t
exception FreeVariables of Svs.t
val t_free_vs_in_set : Svs.t -> term -> unit

type checking

exception TermExpected of term
exception FmlaExpected of term
val t_prop : term -> term
val t_type : term -> Ttypes.ty
val t_ty_check : term -> Ttypes.ty option -> unit
exception BadArity of lsymbol * int
exception PredicateSymbolExpected of lsymbol
exception FunctionSymbolExpected of lsymbol
val ls_arg_inst : lsymbol -> term list -> Ttypes.ty Ttypes.Mtv.t
val ls_app_inst : loc:Ppxlib.Location.t -> lsymbol -> term list -> Ttypes.ty option -> Ttypes.ty Ttypes.Mtv.t

Pattern constructors

exception PDuplicatedVar of vsymbol
exception EmptyCase
val p_app : lsymbol -> pattern list -> Ttypes.ty -> Ppxlib.Location.t -> pattern

Terms constructors

val mk_term : term_node -> Ttypes.ty option -> Ppxlib.Location.t -> term
val t_var : vsymbol -> Ppxlib.Location.t -> term
val t_app : lsymbol -> term list -> Ttypes.ty option -> Ppxlib.Location.t -> term
val t_field : term -> lsymbol -> Ttypes.ty option -> Ppxlib.Location.t -> term
val t_if : term -> term -> term -> Ppxlib.Location.t -> term
val t_let : vsymbol -> term -> term -> Ppxlib.Location.t -> term
val t_case : term -> (pattern * term) list -> Ppxlib.Location.t -> term
val t_binop : binop -> term -> term -> Ppxlib.Location.t -> term
val t_not : term -> Ppxlib.Location.t -> term
val t_old : term -> Ppxlib.Location.t -> term
val t_true : Ppxlib.Location.t -> term
val t_false : Ppxlib.Location.t -> term
val t_attr_set : string list -> term -> term
val t_bool_true : Ppxlib.Location.t -> term
val t_bool_false : Ppxlib.Location.t -> term
val t_equ : term -> term -> Ppxlib.Location.t -> term
val f_binop : binop -> term -> term -> Ppxlib.Location.t -> term
val f_not : term -> Ppxlib.Location.t -> term
val t_quant : quant -> vsymbol list -> term -> Ttypes.ty option -> Ppxlib.Location.t -> term
val f_forall : vsymbol list -> term -> Ttypes.ty option -> Ppxlib.Location.t -> term
val f_exists : vsymbol list -> term -> Ttypes.ty option -> Ppxlib.Location.t -> term
val t_lambda : vsymbol list -> term -> Ttypes.ty option -> Ppxlib.Location.t -> term
val f_and : term -> term -> Ppxlib.Location.t -> term
val f_and_asym : term -> term -> Ppxlib.Location.t -> term
val f_or : term -> term -> Ppxlib.Location.t -> term
val f_or_asym : term -> term -> Ppxlib.Location.t -> term
val f_implies : term -> term -> Ppxlib.Location.t -> term
val f_iff : term -> term -> Ppxlib.Location.t -> term

Pretty printing

val print_vs : Format.formatter -> vsymbol -> unit
val print_ls_decl : Format.formatter -> lsymbol -> unit
val print_ls_nm : Format.formatter -> lsymbol -> unit
val protect_on : bool -> ('a, 'b, 'c, 'd, 'e, 'f) format6 -> ('g, 'h, 'i, 'j, 'k, 'l) format6
val print_pat_node : int -> pattern Utils.Fmt.t
val print_pattern : pattern Utils.Fmt.t
val print_binop : Format.formatter -> binop -> unit
val print_quantifier : Format.formatter -> quant -> unit
val print_term : term Utils.Fmt.t

register exceptions