PUnif (u.71670836abf97ab8c12135ebbc8c29bb.logtk.2.1.doc.logtk.Logtk.PUnif)

Pragmatic variant of JP algorithm

Provides plug-in module for UnifFramework.ml that implements pragmatic restriction of the unification algorithm described in the paper Efficient Full Higher-Order Unification (paper)

module IntSet : CCSet.S with type elt = CCInt.t

val elim_subsets_rule : 
  ?max_elims:int option ->
  elim_vars:IntSet.t ref ->
  counter:IntSet.elt ref ->
  scope:Scoped.scope ->
  Term.t ->
  Term.t ->
  int ->
  (Subst.FO.t * int) OSeq.t

val proj_hs : 
  counter:int ref ->
  scope:Scoped.scope ->
  flex:Term.t ->
  Term.t ->
  Subst.FO.t CCList.t

module Make (S : sig ... end) : UnifFramework.US