From 629067e47d02b5dff3e2cf25c36850b63faa958d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 07:10:12 -0800 Subject: [PATCH 1/9] Add some new code generator combinators --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 7ee099c20d..d4fd01f814 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -236,3 +236,16 @@ var' = var . fromString . occNameString bvar' :: BVar a => OccName -> a bvar' = bvar . fromString . occNameString + +mkFunc :: String -> HsExpr GhcPs +mkFunc = var' . mkVarOcc + +mkVal :: String -> HsExpr GhcPs +mkVal = var' . mkVarOcc + +infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +infixCall s = flip op (fromString s) + +appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +appDollar = infixCall "$" + From 917879a3bcada9a3396aea53ea284e46e4b47c15 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 07:10:45 -0800 Subject: [PATCH 2/9] Add QuickCheck known strategies --- plugins/tactics/hls-tactics-plugin.cabal | 1 + .../Tactic/KnownStrategies/QuickCheck.hs | 92 +++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs diff --git a/plugins/tactics/hls-tactics-plugin.cabal b/plugins/tactics/hls-tactics-plugin.cabal index bc5a4b03f1..aa1256c02c 100644 --- a/plugins/tactics/hls-tactics-plugin.cabal +++ b/plugins/tactics/hls-tactics-plugin.cabal @@ -30,6 +30,7 @@ library Ide.Plugin.Tactic.GHC Ide.Plugin.Tactic.Judgements Ide.Plugin.Tactic.KnownStrategies + Ide.Plugin.Tactic.KnownStrategies.QuickCheck Ide.Plugin.Tactic.Machinery Ide.Plugin.Tactic.Naming Ide.Plugin.Tactic.Range diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs new file mode 100644 index 0000000000..937398923d --- /dev/null +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} + +module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where + +import Data.Bool (bool) +import Data.List (partition) +import DataCon ( DataCon, dataConName ) +import Development.IDE.GHC.Compat (HsExpr, GhcPs, noLoc) +import GHC.Exts ( IsString(fromString) ) +import GHC.List ( foldl' ) +import GHC.SourceGen (int) +import GHC.SourceGen.Binds ( match, valBind ) +import GHC.SourceGen.Expr ( case', lambda, let' ) +import GHC.SourceGen.Overloaded ( App((@@)), HasList(list) ) +import GHC.SourceGen.Pat ( conP ) +import Ide.Plugin.Tactic.CodeGen +import Ide.Plugin.Tactic.Judgements (jGoal) +import Ide.Plugin.Tactic.Machinery (tracePrim) +import Ide.Plugin.Tactic.Types ( Type, TacticsM, CType(unCType) ) +import OccName ( mkVarOcc, HasOccName(occName) ) +import Refinery.Tactic ( rule ) +import TyCon ( TyCon, tyConDataCons ) +import Type ( splitTyConApp_maybe ) + + +deriveArbitrary :: TacticsM () +deriveArbitrary = rule $ \jdg -> do + let arb_ty = unCType $ jGoal jdg + case splitTyConApp_maybe arb_ty of + Just (_gen_tc, [splitTyConApp_maybe -> Just (tc, apps)]) -> do + let dcs = tyConDataCons tc + (small, big) = partition ((== 0) . genRecursiveCount) + $ fmap (mkGenerator tc apps) dcs + small_expr = mkVal "small" + oneof_expr = mkVal "oneof" + pure + ( tracePrim "hi" + , noLoc $ + let' [valBind (fromString "small") $ list $ fmap genExpr small] $ + appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ + case' (infixCall "<=" (mkVal "n") (int 1)) + [ match [conP (fromString "True") []] $ + oneof_expr @@ small_expr + , match [conP (fromString "False") []] $ + appDollar oneof_expr $ + infixCall "<>" + (list $ fmap genExpr big) + small_expr + ] + ) + + +data Generator = Generator + { genRecursiveCount :: Integer + , genExpr :: HsExpr GhcPs + } + + +mkGenerator :: TyCon -> [Type] -> DataCon -> Generator +mkGenerator tc apps dc = do + let dc_expr = var' $ occName $ dataConName dc + args = dataConInstOrigArgTys' dc apps + num_recursive_calls = sum $ fmap (bool 0 1 . isRecursiveValue tc) args + mkArbitrary = mkArbitraryCall tc num_recursive_calls + Generator num_recursive_calls $ case args of + [] -> mkFunc "pure" @@ dc_expr + (a : as) -> + foldl' + (infixCall "<*>") + (infixCall "<$>" dc_expr $ mkArbitrary a) + (fmap mkArbitrary as) + + +isRecursiveValue :: TyCon -> Type -> Bool +isRecursiveValue recursive_tc (splitTyConApp_maybe -> Just (tc, _)) + = recursive_tc == tc +isRecursiveValue _ _ = False + + +mkArbitraryCall :: TyCon -> Integer -> Type -> HsExpr GhcPs +mkArbitraryCall recursive_tc n ty = + let arbitrary = mkFunc "arbitrary" + in case splitTyConApp_maybe ty of + Just (tc, _) | tc == recursive_tc -> + mkFunc "scale" + @@ bool (mkFunc "div" @@ int n) + (mkFunc "subtract" @@ int 1) + (n == 1) + @@ arbitrary + _ -> arbitrary + From 31e69ba39b82933f1a0811587e1f0216704e9007 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 07:13:01 -0800 Subject: [PATCH 3/9] Hook up the new known strategy --- plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs index 610740aba3..ca42e15ac5 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -9,11 +9,13 @@ import Ide.Plugin.Tactic.Types import OccName (mkVarOcc) import Refinery.Tactic import Ide.Plugin.Tactic.Machinery (tracing) +import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary) knownStrategies :: TacticsM () knownStrategies = choice - [ deriveFmap + [ known "fmap" deriveFmap + , known "arbitrary" deriveArbitrary ] @@ -26,7 +28,7 @@ known name t = do deriveFmap :: TacticsM () -deriveFmap = known "fmap" $ do +deriveFmap = do try intros overAlgebraicTerms homo choice From 750a08ce3dee4394c86d93726e41255f4c77e19d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 07:21:55 -0800 Subject: [PATCH 4/9] Make sure arbitrary has the right type --- .../Tactic/KnownStrategies/QuickCheck.hs | 61 ++++++++++--------- 1 file changed, 33 insertions(+), 28 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index 937398923d..6a195bdf6b 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -3,6 +3,7 @@ module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where +import Control.Monad.Except (MonadError(throwError)) import Data.Bool (bool) import Data.List (partition) import DataCon ( DataCon, dataConName ) @@ -17,38 +18,42 @@ import GHC.SourceGen.Pat ( conP ) import Ide.Plugin.Tactic.CodeGen import Ide.Plugin.Tactic.Judgements (jGoal) import Ide.Plugin.Tactic.Machinery (tracePrim) -import Ide.Plugin.Tactic.Types ( Type, TacticsM, CType(unCType) ) -import OccName ( mkVarOcc, HasOccName(occName) ) -import Refinery.Tactic ( rule ) -import TyCon ( TyCon, tyConDataCons ) +import Ide.Plugin.Tactic.Types +import OccName (occNameString, mkVarOcc, HasOccName(occName) ) +import Refinery.Tactic (goal, rule ) +import TyCon (tyConName, TyCon, tyConDataCons ) import Type ( splitTyConApp_maybe ) deriveArbitrary :: TacticsM () -deriveArbitrary = rule $ \jdg -> do - let arb_ty = unCType $ jGoal jdg - case splitTyConApp_maybe arb_ty of - Just (_gen_tc, [splitTyConApp_maybe -> Just (tc, apps)]) -> do - let dcs = tyConDataCons tc - (small, big) = partition ((== 0) . genRecursiveCount) - $ fmap (mkGenerator tc apps) dcs - small_expr = mkVal "small" - oneof_expr = mkVal "oneof" - pure - ( tracePrim "hi" - , noLoc $ - let' [valBind (fromString "small") $ list $ fmap genExpr small] $ - appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ - case' (infixCall "<=" (mkVal "n") (int 1)) - [ match [conP (fromString "True") []] $ - oneof_expr @@ small_expr - , match [conP (fromString "False") []] $ - appDollar oneof_expr $ - infixCall "<>" - (list $ fmap genExpr big) - small_expr - ] - ) +deriveArbitrary = do + ty <- jGoal <$> goal + case splitTyConApp_maybe $ unCType ty of + Just (gen_tc, [splitTyConApp_maybe -> Just (tc, apps)]) + | occNameString (occName $ tyConName gen_tc) == "Gen" -> do + rule $ \_ -> do + let dcs = tyConDataCons tc + (small, big) = partition ((== 0) . genRecursiveCount) + $ fmap (mkGenerator tc apps) dcs + small_expr = mkVal "small" + oneof_expr = mkVal "oneof" + pure + ( tracePrim "deriveArbitrary" + , noLoc $ + let' [valBind (fromString "small") $ list $ fmap genExpr small] $ + appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ + case' (infixCall "<=" (mkVal "n") (int 1)) + [ match [conP (fromString "True") []] $ + oneof_expr @@ small_expr + , match [conP (fromString "False") []] $ + appDollar oneof_expr $ + infixCall "<>" + (list $ fmap genExpr big) + small_expr + ] + ) + _ -> throwError $ GoalMismatch "deriveArbitrary" ty + data Generator = Generator From 9d3243e3fca45c4f085e1181b73b8896f72f7503 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 07:51:57 -0800 Subject: [PATCH 5/9] Be more strict about what constitutes a recursive constructor --- .../Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index 6a195bdf6b..ccf574d5bc 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -23,6 +23,7 @@ import OccName (occNameString, mkVarOcc, HasOccName(occName) ) import Refinery.Tactic (goal, rule ) import TyCon (tyConName, TyCon, tyConDataCons ) import Type ( splitTyConApp_maybe ) +import Data.Generics (mkQ, everything) deriveArbitrary :: TacticsM () @@ -78,20 +79,19 @@ mkGenerator tc apps dc = do isRecursiveValue :: TyCon -> Type -> Bool -isRecursiveValue recursive_tc (splitTyConApp_maybe -> Just (tc, _)) - = recursive_tc == tc -isRecursiveValue _ _ = False +isRecursiveValue recursive_tc = + everything (||) $ mkQ False (== recursive_tc) mkArbitraryCall :: TyCon -> Integer -> Type -> HsExpr GhcPs mkArbitraryCall recursive_tc n ty = let arbitrary = mkFunc "arbitrary" - in case splitTyConApp_maybe ty of - Just (tc, _) | tc == recursive_tc -> + in case isRecursiveValue recursive_tc ty of + True -> mkFunc "scale" @@ bool (mkFunc "div" @@ int n) (mkFunc "subtract" @@ int 1) (n == 1) @@ arbitrary - _ -> arbitrary + False -> arbitrary From b6916bdbd2e08dfee9c4fb910eac14811d785d6d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 08:00:11 -0800 Subject: [PATCH 6/9] Rename "small" to "terminal" --- .../Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index ccf574d5bc..ccc61c3007 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -34,23 +34,23 @@ deriveArbitrary = do | occNameString (occName $ tyConName gen_tc) == "Gen" -> do rule $ \_ -> do let dcs = tyConDataCons tc - (small, big) = partition ((== 0) . genRecursiveCount) + (terminal, big) = partition ((== 0) . genRecursiveCount) $ fmap (mkGenerator tc apps) dcs - small_expr = mkVal "small" + terminal_expr = mkVal "terminal" oneof_expr = mkVal "oneof" pure ( tracePrim "deriveArbitrary" , noLoc $ - let' [valBind (fromString "small") $ list $ fmap genExpr small] $ + let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $ appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ case' (infixCall "<=" (mkVal "n") (int 1)) [ match [conP (fromString "True") []] $ - oneof_expr @@ small_expr + oneof_expr @@ terminal_expr , match [conP (fromString "False") []] $ appDollar oneof_expr $ infixCall "<>" (list $ fmap genExpr big) - small_expr + terminal_expr ] ) _ -> throwError $ GoalMismatch "deriveArbitrary" ty From 36a61db8cf45a4a051c1e28738690f780c29e43f Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 08:00:27 -0800 Subject: [PATCH 7/9] Add an arbitrary test --- test/functional/Tactic.hs | 1 + test/testdata/tactic/GoldenArbitrary.hs | 26 ++++++++++ .../tactic/GoldenArbitrary.hs.expected | 52 +++++++++++++++++++ 3 files changed, 79 insertions(+) create mode 100644 test/testdata/tactic/GoldenArbitrary.hs create mode 100644 test/testdata/tactic/GoldenArbitrary.hs.expected diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 7eeac215d8..0850fc741e 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -116,6 +116,7 @@ tests = testGroup $ goldenTest "GoldenApplicativeThen.hs" 2 11 Auto "" , goldenTest "GoldenSafeHead.hs" 2 12 Auto "" , expectFail "GoldenFish.hs" 5 18 Auto "" + , goldenTest "GoldenArbitrary.hs" 25 13 Auto "" ] diff --git a/test/testdata/tactic/GoldenArbitrary.hs b/test/testdata/tactic/GoldenArbitrary.hs new file mode 100644 index 0000000000..f45d2d1fea --- /dev/null +++ b/test/testdata/tactic/GoldenArbitrary.hs @@ -0,0 +1,26 @@ +-- Emulate a quickcheck import; deriveArbitrary works on any type with the +-- right name and kind +data Gen a + +data Obj + = Square Int Int + | Circle Int + | Polygon [(Int, Int)] + | Rotate2 Double Obj + | Empty + | Full + | Complement Obj + | UnionR Double [Obj] + | DifferenceR Double Obj [Obj] + | IntersectR Double [Obj] + | Translate Double Double Obj + | Scale Double Double Obj + | Mirror Double Double Obj + | Outset Double Obj + | Shell Double Obj + | WithRounding Double Obj + + +arbitrary :: Gen Obj +arbitrary = _ + diff --git a/test/testdata/tactic/GoldenArbitrary.hs.expected b/test/testdata/tactic/GoldenArbitrary.hs.expected new file mode 100644 index 0000000000..881b57c760 --- /dev/null +++ b/test/testdata/tactic/GoldenArbitrary.hs.expected @@ -0,0 +1,52 @@ +-- Emulate a quickcheck import; deriveArbitrary works on any type with the +-- right name and kind +data Gen a + +data Obj + = Square Int Int + | Circle Int + | Polygon [(Int, Int)] + | Rotate2 Double Obj + | Empty + | Full + | Complement Obj + | UnionR Double [Obj] + | DifferenceR Double Obj [Obj] + | IntersectR Double [Obj] + | Translate Double Double Obj + | Scale Double Double Obj + | Mirror Double Double Obj + | Outset Double Obj + | Shell Double Obj + | WithRounding Double Obj + + +arbitrary :: Gen Obj +arbitrary = (let + terminal + = [(Square <$> arbitrary) <*> arbitrary, Circle <$> arbitrary, + Polygon <$> arbitrary, pure Empty, pure Full] + in + sized + $ (\ n + -> case n <= 1 of + True -> oneof terminal + False + -> oneof + $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary, + Complement <$> scale (subtract 1) arbitrary, + (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary, + ((DifferenceR <$> arbitrary) <*> scale (div 2) arbitrary) + <*> scale (div 2) arbitrary, + (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary, + ((Translate <$> arbitrary) <*> arbitrary) + <*> scale (subtract 1) arbitrary, + ((Scale <$> arbitrary) <*> arbitrary) + <*> scale (subtract 1) arbitrary, + ((Mirror <$> arbitrary) <*> arbitrary) + <*> scale (subtract 1) arbitrary, + (Outset <$> arbitrary) <*> scale (subtract 1) arbitrary, + (Shell <$> arbitrary) <*> scale (subtract 1) arbitrary, + (WithRounding <$> arbitrary) <*> scale (subtract 1) arbitrary] + <> terminal))) + From 10e2530818618f67883cba5d2a6b82fde4d611ab Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 08:09:07 -0800 Subject: [PATCH 8/9] Make sure to flip `div`! --- .../src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs | 2 +- test/testdata/tactic/GoldenArbitrary.hs.expected | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index ccc61c3007..055684517e 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -89,7 +89,7 @@ mkArbitraryCall recursive_tc n ty = in case isRecursiveValue recursive_tc ty of True -> mkFunc "scale" - @@ bool (mkFunc "div" @@ int n) + @@ bool (mkFunc "flip" @@ mkFunc "div" @@ int n) (mkFunc "subtract" @@ int 1) (n == 1) @@ arbitrary diff --git a/test/testdata/tactic/GoldenArbitrary.hs.expected b/test/testdata/tactic/GoldenArbitrary.hs.expected index 881b57c760..a3f677d1a1 100644 --- a/test/testdata/tactic/GoldenArbitrary.hs.expected +++ b/test/testdata/tactic/GoldenArbitrary.hs.expected @@ -36,8 +36,8 @@ arbitrary = (let $ ([(Rotate2 <$> arbitrary) <*> scale (subtract 1) arbitrary, Complement <$> scale (subtract 1) arbitrary, (UnionR <$> arbitrary) <*> scale (subtract 1) arbitrary, - ((DifferenceR <$> arbitrary) <*> scale (div 2) arbitrary) - <*> scale (div 2) arbitrary, + ((DifferenceR <$> arbitrary) <*> scale (flip div 2) arbitrary) + <*> scale (flip div 2) arbitrary, (IntersectR <$> arbitrary) <*> scale (subtract 1) arbitrary, ((Translate <$> arbitrary) <*> arbitrary) <*> scale (subtract 1) arbitrary, From 14a07c94d90f03758bd2d087f47d0ae8bf5615a7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 23 Dec 2020 08:14:32 -0800 Subject: [PATCH 9/9] Haddock for the new additions --- .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 11 ++++++++ .../Tactic/KnownStrategies/QuickCheck.hs | 25 +++++++++++++++---- 2 files changed, 31 insertions(+), 5 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index d4fd01f814..3a3785971c 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -237,15 +237,26 @@ bvar' :: BVar a => OccName -> a bvar' = bvar . fromString . occNameString +------------------------------------------------------------------------------ +-- | Get an HsExpr corresponding to a function name. mkFunc :: String -> HsExpr GhcPs mkFunc = var' . mkVarOcc + +------------------------------------------------------------------------------ +-- | Get an HsExpr corresponding to a value name. mkVal :: String -> HsExpr GhcPs mkVal = var' . mkVarOcc + +------------------------------------------------------------------------------ +-- | Like 'op', but easier to call. infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs infixCall s = flip op (fromString s) + +------------------------------------------------------------------------------ +-- | Like '(@@)', but uses a dollar instead of parentheses. appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs appDollar = infixCall "$" diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs index 055684517e..c29c1d58d8 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -26,6 +26,11 @@ import Type ( splitTyConApp_maybe ) import Data.Generics (mkQ, everything) +------------------------------------------------------------------------------ +-- | Known tactic for deriving @arbitrary :: Gen a@. This tactic splits the +-- type's data cons into terminal and inductive cases, and generates code that +-- produces a terminal if the QuickCheck size parameter is <=1, or any data con +-- otherwise. It correctly scales recursive parameters, ensuring termination. deriveArbitrary :: TacticsM () deriveArbitrary = do ty <- jGoal <$> goal @@ -56,18 +61,21 @@ deriveArbitrary = do _ -> throwError $ GoalMismatch "deriveArbitrary" ty - +------------------------------------------------------------------------------ +-- | Helper data type for the generator of a specific data con. data Generator = Generator { genRecursiveCount :: Integer , genExpr :: HsExpr GhcPs } +------------------------------------------------------------------------------ +-- | Make a 'Generator' for a given tycon instantiated with the given @[Type]@. mkGenerator :: TyCon -> [Type] -> DataCon -> Generator mkGenerator tc apps dc = do let dc_expr = var' $ occName $ dataConName dc args = dataConInstOrigArgTys' dc apps - num_recursive_calls = sum $ fmap (bool 0 1 . isRecursiveValue tc) args + num_recursive_calls = sum $ fmap (bool 0 1 . doesTypeContain tc) args mkArbitrary = mkArbitraryCall tc num_recursive_calls Generator num_recursive_calls $ case args of [] -> mkFunc "pure" @@ dc_expr @@ -78,15 +86,22 @@ mkGenerator tc apps dc = do (fmap mkArbitrary as) -isRecursiveValue :: TyCon -> Type -> Bool -isRecursiveValue recursive_tc = +------------------------------------------------------------------------------ +-- | Check if the given 'TyCon' exists anywhere in the 'Type'. +doesTypeContain :: TyCon -> Type -> Bool +doesTypeContain recursive_tc = everything (||) $ mkQ False (== recursive_tc) +------------------------------------------------------------------------------ +-- | Generate the correct sort of call to @arbitrary@. For recursive calls, we +-- need to scale down the size parameter, either by a constant factor of 1 if +-- it's the only recursive parameter, or by @`div` n@ where n is the number of +-- recursive parameters. For all other types, just call @arbitrary@ directly. mkArbitraryCall :: TyCon -> Integer -> Type -> HsExpr GhcPs mkArbitraryCall recursive_tc n ty = let arbitrary = mkFunc "arbitrary" - in case isRecursiveValue recursive_tc ty of + in case doesTypeContain recursive_tc ty of True -> mkFunc "scale" @@ bool (mkFunc "flip" @@ mkFunc "div" @@ int n)