From 2c52a5fbd9a2c01bb8ea99924a476d3e8480a720 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 06:52:13 -0800 Subject: [PATCH 01/13] Store total number of arguments in TopLevelArgPrv --- .../src/Ide/Plugin/Tactic/Judgements.hs | 17 +++++++++-------- .../src/Ide/Plugin/Tactic/LanguageServer.hs | 3 ++- .../src/Ide/Plugin/Tactic/Types.hs | 1 + 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index 06d070548d..c3876cdc19 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -92,14 +92,15 @@ withNewGoal t = field @"_jGoal" .~ t ------------------------------------------------------------------------------ -- | Helper function for implementing functions which introduce new hypotheses. introducing - :: (Int -> Provenance) -- ^ A function from the position of the arg to its - -- provenance. + :: (Int -> Int -> Provenance) + -- ^ A function from the total number of args and position of this arg + -- to its provenance. -> [(OccName, a)] -> Judgement' a -> Judgement' a introducing f ns = field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&> - \(pos, (name, ty)) -> HyInfo name (f pos) ty) + \(pos, (name, ty)) -> HyInfo name (f (length ns) pos) ty) ------------------------------------------------------------------------------ @@ -110,14 +111,14 @@ introducingLambda -> [(OccName, a)] -> Judgement' a -> Judgement' a -introducingLambda func = introducing $ \pos -> - maybe UserPrv (\x -> TopLevelArgPrv x pos) func +introducingLambda func = introducing $ \count pos -> + maybe UserPrv (\x -> TopLevelArgPrv x pos count) func ------------------------------------------------------------------------------ -- | Introduce a binding in a recursive context. introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingRecursively = introducing $ const RecursivePrv +introducingRecursively = introducing $ const $ const RecursivePrv ------------------------------------------------------------------------------ @@ -176,7 +177,7 @@ findPositionVal jdg defn pos = listToMaybe $ do -- ancstry through potentially disallowed terms in the hypothesis. (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg case hi_provenance hi of - TopLevelArgPrv defn' pos' + TopLevelArgPrv defn' pos' _ | defn == defn' , pos == pos' -> pure name PatternMatchPrv pv @@ -253,7 +254,7 @@ introducingPat -> Judgement' a -> Judgement' a introducingPat scrutinee dc ns jdg - = introducing (\pos -> + = introducing (\_ pos -> PatternMatchPrv $ PatVal scrutinee diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 1c672116e1..4fcbdabd5a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -197,7 +197,8 @@ getRhsPosVals rss tcs , isHole $ occName hole -- and the span is a hole -> First $ do patnames <- traverse getPatName ps - pure $ zip patnames $ [0..] <&> TopLevelArgPrv name + pure $ zip patnames $ [0..] <&> \n -> + TopLevelArgPrv name n (length patnames) _ -> mempty ) tcs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index 413b0f69b7..d925f3573a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -165,6 +165,7 @@ data Provenance TopLevelArgPrv OccName -- ^ Binding function Int -- ^ Argument Position + Int -- ^ of how many arguments total? -- | A binding created in a pattern match. | PatternMatchPrv PatVal -- | A class method from the given context. From 2867ff97a89c8235367eed4e8e69b452f75dee79 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 08:16:49 -0800 Subject: [PATCH 02/13] Re-enable tracing other solutions --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index 1a909649e6..6d97df680d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -144,6 +144,7 @@ mkWorkspaceEdits -> RunTacticResults -> Either ResponseError (Maybe WorkspaceEdit) mkWorkspaceEdits span dflags ccs uri pm rtr = do + traceMX "other solutions" $ rtr_other_solns rtr let g = graftHole (RealSrcSpan span) rtr response = transform dflags ccs uri g pm in case response of From 8d84ccc4a6b409d3a5a331f364a0b44917203e9b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 08:18:08 -0800 Subject: [PATCH 03/13] Document a bug I ran into while trying to dogfood --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 44c53b3d95..2c9f848905 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -148,12 +148,14 @@ homoLambdaCase = apply :: HyInfo CType -> TacticsM () apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do jdg <- goal - let hy = jHypothesis jdg - g = jGoal jdg + let g = jGoal jdg ty = unCType $ hi_type hi func = hi_name hi ty' <- freshTyvars ty let (_, _, args, ret) = tacticsSplitFunTy ty' + -- TODO(sandy): Bug here! Prevents us from doing mono-map like things + -- Don't require new holes for locally bound vars; only respect linearity + -- requireNewHoles $ requireNewHoles $ rule $ \jdg -> do unify g (CType ret) useOccName jdg func From 28d2913db886da8c0c68bfc130637f7a6da72c92 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 08:18:24 -0800 Subject: [PATCH 04/13] Replace the janky (Trace,) extract with something more principled --- .../src/Ide/Plugin/Tactic/CodeGen.hs | 35 +++++++------- .../Tactic/KnownStrategies/QuickCheck.hs | 5 +- .../src/Ide/Plugin/Tactic/Machinery.hs | 14 +++--- .../src/Ide/Plugin/Tactic/Tactics.hs | 21 ++++----- .../src/Ide/Plugin/Tactic/Types.hs | 47 +++++++++++++++---- 5 files changed, 73 insertions(+), 49 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs index d84e2b7e43..00a1b6f36b 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs @@ -64,7 +64,7 @@ destructMatches -> CType -- ^ Type being destructed -> Judgement - -> RuleM (Trace, [RawMatch]) + -> RuleM (Synthesized [RawMatch]) destructMatches f scrut t jdg = do let hy = jEntireHypothesis jdg g = jGoal jdg @@ -80,13 +80,15 @@ destructMatches f scrut t jdg = do let hy' = zip names $ coerce args j = introducingPat scrut dc hy' $ withNewGoal g jdg - (tr, sg) <- f dc j + Synthesized tr sg <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names - pure ( rose ("match " <> show dc <> " {" <> + pure + $ Synthesized + ( rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}") - $ pure tr - , match [mkDestructPat dc names] $ unLoc sg - ) + $ pure tr) + $ match [mkDestructPat dc names] + $ unLoc sg ------------------------------------------------------------------------------ @@ -115,10 +117,8 @@ infixifyPatIfNecessary dcon x -unzipTrace :: [(Trace, a)] -> (Trace, [a]) -unzipTrace l = - let (trs, as) = unzip l - in (rose mempty trs, as) +unzipTrace :: [Synthesized a] -> Synthesized [a] +unzipTrace = sequenceA -- | Essentially same as 'dataConInstOrigArgTys' in GHC, @@ -156,15 +156,16 @@ destruct' f hi jdg = do when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let term = hi_name hi useOccName jdg term - (tr, ms) + Synthesized tr ms <- destructMatches f (Just term) (hi_type hi) $ disallowing AlreadyDestructed [term] jdg - pure ( rose ("destruct " <> show term) $ pure tr - , noLoc $ case' (var' term) ms - ) + pure + $ Synthesized (rose ("destruct " <> show term) $ pure tr) + $ noLoc + $ case' (var' term) ms ------------------------------------------------------------------------------ @@ -187,10 +188,10 @@ buildDataCon :: Judgement -> DataCon -- ^ The data con to build -> [Type] -- ^ Type arguments for the data con - -> RuleM (Trace, LHsExpr GhcPs) + -> RuleM (Synthesized (LHsExpr GhcPs)) buildDataCon jdg dc tyapps = do let args = dataConInstOrigArgTys' dc tyapps - (tr, sgs) + Synthesized tr sgs <- fmap unzipTrace $ traverse ( \(arg, n) -> newSubgoal @@ -200,6 +201,6 @@ buildDataCon jdg dc tyapps = do $ CType arg ) $ zip args [0..] pure - . (rose (show dc) $ pure tr,) + $ Synthesized (rose (show dc) $ pure tr) $ mkCon dc sgs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index 7c595a0b57..ada80abddb 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -43,8 +43,8 @@ deriveArbitrary = do terminal_expr = mkVal "terminal" oneof_expr = mkVal "oneof" pure - ( tracePrim "deriveArbitrary" - , noLoc $ + $ Synthesized (tracePrim "deriveArbitrary") + $ noLoc $ let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $ appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ case' (infixCall "<=" (mkVal "n") (int 1)) @@ -56,7 +56,6 @@ deriveArbitrary = do (list $ fmap genExpr big) terminal_expr ] - ) _ -> throwError $ GoalMismatch "deriveArbitrary" ty diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index a061aa43cd..f5373c23ba 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -93,14 +93,14 @@ runTactic ctx jdg t = (errs, []) -> Left $ take 50 errs (_, fmap assoc23 -> solns) -> do let sorted = - flip sortBy solns $ comparing $ \((_, ext), (jdg, holes)) -> + flip sortBy solns $ comparing $ \((syn_val -> ext), (jdg, holes)) -> Down $ scoreSolution ext jdg holes case sorted of - (((tr, ext), _) : _) -> + ((syn, _) : _) -> Right $ RunTacticResults - { rtr_trace = tr - , rtr_extract = simplify ext + { rtr_trace = syn_trace syn + , rtr_extract = simplify $ syn_val syn , rtr_other_solns = reverse . fmap fst $ take 5 sorted , rtr_jdg = jdg , rtr_ctx = ctx @@ -119,11 +119,11 @@ tracePrim = flip rose [] tracing :: Functor m => String - -> TacticT jdg (Trace, ext) err s m a - -> TacticT jdg (Trace, ext) err s m a + -> TacticT jdg (Synthesized ext) err s m a + -> TacticT jdg (Synthesized ext) err s m a tracing s (TacticT m) = TacticT $ StateT $ \jdg -> - mapExtract' (first $ rose s . pure) $ runStateT m jdg + mapExtract' (mapTrace $ rose s . pure) $ runStateT m jdg ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 2c9f848905..bf05c88b0a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -50,13 +50,14 @@ assumption = attemptOn (S.toList . allNames) assume -- | Use something named in the hypothesis to fill the hole. assume :: OccName -> TacticsM () assume name = rule $ \jdg -> do - let g = jGoal jdg case M.lookup name $ hyByName $ jHypothesis jdg of Just (hi_type -> ty) -> do unify ty $ jGoal jdg for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion useOccName jdg name - pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name + pure $ Synthesized (tracePrim $ "assume " <> occNameString name) + $ noLoc + $ var' name Nothing -> throwError $ UndefinedHypothesis name @@ -74,8 +75,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do -- | Introduce a lambda binding every variable. intros :: TacticsM () intros = rule $ \jdg -> do - let hy = jHypothesis jdg - g = jGoal jdg + let g = jGoal jdg ctx <- ask case tcSplitFunTys $ unCType g of ([], _) -> throwError $ GoalMismatch "intros" g @@ -86,9 +86,9 @@ intros = rule $ \jdg -> do $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs - (tr, sg) <- newSubgoal jdg' + Synthesized tr sg <- newSubgoal jdg' pure - . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) + . Synthesized (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr) . noLoc . lambda (fmap bvar' vs) $ unLoc sg @@ -155,22 +155,17 @@ apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do let (_, _, args, ret) = tacticsSplitFunTy ty' -- TODO(sandy): Bug here! Prevents us from doing mono-map like things -- Don't require new holes for locally bound vars; only respect linearity - -- requireNewHoles $ requireNewHoles $ rule $ \jdg -> do unify g (CType ret) useOccName jdg func - (tr, sgs) + sgs <- fmap unzipTrace $ traverse ( newSubgoal . blacklistingDestruct . flip withNewGoal jdg . CType ) args - pure - . (tr, ) - . noLoc - . foldl' (@@) (var' func) - $ fmap unLoc sgs + pure $ fmap (noLoc . foldl' (@@) (var' func) . fmap unLoc) sgs ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index d925f3573a..d533a5be0a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -1,5 +1,7 @@ +{-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -20,6 +22,7 @@ module Ide.Plugin.Tactic.Types , Range ) where +import Data.Semigroup import Control.Lens hiding (Context, (.=)) import Control.Monad.Reader import Control.Monad.State @@ -37,9 +40,11 @@ import Ide.Plugin.Tactic.FeatureSet (FeatureSet) import OccName import Refinery.Tactic import System.IO.Unsafe (unsafePerformIO) -import Type +import Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst) import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) +import Data.List.NonEmpty (NonEmpty (..)) +import GHC.SourceGen (var) ------------------------------------------------------------------------------ @@ -264,8 +269,12 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. -instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where - hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_") +instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where + hole + = pure + . Synthesized mempty + . noLoc + $ var "_" ------------------------------------------------------------------------------ @@ -324,12 +333,29 @@ instance Show TacticError where ------------------------------------------------------------------------------ -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 TacticsM = TacticT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM +type RuleM = RuleT Judgement (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM +type Rule = RuleM (Synthesized (LHsExpr GhcPs)) type Trace = Rose String +data Synthesized a = Synthesized + { syn_trace :: Trace + , syn_val :: a + } + deriving (Eq, Show, Functor, Foldable, Traversable) + +mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a +mapTrace f (Synthesized tr a) = Synthesized (f tr) a + + +------------------------------------------------------------------------------ +-- | This might not be lawful, due to the semigroup on 'Trace' maybe not being +-- lawful. +instance Applicative Synthesized where + pure = Synthesized mempty + Synthesized tr1 f <*> Synthesized tr2 a = Synthesized (tr1 <> tr2) $ f a + ------------------------------------------------------------------------------ -- | The Reader context of tactics and rules @@ -360,10 +386,13 @@ dropEveryOther [] = [] dropEveryOther [a] = [a] dropEveryOther (a : _ : as) = a : dropEveryOther as -instance Semigroup a => Semigroup (Rose a) where +------------------------------------------------------------------------------ +-- | This might not be lawful! I didn't check, and it feels sketchy. +instance (Eq a, Monoid a) => Semigroup (Rose a) where Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs) + sconcat (a :| as) = rose mempty $ a : as -instance Monoid a => Monoid (Rose a) where +instance (Eq a, Monoid a) => Monoid (Rose a) where mempty = Rose $ Node mempty mempty rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a @@ -376,7 +405,7 @@ rose a rs = Rose $ Node a $ coerce rs data RunTacticResults = RunTacticResults { rtr_trace :: Trace , rtr_extract :: LHsExpr GhcPs - , rtr_other_solns :: [(Trace, LHsExpr GhcPs)] + , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)] , rtr_jdg :: Judgement , rtr_ctx :: Context } deriving Show From 4abb30375b30d724fd67d81aecdca34ca0ade422 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 08:47:50 -0800 Subject: [PATCH 05/13] Add explicit constructors for introducing hypotheses --- .../src/Ide/Plugin/Tactic/Judgements.hs | 74 +++++++++++-------- 1 file changed, 45 insertions(+), 29 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index c3876cdc19..f81a5e0a38 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -1,33 +1,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} -module Ide.Plugin.Tactic.Judgements - ( blacklistingDestruct - , unwhitelistingSplit - , introducingLambda - , introducingRecursively - , introducingPat - , jGoal - , jHypothesis - , jEntireHypothesis - , jPatHypothesis - , substJdg - , unsetIsTopHole - , filterSameTypeFromOtherPositions - , isDestructBlacklisted - , withNewGoal - , jLocalHypothesis - , isSplitWhitelisted - , isPatternMatch - , filterPosition - , isTopHole - , disallowing - , mkFirstJudgement - , hypothesisFromBindings - , isTopLevel - , hyNamesInScope - , hyByName - ) where +module Ide.Plugin.Tactic.Judgements where import Control.Arrow import Control.Lens hiding (Context) @@ -99,8 +73,18 @@ introducing -> Judgement' a -> Judgement' a introducing f ns = - field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&> - \(pos, (name, ty)) -> HyInfo name (f (length ns) pos) ty) + field @"_jHypothesis" <>~ introduceHypothesis f ns + + +introduceHypothesis + :: (Int -> Int -> Provenance) + -- ^ A function from the total number of args and position of this arg + -- to its provenance. + -> [(OccName, a)] + -> Hypothesis a +introduceHypothesis f ns = + Hypothesis $ zip [0..] ns <&> \(pos, (name, ty)) -> + HyInfo name (f (length ns) pos) ty ------------------------------------------------------------------------------ @@ -115,11 +99,26 @@ introducingLambda func = introducing $ \count pos -> maybe UserPrv (\x -> TopLevelArgPrv x pos count) func +------------------------------------------------------------------------------ +-- | Introduce bindings in the context of a lamba. +introduceLambdaHypothesis + :: Maybe OccName -- ^ The name of the top level function. For any other + -- function, this should be 'Nothing'. + -> [(OccName, a)] + -> Hypothesis a +introduceLambdaHypothesis func = + introduceHypothesis $ \count pos -> + maybe UserPrv (\x -> TopLevelArgPrv x pos count) func + + ------------------------------------------------------------------------------ -- | Introduce a binding in a recursive context. introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a introducingRecursively = introducing $ const $ const RecursivePrv +introduceRecursiveHypothesis :: [(OccName, a)] -> Hypothesis a +introduceRecursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv + ------------------------------------------------------------------------------ -- | Check whether any of the given occnames are an ancestor of the term. @@ -265,6 +264,23 @@ introducingPat scrutinee dc ns jdg pos ) ns jdg +introducePatHypothesis + :: Maybe OccName + -> DataCon + -> Judgement' a + -> [(OccName, a)] + -> Hypothesis a +introducePatHypothesis scrutinee dc jdg + = introduceHypothesis $ \_ pos -> + PatternMatchPrv $ + PatVal + scrutinee + (maybe mempty + (\scrut -> S.singleton scrut <> getAncestry jdg scrut) + scrutinee) + (Uniquely dc) + pos + ------------------------------------------------------------------------------ -- | Prevent some occnames from being used in the hypothesis. This will hide From cecc4005dd482926f037910911a07e5d13cba9fb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 08:56:22 -0800 Subject: [PATCH 06/13] Split apart creation of hypothesis from introduction of it --- .../src/Ide/Plugin/Tactic/CodeGen.hs | 6 +- .../src/Ide/Plugin/Tactic/Judgements.hs | 63 +++---------------- .../src/Ide/Plugin/Tactic/Tactics.hs | 7 ++- 3 files changed, 19 insertions(+), 57 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs index 00a1b6f36b..d2dae5584f 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs @@ -77,8 +77,10 @@ destructMatches f scrut t jdg = do _ -> fmap unzipTrace $ for dcs $ \dc -> do let args = dataConInstOrigArgTys' dc apps names <- mkManyGoodNames (hyNamesInScope hy) args - let hy' = zip names $ coerce args - j = introducingPat scrut dc hy' + let hy' = patternHypothesis scrut dc jdg + $ zip names + $ coerce args + j = introduce hy' $ withNewGoal g jdg Synthesized tr sg <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs index f81a5e0a38..916a787a06 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs @@ -63,19 +63,12 @@ withNewGoal :: a -> Judgement' a -> Judgement' a withNewGoal t = field @"_jGoal" .~ t ------------------------------------------------------------------------------- --- | Helper function for implementing functions which introduce new hypotheses. -introducing - :: (Int -> Int -> Provenance) - -- ^ A function from the total number of args and position of this arg - -- to its provenance. - -> [(OccName, a)] - -> Judgement' a - -> Judgement' a -introducing f ns = - field @"_jHypothesis" <>~ introduceHypothesis f ns +introduce :: Hypothesis a -> Judgement' a -> Judgement' a +introduce hy = field @"_jHypothesis" <>~ hy +------------------------------------------------------------------------------ +-- | Helper function for implementing functions which introduce new hypotheses. introduceHypothesis :: (Int -> Int -> Provenance) -- ^ A function from the total number of args and position of this arg @@ -89,35 +82,20 @@ introduceHypothesis f ns = ------------------------------------------------------------------------------ -- | Introduce bindings in the context of a lamba. -introducingLambda - :: Maybe OccName -- ^ The name of the top level function. For any other - -- function, this should be 'Nothing'. - -> [(OccName, a)] - -> Judgement' a - -> Judgement' a -introducingLambda func = introducing $ \count pos -> - maybe UserPrv (\x -> TopLevelArgPrv x pos count) func - - ------------------------------------------------------------------------------- --- | Introduce bindings in the context of a lamba. -introduceLambdaHypothesis +lambdaHypothesis :: Maybe OccName -- ^ The name of the top level function. For any other -- function, this should be 'Nothing'. -> [(OccName, a)] -> Hypothesis a -introduceLambdaHypothesis func = +lambdaHypothesis func = introduceHypothesis $ \count pos -> maybe UserPrv (\x -> TopLevelArgPrv x pos count) func ------------------------------------------------------------------------------ -- | Introduce a binding in a recursive context. -introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a -introducingRecursively = introducing $ const $ const RecursivePrv - -introduceRecursiveHypothesis :: [(OccName, a)] -> Hypothesis a -introduceRecursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv +recursiveHypothesis :: [(OccName, a)] -> Hypothesis a +recursiveHypothesis = introduceHypothesis $ const $ const RecursivePrv ------------------------------------------------------------------------------ @@ -243,34 +221,13 @@ extremelyStupid__definingFunction = fst . head . ctxDefiningFuncs ------------------------------------------------------------------------------- --- | 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 - = introducing (\_ pos -> - PatternMatchPrv $ - PatVal - scrutinee - (maybe mempty - (\scrut -> S.singleton scrut <> getAncestry jdg scrut) - scrutinee) - (Uniquely dc) - pos - ) ns jdg - -introducePatHypothesis +patternHypothesis :: Maybe OccName -> DataCon -> Judgement' a -> [(OccName, a)] -> Hypothesis a -introducePatHypothesis scrutinee dc jdg +patternHypothesis scrutinee dc jdg = introduceHypothesis $ \_ pos -> PatternMatchPrv $ PatVal diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index bf05c88b0a..fa4977d47d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -67,7 +67,9 @@ recursion = requireConcreteHole $ tracing "recursion" $ do attemptOn (const defs) $ \(name, ty) -> do modify $ pushRecursionStack . countRecursiveCall ensure guardStructurallySmallerRecursion popRecursionStack $ do - (localTactic (apply $ HyInfo name RecursivePrv ty) $ introducingRecursively defs) + let hy' = recursiveHypothesis defs + + localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy') <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -82,7 +84,8 @@ intros = rule $ \jdg -> do (as, b) -> do vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as let top_hole = isTopHole ctx jdg - jdg' = introducingLambda top_hole (zip vs $ coerce as) + hy' = lambdaHypothesis top_hole $ zip vs $ coerce as + jdg' = introduce hy' $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs From 79741bb6a595eb90b50c83aeea936af79a6a6e28 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 09:19:51 -0800 Subject: [PATCH 07/13] Produce better debug output for other solns --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index 6d97df680d..b00f4185bc 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -50,6 +50,7 @@ import Language.LSP.Types.Capabilities import OccName import Prelude hiding (span) import System.Timeout +import Data.Foldable (for_) descriptor :: PluginId -> PluginDescriptor IdeState @@ -144,7 +145,7 @@ mkWorkspaceEdits -> RunTacticResults -> Either ResponseError (Maybe WorkspaceEdit) mkWorkspaceEdits span dflags ccs uri pm rtr = do - traceMX "other solutions" $ rtr_other_solns rtr + for_ (rtr_other_solns rtr) $ traceMX "other solution" let g = graftHole (RealSrcSpan span) rtr response = transform dflags ccs uri g pm in case response of From 389e179a314aa4b8361d784b9b5a0d8565090bd5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 09:20:12 -0800 Subject: [PATCH 08/13] Track all the bindings that get generated in Synthesized --- .../src/Ide/Plugin/Tactic/CodeGen.hs | 11 ++++++----- .../Tactic/KnownStrategies/QuickCheck.hs | 4 ++++ .../src/Ide/Plugin/Tactic/Tactics.hs | 9 ++++++--- .../src/Ide/Plugin/Tactic/Types.hs | 18 ++++++++++++------ 4 files changed, 28 insertions(+), 14 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs index d2dae5584f..0f526aeb3c 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs @@ -82,13 +82,14 @@ destructMatches f scrut t jdg = do $ coerce args j = introduce hy' $ withNewGoal g jdg - Synthesized tr sg <- f dc j + Synthesized tr sc sg <- f dc j modify $ withIntroducedVals $ mappend $ S.fromList names pure $ Synthesized ( rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}") $ pure tr) + (sc <> hy') $ match [mkDestructPat dc names] $ unLoc sg @@ -158,14 +159,14 @@ destruct' f hi jdg = do when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let term = hi_name hi useOccName jdg term - Synthesized tr ms + Synthesized tr sc ms <- destructMatches f (Just term) (hi_type hi) $ disallowing AlreadyDestructed [term] jdg pure - $ Synthesized (rose ("destruct " <> show term) $ pure tr) + $ Synthesized (rose ("destruct " <> show term) $ pure tr) sc $ noLoc $ case' (var' term) ms @@ -193,7 +194,7 @@ buildDataCon -> RuleM (Synthesized (LHsExpr GhcPs)) buildDataCon jdg dc tyapps = do let args = dataConInstOrigArgTys' dc tyapps - Synthesized tr sgs + Synthesized tr sc sgs <- fmap unzipTrace $ traverse ( \(arg, n) -> newSubgoal @@ -203,6 +204,6 @@ buildDataCon jdg dc tyapps = do $ CType arg ) $ zip args [0..] pure - $ Synthesized (rose (show dc) $ pure tr) + $ Synthesized (rose (show dc) $ pure tr) sc $ mkCon dc sgs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index ada80abddb..9bdb810902 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -44,6 +44,10 @@ deriveArbitrary = do oneof_expr = mkVal "oneof" pure $ Synthesized (tracePrim "deriveArbitrary") + -- TODO(sandy): This thing is not actually empty! We produced + -- a bespoke binding "terminal", and a not-so-bespoke "n". + -- But maybe it's fine for known rules? + mempty $ noLoc $ let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $ appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index fa4977d47d..8d355ad2bd 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -55,7 +55,7 @@ assume name = rule $ \jdg -> do unify ty $ jGoal jdg for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion useOccName jdg name - pure $ Synthesized (tracePrim $ "assume " <> occNameString name) + pure $ Synthesized (tracePrim $ "assume " <> occNameString name) mempty $ noLoc $ var' name Nothing -> throwError $ UndefinedHypothesis name @@ -69,6 +69,7 @@ recursion = requireConcreteHole $ tracing "recursion" $ do ensure guardStructurallySmallerRecursion popRecursionStack $ do let hy' = recursiveHypothesis defs + -- TODO(sandy): do we need to add this to syn_scoped? localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy') <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -89,9 +90,11 @@ intros = rule $ \jdg -> do $ withNewGoal (CType b) jdg modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs - Synthesized tr sg <- newSubgoal jdg' + Synthesized tr sc sg <- newSubgoal jdg' pure - . Synthesized (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr) + . Synthesized + (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr) + (sc <> hy') . noLoc . lambda (fmap bvar' vs) $ unLoc sg diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index d533a5be0a..a22d65143d 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -272,7 +272,7 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where hole = pure - . Synthesized mempty + . Synthesized mempty mempty . noLoc $ var "_" @@ -340,21 +340,27 @@ type Rule = RuleM (Synthesized (LHsExpr GhcPs)) type Trace = Rose String data Synthesized a = Synthesized - { syn_trace :: Trace - , syn_val :: a + { syn_trace :: Trace + -- ^ A tree describing which tactics were used produce the 'syn_val'. + -- Mainly for debugging when you get the wrong answer, to see the other + -- things it tried. + , syn_scoped :: Hypothesis CType + -- ^ All of the bindings created to produce the 'syn_val'. + , syn_val :: a } deriving (Eq, Show, Functor, Foldable, Traversable) mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a -mapTrace f (Synthesized tr a) = Synthesized (f tr) a +mapTrace f (Synthesized tr sc a) = Synthesized (f tr) sc a ------------------------------------------------------------------------------ -- | This might not be lawful, due to the semigroup on 'Trace' maybe not being -- lawful. instance Applicative Synthesized where - pure = Synthesized mempty - Synthesized tr1 f <*> Synthesized tr2 a = Synthesized (tr1 <> tr2) $ f a + pure = Synthesized mempty mempty + Synthesized tr1 sc1 f <*> Synthesized tr2 sc2 a = + Synthesized (tr1 <> tr2) (sc1 <> sc2) $ f a ------------------------------------------------------------------------------ From bae2581524da30f85fd7083d03c1d9819f8bb9c9 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 11:58:11 -0800 Subject: [PATCH 09/13] Remove ts_intro_vals; use synthesized bindings instead --- .../src/Ide/Plugin/Tactic/CodeGen.hs | 1 - .../src/Ide/Plugin/Tactic/Machinery.hs | 16 +++++++++------- .../src/Ide/Plugin/Tactic/Tactics.hs | 1 - .../src/Ide/Plugin/Tactic/Types.hs | 8 -------- 4 files changed, 9 insertions(+), 17 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs index 0f526aeb3c..7893e501dc 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs @@ -83,7 +83,6 @@ destructMatches f scrut t jdg = do j = introduce hy' $ withNewGoal g jdg Synthesized tr sc sg <- f dc j - modify $ withIntroducedVals $ mappend $ S.fromList names pure $ Synthesized ( rose ("match " <> show dc <> " {" <> diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index f5373c23ba..0489f61d6e 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -93,7 +93,7 @@ runTactic ctx jdg t = (errs, []) -> Left $ take 50 errs (_, fmap assoc23 -> solns) -> do let sorted = - flip sortBy solns $ comparing $ \((syn_val -> ext), (jdg, holes)) -> + flip sortBy solns $ comparing $ \(ext, (jdg, holes)) -> Down $ scoreSolution ext jdg holes case sorted of ((syn, _) : _) -> @@ -155,10 +155,10 @@ markStructuralySmallerRecursion pv = do -- | Given the results of running a tactic, score the solutions by -- desirability. -- --- TODO(sandy): This function is completely unprincipled and was just hacked --- together to produce the right test results. +-- NOTE: This function is completely unprincipled and was just hacked together +-- to produce the right test results. scoreSolution - :: LHsExpr GhcPs + :: Synthesized (LHsExpr GhcPs) -> TacticState -> [Judgement] -> ( Penalize Int -- number of holes @@ -171,13 +171,15 @@ scoreSolution ) scoreSolution ext TacticState{..} holes = ( Penalize $ length holes - , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals + , Reward $ S.null $ intro_vals S.\\ ts_used_vals , Penalize $ S.size ts_unused_top_vals - , Penalize $ S.size ts_intro_vals + , Penalize $ S.size intro_vals , Reward $ S.size ts_used_vals , Penalize ts_recursion_count - , Penalize $ solutionSize ext + , Penalize $ solutionSize $ syn_val ext ) + where + intro_vals = M.keysSet $ hyByName $ syn_scoped ext ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 8d355ad2bd..7a3d1e97a8 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -88,7 +88,6 @@ intros = rule $ \jdg -> do hy' = lambdaHypothesis top_hole $ zip vs $ coerce as jdg' = introduce hy' $ withNewGoal (CType b) jdg - modify $ withIntroducedVals $ mappend $ S.fromList vs when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs Synthesized tr sc sg <- newSubgoal jdg' pure diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index a22d65143d..0400aa080f 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -90,8 +90,6 @@ data TacticState = TacticState -- ^ The current substitution of univars. , ts_used_vals :: !(Set OccName) -- ^ Set of values used by tactics. - , ts_intro_vals :: !(Set OccName) - -- ^ Set of values introduced by tactics. , ts_unused_top_vals :: !(Set OccName) -- ^ Set of currently unused arguments to the function being defined. , ts_recursion_stack :: ![Maybe PatVal] @@ -121,7 +119,6 @@ defaultTacticState = { ts_skolems = mempty , ts_unifier = emptyTCvSubst , ts_used_vals = mempty - , ts_intro_vals = mempty , ts_unused_top_vals = mempty , ts_recursion_stack = mempty , ts_recursion_count = 0 @@ -155,11 +152,6 @@ withUsedVals f = field @"ts_used_vals" %~ f -withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState -withIntroducedVals f = - field @"ts_intro_vals" %~ f - - ------------------------------------------------------------------------------ -- | Describes where hypotheses came from. Used extensively to prune stupid -- solutions from the search space. From b31ec5c59f4b60dadcefbee0f791f7c8681772bd Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 12:36:27 -0800 Subject: [PATCH 10/13] Track used variables in the Synthesis --- .../src/Ide/Plugin/Tactic/CodeGen.hs | 38 ++++++------------- .../Tactic/KnownStrategies/QuickCheck.hs | 1 + .../src/Ide/Plugin/Tactic/Machinery.hs | 14 +++---- .../src/Ide/Plugin/Tactic/Tactics.hs | 17 +++++---- .../src/Ide/Plugin/Tactic/Types.hs | 23 ++++------- 5 files changed, 34 insertions(+), 59 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs index 7893e501dc..50afe4d6bc 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs @@ -8,13 +8,10 @@ module Ide.Plugin.Tactic.CodeGen , module Ide.Plugin.Tactic.CodeGen.Utils ) where -import Control.Lens ((+~), (%~), (<>~)) +import Control.Lens ((+~)) import Control.Monad.Except -import Control.Monad.State (MonadState) -import Control.Monad.State.Class (modify) import Data.Generics.Product (field) import Data.List -import qualified Data.Map as M import qualified Data.Set as S import Data.Traversable import DataCon @@ -24,24 +21,15 @@ import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.CodeGen.Utils import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Naming import Ide.Plugin.Tactic.Types -import Ide.Plugin.Tactic.CodeGen.Utils import Type hiding (Var) -useOccName :: MonadState TacticState m => Judgement -> OccName -> m () -useOccName jdg name = - -- Only score points if this is in the local hypothesis - case M.lookup name $ hyByName $ jLocalHypothesis jdg of - Just{} -> modify - $ (withUsedVals $ S.insert name) - . (field @"ts_unused_top_vals" %~ S.delete name) - Nothing -> pure () - ------------------------------------------------------------------------------ -- | Doing recursion incurs a small penalty in the score. @@ -49,13 +37,6 @@ countRecursiveCall :: TacticState -> TacticState countRecursiveCall = field @"ts_recursion_count" +~ 1 ------------------------------------------------------------------------------- --- | Insert some values into the unused top values field. These are --- subsequently removed via 'useOccName'. -addUnusedTopVals :: MonadState TacticState m => S.Set OccName -> m () -addUnusedTopVals vals = modify $ field @"ts_unused_top_vals" <>~ vals - - destructMatches :: (DataCon -> Judgement -> Rule) -- ^ How to construct each match @@ -82,13 +63,14 @@ destructMatches f scrut t jdg = do $ coerce args j = introduce hy' $ withNewGoal g jdg - Synthesized tr sc sg <- f dc j + Synthesized tr sc uv sg <- f dc j pure $ Synthesized ( rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}") $ pure tr) (sc <> hy') + uv $ match [mkDestructPat dc names] $ unLoc sg @@ -157,15 +139,17 @@ destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule destruct' f hi jdg = do when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let term = hi_name hi - useOccName jdg term - Synthesized tr sc ms + Synthesized tr sc uv ms <- destructMatches f (Just term) (hi_type hi) $ disallowing AlreadyDestructed [term] jdg pure - $ Synthesized (rose ("destruct " <> show term) $ pure tr) sc + $ Synthesized + (rose ("destruct " <> show term) $ pure tr) + sc + (S.insert term uv) $ noLoc $ case' (var' term) ms @@ -193,7 +177,7 @@ buildDataCon -> RuleM (Synthesized (LHsExpr GhcPs)) buildDataCon jdg dc tyapps = do let args = dataConInstOrigArgTys' dc tyapps - Synthesized tr sc sgs + Synthesized tr sc uv sgs <- fmap unzipTrace $ traverse ( \(arg, n) -> newSubgoal @@ -203,6 +187,6 @@ buildDataCon jdg dc tyapps = do $ CType arg ) $ zip args [0..] pure - $ Synthesized (rose (show dc) $ pure tr) sc + $ Synthesized (rose (show dc) $ pure tr) sc uv $ mkCon dc sgs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index 9bdb810902..d81c067e1a 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -48,6 +48,7 @@ deriveArbitrary = do -- a bespoke binding "terminal", and a not-so-bespoke "n". -- But maybe it's fine for known rules? mempty + mempty $ noLoc $ let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $ appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index 0489f61d6e..7423756748 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -77,14 +77,9 @@ runTactic ctx jdg t = $ toList $ hyByName $ jHypothesis jdg - unused_topvals = M.keysSet - $ M.filter (isTopLevel . hi_provenance) - $ hyByName - $ jHypothesis jdg tacticState = defaultTacticState { ts_skolems = skolems - , ts_unused_top_vals = unused_topvals } in case partitionEithers . flip runReader ctx @@ -171,15 +166,18 @@ scoreSolution ) scoreSolution ext TacticState{..} holes = ( Penalize $ length holes - , Reward $ S.null $ intro_vals S.\\ ts_used_vals - , Penalize $ S.size ts_unused_top_vals + , Reward $ S.null $ intro_vals S.\\ used_vals + , Penalize $ S.size unused_top_vals , Penalize $ S.size intro_vals - , Reward $ S.size ts_used_vals + , Reward $ S.size $ traceIdX "used vals" $ used_vals , Penalize ts_recursion_count , Penalize $ solutionSize $ syn_val ext ) where intro_vals = M.keysSet $ hyByName $ syn_scoped ext + used_vals = S.intersection intro_vals $ syn_used_vals ext + top_vals = S.fromList . fmap hi_name . filter (isTopLevel . hi_provenance) $ unHypothesis $ syn_scoped ext + unused_top_vals = top_vals S.\\ used_vals ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 7a3d1e97a8..3ec089fe57 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -14,7 +14,6 @@ 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.Foldable import Data.List import qualified Data.Map as M @@ -54,8 +53,9 @@ assume name = rule $ \jdg -> do Just (hi_type -> ty) -> do unify ty $ jGoal jdg for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion - useOccName jdg name - pure $ Synthesized (tracePrim $ "assume " <> occNameString name) mempty + pure $ Synthesized (tracePrim $ "assume " <> occNameString name) + mempty + (S.singleton name) $ noLoc $ var' name Nothing -> throwError $ UndefinedHypothesis name @@ -88,12 +88,12 @@ intros = rule $ \jdg -> do hy' = lambdaHypothesis top_hole $ zip vs $ coerce as jdg' = introduce hy' $ withNewGoal (CType b) jdg - when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs - Synthesized tr sc sg <- newSubgoal jdg' + Synthesized tr sc uv sg <- newSubgoal jdg' pure . Synthesized (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr) (sc <> hy') + uv . noLoc . lambda (fmap bvar' vs) $ unLoc sg @@ -162,15 +162,16 @@ apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do -- Don't require new holes for locally bound vars; only respect linearity requireNewHoles $ rule $ \jdg -> do unify g (CType ret) - useOccName jdg func - sgs + Synthesized tr sc uv sgs <- fmap unzipTrace $ traverse ( newSubgoal . blacklistingDestruct . flip withNewGoal jdg . CType ) args - pure $ fmap (noLoc . foldl' (@@) (var' func) . fmap unLoc) sgs + pure $ Synthesized tr sc (S.insert func uv) + $ noLoc . foldl' (@@) (var' func) + $ fmap unLoc sgs ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index 0400aa080f..403f46aec2 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -88,10 +88,6 @@ data TacticState = TacticState -- ^ The known skolems. , ts_unifier :: !TCvSubst -- ^ The current substitution of univars. - , ts_used_vals :: !(Set OccName) - -- ^ Set of values used by tactics. - , ts_unused_top_vals :: !(Set OccName) - -- ^ Set of currently unused arguments to the function being defined. , ts_recursion_stack :: ![Maybe PatVal] -- ^ Stack for tracking whether or not the current recursive call has -- used at least one smaller pat val. Recursive calls for which this @@ -118,8 +114,6 @@ defaultTacticState = TacticState { ts_skolems = mempty , ts_unifier = emptyTCvSubst - , ts_used_vals = mempty - , ts_unused_top_vals = mempty , ts_recursion_stack = mempty , ts_recursion_count = 0 , ts_unique_gen = unsafeDefaultUniqueSupply @@ -147,11 +141,6 @@ popRecursionStack :: TacticState -> TacticState popRecursionStack = withRecursionStack tail -withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState -withUsedVals f = - field @"ts_used_vals" %~ f - - ------------------------------------------------------------------------------ -- | Describes where hypotheses came from. Used extensively to prune stupid -- solutions from the search space. @@ -264,7 +253,7 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where hole = pure - . Synthesized mempty mempty + . Synthesized mempty mempty mempty . noLoc $ var "_" @@ -338,21 +327,23 @@ data Synthesized a = Synthesized -- things it tried. , syn_scoped :: Hypothesis CType -- ^ All of the bindings created to produce the 'syn_val'. + , syn_used_vals :: Set OccName + -- ^ The values used when synthesizing the 'syn_val'. , syn_val :: a } deriving (Eq, Show, Functor, Foldable, Traversable) mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a -mapTrace f (Synthesized tr sc a) = Synthesized (f tr) sc a +mapTrace f (Synthesized tr sc uv a) = Synthesized (f tr) sc uv a ------------------------------------------------------------------------------ -- | This might not be lawful, due to the semigroup on 'Trace' maybe not being -- lawful. instance Applicative Synthesized where - pure = Synthesized mempty mempty - Synthesized tr1 sc1 f <*> Synthesized tr2 sc2 a = - Synthesized (tr1 <> tr2) (sc1 <> sc2) $ f a + pure = Synthesized mempty mempty mempty + Synthesized tr1 sc1 uv1 f <*> Synthesized tr2 sc2 uv2 a = + Synthesized (tr1 <> tr2) (sc1 <> sc2) (uv1 <> uv2) $ f a ------------------------------------------------------------------------------ From a6df284ac4dd3f46f342effefb40b1f806f191e7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 13:16:32 -0800 Subject: [PATCH 11/13] Remove a debug trace --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index 7423756748..b3ffd1671b 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -169,7 +169,7 @@ scoreSolution ext TacticState{..} holes , Reward $ S.null $ intro_vals S.\\ used_vals , Penalize $ S.size unused_top_vals , Penalize $ S.size intro_vals - , Reward $ S.size $ traceIdX "used vals" $ used_vals + , Reward $ S.size used_vals , Penalize ts_recursion_count , Penalize $ solutionSize $ syn_val ext ) From b8f70af909d25518f6d85bdcc96240ecb7cc31ed Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 13:16:53 -0800 Subject: [PATCH 12/13] Add some documentation about what's happening here. --- .../src/Ide/Plugin/Tactic/Tactics.hs | 4 ++++ .../src/Ide/Plugin/Tactic/Types.hs | 18 +++++++++++++++++- 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 3ec089fe57..07e468736b 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -65,6 +65,10 @@ recursion :: TacticsM () recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const defs) $ \(name, ty) -> do + -- TODO(sandy): When we can inspect the extract of a TacticsM bind + -- (requires refinery support), this recursion stack stuff is unnecessary. + -- We can just inspect the extract to see i we used any pattern vals, and + -- then be on our merry way. modify $ pushRecursionStack . countRecursiveCall ensure guardStructurallySmallerRecursion popRecursionStack $ do let hy' = recursiveHypothesis defs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index 403f46aec2..af1c9fc98e 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -83,6 +83,8 @@ instance Show (Pat GhcPs) where ------------------------------------------------------------------------------ +-- | The state that should be shared between subgoals. Extracts move towards +-- the root, judgments move towards the leaves, and the state moves *sideways*. data TacticState = TacticState { ts_skolems :: !(Set TyVar) -- ^ The known skolems. @@ -92,8 +94,16 @@ 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. + -- + -- TODO(sandy): This thing need not exist; we should just inspect + -- 'syn_used_vals' to see if anything was a pattern val. , ts_recursion_count :: !Int -- ^ Number of calls to recursion. We penalize each. + -- + -- TODO(sandy): This thing need not exist; it should just be a field + -- inside of 'Synthesized', but can't implement that without support from + -- refinery directly. Need the ability to get the extract of a TacticT + -- inside of TacticT, first. , ts_unique_gen :: !UniqSupply } deriving stock (Show, Generic) @@ -320,6 +330,11 @@ type Rule = RuleM (Synthesized (LHsExpr GhcPs)) type Trace = Rose String +------------------------------------------------------------------------------ +-- | The extract for refinery. Represents a "synthesized attribute" in the +-- context of attribute grammars. In essence, 'Synthesized' describes +-- information we'd like to pass from leaves of the tactics search upwards. +-- This includes the actual AST we've generated (in 'syn_val'). data Synthesized a = Synthesized { syn_trace :: Trace -- ^ A tree describing which tactics were used produce the 'syn_val'. @@ -339,7 +354,8 @@ mapTrace f (Synthesized tr sc uv a) = Synthesized (f tr) sc uv a ------------------------------------------------------------------------------ -- | This might not be lawful, due to the semigroup on 'Trace' maybe not being --- lawful. +-- lawful. But that's only for debug output, so it's not anything I'm concerned +-- about. instance Applicative Synthesized where pure = Synthesized mempty mempty mempty Synthesized tr1 sc1 uv1 f <*> Synthesized tr2 sc2 uv2 a = From 117fa0a43556edcef1349f1e243e1adc59752d28 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 26 Feb 2021 13:32:41 -0800 Subject: [PATCH 13/13] Minor tidying --- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 2 +- plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs index b00f4185bc..3fb774d4d1 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs @@ -23,6 +23,7 @@ import Data.Aeson import Data.Bifunctor (Bifunctor (bimap)) import Data.Bool (bool) import Data.Data (Data) +import Data.Foldable (for_) import Data.Generics.Aliases (mkQ) import Data.Generics.Schemes (everything) import Data.Maybe @@ -50,7 +51,6 @@ import Language.LSP.Types.Capabilities import OccName import Prelude hiding (span) import System.Timeout -import Data.Foldable (for_) descriptor :: PluginId -> PluginDescriptor IdeState diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 07e468736b..f355013664 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -72,8 +72,6 @@ recursion = requireConcreteHole $ tracing "recursion" $ do modify $ pushRecursionStack . countRecursiveCall ensure guardStructurallySmallerRecursion popRecursionStack $ do let hy' = recursiveHypothesis defs - - -- TODO(sandy): do we need to add this to syn_scoped? localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy') <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -164,6 +162,7 @@ apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do let (_, _, args, ret) = tacticsSplitFunTy ty' -- TODO(sandy): Bug here! Prevents us from doing mono-map like things -- Don't require new holes for locally bound vars; only respect linearity + -- see https://github.com/haskell/haskell-language-server/issues/1447 requireNewHoles $ rule $ \jdg -> do unify g (CType ret) Synthesized tr sc uv sgs