package logtk

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

Terms

Those terms provide a direct presentation of higher-order terms with lambdas in the sense that they make currying possible (as well as applying functions to other terms).

This is as if terms had an `apply` symbol everywhere, but more lightweight.

Types and terms are mixed because it makes application much easier (applying to a type and to a term are the same thing). It might also make dependent typing possible some day.

Term

type t = private InnerTerm.t
type term = t
type var = Type.t HVar.t

Variables are typed with Type.t

type view = private
  1. | AppBuiltin of Builtin.t * t list
  2. | DB of int
    (*

    Bound variable (De Bruijn index)

    *)
  3. | Var of var
    (*

    Term variable

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

    Typed constant

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

    Application to a list of terms (cannot be left-nested)

    *)
  6. | Fun of Type.t * t
    (*

    Lambda abstraction

    *)
val view : t -> view
module Classic : sig ... end
val subterm : sub:t -> t -> bool

checks whether sub is a (non-strict) subterm of t

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
val ty : t -> Type.t

Obtain the type of a term..

module IntMap : Map.S with type key = int
module Set : CCSet.S with type elt = t
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t
val hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

val same_l : t list -> t list -> bool

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise. Precondition: both lists have the same length

val same_l_gen : t list -> t list -> bool

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise. Precondition: both lists have the same length

Constructors

val var : var -> t
val var_of_int : ty:Type.t -> int -> t
val bvar : ty:Type.t -> int -> t

Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.

val builtin : ty:Type.t -> Builtin.t -> t
val app_builtin : ty:Type.t -> Builtin.t -> t list -> t
val const : ty:Type.t -> ID.t -> t

Create a typed constant

val tyapp : t -> Type.t list -> t

Apply a term to types

  • raises Type.Error

    if types do not match.

val app : t -> t list -> t

Apply a term to a list of terms

val app_w_ty : ty:Type.t -> t -> t list -> t

Apply a term to a list of terms

val app_full : t -> Type.t list -> t list -> t

Apply the term to types, then to terms

val true_ : t
val false_ : t
val fun_ : Type.t -> t -> t
val fun_l : Type.t list -> t -> t
val fun_of_fvars : var list -> t -> t

Build a function from a list of free vars + the body. This performs the De Bruijn transformation, and shifts the body.

val open_fun : t -> Type.t list * t
val open_fun_offset : offset:int -> t -> var list * t * int

open_fun ~offset (λxy. F) returns [v1,v2], F[v1/x,v2/y], offset+2 where v1 and v2 are fresh variables starting from offset

val grounding : Type.t -> t

grounding ty is a unique constant of type ty

val is_var : t -> bool
val is_appbuiltin : t -> bool
val is_bvar : t -> bool
val is_formula : t -> bool
val is_app : t -> bool
val is_const : t -> bool
val is_fun : t -> bool
val is_app_var : t -> bool
val is_type : t -> bool

Does it have type tType?

val in_pfho_fragment : t -> bool
val in_lfho_fragment : t -> bool
val is_fo_term : t -> bool
val is_true_or_false : t -> bool
val mk_fresh_skolem : var list -> Type.t -> (ID.t * Type.t) * t
val as_const : t -> ID.t option
val as_const_exn : t -> ID.t
val as_var : t -> var option
val as_var_exn : t -> var
val as_bvar_exn : t -> int
val as_app : t -> t * t list

as_app t decomposes t into a head (non-application) and arguments, such as (let f,l = as_app t in app f l) = t

val as_fun : t -> Type.t list * t

Open functions

val head_term : t -> t

head_term t = fst (as_app t)

val head_term_mono : t -> t

head term, but still with type arguments

val args : t -> t list

args t = snd (as_app t)

val of_term_unsafe : InnerTerm.t -> t

NOTE: this can break the invariants and make view fail. Only apply with caution.

val of_term_unsafe_l : InnerTerm.t list -> t list
val of_ty : Type.t -> t

Upcast from type

val mk_tmp_cst : counter:int ref -> ty:Type.t -> t
module VarSet : CCSet.S with type elt = var
module VarMap : CCMap.S with type key = var
module VarTbl : CCHashtbl.S with type key = var

