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

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