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 in_fool_fragment : t -> bool * bool
val is_true_or_false : t -> bool
val lambda_depth : t -> int option

If term has no lambdas reutrn None; otherwise, return Some d where d is the maximal level of lambda nestings

val comb_depth : t -> int option

combinatory equivalent to lambda_depth

val hd_is_comb : Builtin.t -> bool
val is_comb : t -> bool
val mk_fresh_skolem : ?prefix:string -> 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 as_app_mono : t -> t * t list

head term, but still with type arguments and the remaining 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
val is_properly_encoded : t -> bool
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 occurring multiple times)

val monomorphic : t -> bool

is the term linear? (no vars occurring 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 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 : ?filter_formula_subterms:(Builtin.t -> t list -> int list CCOpt.t) -> ?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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct