hls-tactics-plugin-1.6.1.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.Judgements

Synopsis

Documentation

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

Given a SrcSpan and a Bindings, create a hypothesis.

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.

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.

introduceHypothesis 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.

lambdaHypothesis Source #

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 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 #

Return the ancestry of a PatVal, or mempty otherwise.

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.

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?

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

mkFirstJudgement 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?