DDC.Core.Check.TaggedClosure

Documentation

data TaggedClosure n

A closure-term tagged with the bound variable that the term is due to.

Constructors

GBoundVal (Bound n) (TypeSum n)

Term due to a free value variable.

GBoundRgnVar (Bound n)

Term due to a free region variable.

GBoundRgnCon (Bound n)

Term due to a region handle.

Instances

LowerT TaggedClosure

Eq n => Eq (TaggedClosure n)

Ord n => Ord (TaggedClosure n)

Show n => Show (TaggedClosure n)

(Eq n, Pretty n) => Pretty (TaggedClosure n)

closureOfTagged :: TaggedClosure n -> Closure n

Convert a tagged clousure to a regular closure by dropping the tag variables.

closureOfTaggedSet :: Ord n => Set (TaggedClosure n) -> Closure n

Convert a set of tagged closures to a regular closure by dropping the tag variables.

taggedClosureOfValBound :: (Ord n, Pretty n) => Bound n -> TaggedClosure n

Yield the tagged closure of a value variable.

taggedClosureOfTyArg :: (Ord n, Pretty n) => Type n -> Set (TaggedClosure n)

Yield the tagged closure of a type argument.

taggedClosureOfWeakClo :: (Ord n, Pretty n) => Closure n -> Maybe (Set (TaggedClosure n))

Convert the closure provided as a weakclo to tagged form. Only terms of form `Use r` can be converted.

maskFromTaggedSet :: Ord n => TypeSum n -> Set (TaggedClosure n) -> Set (TaggedClosure n)

Mask a closure term from a tagged closure.

This is used for the forget cast.

cutTaggedClosureX :: (Eq n, Ord n) => Bind n -> TaggedClosure n -> Maybe (TaggedClosure n)

Cut the terms due to the outermost binder from a tagged closure.

cutTaggedClosureXs :: (Eq n, Ord n) => [Bind n] -> TaggedClosure n -> Maybe (TaggedClosure n)

Like cutTaggedClosureX but cut terms due to several binders.

cutTaggedClosureT :: (Eq n, Ord n) => Bind n -> TaggedClosure n -> Maybe (TaggedClosure n)

Cut the terms due to the outermost binder from a tagged closure.