Safe Haskell	None
Language	Haskell2010

AST.Unify.Term

Description

Unification terms.

These represent the known state of a unification variable.

Synopsis

data UTerm v ast
- = UUnbound (TypeConstraintsOf (GetKnot ast))
- | USkolem (TypeConstraintsOf (GetKnot ast))
- | UToVar (v ast)
- | UTerm (UTermBody v ast)
- | UInstantiated (v ast)
- | UResolving (UTermBody v ast)
- | UResolved (Pure ast)
- | UConverted 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 = UTermBody {
- _uConstraints :: TypeConstraintsOf (GetKnot ast)
- _uBody :: 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))

Documentation

data UTerm v ast Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in AST.Unify.Term Methods rnf :: UTerm v ast -> () #
type Rep (UTerm v ast) Source #
Instance details 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)) Source #

_USkolem :: forall v ast. Prism' (UTerm v ast) (TypeConstraintsOf (GetKnot ast)) Source #

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

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

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

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

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

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

data UTermBody v ast Source #

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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in AST.Unify.Term Methods rnf :: UTermBody v ast -> () #
type Rep (UTermBody v ast) Source #
Instance details 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) Source #

uConstraints :: forall v ast. Lens' (UTermBody v ast) (TypeConstraintsOf (GetKnot ast)) Source #