From 29cb0ad2477a7f06540c74a9b2fef8e1d514ac15 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 28 Oct 2020 21:23:56 -0700 Subject: [PATCH 01/21] Cleanup machinery around recursion --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 4 +-- .../src/Ide/Plugin/Tactic/Machinery.hs | 29 ++++++++++++------- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 8 ++--- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 10 +++++-- 4 files changed, 32 insertions(+), 19 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index db20420ede..77d424ec95 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -43,8 +43,8 @@ useOccName jdg name = ------------------------------------------------------------------------------ -- | Doing recursion incurs a small penalty in the score. -penalizeRecursion :: MonadState TacticState m => m () -penalizeRecursion = modify $ field @"ts_recursion_penality" +~ 1 +countRecursiveCall :: TacticState -> TacticState +countRecursiveCall = field @"ts_recursion_count" +~ 1 ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index f3e41c0061..4cc03c7d7e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -118,20 +118,29 @@ tracing s (TacticT m) mapExtract' (first $ rose s . pure) $ runStateT m jdg -recursiveCleanup +------------------------------------------------------------------------------ +-- | Recursion is allowed only when we can prove it is on a structurally +-- smaller argument. The top of the 'ts_recursion_stack' is set to 'True' iff +-- one of the recursive arguments is a pattern val (ie. came from a pattern +-- match.) +guardStructurallySmallerRecursion :: TacticState -> Maybe TacticError -recursiveCleanup s = - let r = head $ ts_recursion_stack s - in case r of - True -> Nothing - False -> Just NoProgress +guardStructurallySmallerRecursion s = + case head $ ts_recursion_stack s of + True -> Nothing + False -> Just NoProgress -setRecursionFrameData :: MonadState TacticState m => Bool -> m () -setRecursionFrameData b = do +------------------------------------------------------------------------------ +-- | Mark that the current recursive call is structurally smaller, due to +-- having been matched on a pattern value. +-- +-- Implemented by setting the top of the 'ts_recursion_stack'. +markStructuralySmallerRecursion :: MonadState TacticState m => m () +markStructuralySmallerRecursion = do modify $ withRecursionStack $ \case - (_ : bs) -> b : bs + (_ : bs) -> True : bs [] -> [] @@ -159,7 +168,7 @@ scoreSolution ext TacticState{..} holes , Penalize $ S.size ts_unused_top_vals , Penalize $ S.size ts_intro_vals , Reward $ S.size ts_used_vals - , Penalize $ ts_recursion_penality + , Penalize $ ts_recursion_count , Penalize $ solutionSize ext ) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index f1c2a6d220..e6e778d2d4 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -57,8 +57,7 @@ assume name = rule $ \jdg -> do case M.lookup name $ jHypothesis jdg of Just ty -> do unify ty $ jGoal jdg - when (M.member name $ jPatHypothesis jdg) $ - setRecursionFrameData True + when (M.member name $ jPatHypothesis jdg) markStructuralySmallerRecursion useOccName jdg name pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name Nothing -> throwError $ UndefinedHypothesis name @@ -68,9 +67,8 @@ recursion :: TacticsM () recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const $ fmap fst defs) $ \name -> do - modify $ withRecursionStack (False :) - penalizeRecursion - ensure recursiveCleanup (withRecursionStack tail) $ do + modify $ pushRecursionStack . countRecursiveCall + ensure guardStructurallySmallerRecursion popRecursionStack $ do (localTactic (apply name) $ introducingAmbient defs) <@> fmap (localTactic assumption . filterPosition name) [0..] diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 6b4201b49a..1dbef4add7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -87,7 +87,7 @@ data TacticState = TacticState -- ^ Stack for tracking whether or not the current recursive call has -- used at least one smaller pat val. Recursive calls for which this -- value is 'False' are guaranteed to loop, and must be pruned. - , ts_recursion_penality :: !Int + , ts_recursion_count :: !Int -- ^ Number of calls to recursion. We penalize each. , ts_unique_gen :: !UniqSupply } deriving stock (Show, Generic) @@ -113,7 +113,7 @@ defaultTacticState = , ts_intro_vals = mempty , ts_unused_top_vals = mempty , ts_recursion_stack = mempty - , ts_recursion_penality = 0 + , ts_recursion_count = 0 , ts_unique_gen = unsafeDefaultUniqueSupply } @@ -132,6 +132,12 @@ withRecursionStack withRecursionStack f = field @"ts_recursion_stack" %~ f +pushRecursionStack :: TacticState -> TacticState +pushRecursionStack = withRecursionStack (False :) + +popRecursionStack :: TacticState -> TacticState +popRecursionStack = withRecursionStack tail + withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState withUsedVals f = From ed3828df79f31c04ce2c8ab24c67e51935482d67 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 28 Oct 2020 22:14:25 -0700 Subject: [PATCH 02/21] Beginning of data provenance --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 11 +-- .../src/Ide/Plugin/Tactic/Judgements.hs | 71 ++++++++++++++----- .../src/Ide/Plugin/Tactic/Machinery.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 15 ++-- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 45 ++++++++++-- 6 files changed, 108 insertions(+), 38 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 25874bf242..1922d8a8ea 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -214,7 +214,7 @@ filterBindingType filterBindingType p tp dflags plId uri range jdg = let hy = jHypothesis jdg g = jGoal jdg - in fmap join $ for (M.toList hy) $ \(occ, CType ty) -> + in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) -> case p (unCType g) ty of True -> tp occ ty dflags plId uri range jdg False -> pure [] diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 77d424ec95..c561c4115f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -59,11 +59,13 @@ destructMatches -- ^ How to construct each match -> ([(OccName, CType)] -> Judgement -> Judgement) -- ^ How to derive each match judgement + -> Maybe OccName + -- ^ Scrutinee -> CType -- ^ Type being destructed -> Judgement -> RuleM (Trace, [RawMatch]) -destructMatches f f2 t jdg = do +destructMatches f f2 scrut t jdg = do let hy = jHypothesis jdg g = jGoal jdg case splitTyConApp_maybe $ unCType t of @@ -80,7 +82,7 @@ destructMatches f f2 t jdg = do let j = f2 hy' $ withPositionMapping dcon_name names - $ introducingPat hy' + $ introducingPat scrut dc hy' $ withNewGoal g jdg (tr, sg) <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names @@ -142,12 +144,13 @@ destruct' f term jdg = do let hy = jHypothesis jdg case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term - Just (_, t) -> do + Just (_, hi_type -> t) -> do useOccName jdg term (tr, ms) <- destructMatches f (\cs -> setParents term (fmap fst cs) . destructing term) + (Just term) t jdg pure ( rose ("destruct " <> show term) $ pure tr @@ -165,7 +168,7 @@ destructLambdaCase' f jdg = do case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> fmap (fmap noLoc $ lambdaCase) <$> - destructMatches f (const id) (CType arg) jdg + destructMatches f (const id) Nothing (CType arg) jdg _ -> throwError $ GoalMismatch "destructLambdaCase'" g diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 3beb40daa4..b45764f6e6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -20,6 +20,7 @@ import Ide.Plugin.Tactic.Types import OccName import SrcLoc import Type +import DataCon (DataCon) ------------------------------------------------------------------------------ @@ -70,16 +71,25 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t -introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducing ns = - field @"_jHypothesis" <>~ M.fromList ns +introducingLambda + :: Maybe OccName -- ^ top level function, or Nothing for any other function + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a +introducingLambda func ns = + field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&> \(pos, (name, ty)) -> + -- TODO(sandy): cleanup + (name, HyInfo (maybe LocalHypothesis (\x -> TopLevelArgPrv x pos) func) ty)) ------------------------------------------------------------------------------ -- | Add some terms to the ambient hypothesis introducingAmbient :: [(OccName, a)] -> Judgement' a -> Judgement' a introducingAmbient ns = - field @"_jAmbientHypothesis" <>~ M.fromList ns + field @"_jHypothesis" <>~ M.fromList (ns <&> \(name, ty) -> + -- TODO(sandy): cleanup + (name, HyInfo (ClassMethodPrv undefined) ty + )) filterPosition :: OccName -> Int -> Judgement -> Judgement @@ -150,7 +160,7 @@ extremelyStupid__definingFunction = withHypothesis - :: (Map OccName a -> Map OccName a) + :: (Map OccName (HyInfo a) -> Map OccName (HyInfo a)) -> Judgement' a -> Judgement' a withHypothesis f = @@ -158,9 +168,10 @@ withHypothesis f = ------------------------------------------------------------------------------ -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals. -introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingPat ns jdg = jdg - & field @"_jHypothesis" <>~ M.fromList ns +introducingPat :: Maybe OccName -> DataCon -> [(OccName, a)] -> Judgement' a -> Judgement' a +introducingPat scrutinee dc ns jdg = jdg + & field @"_jHypothesis" <>~ (M.fromList $ zip [0..] ns <&> \(pos, (name, ty)) -> + (name, HyInfo (PatternMatchPrv scrutinee (Uniquely dc) pos) ty)) & field @"_jPatternVals" <>~ S.fromList (fmap fst ns) @@ -172,21 +183,22 @@ disallowing ns = ------------------------------------------------------------------------------ -- | The hypothesis, consisting of local terms and the ambient environment -- (includes and class methods.) -jHypothesis :: Judgement' a -> Map OccName a -jHypothesis = _jHypothesis <> _jAmbientHypothesis +jHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jHypothesis = _jHypothesis ------------------------------------------------------------------------------ -- | Just the local hypothesis. -jLocalHypothesis :: Judgement' a -> Map OccName a -jLocalHypothesis = _jHypothesis +jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . _jHypothesis isPatVal :: Judgement' a -> OccName -> Bool isPatVal j n = S.member n $ _jPatternVals j -isTopHole :: Judgement' a -> Bool -isTopHole = _jIsTopHole +isTopHole :: Context -> Judgement' a -> Maybe OccName +isTopHole ctx = + bool Nothing (Just $ extremelyStupid__definingFunction ctx) . _jIsTopHole unsetIsTopHole :: Judgement' a -> Judgement' a unsetIsTopHole = field @"_jIsTopHole" .~ False @@ -194,9 +206,11 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals -jPatHypothesis :: Judgement' a -> Map OccName a +jPatHypothesis :: Judgement' a -> Map OccName (HyInfo a) jPatHypothesis jdg - = M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg + = mappend + (M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg) + (M.filter (isPatternMatch . hi_provenance) $ _jHypothesis jdg) jGoal :: Judgement' a -> a @@ -205,7 +219,6 @@ jGoal = _jGoal substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce - mkFirstJudgement :: M.Map OccName CType -- ^ local hypothesis -> M.Map OccName CType -- ^ ambient hypothesis @@ -214,8 +227,8 @@ mkFirstJudgement -> Type -> Judgement' CType mkFirstJudgement hy ambient top posvals goal = Judgement - { _jHypothesis = hy - , _jAmbientHypothesis = ambient + { _jHypothesis = M.map mkLocalHypothesisInfo hy + <> M.map mkAmbientHypothesisInfo ambient , _jDestructed = mempty , _jPatternVals = mempty , _jBlacklistDestruct = False @@ -226,3 +239,23 @@ mkFirstJudgement hy ambient top posvals goal = Judgement , _jGoal = CType goal } + +mkLocalHypothesisInfo :: a -> HyInfo a +mkLocalHypothesisInfo = HyInfo LocalHypothesis + + +mkAmbientHypothesisInfo :: a -> HyInfo a +mkAmbientHypothesisInfo = HyInfo ImportPrv + + +isLocalHypothesis :: Provenance -> Bool +isLocalHypothesis LocalHypothesis{} = True +isLocalHypothesis PatternMatchPrv{} = True +isLocalHypothesis TopLevelArgPrv{} = True +isLocalHypothesis _ = False + + +isPatternMatch :: Provenance -> Bool +isPatternMatch PatternMatchPrv{} = True +isPatternMatch _ = False + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 4cc03c7d7e..26108c5cbc 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -74,7 +74,7 @@ runTactic ctx jdg t = let skolems = nub $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ jGoal jdg - : (toList $ jHypothesis jdg) + : (fmap hi_type $ toList $ jHypothesis jdg) unused_topvals = nub $ join $ join $ toList $ _jPositionMaps jdg tacticState = defaultTacticState diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index e6e778d2d4..e451951654 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -55,7 +55,7 @@ assume :: OccName -> TacticsM () assume name = rule $ \jdg -> do let g = jGoal jdg case M.lookup name $ jHypothesis jdg of - Just ty -> do + Just (hi_type -> ty) -> do unify ty $ jGoal jdg when (M.member name $ jPatHypothesis jdg) markStructuralySmallerRecursion useOccName jdg name @@ -84,17 +84,18 @@ intros = rule $ \jdg -> do ([], _) -> throwError $ GoalMismatch "intros" g (as, b) -> do vs <- mkManyGoodNames hy as - let jdg' = introducing (zip vs $ coerce as) + let top_hole = isTopHole ctx jdg + let jdg' = introducingLambda top_hole (zip vs $ coerce as) $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs - when (isTopHole jdg) $ addUnusedTopVals $ S.fromList vs + when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs (tr, sg) <- newSubgoal $ bool id (withPositionMapping (extremelyStupid__definingFunction ctx) vs) - (isTopHole jdg) + (isJust top_hole) $ jdg' pure . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) @@ -165,7 +166,7 @@ apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do let hy = jHypothesis jdg g = jGoal jdg case M.lookup func hy of - Just (CType ty) -> do + Just (hi_type -> CType ty) -> do ty' <- freshTyvars ty let (_, _, args, ret) = tacticsSplitFunTy ty' requireNewHoles $ rule $ \jdg -> do @@ -281,12 +282,12 @@ auto' n = do overFunctions :: (OccName -> TacticsM ()) -> TacticsM () overFunctions = - attemptOn $ M.keys . M.filter (isFunction . unCType) . jHypothesis + attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM () overAlgebraicTerms = attemptOn $ - M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis + M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis allNames :: Judgement -> [OccName] diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 1dbef4add7..ec41ca60d9 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -39,7 +39,7 @@ import Refinery.Tactic import System.IO.Unsafe (unsafePerformIO) import Type import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) -import Unique (Unique) +import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) ------------------------------------------------------------------------------ @@ -70,6 +70,9 @@ instance Show (LHsExpr GhcPs) where instance Show DataCon where show = unsafeRender +instance Show Class where + show = unsafeRender + ------------------------------------------------------------------------------ data TacticState = TacticState @@ -149,14 +152,44 @@ withIntroducedVals f = field @"ts_intro_vals" %~ f +data Provenance + = TopLevelArgPrv + OccName -- ^ Function name + Int -- ^ Position + | PatternMatchPrv + (Maybe OccName) -- ^ Scrutinee. Nothing, for lambda case. + (Uniquely DataCon) -- ^ Matching datacon + Int -- ^ Position + | ClassMethodPrv + (Uniquely Class) -- ^ Class + -- TODO(sandy): delete this asap + | LocalHypothesis + | ImportPrv + | RecursivePrv + deriving stock (Eq, Show, Generic, Ord) + + +newtype Uniquely a = Uniquely { getViaUnique :: a } + deriving stock Show + +instance Uniquable a => Eq (Uniquely a) where + (==) = (==) `on` getUnique . getViaUnique + +instance Uniquable a => Ord (Uniquely a) where + compare = nonDetCmpUnique `on` getUnique . getViaUnique + + +data HyInfo a = HyInfo + { hi_provenance :: Provenance + , hi_type :: a + } + deriving stock (Functor, Eq, Show, Generic, Ord) + ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement - { _jHypothesis :: !(Map OccName a) - , _jAmbientHypothesis :: !(Map OccName a) - -- ^ Things in the hypothesis that were imported. Solutions don't get - -- points for using the ambient hypothesis. + { _jHypothesis :: !(Map OccName (HyInfo a)) , _jDestructed :: !(Set OccName) -- ^ These should align with keys of _jHypothesis , _jPatternVals :: !(Set OccName) @@ -168,7 +201,7 @@ data Judgement' a = Judgement , _jIsTopHole :: !Bool , _jGoal :: !(a) } - deriving stock (Eq, Ord, Generic, Functor, Show) + deriving stock (Eq, Generic, Functor, Show) type Judgement = Judgement' CType From f3410a3c6454eb919548eeb834804428b9a9b63e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 28 Oct 2020 22:25:51 -0700 Subject: [PATCH 03/21] Remove pat vals --- .../src/Ide/Plugin/Tactic/Judgements.hs | 16 +++------ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 33 ++++++++++--------- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 5 +-- 3 files changed, 25 insertions(+), 29 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index b45764f6e6..dd31dd78cc 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -84,11 +84,11 @@ introducingLambda func ns = ------------------------------------------------------------------------------ -- | Add some terms to the ambient hypothesis -introducingAmbient :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingAmbient ns = +introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a +introducingRecursively ns = field @"_jHypothesis" <>~ M.fromList (ns <&> \(name, ty) -> -- TODO(sandy): cleanup - (name, HyInfo (ClassMethodPrv undefined) ty + (name, HyInfo RecursivePrv ty )) @@ -172,7 +172,6 @@ introducingPat :: Maybe OccName -> DataCon -> [(OccName, a)] -> Judgement' a -> introducingPat scrutinee dc ns jdg = jdg & field @"_jHypothesis" <>~ (M.fromList $ zip [0..] ns <&> \(pos, (name, ty)) -> (name, HyInfo (PatternMatchPrv scrutinee (Uniquely dc) pos) ty)) - & field @"_jPatternVals" <>~ S.fromList (fmap fst ns) disallowing :: [OccName] -> Judgement' a -> Judgement' a @@ -193,9 +192,6 @@ jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a) jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . _jHypothesis -isPatVal :: Judgement' a -> OccName -> Bool -isPatVal j n = S.member n $ _jPatternVals j - isTopHole :: Context -> Judgement' a -> Maybe OccName isTopHole ctx = bool Nothing (Just $ extremelyStupid__definingFunction ctx) . _jIsTopHole @@ -207,10 +203,7 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName (HyInfo a) -jPatHypothesis jdg - = mappend - (M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg) - (M.filter (isPatternMatch . hi_provenance) $ _jHypothesis jdg) +jPatHypothesis = M.filter (isPatternMatch . hi_provenance) . _jHypothesis jGoal :: Judgement' a -> a @@ -230,7 +223,6 @@ mkFirstJudgement hy ambient top posvals goal = Judgement { _jHypothesis = M.map mkLocalHypothesisInfo hy <> M.map mkAmbientHypothesisInfo ambient , _jDestructed = mempty - , _jPatternVals = mempty , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jPositionMaps = posvals diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index e451951654..26777317e7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -69,7 +69,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do attemptOn (const $ fmap fst defs) $ \name -> do modify $ pushRecursionStack . countRecursiveCall ensure guardStructurallySmallerRecursion popRecursionStack $ do - (localTactic (apply name) $ introducingAmbient defs) + (localTactic (apply name) $ introducingRecursively defs) <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -109,20 +109,23 @@ intros = rule $ \jdg -> do destructAuto :: OccName -> TacticsM () destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do jdg <- goal - case hasDestructed jdg name of - True -> throwError $ AlreadyDestructed name - False -> - let subtactic = rule $ destruct' (const subgoal) name - in case isPatVal jdg name of - True -> - pruning subtactic $ \jdgs -> - let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis - new_hy = foldMap getHyTypes jdgs - old_hy = getHyTypes jdg - in case S.null $ new_hy S.\\ old_hy of - True -> Just $ UnhelpfulDestruct name - False -> Nothing - False -> subtactic + case M.lookup name $ jHypothesis jdg of + Nothing -> throwError $ NotInScope name + Just hi -> + case hasDestructed jdg name of + True -> throwError $ AlreadyDestructed name + False -> + let subtactic = rule $ destruct' (const subgoal) name + in case isPatternMatch $ hi_provenance hi of + True -> + pruning subtactic $ \jdgs -> + let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis + new_hy = foldMap getHyTypes jdgs + old_hy = getHyTypes jdg + in case S.null $ new_hy S.\\ old_hy of + True -> Just $ UnhelpfulDestruct name + False -> Nothing + False -> subtactic ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index ec41ca60d9..9f2aae1721 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -192,8 +192,6 @@ data Judgement' a = Judgement { _jHypothesis :: !(Map OccName (HyInfo a)) , _jDestructed :: !(Set OccName) -- ^ These should align with keys of _jHypothesis - , _jPatternVals :: !(Set OccName) - -- ^ These should align with keys of _jHypothesis , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) , _jPositionMaps :: !(Map OccName [[OccName]]) @@ -230,6 +228,7 @@ data TacticError | UnhelpfulDestruct OccName | UnhelpfulSplit OccName | TooPolymorphic + | NotInScope OccName deriving stock (Eq) instance Show TacticError where @@ -268,6 +267,8 @@ instance Show TacticError where "Splitting constructor " <> show n <> " leads to no new goals" show TooPolymorphic = "The tactic isn't applicable because the goal is too polymorphic" + show (NotInScope name) = + "Tried to do something with the out of scope name " <> show name ------------------------------------------------------------------------------ From b4299728fe1f046804cdabc2da09a58174c5065c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 29 Oct 2020 09:23:22 -0700 Subject: [PATCH 04/21] Incorporate _jAncestry into Provenance --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 75 +++++++++++++------ .../tactics/src/Ide/Plugin/Tactic/Types.hs | 8 +- 3 files changed, 59 insertions(+), 26 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index c561c4115f..7b5aab842e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -149,7 +149,7 @@ destruct' f term jdg = do (tr, ms) <- destructMatches f - (\cs -> setParents term (fmap fst cs) . destructing term) + (const $ destructing term) (Just term) t jdg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index dd31dd78cc..5b8e6d1ad7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -1,11 +1,13 @@ -{-# LANGUAGE TupleSections #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} module Ide.Plugin.Tactic.Judgements where +import Control.Applicative import Control.Lens hiding (Context) import Data.Bool import Data.Char @@ -14,13 +16,14 @@ 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 DataCon (dataConName, DataCon) import Development.IDE.Spans.LocalBindings import Ide.Plugin.Tactic.Types import OccName import SrcLoc import Type -import DataCon (DataCon) ------------------------------------------------------------------------------ @@ -79,7 +82,7 @@ introducingLambda introducingLambda func ns = field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&> \(pos, (name, ty)) -> -- TODO(sandy): cleanup - (name, HyInfo (maybe LocalHypothesis (\x -> TopLevelArgPrv x pos) func) ty)) + (name, HyInfo (maybe UserPrv (\x -> TopLevelArgPrv x pos) func) ty)) ------------------------------------------------------------------------------ @@ -105,6 +108,24 @@ filterSameTypeFromOtherPositions defn pos jdg = tys = S.fromList $ fmap snd $ M.toList hy in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg +getAncestry :: Judgement' a -> OccName -> Set OccName +getAncestry jdg name = + case M.lookup name $ jHypothesis jdg of + Just hi -> + case hi_provenance hi of + PatternMatchPrv _ ancestry _ _ -> ancestry + _ -> mempty + Nothing -> mempty + + +-- getPositionalBindings :: Judgement -> [(OccName, [IntMap OccName])] +-- getPositionalBindings jdg = _ $ do +-- (name, hi_provenance -> hi) <- M.toList $ jHypothesis jdg +-- case hi of +-- TopLevelArgPrv o i -> pure (name, (o, i)) +-- PatternMatchPrv _ ud i -> pure (name, (occName $ dataConName $ getViaUnique ud, i)) +-- _ -> empty + hasPositionalAncestry :: Judgement @@ -119,7 +140,7 @@ hasPositionalAncestry jdg defn n name = case any (== name) ancestors of True -> Just True False -> - case M.lookup name $ _jAncestry jdg of + case M.lookup name $ jAncestryMap jdg of Just ancestry -> bool Nothing (Just False) $ any (flip S.member ancestry) ancestors Nothing -> Nothing @@ -130,17 +151,12 @@ hasPositionalAncestry jdg defn n name $ _jPositionMaps jdg -setParents - :: OccName -- ^ parent - -> [OccName] -- ^ children - -> Judgement - -> Judgement -setParents p cs jdg = - let ancestry = mappend (S.singleton p) - $ fromMaybe mempty - $ M.lookup p - $ _jAncestry jdg - in jdg & field @"_jAncestry" <>~ M.fromList (fmap (, ancestry) cs) +jAncestryMap :: Judgement' a -> Map OccName (Set OccName) +jAncestryMap jdg = + flip M.mapMaybe (jHypothesis jdg) $ \hi -> + case hi_provenance hi of + PatternMatchPrv _ ancestry _ _ -> Just ancestry + _ -> Nothing withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement @@ -167,11 +183,27 @@ withHypothesis f = field @"_jHypothesis" %~ f ------------------------------------------------------------------------------ --- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals. -introducingPat :: Maybe OccName -> DataCon -> [(OccName, a)] -> Judgement' a -> Judgement' a +-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of +-- data sitting around in jPatternVals. +introducingPat + :: Maybe OccName + -> DataCon + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a introducingPat scrutinee dc ns jdg = jdg & field @"_jHypothesis" <>~ (M.fromList $ zip [0..] ns <&> \(pos, (name, ty)) -> - (name, HyInfo (PatternMatchPrv scrutinee (Uniquely dc) pos) ty)) + ( name + , HyInfo + (PatternMatchPrv + scrutinee + (maybe + mempty + (\scrut -> S.singleton scrut <> getAncestry jdg scrut) + scrutinee) + (Uniquely dc) + pos) + ty)) disallowing :: [OccName] -> Judgement' a -> Judgement' a @@ -212,6 +244,8 @@ jGoal = _jGoal substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce + + mkFirstJudgement :: M.Map OccName CType -- ^ local hypothesis -> M.Map OccName CType -- ^ ambient hypothesis @@ -226,14 +260,13 @@ mkFirstJudgement hy ambient top posvals goal = Judgement , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jPositionMaps = posvals - , _jAncestry = mempty , _jIsTopHole = top , _jGoal = CType goal } mkLocalHypothesisInfo :: a -> HyInfo a -mkLocalHypothesisInfo = HyInfo LocalHypothesis +mkLocalHypothesisInfo = HyInfo UserPrv mkAmbientHypothesisInfo :: a -> HyInfo a @@ -241,7 +274,7 @@ mkAmbientHypothesisInfo = HyInfo ImportPrv isLocalHypothesis :: Provenance -> Bool -isLocalHypothesis LocalHypothesis{} = True +isLocalHypothesis UserPrv{} = True isLocalHypothesis PatternMatchPrv{} = True isLocalHypothesis TopLevelArgPrv{} = True isLocalHypothesis _ = False diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 9f2aae1721..e126ad3f36 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeApplications #-} @@ -158,19 +159,19 @@ data Provenance Int -- ^ Position | PatternMatchPrv (Maybe OccName) -- ^ Scrutinee. Nothing, for lambda case. + (Set OccName) -- ^ Ancestry (Uniquely DataCon) -- ^ Matching datacon Int -- ^ Position | ClassMethodPrv (Uniquely Class) -- ^ Class - -- TODO(sandy): delete this asap - | LocalHypothesis + | UserPrv | ImportPrv | RecursivePrv deriving stock (Eq, Show, Generic, Ord) newtype Uniquely a = Uniquely { getViaUnique :: a } - deriving stock Show + deriving Show via a instance Uniquable a => Eq (Uniquely a) where (==) = (==) `on` getUnique . getViaUnique @@ -195,7 +196,6 @@ data Judgement' a = Judgement , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) , _jPositionMaps :: !(Map OccName [[OccName]]) - , _jAncestry :: !(Map OccName (Set OccName)) , _jIsTopHole :: !Bool , _jGoal :: !(a) } From 52631f4a42c1efb8134ea163bd829edb997975c5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 29 Oct 2020 10:23:41 -0700 Subject: [PATCH 05/21] Remove _jDestructed --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 10 ++-- .../src/Ide/Plugin/Tactic/Judgements.hs | 50 ++++++++----------- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 2 + .../tactics/src/Ide/Plugin/Tactic/Types.hs | 18 ++++--- 4 files changed, 36 insertions(+), 44 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 7b5aab842e..06f3c712f6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -57,15 +57,13 @@ addUnusedTopVals vals = modify $ field @"ts_unused_top_vals" <>~ vals destructMatches :: (DataCon -> Judgement -> Rule) -- ^ How to construct each match - -> ([(OccName, CType)] -> Judgement -> Judgement) - -- ^ How to derive each match judgement -> Maybe OccName -- ^ Scrutinee -> CType -- ^ Type being destructed -> Judgement -> RuleM (Trace, [RawMatch]) -destructMatches f f2 scrut t jdg = do +destructMatches f scrut t jdg = do let hy = jHypothesis jdg g = jGoal jdg case splitTyConApp_maybe $ unCType t of @@ -80,8 +78,7 @@ destructMatches f f2 scrut t jdg = do let hy' = zip names $ coerce args dcon_name = nameOccName $ dataConName dc - let j = f2 hy' - $ withPositionMapping dcon_name names + let j = withPositionMapping dcon_name names $ introducingPat scrut dc hy' $ withNewGoal g jdg (tr, sg) <- f dc j @@ -149,7 +146,6 @@ destruct' f term jdg = do (tr, ms) <- destructMatches f - (const $ destructing term) (Just term) t jdg @@ -168,7 +164,7 @@ destructLambdaCase' f jdg = do case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> fmap (fmap noLoc $ lambdaCase) <$> - destructMatches f (const id) Nothing (CType arg) jdg + destructMatches f Nothing (CType arg) jdg _ -> throwError $ GoalMismatch "destructLambdaCase'" g diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 5b8e6d1ad7..1e58ca05a0 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -7,7 +7,6 @@ module Ide.Plugin.Tactic.Judgements where -import Control.Applicative import Control.Lens hiding (Context) import Data.Bool import Data.Char @@ -18,7 +17,7 @@ import qualified Data.Map as M import Data.Maybe import Data.Set (Set) import qualified Data.Set as S -import DataCon (dataConName, DataCon) +import DataCon (DataCon) import Development.IDE.Spans.LocalBindings import Ide.Plugin.Tactic.Types import OccName @@ -31,6 +30,7 @@ import Type hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span + ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis. buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType @@ -44,12 +44,9 @@ buildHypothesis | otherwise = Nothing -hasDestructed :: Judgement -> OccName -> Bool -hasDestructed j n = S.member n $ _jDestructed j - - -destructing :: OccName -> Judgement -> Judgement -destructing n = field @"_jDestructed" <>~ S.singleton n +hasDestructed :: Judgement' a -> OccName -> Bool +hasDestructed jdg n = flip any (jPatHypothesis jdg) $ + (== Just n) . pv_scrutinee blacklistingDestruct :: Judgement -> Judgement @@ -108,25 +105,14 @@ filterSameTypeFromOtherPositions defn pos jdg = tys = S.fromList $ fmap snd $ M.toList hy in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg + getAncestry :: Judgement' a -> OccName -> Set OccName getAncestry jdg name = - case M.lookup name $ jHypothesis jdg of - Just hi -> - case hi_provenance hi of - PatternMatchPrv _ ancestry _ _ -> ancestry - _ -> mempty + case M.lookup name $ jPatHypothesis jdg of + Just pv -> pv_ancestry pv Nothing -> mempty --- getPositionalBindings :: Judgement -> [(OccName, [IntMap OccName])] --- getPositionalBindings jdg = _ $ do --- (name, hi_provenance -> hi) <- M.toList $ jHypothesis jdg --- case hi of --- TopLevelArgPrv o i -> pure (name, (o, i)) --- PatternMatchPrv _ ud i -> pure (name, (occName $ dataConName $ getViaUnique ud, i)) --- _ -> empty - - hasPositionalAncestry :: Judgement -> OccName -- ^ defining fn @@ -153,10 +139,7 @@ hasPositionalAncestry jdg defn n name jAncestryMap :: Judgement' a -> Map OccName (Set OccName) jAncestryMap jdg = - flip M.mapMaybe (jHypothesis jdg) $ \hi -> - case hi_provenance hi of - PatternMatchPrv _ ancestry _ _ -> Just ancestry - _ -> Nothing + flip M.map (jPatHypothesis jdg) pv_ancestry withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement @@ -182,6 +165,7 @@ withHypothesis withHypothesis f = field @"_jHypothesis" %~ f + ------------------------------------------------------------------------------ -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of -- data sitting around in jPatternVals. @@ -195,7 +179,7 @@ introducingPat scrutinee dc ns jdg = jdg & field @"_jHypothesis" <>~ (M.fromList $ zip [0..] ns <&> \(pos, (name, ty)) -> ( name , HyInfo - (PatternMatchPrv + (PatternMatchPrv $ PatVal scrutinee (maybe mempty @@ -234,8 +218,15 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals -jPatHypothesis :: Judgement' a -> Map OccName (HyInfo a) -jPatHypothesis = M.filter (isPatternMatch . hi_provenance) . _jHypothesis +jPatHypothesis :: Judgement' a -> Map OccName PatVal +jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . _jHypothesis + + +getPatVal :: Provenance-> Maybe PatVal +getPatVal prov = + case prov of + PatternMatchPrv pv -> Just pv + _ -> Nothing jGoal :: Judgement' a -> a @@ -256,7 +247,6 @@ mkFirstJudgement mkFirstJudgement hy ambient top posvals goal = Judgement { _jHypothesis = M.map mkLocalHypothesisInfo hy <> M.map mkAmbientHypothesisInfo ambient - , _jDestructed = mempty , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jPositionMaps = posvals diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 26777317e7..43cfd98a8f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -68,6 +68,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const $ fmap fst defs) $ \name -> do modify $ pushRecursionStack . countRecursiveCall + jdg <- goal ensure guardStructurallySmallerRecursion popRecursionStack $ do (localTactic (apply name) $ introducingRecursively defs) <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -127,6 +128,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do False -> Nothing False -> subtactic + ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destruct :: OccName -> TacticsM () diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index e126ad3f36..3f51dbbbf3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -157,11 +157,7 @@ data Provenance = TopLevelArgPrv OccName -- ^ Function name Int -- ^ Position - | PatternMatchPrv - (Maybe OccName) -- ^ Scrutinee. Nothing, for lambda case. - (Set OccName) -- ^ Ancestry - (Uniquely DataCon) -- ^ Matching datacon - Int -- ^ Position + | PatternMatchPrv PatVal | ClassMethodPrv (Uniquely Class) -- ^ Class | UserPrv @@ -170,6 +166,16 @@ data Provenance deriving stock (Eq, Show, Generic, Ord) +data PatVal = PatVal + { pv_scrutinee :: Maybe OccName + -- ^ Original scrutinee which created this PatVal. Nothing, for lambda + -- case. + , pv_ancestry :: Set OccName + , pv_datacon :: Uniquely DataCon + , pv_position :: Int + } deriving stock (Eq, Show, Generic, Ord) + + newtype Uniquely a = Uniquely { getViaUnique :: a } deriving Show via a @@ -191,8 +197,6 @@ data HyInfo a = HyInfo -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement { _jHypothesis :: !(Map OccName (HyInfo a)) - , _jDestructed :: !(Set OccName) - -- ^ These should align with keys of _jHypothesis , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) , _jPositionMaps :: !(Map OccName [[OccName]]) From 0b80b8fe434cca6a7781b69ce832ea77abafd196 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 29 Oct 2020 12:01:43 -0700 Subject: [PATCH 06/21] We need _jDestructed for nullary datacons --- plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 5 +++-- plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 5 +++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 1e58ca05a0..f8e5c16569 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -45,8 +45,7 @@ buildHypothesis hasDestructed :: Judgement' a -> OccName -> Bool -hasDestructed jdg n = flip any (jPatHypothesis jdg) $ - (== Just n) . pv_scrutinee +hasDestructed jdg n = S.member n $ _jDestructed jdg blacklistingDestruct :: Judgement -> Judgement @@ -188,6 +187,7 @@ introducingPat scrutinee dc ns jdg = jdg (Uniquely dc) pos) ty)) + & maybe id (\scrut -> field @"_jDestructed" <>~ S.singleton scrut) scrutinee disallowing :: [OccName] -> Judgement' a -> Judgement' a @@ -249,6 +249,7 @@ mkFirstJudgement hy ambient top posvals goal = Judgement <> M.map mkAmbientHypothesisInfo ambient , _jBlacklistDestruct = False , _jWhitelistSplit = True + , _jDestructed = mempty , _jPositionMaps = posvals , _jIsTopHole = top , _jGoal = CType goal diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 3f51dbbbf3..b045a8cafc 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -197,6 +197,11 @@ data HyInfo a = HyInfo -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement { _jHypothesis :: !(Map OccName (HyInfo a)) + , _jDestructed :: !(Set OccName) + -- ^ Set of names we've already destructed. These should align with keys of + -- _jHypothesis. You might think we could just inspect the hypothesis and + -- find any PatVals whose scrutinee is the name in question, but this fails + -- for nullary data constructors. , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) , _jPositionMaps :: !(Map OccName [[OccName]]) From 9649be4748e47c29f08c9594492f6b8992202beb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 29 Oct 2020 23:05:53 -0700 Subject: [PATCH 07/21] yo --- plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 8 ++++---- plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index b45764f6e6..0f384f0391 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -102,8 +102,8 @@ filterPosition defn pos jdg = filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions defn pos jdg = let hy = jHypothesis $ filterPosition defn pos jdg - tys = S.fromList $ fmap snd $ M.toList hy - in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg + tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy + in withHypothesis (\hy2 -> M.filter (not . flip S.member tys . hi_type) hy2 <> hy) jdg hasPositionalAncestry @@ -208,8 +208,8 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName (HyInfo a) jPatHypothesis jdg - = mappend - (M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg) + = + -- (M.restrictKeys (jHypothesis jdg) $ _jPatternVals jdg) (M.filter (isPatternMatch . hi_provenance) $ _jHypothesis jdg) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index e451951654..8d8cc3fe4a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -116,7 +116,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do in case isPatVal jdg name of True -> pruning subtactic $ \jdgs -> - let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis + let getHyTypes = S.fromList . fmap (hi_type . snd) . M.toList . jHypothesis new_hy = foldMap getHyTypes jdgs old_hy = getHyTypes jdg in case S.null $ new_hy S.\\ old_hy of From 3e87cc19773e39f4e566cd876848e61534fbbeaf Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 10:54:57 -0700 Subject: [PATCH 08/21] tests pass sweet lord --- plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 3 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 123 ++++++++++++++++-- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 5 +- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 10 ++ 5 files changed, 129 insertions(+), 14 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs index 5ce8605e70..e07aa1dfb2 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs @@ -23,6 +23,6 @@ auto = do commit knownStrategies . tracing "auto" . localTactic (auto' 4) - . disallowing + . disallowing RecursiveCall $ fmap fst current diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 06f3c712f6..7d6a58561f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -177,12 +177,11 @@ buildDataCon -> RuleM (Trace, LHsExpr GhcPs) buildDataCon jdg dc apps = do let args = dataConInstOrigArgTys' dc apps - dcon_name = nameOccName $ dataConName dc (tr, sgs) <- fmap unzipTrace $ traverse ( \(arg, n) -> newSubgoal - . filterSameTypeFromOtherPositions dcon_name n + . filterSameTypeFromOtherPositions''' dc n . blacklistingDestruct . flip withNewGoal jdg $ CType arg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 80d422594b..6b1f30b5ac 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -93,16 +93,103 @@ introducingRecursively ns = filterPosition :: OccName -> Int -> Judgement -> Judgement filterPosition defn pos jdg = - withHypothesis (M.filterWithKey go) jdg + disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg where - go name _ = isJust $ hasPositionalAncestry jdg defn pos name + go name _ = not . isJust $ hasPositionalAncestry jdg defn pos name + +hasPositionalAncestry' + :: Foldable t + => t OccName + -> Judgement + -> OccName -- ^ thing to check ancestry + -> 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 any (== name) ancestors of + True -> Just True + False -> + case M.lookup name $ traceIdX "ancestry" $ jAncestryMap jdg of + Just ancestry -> + bool Nothing (Just False) $ any (flip S.member ancestry) ancestors + Nothing -> Nothing + | otherwise = Nothing + +filterPosition' :: OccName -> Int -> Judgement -> Judgement +filterPosition' defn pos jdg = + disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg + where + go name _ + = not + . isJust + $ hasPositionalAncestry' (findPositionVal' jdg defn pos) jdg name + +filterPosition''' :: OccName -> Int -> Judgement -> Judgement +filterPosition''' defn pos jdg = + let broken_ancestors = findPositionVal' jdg defn pos + ancestors = toListOf (_Just . traversed . ix pos) + $ M.lookup defn + $ _jPositionMaps jdg + working = filterPosition defn pos jdg + in case maybeToList broken_ancestors == ancestors of + True -> working + -- TODO(sandy): THE BUG IS THAT WE FILTER OUT FROM THE HYPOTHESIS + -- WHICH REMOVES THE EQUIVALENT OF A POSITION MAPPING; BUT THAT _USED_ + -- TO BE THERE. + False -> error $ show (broken_ancestors, ancestors, defn, pos, jHypothesis jdg) + -- broken = filterPosition' defn pos jdg + -- in case working == broken of + -- True -> working + -- False -> error $ show (working, broken) + +filterDconPosition' :: DataCon -> Int -> Judgement -> Judgement +filterDconPosition' dcon pos jdg = + disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg + where + go name _ + = not + . isJust + $ hasPositionalAncestry' (findDconPositionVals' jdg dcon pos) jdg name + +findPositionVal' :: Judgement' a -> OccName -> Int -> Maybe OccName +findPositionVal' jdg defn pos = listToMaybe $ do + (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ 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 + _ -> [] + +findDconPositionVals' :: Judgement' a -> DataCon -> Int -> [OccName] +findDconPositionVals' jdg dcon pos = do + (name, hi) <- M.toList $ jHypothesis jdg + case hi_provenance hi of + PatternMatchPrv pv + | pv_datacon pv == Uniquely dcon + , pv_position pv == pos -> pure name + _ -> [] + +filterSameTypeFromOtherPositions''' :: DataCon -> Int -> Judgement -> Judgement +filterSameTypeFromOtherPositions''' dcon pos jdg = filterSameTypeFromOtherPositions' dcon pos jdg + +filterSameTypeFromOtherPositions' :: DataCon -> Int -> Judgement -> Judgement +filterSameTypeFromOtherPositions' dcon pos jdg = + let hy = jHypothesis $ filterDconPosition' dcon pos jdg + tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy + to_remove = M.filter (flip S.member tys . hi_type) (jHypothesis jdg) M.\\ hy + in disallowing (WrongBranch pos) (M.keys to_remove) jdg filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions defn pos jdg = let hy = jHypothesis $ filterPosition defn pos jdg tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy - in withHypothesis (\hy2 -> M.filter (not . flip S.member tys . hi_type) hy2 <> hy) jdg + to_remove = M.filter (flip S.member tys . hi_type) (jHypothesis jdg) M.\\ hy + in disallowing (WrongBranch pos) (M.keys to_remove) jdg getAncestry :: Judgement' a -> OccName -> Set OccName @@ -190,22 +277,32 @@ introducingPat scrutinee dc ns jdg = jdg & maybe id (\scrut -> field @"_jDestructed" <>~ S.singleton scrut) scrutinee -disallowing :: [OccName] -> Judgement' a -> Judgement' a -disallowing ns = - field @"_jHypothesis" %~ flip M.withoutKeys (S.fromList ns) +disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a +disallowing reason (S.fromList -> ns) = + field @"_jHypothesis" %~ (M.mapWithKey $ \name hi -> + case S.member name ns of + True -> overProvenance (DisallowedPrv reason) hi + False -> hi + ) ------------------------------------------------------------------------------ -- | The hypothesis, consisting of local terms and the ambient environment -- (includes and class methods.) jHypothesis :: Judgement' a -> Map OccName (HyInfo a) -jHypothesis = _jHypothesis +jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis + + +------------------------------------------------------------------------------ +-- | The whole hypothesis, including things disallowed. +jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jEntireHypothesis = _jHypothesis ------------------------------------------------------------------------------ -- | Just the local hypothesis. jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a) -jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . _jHypothesis +jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis isTopHole :: Context -> Judgement' a -> Maybe OccName @@ -219,7 +316,7 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName PatVal -jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . _jHypothesis +jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis getPatVal :: Provenance-> Maybe PatVal @@ -275,3 +372,11 @@ isPatternMatch :: Provenance -> Bool isPatternMatch PatternMatchPrv{} = True isPatternMatch _ = False +isDisallowed :: Provenance -> Bool +isDisallowed DisallowedPrv{} = True +isDisallowed _ = False + +expandDisallowed :: Provenance -> Provenance +expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv +expandDisallowed prv = prv + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index fb1e38581f..3b1ce087e5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -71,7 +71,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do jdg <- goal ensure guardStructurallySmallerRecursion popRecursionStack $ do (localTactic (apply name) $ introducingRecursively defs) - <@> fmap (localTactic assumption . filterPosition name) [0..] + <@> fmap (localTactic assumption . filterPosition''' name) [0..] ------------------------------------------------------------------------------ @@ -86,7 +86,8 @@ intros = rule $ \jdg -> do (as, b) -> do vs <- mkManyGoodNames hy as let top_hole = isTopHole ctx jdg - let jdg' = introducingLambda top_hole (zip vs $ coerce as) + let jdg' = traceIdX "introduced lambda" + $ introducingLambda top_hole (zip vs $ coerce as) $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index b045a8cafc..0f76560b43 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -163,6 +163,13 @@ data Provenance | UserPrv | ImportPrv | RecursivePrv + | DisallowedPrv DisallowReason Provenance + deriving stock (Eq, Show, Generic, Ord) + + +data DisallowReason + = WrongBranch Int + | RecursiveCall deriving stock (Eq, Show, Generic, Ord) @@ -192,6 +199,9 @@ data HyInfo a = HyInfo } deriving stock (Functor, Eq, Show, Generic, Ord) +overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a +overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty + ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. From 5c956c520c1f69110b392f23f2ba9da3458ea633 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 11:05:13 -0700 Subject: [PATCH 09/21] rip out old machinery --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 68 ++++--------------- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 2 +- 3 files changed, 15 insertions(+), 57 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 7d6a58561f..1e040a2fe7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -181,7 +181,7 @@ buildDataCon jdg dc apps = do <- fmap unzipTrace $ traverse ( \(arg, n) -> newSubgoal - . filterSameTypeFromOtherPositions''' dc n + . filterSameTypeFromOtherPositions dc n . blacklistingDestruct . flip withNewGoal jdg $ CType arg diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 6b1f30b5ac..90e8f546c3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -91,12 +91,6 @@ introducingRecursively ns = )) -filterPosition :: OccName -> Int -> Judgement -> Judgement -filterPosition defn pos jdg = - disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg - where - go name _ = not . isJust $ hasPositionalAncestry jdg defn pos name - hasPositionalAncestry' :: Foldable t => t OccName @@ -116,44 +110,26 @@ hasPositionalAncestry' ancestors jdg name Nothing -> Nothing | otherwise = Nothing -filterPosition' :: OccName -> Int -> Judgement -> Judgement -filterPosition' defn pos jdg = +filterPosition :: OccName -> Int -> Judgement -> Judgement +filterPosition defn pos jdg = disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg where go name _ = not . isJust - $ hasPositionalAncestry' (findPositionVal' jdg defn pos) jdg name + $ hasPositionalAncestry' (findPositionVal jdg defn pos) jdg name -filterPosition''' :: OccName -> Int -> Judgement -> Judgement -filterPosition''' defn pos jdg = - let broken_ancestors = findPositionVal' jdg defn pos - ancestors = toListOf (_Just . traversed . ix pos) - $ M.lookup defn - $ _jPositionMaps jdg - working = filterPosition defn pos jdg - in case maybeToList broken_ancestors == ancestors of - True -> working - -- TODO(sandy): THE BUG IS THAT WE FILTER OUT FROM THE HYPOTHESIS - -- WHICH REMOVES THE EQUIVALENT OF A POSITION MAPPING; BUT THAT _USED_ - -- TO BE THERE. - False -> error $ show (broken_ancestors, ancestors, defn, pos, jHypothesis jdg) - -- broken = filterPosition' defn pos jdg - -- in case working == broken of - -- True -> working - -- False -> error $ show (working, broken) - -filterDconPosition' :: DataCon -> Int -> Judgement -> Judgement -filterDconPosition' dcon pos jdg = +filterDconPosition :: DataCon -> Int -> Judgement -> Judgement +filterDconPosition dcon pos jdg = disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg where go name _ = not . isJust - $ hasPositionalAncestry' (findDconPositionVals' jdg dcon pos) jdg name + $ hasPositionalAncestry' (findDconPositionVals jdg dcon pos) jdg name -findPositionVal' :: Judgement' a -> OccName -> Int -> Maybe OccName -findPositionVal' jdg defn pos = listToMaybe $ do +findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName +findPositionVal jdg defn pos = listToMaybe $ do (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg case hi_provenance hi of TopLevelArgPrv defn' pos' @@ -164,8 +140,8 @@ findPositionVal' jdg defn pos = listToMaybe $ do , pv_position pv == pos -> pure name _ -> [] -findDconPositionVals' :: Judgement' a -> DataCon -> Int -> [OccName] -findDconPositionVals' jdg dcon pos = do +findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName] +findDconPositionVals jdg dcon pos = do (name, hi) <- M.toList $ jHypothesis jdg case hi_provenance hi of PatternMatchPrv pv @@ -173,24 +149,14 @@ findDconPositionVals' jdg dcon pos = do , pv_position pv == pos -> pure name _ -> [] -filterSameTypeFromOtherPositions''' :: DataCon -> Int -> Judgement -> Judgement -filterSameTypeFromOtherPositions''' dcon pos jdg = filterSameTypeFromOtherPositions' dcon pos jdg - -filterSameTypeFromOtherPositions' :: DataCon -> Int -> Judgement -> Judgement -filterSameTypeFromOtherPositions' dcon pos jdg = - let hy = jHypothesis $ filterDconPosition' dcon pos jdg +filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement +filterSameTypeFromOtherPositions dcon pos jdg = + let hy = jHypothesis $ filterDconPosition dcon pos jdg tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy to_remove = M.filter (flip S.member tys . hi_type) (jHypothesis jdg) M.\\ hy in disallowing (WrongBranch pos) (M.keys to_remove) jdg -filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement -filterSameTypeFromOtherPositions defn pos jdg = - let hy = jHypothesis $ filterPosition defn pos jdg - tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy - to_remove = M.filter (flip S.member tys . hi_type) (jHypothesis jdg) M.\\ hy - in disallowing (WrongBranch pos) (M.keys to_remove) jdg - getAncestry :: Judgement' a -> OccName -> Set OccName getAncestry jdg name = @@ -244,14 +210,6 @@ extremelyStupid__definingFunction = fst . head . ctxDefiningFuncs -withHypothesis - :: (Map OccName (HyInfo a) -> Map OccName (HyInfo a)) - -> Judgement' a - -> Judgement' a -withHypothesis f = - field @"_jHypothesis" %~ f - - ------------------------------------------------------------------------------ -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of -- data sitting around in jPatternVals. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 3b1ce087e5..8e39ae41ef 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -71,7 +71,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do jdg <- goal ensure guardStructurallySmallerRecursion popRecursionStack $ do (localTactic (apply name) $ introducingRecursively defs) - <@> fmap (localTactic assumption . filterPosition''' name) [0..] + <@> fmap (localTactic assumption . filterPosition name) [0..] ------------------------------------------------------------------------------ From 3e5dc412fca227f6c1186d331fa34b057dd7e790 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 11:09:02 -0700 Subject: [PATCH 10/21] Remove _jPositionMaps --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 3 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 40 +++---------------- .../src/Ide/Plugin/Tactic/Machinery.hs | 2 +- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 9 +---- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 1 - 5 files changed, 8 insertions(+), 47 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 1e040a2fe7..eeaf560a2d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -78,8 +78,7 @@ destructMatches f scrut t jdg = do let hy' = zip names $ coerce args dcon_name = nameOccName $ dataConName dc - let j = withPositionMapping dcon_name names - $ introducingPat scrut dc hy' + let j = introducingPat scrut dc hy' $ withNewGoal g jdg (tr, sg) <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 90e8f546c3..4b53e2af0a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -91,7 +91,7 @@ introducingRecursively ns = )) -hasPositionalAncestry' +hasPositionalAncestry :: Foldable t => t OccName -> Judgement @@ -99,7 +99,7 @@ hasPositionalAncestry' -> 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 +hasPositionalAncestry ancestors jdg name | not $ null ancestors = case any (== name) ancestors of True -> Just True @@ -117,7 +117,7 @@ filterPosition defn pos jdg = go name _ = not . isJust - $ hasPositionalAncestry' (findPositionVal jdg defn pos) jdg name + $ hasPositionalAncestry (findPositionVal jdg defn pos) jdg name filterDconPosition :: DataCon -> Int -> Judgement -> Judgement filterDconPosition dcon pos jdg = @@ -126,7 +126,7 @@ filterDconPosition dcon pos jdg = go name _ = not . isJust - $ hasPositionalAncestry' (findDconPositionVals jdg dcon pos) jdg name + $ hasPositionalAncestry (findDconPositionVals jdg dcon pos) jdg name findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName findPositionVal jdg defn pos = listToMaybe $ do @@ -165,40 +165,11 @@ getAncestry jdg name = Nothing -> mempty -hasPositionalAncestry - :: Judgement - -> OccName -- ^ defining fn - -> Int -- ^ position - -> OccName -- ^ thing to check ancestry - -> Maybe Bool -- ^ Just True if the result is the oldest positional ancestor - -- just false if it's a descendent - -- otherwise nothing -hasPositionalAncestry jdg defn n name - | not $ null ancestors - = case any (== name) 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 - where - ancestors = toListOf (_Just . traversed . ix n) - $ M.lookup defn - $ _jPositionMaps jdg - - jAncestryMap :: Judgement' a -> Map OccName (Set OccName) jAncestryMap jdg = flip M.map (jPatHypothesis jdg) pv_ancestry -withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement -withPositionMapping defn names = - field @"_jPositionMaps" . at defn <>~ Just [names] - - ------------------------------------------------------------------------------ -- TODO(sandy): THIS THING IS A BIG BIG HACK -- @@ -299,13 +270,12 @@ mkFirstJudgement -> M.Map OccName [[OccName]] -- ^ existing pos vals -> Type -> Judgement' CType -mkFirstJudgement hy ambient top posvals goal = Judgement +mkFirstJudgement hy ambient top _posvals goal = Judgement { _jHypothesis = M.map mkLocalHypothesisInfo hy <> M.map mkAmbientHypothesisInfo ambient , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jDestructed = mempty - , _jPositionMaps = posvals , _jIsTopHole = top , _jGoal = CType goal } diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 26108c5cbc..8d4eee1c06 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -75,7 +75,7 @@ runTactic ctx jdg t = $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ jGoal jdg : (fmap hi_type $ toList $ jHypothesis jdg) - unused_topvals = nub $ join $ join $ toList $ _jPositionMaps jdg + unused_topvals = [] -- nub $ join $ join $ toList $ _jPositionMaps jdg tacticState = defaultTacticState { ts_skolems = skolems diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 8e39ae41ef..21844ef1b5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -91,14 +91,7 @@ intros = rule $ \jdg -> do $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs - (tr, sg) - <- newSubgoal - $ bool - id - (withPositionMapping - (extremelyStupid__definingFunction ctx) vs) - (isJust top_hole) - $ jdg' + (tr, sg) <- newSubgoal jdg' pure . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) . noLoc diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 0f76560b43..563b683a44 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -214,7 +214,6 @@ data Judgement' a = Judgement -- for nullary data constructors. , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) - , _jPositionMaps :: !(Map OccName [[OccName]]) , _jIsTopHole :: !Bool , _jGoal :: !(a) } From fb329a9f8aaa3bd2d3f3c16ce22f387ddaa08c6b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 11:16:37 -0700 Subject: [PATCH 11/21] minor cleanup --- plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 21844ef1b5..597f2db274 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -68,7 +68,6 @@ recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const $ fmap fst defs) $ \name -> do modify $ pushRecursionStack . countRecursiveCall - jdg <- goal ensure guardStructurallySmallerRecursion popRecursionStack $ do (localTactic (apply name) $ introducingRecursively defs) <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -86,8 +85,7 @@ intros = rule $ \jdg -> do (as, b) -> do vs <- mkManyGoodNames hy as let top_hole = isTopHole ctx jdg - let jdg' = traceIdX "introduced lambda" - $ introducingLambda top_hole (zip vs $ coerce as) + jdg' = introducingLambda top_hole (zip vs $ coerce as) $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs From f2d9074d0d6dbd8e5e89049dc4ad019f0bce773e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 11:36:06 -0700 Subject: [PATCH 12/21] Cleanup judgements --- .../src/Ide/Plugin/Tactic/Judgements.hs | 138 +++++++++++------- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 1 + 2 files changed, 83 insertions(+), 56 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 4b53e2af0a..c0b1b22f4a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -5,7 +5,30 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} -module Ide.Plugin.Tactic.Judgements where +module Ide.Plugin.Tactic.Judgements + ( blacklistingDestruct + , unwhitelistingSplit + , introducingLambda + , introducingRecursively + , introducingPat + , jGoal + , jHypothesis + , jPatHypothesis + , substJdg + , unsetIsTopHole + , filterSameTypeFromOtherPositions + , isDestructBlacklisted + , withNewGoal + , jLocalHypothesis + , hasDestructed + , isSplitWhitelisted + , isPatternMatch + , filterPosition + , isTopHole + , disallowing + , mkFirstJudgement + , hypothesisFromBindings + ) where import Control.Lens hiding (Context) import Data.Bool @@ -70,25 +93,27 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t +introducing + :: (Int -> Provenance) + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a +introducing f ns = + field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&> + \(pos, (name, ty)) -> (name, HyInfo (f pos) ty)) + + introducingLambda :: Maybe OccName -- ^ top level function, or Nothing for any other function -> [(OccName, a)] -> Judgement' a -> Judgement' a -introducingLambda func ns = - field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&> \(pos, (name, ty)) -> - -- TODO(sandy): cleanup - (name, HyInfo (maybe UserPrv (\x -> TopLevelArgPrv x pos) func) ty)) +introducingLambda func = introducing $ \pos -> + maybe UserPrv (\x -> TopLevelArgPrv x pos) func ------------------------------------------------------------------------------- --- | Add some terms to the ambient hypothesis introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingRecursively ns = - field @"_jHypothesis" <>~ M.fromList (ns <&> \(name, ty) -> - -- TODO(sandy): cleanup - (name, HyInfo RecursivePrv ty - )) +introducingRecursively = introducing $ const RecursivePrv hasPositionalAncestry @@ -110,26 +135,30 @@ hasPositionalAncestry ancestors jdg name Nothing -> Nothing | otherwise = Nothing -filterPosition :: OccName -> Int -> Judgement -> Judgement -filterPosition defn pos jdg = - disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg - where - go name _ - = not - . isJust - $ hasPositionalAncestry (findPositionVal jdg defn pos) jdg name -filterDconPosition :: DataCon -> Int -> Judgement -> Judgement -filterDconPosition dcon pos jdg = - disallowing (WrongBranch pos) (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg +filterAncestry + :: Foldable t + => t OccName + -> DisallowReason + -> Judgement + -> Judgement +filterAncestry ancestry reason jdg = + disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg where go name _ = not . isJust - $ hasPositionalAncestry (findDconPositionVals jdg dcon pos) jdg name + $ hasPositionalAncestry ancestry jdg name + +filterPosition :: OccName -> Int -> Judgement -> Judgement +filterPosition defn pos jdg = + filterAncestry (findPositionVal jdg defn pos) (WrongBranch pos) jdg + 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) $ jEntireHypothesis jdg case hi_provenance hi of TopLevelArgPrv defn' pos' @@ -149,12 +178,19 @@ findDconPositionVals jdg dcon pos = do , pv_position pv == pos -> pure name _ -> [] + filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions dcon pos jdg = - let hy = jHypothesis $ filterDconPosition dcon pos jdg + let hy = jHypothesis + $ filterAncestry + (findDconPositionVals jdg dcon pos) + (WrongBranch pos) + jdg tys = S.fromList $ fmap (hi_type . snd) $ M.toList hy - to_remove = M.filter (flip S.member tys . hi_type) (jHypothesis jdg) M.\\ hy - in disallowing (WrongBranch pos) (M.keys to_remove) jdg + to_remove = + M.filter (flip S.member tys . hi_type) (jHypothesis jdg) + M.\\ hy + in disallowing Shadowed (M.keys to_remove) jdg @@ -190,20 +226,18 @@ introducingPat -> [(OccName, a)] -> Judgement' a -> Judgement' a -introducingPat scrutinee dc ns jdg = jdg - & field @"_jHypothesis" <>~ (M.fromList $ zip [0..] ns <&> \(pos, (name, ty)) -> - ( name - , HyInfo - (PatternMatchPrv $ PatVal - scrutinee - (maybe - mempty - (\scrut -> S.singleton scrut <> getAncestry jdg scrut) - scrutinee) - (Uniquely dc) - pos) - ty)) - & maybe id (\scrut -> field @"_jDestructed" <>~ S.singleton scrut) scrutinee +introducingPat scrutinee dc ns jdg + = maybe id (\scrut -> field @"_jDestructed" <>~ S.singleton scrut) scrutinee + $ introducing (\pos -> + PatternMatchPrv $ + PatVal + scrutinee + (maybe mempty + (\scrut -> S.singleton scrut <> getAncestry jdg scrut) + scrutinee) + (Uniquely dc) + pos + ) ns jdg disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a @@ -271,8 +305,8 @@ mkFirstJudgement -> Type -> Judgement' CType mkFirstJudgement hy ambient top _posvals goal = Judgement - { _jHypothesis = M.map mkLocalHypothesisInfo hy - <> M.map mkAmbientHypothesisInfo ambient + { _jHypothesis = M.map (HyInfo UserPrv) hy + <> M.map (HyInfo ImportPrv) ambient , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jDestructed = mempty @@ -281,28 +315,20 @@ mkFirstJudgement hy ambient top _posvals goal = Judgement } -mkLocalHypothesisInfo :: a -> HyInfo a -mkLocalHypothesisInfo = HyInfo UserPrv - - -mkAmbientHypothesisInfo :: a -> HyInfo a -mkAmbientHypothesisInfo = HyInfo ImportPrv - - isLocalHypothesis :: Provenance -> Bool -isLocalHypothesis UserPrv{} = True +isLocalHypothesis UserPrv{} = True isLocalHypothesis PatternMatchPrv{} = True -isLocalHypothesis TopLevelArgPrv{} = True -isLocalHypothesis _ = False +isLocalHypothesis TopLevelArgPrv{} = True +isLocalHypothesis _ = False isPatternMatch :: Provenance -> Bool isPatternMatch PatternMatchPrv{} = True -isPatternMatch _ = False +isPatternMatch _ = False isDisallowed :: Provenance -> Bool isDisallowed DisallowedPrv{} = True -isDisallowed _ = False +isDisallowed _ = False expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 563b683a44..58b6ed8cbe 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -169,6 +169,7 @@ data Provenance data DisallowReason = WrongBranch Int + | Shadowed | RecursiveCall deriving stock (Eq, Show, Generic, Ord) From e4bc045aafc371c1296822c754acf0b920436c3f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 11:44:40 -0700 Subject: [PATCH 13/21] Witness structurally smaller patval for recursion --- plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 10 +++++----- plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 3 ++- plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 6 +++--- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 8d4eee1c06..69b9e4aff1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -128,8 +128,8 @@ guardStructurallySmallerRecursion -> Maybe TacticError guardStructurallySmallerRecursion s = case head $ ts_recursion_stack s of - True -> Nothing - False -> Just NoProgress + Just _ -> Nothing + Nothing -> Just NoProgress ------------------------------------------------------------------------------ @@ -137,10 +137,10 @@ guardStructurallySmallerRecursion s = -- having been matched on a pattern value. -- -- Implemented by setting the top of the 'ts_recursion_stack'. -markStructuralySmallerRecursion :: MonadState TacticState m => m () -markStructuralySmallerRecursion = do +markStructuralySmallerRecursion :: MonadState TacticState m => PatVal -> m () +markStructuralySmallerRecursion pv = do modify $ withRecursionStack $ \case - (_ : bs) -> True : bs + (_ : bs) -> Just pv : bs [] -> [] diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 597f2db274..9f3e978b26 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -20,6 +20,7 @@ import Control.Monad.Reader.Class (MonadReader(ask)) import Control.Monad.State.Class import Control.Monad.State.Strict (StateT(..), runStateT) import Data.Bool (bool) +import Data.Foldable import Data.List import qualified Data.Map as M import Data.Maybe @@ -57,7 +58,7 @@ assume name = rule $ \jdg -> do case M.lookup name $ jHypothesis jdg of Just (hi_type -> ty) -> do unify ty $ jGoal jdg - when (M.member name $ jPatHypothesis jdg) markStructuralySmallerRecursion + for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion useOccName jdg name pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name Nothing -> throwError $ UndefinedHypothesis name diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 58b6ed8cbe..ef8d823ff6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -87,7 +87,7 @@ data TacticState = TacticState -- ^ Set of values introduced by tactics. , ts_unused_top_vals :: !(Set OccName) -- ^ Set of currently unused arguments to the function being defined. - , ts_recursion_stack :: ![Bool] + , ts_recursion_stack :: ![Maybe PatVal] -- ^ Stack for tracking whether or not the current recursive call has -- used at least one smaller pat val. Recursive calls for which this -- value is 'False' are guaranteed to loop, and must be pruned. @@ -132,12 +132,12 @@ freshUnique = do withRecursionStack - :: ([Bool] -> [Bool]) -> TacticState -> TacticState + :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState withRecursionStack f = field @"ts_recursion_stack" %~ f pushRecursionStack :: TacticState -> TacticState -pushRecursionStack = withRecursionStack (False :) +pushRecursionStack = withRecursionStack (Nothing :) popRecursionStack :: TacticState -> TacticState popRecursionStack = withRecursionStack tail From 98f53e09c7b6d28ef51faf81f323629831ee4dbe Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 12:08:49 -0700 Subject: [PATCH 14/21] Remove notions of position maps from mkFirstJudgement --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 52 ++++++++++++------- .../tactics/src/Ide/Plugin/Tactic/Context.hs | 9 ++-- .../src/Ide/Plugin/Tactic/Judgements.hs | 17 +++--- .../src/Ide/Plugin/Tactic/Machinery.hs | 6 ++- plugins/tactics/test/AutoTupleSpec.hs | 6 +-- 5 files changed, 52 insertions(+), 38 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 1922d8a8ea..22b15a3c99 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -16,12 +16,15 @@ module Ide.Plugin.Tactic , TacticCommand (..) ) where +import qualified Data.Map as M +import Data.Map (Map) import Control.Arrow import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce +import Data.Functor ((<&>)) import Data.Generics.Aliases (mkQ) import Data.Generics.Schemes (everything) import Data.List @@ -264,23 +267,29 @@ judgementForHole state nfp range = do (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings binds rss) tcg - hyps = hypothesisFromBindings rss binds - ambient = M.fromList $ contextMethodHypothesis ctx + top_provs = getRhsPosVals rss tcs + local_hy = spliceProvenance top_provs + $ hypothesisFromBindings rss binds + cls_hy = contextMethodHypothesis ctx pure ( resulting_range , mkFirstJudgement - hyps - ambient + (local_hy <> cls_hy) (isRhsHole rss tcs) - (maybe - mempty - (uncurry M.singleton . fmap pure) - $ getRhsPosVals rss tcs) goal , ctx , dflags ) +spliceProvenance :: Map OccName Provenance -> Map OccName (HyInfo a) -> Map OccName (HyInfo a) +spliceProvenance provs hy = + M.mapWithKey + (\name hi -> + overProvenance + (maybe id const $ M.lookup name provs) + hi) + hy + tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) @@ -334,17 +343,22 @@ isRhsHole rss tcs = everything (||) (mkQ False $ \case ------------------------------------------------------------------------------ -- | Compute top-level position vals of a function -getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName]) -getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case - TopLevelRHS name ps - (L (RealSrcSpan span) -- body with no guards and a single defn - (HsVar _ (L _ hole))) - | containsSpan rss span -- which contains our span - , isHole $ occName hole -- and the span is a hole - -> First $ do - patnames <- traverse getPatName ps - pure (occName name, patnames) - _ -> mempty +getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance +getRhsPosVals rss tcs + = M.fromList + $ join + $ maybeToList + $ getFirst + $ everything (<>) (mkQ mempty $ \case + TopLevelRHS name ps + (L (RealSrcSpan span) -- body with no guards and a single defn + (HsVar _ (L _ hole))) + | containsSpan rss span -- which contains our span + , isHole $ occName hole -- and the span is a hole + -> First $ do + patnames <- traverse getPatName ps + pure $ zip patnames $ [0..] <&> TopLevelArgPrv name + _ -> mempty ) tcs diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs index 1621c36393..8522e0ddc4 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs @@ -7,6 +7,8 @@ import Bag import Control.Arrow import Control.Monad.Reader import Data.List +import Data.Map (Map) +import qualified Data.Map as M import Data.Maybe (mapMaybe) import Data.Set (Set) import qualified Data.Set as S @@ -33,9 +35,10 @@ mkContext locals tcg = Context ------------------------------------------------------------------------------ -- | Find all of the class methods that exist from the givens in the context. -contextMethodHypothesis :: Context -> [(OccName, CType)] +contextMethodHypothesis :: Context -> Map OccName (HyInfo CType) contextMethodHypothesis ctx - = excludeForbiddenMethods + = M.fromList + . excludeForbiddenMethods . join . concatMap ( mapMaybe methodHypothesis @@ -51,7 +54,7 @@ contextMethodHypothesis ctx -- | Many operations are defined in typeclasses for performance reasons, rather -- than being a true part of the class. This function filters out those, in -- order to keep our hypothesis space small. -excludeForbiddenMethods :: [(OccName, CType)] -> [(OccName, CType)] +excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)] excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . fst) where forbiddenMethods :: Set OccName diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index c0b1b22f4a..05bf71fd85 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -50,20 +50,20 @@ import Type ------------------------------------------------------------------------------ -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. -hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType +hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType) hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis. -buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType +buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType) buildHypothesis = M.fromList . mapMaybe go where go (occName -> occ, t) | Just ty <- t - , isAlpha . head . occNameString $ occ = Just (occ, CType ty) + , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty) | otherwise = Nothing @@ -129,7 +129,7 @@ hasPositionalAncestry ancestors jdg name = case any (== name) ancestors of True -> Just True False -> - case M.lookup name $ traceIdX "ancestry" $ jAncestryMap jdg of + case M.lookup name $ jAncestryMap jdg of Just ancestry -> bool Nothing (Just False) $ any (flip S.member ancestry) ancestors Nothing -> Nothing @@ -298,15 +298,12 @@ substJdg subst = fmap $ coerce . substTy subst . coerce mkFirstJudgement - :: M.Map OccName CType -- ^ local hypothesis - -> M.Map OccName CType -- ^ ambient hypothesis + :: M.Map OccName (HyInfo CType) -> Bool -- ^ are we in the top level rhs hole? - -> M.Map OccName [[OccName]] -- ^ existing pos vals -> Type -> Judgement' CType -mkFirstJudgement hy ambient top _posvals goal = Judgement - { _jHypothesis = M.map (HyInfo UserPrv) hy - <> M.map (HyInfo ImportPrv) ambient +mkFirstJudgement hy top goal = Judgement + { _jHypothesis = hy , _jBlacklistDestruct = False , _jWhitelistSplit = True , _jDestructed = mempty diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 69b9e4aff1..fe21a82e07 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -222,7 +222,7 @@ unify goal inst = do ------------------------------------------------------------------------------ -- | Get the class methods of a 'PredType', correctly dealing with -- instantiation of quantified class types. -methodHypothesis :: PredType -> Maybe [(OccName, CType)] +methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)] methodHypothesis ty = do (tc, apps) <- splitTyConApp_maybe ty cls <- tyConClass_maybe tc @@ -234,7 +234,9 @@ methodHypothesis ty = do $ classSCTheta cls pure $ mappend sc_methods $ methods <&> \method -> let (_, _, ty) = tcSplitSigmaTy $ idType method - in (occName method, CType $ substTy subst ty) + in ( occName method + , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty + ) ------------------------------------------------------------------------------ diff --git a/plugins/tactics/test/AutoTupleSpec.hs b/plugins/tactics/test/AutoTupleSpec.hs index 9b73c7c2f9..94125c06c4 100644 --- a/plugins/tactics/test/AutoTupleSpec.hs +++ b/plugins/tactics/test/AutoTupleSpec.hs @@ -40,12 +40,10 @@ spec = describe "auto for tuple" $ do pure $ -- We should always be able to find a solution runTactic - (Context [] []) + emptyContext (mkFirstJudgement - (M.singleton (mkVarOcc "x") $ CType in_type) - mempty + (M.singleton (mkVarOcc "x") $ HyInfo UserPrv $ CType in_type) True - mempty out_type) (auto' $ n * 2) `shouldSatisfy` isRight From 2e44b86c2a55db587b30398f95fec0c590ecb26c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 12:18:04 -0700 Subject: [PATCH 15/21] import cleanup --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 3 +- test/functional/Tactic.hs | 77 ++++++++++++------------ 2 files changed, 40 insertions(+), 40 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 22b15a3c99..018a69cd59 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -16,8 +16,6 @@ module Ide.Plugin.Tactic , TacticCommand (..) ) where -import qualified Data.Map as M -import Data.Map (Map) import Control.Arrow import Control.Monad import Control.Monad.Trans @@ -28,6 +26,7 @@ import Data.Functor ((<&>)) import Data.Generics.Aliases (mkQ) import Data.Generics.Schemes (everything) import Data.List +import Data.Map (Map) import qualified Data.Map as M import Data.Maybe import Data.Monoid diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index a37474771b..3bcf93776b 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -53,44 +53,45 @@ codeActionTitle (CACodeAction(CodeAction title _ _ _ _)) = Just title tests :: TestTree tests = testGroup "tactic" - [ mkTest - "Produces intros code action" - "T1.hs" 2 14 - [ (id, Intros, "") - ] - , mkTest - "Produces destruct and homomorphism code actions" - "T2.hs" 2 21 - [ (id, Destruct, "eab") - , (id, Homomorphism, "eab") - ] - , mkTest - "Won't suggest homomorphism on the wrong type" - "T2.hs" 8 8 - [ (not, Homomorphism, "global") - ] - , mkTest - "Won't suggest intros on the wrong type" - "T2.hs" 8 8 - [ (not, Intros, "") - ] - , mkTest - "Produces (homomorphic) lambdacase code actions" - "T3.hs" 4 24 - [ (id, HomomorphismLambdaCase, "") - , (id, DestructLambdaCase, "") - ] - , mkTest - "Produces lambdacase code actions" - "T3.hs" 7 13 - [ (id, DestructLambdaCase, "") - ] - , mkTest - "Doesn't suggest lambdacase without -XLambdaCase" - "T2.hs" 11 25 - [ (not, DestructLambdaCase, "") - ] - , goldenTest "GoldenIntros.hs" 2 8 Intros "" + [ + -- mkTest + -- "Produces intros code action" + -- "T1.hs" 2 14 + -- [ (id, Intros, "") + -- ] + -- , mkTest + -- "Produces destruct and homomorphism code actions" + -- "T2.hs" 2 21 + -- [ (id, Destruct, "eab") + -- , (id, Homomorphism, "eab") + -- ] + -- , mkTest + -- "Won't suggest homomorphism on the wrong type" + -- "T2.hs" 8 8 + -- [ (not, Homomorphism, "global") + -- ] + -- , mkTest + -- "Won't suggest intros on the wrong type" + -- "T2.hs" 8 8 + -- [ (not, Intros, "") + -- ] + -- , mkTest + -- "Produces (homomorphic) lambdacase code actions" + -- "T3.hs" 4 24 + -- [ (id, HomomorphismLambdaCase, "") + -- , (id, DestructLambdaCase, "") + -- ] + -- , mkTest + -- "Produces lambdacase code actions" + -- "T3.hs" 7 13 + -- [ (id, DestructLambdaCase, "") + -- ] + -- , mkTest + -- "Doesn't suggest lambdacase without -XLambdaCase" + -- "T2.hs" 11 25 + -- [ (not, DestructLambdaCase, "") + -- ] + goldenTest "GoldenIntros.hs" 2 8 Intros "" , goldenTest "GoldenEitherAuto.hs" 2 11 Auto "" , goldenTest "GoldenJoinCont.hs" 4 12 Auto "" , goldenTest "GoldenIdentityFunctor.hs" 3 11 Auto "" From 9ac7b27b469f67e014ef7b343b7fd23b6468ef2b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 12:18:45 -0700 Subject: [PATCH 16/21] tess --- test/functional/Tactic.hs | 77 +++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 39 deletions(-) diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 3bcf93776b..a37474771b 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -53,45 +53,44 @@ codeActionTitle (CACodeAction(CodeAction title _ _ _ _)) = Just title tests :: TestTree tests = testGroup "tactic" - [ - -- mkTest - -- "Produces intros code action" - -- "T1.hs" 2 14 - -- [ (id, Intros, "") - -- ] - -- , mkTest - -- "Produces destruct and homomorphism code actions" - -- "T2.hs" 2 21 - -- [ (id, Destruct, "eab") - -- , (id, Homomorphism, "eab") - -- ] - -- , mkTest - -- "Won't suggest homomorphism on the wrong type" - -- "T2.hs" 8 8 - -- [ (not, Homomorphism, "global") - -- ] - -- , mkTest - -- "Won't suggest intros on the wrong type" - -- "T2.hs" 8 8 - -- [ (not, Intros, "") - -- ] - -- , mkTest - -- "Produces (homomorphic) lambdacase code actions" - -- "T3.hs" 4 24 - -- [ (id, HomomorphismLambdaCase, "") - -- , (id, DestructLambdaCase, "") - -- ] - -- , mkTest - -- "Produces lambdacase code actions" - -- "T3.hs" 7 13 - -- [ (id, DestructLambdaCase, "") - -- ] - -- , mkTest - -- "Doesn't suggest lambdacase without -XLambdaCase" - -- "T2.hs" 11 25 - -- [ (not, DestructLambdaCase, "") - -- ] - goldenTest "GoldenIntros.hs" 2 8 Intros "" + [ mkTest + "Produces intros code action" + "T1.hs" 2 14 + [ (id, Intros, "") + ] + , mkTest + "Produces destruct and homomorphism code actions" + "T2.hs" 2 21 + [ (id, Destruct, "eab") + , (id, Homomorphism, "eab") + ] + , mkTest + "Won't suggest homomorphism on the wrong type" + "T2.hs" 8 8 + [ (not, Homomorphism, "global") + ] + , mkTest + "Won't suggest intros on the wrong type" + "T2.hs" 8 8 + [ (not, Intros, "") + ] + , mkTest + "Produces (homomorphic) lambdacase code actions" + "T3.hs" 4 24 + [ (id, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + , mkTest + "Produces lambdacase code actions" + "T3.hs" 7 13 + [ (id, DestructLambdaCase, "") + ] + , mkTest + "Doesn't suggest lambdacase without -XLambdaCase" + "T2.hs" 11 25 + [ (not, DestructLambdaCase, "") + ] + , goldenTest "GoldenIntros.hs" 2 8 Intros "" , goldenTest "GoldenEitherAuto.hs" 2 11 Auto "" , goldenTest "GoldenJoinCont.hs" 4 12 Auto "" , goldenTest "GoldenIdentityFunctor.hs" 3 11 Auto "" From 003d311019494225fa8528d67a4cd593037a38f9 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 13:00:02 -0700 Subject: [PATCH 17/21] make ts_skolems a set --- .../src/Ide/Plugin/Tactic/Machinery.hs | 23 ++++++++----------- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 2 +- 2 files changed, 11 insertions(+), 14 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index fe21a82e07..2cc9219971 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -25,13 +25,15 @@ import Control.Monad.Reader import Control.Monad.State (MonadState(..)) import Control.Monad.State.Class (gets, modify) import Control.Monad.State.Strict (StateT (..)) +import Data.Bool (bool) import Data.Coerce import Data.Either import Data.Foldable import Data.Functor ((<&>)) import Data.Generics (mkQ, everything, gcount) -import Data.List (nub, sortBy) +import Data.List (sortBy) import Data.Ord (comparing, Down(..)) +import Data.Set (Set) import qualified Data.Set as S import Development.IDE.GHC.Compat import Ide.Plugin.Tactic.Judgements @@ -71,7 +73,7 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either [TacticError] RunTacticResults runTactic ctx jdg t = - let skolems = nub + let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ jGoal jdg : (fmap hi_type $ toList $ jHypothesis jdg) @@ -190,21 +192,16 @@ newtype Reward a = Reward a ------------------------------------------------------------------------------ -- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. -tryUnifyUnivarsButNotSkolems :: [TyVar] -> CType -> CType -> Maybe TCvSubst +tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst tryUnifyUnivarsButNotSkolems skolems goal inst = - case tcUnifyTysFG (skolemsOf skolems) [unCType inst] [unCType goal] of + case tcUnifyTysFG + (bool BindMe Skolem . flip S.member skolems) + [unCType inst] + [unCType goal] of Unifiable subst -> pure subst _ -> Nothing ------------------------------------------------------------------------------- --- | Helper method for 'tryUnifyUnivarsButNotSkolems' -skolemsOf :: [TyVar] -> TyVar -> BindFlag -skolemsOf tvs tv = - case elem tv tvs of - True -> Skolem - False -> BindMe - ------------------------------------------------------------------------------ -- | Attempt to unify two types. @@ -245,7 +242,7 @@ methodHypothesis ty = do requireConcreteHole :: TacticsM a -> TacticsM a requireConcreteHole m = do jdg <- goal - skolems <- gets $ S.fromList . ts_skolems + skolems <- gets ts_skolems let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg case S.size $ vars S.\\ skolems of 0 -> m diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index ef8d823ff6..1aea3015fd 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -77,7 +77,7 @@ instance Show Class where ------------------------------------------------------------------------------ data TacticState = TacticState - { ts_skolems :: !([TyVar]) + { ts_skolems :: !(Set TyVar) -- ^ The known skolems. , ts_unifier :: !(TCvSubst) -- ^ The current substitution of univars. From b807641ab45f8c5e285cfb95b5c0d8af080ba9dc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 13:09:41 -0700 Subject: [PATCH 18/21] Check usage of toplevel vals --- .../src/Ide/Plugin/Tactic/Judgements.hs | 7 ++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 12 ++++--- plugins/tactics/test/UnificationSpec.hs | 33 ++++++++++--------- 3 files changed, 31 insertions(+), 21 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 05bf71fd85..9894ce4bd4 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -28,6 +28,7 @@ module Ide.Plugin.Tactic.Judgements , disallowing , mkFirstJudgement , hypothesisFromBindings + , isTopLevel ) where import Control.Lens hiding (Context) @@ -312,6 +313,10 @@ mkFirstJudgement hy top goal = Judgement } +isTopLevel :: Provenance -> Bool +isTopLevel TopLevelArgPrv{} = True +isTopLevel _ = False + isLocalHypothesis :: Provenance -> Bool isLocalHypothesis UserPrv{} = True isLocalHypothesis PatternMatchPrv{} = True @@ -323,10 +328,12 @@ isPatternMatch :: Provenance -> Bool isPatternMatch PatternMatchPrv{} = True isPatternMatch _ = False + isDisallowed :: Provenance -> Bool isDisallowed DisallowedPrv{} = True isDisallowed _ = False + expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv expandDisallowed prv = prv diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 2cc9219971..ffc96378fb 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -32,6 +32,7 @@ import Data.Foldable import Data.Functor ((<&>)) import Data.Generics (mkQ, everything, gcount) import Data.List (sortBy) +import qualified Data.Map as M import Data.Ord (comparing, Down(..)) import Data.Set (Set) import qualified Data.Set as S @@ -77,11 +78,13 @@ runTactic ctx jdg t = $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ jGoal jdg : (fmap hi_type $ toList $ jHypothesis jdg) - unused_topvals = [] -- nub $ join $ join $ toList $ _jPositionMaps jdg + unused_topvals = M.keysSet + $ M.filter (isTopLevel . hi_provenance) + $ jHypothesis jdg tacticState = defaultTacticState { ts_skolems = skolems - , ts_unused_top_vals = S.fromList unused_topvals + , ts_unused_top_vals = unused_topvals } in case partitionEithers . flip runReader ctx @@ -122,9 +125,8 @@ tracing s (TacticT m) ------------------------------------------------------------------------------ -- | Recursion is allowed only when we can prove it is on a structurally --- smaller argument. The top of the 'ts_recursion_stack' is set to 'True' iff --- one of the recursive arguments is a pattern val (ie. came from a pattern --- match.) +-- smaller argument. The top of the 'ts_recursion_stack' witnesses the smaller +-- pattern val. guardStructurallySmallerRecursion :: TacticState -> Maybe TacticError diff --git a/plugins/tactics/test/UnificationSpec.hs b/plugins/tactics/test/UnificationSpec.hs index 9351725036..a5a21567ae 100644 --- a/plugins/tactics/test/UnificationSpec.hs +++ b/plugins/tactics/test/UnificationSpec.hs @@ -3,21 +3,22 @@ module UnificationSpec where -import Control.Arrow -import Data.Bool (bool) -import Data.Functor ((<&>)) -import Data.Maybe (mapMaybe) -import Data.Traversable -import Data.Tuple (swap) -import Ide.Plugin.Tactic.Debug -import Ide.Plugin.Tactic.Machinery -import Ide.Plugin.Tactic.Types -import TcType (tcGetTyVar_maybe, substTy) -import Test.Hspec -import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) -import TysWiredIn (mkBoxedTupleTy) +import Control.Arrow +import Data.Bool (bool) +import Data.Functor ((<&>)) +import Data.Maybe (mapMaybe) +import qualified Data.Set as S +import Data.Traversable +import Data.Tuple (swap) +import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Types +import TcType (tcGetTyVar_maybe, substTy) +import Test.Hspec +import Test.QuickCheck +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) instance Show Type where @@ -42,7 +43,7 @@ spec = describe "unification" $ do counterexample (show lhs) $ counterexample (show rhs) $ case tryUnifyUnivarsButNotSkolems - (mapMaybe tcGetTyVar_maybe skolems) + (S.fromList $ mapMaybe tcGetTyVar_maybe skolems) (CType lhs) (CType rhs) of Just subst -> From c3cfcaa3706ab95d9a67df7f972b0492b4bb8b3a Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 13:13:19 -0700 Subject: [PATCH 19/21] Minor styling --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 15 +++++++-------- .../tactics/src/Ide/Plugin/Tactic/Machinery.hs | 6 ++++-- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 018a69cd59..c5744e811a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -280,14 +280,13 @@ judgementForHole state nfp range = do ) -spliceProvenance :: Map OccName Provenance -> Map OccName (HyInfo a) -> Map OccName (HyInfo a) -spliceProvenance provs hy = - M.mapWithKey - (\name hi -> - overProvenance - (maybe id const $ M.lookup name provs) - hi) - hy +spliceProvenance + :: Map OccName Provenance + -> Map OccName (HyInfo a) + -> Map OccName (HyInfo a) +spliceProvenance provs = + M.mapWithKey $ \name hi -> + overProvenance (maybe id const $ M.lookup name provs) hi tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index ffc96378fb..22ef2b6b5e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -76,8 +76,10 @@ runTactic runTactic ctx jdg t = let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) - $ jGoal jdg - : (fmap hi_type $ toList $ jHypothesis jdg) + $ (:) (jGoal jdg) + $ fmap hi_type + $ toList + $ jHypothesis jdg unused_topvals = M.keysSet $ M.filter (isTopLevel . hi_provenance) $ jHypothesis jdg From 92119dcc2cc5f9a5caca1670f9bb190e45687c30 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 13:35:38 -0700 Subject: [PATCH 20/21] Haddock for judgements and types --- .../src/Ide/Plugin/Tactic/Judgements.hs | 60 +++++++++++++++++-- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 37 ++++++++++-- 2 files changed, 87 insertions(+), 10 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 9894ce4bd4..173e7a8214 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -68,6 +68,8 @@ buildHypothesis | otherwise = Nothing +------------------------------------------------------------------------------ +-- | Has the given 'OccName' already been destructed? hasDestructed :: Judgement' a -> OccName -> Bool hasDestructed jdg n = S.member n $ _jDestructed jdg @@ -94,8 +96,11 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t +------------------------------------------------------------------------------ +-- | Helper function for implementing functions which introduce new hypotheses. introducing - :: (Int -> Provenance) + :: (Int -> Provenance) -- ^ A function from the position of the arg to its + -- provenance. -> [(OccName, a)] -> Judgement' a -> Judgement' a @@ -104,8 +109,11 @@ introducing f ns = \(pos, (name, ty)) -> (name, HyInfo (f pos) ty)) +------------------------------------------------------------------------------ +-- | Introduce bindings in the context of a lamba. introducingLambda - :: Maybe OccName -- ^ top level function, or Nothing for any other function + :: Maybe OccName -- ^ The name of the top level function. For any other + -- function, this should be 'Nothing'. -> [(OccName, a)] -> Judgement' a -> Judgement' a @@ -113,15 +121,19 @@ introducingLambda func = introducing $ \pos -> maybe UserPrv (\x -> TopLevelArgPrv x pos) func +------------------------------------------------------------------------------ +-- | Introduce a binding in a recursive context. introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a introducingRecursively = introducing $ const RecursivePrv +------------------------------------------------------------------------------ +-- | Check whether any of the given occnames are an ancestor of the term. hasPositionalAncestry :: Foldable t - => t OccName + => t OccName -- ^ Desired ancestors. -> Judgement - -> OccName -- ^ thing to check ancestry + -> OccName -- ^ Potential child -> Maybe Bool -- ^ Just True if the result is the oldest positional ancestor -- just false if it's a descendent -- otherwise nothing @@ -137,6 +149,8 @@ hasPositionalAncestry ancestors jdg name | otherwise = Nothing +------------------------------------------------------------------------------ +-- | Helper function for disallowing hypotheses that have the wrong ancestry. filterAncestry :: Foldable t => t OccName @@ -151,11 +165,18 @@ filterAncestry ancestry reason jdg = . isJust $ 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 @@ -170,6 +191,10 @@ findPositionVal jdg defn pos = listToMaybe $ do , pv_position pv == pos -> pure name _ -> [] + +------------------------------------------------------------------------------ +-- | Helper function for determining the ancestry list for +-- 'filterSameTypeFromOtherPositions'. findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName] findDconPositionVals jdg dcon pos = do (name, hi) <- M.toList $ jHypothesis jdg @@ -180,6 +205,11 @@ findDconPositionVals jdg dcon pos = do _ -> [] +------------------------------------------------------------------------------ +-- | 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 :: DataCon -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions dcon pos jdg = let hy = jHypothesis @@ -194,7 +224,8 @@ filterSameTypeFromOtherPositions dcon pos jdg = in disallowing Shadowed (M.keys to_remove) jdg - +------------------------------------------------------------------------------ +-- | Return the ancestry of a 'PatVal', or 'mempty' otherwise. getAncestry :: Judgement' a -> OccName -> Set OccName getAncestry jdg name = case M.lookup name $ jPatHypothesis jdg of @@ -241,6 +272,9 @@ introducingPat scrutinee dc ns jdg ) ns jdg +------------------------------------------------------------------------------ +-- | Prevent some occnames from being used in the hypothesis. This will hide +-- them from 'jHypothesis', but not from 'jEntireHypothesis'. disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a disallowing reason (S.fromList -> ns) = field @"_jHypothesis" %~ (M.mapWithKey $ \name hi -> @@ -252,7 +286,7 @@ disallowing reason (S.fromList -> ns) = ------------------------------------------------------------------------------ -- | The hypothesis, consisting of local terms and the ambient environment --- (includes and class methods.) +-- (impors and class methods.) Hides disallowed values. jHypothesis :: Judgement' a -> Map OccName (HyInfo a) jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis @@ -269,10 +303,13 @@ jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a) jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis +------------------------------------------------------------------------------ +-- | 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 @@ -313,10 +350,15 @@ mkFirstJudgement hy top goal = Judgement } +------------------------------------------------------------------------------ +-- | 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 @@ -324,16 +366,22 @@ 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 +------------------------------------------------------------------------------ +-- | Eliminates 'DisallowedPrv' provenances. expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv expandDisallowed prv = prv diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index 1aea3015fd..b76ce91f5d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -153,20 +153,35 @@ withIntroducedVals f = field @"ts_intro_vals" %~ f +------------------------------------------------------------------------------ +-- | Describes where hypotheses came from. Used extensively to prune stupid +-- solutions from the search space. data Provenance - = TopLevelArgPrv - OccName -- ^ Function name - Int -- ^ Position + = -- | An argument given to the topmost function that contains the current + -- hole. Recursive calls are restricted to values whose provenance lines up + -- with the same argument. + TopLevelArgPrv + OccName -- ^ Binding function + Int -- ^ Argument Position + -- | A binding created in a pattern match. | PatternMatchPrv PatVal + -- | A class method from the given context. | ClassMethodPrv (Uniquely Class) -- ^ Class + -- | A binding explicitly written by the user. | UserPrv - | ImportPrv + -- | The recursive hypothesis. Present only in the context of the recursion + -- tactic. | RecursivePrv + -- | A hypothesis which has been disallowed for some reason. It's important + -- to keep these in the hypothesis set, rather than filtering it, in order + -- to continue tracking downstream provenance. | DisallowedPrv DisallowReason Provenance deriving stock (Eq, Show, Generic, Ord) +------------------------------------------------------------------------------ +-- | Why was a hypothesis disallowed? data DisallowReason = WrongBranch Int | Shadowed @@ -174,16 +189,25 @@ data DisallowReason deriving stock (Eq, Show, Generic, Ord) +------------------------------------------------------------------------------ +-- | Provenance of a pattern value. data PatVal = PatVal { pv_scrutinee :: Maybe OccName -- ^ Original scrutinee which created this PatVal. Nothing, for lambda -- case. , pv_ancestry :: Set OccName + -- ^ The set of values which had to be destructed to discover this term. + -- Always contains the scrutinee. , pv_datacon :: Uniquely DataCon + -- ^ The datacon which introduced this term. , pv_position :: Int + -- ^ The position of this binding in the datacon's arguments. } deriving stock (Eq, Show, Generic, Ord) +------------------------------------------------------------------------------ +-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord' +-- instances. newtype Uniquely a = Uniquely { getViaUnique :: a } deriving Show via a @@ -194,12 +218,17 @@ instance Uniquable a => Ord (Uniquely a) where compare = nonDetCmpUnique `on` getUnique . getViaUnique +------------------------------------------------------------------------------ +-- | The provenance and type of a hypothesis term. data HyInfo a = HyInfo { hi_provenance :: Provenance , hi_type :: a } deriving stock (Functor, Eq, Show, Generic, Ord) + +------------------------------------------------------------------------------ +-- | Map a function over the provenance. overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty From 58eece0551eeb539e2432c40356a9eb0d2cfb8dd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 30 Oct 2020 13:57:36 -0700 Subject: [PATCH 21/21] Remove _jDestructed --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 8 ++--- .../src/Ide/Plugin/Tactic/Judgements.hs | 12 ++----- .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 34 ++++++++----------- .../tactics/src/Ide/Plugin/Tactic/Types.hs | 9 +---- 4 files changed, 20 insertions(+), 43 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index eeaf560a2d..ec8caf8a9b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -64,7 +64,7 @@ destructMatches -> Judgement -> RuleM (Trace, [RawMatch]) destructMatches f scrut t jdg = do - let hy = jHypothesis jdg + let hy = jEntireHypothesis jdg g = jGoal jdg case splitTyConApp_maybe $ unCType t of Nothing -> throwError $ GoalMismatch "destruct" g @@ -76,9 +76,7 @@ destructMatches f scrut t jdg = do let args = dataConInstOrigArgTys' dc apps names <- mkManyGoodNames hy args let hy' = zip names $ coerce args - dcon_name = nameOccName $ dataConName dc - - let j = introducingPat scrut dc hy' + j = introducingPat scrut dc hy' $ withNewGoal g jdg (tr, sg) <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names @@ -147,7 +145,7 @@ destruct' f term jdg = do f (Just term) t - jdg + $ disallowing AlreadyDestructed [term] jdg pure ( rose ("destruct " <> show term) $ pure tr , noLoc $ case' (var' term) ms ) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 173e7a8214..d4fdc6fa00 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -13,6 +13,7 @@ module Ide.Plugin.Tactic.Judgements , introducingPat , jGoal , jHypothesis + , jEntireHypothesis , jPatHypothesis , substJdg , unsetIsTopHole @@ -20,7 +21,6 @@ module Ide.Plugin.Tactic.Judgements , isDestructBlacklisted , withNewGoal , jLocalHypothesis - , hasDestructed , isSplitWhitelisted , isPatternMatch , filterPosition @@ -68,12 +68,6 @@ buildHypothesis | otherwise = Nothing ------------------------------------------------------------------------------- --- | Has the given 'OccName' already been destructed? -hasDestructed :: Judgement' a -> OccName -> Bool -hasDestructed jdg n = S.member n $ _jDestructed jdg - - blacklistingDestruct :: Judgement -> Judgement blacklistingDestruct = field @"_jBlacklistDestruct" .~ True @@ -259,8 +253,7 @@ introducingPat -> Judgement' a -> Judgement' a introducingPat scrutinee dc ns jdg - = maybe id (\scrut -> field @"_jDestructed" <>~ S.singleton scrut) scrutinee - $ introducing (\pos -> + = introducing (\pos -> PatternMatchPrv $ PatVal scrutinee @@ -344,7 +337,6 @@ mkFirstJudgement hy top goal = Judgement { _jHypothesis = hy , _jBlacklistDestruct = False , _jWhitelistSplit = True - , _jDestructed = mempty , _jIsTopHole = top , _jGoal = CType goal } diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 9f3e978b26..8f6de3ebce 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -84,7 +84,7 @@ intros = rule $ \jdg -> do case tcSplitFunTys $ unCType g of ([], _) -> throwError $ GoalMismatch "intros" g (as, b) -> do - vs <- mkManyGoodNames hy as + vs <- mkManyGoodNames (jEntireHypothesis jdg) as let top_hole = isTopHole ctx jdg jdg' = introducingLambda top_hole (zip vs $ coerce as) $ withNewGoal (CType b) jdg @@ -106,30 +106,24 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do case M.lookup name $ jHypothesis jdg of Nothing -> throwError $ NotInScope name Just hi -> - case hasDestructed jdg name of - True -> throwError $ AlreadyDestructed name - False -> - let subtactic = rule $ destruct' (const subgoal) name - in case isPatternMatch $ hi_provenance hi of - True -> - pruning subtactic $ \jdgs -> - let getHyTypes = S.fromList . fmap (hi_type . snd) . M.toList . jHypothesis - new_hy = foldMap getHyTypes jdgs - old_hy = getHyTypes jdg - in case S.null $ new_hy S.\\ old_hy of - True -> Just $ UnhelpfulDestruct name - False -> Nothing - False -> subtactic + let subtactic = rule $ destruct' (const subgoal) name + in case isPatternMatch $ hi_provenance hi of + True -> + pruning subtactic $ \jdgs -> + let getHyTypes = S.fromList . fmap (hi_type . snd) . M.toList . jHypothesis + new_hy = foldMap getHyTypes jdgs + old_hy = getHyTypes jdg + in case S.null $ new_hy S.\\ old_hy of + True -> Just $ UnhelpfulDestruct name + False -> Nothing + False -> subtactic ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destruct :: OccName -> TacticsM () -destruct name = requireConcreteHole $ tracing "destruct(user)" $ do - jdg <- goal - case hasDestructed jdg name of - True -> throwError $ AlreadyDestructed name - False -> rule $ \jdg -> destruct' (const subgoal) name jdg +destruct name = requireConcreteHole $ tracing "destruct(user)" $ + rule $ destruct' (const subgoal) name ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index b76ce91f5d..95e80f004f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -186,6 +186,7 @@ data DisallowReason = WrongBranch Int | Shadowed | RecursiveCall + | AlreadyDestructed deriving stock (Eq, Show, Generic, Ord) @@ -237,11 +238,6 @@ overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement { _jHypothesis :: !(Map OccName (HyInfo a)) - , _jDestructed :: !(Set OccName) - -- ^ Set of names we've already destructed. These should align with keys of - -- _jHypothesis. You might think we could just inspect the hypothesis and - -- find any PatVals whose scrutinee is the name in question, but this fails - -- for nullary data constructors. , _jBlacklistDestruct :: !(Bool) , _jWhitelistSplit :: !(Bool) , _jIsTopHole :: !Bool @@ -270,7 +266,6 @@ data TacticError | UnificationError CType CType | NoProgress | NoApplicableTactic - | AlreadyDestructed OccName | IncorrectDataCon DataCon | RecursionOnWrongParam OccName Int OccName | UnhelpfulDestruct OccName @@ -302,8 +297,6 @@ instance Show TacticError where "Unable to make progress" show NoApplicableTactic = "No tactic could be applied" - show (AlreadyDestructed name) = - "Already destructed " <> unsafeRender name show (IncorrectDataCon dcon) = "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")" show (RecursionOnWrongParam call p arg) =