| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Unison.Typechecker.Context.Structure
Synopsis
- data Element v loc
- variable :: Element v loc -> v
- data Info v loc = Info {
- boundExistentialVars :: Set v
- solvedExistentials :: Map v (Monotype v loc)
- boundUniversalVars :: Set v
- termVarAnnotations :: Map v (loc, Type v loc)
- allBoundVars :: Set v
- freeUniversalVars :: Set v
- freeExistentialVars :: Set v
- shadowedVars :: Set v
- recorded :: Map v (Recorded loc, Type v loc)
- unsolvedExistentials :: Ord v => Info v loc -> Set v
- newtype Context v loc = Context (CtxSegment v loc)
- context0 :: Ord v => Context v loc
- type CtxSegment v loc = FingerTree (Info v loc) (Element v loc)
- (|>) :: Measured v a => FingerTree v a -> a -> FingerTree v a
- (<|) :: Measured v a => a -> FingerTree v a -> FingerTree v a
- fmap' :: (Measured v1 a1, Measured v2 a2) => (a1 -> a2) -> FingerTree v1 a1 -> FingerTree v2 a2
- data BadContext
- validateSegment :: Ord v => CtxSegment v loc -> Either BadContext (Context v loc)
- data SearchResult v a
- = Position !(FingerTree v a) a !(FingerTree v a)
- | OnLeft
- | OnRight
- | Nowhere
- focusProblem :: Measured v e => (v -> Bool) -> FingerTree v e -> SearchResult v e
- culprit :: Ord v => CtxSegment v loc -> BadContext -> (CtxSegment v loc, Element v loc)
- info :: (Ord v, Measured (Info v loc) c) => c -> Info v loc
- filter :: Var v => (Element v loc -> Bool) -> CtxSegment v loc -> CtxSegment v loc
- partition :: Var v => (Element v loc -> Either (Element v loc) (Element v loc)) -> CtxSegment v loc -> (CtxSegment v loc, CtxSegment v loc)
- apply :: (Var v, Measured (Info v loc) c) => c -> Type v loc -> Type v loc
- fromList :: Measured v a => [a] -> FingerTree v a
- mapMaybe :: (Element v loc -> Maybe b) -> CtxSegment v loc -> [b]
- single :: Var v => Element v loc -> CtxSegment v loc
- split :: Ord v => v -> Context v loc -> Maybe (Context v loc, Element v loc, CtxSegment v loc)
- splitSeg :: Ord v => v -> CtxSegment v loc -> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
- surround :: Ord v => CtxSegment v loc -> Element v loc -> CtxSegment v loc -> CtxSegment v loc
Documentation
Elements of an ordered algorithmic context. A context is a sequence
of Elements (here represented as a finger tree), but not every
sequence represents a valid context. A context is only valid if every
type that occurs in the context is well scoped with regard to the
previous variable bindings in the context.
We will refer to invalid trees as 'context segments' since they can be prefixed to become part of a valid context. Keeping track of the same context information for _every_ segment is important to avoiding some performance problems with a more naive implementation.
Constructors
| Var (TypeVar v loc) | A variable declaration |
| Solved (Blank loc) v (Monotype v loc) |
|
| Ann v loc (Type v loc) |
|
| Marker v | used for scoping |
Aggregate context (segment) information, built up from Elements.
$sel:boundExistentialVars:Info is the set of existential variables that are
known to be 'in scope' due to the context segment.
$sel:solvedExistentials:Info is a mapping of existential variables to their
solutions in the segment.
$sel:boundUniversalVars:Info is the set of universal variables that are known
to be 'in scope' due to the context segment.
$sel:termVarAnnotations:Info is a mapping of term variables to their type.
$sel:allBoundVars:Info contains all the variables 'in scope' due to the
segment. Primarily used for freshening.
`freeUniversal/ExistentialVars` contains all the variables that occur
_free_ in types in the segment. This means that they are _not_ bound
in an Element previous to the one that the type occurs in.
$sel:shadowedVars:Info contains variables that occur _multiple_ times in the
segment, and thus the latter shadows the former.
$sel:recorded:Info tracks certain annotated elements.
A context segment is a well formed context if `free*Vars` and
$sel:shadowedVars:Info are both empty.
Note: the fields here are intentionally lazy. In situations where there is heavy context manipulation, this seems to actually be faster, probably because the info is not actually used all of the time, and any fields that are strict are actually demanded by use of every other field in the info, regardless of whether the strict field ends up needed.
Constructors
| Info | |
Fields
| |
unsolvedExistentials :: Ord v => Info v loc -> Set v Source #
Gets the _unsolved_ existential variables of a context info.
newtype Context v loc Source #
Constructors
| Context (CtxSegment v loc) |
type CtxSegment v loc = FingerTree (Info v loc) (Element v loc) Source #
(|>) :: Measured v a => FingerTree v a -> a -> FingerTree v a infixl 5 #
O(1). Add an element to the right end of a sequence. Mnemonic: a triangle with the single element at the pointy end.
(<|) :: Measured v a => a -> FingerTree v a -> FingerTree v a infixr 5 #
O(1). Add an element to the left end of a sequence. Mnemonic: a triangle with the single element at the pointy end.
fmap' :: (Measured v1 a1, Measured v2 a2) => (a1 -> a2) -> FingerTree v1 a1 -> FingerTree v2 a2 #
Like fmap, but with constraints on the element types.
validateSegment :: Ord v => CtxSegment v loc -> Either BadContext (Context v loc) Source #
Checks that a context segment forms a valid context. If so, then the proper context is yielded. Otherwise an indication of what is wrong with the segment is returned.
data SearchResult v a #
A result of search, attempting to find a point where a predicate
on splits of the sequence changes from False to True.
Since: fingertree-0.1.2.0
Constructors
| Position !(FingerTree v a) a !(FingerTree v a) | A tree opened at a particular element: the prefix to the left, the element, and the suffix to the right. |
| OnLeft | A position to the left of the sequence, indicating that the
predicate is |
| OnRight | A position to the right of the sequence, indicating that the
predicate is |
| Nowhere | No position in the tree, returned if the predicate is |
Instances
focusProblem :: Measured v e => (v -> Bool) -> FingerTree v e -> SearchResult v e Source #
culprit :: Ord v => CtxSegment v loc -> BadContext -> (CtxSegment v loc, Element v loc) Source #
info :: (Ord v, Measured (Info v loc) c) => c -> Info v loc Source #
Return the aggregate Info associated to the context.
filter :: Var v => (Element v loc -> Bool) -> CtxSegment v loc -> CtxSegment v loc Source #
partition :: Var v => (Element v loc -> Either (Element v loc) (Element v loc)) -> CtxSegment v loc -> (CtxSegment v loc, CtxSegment v loc) Source #
apply :: (Var v, Measured (Info v loc) c) => c -> Type v loc -> Type v loc Source #
Replace any existentials with their solution in the context
fromList :: Measured v a => [a] -> FingerTree v a #
mapMaybe :: (Element v loc -> Maybe b) -> CtxSegment v loc -> [b] Source #
Applies a partial mapping to a context segment, resulting in a list.
split :: Ord v => v -> Context v loc -> Maybe (Context v loc, Element v loc, CtxSegment v loc) Source #
splitSeg :: Ord v => v -> CtxSegment v loc -> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc) Source #
surround :: Ord v => CtxSegment v loc -> Element v loc -> CtxSegment v loc -> CtxSegment v loc Source #