Iters

module Seq : sig ... end
val var_occurs : var:var -> t -> bool

var_occurs ~var t true iff var in t

val is_ground : t -> bool

is the term ground? (no free vars)

val is_linear : t -> bool

is the term ground? (no free vars)

is the term linear? (no vars occuring multiple times)

val monomorphic : t -> bool

is the term linear? (no vars occuring multiple times)

true if the term contains no type var

val is_beta_reducible : t -> bool
val has_lambda : t -> bool
val max_var : VarSet.t -> int

find the maximum variable

val min_var : VarSet.t -> int

minimum variable

val add_vars : unit VarTbl.t -> t -> unit

add variables of the term to the set

val vars : t -> VarSet.t

compute variables of the terms

val vars_prefix_order : t -> var list

variables in prefix traversal order

val depth : t -> int

depth of the term

val head : t -> ID.t option

head ID.t

val head_exn : t -> ID.t

head ID.t (or Invalid_argument)

val size : t -> int

Size (number of nodes)

val simplify_bools : t -> t
val normalize_bools : t -> t
val cover_with_terms : ?depth:int -> ?recurse:bool -> t -> t option list -> t list
val max_cover : t -> t option list -> t
val weight : ?var:int -> ?sym:(ID.t -> int) -> t -> int

Compute the weight of a term, given a weight for variables and one for ID.ts.

  • parameter var

    unique weight for every variable (default 1)

  • parameter sym

    function from ID.ts to their weight (default const 1)

  • since 0.5.3
val ho_weight : t -> int
val ty_vars : t -> Type.VarSet.t

Set of free type variables

val is_ho_var : t -> bool
val is_ho_app : t -> bool

is_ho_app (F t1…tn) is true, when F is a variable (of any function type)

val as_ho_app : t -> (Type.t HVar.t * t list) option

as_ho_app (F t1…tn) = Some (F, [t1…tn])

val is_ho_pred : t -> bool

is_ho_pred (F t1…tn) is true, when F is a predicate variable

val is_ho_at_root : t -> bool

is_ho_at_root t returns true if the term t is a higher-order variable, possibly applied (i.e. is_ho_var t || is_ho_app t)

Subterms and Positions

module Pos : sig ... end
val replace : t -> old:t -> by:t -> t

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

val replace_m : t -> t Map.t -> t

replace t m syntactically replaces all occurrences of bindings of the map in t, starting from the root

High-level operations

val symbols : ?init:ID.Set.t -> t -> ID.Set.t

Symbols of the term (keys of signature)

val contains_symbol : ID.t -> t -> bool

Does the term contain this given ID.t?

Fold

High level fold-like combinators

val all_positions : ?vars:bool -> ?ty_args:bool -> ?var_args:bool -> ?fun_bodies:bool -> ?pos:Position.t -> t -> t Position.With.t Iter.t

Iterate on all sub-terms with their position.

  • parameter vars

    specifies whether variables are folded on (default false).

  • parameter ty_args

    specifies whether type arguments are folded on (default true).

  • parameter var_args

    specifies whether arguments of applied variables are folded on (default true).

  • parameter fun_bodies

    specifies whether bodies of lambda-expressions are folded on (default true).

  • parameter pos

    the initial position (default empty)

Some AC-utils

module type AC_SPEC = sig ... end
module AC (A : AC_SPEC) : sig ... end

Printing/parsing

val print_all_types : bool ref

If true, pp will print the types of all annotated terms

include Interfaces.PRINT with type t := t
val to_string : t -> string
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type print_hook = int -> t CCFormat.printer -> Format.formatter -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

val pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
val add_hook : print_hook -> unit

Hook used by default for printing

val default_hooks : unit -> print_hook list

List of default hooks

val debugf : Format.formatter -> t -> unit

debugf printing, with sorts

Formulas

module Form : sig ... end

Arith

module Arith : sig ... end
val close_quantifier : Builtin.t -> Type.t list -> t -> t
val has_ho_subterm : t -> bool
module DB : sig ... end

TPTP

module TPTP : sig ... end
module ZF : sig ... end
module Conv : sig ... end