package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = LogtkType.t
val unification : ?env1:env -> ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst

LogtkUnify terms, returns a subst or

  • raises Fail

    if the terms are not unifiable

  • parameter env1

    environment for the first term

  • parameter env2

    environment for the second term

val matching : ?allow_open:bool -> ?env1:env -> ?env2:env -> ?subst:subst -> pattern:term -> scope -> term -> scope -> subst

matching ~pattern scope_p b scope_b returns sigma such that sigma pattern = b, or fails. Only variables from the scope of pattern can be bound in the subst.

  • parameter subst

    initial substitution (default empty)

  • parameter allow_open

    if true, variables can bind to non-closed DB terms (default false)

  • raises Fail

    if the terms do not match.

  • raises Invalid_argument

    if the two scopes are equal

val matching_same_scope : ?env1:env -> ?env2:env -> ?protect:term Sequence.t -> ?subst:subst -> scope:scope -> pattern:term -> term -> subst

matches pattern (more general) with the other term. The two terms live in the same scope, which is passed as the scope argument. It needs to gather the variables of the other term to make sure they are not bound.

  • parameter scope

    the common scope of both terms

  • parameter protect

    a sequence of variables to protect (they cannot be bound during matching!). Variables of the second term are automatically protected.

val matching_adapt_scope : ?env1:env -> ?env2:env -> ?protect:term Sequence.t -> ?subst:subst -> pattern:term -> scope -> term -> scope -> subst

Call either matching or matching_same_scope depending on whether the given scopes are the same or not.

val variant : ?env1:env -> ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst

Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent

val eq : ?env1:env -> ?env2:env -> subst:subst -> term -> scope -> term -> scope -> bool

eq subst t1 s1 t2 s2 returns true iff the two terms are equal under the given substitution, i.e. if applying the substitution will return the same term.

val are_unifiable : term -> term -> bool
val matches : pattern:term -> term -> bool
val are_variant : term -> term -> bool