Safe Haskell	None
Language	Haskell2010

AST.Unify

Description

Unification

Synopsis

unify :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UVarOf m) t -> m (Tree (UVarOf m) t)
class (Eq (Tree (UVarOf m) t), RTraversable t, ZipMatch t, HasTypeConstraints t, HasQuantifiedVar t, MonadScopeConstraints (TypeConstraintsOf t) m, MonadQuantify (TypeConstraintsOf t) (QVar t) m) => Unify m t where
- binding :: BindingDict (UVarOf m) m t
- unifyError :: Tree (UnifyError t) (UVarOf m) -> m a
- structureMismatch :: (forall c. Unify m c => Tree (UVarOf m) c -> Tree (UVarOf m) c -> m (Tree (UVarOf m) c)) -> Tree (UTermBody (UVarOf m)) t -> Tree (UTermBody (UVarOf m)) t -> m ()
- unifyRecursive :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Unify m))
data BindingDict v m t = BindingDict {
- lookupVar :: Tree v t -> m (Tree (UTerm v) t)
- newVar :: Tree (UTerm v) t -> m (Tree v t)
- bindVar :: Tree v t -> Tree (UTerm v) t -> m ()
}
type family UVarOf (m :: Type -> Type) :: Knot -> Type
module AST.Unify.Constraints
data UnifyError t k
- = SkolemUnified (k # t) (k # t)
- | SkolemEscape (k # t)
- | ConstraintsViolation (t k) (TypeConstraintsOf t)
- | Occurs (t k) (t k)
- | Mismatch (t k) (t k)
updateConstraints :: Unify m t => TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m ()
updateTermConstraints :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTermBody (UVarOf m)) t -> TypeConstraintsOf t -> m ()
updateTermConstraintsH :: Unify m t => Tree (WithConstraint (UVarOf m)) t -> m ()
unifyUTerms :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t)
unifyUnbound :: Unify m t => Tree (UVarOf m) t -> TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t)

Documentation

unify :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UVarOf m) t -> m (Tree (UVarOf m) t) Source #

Unify unification variables

class (Eq (Tree (UVarOf m) t), RTraversable t, ZipMatch t, HasTypeConstraints t, HasQuantifiedVar t, MonadScopeConstraints (TypeConstraintsOf t) m, MonadQuantify (TypeConstraintsOf t) (QVar t) m) => Unify m t where Source #

Unify m t enables unify to perform unification for t in the Monad m.

The unifyRecursive method represents the constraint that Unify m applies to all recursive child nodes. It replaces context for Unify to avoid UndecidableSuperClasses.

Minimal complete definition

binding, unifyError

Methods

binding :: BindingDict (UVarOf m) m t Source #

The implementation for unification variables binding and lookup

unifyError :: Tree (UnifyError t) (UVarOf m) -> m a Source #

Handles a unification error.

If unifyError is called then unification has failed. A compiler implementation may present an error message based on the provided UnifyError when this occurs.

structureMismatch :: (forall c. Unify m c => Tree (UVarOf m) c -> Tree (UVarOf m) c -> m (Tree (UVarOf m) c)) -> Tree (UTermBody (UVarOf m)) t -> Tree (UTermBody (UVarOf m)) t -> m () Source #

What to do when top-levels of terms being unified do not match.

Usually this will cause a unifyError.

Some AST terms could be equivalent despite not matching structurally, like record field extentions with the fields ordered differently. Those would override the default implementation to handle the unification of mismatching structures.

unifyRecursive :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Unify m)) Source #

unifyRecursive :: KNodesConstraint t (Unify m) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Unify m)) Source #

Instances

Recursive (Unify m) Source #
Instance details Defined in AST.Class.Unify Methods recurse :: (KNodes k, Unify m k) => Proxy (Unify m k) -> Dict (KNodesConstraint k (Unify m)) Source #

data BindingDict v m t Source #

BindingDict implements unification variables for a type in a unification monad.

It is parameterized on:

v: The unification variable Knot
m: The Monad to bind in
t: The unified term's Knot

Has 2 implementations in syntax-tree:

bindingDict for pure state based unification
stBinding for ST based unification

Constructors

BindingDict
Fields lookupVar :: Tree v t -> m (Tree (UTerm v) t) newVar :: Tree (UTerm v) t -> m (Tree v t) bindVar :: Tree v t -> Tree (UTerm v) t -> m ()

type family UVarOf (m :: Type -> Type) :: Knot -> Type Source #

Unification variable type for a unification monad

module AST.Unify.Constraints

data UnifyError t k Source #

An error that occurred during unification

Constructors

