From 29cb0ad2477a7f06540c74a9b2fef8e1d514ac15 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 28 Oct 2020 21:23:56 -0700 Subject: [PATCH 1/8] 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 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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.