package logtk

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

Prolog-like LogtkTyped Terms

.

These terms are scoped, and possibly typed. LogtkType inference should be performed on them.

type location = LogtkParseLocation.t
type t
type term = t
type view = private
  1. | Var of string
    (*

    variable

    *)
  2. | BVar of string
    (*

    bound variable

    *)
  3. | Const of LogtkSymbol.t
    (*

    constant

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

    apply term

    *)
  5. | Bind of LogtkSymbol.t * t * t
    (*

    bind variable in term

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

    extensible record

    *)
val view : t -> view
val loc : t -> location option
val ty : t -> t option
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

exception IllFormedTerm of string
val tType : t
val wildcard : t
val var : ?loc:location -> ?ty:t -> string -> t
val bvar : ?loc:location -> ?ty:t -> string -> t
val app : ?loc:location -> ?ty:t -> t -> t list -> t
val const : ?loc:location -> ?ty:t -> LogtkSymbol.t -> t
val bind : ?loc:location -> ?ty:t -> LogtkSymbol.t -> t -> t -> t
val bind_list : ?loc:location -> ?ty:t -> LogtkSymbol.t -> t list -> t -> t
val multiset : ?loc:location -> ?ty:t -> t list -> t
val record : ?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 of_string : ?loc:location -> ?ty:t -> string -> t
val of_int : ?ty:t -> int -> t
val at_loc : ?loc:location -> t -> t
val with_ty : ?ty:t -> t -> t
val fresh_var : ?loc:location -> ?ty:t -> unit -> t

fresh free variable with the given type.

val fresh_bvar : ?loc:location -> ?ty:t -> unit -> t

LogtkUtils

val is_var : t -> bool
val is_bvar : t -> bool
val ground : t -> bool

true iff there is no free variable

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 vars : t -> t list
val close_all : ?ty:t -> LogtkSymbol.t -> t -> t

Bind all free vars with the symbol

include LogtkInterfaces.PRINT with type t := t
val pp : Buffer.t -> t -> unit
val to_string : t -> string
val fmt : Format.formatter -> t -> unit
module Set : Sequence.Set.S with type elt = term
module Map : Sequence.Map.S with type key = term
module Tbl : Hashtbl.S with type key = term
module Seq : sig ... end

Visitor

module Visitor : sig ... end

Substitutions, LogtkUnification

type 'a or_error = [
  1. | `Error of string
  2. | `Ok of 'a
]
module Subst : sig ... end
val rename : term -> term

Rename all free variables

exception LogtkUnifyFailure of term * term * Subst.t
val unify : ?subst:Subst.t -> term -> term -> Subst.t or_error

LogtkUnify two terms, might fail

val unify_exn : ?subst:Subst.t -> term -> term -> Subst.t

Same as unify, but can raise.

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