SkolemUnified (k # t) (k # t)	A universally quantified variable was unified with a different type
SkolemEscape (k # t)	A universally quantified variable escapes its scope
ConstraintsViolation (t k) (TypeConstraintsOf t)	A term violates constraints that should apply to it
Occurs (t k) (t k)	Infinite type encountered. A type occurs within itself
Mismatch (t k) (t k)	Unification between two mismatching type structures

Instances

KNodes t => KNodes (UnifyError t) Source #
Instance details Defined in AST.Unify.Error Associated Types type KNodesConstraint (UnifyError t) c :: Constraint Source # data KWitness (UnifyError t) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (UnifyError t) c => KWitness (UnifyError t) n -> Proxy c -> (c n -> r) -> r Source #
KFunctor t => KFunctor (UnifyError t) Source #
Instance details Defined in AST.Unify.Error Methods mapK :: (forall (n :: Knot -> Type). KWitness (UnifyError t) n -> Tree p n -> Tree q n) -> Tree (UnifyError t) p -> Tree (UnifyError t) q Source #
KFoldable t => KFoldable (UnifyError t) Source #
Instance details Defined in AST.Unify.Error Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (UnifyError t) n -> Tree p n -> a) -> Tree (UnifyError t) p -> a Source #
KTraversable t => KTraversable (UnifyError t) Source #
Instance details Defined in AST.Unify.Error Methods sequenceK :: Applicative f => Tree (UnifyError t) (ContainedK f p) -> f (Tree (UnifyError t) p) Source #
Constraints (UnifyError t k) Eq => Eq (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods (==) :: UnifyError t k -> UnifyError t k -> Bool # (/=) :: UnifyError t k -> UnifyError t k -> Bool #
Constraints (UnifyError t k) Ord => Ord (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods compare :: UnifyError t k -> UnifyError t k -> Ordering # (<) :: UnifyError t k -> UnifyError t k -> Bool # (<=) :: UnifyError t k -> UnifyError t k -> Bool # (>) :: UnifyError t k -> UnifyError t k -> Bool # (>=) :: UnifyError t k -> UnifyError t k -> Bool # max :: UnifyError t k -> UnifyError t k -> UnifyError t k # min :: UnifyError t k -> UnifyError t k -> UnifyError t k #
Constraints (UnifyError t k) Show => Show (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods showsPrec :: Int -> UnifyError t k -> ShowS # show :: UnifyError t k -> String # showList :: [UnifyError t k] -> ShowS #
Generic (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Associated Types type Rep (UnifyError t k) :: Type -> Type # Methods from :: UnifyError t k -> Rep (UnifyError t k) x # to :: Rep (UnifyError t k) x -> UnifyError t k #
Constraints (UnifyError t k) Binary => Binary (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods put :: UnifyError t k -> Put # get :: Get (UnifyError t k) # putList :: [UnifyError t k] -> Put #
Constraints (UnifyError t k) NFData => NFData (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods rnf :: UnifyError t k -> () #
Constraints (UnifyError t k) Pretty => Pretty (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error Methods pPrintPrec :: PrettyLevel -> Rational -> UnifyError t k -> Doc # pPrint :: UnifyError t k -> Doc # pPrintList :: PrettyLevel -> [UnifyError t k] -> Doc #
data KWitness (UnifyError t) n Source #
Instance details Defined in AST.Unify.Error data KWitness (UnifyError t) n where W_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness (UnifyError t) t E_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness t n -> KWitness (UnifyError t) n
type KNodesConstraint (UnifyError t) c Source #
Instance details Defined in AST.Unify.Error type KNodesConstraint (UnifyError t) c = (c t, KNodesConstraint t c)
type Rep (UnifyError t k) Source #
Instance details Defined in AST.Unify.Error type Rep (UnifyError t k) = D1 (MetaData "UnifyError" "AST.Unify.Error" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) ((C1 (MetaCons "SkolemUnified" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t)) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t))) :+: C1 (MetaCons "SkolemEscape" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # t)))) :+: (C1 (MetaCons "ConstraintsViolation" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k)) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TypeConstraintsOf t))) :+: (C1 (MetaCons "Occurs" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k)) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k))) :+: C1 (MetaCons "Mismatch" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k)) :: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (t k))))))

Exported only for SPECIALIZE pragmas

updateConstraints :: Unify m t => TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m () Source #

updateTermConstraints :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTermBody (UVarOf m)) t -> TypeConstraintsOf t -> m () Source #

updateTermConstraintsH :: Unify m t => Tree (WithConstraint (UVarOf m)) t -> m () Source #

unifyUTerms :: forall m t. Unify m t => Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t) Source #

unifyUnbound :: Unify m t => Tree (UVarOf m) t -> TypeConstraintsOf t -> Tree (UVarOf m) t -> Tree (UTerm (UVarOf m)) t -> m (Tree (UVarOf m) t) Source #