AST.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 (GetKnot ast))

Unbound variable with at least the given constraints

USkolem (TypeConstraintsOf (GetKnot 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 AST.Unify.Binding.ST.Save while converting to a pure binding

Instances

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

Defined in AST.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 AST.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 AST.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 AST.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 AST.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 AST.Unify.Term

Methods

rnf :: UTerm v ast -> ()

type Rep (UTerm v ast)

Defined in AST.Unify.Term

type Rep (UTerm v ast) = D1 (MetaData "UTerm" "AST.Unify.Term" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (((C1 (MetaCons "UUnbound" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TypeConstraintsOf (GetKnot ast)))) :+: C1 (MetaCons "USkolem" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TypeConstraintsOf (GetKnot 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 (GetKnot ast))

_USkolem :: forall v ast. Prism' (UTerm v ast) (TypeConstraintsOf (GetKnot 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 (GetKnot ast)
• _uBody :: ast # v

Instances

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

Defined in AST.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 AST.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 AST.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 AST.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 AST.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 AST.Unify.Term

Methods

rnf :: UTermBody v ast -> ()

type Rep (UTermBody v ast)

Defined in AST.Unify.Term

type Rep (UTermBody v ast) = D1 (MetaData "UTermBody" "AST.Unify.Term" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (C1 (MetaCons "UTermBody" PrefixI True) (S1 (MetaSel (Just "_uConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TypeConstraintsOf (GetKnot 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 (GetKnot ast))