module Wingman.Judgements where import Control.Arrow import Control.Lens hiding (Context) import Data.Bool import Data.Char import Data.Coerce import Data.Generics.Product (field) import Data.Map (Map) import qualified Data.Map as M import Data.Maybe import Data.Set (Set) import qualified Data.Set as S import Development.IDE.Core.UseStale (Tracked, unTrack) import Development.IDE.GHC.Compat hiding (isTopLevel) import Development.IDE.Spans.LocalBindings import Wingman.GHC (algebraicTyCon, normalizeType) import Wingman.Judgements.Theta import Wingman.Types ------------------------------------------------------------------------------ -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType hypothesisFromBindings (unTrack -> span) (unTrack -> bs) = buildHypothesis $ getLocalScope bs span ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis. buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType buildHypothesis = Hypothesis . mapMaybe go where go (occName -> occ, t) | Just ty <- t , (h:_) <- occNameString occ , isAlpha h = Just $ HyInfo occ UserPrv $ CType ty | otherwise = Nothing ------------------------------------------------------------------------------ -- | Build a trivial hypothesis containing only a single name. The corresponding -- HyInfo has no provenance or type. hySingleton :: OccName -> Hypothesis () hySingleton n = Hypothesis . pure $ HyInfo n UserPrv () blacklistingDestruct :: Judgement -> Judgement blacklistingDestruct = field @"_jBlacklistDestruct" .~ True unwhitelistingSplit :: Judgement -> Judgement unwhitelistingSplit = field @"_jWhitelistSplit" .~ False isDestructBlacklisted :: Judgement -> Bool isDestructBlacklisted = _jBlacklistDestruct isSplitWhitelisted :: Judgement -> Bool isSplitWhitelisted = _jWhitelistSplit withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t ------------------------------------------------------------------------------ -- | Like 'withNewGoal' but allows you to modify the goal rather than replacing -- it. withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a withModifiedGoal f = field @"_jGoal" %~ f ------------------------------------------------------------------------------ -- | Add some new type equalities to the local judgement. withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement withNewCoercions ev j = let subst = allEvidenceToSubst mempty $ coerce ev in fmap (CType . substTyAddInScope subst . unCType) j & field @"j_coercion" %~ unionTCvSubst subst normalizeHypothesis :: Functor f => Context -> f CType -> f CType normalizeHypothesis = fmap . coerce . normalizeType normalizeJudgement :: Functor f => Context -> f CType -> f CType normalizeJudgement = normalizeHypothesis introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType -- NOTE(sandy): It's important that we put the new hypothesis terms first, -- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs -- after a previously-destructed term. introduce ctx hy = field @"_jHypothesis" %~ mappend (normalizeHypothesis ctx hy) ------------------------------------------------------------------------------ -- | Helper function for implementing functions which introduce new hypotheses. introduceHypothesis :: (Int -> Int -> Provenance) -- ^ A function from the total number of args and position of this arg -- to its provenance. -> [(OccName, a)] -> Hypothesis a introduceHypothesis f ns = Hypothesis $ zip [0..] ns <&> \(pos, (name, ty)) -> HyInfo name (f (length ns) pos) ty ------------------------------------------------------------------------------ -- | Introduce bindings in the context of a lamba. lambdaHypothesis :: Maybe OccName -- ^ The name of the top level function. For any other -- function, this should be 'Nothing'. -> [(OccName, a)] -> Hypothesis a lambdaHypothesis func = introduceHypothesis $ \count pos -> maybe UserPrv (\x -> TopLevelArgPrv x pos count) func ------------------------------------------------------------------------------ -- | Introduce a binding in a recursive context. recursiveHypothesis :: [(OccName, a)] -> Hypothesis a recursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv ------------------------------------------------------------------------------ -- | Introduce a binding in a recursive context. userHypothesis :: [(OccName, a)] -> Hypothesis a userHypothesis = introduceHypothesis $ const $ const UserPrv ------------------------------------------------------------------------------ -- | Check whether any of the given occnames are an ancestor of the term. hasPositionalAncestry :: 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 hasPositionalAncestry ancestors jdg name | not $ null ancestors = case name `elem` ancestors of True -> Just True False -> case M.lookup name $ jAncestryMap jdg of Just ancestry -> bool Nothing (Just False) $ any (flip S.member ancestry) ancestors Nothing -> Nothing | otherwise = Nothing ------------------------------------------------------------------------------ -- | Helper function for disallowing hypotheses that have the wrong ancestry. filterAncestry :: Foldable t => t OccName -> DisallowReason -> Judgement -> Judgement filterAncestry ancestry reason jdg = disallowing reason (M.keysSet $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg where go name _ = isNothing $ hasPositionalAncestry ancestry jdg name ------------------------------------------------------------------------------ -- | @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. filterPosition :: OccName -> Int -> Judgement -> Judgement filterPosition defn pos jdg = filterAncestry (findPositionVal jdg defn pos) (WrongBranch pos) jdg ------------------------------------------------------------------------------ -- | Helper function for determining the ancestry list for 'filterPosition'. findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName findPositionVal jdg defn pos = listToMaybe $ do -- It's important to inspect the entire hypothesis here, as we need to trace -- ancstry through potentially disallowed terms in the hypothesis. (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg case hi_provenance hi of TopLevelArgPrv defn' pos' _ | defn == defn' , pos == pos' -> pure name PatternMatchPrv pv | pv_scrutinee pv == Just defn , pv_position pv == pos -> pure name _ -> [] ------------------------------------------------------------------------------ -- | Helper function for determining the ancestry list for -- 'filterSameTypeFromOtherPositions'. findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName] findDconPositionVals jdg dcon pos = do (name, hi) <- M.toList $ hyByName $ jHypothesis jdg case hi_provenance hi of PatternMatchPrv pv | pv_datacon pv == Uniquely dcon , pv_position pv == pos -> pure name _ -> [] ------------------------------------------------------------------------------ -- | 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. filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions dcon pos jdg = let hy = hyByName . jHypothesis $ filterAncestry (findDconPositionVals jdg dcon pos) (WrongBranch pos) jdg tys = S.fromList $ hi_type <$> M.elems hy to_remove = M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg) M.\\ hy in disallowing Shadowed (M.keysSet to_remove) jdg ------------------------------------------------------------------------------ -- | Return the ancestry of a 'PatVal', or 'mempty' otherwise. getAncestry :: Judgement' a -> OccName -> Set OccName getAncestry jdg name = maybe mempty pv_ancestry . M.lookup name $ jPatHypothesis jdg jAncestryMap :: Judgement' a -> Map OccName (Set OccName) jAncestryMap jdg = M.map pv_ancestry (jPatHypothesis jdg) provAncestryOf :: Provenance -> Set OccName provAncestryOf (TopLevelArgPrv o _ _) = S.singleton o provAncestryOf (PatternMatchPrv (PatVal mo so _ _)) = maybe mempty S.singleton mo <> so provAncestryOf (ClassMethodPrv _) = mempty provAncestryOf UserPrv = mempty provAncestryOf RecursivePrv = mempty provAncestryOf ImportPrv = mempty provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2 ------------------------------------------------------------------------------ -- TODO(sandy): THIS THING IS A BIG BIG HACK -- -- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined -- (eg, we might be in a where block). The head of this list is not guaranteed -- to be the one we're interested in. extremelyStupid__definingFunction :: Context -> OccName extremelyStupid__definingFunction = fst . head . ctxDefiningFuncs patternHypothesis :: Maybe OccName -> ConLike -> Judgement' a -> [(OccName, a)] -> Hypothesis a patternHypothesis scrutinee dc jdg = introduceHypothesis $ \_ pos -> PatternMatchPrv $ PatVal scrutinee (maybe mempty (\scrut -> S.singleton scrut <> getAncestry jdg scrut) scrutinee) (Uniquely dc) pos ------------------------------------------------------------------------------ -- | Prevent some occnames from being used in the hypothesis. This will hide -- them from 'jHypothesis', but not from 'jEntireHypothesis'. disallowing :: DisallowReason -> S.Set OccName -> Judgement' a -> Judgement' a disallowing reason ns = field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi -> case S.member (hi_name hi) ns of True -> overProvenance (DisallowedPrv reason) hi False -> hi ) ------------------------------------------------------------------------------ -- | The hypothesis, consisting of local terms and the ambient environment -- (impors and class methods.) Hides disallowed values. jHypothesis :: Judgement' a -> Hypothesis a jHypothesis = Hypothesis . filter (not . isDisallowed . hi_provenance) . unHypothesis . jEntireHypothesis ------------------------------------------------------------------------------ -- | The whole hypothesis, including things disallowed. jEntireHypothesis :: Judgement' a -> Hypothesis a jEntireHypothesis = _jHypothesis ------------------------------------------------------------------------------ -- | Just the local hypothesis. jLocalHypothesis :: Judgement' a -> Hypothesis a jLocalHypothesis = Hypothesis . filter (isLocalHypothesis . hi_provenance) . unHypothesis . jHypothesis ------------------------------------------------------------------------------ -- | Filter elements from the hypothesis hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a hyFilter f = Hypothesis . filter f . unHypothesis ------------------------------------------------------------------------------ -- | 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. jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType] jAcceptableDestructTargets = filter (isJust . algebraicTyCon . unCType . hi_type) . takeWhile (not . isAlreadyDestructed . hi_provenance) . unHypothesis . jEntireHypothesis ------------------------------------------------------------------------------ -- | If we're in a top hole, the name of the defining function. isTopHole :: Context -> Judgement' a -> Maybe OccName isTopHole ctx = bool Nothing (Just $ extremelyStupid__definingFunction ctx) . _jIsTopHole unsetIsTopHole :: Judgement' a -> Judgement' a unsetIsTopHole = field @"_jIsTopHole" .~ False ------------------------------------------------------------------------------ -- | What names are currently in scope in the hypothesis? hyNamesInScope :: Hypothesis a -> Set OccName hyNamesInScope = M.keysSet . hyByName ------------------------------------------------------------------------------ -- | Are there any top-level function argument bindings in this judgement? jHasBoundArgs :: Judgement' a -> Bool jHasBoundArgs = any (isTopLevel . hi_provenance) . unHypothesis . jLocalHypothesis jNeedsToBindArgs :: Judgement' CType -> Bool jNeedsToBindArgs = isFunTy . unCType . jGoal ------------------------------------------------------------------------------ -- | Fold a hypothesis into a single mapping from name to info. This -- unavoidably will cause duplicate names (things like methods) to shadow one -- another. hyByName :: Hypothesis a -> Map OccName (HyInfo a) hyByName = M.fromList . fmap (hi_name &&& id) . unHypothesis ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName PatVal jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . hyByName . jHypothesis getPatVal :: Provenance-> Maybe PatVal getPatVal prov = case prov of PatternMatchPrv pv -> Just pv _ -> Nothing jGoal :: Judgement' a -> a jGoal = _jGoal substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce mkFirstJudgement :: Context -> Hypothesis CType -> Bool -- ^ are we in the top level rhs hole? -> Type -> Judgement' CType mkFirstJudgement ctx hy top goal = normalizeJudgement ctx $ Judgement { _jHypothesis = hy , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jIsTopHole = top , _jGoal = CType goal , j_coercion = emptyTCvSubst } ------------------------------------------------------------------------------ -- | Is this a top level function binding? isTopLevel :: Provenance -> Bool isTopLevel TopLevelArgPrv{} = True isTopLevel _ = False ------------------------------------------------------------------------------ -- | Is this a local function argument, pattern match or user val? isLocalHypothesis :: Provenance -> Bool isLocalHypothesis UserPrv{} = True isLocalHypothesis PatternMatchPrv{} = True isLocalHypothesis TopLevelArgPrv{} = True isLocalHypothesis _ = False ------------------------------------------------------------------------------ -- | Is this a pattern match? isPatternMatch :: Provenance -> Bool isPatternMatch PatternMatchPrv{} = True isPatternMatch _ = False ------------------------------------------------------------------------------ -- | Was this term ever disallowed? isDisallowed :: Provenance -> Bool isDisallowed DisallowedPrv{} = True isDisallowed _ = False ------------------------------------------------------------------------------ -- | Has this term already been disallowed? isAlreadyDestructed :: Provenance -> Bool isAlreadyDestructed (DisallowedPrv AlreadyDestructed _) = True isAlreadyDestructed _ = False ------------------------------------------------------------------------------ -- | Eliminates 'DisallowedPrv' provenances. expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv expandDisallowed prv = prv