package logtk

  1. Overview
  2. Docs
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.

  • raises LogtkUnifyFailure

    if the unification fails