Module Logtk__TypedSTerm

Simple Typed Terms

.

type location = Logtk.ParseLocation.t
type t
type term = t
type ty = t
type match_cstor = {
cstor_id : Logtk.ID.t;
cstor_ty : ty;
cstor_args : ty list;
}

a constructor of given type, applied to a list of type argumentss

type match_branch = match_cstor * t Logtk.Var.t list * t
type view = private
| Var of t Logtk.Var.t

variable

| Const of Logtk.ID.t

constant

| App of t * t list

apply term

| Ite of t * t * t
| Match of t * match_branch list
| Let of (t Logtk.Var.t * t) list * t
| Bind of Logtk.Binder.t * t Logtk.Var.t * t

bind variable in term

| AppBuiltin of Logtk.Builtin.t * t list
| Multiset of t list
| Record of (string * t) list * t option

extensible record

| Meta of meta_var

Unification variable

and meta_var = t Logtk.Var.t * t option Stdlib.ref * [ `Generalize | `BindDefault | `NoBind ]
val view : t -> view
val loc : t -> location option
val ty : t -> t option
val ty_exn : t -> t
val head : t -> Logtk.ID.t option
val head_exn : t -> Logtk.ID.t
raises Not_found

if not an application/const

val deref : t -> t

While t is a bound Meta variable, follow its link

include Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
type t
val compare : t -> t -> int

Constructors

exception IllFormedTerm of string
val tType : t
val prop : t
val var : ?⁠loc:location -> t Logtk.Var.t -> t
val var_of_string : ?⁠loc:location -> ty:t -> string -> t
val app : ?⁠loc:location -> ty:t -> t -> t list -> t
val app_whnf : ?⁠loc:location -> ty:t -> t -> t list -> t

application + WHNF

val const : ?⁠loc:location -> ty:t -> Logtk.ID.t -> t
val const_of_cstor : ?⁠loc:location -> match_cstor -> t
val ite : ?⁠loc:location -> t -> t -> t -> t
val match_ : ?⁠loc:location -> t -> match_branch list -> t
val let_ : ?⁠loc:location -> (t Logtk.Var.t * t) list -> t -> t
val app_builtin : ?⁠loc:location -> ty:t -> Logtk.Builtin.t -> t list -> t
val builtin : ?⁠loc:location -> ty:t -> Logtk.Builtin.t -> t
val bind : ?⁠loc:location -> ty:t -> Logtk.Binder.t -> t Logtk.Var.t -> t -> t
val bind_list : ?⁠loc:location -> ty:t -> Logtk.Binder.t -> t Logtk.Var.t list -> t -> t
val multiset : ?⁠loc:location -> ty:t -> t list -> t
val meta : ?⁠loc:location -> meta_var -> t
val record : ?⁠loc:location -> ty:t -> (string * t) list -> rest:t Logtk.Var.t option -> t
val record_flatten : ?⁠loc:location -> ty:t -> (string * t) list -> rest:t option -> t

Build a record with possibly a row variable.

raises IllFormedTerm

if the rest is not either a record or a variable.

val fun_l : ?⁠loc:location -> t Logtk.Var.t list -> t -> t
val of_string : ?⁠loc:location -> ty:t -> string -> t

Make a constant from this string

val at_loc : ?⁠loc:location -> t -> t
val with_ty : ty:t -> t -> t
val map_ty : t -> f:(t -> t) -> t
val fresh_var : ?⁠loc:location -> ty:t -> unit -> t

fresh free variable with the given type.

val box_opaque : t -> t

Put a box around this

Specific Views

module Ty : sig ... end
val sort_ty_vars_first : t Logtk.Var.t list -> t Logtk.Var.t list

sort the given list of variables by putting type variables first

module Form : sig ... end

Utils

val is_var : t -> bool
val is_meta : t -> bool
val is_const : t -> bool
val is_fun : t -> bool
val is_ground : t -> bool

true iff there is no free variable

val is_monomorphic : t -> bool

true if there are no type variables

val is_subterm : strict:bool -> t -> of_:t -> bool

is_subterm a ~of_:b is true if a is a subterm of b.

parameter strict

if true, a must be a strict subterm of b, that is, not b itself

val closed : t -> bool

closed t is true iff all bound variables of t occur under a binder (i.e. they are actually bound in t)

val unfold_binder : Logtk.Binder.t -> t -> t Logtk.Var.t list * t

unfold_binder b (b v1 (b v2... (b vn t))) returns [v1,...,vn], t

val unfold_fun : t -> t Logtk.Var.t list * t
val var_occurs : var:t Logtk.Var.t -> t -> bool

var_occurs ~var t is true iff var occurs in t

val as_id_app : t -> (Logtk.ID.t * Ty.t * t list) option
val vars : t -> t Logtk.Var.t list
val free_vars : t -> t Logtk.Var.t list
val free_vars_l : t list -> t Logtk.Var.t list
val free_vars_set : t -> t Logtk.Var.Set.t
val close_all : ty:t -> Logtk.Binder.t -> t -> t

Bind all free vars with the symbol

val close_with_vars : ?⁠binder:Logtk.Binder.t -> t list -> t -> t
val map : f:('a -> t -> t) -> bind:('a -> ty Logtk.Var.t -> 'a * ty Logtk.Var.t) -> 'a -> t -> t

Generic non-recursive map

include Logtk.Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_inner : t CCFormat.printer
val pp_with_ty : t CCFormat.printer
val pp_in : Logtk.Output_format.t -> t CCFormat.printer
module Set : Iter.Set.S with type Set.elt = term
module Map : Iter.Map.S with type Map.key = term
module Tbl : Stdlib.Hashtbl.S with type Tbl.key = term
module Seq : sig ... end

Substitutions

module Subst : sig ... end
val rename : (term, term Logtk.Var.t) Logtk.Var.Subst.t -> t -> t

Perform renaming

val rename_all_vars : t -> t

Rename bound variables

Table of Variables

module Var_tbl : CCHashtbl.S with type Var_tbl.key = t Logtk.Var.t

Unification

exception UnifyFailure of string * (term * term) list * location option
val pp_stack : (term * term) list CCFormat.printer
module UStack : sig ... end
val unify : ?⁠allow_open:bool -> ?⁠loc:location -> ?⁠st:UStack.t -> ?⁠subst:Subst.t -> term -> term -> unit

unifies destructively the two given terms, by modifying references that occur under Meta. Regular variables are not modified.

parameter allow_open

if true, metas can be unified to terms with free variables (default false)

parameter st

used for backtracking

parameter subst

substitution for bound variables

raises UnifyFailure

if unification fails.

val apply_unify : ?⁠gen_fresh_meta:(unit -> meta_var) -> ?⁠allow_open:bool -> ?⁠loc:location -> ?⁠st:UStack.t -> ?⁠subst:Subst.t -> t -> t list -> t

apply_unify f_ty args compute the type of a function of type f_ty, when applied to parameters args. The first elements of args might be interpreted as types, the other ones as terms (whose types are unified against expected types).

val app_infer : ?⁠st:UStack.t -> ?⁠subst:Subst.t -> t -> t list -> t

app_infer f l computes the type ty of f l, and return app ~ty f l

raises UnifyFailure

if types do not correspond

val try_alpha_renaming : t -> t -> Subst.t option
val simplify_formula : t -> t

Conversion

val erase : t -> Logtk.STerm.t

TPTP

module TPTP : sig ... end
module TPTP_THF : sig ... end
module ZF : sig ... end