Merge pull request #26 from isovector/tracing

Tactic tracing

Author: isovector

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)

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
 

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,18 +119,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 = 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
                   . flip withNewGoal jdg
                   $ 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

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
 
 

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

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,14 +91,16 @@ 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
                 (extremelyStupid__definingFunction ctx) vs)
               (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,24 +170,28 @@ 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
 
 
 ------------------------------------------------------------------------------
 -- | 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