Unif (p.logtk.1.5.1.doc.logtk.Logtk.Unif)

Unification and Matching

Sourcetype unif_subst = Unif_subst.t

Sourcetype subst = Subst.t

Sourcetype term = InnerTerm.t

Sourcetype ty = InnerTerm.t

Sourcetype 'a sequence = ('a -> unit) -> unit

Sourceexception Fail

Raised when a unification/matching attempt fails

Source

val occurs_check : 
  depth:int ->
  subst ->
  InnerTerm.t HVar.t Scoped.t ->
  InnerTerm.t Scoped.t ->
  bool

Source

val unif_array_com : 
  ?size:[ `Same | `Smaller ] ->
  'subst ->
  op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
  'a array Scoped.t ->
  'a array Scoped.t ->
  'subst Iter.t

Generic unification over two arrays (of the same size, or the first one must be smaller or equal)

Source

val unif_list : 
  'subst ->
  op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
  'a list Scoped.t ->
  'a list Scoped.t ->
  'subst Iter.t

Generic unification over two lists (of the same size)

Source

val unif_list_com : 
  ?size:[ `Same | `Smaller ] ->
  'subst ->
  op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
  'a list Scoped.t ->
  'a list Scoped.t ->
  'subst Iter.t

Generic unification over two lists (of the same size or smaller)

Source

val pair_lists_right : 
  term ->
  term list ->
  term ->
  term list ->
  term list * term list

in HO, we have f1 l1 and f2 l2, where application is left-associative. we need to unify from the right (the outermost application is on the right) so this returns pairs to unify (including heads).

Source

val pair_lists_left : 
  term list ->
  term ->
  term list ->
  term ->
  term list * term list

in HO, we have l1 -> ret1 and l2 -> ret2, where -> is right-associative. we need to unify from the left, so this returns pairs to unify (including return types).

Signatures

Sourcemodule type S = Unif_intf.S

Base (scoped terms)

Sourcemodule Inner : S with type term = InnerTerm.t and type ty = InnerTerm.t

To be used only on terms without InnerTerm.Multiset constructor

Specializations

Sourcemodule Ty : sig ... end

Sourcemodule FO : sig ... end