Module Logtk.STerm

Simple Terms

.

type location = ParseLocation.t
type var =
| V of string
| Wildcard
type t = private {
term : view;
loc : location option;
}
type match_branch =
| Match_case of string * var list * t
| Match_default of t
type view =
| Var of var

variable

| Const of string

constant

| AppBuiltin of Builtin.t * t list
| App of t * t list

apply term

| Ite of t * t * t
| Match of t * match_branch list
| Let of (var * t) list * t
| Bind of Binder.t * typed_var list * t

bind n variables

| List of t list

special constructor for lists

| Record of (string * t) list * var option

extensible record

type typed_var = var * t option
type term = t
val view : t -> view
val loc : t -> location option
include Interfaces.HASH with type t := t
include Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
val var : ?⁠loc:location -> string -> t
val v_wild : t

wildcard

val mk_var : ?⁠loc:location -> var -> t

wildcard

val app : ?⁠loc:location -> t -> t list -> t
val app_const : ?⁠loc:location -> string -> t list -> t
val builtin : ?⁠loc:location -> Builtin.t -> t
val app_builtin : ?⁠loc:location -> Builtin.t -> t list -> t
val const : ?⁠loc:location -> string -> t
val bind : ?⁠loc:location -> Binder.t -> typed_var list -> t -> t
val ite : ?⁠loc:location -> t -> t -> t -> t
val match_ : ?⁠loc:location -> t -> match_branch list -> t
val let_ : ?⁠loc:location -> (var * t) list -> t -> t
val list_ : ?⁠loc:location -> t list -> t
val nil : t
val record : ?⁠loc:location -> (string * t) list -> rest:var option -> t
val at_loc : loc:location -> t -> t
val wildcard : t
val is_app : t -> bool
val is_var : t -> bool
val true_ : t
val false_ : t
val and_ : ?⁠loc:location -> t list -> t
val or_ : ?⁠loc:location -> t list -> t
val not_ : ?⁠loc:location -> t -> t
val equiv : ?⁠loc:location -> t -> t -> t
val xor : ?⁠loc:location -> t -> t -> t
val imply : ?⁠loc:location -> t -> t -> t
val eq : ?⁠loc:location -> t -> t -> t
val neq : ?⁠loc:location -> t -> t -> t
val forall : ?⁠loc:location -> typed_var list -> t -> t
val exists : ?⁠loc:location -> typed_var list -> t -> t
val lambda : ?⁠loc:location -> typed_var list -> t -> t
val int_ : Z.t -> t
val of_int : int -> t
val rat : Q.t -> t
val real : string -> t
val tType : t
val term : t
val prop : t
val ty_int : t
val ty_rat : t
val ty_real : t
val fun_ty : ?⁠loc:location -> t list -> t -> t
val forall_ty : ?⁠loc:location -> typed_var list -> t -> t
val ty_unfold : t -> t list * t
val unfold_bind : Binder.t -> t -> typed_var list * t
module Set : CCSet.S with type Set.elt = term
module Map : CCMap.S with type Map.key = term
module Tbl : CCHashtbl.S with type Tbl.key = term
module StringSet : CCSet.S with type StringSet.elt = string
module Seq : sig ... end
val ground : t -> bool
val close_all : Binder.t -> t -> t

Bind all free vars with the symbol

val subterm : strict:bool -> t -> sub:t -> bool

Bind all free vars with the symbol

is sub a (strict?) subterm of the other arg?

Print

include Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_typed_var : typed_var CCFormat.printer
val pp_var : var CCFormat.printer

Formats

module TPTP : sig ... end
module ZF : sig ... end
val pp_in : Output_format.t -> t CCFormat.printer

Subst

module StrMap : CCMap.S with type StrMap.key = string
type subst = t StrMap.t
val empty_subst : subst
val merge_subst : subst -> subst -> subst

merge a b merges a into b, but favors b in case of conflict

val apply_subst : subst -> term -> term