PatternUnif (p.logtk.2.0.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.

module US = Unif_subst

type subst = US.t

module S : sig ... end

exception NotUnifiable

exception NotInFragment

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

val norm_deref : Unif_subst.t -> Term.t Scoped.t -> Term.t

val unif_simple : 
  ?subst:Subst.t ->
  scope:int ->
  Term.t ->
  Term.t ->
  US.t option

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