package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Simple Typed Terms

.

Similar to STerm, but this time the terms are properly scoped (using Var) and typed.

These terms are suitable for many preprocessing transformations, including CNF.

They can be obtained from STerm.t using TypeInference.

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

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

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

    variable

    *)
  2. | Const of ID.t
    (*

    constant

    *)
  3. | App of t * t list
    (*

    apply term

    *)
  4. | Ite of t * t * t
  5. | Match of t * match_branch list
  6. | Let of (t Var.t * t) list * t
  7. | Bind of Binder.t * t Var.t * t
    (*

    bind variable in term

    *)
  8. | AppBuiltin of Builtin.t * t list
  9. | Multiset of t list
  10. | Record of (string * t) list * t option
    (*

    extensible record

    *)
  11. | Meta of meta_var
    (*

    Unification variable

    *)
and meta_var = t Var.t * t option 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 -> ID.t option
val head_exn : t -> ID.t
val deref : t -> t

While t is a bound Meta variable, follow its link

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

Constructors

exception IllFormedTerm of string
val tType : t
val prop : t
val var : ?loc:location -> t 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 -> 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 Var.t * t) list -> t -> t
val app_builtin : ?loc:location -> ty:t -> Builtin.t -> t list -> t
val builtin : ?loc:location -> ty:t -> Builtin.t -> t
val bind : ?loc:location -> ty:t -> Binder.t -> t Var.t -> t -> t
val bind_list : ?loc:location -> ty:t -> Binder.t -> t 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 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 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 Var.t list -> t 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 : Binder.t -> t -> t Var.t list * t

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

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

var_occurs ~var t is true iff var occurs in t

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

Bind all free vars with the symbol

val close_with_vars : t list -> t -> t
val lift_lambdas : t -> t * t list
val map : f:('a -> t -> t) -> bind:('a -> ty Var.t -> 'a * ty Var.t) -> 'a -> t -> t

Generic non-recursive map

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

Substitutions

module Subst : sig ... end
val rename : (term, term Var.t) 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 key = t 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

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

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

Conversion

val erase : t -> STerm.t

TPTP

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