Wingman.Judgements

Documentation

hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType

Given a SrcSpan and a Bindings, create a hypothesis.

buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType

Convert a Set Id into a hypothesis.

hySingleton :: OccName -> Hypothesis ()

Build a trivial hypothesis containing only a single name. The corresponding HyInfo has no provenance or type.

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

Like withNewGoal but allows you to modify the goal rather than replacing it.

withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement

Add some new type equalities to the local 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

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.

lambdaHypothesis

Arguments

:: Maybe OccName

The name of the top level function. For any other function, this should be Nothing.

-> [(OccName, a)]

-> Hypothesis a

Introduce bindings in the context of a lamba.

recursiveHypothesis :: [(OccName, a)] -> Hypothesis a

Introduce a binding in a recursive context.

userHypothesis :: [(OccName, a)] -> Hypothesis a

Introduce a binding in a recursive context.

hasPositionalAncestry

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

Helper function for disallowing hypotheses that have the wrong ancestry.

filterPosition :: OccName -> Int -> Judgement -> Judgement

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

Helper function for determining the ancestry list for filterPosition.

findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]

Helper function for determining the ancestry list for filterSameTypeFromOtherPositions.

filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement

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

Return the ancestry of a PatVal, or mempty otherwise.

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

Prevent some occnames from being used in the hypothesis. This will hide them from jHypothesis, but not from jEntireHypothesis.

jHypothesis :: Judgement' a -> Hypothesis a

The hypothesis, consisting of local terms and the ambient environment (impors and class methods.) Hides disallowed values.

jEntireHypothesis :: Judgement' a -> Hypothesis a

The whole hypothesis, including things disallowed.

jLocalHypothesis :: Judgement' a -> Hypothesis a

Just the local hypothesis.

hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a

Filter elements from the hypothesis

jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]

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

If we're in a top hole, the name of the defining function.

unsetIsTopHole :: Judgement' a -> Judgement' a

hyNamesInScope :: Hypothesis a -> Set OccName

What names are currently in scope in the hypothesis?

jHasBoundArgs :: Judgement' a -> Bool

Are there any top-level function argument bindings in this judgement?

jNeedsToBindArgs :: Judgement' CType -> Bool

hyByName :: Hypothesis a -> Map OccName (HyInfo a)

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

Only the hypothesis members which are pattern vals

getPatVal :: Provenance -> Maybe PatVal

jGoal :: Judgement' a -> a

substJdg :: TCvSubst -> Judgement -> Judgement

mkFirstJudgement

Arguments

:: Context

-> Hypothesis CType

-> Bool

are we in the top level rhs hole?

-> Type

-> Judgement' CType

isTopLevel :: Provenance -> Bool

Is this a top level function binding?

isLocalHypothesis :: Provenance -> Bool

Is this a local function argument, pattern match or user val?

isPatternMatch :: Provenance -> Bool

Is this a pattern match?

isDisallowed :: Provenance -> Bool

Was this term ever disallowed?

isAlreadyDestructed :: Provenance -> Bool

Has this term already been disallowed?

expandDisallowed :: Provenance -> Provenance

Eliminates DisallowedPrv provenances.