diff --git a/cabal.project b/cabal.project index 669375a7da..7d23377471 100644 --- a/cabal.project +++ b/cabal.project @@ -25,6 +25,6 @@ package ghcide write-ghc-environment-files: never -index-state: 2020-10-08T12:51:21Z +index-state: 2020-10-16T04:00:00Z allow-newer: data-tree-print:base diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index ea3e80cd87..4f75fad4c6 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -94,11 +94,13 @@ executable haskell-language-server Ide.Plugin.Retrie Ide.Plugin.StylishHaskell Ide.Plugin.Tactic + Ide.Plugin.Tactic.Auto Ide.Plugin.Tactic.CodeGen Ide.Plugin.Tactic.Context Ide.Plugin.Tactic.Debug Ide.Plugin.Tactic.GHC Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.KnownStrategies Ide.Plugin.Tactic.Machinery Ide.Plugin.Tactic.Naming Ide.Plugin.Tactic.Range @@ -156,9 +158,10 @@ executable haskell-language-server , transformers , unordered-containers , ghc-source-gen - , refinery ^>=0.2 + , refinery ^>=0.3 , ghc-exactprint , fingertree + , generic-lens if flag(agpl) build-depends: brittany diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 199cc1a609..82b91d942b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -1,7 +1,9 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NumDecimals #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} @@ -20,8 +22,12 @@ import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce +import Data.Generics.Aliases (mkQ) +import Data.Generics.Schemes (everything) +import Data.List import qualified Data.Map as M import Data.Maybe +import Data.Monoid import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable @@ -38,6 +44,7 @@ import qualified FastString import GHC.Generics (Generic) import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin (mkLspCommand) +import Ide.Plugin.Tactic.Auto import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements @@ -50,6 +57,8 @@ import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) import Language.Haskell.LSP.Types import OccName +import SrcLoc (containsSpan) +import System.Timeout descriptor :: PluginId -> PluginDescriptor @@ -250,12 +259,24 @@ judgementForHole state nfp range = do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp let tcg = fst $ tm_internals_ $ tmrModule tcmod + tcs = tm_typechecked_source $ tmrModule tcmod ctx = mkContext (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings binds rss) tcg hyps = hypothesisFromBindings rss binds - pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags) + pure ( resulting_range + , mkFirstJudgement + hyps + (isRhsHole rss tcs) + (maybe + mempty + (uncurry M.singleton . fmap pure) + $ getRhsPosVals rss tcs) + goal + , ctx + , dflags + ) @@ -266,20 +287,26 @@ tacticCmd tac lf state (TacticParams uri range var_name) (range', jdg, ctx, dflags) <- judgementForHole state nfp range let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp - case runTactic ctx jdg - $ tac - $ mkVarOcc - $ T.unpack var_name of - Left err -> - pure $ (, Nothing) - $ Left - $ ResponseError InvalidRequest (T.pack $ show err) Nothing - Right res -> do - let g = graft (RealSrcSpan span) res - response = transform dflags (clientCapabilities lf) uri g pm - pure $ case response of - Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) - Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) + x <- lift $ timeout 2e8 $ + case runTactic ctx jdg + $ tac + $ mkVarOcc + $ T.unpack var_name of + Left err -> + pure $ (, Nothing) + $ Left + $ ResponseError InvalidRequest (T.pack $ show err) Nothing + Right (_, ext) -> do + let g = graft (RealSrcSpan span) ext + response = transform dflags (clientCapabilities lf) uri g pm + pure $ case response of + Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) + Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) + pure $ case x of + Just y -> y + Nothing -> (, Nothing) + $ Left + $ ResponseError InvalidRequest "timed out" Nothing tacticCmd _ _ _ _ = pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing , Nothing @@ -292,3 +319,34 @@ fromMaybeT def = fmap (fromMaybe def) . runMaybeT liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a + +------------------------------------------------------------------------------ +-- | Is this hole immediately to the right of an equals sign? +isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool +isRhsHole rss tcs = everything (||) (mkQ False $ \case + TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span + _ -> False + ) tcs + + +------------------------------------------------------------------------------ +-- | 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 + ) tcs + + + +-- TODO(sandy): Make this more robust +isHole :: OccName -> Bool +isHole = isPrefixOf "_" . occNameString + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs new file mode 100644 index 0000000000..0a22255e60 --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs @@ -0,0 +1,25 @@ +module Ide.Plugin.Tactic.Auto where + +import Ide.Plugin.Tactic.Context +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.KnownStrategies +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types +import Refinery.Tactic +import Ide.Plugin.Tactic.Machinery (tracing) + + +------------------------------------------------------------------------------ +-- | Automatically solve a goal. +auto :: TacticsM () +auto = do + jdg <- goal + current <- getCurrentDefinitions + traceMX "goal" jdg + traceMX "ctx" current + commit knownStrategies + . tracing "auto" + . localTactic (auto' 4) + . disallowing + $ fmap fst current + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 156673f5fe..f89a9964dd 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -1,33 +1,45 @@ +{-# LANGUAGE TupleSections #-} {-# LANGUAGE FlexibleContexts #-} module Ide.Plugin.Tactic.CodeGen where -import Control.Monad.Except -import Data.List -import Data.Traversable -import DataCon -import Development.IDE.GHC.Compat -import GHC.Exts -import GHC.SourceGen.Binds -import GHC.SourceGen.Expr -import GHC.SourceGen.Overloaded -import GHC.SourceGen.Pat -import Ide.Plugin.Tactic.Judgements -import Ide.Plugin.Tactic.Machinery -import Ide.Plugin.Tactic.Naming -import Ide.Plugin.Tactic.Types -import Name -import Type hiding (Var) +import Control.Monad.Except +import Control.Monad.State (MonadState) +import Control.Monad.State.Class (modify) +import Data.List +import qualified Data.Map as M +import qualified Data.Set as S +import Data.Traversable +import DataCon +import Development.IDE.GHC.Compat +import GHC.Exts +import GHC.SourceGen.Binds +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Naming +import Ide.Plugin.Tactic.Types +import Name +import Type hiding (Var) + + +useOccName :: MonadState TacticState m => Judgement -> OccName -> m () +useOccName jdg name = + case M.lookup name $ jHypothesis jdg of + Just{} -> modify $ withUsedVals $ S.insert name + Nothing -> pure () destructMatches :: (DataCon -> Judgement -> Rule) -- ^ How to construct each match - -> (Judgement -> Judgement) + -> ([(OccName, CType)] -> Judgement -> Judgement) -- ^ How to derive each match judgement -> CType -- ^ Type being destructed -> Judgement - -> RuleM [RawMatch] + -> RuleM (Trace, [RawMatch]) destructMatches f f2 t jdg = do let hy = jHypothesis jdg g = jGoal jdg @@ -37,18 +49,32 @@ destructMatches f f2 t jdg = do let dcs = tyConDataCons tc case dcs of [] -> throwError $ GoalMismatch "destruct" g - _ -> for dcs $ \dc -> do + _ -> fmap unzipTrace $ for dcs $ \dc -> do let args = dataConInstOrigArgTys' dc apps names <- mkManyGoodNames hy args + let hy' = zip names $ coerce args + dcon_name = nameOccName $ dataConName dc let pat :: Pat GhcPs - pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + pat = conP (fromString $ occNameString dcon_name) $ fmap bvar' names - j = f2 - $ introducingPat (zip names $ coerce args) + j = f2 hy' + $ withPositionMapping dcon_name names + $ introducingPat hy' $ withNewGoal g jdg - sg <- f dc j - pure $ match [pat] $ unLoc sg + (tr, sg) <- f dc j + modify $ withIntroducedVals $ mappend $ S.fromList names + pure ( rose ("match " <> show dc <> " {" <> + intercalate ", " (fmap show names) <> "}") + $ pure tr + , match [pat] $ unLoc sg + ) + + +unzipTrace :: [(Trace, a)] -> (Trace, [a]) +unzipTrace l = + let (trs, as) = unzip l + in (rose mempty trs, as) -- | Essentially same as 'dataConInstOrigArgTys' in GHC, @@ -66,12 +92,21 @@ dataConInstOrigArgTys' con ty = destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule destruct' f term jdg = do + when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let hy = jHypothesis jdg case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term - Just (_, t) -> - fmap noLoc $ case' (var' term) <$> - destructMatches f (destructing term) t jdg + Just (_, t) -> do + useOccName jdg term + (tr, ms) + <- destructMatches + f + (\cs -> setParents term (fmap fst cs) . destructing term) + t + jdg + pure ( rose ("destruct " <> show term) $ pure tr + , noLoc $ case' (var' term) ms + ) ------------------------------------------------------------------------------ @@ -79,11 +114,12 @@ destruct' f term jdg = do -- resulting matches. destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule destructLambdaCase' f jdg = do + when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let g = jGoal jdg case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> - fmap noLoc $ lambdaCase <$> - destructMatches f id (CType arg) jdg + fmap (fmap noLoc $ lambdaCase) <$> + destructMatches f (const id) (CType arg) jdg _ -> throwError $ GoalMismatch "destructLambdaCase'" g @@ -93,11 +129,21 @@ buildDataCon :: Judgement -> DataCon -- ^ The data con to build -> [Type] -- ^ Type arguments for the data con - -> RuleM (LHsExpr GhcPs) + -> RuleM (Trace, LHsExpr GhcPs) buildDataCon jdg dc apps = do let args = dataConInstOrigArgTys' dc apps - sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args + dcon_name = nameOccName $ dataConName dc + (tr, sgs) + <- fmap unzipTrace + $ traverse ( \(arg, n) -> + newSubgoal + . filterSameTypeFromOtherPositions dcon_name n + . blacklistingDestruct + . flip withNewGoal jdg + $ CType arg + ) $ zip args [0..] pure + . (rose (show dc) $ pure tr,) . noLoc . foldl' (@@) (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) @@ -109,7 +155,9 @@ buildDataCon jdg dc apps = do var' :: Var a => OccName -> a var' = var . fromString . occNameString + ------------------------------------------------------------------------------ -- | Like 'bvar', but works over standard GHC 'OccName's. bvar' :: BVar a => OccName -> a bvar' = bvar . fromString . occNameString + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs index f1cccae928..2c8b48227a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs @@ -34,8 +34,8 @@ getFunBindId (AbsBinds _ _ _ abes _ _ _) getFunBindId _ = [] -getCurrentDefinitions :: MonadReader Context m => m [OccName] -getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs +getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] +getCurrentDefinitions = asks $ ctxDefiningFuncs getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] getModuleHypothesis = asks ctxModuleFuncs diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs index 6d1053c2c6..ba91a7c1cb 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs @@ -4,11 +4,14 @@ module Ide.Plugin.Tactic.Debug , traceM , traceShowId , trace + , traceX + , traceIdX + , traceMX ) where import Debug.Trace import DynFlags (unsafeGlobalDynFlags) -import Outputable +import Outputable hiding ((<>)) ------------------------------------------------------------------------------ -- | Print something @@ -18,3 +21,12 @@ unsafeRender = unsafeRender' . ppr unsafeRender' :: SDoc -> String unsafeRender' = showSDoc unsafeGlobalDynFlags +traceMX :: (Monad m, Show a) => String -> a -> m () +traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a + +traceX :: (Show a) => String -> a -> b -> b +traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) + +traceIdX :: (Show a) => String -> a -> a +traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 9d1c34851b..7f89e4c0c9 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -1,11 +1,14 @@ -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} module Ide.Plugin.Tactic.GHC where import Data.Maybe (isJust) +import Development.IDE.GHC.Compat +import OccName import TcType import TyCoRep -import TyCon import Type import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon) import Unique @@ -67,3 +70,39 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res)) = Just $ isJust $ algebraicTyCon res lambdaCaseable _ = Nothing +fromPatCompat :: PatCompat GhcTc -> Pat GhcTc +#if __GLASGOW_HASKELL__ == 808 +type PatCompat pass = Pat pass +fromPatCompat = id +#else +type PatCompat pass = LPat pass +fromPatCompat = unLoc +#endif + +------------------------------------------------------------------------------ +-- | Should make sure it's a fun bind +pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc) +pattern TopLevelRHS name ps body <- + Match _ + (FunRhs (L _ (occName -> name)) _ _) + ps + (GRHSs _ + [L _ (GRHS _ [] body)] _) + +getPatName :: PatCompat GhcTc -> Maybe OccName +getPatName (fromPatCompat -> p0) = + case p0 of + VarPat _ x -> Just $ occName $ unLoc x + LazyPat _ p -> getPatName p + AsPat _ x _ -> Just $ occName $ unLoc x + ParPat _ p -> getPatName p + BangPat _ p -> getPatName p + ViewPat _ _ p -> getPatName p +#if __GLASGOW_HASKELL__ >= 808 + SigPat _ p _ -> getPatName p +#endif +#if __GLASGOW_HASKELL__ == 808 + XPat p -> getPatName $ unLoc p +#endif + _ -> Nothing + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs index 51c1cef988..32ad70bc2e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs @@ -1,10 +1,16 @@ -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} module Ide.Plugin.Tactic.Judgements where +import Control.Lens hiding (Context) +import Data.Bool import Data.Char import Data.Coerce +import Data.Generics.Product (field) import Data.Map (Map) import qualified Data.Map as M import Data.Maybe @@ -37,39 +43,139 @@ buildHypothesis hasDestructed :: Judgement -> OccName -> Bool hasDestructed j n = S.member n $ _jDestructed j + destructing :: OccName -> Judgement -> Judgement -destructing n jdg@Judgement{..} = jdg - { _jDestructed = _jDestructed <> S.singleton n - } +destructing n = field @"_jDestructed" <>~ S.singleton n + + +blacklistingDestruct :: Judgement -> Judgement +blacklistingDestruct = + field @"_jBlacklistDestruct" .~ True + + +unwhitelistingSplit :: Judgement -> Judgement +unwhitelistingSplit = + field @"_jWhitelistSplit" .~ False + + +isDestructBlacklisted :: Judgement -> Bool +isDestructBlacklisted = _jBlacklistDestruct + + +isSplitWhitelisted :: Judgement -> Bool +isSplitWhitelisted = _jWhitelistSplit + withNewGoal :: a -> Judgement' a -> Judgement' a -withNewGoal t jdg = jdg - { _jGoal = t - } +withNewGoal t = field @"_jGoal" .~ t + introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducing ns jdg@Judgement{..} = jdg - { _jHypothesis = M.fromList ns <> _jHypothesis - } +introducing ns = + field @"_jHypothesis" <>~ M.fromList ns + + +filterPosition :: OccName -> Int -> Judgement -> Judgement +filterPosition defn pos jdg = + withHypothesis (M.filterWithKey go) jdg + where + go name _ = isJust $ hasPositionalAncestry jdg defn pos name + + +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 + + +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 $ _jAncestry 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 + + +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) + + +withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement +withPositionMapping defn names = + field @"_jPositionMaps" . at defn <>~ Just [names] + + +------------------------------------------------------------------------------ +-- TODO(sandy): THIS THING IS A BIG BIG HACK +-- +-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined +-- (eg, we might be in a where block). The head of this list is not guaranteed +-- to be the one we're interested in. +extremelyStupid__definingFunction :: Context -> OccName +extremelyStupid__definingFunction = + fst . head . ctxDefiningFuncs + + +withHypothesis + :: (Map OccName a -> Map OccName 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. introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingPat ns jdg@Judgement{..} = jdg - { _jHypothesis = M.fromList ns <> _jHypothesis - , _jPatternVals = S.fromList (fmap fst ns) <> _jPatternVals - } +introducingPat ns jdg = jdg + & field @"_jHypothesis" <>~ M.fromList ns + & field @"_jPatternVals" <>~ S.fromList (fmap fst ns) disallowing :: [OccName] -> Judgement' a -> Judgement' a -disallowing ns jdg@Judgement{..} = jdg - { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns - } +disallowing ns = + field @"_jHypothesis" %~ flip M.withoutKeys (S.fromList ns) + jHypothesis :: Judgement' a -> Map OccName a jHypothesis = _jHypothesis +isPatVal :: Judgement' a -> OccName -> Bool +isPatVal j n = S.member n $ _jPatternVals j + +isTopHole :: Judgement' a -> Bool +isTopHole = _jIsTopHole + +unsetIsTopHole :: Judgement' a -> Judgement' a +unsetIsTopHole = field @"_jIsTopHole" .~ False + + ------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName a @@ -84,6 +190,21 @@ jGoal = _jGoal substJdg :: TCvSubst -> Judgement -> Judgement substJdg subst = fmap $ coerce . substTy subst . coerce -mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType -mkFirstJudgement hy = Judgement hy mempty mempty . CType +mkFirstJudgement + :: M.Map OccName CType + -> Bool -- ^ are we in the top level rhs hole? + -> M.Map OccName [[OccName]] -- ^ existing pos vals + -> Type + -> Judgement' CType +mkFirstJudgement hy top posvals goal = Judgement + { _jHypothesis = hy + , _jDestructed = mempty + , _jPatternVals = mempty + , _jBlacklistDestruct = False + , _jWhitelistSplit = True + , _jPositionMaps = posvals + , _jAncestry = mempty + , _jIsTopHole = top + , _jGoal = CType goal + } diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs new file mode 100644 index 0000000000..610740aba3 --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE LambdaCase #-} + +module Ide.Plugin.Tactic.KnownStrategies where + +import Control.Monad.Error.Class +import Ide.Plugin.Tactic.Context (getCurrentDefinitions) +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types +import OccName (mkVarOcc) +import Refinery.Tactic +import Ide.Plugin.Tactic.Machinery (tracing) + + +knownStrategies :: TacticsM () +knownStrategies = choice + [ deriveFmap + ] + + +known :: String -> TacticsM () -> TacticsM () +known name t = do + getCurrentDefinitions >>= \case + [(def, _)] | def == mkVarOcc name -> + tracing ("known " <> name) t + _ -> throwError NoApplicableTactic + + +deriveFmap :: TacticsM () +deriveFmap = known "fmap" $ do + try intros + overAlgebraicTerms homo + choice + [ overFunctions apply >> auto' 2 + , assumption + , recursion + ] + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 65885324c0..972cb8a574 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} @@ -16,10 +17,12 @@ module Ide.Plugin.Tactic.Machinery ( module Ide.Plugin.Tactic.Machinery ) where -import Control.Applicative -import Control.Monad.Except (throwError) +import Control.Arrow +import Control.Monad.Error.Class import Control.Monad.Reader -import Control.Monad.State (gets, modify) +import Control.Monad.State (MonadState(..)) +import Control.Monad.State.Class (gets, modify) +import Control.Monad.State.Strict (StateT (..)) import Data.Coerce import Data.Either import Data.List (intercalate, sortBy) @@ -45,10 +48,12 @@ substCTy subst = coerce . substTy subst . coerce -- goal. newSubgoal :: Judgement - -> RuleM (LHsExpr GhcPs) + -> Rule newSubgoal j = do unifier <- gets ts_unifier - subgoal $ substJdg unifier j + subgoal + $ substJdg unifier + $ unsetIsTopHole j ------------------------------------------------------------------------------ @@ -58,58 +63,86 @@ runTactic :: Context -> Judgement -> TacticsM () -- ^ Tactic to use - -> Either [TacticError] (LHsExpr GhcPs) + -> Either [TacticError] (Trace, LHsExpr GhcPs) runTactic ctx jdg t = let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg - tacticState = mempty { ts_skolems = skolems } + tacticState = defaultTacticState { ts_skolems = skolems } in case partitionEithers . flip runReader ctx . unExtractM - $ runTacticTWithState t jdg tacticState of - (errs, []) -> Left $ errs - (_, solns) -> do + $ runTacticT t jdg tacticState of + (errs, []) -> Left $ take 50 $ errs + (_, fmap assoc23 -> solns) -> do + let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) $ solns -- TODO(sandy): remove this trace sometime - traceM $ intercalate "\n" $ fmap (unsafeRender . fst) $ solns - case sortBy (comparing $ Down . uncurry scoreSolution . snd) solns of + traceM + $ mappend "!!!solns: " + $ intercalate "\n" + $ reverse + $ take 5 + $ fmap (show . fst) sorted + case sorted of (res : _) -> Right $ fst res -- guaranteed to not be empty _ -> Left [] +assoc23 :: (a, b, c) -> (a, (b, c)) +assoc23 (a, b, c) = (a, (b, c)) -scoreSolution :: TacticState -> [Judgement] -> Int + +tracePrim :: String -> Trace +tracePrim = flip rose [] + + +tracing + :: Functor m + => String + -> TacticT jdg (Trace, ext) err s m a + -> TacticT jdg (Trace, ext) err s m a +tracing s (TacticT m) + = TacticT $ StateT $ \jdg -> + mapExtract' (first $ rose s . pure) $ runStateT m jdg + + +recursiveCleanup + :: TacticState + -> Maybe TacticError +recursiveCleanup s = + let r = head $ ts_recursion_stack s + in case r of + True -> Nothing + False -> Just NoProgress + + +setRecursionFrameData :: MonadState TacticState m => Bool -> m () +setRecursionFrameData b = do + modify $ withRecursionStack $ \case + (_ : bs) -> b : bs + [] -> [] + + +scoreSolution + :: TacticState + -> [Judgement] + -> ( Penalize Int -- number of holes + , Reward Bool -- all bindings used + , Penalize Int -- number of introduced bindings + , Reward Int -- number used bindings + ) scoreSolution TacticState{..} holes - -- TODO(sandy): should this be linear? - = S.size ts_used_vals - length holes * 5 - - -runTacticTWithState - :: (MonadExtract ext m) - => TacticT jdg ext err s m () - -> jdg - -> s - -> m [Either err (ext, (s, [jdg]))] -runTacticTWithState t j s = proofs' s $ fmap snd $ proofState t j - - -proofs' - :: (MonadExtract ext m) - => s - -> ProofStateT ext ext err s m goal - -> m [(Either err (ext, (s, [goal])))] -proofs' s p = go s [] p - where - go s goals (Subgoal goal k) = do - h <- hole - (go s (goals ++ [goal]) $ k h) - go s goals (Effect m) = go s goals =<< m - go s goals (Stateful f) = - let (s', p) = f s - in go s' goals p - go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2) - go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2) - go _ _ Empty = pure [] - go _ _ (Failure err) = pure [throwError err] - go s goals (Axiom ext) = pure [Right (ext, (s, goals))] + = ( Penalize $ length holes + , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals + , Penalize $ S.size ts_intro_vals + , Reward $ S.size ts_used_vals + ) + + +newtype Penalize a = Penalize a + deriving (Eq, Ord, Show) via (Down a) + +newtype Reward a = Reward a + deriving (Eq, Ord, Show) via a + ------------------------------------------------------------------------------ diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 89cb181275..4fcccbb61b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -1,6 +1,10 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} @@ -10,15 +14,16 @@ module Ide.Plugin.Tactic.Tactics , runTactic ) where -import Control.Applicative import Control.Monad.Except (throwError) +import Control.Monad.Reader.Class (MonadReader(ask)) import Control.Monad.State.Class import Control.Monad.State.Strict (StateT(..), runStateT) -import Data.Function +import Data.Bool (bool) import Data.List import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S +import DataCon import Development.IDE.GHC.Compat import GHC.Exts import GHC.SourceGen.Expr @@ -30,23 +35,17 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Types +import Name (nameOccName, occNameString) import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) - ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. --- TODO(sandy): deprecate this assumption :: TacticsM () -assumption = rule $ \jdg -> do - let hy = jHypothesis jdg - g = jGoal jdg - case find ((== g) . snd) $ toList hy of - Just (v, _) -> pure $ noLoc $ var' v - Nothing -> throwError $ GoalMismatch "assumption" g +assumption = attemptOn allNames assume ------------------------------------------------------------------------------ @@ -58,32 +57,24 @@ assume name = rule $ \jdg -> do Just ty -> case ty == jGoal jdg of True -> do + case M.member name (jPatHypothesis jdg) of + True -> setRecursionFrameData True + False -> pure () useOccName jdg name - pure $ noLoc $ var' name + pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name False -> throwError $ GoalMismatch "assume" g Nothing -> throwError $ UndefinedHypothesis name -useOccName :: MonadState TacticState m => Judgement -> OccName -> m () -useOccName jdg name = - case M.lookup name $ jHypothesis jdg of - Just{} -> modify $ withUsedVals $ S.insert name - Nothing -> pure () - ------------------------------------------------------------------------------- --- | Introduce a lambda. -intro :: TacticsM () -intro = rule $ \jdg -> do - let hy = jHypothesis jdg - g = jGoal jdg - case splitFunTy_maybe $ unCType g of - Just (a, b) -> do - v <- pure $ mkGoodName (getInScope hy) a - let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg - sg <- newSubgoal jdg' - pure $ noLoc $ lambda [bvar' v] $ unLoc sg - _ -> throwError $ GoalMismatch "intro" g +recursion :: TacticsM () +recursion = tracing "recursion" $ do + defs <- getCurrentDefinitions + attemptOn (const $ fmap fst defs) $ \name -> do + modify $ withRecursionStack (False :) + ensure recursiveCleanup (withRecursionStack tail) $ do + (localTactic (apply' (const id) name) $ introducing defs) + <@> fmap (localTactic assumption . filterPosition name) [0..] ------------------------------------------------------------------------------ @@ -92,22 +83,53 @@ intros :: TacticsM () intros = rule $ \jdg -> do let hy = jHypothesis jdg g = jGoal jdg + ctx <- ask case tcSplitFunTys $ unCType g of - ([], _) -> throwError $ GoalMismatch "intro" g + ([], _) -> throwError $ GoalMismatch "intros" g (as, b) -> do vs <- mkManyGoodNames hy as - let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg - sg <- newSubgoal jdg' + let jdg' = introducing (zip vs $ coerce as) + $ withNewGoal (CType b) jdg + modify $ withIntroducedVals $ mappend $ S.fromList vs + (tr, sg) + <- newSubgoal + $ bool + id + (withPositionMapping + (extremelyStupid__definingFunction ctx) vs) + (isTopHole jdg) + $ jdg' pure + . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) . noLoc . lambda (fmap bvar' vs) $ unLoc sg +------------------------------------------------------------------------------ +-- | Case split, and leave holes in the matches. +destructAuto :: OccName -> TacticsM () +destructAuto name = 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 split, and leave holes in the matches. destruct :: OccName -> TacticsM () -destruct name = do +destruct name = tracing "destruct(user)" $ do jdg <- goal case hasDestructed jdg name of True -> throwError $ AlreadyDestructed name @@ -117,60 +139,98 @@ destruct name = do ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () -homo = rule . destruct' (\dc jdg -> +homo = tracing "homo" . rule . destruct' (\dc jdg -> buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) ------------------------------------------------------------------------------ -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM () -destructLambdaCase = rule $ destructLambdaCase' (const subgoal) +destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal) ------------------------------------------------------------------------------ -- | LambdaCase split, using the same data constructor in the matches. homoLambdaCase :: TacticsM () -homoLambdaCase = rule $ destructLambdaCase' (\dc jdg -> +homoLambdaCase = tracing "homoLambdaCase" $ rule $ destructLambdaCase' (\dc jdg -> buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) -apply' :: OccName -> TacticsM () -apply' func = rule $ \jdg -> do - let hy = jHypothesis jdg - g = jGoal jdg - case M.lookup func hy of - Just (CType ty) -> do - let (args, ret) = splitFunTys ty - unify g (CType ret) - sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args - pure . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs - Nothing -> throwError $ GoalMismatch "apply" g +apply :: OccName -> TacticsM () +apply = apply' (const id) + + +apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM () +apply' f func = tracing ("apply' " <> show func) $ do + rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg + case M.lookup func hy of + Just (CType ty) -> do + let (args, ret) = splitFunTys ty + unify g (CType ret) + useOccName jdg func + (tr, sgs) + <- fmap unzipTrace + $ traverse ( \(i, t) -> + newSubgoal + . f i + . blacklistingDestruct + . flip withNewGoal jdg + $ CType t + ) $ zip [0..] args + pure + . (tr, ) + . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + Nothing -> do + throwError $ GoalMismatch "apply" g ------------------------------------------------------------------------------ -- | Choose between each of the goal's data constructors. split :: TacticsM () -split = do +split = tracing "split(user)" $ do jdg <- goal let g = jGoal jdg case splitTyConApp_maybe $ unCType g of - Nothing -> throwError $ GoalMismatch "getGoalTyCon" g + Nothing -> throwError $ GoalMismatch "split" g Just (tc, _) -> do let dcs = tyConDataCons tc choice $ fmap splitDataCon dcs +------------------------------------------------------------------------------ +-- | Choose between each of the goal's data constructors. Different than +-- 'split' because it won't split a data con if it doesn't result in any new +-- goals. +splitAuto :: TacticsM () +splitAuto = tracing "split(auto)" $ do + jdg <- goal + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Nothing -> throwError $ GoalMismatch "split" g + Just (tc, _) -> do + let dcs = tyConDataCons tc + case isSplitWhitelisted jdg of + True -> choice $ fmap splitDataCon dcs + False -> do + choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs -> + case any (/= jGoal jdg) $ fmap jGoal jdgs of + False -> Nothing + True -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc + + ------------------------------------------------------------------------------ -- | Attempt to instantiate the given data constructor to solve the goal. splitDataCon :: DataCon -> TacticsM () -splitDataCon dc = rule $ \jdg -> do +splitDataCon dc = tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do let g = jGoal jdg case splitTyConApp_maybe $ unCType g of Just (tc, apps) -> do case elem dc $ tyConDataCons tc of - True -> buildDataCon jdg dc apps + True -> buildDataCon (unwhitelistingSplit jdg) dc apps False -> throwError $ IncorrectDataCon dc Nothing -> throwError $ GoalMismatch "splitDataCon" g @@ -186,41 +246,37 @@ attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM () attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames) ------------------------------------------------------------------------------- --- | Automatically solve a goal. -auto :: TacticsM () -auto = do - current <- getCurrentDefinitions +localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a +localTactic t f = do TacticT $ StateT $ \jdg -> - runStateT (unTacticT $ auto' 5) $ disallowing current jdg + runStateT (unTacticT t) $ f jdg + auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do let loop = auto' (n - 1) - intros <|> many_ intro + try intros choice - [ attemptOn functionNames $ \fname -> do - apply' fname + [ overFunctions $ \fname -> do + apply fname loop - , attemptOn algebraicNames $ \aname -> do - progress ((==) `on` jGoal) NoProgress (destruct aname) - loop - , split >> loop - , attemptOn allNames $ \name -> do - assume name + , overAlgebraicTerms $ \aname -> do + destructAuto aname loop + , splitAuto >> loop + , assumption >> loop + , recursion ] +overFunctions :: (OccName -> TacticsM ()) -> TacticsM () +overFunctions = + attemptOn $ M.keys . M.filter (isFunction . unCType) . jHypothesis -functionNames :: Judgement -> [OccName] -functionNames = - M.keys . M.filter (isFunction . unCType) . jHypothesis - - -algebraicNames :: Judgement -> [OccName] -algebraicNames = - M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis +overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM () +overAlgebraicTerms = + attemptOn $ + M.keys . M.filter (isJust . algebraicTyCon . unCType) . 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 291d732fad..5cfd62b5a6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -1,10 +1,13 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} module Ide.Plugin.Tactic.Types ( module Ide.Plugin.Tactic.Types @@ -17,17 +20,21 @@ module Ide.Plugin.Tactic.Types , Range ) where +import Control.Lens hiding (Context) +import Data.Generics.Product (field) import Control.Monad.Reader import Data.Function import Data.Map (Map) import Data.Set (Set) -import Development.IDE.GHC.Compat +import Development.IDE.GHC.Compat hiding (Node) import Development.IDE.Types.Location import GHC.Generics import Ide.Plugin.Tactic.Debug import OccName import Refinery.Tactic import Type +import Data.Tree +import Data.Coerce ------------------------------------------------------------------------------ @@ -40,42 +47,73 @@ instance Eq CType where instance Ord CType where compare = nonDetCmpType `on` unCType +instance Show CType where + show = unsafeRender . unCType + +instance Show OccName where + show = unsafeRender + +instance Show Var where + show = unsafeRender + +instance Show TCvSubst where + show = unsafeRender + +instance Show (LHsExpr GhcPs) where + show = unsafeRender + +instance Show DataCon where + show = unsafeRender + ------------------------------------------------------------------------------ data TacticState = TacticState { ts_skolems :: !([TyVar]) , ts_unifier :: !(TCvSubst) , ts_used_vals :: !(Set OccName) - } + , ts_intro_vals :: !(Set OccName) + , ts_recursion_stack :: ![Bool] + } deriving stock (Show, Generic) + + +defaultTacticState :: TacticState +defaultTacticState = + TacticState mempty emptyTCvSubst mempty mempty mempty -instance Semigroup TacticState where - TacticState a1 b1 c1 <> TacticState a2 b2 c2 - = TacticState - (a1 <> a2) - (unionTCvSubst b1 b2) - (c1 <> c2) -instance Monoid TacticState where - mempty = TacticState mempty emptyTCvSubst mempty +withRecursionStack + :: ([Bool] -> [Bool]) -> TacticState -> TacticState +withRecursionStack f = + field @"ts_recursion_stack" %~ f withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState -withUsedVals f ts = ts - { ts_used_vals = f $ ts_used_vals ts - } +withUsedVals f = + field @"ts_used_vals" %~ f + + +withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState +withIntroducedVals f = + field @"ts_intro_vals" %~ f + ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement - { _jHypothesis :: !(Map OccName a) - , _jDestructed :: !(Set OccName) + { _jHypothesis :: !(Map OccName a) + , _jDestructed :: !(Set OccName) -- ^ These should align with keys of _jHypothesis , _jPatternVals :: !(Set OccName) -- ^ These should align with keys of _jHypothesis - , _jGoal :: !(a) + , _jBlacklistDestruct :: !(Bool) + , _jWhitelistSplit :: !(Bool) + , _jPositionMaps :: !(Map OccName [[OccName]]) + , _jAncestry :: !(Map OccName (Set OccName)) + , _jIsTopHole :: !Bool + , _jGoal :: !(a) } - deriving stock (Eq, Ord, Generic, Functor) + deriving stock (Eq, Ord, Generic, Functor, Show) type Judgement = Judgement' CType @@ -85,8 +123,8 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. -instance MonadExtract (LHsExpr GhcPs) ExtractM where - hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" +instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where + hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_") ------------------------------------------------------------------------------ @@ -100,6 +138,9 @@ data TacticError | NoApplicableTactic | AlreadyDestructed OccName | IncorrectDataCon DataCon + | RecursionOnWrongParam OccName Int OccName + | UnhelpfulDestruct OccName + | UnhelpfulSplit OccName deriving stock (Eq) instance Show TacticError where @@ -129,12 +170,21 @@ instance Show TacticError where "Already destructed " <> unsafeRender name show (IncorrectDataCon dcon) = "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")" + show (RecursionOnWrongParam call p arg) = + "Recursion on wrong param (" <> show call <> ") on arg" + <> show p <> ": " <> show arg + show (UnhelpfulDestruct n) = + "Destructing patval " <> show n <> " leads to no new types" + show (UnhelpfulSplit n) = + "Splitting constructor " <> show n <> " leads to no new goals" ------------------------------------------------------------------------------ -type TacticsM = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM -type RuleM = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM -type Rule = RuleM (LHsExpr GhcPs) +type TacticsM = TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM +type RuleM = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM +type Rule = RuleM (Trace, LHsExpr GhcPs) + +type Trace = Rose String ------------------------------------------------------------------------------ @@ -147,3 +197,25 @@ data Context = Context } deriving stock (Eq, Ord) + +newtype Rose a = Rose (Tree a) + deriving stock (Eq, Functor, Generic) + +instance Show (Rose String) where + show = unlines . dropEveryOther . lines . drawTree . coerce + +dropEveryOther :: [a] -> [a] +dropEveryOther [] = [] +dropEveryOther [a] = [a] +dropEveryOther (a : _ : as) = a : dropEveryOther as + +instance Semigroup a => Semigroup (Rose a) where + Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs) + +instance Monoid a => Monoid (Rose a) where + mempty = Rose $ Node mempty mempty + +rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a +rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs +rose a rs = Rose $ Node a $ coerce rs + diff --git a/plugins/tactics/src/Ide/TreeTransform.hs b/plugins/tactics/src/Ide/TreeTransform.hs index 012426de68..80b0062ff5 100644 --- a/plugins/tactics/src/Ide/TreeTransform.hs +++ b/plugins/tactics/src/Ide/TreeTransform.hs @@ -12,7 +12,6 @@ import BasicTypes (appPrec) import Control.Monad import Control.Monad.Trans.Class import qualified Data.Text as T -import Debug.Trace import Development.IDE.Core.RuleTypes import Development.IDE.Core.Rules import Development.IDE.Core.Shake @@ -104,7 +103,7 @@ fixAnns ParsedModule {..} = annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs) annotate dflags expr = do uniq <- show <$> uniqueSrcSpanT - let rendered = traceId $ render dflags expr + let rendered = render dflags expr (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered let anns' = setPrecedingLines expr' 0 1 anns pure (anns', expr') diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml index e462e45fca..8353abf148 100644 --- a/stack-8.10.1.yaml +++ b/stack-8.10.1.yaml @@ -21,7 +21,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 - ormolu-0.1.3.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index a594da29c8..66fa833fb6 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -19,7 +19,7 @@ extra-deps: - fourmolu-0.2.0.0 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - retrie-0.1.1.1 - stylish-haskell-0.12.2.0 - semigroups-0.18.5 diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index 97051012b9..9796b068ef 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -46,7 +46,7 @@ extra-deps: - ormolu-0.1.3.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index 888670dd8f..1a0b67c2b2 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -45,7 +45,7 @@ extra-deps: - ormolu-0.1.3.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml index 0d6a229d1f..94ad80cd99 100644 --- a/stack-8.8.2.yaml +++ b/stack-8.8.2.yaml @@ -38,7 +38,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 - ormolu-0.1.3.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index 1468ae7444..c01a2649e1 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -30,7 +30,7 @@ extra-deps: - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 - ormolu-0.1.3.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index ebf11425f1..57518e9e24 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -30,7 +30,7 @@ extra-deps: - ilist-0.3.1.0 - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack.yaml b/stack.yaml index 888670dd8f..1a0b67c2b2 100644 --- a/stack.yaml +++ b/stack.yaml @@ -45,7 +45,7 @@ extra-deps: - ormolu-0.1.3.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 -- refinery-0.2.0.0 +- refinery-0.3.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index f251d70411..38594eae61 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -86,13 +86,18 @@ tests = testGroup [ (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 "" - , goldenTest "GoldenIdTypeFam.hs" 7 11 Auto "" + , goldenTest "GoldenEitherAuto.hs" 2 11 Auto "" + , goldenTest "GoldenJoinCont.hs" 4 12 Auto "" + , goldenTest "GoldenIdentityFunctor.hs" 3 11 Auto "" + , goldenTest "GoldenIdTypeFam.hs" 7 11 Auto "" , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto "" , goldenTest "GoldenNote.hs" 2 8 Auto "" , goldenTest "GoldenPureList.hs" 2 12 Auto "" + , goldenTest "GoldenListFmap.hs" 2 12 Auto "" + , goldenTest "GoldenFromMaybe.hs" 2 13 Auto "" + , goldenTest "GoldenFoldr.hs" 2 10 Auto "" + , goldenTest "GoldenSwap.hs" 2 8 Auto "" + , goldenTest "GoldenFmapTree.hs" 4 11 Auto "" , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" , goldenTest "GoldenGADTAuto.hs" 7 13 Auto "" ] diff --git a/test/testdata/tactic/GoldenFmapTree.hs b/test/testdata/tactic/GoldenFmapTree.hs new file mode 100644 index 0000000000..679e7902df --- /dev/null +++ b/test/testdata/tactic/GoldenFmapTree.hs @@ -0,0 +1,4 @@ +data Tree a = Leaf a | Branch (Tree a) (Tree a) + +instance Functor Tree where + fmap = _ diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected new file mode 100644 index 0000000000..4e8b97d735 --- /dev/null +++ b/test/testdata/tactic/GoldenFmapTree.hs.expected @@ -0,0 +1,7 @@ +data Tree a = Leaf a | Branch (Tree a) (Tree a) + +instance Functor Tree where + fmap = (\ fab ta + -> case ta of + (Leaf a) -> Leaf (fab a) + (Branch ta2 ta3) -> Branch (fmap fab ta2) (fmap fab ta3)) diff --git a/test/testdata/tactic/GoldenFoldr.hs b/test/testdata/tactic/GoldenFoldr.hs new file mode 100644 index 0000000000..bade9c1e7a --- /dev/null +++ b/test/testdata/tactic/GoldenFoldr.hs @@ -0,0 +1,2 @@ +foldr2 :: (a -> b -> b) -> b -> [a] -> b +foldr2 = _ diff --git a/test/testdata/tactic/GoldenFoldr.hs.expected b/test/testdata/tactic/GoldenFoldr.hs.expected new file mode 100644 index 0000000000..fe0463b75f --- /dev/null +++ b/test/testdata/tactic/GoldenFoldr.hs.expected @@ -0,0 +1,5 @@ +foldr2 :: (a -> b -> b) -> b -> [a] -> b +foldr2 = (\ f_b b l_a + -> case l_a of + [] -> b + ((:) a l_a4) -> f_b a (foldr2 f_b b l_a4)) diff --git a/test/testdata/tactic/GoldenFromMaybe.hs b/test/testdata/tactic/GoldenFromMaybe.hs new file mode 100644 index 0000000000..e3046a29c3 --- /dev/null +++ b/test/testdata/tactic/GoldenFromMaybe.hs @@ -0,0 +1,2 @@ +fromMaybe :: a -> Maybe a -> a +fromMaybe = _ diff --git a/test/testdata/tactic/GoldenFromMaybe.hs.expected b/test/testdata/tactic/GoldenFromMaybe.hs.expected new file mode 100644 index 0000000000..1375967a70 --- /dev/null +++ b/test/testdata/tactic/GoldenFromMaybe.hs.expected @@ -0,0 +1,5 @@ +fromMaybe :: a -> Maybe a -> a +fromMaybe = (\ a ma + -> case ma of + Nothing -> a + (Just a2) -> a2) diff --git a/test/testdata/tactic/GoldenJoinCont.hs b/test/testdata/tactic/GoldenJoinCont.hs index a0cdb05da6..f2c63714da 100644 --- a/test/testdata/tactic/GoldenJoinCont.hs +++ b/test/testdata/tactic/GoldenJoinCont.hs @@ -1,4 +1,4 @@ type Cont r a = ((a -> r) -> r) -joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d +joinCont :: Cont r (Cont r a) -> Cont r a joinCont = _ diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected index 306591b32c..ebf84d1371 100644 --- a/test/testdata/tactic/GoldenJoinCont.hs.expected +++ b/test/testdata/tactic/GoldenJoinCont.hs.expected @@ -1,7 +1,4 @@ type Cont r a = ((a -> r) -> r) -joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d -joinCont = (\ fac fbc eab fcd - -> case eab of - (Left a) -> fcd (fac a) - (Right b) -> fcd (fbc b)) +joinCont :: Cont r (Cont r a) -> Cont r a +joinCont = (\ f_r far -> f_r (\ f_r2 -> f_r2 far)) diff --git a/test/testdata/tactic/GoldenListFmap.hs b/test/testdata/tactic/GoldenListFmap.hs new file mode 100644 index 0000000000..85293daaf4 --- /dev/null +++ b/test/testdata/tactic/GoldenListFmap.hs @@ -0,0 +1,2 @@ +fmapList :: (a -> b) -> [a] -> [b] +fmapList = _ diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected new file mode 100644 index 0000000000..26766d57c3 --- /dev/null +++ b/test/testdata/tactic/GoldenListFmap.hs.expected @@ -0,0 +1,5 @@ +fmapList :: (a -> b) -> [a] -> [b] +fmapList = (\ fab l_a + -> case l_a of + [] -> [] + ((:) a l_a3) -> (:) (fab a) (fmapList fab l_a3)) diff --git a/test/testdata/tactic/GoldenSwap.hs b/test/testdata/tactic/GoldenSwap.hs new file mode 100644 index 0000000000..9243955c54 --- /dev/null +++ b/test/testdata/tactic/GoldenSwap.hs @@ -0,0 +1,2 @@ +swap :: (a, b) -> (b, a) +swap = _ diff --git a/test/testdata/tactic/GoldenSwap.hs.expected b/test/testdata/tactic/GoldenSwap.hs.expected new file mode 100644 index 0000000000..4281fc81d9 --- /dev/null +++ b/test/testdata/tactic/GoldenSwap.hs.expected @@ -0,0 +1,2 @@ +swap :: (a, b) -> (b, a) +swap = (\ p_ab -> case p_ab of { ((,) a b) -> (,) b a })