JP_unif (u.24fd6415a75478f49004d92b3db5e0eb.logtk.1.6.doc.logtk.Logtk.JP

Sourcemodule T = Term

Sourcemodule US = Unif_subst

Sourcetype subst = US.t

Sourcemodule S : sig ... end

val project_onesided : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  subst OSeq.t

Source

val imitate_onesided : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  subst OSeq.t

Source

val imitate : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  (T.var * int) list ->
  subst OSeq.t

Source

val identify : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  (T.var * int) list ->
  subst OSeq.t

Source

val eliminate : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  (Type.t HVar.t * int) list ->
  subst OSeq.t

Source

val iterate : 
  ?flex_same:bool ->
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  (T.var * 'a) CCList.t ->
  Unif_subst.t option OSeq.t

Source

val find_disagreement : 
  T.t ->
  T.t ->
  ((T.t * T.t) * (T.var * int) CCList.t) option

Find disagreeing subterms. This function also returns a list of variables occurring above the disagreement pair, along with the index of the argument that the disagreement pair occurs in.

Source

val unify : 
  scope:Scoped.scope ->
  counter:int ref ->
  T.t ->
  T.t ->
  subst option OSeq.t

Sourceval unify_scoped_nonterminating : T.t Scoped.t -> T.t Scoped.t -> subst OSeq.t

Sourceval unify_scoped : T.t Scoped.t -> T.t Scoped.t -> subst option OSeq.t