Module `Gospel.Tterm`Source

Sourcemodule Ident = Identifier.Ident

Sourcetype vsymbol = {

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

}

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

Sourcemodule Vs : sig ... end

Sourcemodule Svs : sig ... end

Sourcetype lsymbol = {

ls_name : Ident.t;
ls_args : Ttypes.ty list;
ls_value : Ttypes.ty option;
ls_constr : bool;
ls_field : bool;

}

Sourceval ls_equal : lsymbol -> lsymbol -> bool

Sourcemodule LS : sig ... end

Sourcemodule Sls : sig ... end

Sourcemodule Mls : sig ... end

Source

val lsymbol : 
  ?constr:bool ->
  field:bool ->
  Ident.t ->
  Ttypes.ty list ->
  Ttypes.ty option ->
  lsymbol

Source

val fsymbol : 
  ?constr:bool ->
  field:bool ->
  Ident.t ->
  Ttypes.ty list ->
  Ttypes.ty ->
  lsymbol

Sourceval psymbol : Ident.t -> Ttypes.ty list -> lsymbol

Sourceval ls_subst_ts : Ttypes.tysymbol -> Ttypes.tysymbol -> lsymbol -> lsymbol

Source

val ls_subst_ty : 
  Ttypes.tysymbol ->
  Ttypes.tysymbol ->
  Ttypes.ty ->
  lsymbol ->
  lsymbol

buil-in lsymbols

Sourceval ps_equ : lsymbol

Sourceval fs_unit : lsymbol

Sourceval fs_bool_true : lsymbol

Sourceval fs_bool_false : lsymbol

Sourceval fs_apply : lsymbol

Sourceval fs_tuple_ids : (Ident.t, lsymbol) Hashtbl.t

Sourceval fs_tuple : int -> lsymbol

Sourceval is_fs_tuple : lsymbol -> bool

terms

Sourcetype pattern = {

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

}

Sourceand pattern_node =

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

Sourcetype binop =

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

Sourcetype quant =

| Tforall
| Texists
| Tlambda

Sourcetype term = {

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

}

Sourceand 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

Sourceval p_vars : pattern -> Svs.t

Sourceval t_free_vars : term -> Svs.t

Sourceexception FreeVariables of Svs.t

Sourceval t_free_vs_in_set : Svs.t -> term -> unit

type checking

Sourceexception TermExpected of term

Sourceexception FmlaExpected of term

Sourceval t_prop : term -> term

Sourceval t_type : term -> Ttypes.ty

Sourceval t_ty_check : term -> Ttypes.ty option -> unit

Sourceexception BadArity of lsymbol * int

Sourceexception PredicateSymbolExpected of lsymbol

Sourceexception FunctionSymbolExpected of lsymbol

Sourceval ls_arg_inst : lsymbol -> term list -> Ttypes.ty Ttypes.Mtv.t

Source

val ls_app_inst : 
  loc:Ppxlib.Location.t ->
  lsymbol ->
  term list ->
  Ttypes.ty option ->
  Ttypes.ty Ttypes.Mtv.t

Pattern constructors

Source

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

Sourceexception PDuplicatedVar of vsymbol

Sourceexception EmptyCase

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

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

Source

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

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

Sourceval p_as : pattern -> vsymbol -> Ppxlib.Location.t -> pattern

Terms constructors

Sourceval mk_term : term_node -> Ttypes.ty option -> Ppxlib.Location.t -> term

Sourceval t_var : vsymbol -> Ppxlib.Location.t -> term

Source

val t_const : 
  Ppxlib.Parsetree.constant ->
  Ttypes.ty ->
  Ppxlib.Location.t ->
  term

Source

val t_app : 
  lsymbol ->
  term list ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  term

Sourceval t_field : term -> lsymbol -> Ttypes.ty option -> Ppxlib.Location.t -> term

Sourceval t_if : term -> term -> term -> Ppxlib.Location.t -> term

Sourceval t_let : vsymbol -> term -> term -> Ppxlib.Location.t -> term

Sourceval t_case : term -> (pattern * term) list -> Ppxlib.Location.t -> term

Sourceval t_binop : binop -> term -> term -> Ppxlib.Location.t -> term

Sourceval t_not : term -> Ppxlib.Location.t -> term

Sourceval t_old : term -> Ppxlib.Location.t -> term

Sourceval t_true : Ppxlib.Location.t -> term

Sourceval t_false : Ppxlib.Location.t -> term

Sourceval t_attr_set : string list -> term -> term

Sourceval t_bool_true : Ppxlib.Location.t -> term

Sourceval t_bool_false : Ppxlib.Location.t -> term

Sourceval t_equ : term -> term -> Ppxlib.Location.t -> term

Sourceval t_neq : term -> term -> Ppxlib.Location.t -> Ppxlib.Location.t -> term

Sourceval f_binop : binop -> term -> term -> Ppxlib.Location.t -> term

Sourceval f_not : term -> Ppxlib.Location.t -> term

Source

val t_quant : 
  quant ->
  vsymbol list ->
  term ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  term

Source

val f_forall : 
  vsymbol list ->
  term ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  term

Source

val f_exists : 
  vsymbol list ->
  term ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  term

Source

val t_lambda : 
  vsymbol list ->
  term ->
  Ttypes.ty option ->
  Ppxlib.Location.t ->
  term

Sourceval f_and : term -> term -> Ppxlib.Location.t -> term

Sourceval f_and_asym : term -> term -> Ppxlib.Location.t -> term

Sourceval f_or : term -> term -> Ppxlib.Location.t -> term

Sourceval f_or_asym : term -> term -> Ppxlib.Location.t -> term

Sourceval f_implies : term -> term -> Ppxlib.Location.t -> term

Sourceval f_iff : term -> term -> Ppxlib.Location.t -> term

Pretty printing

Sourceval print_vs : Format.formatter -> vsymbol -> unit

Sourceval print_ls_decl : Format.formatter -> lsymbol -> unit

Sourceval print_ls_nm : Format.formatter -> lsymbol -> unit

Source

val protect_on : 
  bool ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6 ->
  ('a, 'b, 'c, 'd, 'e, 'f) format6

Sourceval print_pat_node : int -> pattern Utils.Fmt.t

Sourceval print_pattern : pattern Utils.Fmt.t

Sourceval print_binop : Format.formatter -> binop -> unit

Sourceval print_quantifier : Format.formatter -> quant -> unit

Sourceval print_term : term Utils.Fmt.t

package gospel

Module Gospel.TtermSource

Module `Gospel.Tterm`Source