gospel 0.1.0 · OCaml Package

module Ident = Identifier.Ident

type vsymbol = {

vs_name : Ident.t;
vs_ty : Ttypes.ty;

}

val create_vsymbol : Gospel__Identifier.Preid.t -> Ttypes.ty -> vsymbol

module Vs : sig ... end

module Svs : sig ... end

type lsymbol = {

ls_name : Ident.t;
ls_args : Ttypes.ty list;
ls_value : Ttypes.ty option;
ls_constr : bool;
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

val ls_subst_ty : 
  Ttypes.tysymbol ->
  Ttypes.tysymbol ->
  Ttypes.ty ->
  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 = {

p_node : pattern_node;
p_ty : Ttypes.ty;
p_vars : Svs.t;
p_loc : Ppxlib.Location.t;

}

and pattern_node =

| Pwild
| Pvar of vsymbol
| Papp of lsymbol * pattern list
| Por of pattern * pattern
| Pas of pattern * vsymbol

type binop =

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

type quant =

| Tforall
| Texists
| Tlambda

type term = {

t_node : term_node;
t_ty : Ttypes.ty option;
t_attrs : string list;
t_loc : Ppxlib.Location.t;

}

and term_node =

| Tvar of vsymbol
| Tconst of Ppxlib.Parsetree.constant
| Tapp of lsymbol * term list
| Tfield of term * lsymbol
| Tif of term * term * term
| Tlet of vsymbol * term * term
| Tcase of term * (pattern * term) list
| Tquant of quant * vsymbol list * term
| Tbinop of binop * term * term
| Tnot of term
| Told of term
| Ttrue
| 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

val mk_pattern : 
  pattern_node ->
  Ttypes.ty ->
  Svs.t ->
  Ppxlib.Location.t ->
  pattern

exception PDuplicatedVar of vsymbol

exception EmptyCase

val p_wild : Ttypes.ty -> Ppxlib.Location.t -> pattern

val p_var : Svs.elt -> Ppxlib.Location.t -> pattern

val p_app : 
  lsymbol ->
  pattern list ->
  Ttypes.ty ->
  Ppxlib.Location.t ->
  pattern

val p_or : pattern -> pattern -> Ppxlib.Location.t -> pattern

val p_as : pattern -> vsymbol -> 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_const : 
  Ppxlib.Parsetree.constant ->
  Ttypes.ty ->
  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 t_neq : term -> term -> Ppxlib.Location.t -> 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

package gospel