package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.PatternUnifSource

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
Sourceval 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
Sourceval unify_scoped : ?subst:subst -> ?counter:int ref -> T.t Scoped.t -> T.t Scoped.t -> subst
OCaml

Innovation. Community. Security.