| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Wingman.Judgements
Synopsis
- hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType
- buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
- hySingleton :: OccName -> Hypothesis ()
- blacklistingDestruct :: Judgement -> Judgement
- unwhitelistingSplit :: Judgement -> Judgement
- isDestructBlacklisted :: Judgement -> Bool
- isSplitWhitelisted :: Judgement -> Bool
- withNewGoal :: a -> Judgement' a -> Judgement' a
- withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
- withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement
- normalizeHypothesis :: Functor f => Context -> f CType -> f CType
- normalizeJudgement :: Functor f => Context -> f CType -> f CType
- introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType
- introduceHypothesis :: (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
- lambdaHypothesis :: Maybe OccName -> [(OccName, a)] -> Hypothesis a
- recursiveHypothesis :: [(OccName, a)] -> Hypothesis a
- userHypothesis :: [(OccName, a)] -> Hypothesis a
- hasPositionalAncestry :: Foldable t => t OccName -> Judgement -> OccName -> Maybe Bool
- filterAncestry :: Foldable t => t OccName -> DisallowReason -> Judgement -> Judgement
- filterPosition :: OccName -> Int -> Judgement -> Judgement
- findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
- findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]
- filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement
- getAncestry :: Judgement' a -> OccName -> Set OccName
- jAncestryMap :: Judgement' a -> Map OccName (Set OccName)
- provAncestryOf :: Provenance -> Set OccName
- extremelyStupid__definingFunction :: Context -> OccName
- patternHypothesis :: Maybe OccName -> ConLike -> Judgement' a -> [(OccName, a)] -> Hypothesis a
- disallowing :: DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
- jHypothesis :: Judgement' a -> Hypothesis a
- jEntireHypothesis :: Judgement' a -> Hypothesis a
- jLocalHypothesis :: Judgement' a -> Hypothesis a
- hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
- jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]
- isTopHole :: Context -> Judgement' a -> Maybe OccName
- unsetIsTopHole :: Judgement' a -> Judgement' a
- hyNamesInScope :: Hypothesis a -> Set OccName
- jHasBoundArgs :: Judgement' a -> Bool
- jNeedsToBindArgs :: Judgement' CType -> Bool
- hyByName :: Hypothesis a -> Map OccName (HyInfo a)
- jPatHypothesis :: Judgement' a -> Map OccName PatVal
- getPatVal :: Provenance -> Maybe PatVal
- jGoal :: Judgement' a -> a
- substJdg :: TCvSubst -> Judgement -> Judgement
- mkFirstJudgement :: Context -> Hypothesis CType -> Bool -> Type -> Judgement' CType
- isTopLevel :: Provenance -> Bool
- isLocalHypothesis :: Provenance -> Bool
- isPatternMatch :: Provenance -> Bool
- isDisallowed :: Provenance -> Bool
- isAlreadyDestructed :: Provenance -> Bool
- expandDisallowed :: Provenance -> Provenance
Documentation
hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType Source #
buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType Source #
Convert a Set Id into a hypothesis.
hySingleton :: OccName -> Hypothesis () Source #
Build a trivial hypothesis containing only a single name. The corresponding HyInfo has no provenance or type.
isSplitWhitelisted :: Judgement -> Bool Source #
withNewGoal :: a -> Judgement' a -> Judgement' a Source #
withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a Source #
Like withNewGoal but allows you to modify the goal rather than replacing
it.
withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement Source #
Add some new type equalities to the local judgement.
introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType Source #
Arguments
| :: (Int -> Int -> Provenance) | A function from the total number of args and position of this arg to its provenance. |
| -> [(OccName, a)] | |
| -> Hypothesis a |
Helper function for implementing functions which introduce new hypotheses.
Arguments
| :: Maybe OccName | The name of the top level function. For any other
function, this should be |
| -> [(OccName, a)] | |
| -> Hypothesis a |
Introduce bindings in the context of a lamba.
recursiveHypothesis :: [(OccName, a)] -> Hypothesis a Source #
Introduce a binding in a recursive context.
userHypothesis :: [(OccName, a)] -> Hypothesis a Source #
Introduce a binding in a recursive context.
hasPositionalAncestry Source #
Arguments
| :: Foldable t | |
| => t OccName | Desired ancestors. |
| -> Judgement | |
| -> OccName | Potential child |
| -> Maybe Bool | Just True if the result is the oldest positional ancestor just false if it's a descendent otherwise nothing |
Check whether any of the given occnames are an ancestor of the term.
filterAncestry :: Foldable t => t OccName -> DisallowReason -> Judgement -> Judgement Source #
Helper function for disallowing hypotheses that have the wrong ancestry.
filterPosition :: OccName -> Int -> Judgement -> Judgement Source #
filter defn pos removes any hypotheses which are bound in defn to
a position other than pos. Any terms whose ancestry doesn't include defn
remain.
findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName Source #
Helper function for determining the ancestry list for filterPosition.
findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName] Source #
Helper function for determining the ancestry list for
filterSameTypeFromOtherPositions.
filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement Source #
Disallow any hypotheses who have the same type as anything bound by the
given position for the datacon. Used to ensure recursive functions like
fmap preserve the relative ordering of their arguments by eliminating any
other term which might match.
getAncestry :: Judgement' a -> OccName -> Set OccName Source #
jAncestryMap :: Judgement' a -> Map OccName (Set OccName) Source #
provAncestryOf :: Provenance -> Set OccName Source #
patternHypothesis :: Maybe OccName -> ConLike -> Judgement' a -> [(OccName, a)] -> Hypothesis a Source #
disallowing :: DisallowReason -> Set OccName -> Judgement' a -> Judgement' a Source #
Prevent some occnames from being used in the hypothesis. This will hide
them from jHypothesis, but not from jEntireHypothesis.
jHypothesis :: Judgement' a -> Hypothesis a Source #
The hypothesis, consisting of local terms and the ambient environment (impors and class methods.) Hides disallowed values.
jEntireHypothesis :: Judgement' a -> Hypothesis a Source #
The whole hypothesis, including things disallowed.
jLocalHypothesis :: Judgement' a -> Hypothesis a Source #
Just the local hypothesis.
hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a Source #
Filter elements from the hypothesis
jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType] Source #
Given a judgment, return the hypotheses that are acceptable to destruct.
We use the ordering of the hypothesis for this purpose. Since new bindings are always inserted at the beginning, we can impose a canonical ordering on which order to try destructs by what order they are introduced --- stopping at the first one we've already destructed.
isTopHole :: Context -> Judgement' a -> Maybe OccName Source #
If we're in a top hole, the name of the defining function.
unsetIsTopHole :: Judgement' a -> Judgement' a Source #
hyNamesInScope :: Hypothesis a -> Set OccName Source #
What names are currently in scope in the hypothesis?
jHasBoundArgs :: Judgement' a -> Bool Source #
Are there any top-level function argument bindings in this judgement?
jNeedsToBindArgs :: Judgement' CType -> Bool Source #
hyByName :: Hypothesis a -> Map OccName (HyInfo a) Source #
Fold a hypothesis into a single mapping from name to info. This unavoidably will cause duplicate names (things like methods) to shadow one another.
jPatHypothesis :: Judgement' a -> Map OccName PatVal Source #
Only the hypothesis members which are pattern vals
jGoal :: Judgement' a -> a Source #
Arguments
| :: Context | |
| -> Hypothesis CType | |
| -> Bool | are we in the top level rhs hole? |
| -> Type | |
| -> Judgement' CType |
isTopLevel :: Provenance -> Bool Source #
Is this a top level function binding?
isLocalHypothesis :: Provenance -> Bool Source #
Is this a local function argument, pattern match or user val?
isPatternMatch :: Provenance -> Bool Source #
Is this a pattern match?
isDisallowed :: Provenance -> Bool Source #
Was this term ever disallowed?
isAlreadyDestructed :: Provenance -> Bool Source #
Has this term already been disallowed?
expandDisallowed :: Provenance -> Provenance Source #
Eliminates DisallowedPrv provenances.