Hyper.Unify.Term

Unification terms.

These represent the known state of a unification variable.

Documentation

data UTerm v ast

A unification term pointed by a unification variable

Constructors

UUnbound (TypeConstraintsOf (GetHyperType ast))

Unbound variable with at least the given constraints

USkolem (TypeConstraintsOf (GetHyperType ast))

A variable bound by a rigid quantified variable with *exactly* the given constraints

UToVar (v ast)

Unified with another variable (union-find)

UTerm (UTermBody v ast)

Known type term with unification variables as children

UInstantiated (v ast)

Temporary state during instantiation indicating which fresh unification variable a skolem is mapped to

UResolving (UTermBody v ast)

Temporary state while unification term is being traversed, if it occurs inside itself (detected via state still being UResolving), then the type is an infinite type

UResolved (Pure ast)

Final resolved state. applyBindings resolved to this expression (allowing caching/sharing)

UConverted Int

Temporary state used in Hyper.Unify.Binding.ST.Save while converting to a pure binding

Instances

Constraints (UTerm v ast) Eq => Eq (UTerm v ast)

Defined in Hyper.Unify.Term

Methods

(==) :: UTerm v ast -> UTerm v ast -> Bool

(/=) :: UTerm v ast -> UTerm v ast -> Bool

Constraints (UTerm v ast) Ord => Ord (UTerm v ast)

Defined in Hyper.Unify.Term

Methods

compare :: UTerm v ast -> UTerm v ast -> Ordering

(<) :: UTerm v ast -> UTerm v ast -> Bool

(<=) :: UTerm v ast -> UTerm v ast -> Bool

(>) :: UTerm v ast -> UTerm v ast -> Bool

(>=) :: UTerm v ast -> UTerm v ast -> Bool

max :: UTerm v ast -> UTerm v ast -> UTerm v ast

min :: UTerm v ast -> UTerm v ast -> UTerm v ast

Constraints (UTerm v ast) Show => Show (UTerm v ast)

Defined in Hyper.Unify.Term

Methods

showsPrec :: Int -> UTerm v ast -> ShowS

show :: UTerm v ast -> String

showList :: [UTerm v ast] -> ShowS

Generic (UTerm v ast)

Defined in Hyper.Unify.Term

Associated Types

type Rep (UTerm v ast) :: Type -> Type

Methods

from :: UTerm v ast -> Rep (UTerm v ast) x

to :: Rep (UTerm v ast) x -> UTerm v ast

Constraints (UTerm v ast) Binary => Binary (UTerm v ast)

Defined in Hyper.Unify.Term

Methods

put :: UTerm v ast -> Put

get :: Get (UTerm v ast)

putList :: [UTerm v ast] -> Put

Constraints (UTerm v ast) NFData => NFData (UTerm v ast)

Defined in Hyper.Unify.Term

Methods

rnf :: UTerm v ast -> ()

type Rep (UTerm v ast)

Defined in Hyper.Unify.Term

type Rep (UTerm v ast) = D1 ('MetaData "UTerm" "Hyper.Unify.Term" "hypertypes-0.1.0.2-GDiSRF0EwgQ6Mkx3yytlTL" 'False) (((C1 ('MetaCons "UUnbound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeConstraintsOf (GetHyperType ast)))) :+: C1 ('MetaCons "USkolem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeConstraintsOf (GetHyperType ast))))) :+: (C1 ('MetaCons "UToVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (v ast))) :+: C1 ('MetaCons "UTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UTermBody v ast))))) :+: ((C1 ('MetaCons "UInstantiated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (v ast))) :+: C1 ('MetaCons "UResolving" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (UTermBody v ast)))) :+: (C1 ('MetaCons "UResolved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pure ast))) :+: C1 ('MetaCons "UConverted" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))))

_UUnbound :: forall v ast. Prism' (UTerm v ast) (TypeConstraintsOf (GetHyperType ast))

_USkolem :: forall v ast. Prism' (UTerm v ast) (TypeConstraintsOf (GetHyperType ast))

_UToVar :: forall v ast. Prism' (UTerm v ast) (v ast)

_UTerm :: forall v ast. Prism' (UTerm v ast) (UTermBody v ast)

_UInstantiated :: forall v ast. Prism' (UTerm v ast) (v ast)

_UResolving :: forall v ast. Prism' (UTerm v ast) (UTermBody v ast)

_UResolved :: forall v ast. Prism' (UTerm v ast) (Pure ast)

_UConverted :: forall v ast. Prism' (UTerm v ast) Int

data UTermBody v ast

A unification term with a known body

Constructors

UTermBody

Fields

• _uConstraints :: TypeConstraintsOf (GetHyperType ast)
• _uBody :: ast :# v

Instances

Constraints (UTermBody v ast) Eq => Eq (UTermBody v ast)

Defined in Hyper.Unify.Term

Methods

(==) :: UTermBody v ast -> UTermBody v ast -> Bool

(/=) :: UTermBody v ast -> UTermBody v ast -> Bool

Constraints (UTermBody v ast) Ord => Ord (UTermBody v ast)

Defined in Hyper.Unify.Term

Methods

compare :: UTermBody v ast -> UTermBody v ast -> Ordering

(<) :: UTermBody v ast -> UTermBody v ast -> Bool

(<=) :: UTermBody v ast -> UTermBody v ast -> Bool

(>) :: UTermBody v ast -> UTermBody v ast -> Bool

(>=) :: UTermBody v ast -> UTermBody v ast -> Bool

max :: UTermBody v ast -> UTermBody v ast -> UTermBody v ast

min :: UTermBody v ast -> UTermBody v ast -> UTermBody v ast

Constraints (UTermBody v ast) Show => Show (UTermBody v ast)

Defined in Hyper.Unify.Term

Methods

showsPrec :: Int -> UTermBody v ast -> ShowS

show :: UTermBody v ast -> String

showList :: [UTermBody v ast] -> ShowS

Generic (UTermBody v ast)

Defined in Hyper.Unify.Term

Associated Types

type Rep (UTermBody v ast) :: Type -> Type

Methods

from :: UTermBody v ast -> Rep (UTermBody v ast) x

to :: Rep (UTermBody v ast) x -> UTermBody v ast

Constraints (UTermBody v ast) Binary => Binary (UTermBody v ast)

Defined in Hyper.Unify.Term

Methods

put :: UTermBody v ast -> Put

get :: Get (UTermBody v ast)

putList :: [UTermBody v ast] -> Put

Constraints (UTermBody v ast) NFData => NFData (UTermBody v ast)

Defined in Hyper.Unify.Term

Methods

rnf :: UTermBody v ast -> ()

type Rep (UTermBody v ast)

Defined in Hyper.Unify.Term

type Rep (UTermBody v ast) = D1 ('MetaData "UTermBody" "Hyper.Unify.Term" "hypertypes-0.1.0.2-GDiSRF0EwgQ6Mkx3yytlTL" 'False) (C1 ('MetaCons "UTermBody" 'PrefixI 'True) (S1 ('MetaSel ('Just "_uConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeConstraintsOf (GetHyperType ast))) :*: S1 ('MetaSel ('Just "_uBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ast :# v))))

uBody :: forall v ast v. Lens (UTermBody v ast) (UTermBody v ast) ((:#) ast v) ((:#) ast v)

uConstraints :: forall v ast. Lens' (UTermBody v ast) (TypeConstraintsOf (GetHyperType ast))