package logtk

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

Scoped Terms

Those terms are not designed to be used directly, but rather to provide a generic backend (implementing De Bruijn indices, subterms, substitutions, etc.) for other more specific representations like LogtkType, LogtkFOTerm, FOLogtkFormula...

type symbol = LogtkSymbol.t
type t

Abstract type of term

type term = t
type view = private
  1. | Var of int
    (*

    Free variable (integer: mostly useless)

    *)
  2. | RigidVar of int
    (*

    Variable that only unifies with other rigid variables

    *)
  3. | BVar of int
    (*

    Bound variable (De Bruijn index)

    *)
  4. | Bind of symbol * t * t
    (*

    LogtkType, sub-term

    *)
  5. | Const of symbol
    (*

    Constant

    *)
  6. | Record of (string * t) list * t option
    (*

    Extensible record

    *)
  7. | RecordGet of t * string
    (*

    get r name is r.name

    *)
  8. | RecordSet of t * string * t
    (*

    set r name t is r.name <- t

    *)
  9. | Multiset of t list
    (*

    Multiset of terms

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

    Uncurried application

    *)
  11. | At of t * t
    (*

    Curried application

    *)
  12. | SimpleApp of symbol * t list
    (*

    For representing special constructors

    *)
val view : t -> view

View on the term's head form

module Kind : sig ... end
val kind : t -> Kind.t
type type_result =
  1. | NoType
  2. | HasType of t
val ty : t -> type_result

LogtkType of the term, if any

val ty_exn : t -> t

Same as ty, but fails if the term has no type

  • raises Invalid_argument

    if the type is NoType

include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int

Constructors

Some constructors, such as record, may raise IllFormedTermif the arguments are ill-formed (several occurrences of a key), or, for variables, if the number is negative

exception IllFormedTerm of string
type nat = int
val const : kind:Kind.t -> ty:t -> symbol -> t
val app : kind:Kind.t -> ty:t -> t -> t list -> t
val bind : kind:Kind.t -> ty:t -> varty:t -> symbol -> t -> t
val var : kind:Kind.t -> ty:t -> nat -> t
val rigid_var : kind:Kind.t -> ty:t -> nat -> t
val bvar : kind:Kind.t -> ty:t -> nat -> t
val record : kind:Kind.t -> ty:t -> (string * t) list -> rest:t option -> t
val record_get : kind:Kind.t -> ty:t -> t -> string -> t
val record_set : kind:Kind.t -> ty:t -> t -> string -> t -> t
val multiset : kind:Kind.t -> ty:t -> t list -> t
val at : kind:Kind.t -> ty:t -> t -> t -> t
val simple_app : kind:Kind.t -> ty:t -> symbol -> t list -> t
val mk_at : kind:Kind.t -> ty:t -> t -> t -> t

alias to at

val tType : t

The root of the type system. It doesn't have a type. It has kind Kind.LogtkType

val cast : ty:t -> t -> t

Change the type

val change_kind : kind:Kind.t -> t -> t

Change the kind

val is_var : t -> bool
val is_bvar : t -> bool
val is_rigid_var : t -> bool
val is_const : t -> bool
val is_bind : t -> bool
val is_app : t -> bool
val is_record : t -> bool
val is_record_get : t -> bool
val is_record_set : t -> bool
val is_multiset : t -> bool
val is_at : t -> bool
val hashcons_stats : unit -> int * int * int * int * int * int

Flags

be VERY careful with flags. Due to hashconsing, they will be shared between every instance of a term, so only use them for properties that are universal. Only Sys.word_size - 1 flags can exist in a program.

type flag
val new_flag : unit -> flag
val set_flag : t -> flag -> unit
val get_flag : t -> flag -> bool

Containers

module Map : Sequence.Map.S with type key = term
module Set : Sequence.Set.S with type elt = term
module Tbl : sig ... end

De Bruijn indices handling

module DB : sig ... end

High level constructors

val bind_vars : kind:Kind.t -> ty:t -> symbol -> t list -> t -> t

bind several free variables in the term, transforming it to use De Bruijn indices.

  • parameter ty

    return type of the term

Iterators

module Seq : sig ... end

LogtkPositions

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.

Variables

val close_vars : kind:Kind.t -> ty:t -> symbol -> t -> t

Close all free variables of the term using the binding symbol

val ground : t -> bool

true if the term contains no free variables

Misc

val size : t -> int
val depth : t -> int
val head : t -> symbol option

Head symbol, or None if the term is a (bound) variable

val all_positions : ?vars:bool -> ?pos:LogtkPosition.t -> t -> 'a -> ('a -> t -> LogtkPosition.t -> 'a) -> 'a

Fold on all subterms of the given term, with their position.

  • parameter pos

    the initial position (prefix). Default: empty.

  • parameter vars

    if true, also fold on variables Default: false.

  • returns

    the accumulator

IO

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
include LogtkInterfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type print_hook = int -> (Buffer.t -> t -> unit) -> Buffer.t -> 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 -> Buffer.t -> t -> unit
val add_default_hook : print_hook -> unit

Add a print hook that will be used from now on

Misc

val fresh_var : kind:Kind.t -> ty:t -> unit -> t

fresh_var ~kind ~ty () returns a fresh, unique, NOT HASHCONSED variable that will therefore never be equal to any other variable.

val _var : kind:Kind.t -> ty:t -> int -> t

Unsafe version of var that accepts negative index