Skip to content

Commit dcd8299

Browse files
isovectorisovector
authored
Simplify extracts after running tactics (#1351)
* More tests of overlapping methods * Do a simplification pass of the extract * Do less work when simplifiying * Remove unnecessary parens simplification * Implement simplify as a fold over endos * Fix tests * Haddock for the new module * Minor note on implementation * Note a TODO * Use PatCompat to unpack patterns * Pull out codegen utilities to break a cyclic dependency * Re-export utils * Try a different strategy for generalizing PatCompat * Try, try again to compat * Could this be the answer we've all been waiting for?
1 parent 5cfe4ec commit dcd8299

17 files changed

+233
-66
lines changed

‎plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ library
2525
Ide.Plugin.Tactic
2626
Ide.Plugin.Tactic.Auto
2727
Ide.Plugin.Tactic.CodeGen
28+
Ide.Plugin.Tactic.CodeGen.Utils
2829
Ide.Plugin.Tactic.Context
2930
Ide.Plugin.Tactic.Debug
3031
Ide.Plugin.Tactic.GHC
@@ -34,6 +35,7 @@ library
3435
Ide.Plugin.Tactic.Machinery
3536
Ide.Plugin.Tactic.Naming
3637
Ide.Plugin.Tactic.Range
38+
Ide.Plugin.Tactic.Simplify
3739
Ide.Plugin.Tactic.Tactics
3840
Ide.Plugin.Tactic.Types
3941
Ide.Plugin.Tactic.TestTypes

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -327,6 +327,7 @@ tacticCmd tac lf state (TacticParams uri range var_name)
327327
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
328328
Right rtr -> do
329329
traceMX "solns" $ rtr_other_solns rtr
330+
traceMX "after simplification" $ rtr_extract rtr
330331
let g = graft (RealSrcSpan span) $ rtr_extract rtr
331332
response = transform dflags (clientCapabilities lf) uri g pm
332333
pure $ case response of

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs

Lines changed: 7 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
1-
{-# LANGUAGE DataKinds #-}
2-
{-# LANGUAGE TypeApplications #-}
1+
{-# LANGUAGE DataKinds #-}
32
{-# LANGUAGE FlexibleContexts #-}
43
{-# LANGUAGE TupleSections #-}
4+
{-# LANGUAGE TypeApplications #-}
55
{-# LANGUAGE ViewPatterns #-}
66

7-
module Ide.Plugin.Tactic.CodeGen where
7+
module Ide.Plugin.Tactic.CodeGen
8+
( module Ide.Plugin.Tactic.CodeGen
9+
, module Ide.Plugin.Tactic.CodeGen.Utils
10+
) where
811

912
import Control.Lens ((+~), (%~), (<>~))
1013
import Control.Monad.Except
@@ -18,7 +21,6 @@ import Data.Traversable
1821
import DataCon
1922
import Development.IDE.GHC.Compat
2023
import GHC.Exts
21-
import GHC.SourceGen (RdrNameStr)
2224
import GHC.SourceGen.Binds
2325
import GHC.SourceGen.Expr
2426
import GHC.SourceGen.Overloaded
@@ -28,7 +30,7 @@ import Ide.Plugin.Tactic.Judgements
2830
import Ide.Plugin.Tactic.Machinery
2931
import Ide.Plugin.Tactic.Naming
3032
import Ide.Plugin.Tactic.Types
31-
import Name
33+
import Ide.Plugin.Tactic.CodeGen.Utils
3234
import Type hiding (Var)
3335

3436

@@ -202,57 +204,3 @@ buildDataCon jdg dc apps = do
202204
. (rose (show dc) $ pure tr,)
203205
$ mkCon dc sgs
204206

205-
206-
mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
207-
mkCon dcon (fmap unLoc -> args)
208-
| isTupleDataCon dcon =
209-
noLoc $ tuple args
210-
| dataConIsInfix dcon
211-
, (lhs : rhs : args') <- args =
212-
noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'
213-
| otherwise =
214-
noLoc $ foldl' (@@) (bvar' $ occName dcon_name) args
215-
where
216-
dcon_name = dataConName dcon
217-
218-
219-
220-
coerceName :: HasOccName a => a -> RdrNameStr
221-
coerceName = fromString . occNameString . occName
222-
223-
224-
225-
------------------------------------------------------------------------------
226-
-- | Like 'var', but works over standard GHC 'OccName's.
227-
var' :: Var a => OccName -> a
228-
var' = var . fromString . occNameString
229-
230-
231-
------------------------------------------------------------------------------
232-
-- | Like 'bvar', but works over standard GHC 'OccName's.
233-
bvar' :: BVar a => OccName -> a
234-
bvar' = bvar . fromString . occNameString
235-
236-
237-
------------------------------------------------------------------------------
238-
-- | Get an HsExpr corresponding to a function name.
239-
mkFunc :: String -> HsExpr GhcPs
240-
mkFunc = var' . mkVarOcc
241-
242-
243-
------------------------------------------------------------------------------
244-
-- | Get an HsExpr corresponding to a value name.
245-
mkVal :: String -> HsExpr GhcPs
246-
mkVal = var' . mkVarOcc
247-
248-
249-
------------------------------------------------------------------------------
250-
-- | Like 'op', but easier to call.
251-
infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
252-
infixCall s = flip op (fromString s)
253-
254-
255-
------------------------------------------------------------------------------
256-
-- | Like '(@@)', but uses a dollar instead of parentheses.
257-
appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
258-
appDollar = infixCall "$"

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen/Utils.hs

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
{-# LANGUAGE ViewPatterns #-}
2+
3+
module Ide.Plugin.Tactic.CodeGen.Utils where
4+
5+
import Data.List
6+
import DataCon
7+
import Development.IDE.GHC.Compat
8+
import GHC.Exts
9+
import GHC.SourceGen (RdrNameStr)
10+
import GHC.SourceGen.Overloaded
11+
import Name
12+
13+
14+
------------------------------------------------------------------------------
15+
-- | Make a data constructor with the given arguments.
16+
mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
17+
mkCon dcon (fmap unLoc -> args)
18+
| isTupleDataCon dcon =
19+
noLoc $ tuple args
20+
| dataConIsInfix dcon
21+
, (lhs : rhs : args') <- args =
22+
noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'
23+
| otherwise =
24+
noLoc $ foldl' (@@) (bvar' $ occName dcon_name) args
25+
where
26+
dcon_name = dataConName dcon
27+
28+
29+
coerceName :: HasOccName a => a -> RdrNameStr
30+
coerceName = fromString . occNameString . occName
31+
32+
33+
------------------------------------------------------------------------------
34+
-- | Like 'var', but works over standard GHC 'OccName's.
35+
var' :: Var a => OccName -> a
36+
var' = var . fromString . occNameString
37+
38+
39+
------------------------------------------------------------------------------
40+
-- | Like 'bvar', but works over standard GHC 'OccName's.
41+
bvar' :: BVar a => OccName -> a
42+
bvar' = bvar . fromString . occNameString
43+
44+
45+
------------------------------------------------------------------------------
46+
-- | Get an HsExpr corresponding to a function name.
47+
mkFunc :: String -> HsExpr GhcPs
48+
mkFunc = var' . mkVarOcc
49+
50+
51+
------------------------------------------------------------------------------
52+
-- | Get an HsExpr corresponding to a value name.
53+
mkVal :: String -> HsExpr GhcPs
54+
mkVal = var' . mkVarOcc
55+
56+
57+
------------------------------------------------------------------------------
58+
-- | Like 'op', but easier to call.
59+
infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
60+
infixCall s = flip op (fromString s)
61+
62+
63+
------------------------------------------------------------------------------
64+
-- | Like '(@@)', but uses a dollar instead of parentheses.
65+
appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
66+
appDollar = infixCall "$"
67+

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -112,13 +112,17 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
112112
= Just $ isJust $ algebraicTyCon res
113113
lambdaCaseable _ = Nothing
114114

115-
fromPatCompat :: PatCompat GhcTc -> Pat GhcTc
115+
-- It's hard to generalize over these since weird type families are involved.
116+
fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc
117+
fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs
116118
#if __GLASGOW_HASKELL__ == 808
117119
type PatCompat pass = Pat pass
118-
fromPatCompat = id
120+
fromPatCompatTc = id
121+
fromPatCompatPs = id
119122
#else
120123
type PatCompat pass = LPat pass
121-
fromPatCompat = unLoc
124+
fromPatCompatTc = unLoc
125+
fromPatCompatPs = unLoc
122126
#endif
123127

124128
------------------------------------------------------------------------------
@@ -132,7 +136,7 @@ pattern TopLevelRHS name ps body <-
132136
[L _ (GRHS _ [] body)] _)
133137

134138
getPatName :: PatCompat GhcTc -> Maybe OccName
135-
getPatName (fromPatCompat -> p0) =
139+
getPatName (fromPatCompatTc -> p0) =
136140
case p0 of
137141
VarPat _ x -> Just $ occName $ unLoc x
138142
LazyPat _ p -> getPatName p

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ import Data.Set (Set)
3333
import qualified Data.Set as S
3434
import Development.IDE.GHC.Compat
3535
import Ide.Plugin.Tactic.Judgements
36+
import Ide.Plugin.Tactic.Simplify (simplify)
3637
import Ide.Plugin.Tactic.Types
3738
import OccName (HasOccName(occName))
3839
import Refinery.ProofState
@@ -97,7 +98,7 @@ runTactic ctx jdg t =
9798
case sorted of
9899
(((tr, ext), _) : _) ->
99100
Right
100-
. RunTacticResults tr ext
101+
. RunTacticResults tr (simplify ext)
101102
. reverse
102103
. fmap fst
103104
$ take 5 sorted

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Simplify.hs

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
{-# LANGUAGE LambdaCase #-}
2+
{-# LANGUAGE OverloadedStrings #-}
3+
{-# LANGUAGE PatternSynonyms #-}
4+
{-# LANGUAGE ScopedTypeVariables #-}
5+
{-# LANGUAGE ViewPatterns #-}
6+
7+
module Ide.Plugin.Tactic.Simplify
8+
( simplify
9+
) where
10+
11+
import Data.Data (Data)
12+
import Data.Generics (everywhere, somewhere, something, listify, extT, mkT, GenericT, mkQ)
13+
import Data.List.Extra (unsnoc)
14+
import Data.Maybe (isJust)
15+
import Data.Monoid (Endo (..))
16+
import Development.IDE.GHC.Compat
17+
import GHC.Exts (fromString)
18+
import GHC.SourceGen (var, op)
19+
import GHC.SourceGen.Expr (lambda)
20+
import Ide.Plugin.Tactic.CodeGen.Utils
21+
import Ide.Plugin.Tactic.GHC (fromPatCompatPs)
22+
23+
24+
------------------------------------------------------------------------------
25+
-- | A pattern over the otherwise (extremely) messy AST for lambdas.
26+
pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
27+
pattern Lambda pats body <-
28+
HsLam _
29+
(MG {mg_alts = L _ [L _
30+
(Match { m_pats = fmap fromPatCompatPs -> pats
31+
, m_grhss = GRHSs {grhssGRHSs = [L _ (
32+
GRHS _ [] (L _ body))]}
33+
})]})
34+
where
35+
-- If there are no patterns to bind, just stick in the body
36+
Lambda [] body = body
37+
Lambda pats body = lambda pats body
38+
39+
40+
------------------------------------------------------------------------------
41+
-- | Simlify an expression.
42+
simplify :: LHsExpr GhcPs -> LHsExpr GhcPs
43+
simplify
44+
= head
45+
. drop 3 -- Do three passes; this should be good enough for the limited
46+
-- amount of gas we give to auto
47+
. iterate (everywhere $ foldEndo
48+
[ simplifyEtaReduce
49+
, simplifyRemoveParens
50+
, simplifyCompose
51+
])
52+
53+
54+
------------------------------------------------------------------------------
55+
-- | Like 'foldMap' but for endomorphisms.
56+
foldEndo :: Foldable t => t (a -> a) -> a -> a
57+
foldEndo = appEndo . foldMap Endo
58+
59+
60+
------------------------------------------------------------------------------
61+
-- | Does this thing contain any references to 'HsVar's with the given
62+
-- 'RdrName'?
63+
containsHsVar :: Data a => RdrName -> a -> Bool
64+
containsHsVar name x = not $ null $ listify (
65+
\case
66+
((HsVar _ (L _ a)) :: HsExpr GhcPs) | a == name -> True
67+
_ -> False
68+
) x
69+
70+
71+
------------------------------------------------------------------------------
72+
-- | Perform an eta reduction. For example, transforms @\x -> (f g) x@ into
73+
-- @f g@.
74+
simplifyEtaReduce :: GenericT
75+
simplifyEtaReduce = mkT $ \case
76+
Lambda
77+
[VarPat _ (L _ pat)]
78+
(HsVar _ (L _ a)) | pat == a ->
79+
var "id"
80+
Lambda
81+
(unsnoc -> Just (pats, (VarPat _ (L _ pat))))
82+
(HsApp _ (L _ f) (L _ (HsVar _ (L _ a))))
83+
| pat == a
84+
-- We can only perform this simplifiation if @pat@ is otherwise unused.
85+
, not (containsHsVar pat f) ->
86+
Lambda pats f
87+
x -> x
88+
89+
90+
------------------------------------------------------------------------------
91+
-- | Perform an eta-reducing function composition. For example, transforms
92+
-- @\x -> f (g (h x))@ into @f . g . h@.
93+
simplifyCompose :: GenericT
94+
simplifyCompose = mkT $ \case
95+
Lambda
96+
(unsnoc -> Just (pats, (VarPat _ (L _ pat))))
97+
(unroll -> (fs@(_:_), (HsVar _ (L _ a))))
98+
| pat == a
99+
-- We can only perform this simplifiation if @pat@ is otherwise unused.
100+
, not (containsHsVar pat fs) ->
101+
Lambda pats (foldr1 (infixCall ".") fs)
102+
x -> x
103+
104+
105+
------------------------------------------------------------------------------
106+
-- | Removes unnecessary parentheses on any token that doesn't need them.
107+
simplifyRemoveParens :: GenericT
108+
simplifyRemoveParens = mkT $ \case
109+
HsPar _ (L _ x) | isAtomicHsExpr x -> x
110+
(x :: HsExpr GhcPs) -> x
111+
112+
113+
------------------------------------------------------------------------------
114+
-- | Unrolls a right-associative function application of the form
115+
-- @HsApp f (HsApp g (HsApp h x))@ into @([f, g, h], x)@.
116+
unroll :: HsExpr GhcPs -> ([HsExpr GhcPs], HsExpr GhcPs)
117+
unroll (HsPar _ (L _ x)) = unroll x
118+
unroll (HsApp _ (L _ f) (L _ a)) =
119+
let (fs, r) = unroll a
120+
in (f : fs, r)
121+
unroll x = ([], x)
122+

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,9 @@ instance Show DataCon where
7070
instance Show Class where
7171
show = unsafeRender
7272

73+
instance Show (HsExpr GhcPs) where
74+
show = unsafeRender
75+
7376

7477
------------------------------------------------------------------------------
7578
data TacticState = TacticState

‎test/functional/Tactic.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,9 @@ tests = testGroup
117117
, expectFail "GoldenFish.hs" 5 18 Auto ""
118118
, goldenTest "GoldenArbitrary.hs" 25 13 Auto ""
119119
, goldenTest "FmapBoth.hs" 2 12 Auto ""
120+
, goldenTest "FmapJoin.hs" 2 14 Auto ""
121+
, goldenTest "Fgmap.hs" 2 9 Auto ""
122+
, goldenTest "FmapJoinInLet.hs" 4 19 Auto ""
120123
]
121124

122125

‎test/testdata/tactic/Fgmap.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b))
2+
fgmap = _

‎test/testdata/tactic/Fgmap.hs.expected

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b))
2+
fgmap = (fmap . fmap)

‎test/testdata/tactic/FmapJoin.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)
2+
fJoin = fmap _

‎test/testdata/tactic/FmapJoin.hs.expected

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)
2+
fJoin = fmap (\ mma -> (>>=) mma id)

‎test/testdata/tactic/FmapJoinInLet.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{-# LANGUAGE ScopedTypeVariables #-}
2+
3+
fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a)
4+
fJoin = let f = (_ :: m (m a) -> m a) in fmap f

‎test/testdata/tactic/FmapJoinInLet.hs.expected

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{-# LANGUAGE ScopedTypeVariables #-}
2+
3+
fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a)
4+
fJoin = let f = ( (\ mma -> (>>=) mma id) :: m (m a) -> m a) in fmap f

0 commit comments

Comments
 (0)