diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 1dbccedfa0..27171fe7fd 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -258,7 +258,6 @@ judgementForHole state nfp range = do resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp - -- traceMX "holes!" $ isRhsHole rss $ let tcg = fst $ tm_internals_ $ tmrModule tcmod tcs = tm_typechecked_source $ tmrModule tcmod ctx = mkContext @@ -297,9 +296,10 @@ tacticCmd tac lf state (TacticParams uri range var_name) pure $ (, Nothing) $ Left $ ResponseError InvalidRequest (T.pack $ show err) Nothing - Right res -> do - let g = graft (RealSrcSpan span) res + Right (tr, ext) -> do + let g = graft (RealSrcSpan span) ext response = transform dflags (clientCapabilities lf) uri g pm + traceMX "trace" tr pure $ case response of Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs index 4aadd75ee2..3e4a28d21f 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs @@ -6,6 +6,7 @@ import Ide.Plugin.Tactic.KnownStrategies import Ide.Plugin.Tactic.Tactics import Ide.Plugin.Tactic.Types import Refinery.Tactic +import Ide.Plugin.Tactic.Machinery (tracing) ------------------------------------------------------------------------------ @@ -15,7 +16,9 @@ auto = do jdg <- goal current <- getCurrentDefinitions traceMX "goal" jdg - commit - knownStrategies - (localTactic (auto' 4) $ disallowing $ fmap fst 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 191b4e7c3b..85373a9f61 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TupleSections #-} {-# LANGUAGE FlexibleContexts #-} module Ide.Plugin.Tactic.CodeGen where @@ -38,7 +39,7 @@ destructMatches -> CType -- ^ Type being destructed -> Judgement - -> RuleM [RawMatch] + -> RuleM (Trace, [RawMatch]) destructMatches f f2 t jdg = do let hy = jHypothesis jdg g = jGoal jdg @@ -48,7 +49,7 @@ 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 = dataConInstArgTys dc apps names <- mkManyGoodNames hy args let hy' = zip names $ coerce args @@ -61,9 +62,19 @@ destructMatches f f2 t jdg = do $ withPositionMapping dcon_name names $ introducingPat hy' $ withNewGoal g jdg - sg <- f dc j + (tr, sg) <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names - pure $ match [pat] $ unLoc sg + 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) ------------------------------------------------------------------------------ @@ -77,12 +88,15 @@ destruct' f term jdg = do Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> do useOccName jdg term - fmap noLoc $ case' (var' term) <$> - destructMatches - f - (\cs -> setParents term (fmap fst cs) . destructing term) - t - jdg + (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 + ) ------------------------------------------------------------------------------ @@ -94,7 +108,7 @@ destructLambdaCase' f jdg = do let g = jGoal jdg case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> - fmap noLoc $ lambdaCase <$> + fmap (fmap noLoc $ lambdaCase) <$> destructMatches f (const id) (CType arg) jdg _ -> throwError $ GoalMismatch "destructLambdaCase'" g @@ -105,11 +119,13 @@ 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 = dataConInstArgTys dc apps dcon_name = nameOccName $ dataConName dc - sgs <- traverse ( \(arg, n) -> + (tr, sgs) + <- fmap unzipTrace + $ traverse ( \(arg, n) -> newSubgoal . filterSameTypeFromOtherPositions dcon_name n . blacklistingDestruct @@ -117,6 +133,7 @@ buildDataCon jdg dc apps = do $ CType arg ) $ zip args [0..] pure + . (rose (show dc) $ pure tr,) . noLoc . foldl' (@@) (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) @@ -128,6 +145,7 @@ 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 diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs index 0855cd97e8..610740aba3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -8,6 +8,7 @@ import Ide.Plugin.Tactic.Tactics import Ide.Plugin.Tactic.Types import OccName (mkVarOcc) import Refinery.Tactic +import Ide.Plugin.Tactic.Machinery (tracing) knownStrategies :: TacticsM () @@ -19,9 +20,8 @@ knownStrategies = choice known :: String -> TacticsM () -> TacticsM () known name t = do getCurrentDefinitions >>= \case - [(def, _)] | def == mkVarOcc name -> do - traceMX "running known strategy" name - t + [(def, _)] | def == mkVarOcc name -> + tracing ("known " <> name) t _ -> throwError NoApplicableTactic diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 8228feee00..588445ebb7 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs @@ -36,6 +36,8 @@ import Refinery.Tactic.Internal import TcType import Type import Unify +import Control.Arrow +import Control.Monad.State.Strict (StateT (..)) substCTy :: TCvSubst -> CType -> CType @@ -47,7 +49,7 @@ substCTy subst = coerce . substTy subst . coerce -- goal. newSubgoal :: Judgement - -> RuleM (LHsExpr GhcPs) + -> Rule newSubgoal j = do unifier <- gets ts_unifier subgoal @@ -62,7 +64,7 @@ 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 = defaultTacticState { ts_skolems = skolems } @@ -81,6 +83,20 @@ runTactic ctx jdg t = _ -> Left [] +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 diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 4b20cdfb01..dc6358fec8 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TupleSections #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveGeneric #-} @@ -17,6 +18,7 @@ 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.Bool (bool) import Data.List import qualified Data.Map as M import Data.Maybe @@ -33,12 +35,11 @@ import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Types -import Name (nameOccName) +import Name (occNameString) import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) -import Data.Bool (bool) ------------------------------------------------------------------------------ @@ -60,14 +61,14 @@ assume name = rule $ \jdg -> do 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 recursion :: TacticsM () -recursion = do +recursion = tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const $ fmap fst defs) $ \name -> do modify $ withRecursionStack (False :) @@ -90,7 +91,8 @@ intros = rule $ \jdg -> do let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs - sg <- newSubgoal + (tr, sg) + <- newSubgoal $ bool id (withPositionMapping @@ -98,6 +100,7 @@ intros = rule $ \jdg -> do (isTopHole jdg) $ jdg' pure + . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) . noLoc . lambda (fmap bvar' vs) $ unLoc sg @@ -106,7 +109,7 @@ intros = rule $ \jdg -> do ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches. destructAuto :: OccName -> TacticsM () -destructAuto name = do +destructAuto name = tracing "destruct(auto)" $ do jdg <- goal case hasDestructed jdg name of True -> throwError $ AlreadyDestructed name @@ -126,7 +129,7 @@ destructAuto name = do ------------------------------------------------------------------------------ -- | 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 @@ -136,20 +139,20 @@ 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) @@ -158,7 +161,7 @@ apply = apply' (const id) apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM () -apply' f func = do +apply' f func = tracing ("apply' " <> show func) $ do rule $ \jdg -> do let hy = jHypothesis jdg g = jGoal jdg @@ -167,16 +170,20 @@ apply' f func = do let (args, ret) = splitFunTys ty unify g (CType ret) useOccName jdg func - sgs <- traverse ( \(i, t) -> + (tr, sgs) + <- fmap unzipTrace + $ traverse ( \(i, t) -> newSubgoal . f i . blacklistingDestruct . flip withNewGoal jdg $ CType t ) $ zip [0..] args - pure . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs + pure + . (tr, ) + . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs Nothing -> do throwError $ GoalMismatch "apply" g @@ -184,7 +191,7 @@ apply' f func = do ------------------------------------------------------------------------------ -- | 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 @@ -196,7 +203,7 @@ split = do ------------------------------------------------------------------------------ -- | Choose between each of the goal's data constructors. splitAuto :: TacticsM () -splitAuto = do +splitAuto = tracing "split(auto)" $ do jdg <- goal let g = jGoal jdg case splitTyConApp_maybe $ unCType g of @@ -220,7 +227,7 @@ splitAuto = do ------------------------------------------------------------------------------ -- | 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 diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs index cca6fe8247..5cfd62b5a6 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs @@ -26,13 +26,15 @@ 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 ------------------------------------------------------------------------------ @@ -60,6 +62,9 @@ instance Show TCvSubst where instance Show (LHsExpr GhcPs) where show = unsafeRender +instance Show DataCon where + show = unsafeRender + ------------------------------------------------------------------------------ data TacticState = TacticState @@ -118,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 "_") ------------------------------------------------------------------------------ @@ -175,9 +180,11 @@ instance Show TacticError where ------------------------------------------------------------------------------ -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 ------------------------------------------------------------------------------ @@ -190,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 +