PatternUnif (u.24fd6415a75478f49004d92b3db5e0eb.logtk.1.6.doc.logtk.Logtk.PatternUnif)

Pattern unification algorithm implementation

This module implements pattern unification oracle described in \urlhttp://matryoshka.gforge.inria.fr/pubs/hounif_paper.pdf. It can be applied to terms out of the pattern fragment in which case it raises NotInFragment exception.

Sourcemodule T = Term

Sourcemodule US = Unif_subst

Sourcetype subst = US.t

Sourcemodule S : sig ... end

Sourceexception NotUnifiable

Sourceexception NotInFragment

Source

val eta_expand_otf : 
  subst:subst ->
  scope:Scoped.scope ->
  Type.t list ->
  Type.t list ->
  T.t ->
  T.t ->
  T.t * T.t * Type.t list

Sourceval norm_deref : Unif_subst.t -> T.t Scoped.t -> T.t

Sourceval unif_simple : ?subst:Subst.t -> scope:int -> T.t -> T.t -> US.t option

Source

val unify_scoped : 
  ?subst:subst ->
  ?counter:int ref ->
  T.t Scoped.t ->
  T.t Scoped.t ->
  subst