diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -56,8 +56,6 @@ " d to perform a pattern match, n to fill a hole nnoremap d :set operatorfunc=WingmanDestructg@l nnoremap n :set operatorfunc=WingmanFillHoleg@l - -" beta only nnoremap r :set operatorfunc=WingmanRefineg@l nnoremap c :set operatorfunc=WingmanUseCtorg@l nnoremap a :set operatorfunc=WingmanDestructAllg@l diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal --- a/hls-tactics-plugin.cabal +++ b/hls-tactics-plugin.cabal @@ -1,7 +1,7 @@ cabal-version: 2.4 category: Development name: hls-tactics-plugin -version: 1.1.0.0 +version: 1.2.0.0 synopsis: Wingman plugin for Haskell Language Server description: Please see README.md author: Sandy Maguire, Reed Mullanix @@ -15,7 +15,6 @@ extra-source-files: README.md test/golden/*.cabal - test/golden/*.expected test/golden/*.hs test/golden/*.yaml @@ -34,7 +33,7 @@ Wingman.CodeGen.Utils Wingman.Context Wingman.Debug - Wingman.FeatureSet + Wingman.EmptyCase Wingman.GHC Wingman.Judgements Wingman.Judgements.SYB @@ -42,12 +41,18 @@ Wingman.KnownStrategies Wingman.KnownStrategies.QuickCheck Wingman.LanguageServer + Wingman.LanguageServer.Metaprogram Wingman.LanguageServer.TacticProviders Wingman.Machinery + Wingman.Metaprogramming.Lexer + Wingman.Metaprogramming.Parser + Wingman.Metaprogramming.Parser.Documentation + Wingman.Metaprogramming.ProofState Wingman.Naming Wingman.Plugin Wingman.Range Wingman.Simplify + Wingman.StaticPlugin Wingman.Tactics Wingman.Types @@ -72,14 +77,18 @@ , ghc-boot-th , ghc-exactprint , ghc-source-gen - , ghcide ^>=1.2 + , ghcide ^>=1.4 + , hls-graph , hls-plugin-api ^>=1.1 + , hyphenation , lens , lsp + , megaparsec ^>=9 , mtl + , parser-combinators + , prettyprinter , refinery ^>=0.3 , retrie >=0.1.1.0 - , shake , syb , text , transformers @@ -117,10 +126,13 @@ AutoTupleSpec CodeAction.AutoSpec CodeAction.DestructAllSpec + CodeAction.DestructPunSpec CodeAction.DestructSpec CodeAction.IntrosSpec CodeAction.RefineSpec + CodeAction.RunMetaprogramSpec CodeAction.UseDataConSpec + CodeLens.EmptyCaseSpec ProviderSpec Spec UnificationSpec @@ -141,7 +153,7 @@ , ghcide , hls-plugin-api , hls-tactics-plugin - , hls-test-utils ^>= 1.0 + , hls-test-utils ^>=1.0 , hspec , hspec-expectations , lens diff --git a/src/Wingman/Auto.hs b/src/Wingman/Auto.hs --- a/src/Wingman/Auto.hs +++ b/src/Wingman/Auto.hs @@ -1,5 +1,7 @@ + module Wingman.Auto where +import Control.Monad.Reader.Class (asks) import Control.Monad.State (gets) import qualified Data.Set as S import Refinery.Tactic @@ -17,13 +19,14 @@ auto = do jdg <- goal skolems <- gets ts_skolems + gas <- asks $ cfg_auto_gas . ctxConfig current <- getCurrentDefinitions traceMX "goal" jdg traceMX "ctx" current traceMX "skolems" skolems commit knownStrategies . tracing "auto" - . localTactic (auto' 4) + . localTactic (auto' gas) . disallowing RecursiveCall . S.fromList $ fmap fst current diff --git a/src/Wingman/CaseSplit.hs b/src/Wingman/CaseSplit.hs --- a/src/Wingman/CaseSplit.hs +++ b/src/Wingman/CaseSplit.hs @@ -56,9 +56,17 @@ ------------------------------------------------------------------------------ -- | Replace a 'VarPat' with the given @'Pat' GhcPs@. rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a -rewriteVarPat name rep = everywhere $ mkT $ \case - VarPat _ (L _ var) | eqRdrName name var -> rep - (x :: Pat GhcPs) -> x +rewriteVarPat name rep = everywhere $ + mkT (\case + VarPat _ (L _ var) | eqRdrName name var -> rep + (x :: Pat GhcPs) -> x + ) + `extT` \case + HsRecField lbl _ True + | eqRdrName name $ unLoc $ rdrNameFieldOcc $ unLoc lbl + -> HsRecField lbl (toPatCompat rep) False + (x :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> x + ------------------------------------------------------------------------------ diff --git a/src/Wingman/CodeGen.hs b/src/Wingman/CodeGen.hs --- a/src/Wingman/CodeGen.hs +++ b/src/Wingman/CodeGen.hs @@ -1,7 +1,8 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE OverloadedLabels #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} module Wingman.CodeGen ( module Wingman.CodeGen @@ -12,21 +13,24 @@ import ConLike import Control.Lens ((%~), (<>~), (&)) import Control.Monad.Except +import Control.Monad.Reader (ask) import Control.Monad.State import Data.Bool (bool) +import Data.Functor ((<&>)) import Data.Generics.Labels () import Data.List -import Data.Monoid (Endo(..)) import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat import GHC.Exts +import GHC.SourceGen (occNameToStr) import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat -import GhcPlugins (isSymOcc) +import GhcPlugins (isSymOcc, mkVarOccFS) +import OccName (occName) import PatSyn import Type hiding (Var) import Wingman.CodeGen.Utils @@ -39,7 +43,8 @@ destructMatches - :: (ConLike -> Judgement -> Rule) + :: Bool + -> (ConLike -> Judgement -> Rule) -- ^ How to construct each match -> Maybe OccName -- ^ Scrutinee @@ -47,49 +52,106 @@ -- ^ Type being destructed -> Judgement -> RuleM (Synthesized [RawMatch]) -destructMatches f scrut t jdg = do +-- TODO(sandy): In an ideal world, this would be the same codepath as +-- 'destructionFor'. Make sure to change that if you ever change this. +destructMatches use_field_puns f scrut t jdg = do let hy = jEntireHypothesis jdg g = jGoal jdg - case splitTyConApp_maybe $ unCType t of + case tacticsGetDataCons $ unCType t of Nothing -> throwError $ GoalMismatch "destruct" g - Just (tc, apps) -> do - let dcs = tyConDataCons tc - case dcs of - [] -> throwError $ GoalMismatch "destruct" g - _ -> fmap unzipTrace $ for dcs $ \dc -> do - let con = RealDataCon dc - ev = concatMap mkEvidence $ dataConInstArgTys dc apps - -- We explicitly do not need to add the method hypothesis to - -- #syn_scoped - method_hy = foldMap evidenceToHypothesis ev - args = conLikeInstOrigArgTys' con apps - modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev - subst <- gets ts_unifier - names <- mkManyGoodNames (hyNamesInScope hy) args - let hy' = patternHypothesis scrut con jdg - $ zip names - $ coerce args - j = fmap (CType . substTyAddInScope subst . unCType) - $ introduce hy' - $ introduce method_hy - $ withNewGoal g jdg - ext <- f con j - pure $ ext - & #syn_trace %~ rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}") - . pure - & #syn_scoped <>~ hy' - & #syn_val %~ match [mkDestructPat con names] . unLoc + Just (dcs, apps) -> + fmap unzipTrace $ for dcs $ \dc -> do + let con = RealDataCon dc + ev = concatMap mkEvidence $ dataConInstArgTys dc apps + -- We explicitly do not need to add the method hypothesis to + -- #syn_scoped + method_hy = foldMap evidenceToHypothesis ev + args = conLikeInstOrigArgTys' con apps + modify $ evidenceToSubst ev + subst <- gets ts_unifier + ctx <- ask + let names_in_scope = hyNamesInScope hy + names = mkManyGoodNames (hyNamesInScope hy) args + (names', destructed) = + mkDestructPat (bool Nothing (Just names_in_scope) use_field_puns) con names + let hy' = patternHypothesis scrut con jdg + $ zip names' + $ coerce args + j = fmap (CType . substTyAddInScope subst . unCType) + $ introduce ctx hy' + $ introduce ctx method_hy + $ withNewGoal g jdg + ext <- f con j + pure $ ext + & #syn_trace %~ rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names') <> "}") + . pure + & #syn_scoped <>~ hy' + & #syn_val %~ match [destructed] . unLoc + + ------------------------------------------------------------------------------ +-- | Generate just the 'Match'es for a case split on a specific type. +destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)] +-- TODO(sandy): In an ideal world, this would be the same codepath as +-- 'destructMatches'. Make sure to change that if you ever change this. +destructionFor hy t = do + case tacticsGetDataCons t of + Nothing -> Nothing + Just ([], _) -> Nothing + Just (dcs, apps) -> do + for dcs $ \dc -> do + let con = RealDataCon dc + args = conLikeInstOrigArgTys' con apps + names = mkManyGoodNames (hyNamesInScope hy) args + pure + . noLoc + . Match + noExtField + CaseAlt + [toPatCompat $ snd $ mkDestructPat Nothing con names] + . GRHSs noExtField (pure $ noLoc $ GRHS noExtField [] $ noLoc $ var "_") + . noLoc + $ EmptyLocalBinds noExtField + + + +------------------------------------------------------------------------------ -- | Produces a pattern for a data con and the names of its fields. -mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs -mkDestructPat con names +mkDestructPat :: Maybe (S.Set OccName) -> ConLike -> [OccName] -> ([OccName], Pat GhcPs) +mkDestructPat already_in_scope con names | RealDataCon dcon <- con , isTupleDataCon dcon = - tuple pat_args + (names, tuple pat_args) + | fields@(_:_) <- zip (conLikeFieldLabels con) names + , Just in_scope <- already_in_scope = + let (names', rec_fields) = + unzip $ fields <&> \(label, name) -> do + let label_occ = mkVarOccFS $ flLabel label + case S.member label_occ in_scope of + -- We have a shadow, so use the generated name instead + True -> + (name,) $ noLoc $ + HsRecField + (noLoc $ mkFieldOcc $ noLoc $ Unqual label_occ) + (noLoc $ bvar' name) + False + -- No shadow, safe to use a pun + False -> + (label_occ,) $ noLoc $ + HsRecField + (noLoc $ mkFieldOcc $ noLoc $ Unqual label_occ) + (noLoc $ bvar' label_occ) + True + + in (names', ) + $ ConPatIn (noLoc $ Unqual $ occName $ conLikeName con) + $ RecCon + $ HsRecFields rec_fields + $ Nothing | otherwise = - infixifyPatIfNecessary con $ + (names, ) $ infixifyPatIfNecessary con $ conP (coerceName $ conLikeName con) pat_args @@ -151,12 +213,13 @@ -- | Combinator for performing case splitting, and running sub-rules on the -- resulting matches. -destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule -destruct' f hi jdg = do +destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule +destruct' use_field_puns f hi jdg = do when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let term = hi_name hi ext <- destructMatches + use_field_puns f (Just term) (hi_type hi) @@ -170,14 +233,14 @@ ------------------------------------------------------------------------------ -- | Combinator for performign case splitting, and running sub-rules on the -- resulting matches. -destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule -destructLambdaCase' f jdg = do +destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule +destructLambdaCase' use_field_puns f jdg = do when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic let g = jGoal jdg case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> fmap (fmap noLoc lambdaCase) <$> - destructMatches f Nothing (CType arg) jdg + destructMatches use_field_puns f Nothing (CType arg) jdg _ -> throwError $ GoalMismatch "destructLambdaCase'" g @@ -190,7 +253,22 @@ -> [Type] -- ^ Type arguments for the data con -> RuleM (Synthesized (LHsExpr GhcPs)) buildDataCon should_blacklist jdg dc tyapps = do - let args = conLikeInstOrigArgTys' dc tyapps + args <- case dc of + RealDataCon dc' -> do + let (skolems', theta, args) = dataConInstSig dc' tyapps + modify $ \ts -> + evidenceToSubst (foldMap mkEvidence theta) ts + & #ts_skolems <>~ S.fromList skolems' + pure args + _ -> + -- If we have a 'PatSyn', we can't continue, since there is no + -- 'dataConInstSig' equivalent for 'PatSyn's. I don't think this is + -- a fundamental problem, but I don't know enough about the GHC internals + -- to implement it myself. + -- + -- Fortunately, this isn't an issue in practice, since 'PatSyn's are + -- never in the hypothesis. + throwError $ TacticPanic "Can't build Pattern constructors yet" ext <- fmap unzipTrace $ traverse ( \(arg, n) -> @@ -212,4 +290,29 @@ | isSymOcc occ = noLoc $ foldl' (@@) (op lhs (coerceName occ) rhs) more mkApply occ args = noLoc $ foldl' (@@) (var' occ) args + + +------------------------------------------------------------------------------ +-- | Run a tactic over each term in the given 'Hypothesis', binding the results +-- of each in a let expression. +letForEach + :: (OccName -> OccName) -- ^ How to name bound variables + -> (HyInfo CType -> TacticsM ()) -- ^ The tactic to run + -> Hypothesis CType -- ^ Terms to generate bindings for + -> Judgement -- ^ The goal of original hole + -> RuleM (Synthesized (LHsExpr GhcPs)) +letForEach rename solve (unHypothesis -> hy) jdg = do + case hy of + [] -> newSubgoal jdg + _ -> do + ctx <- ask + let g = jGoal jdg + terms <- fmap sequenceA $ for hy $ \hi -> do + let name = rename $ hi_name hi + res <- tacticToRule jdg $ solve hi + pure $ fmap ((name,) . unLoc) res + let hy' = fmap (g <$) $ syn_val terms + matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms + g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg + pure $ fmap noLoc $ let' <$> matches <*> g diff --git a/src/Wingman/CodeGen/Utils.hs b/src/Wingman/CodeGen/Utils.hs --- a/src/Wingman/CodeGen/Utils.hs +++ b/src/Wingman/CodeGen/Utils.hs @@ -5,7 +5,7 @@ import DataCon import Development.IDE.GHC.Compat import GHC.Exts -import GHC.SourceGen (RdrNameStr, recordConE, string) +import GHC.SourceGen (RdrNameStr (UnqualStr), recordConE, string) import GHC.SourceGen.Overloaded import GhcPlugins (nilDataCon, charTy, eqType) import Name @@ -43,7 +43,7 @@ coerceName :: HasOccName a => a -> RdrNameStr -coerceName = fromString . occNameString . occName +coerceName = UnqualStr . fromString . occNameString . occName ------------------------------------------------------------------------------ diff --git a/src/Wingman/Context.hs b/src/Wingman/Context.hs --- a/src/Wingman/Context.hs +++ b/src/Wingman/Context.hs @@ -3,45 +3,60 @@ import Bag import Control.Arrow import Control.Monad.Reader +import Data.Coerce (coerce) import Data.Foldable.Extra (allM) -import Data.Maybe (fromMaybe, isJust) +import Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import Development.IDE.GHC.Compat -import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys) +import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env) import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import OccName import TcRnTypes import TcType (tcSplitTyConApp, tcSplitPhiTy) import TysPrim (alphaTys) -import Wingman.FeatureSet (FeatureSet) +import Wingman.GHC (normalizeType) import Wingman.Judgements.Theta import Wingman.Types mkContext - :: FeatureSet + :: Config -> [(OccName, CType)] -> TcGblEnv -> ExternalPackageState -> KnownThings -> [Evidence] -> Context -mkContext features locals tcg eps kt ev = Context - { ctxDefiningFuncs = locals - , ctxModuleFuncs = fmap splitId - . (getFunBindId =<<) - . fmap unLoc - . bagToList - $ tcg_binds tcg - , ctxFeatureSet = features - , ctxInstEnvs = - InstEnvs - (eps_inst_env eps) - (tcg_inst_env tcg) - (tcVisibleOrphanMods tcg) - , ctxKnownThings = kt - , ctxTheta = evidenceToThetaType ev - } +mkContext cfg locals tcg eps kt ev = fix $ \ctx -> + Context + { ctxDefiningFuncs + = fmap (second $ coerce $ normalizeType ctx) locals + , ctxModuleFuncs + = fmap (second (coerce $ normalizeType ctx) . splitId) + . mappend (locallyDefinedMethods tcg) + . (getFunBindId =<<) + . fmap unLoc + . bagToList + $ tcg_binds tcg + , ctxConfig = cfg + , ctxFamInstEnvs = + (eps_fam_inst_env eps, tcg_fam_inst_env tcg) + , ctxInstEnvs = + InstEnvs + (eps_inst_env eps) + (tcg_inst_env tcg) + (tcVisibleOrphanMods tcg) + , ctxKnownThings = kt + , ctxTheta = evidenceToThetaType ev + } + + +locallyDefinedMethods :: TcGblEnv -> [Id] +locallyDefinedMethods + = foldMap classMethods + . mapMaybe tyConClass_maybe + . tcg_tcs + splitId :: Id -> (OccName, CType) diff --git a/src/Wingman/EmptyCase.hs b/src/Wingman/EmptyCase.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/EmptyCase.hs @@ -0,0 +1,160 @@ +{-# LANGUAGE OverloadedStrings #-} + +{-# LANGUAGE NoMonoLocalBinds #-} + +module Wingman.EmptyCase where + +import Control.Applicative (empty) +import Control.Monad +import Control.Monad.Except (runExcept) +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Data.Aeson +import Data.Generics.Aliases (mkQ, GenericQ) +import Data.Generics.Schemes (everything) +import Data.Maybe +import Data.Monoid +import qualified Data.Text as T +import Data.Traversable +import Development.IDE (hscEnv) +import Development.IDE (realSrcSpanToRange) +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Shake (IdeState (..)) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat +import Development.IDE.GHC.ExactPrint +import Development.IDE.Spans.LocalBindings (getLocalScope) +import Ide.Types +import Language.LSP.Server +import Language.LSP.Types +import OccName +import Prelude hiding (span) +import Prelude hiding (span) +import TcRnTypes (tcg_binds) +import Wingman.CodeGen (destructionFor) +import Wingman.GHC +import Wingman.Judgements +import Wingman.LanguageServer +import Wingman.Types + + +------------------------------------------------------------------------------ +-- | The 'CommandId' for the empty case completion. +emptyCaseLensCommandId :: CommandId +emptyCaseLensCommandId = CommandId "wingman.emptyCase" + + +------------------------------------------------------------------------------ +-- | A command function that just applies a 'WorkspaceEdit'. +workspaceEditHandler :: CommandFunction IdeState WorkspaceEdit +workspaceEditHandler _ideState wedit = do + _ <- sendRequest SWorkspaceApplyEdit (ApplyWorkspaceEditParams Nothing wedit) (\_ -> pure ()) + return $ Right Null + + +------------------------------------------------------------------------------ +-- | Provide the "empty case completion" code lens +codeLensProvider :: PluginMethodHandler IdeState TextDocumentCodeLens +codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri)) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + let stale a = runStaleIde "codeLensProvider" state nfp a + + cfg <- getTacticConfig plId + ccs <- getClientCapabilities + liftIO $ fromMaybeT (Right $ List []) $ do + dflags <- getIdeDynflags state nfp + TrackedStale pm _ <- stale GetAnnotatedParsedSource + TrackedStale binds bind_map <- stale GetBindings + holes <- emptyCaseScrutinees state nfp + + fmap (Right . List) $ for holes $ \(ss, ty) -> do + binds_ss <- liftMaybe $ mapAgeFrom bind_map ss + let bindings = getLocalScope (unTrack binds) $ unTrack binds_ss + range = realSrcSpanToRange $ unTrack ss + matches <- + liftMaybe $ + destructionFor + (foldMap (hySingleton . occName . fst) bindings) + ty + edits <- liftMaybe $ hush $ + mkWorkspaceEdits dflags ccs uri (unTrack pm) $ + graftMatchGroup (RealSrcSpan $ unTrack ss) $ + noLoc matches + + pure $ + CodeLens range + (Just + $ mkLspCommand + plId + emptyCaseLensCommandId + (mkEmptyCaseLensDesc ty) + $ Just $ pure $ toJSON $ edits + ) + Nothing +codeLensProvider _ _ _ = pure $ Right $ List [] + + +------------------------------------------------------------------------------ +-- | The description for the empty case lens. +mkEmptyCaseLensDesc :: Type -> T.Text +mkEmptyCaseLensDesc ty = + "Wingman: Complete case constructors (" <> T.pack (unsafeRender ty) <> ")" + + +------------------------------------------------------------------------------ +-- | Silence an error. +hush :: Either e a -> Maybe a +hush (Left _) = Nothing +hush (Right a) = Just a + + +------------------------------------------------------------------------------ +-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly +-- deals with top-level holes, in which we might need to fiddle with the +-- 'Match's that bind variables. +graftMatchGroup + :: SrcSpan + -> Located [LMatch GhcPs (LHsExpr GhcPs)] + -> Graft (Either String) ParsedSource +graftMatchGroup ss l = + hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case + L span (HsCase ext scrut mg@_) -> do + pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l } + (_ :: LHsExpr GhcPs) -> pure Nothing + + +fromMaybeT :: Functor m => a -> MaybeT m a -> m a +fromMaybeT def = fmap (fromMaybe def) . runMaybeT + + +------------------------------------------------------------------------------ +-- | Find the last typechecked module, and find the most specific span, as well +-- as the judgement at the given range. +emptyCaseScrutinees + :: IdeState + -> NormalizedFilePath + -> MaybeT IO [(Tracked 'Current RealSrcSpan, Type)] +emptyCaseScrutinees state nfp = do + let stale a = runStaleIde "emptyCaseScrutinees" state nfp a + + TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck + let tcg' = unTrack tcg + hscenv <- stale GhcSessionDeps + + let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg + for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do + ty <- MaybeT $ typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg' scrutinee + case ss of + RealSrcSpan r -> do + rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r + pure (rss', ty) + UnhelpfulSpan _ -> empty + + +------------------------------------------------------------------------------ +-- | Get the 'SrcSpan' and scrutinee of every empty case. +emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)] +emptyCaseQ = everything (<>) $ mkQ mempty $ \case + L new_span (Case scrutinee []) -> pure (new_span, scrutinee) + (_ :: LHsExpr GhcTc) -> mempty + diff --git a/src/Wingman/FeatureSet.hs b/src/Wingman/FeatureSet.hs deleted file mode 100644 --- a/src/Wingman/FeatureSet.hs +++ /dev/null @@ -1,94 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Wingman.FeatureSet - ( Feature (..) - , FeatureSet - , hasFeature - , defaultFeatures - , allFeatures - , parseFeatureSet - , prettyFeatureSet - ) where - -import Data.List (intercalate) -import Data.Maybe (listToMaybe, mapMaybe) -import Data.Set (Set) -import qualified Data.Set as S -import qualified Data.Text as T - - ------------------------------------------------------------------------------- --- | All the available features. A 'FeatureSet' describes the ones currently --- available to the user. -data Feature - = FeatureDestructAll - | FeatureUseDataCon - | FeatureRefineHole - | FeatureKnownMonoid - deriving (Eq, Ord, Show, Read, Enum, Bounded) - - ------------------------------------------------------------------------------- --- | A collection of enabled features. -type FeatureSet = Set Feature - - ------------------------------------------------------------------------------- --- | Parse a feature set. -parseFeatureSet :: T.Text -> FeatureSet -parseFeatureSet - = mappend defaultFeatures - . S.fromList - . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack) - . T.split (== '/') - - ------------------------------------------------------------------------------- --- | Features that are globally enabled for all users. -defaultFeatures :: FeatureSet -defaultFeatures = S.fromList - [ - ] - - ------------------------------------------------------------------------------- --- | All available features. -allFeatures :: FeatureSet -allFeatures = S.fromList $ enumFromTo minBound maxBound - - ------------------------------------------------------------------------------- --- | Pretty print a feature set. -prettyFeatureSet :: FeatureSet -> String -prettyFeatureSet - = intercalate "/" - . fmap (rot13 . drop (length featurePrefix) . show) - . S.toList - - ------------------------------------------------------------------------------- --- | Is a given 'Feature' currently enabled? -hasFeature :: Feature -> FeatureSet -> Bool -hasFeature = S.member - - ------------------------------------------------------------------------------- --- | Like 'read', but not partial. -readMaybe :: Read a => String -> Maybe a -readMaybe = fmap fst . listToMaybe . reads - - -featurePrefix :: String -featurePrefix = "Feature" - - -rot13 :: String -> String -rot13 = fmap (toEnum . rot13int . fromEnum) - - -rot13int :: Integral a => a -> a -rot13int x - | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26 - | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26 - | otherwise = x - diff --git a/src/Wingman/GHC.hs b/src/Wingman/GHC.hs --- a/src/Wingman/GHC.hs +++ b/src/Wingman/GHC.hs @@ -3,10 +3,12 @@ module Wingman.GHC where +import Bag (bagToList) import ConLike import Control.Applicative (empty) import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) +import CoreUtils (exprType) import Data.Function (on) import Data.Functor ((<&>)) import Data.List (isPrefixOf) @@ -18,10 +20,14 @@ import DataCon import Development.IDE (HscEnvEq (hscEnv)) import Development.IDE.Core.Compile (lookupName) -import Development.IDE.GHC.Compat +import Development.IDE.GHC.Compat hiding (exprType) +import DsExpr (dsExpr) +import DsMonad (initDs) +import FamInst (tcLookupDataFamInst_maybe) +import FamInstEnv (normaliseType) import GHC.SourceGen (lambda) import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT) -import GhcPlugins (extractModule, GlobalRdrElt (gre_name)) +import GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal)) import OccName import TcRnMonad import TcType @@ -70,7 +76,7 @@ -- context. tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type) tacticsSplitFunTy t - = let (vars, theta, t') = tcSplitSigmaTy t + = let (vars, theta, t') = tcSplitNestedSigmaTys t (args, res) = tcSplitFunTys t' in (vars, theta, args, res) @@ -193,6 +199,15 @@ } +pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +pattern SingleLet bind pats val expr <- + HsLet _ + (L _ (HsValBinds _ + (ValBinds _ (bagToList -> + [(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _))) + (L _ expr) + + ------------------------------------------------------------------------------ -- | A pattern over the otherwise (extremely) messy AST for lambdas. pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs @@ -341,6 +356,43 @@ Just tt -> liftMaybe $ f tt _ -> empty + liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a + + +------------------------------------------------------------------------------ +-- | Get the type of an @HsExpr GhcTc@. This is slow and you should prefer to +-- not use it, but sometimes it can't be helped. +typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type) +typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr + + +mkFunTys' :: [Type] -> Type -> Type +mkFunTys' = +#if __GLASGOW_HASKELL__ <= 808 + mkFunTys +#else + mkVisFunTys +#endif + + +------------------------------------------------------------------------------ +-- | Expand type and data families +normalizeType :: Context -> Type -> Type +normalizeType ctx ty = + let ty' = expandTyFam ctx ty + in case tcSplitTyConApp_maybe ty' of + Just (tc, tys) -> + -- try to expand any data families + case tcLookupDataFamInst_maybe (ctxFamInstEnvs ctx) tc tys of + Just (dtc, dtys, _) -> mkAppTys (mkTyConTy dtc) dtys + Nothing -> ty' + Nothing -> ty' + +------------------------------------------------------------------------------ +-- | Expand type families +expandTyFam :: Context -> Type -> Type +expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal + diff --git a/src/Wingman/Judgements.hs b/src/Wingman/Judgements.hs --- a/src/Wingman/Judgements.hs +++ b/src/Wingman/Judgements.hs @@ -17,7 +17,7 @@ import OccName import SrcLoc import Type -import Wingman.GHC (algebraicTyCon) +import Wingman.GHC (algebraicTyCon, normalizeType) import Wingman.Types @@ -40,6 +40,13 @@ | otherwise = Nothing +------------------------------------------------------------------------------ +-- | Build a trivial hypothesis containing only a single name. The corresponding +-- HyInfo has no provenance or type. +hySingleton :: OccName -> Hypothesis () +hySingleton n = Hypothesis . pure $ HyInfo n UserPrv () + + blacklistingDestruct :: Judgement -> Judgement blacklistingDestruct = field @"_jBlacklistDestruct" .~ True @@ -62,11 +69,19 @@ withNewGoal t = field @"_jGoal" .~ t -introduce :: Hypothesis a -> Judgement' a -> Judgement' a +normalizeHypothesis :: Functor f => Context -> f CType -> f CType +normalizeHypothesis = fmap . coerce . normalizeType + +normalizeJudgement :: Functor f => Context -> f CType -> f CType +normalizeJudgement = normalizeHypothesis + + +introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType -- NOTE(sandy): It's important that we put the new hypothesis terms first, -- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs -- after a previously-destructed term. -introduce hy = field @"_jHypothesis" %~ mappend hy +introduce ctx hy = + field @"_jHypothesis" %~ mappend (normalizeHypothesis ctx hy) ------------------------------------------------------------------------------ @@ -101,6 +116,12 @@ ------------------------------------------------------------------------------ +-- | Introduce a binding in a recursive context. +userHypothesis :: [(OccName, a)] -> Hypothesis a +userHypothesis = introduceHypothesis $ const $ const UserPrv + + +------------------------------------------------------------------------------ -- | Check whether any of the given occnames are an ancestor of the term. hasPositionalAncestry :: Foldable t @@ -222,6 +243,7 @@ provAncestryOf (ClassMethodPrv _) = mempty provAncestryOf UserPrv = mempty provAncestryOf RecursivePrv = mempty +provAncestryOf ImportPrv = mempty provAncestryOf (DisallowedPrv _ p2) = provAncestryOf p2 @@ -295,6 +317,12 @@ ------------------------------------------------------------------------------ +-- | Filter elements from the hypothesis +hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a +hyFilter f = Hypothesis . filter f . unHypothesis + + +------------------------------------------------------------------------------ -- | Given a judgment, return the hypotheses that are acceptable to destruct. -- -- We use the ordering of the hypothesis for this purpose. Since new bindings @@ -373,17 +401,20 @@ mkFirstJudgement - :: Hypothesis CType + :: Context + -> Hypothesis CType -> Bool -- ^ are we in the top level rhs hole? -> Type -> Judgement' CType -mkFirstJudgement hy top goal = Judgement - { _jHypothesis = hy - , _jBlacklistDestruct = False - , _jWhitelistSplit = True - , _jIsTopHole = top - , _jGoal = CType goal - } +mkFirstJudgement ctx hy top goal = + normalizeJudgement ctx $ + Judgement + { _jHypothesis = hy + , _jBlacklistDestruct = False + , _jWhitelistSplit = True + , _jIsTopHole = top + , _jGoal = CType goal + } ------------------------------------------------------------------------------ diff --git a/src/Wingman/Judgements/SYB.hs b/src/Wingman/Judgements/SYB.hs --- a/src/Wingman/Judgements/SYB.hs +++ b/src/Wingman/Judgements/SYB.hs @@ -4,12 +4,15 @@ -- | Custom SYB traversals module Wingman.Judgements.SYB where -import Data.Foldable (foldl') -import Data.Generics hiding (typeRep) -import Development.IDE.GHC.Compat -import GHC.Exts (Any) -import Type.Reflection -import Unsafe.Coerce (unsafeCoerce) +import Data.Foldable (foldl') +import Data.Generics hiding (typeRep) +import qualified Data.Text as T +import Development.IDE.GHC.Compat +import GHC.Exts (Any) +import GhcPlugins (unpackFS) +import Type.Reflection +import Unsafe.Coerce (unsafeCoerce) +import Wingman.StaticPlugin (pattern WingmanMetaprogram) ------------------------------------------------------------------------------ @@ -80,4 +83,10 @@ Just HRefl -> True Nothing -> False _ -> False + + +metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)] +metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case + L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program) + (_ :: LHsExpr GhcTc) -> mempty diff --git a/src/Wingman/Judgements/Theta.hs b/src/Wingman/Judgements/Theta.hs --- a/src/Wingman/Judgements/Theta.hs +++ b/src/Wingman/Judgements/Theta.hs @@ -12,13 +12,16 @@ import Class (classTyVars) import Control.Applicative (empty) +import Control.Lens (preview) import Data.Maybe (fromMaybe, mapMaybe, maybeToList) +import Data.Generics.Sum (_Ctor) import Data.Set (Set) import qualified Data.Set as S import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat -import Generics.SYB hiding (tyConName, empty) -import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst) +import Generics.SYB hiding (tyConName, empty, Generic) +import GHC.Generics +import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst, unionTCvSubst, emptyTCvSubst, TCvSubst) #if __GLASGOW_HASKELL__ > 806 import GhcPlugins (eqTyCon) #else @@ -40,7 +43,7 @@ = EqualityOfTypes Type Type -- | We have an instance in scope | HasInstance PredType - deriving (Show) + deriving (Show, Generic) ------------------------------------------------------------------------------ @@ -75,21 +78,46 @@ . unTrack ------------------------------------------------------------------------------- --- | Update our knowledge of which types are equal. -evidenceToSubst :: Evidence -> TacticState -> TacticState -evidenceToSubst (EqualityOfTypes a b) ts = +mkSubst :: Set TyVar -> Type -> Type -> TCvSubst +mkSubst skolems a b = let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b] -- If we can unify our skolems, at least one is no longer a skolem. -- Removing them from this set ensures we can get a subtitution between -- the two. But it's okay to leave them in 'ts_skolems' in general, since -- they won't exist after running this substitution. - skolems = ts_skolems ts S.\\ tyvars + skolems' = skolems S.\\ tyvars in - case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of - Just subst -> updateSubst subst ts - Nothing -> ts -evidenceToSubst HasInstance{} ts = ts + case tryUnifyUnivarsButNotSkolems skolems' (CType a) (CType b) of + Just subst -> subst + Nothing -> emptyTCvSubst + + +substPair :: TCvSubst -> (Type, Type) -> (Type, Type) +substPair subst (ty, ty') = (substTy subst ty, substTy subst ty') + + +------------------------------------------------------------------------------ +-- | Construct a substitution given a list of types that are equal to one +-- another. This is more subtle than it seems, since there might be several +-- equalities for the same type. We must be careful to push the accumulating +-- substitution through each pair of types before adding their equalities. +allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst +allEvidenceToSubst _ [] = emptyTCvSubst +allEvidenceToSubst skolems ((a, b) : evs) = + let subst = mkSubst skolems a b + in unionTCvSubst subst + $ allEvidenceToSubst skolems + $ fmap (substPair subst) evs + +------------------------------------------------------------------------------ +-- | Update our knowledge of which types are equal. +evidenceToSubst :: [Evidence] -> TacticState -> TacticState +evidenceToSubst evs ts = + updateSubst + (allEvidenceToSubst (ts_skolems ts) + $ mapMaybe (preview $ _Ctor @"EqualityOfTypes") + $ evs) + ts ------------------------------------------------------------------------------ diff --git a/src/Wingman/KnownStrategies.hs b/src/Wingman/KnownStrategies.hs --- a/src/Wingman/KnownStrategies.hs +++ b/src/Wingman/KnownStrategies.hs @@ -1,18 +1,17 @@ module Wingman.KnownStrategies where +import Control.Applicative (empty) import Control.Monad.Error.Class +import Control.Monad.Reader.Class (asks) +import Data.Foldable (for_) import OccName (mkVarOcc) import Refinery.Tactic import Wingman.Context (getCurrentDefinitions, getKnownInstance) +import Wingman.Judgements (jGoal) import Wingman.KnownStrategies.QuickCheck (deriveArbitrary) import Wingman.Machinery (tracing) import Wingman.Tactics import Wingman.Types -import Wingman.Judgements (jGoal) -import Data.Foldable (for_) -import Wingman.FeatureSet -import Control.Applicative (empty) -import Control.Monad.Reader.Class (asks) knownStrategies :: TacticsM () @@ -20,19 +19,9 @@ [ known "fmap" deriveFmap , known "mempty" deriveMempty , known "arbitrary" deriveArbitrary - , featureGuard FeatureKnownMonoid $ known "<>" deriveMappend - , featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend + , known "<>" deriveMappend + , known "mappend" deriveMappend ] - - ------------------------------------------------------------------------------- --- | Guard a tactic behind a feature. -featureGuard :: Feature -> TacticsM a -> TacticsM a -featureGuard feat t = do - fs <- asks ctxFeatureSet - case hasFeature feat fs of - True -> t - False -> empty known :: String -> TacticsM () -> TacticsM () diff --git a/src/Wingman/LanguageServer.hs b/src/Wingman/LanguageServer.hs --- a/src/Wingman/LanguageServer.hs +++ b/src/Wingman/LanguageServer.hs @@ -1,28 +1,33 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE NoMonoLocalBinds #-} + module Wingman.LanguageServer where import ConLike -import Control.Arrow +import Control.Arrow ((***)) import Control.Monad -import Control.Monad.State (State, get, put, evalState) +import Control.Monad.IO.Class +import Control.Monad.RWS +import Control.Monad.State (State, evalState) import Control.Monad.Trans.Maybe +import Data.Bifunctor (first) import Data.Coerce import Data.Functor ((<&>)) -import Data.Generics.Aliases (mkQ) -import Data.Generics.Schemes (everything) +import Data.Functor.Identity (runIdentity) import qualified Data.HashMap.Strict as Map import Data.IORef (readIORef) import qualified Data.Map as M import Data.Maybe -import Data.Monoid import Data.Set (Set) import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable -import Development.IDE (getFilesOfInterest, ShowDiagnostic (ShowDiag), srcSpanToRange) +import Development.IDE (getFilesOfInterestUntracked, ShowDiagnostic (ShowDiag), srcSpanToRange) import Development.IDE (hscEnv) import Development.IDE.Core.RuleTypes import Development.IDE.Core.Rules (usePropertyAction) @@ -30,31 +35,39 @@ import Development.IDE.Core.Shake (IdeState (..), uses, define, use) import qualified Development.IDE.Core.Shake as IDE import Development.IDE.Core.UseStale -import Development.IDE.GHC.Compat +import Development.IDE.GHC.Compat hiding (parseExpr) import Development.IDE.GHC.Error (realSrcSpanToRange) +import Development.IDE.GHC.ExactPrint +import Development.IDE.Graph (Action, RuleResult, Rules, action) +import Development.IDE.Graph.Classes (Binary, Hashable, NFData) import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings) -import Development.Shake (Action, RuleResult, Rules, action) -import Development.Shake.Classes (Typeable, Binary, Hashable, NFData) import qualified FastString import GHC.Generics (Generic) -import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO) +import Generics.SYB hiding (Generic) +import GhcPlugins (extractModule) +import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS) import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Properties import Ide.PluginUtils (usePropertyLsp) import Ide.Types (PluginId) +import Language.Haskell.GHC.ExactPrint (Transform) +import Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty) import Language.LSP.Server (MonadLsp, sendNotification) import Language.LSP.Types +import Language.LSP.Types.Capabilities import OccName import Prelude hiding (span) +import Retrie (transformA) import SrcLoc (containsSpan) -import TcRnTypes (tcg_binds, TcGblEnv) +import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env)) import Wingman.Context -import Wingman.FeatureSet import Wingman.GHC import Wingman.Judgements -import Wingman.Judgements.SYB (everythingContaining) +import Wingman.Judgements.SYB (everythingContaining, metaprogramQ) import Wingman.Judgements.Theta +import Wingman.Metaprogramming.Lexer (ParserContext(..)) import Wingman.Range +import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax) import Wingman.Types @@ -68,8 +81,8 @@ tcCommandName = T.pack . show -runIde :: IdeState -> Action a -> IO a -runIde state = runAction "tactic" state +runIde :: String -> String -> IdeState -> Action a -> IO a +runIde herald action state = runAction ("Wingman." <> herald <> "." <> action) state runCurrentIde @@ -78,11 +91,13 @@ , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a , Show r, Typeable r, NFData r ) - => IdeState + => String + -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (Tracked 'Current r) -runCurrentIde state nfp a = MaybeT $ fmap (fmap unsafeMkCurrent) $ runIde state $ use a nfp +runCurrentIde herald state nfp a = + MaybeT $ fmap (fmap unsafeMkCurrent) $ runIde herald (show a) state $ use a nfp runStaleIde @@ -91,11 +106,13 @@ , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a , Show r, Typeable r, NFData r ) - => IdeState + => String + -> IdeState -> NormalizedFilePath -> a -> MaybeT IO (TrackedStale r) -runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp +runStaleIde herald state nfp a = + MaybeT $ runIde herald (show a) state $ useWithStale a nfp unsafeRunStaleIde @@ -104,12 +121,13 @@ , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a , Show r, Typeable r, NFData r ) - => IdeState + => String + -> IdeState -> NormalizedFilePath -> a -> MaybeT IO r -unsafeRunStaleIde state nfp a = do - (r, _) <- MaybeT $ runIde state $ IDE.useWithStale a nfp +unsafeRunStaleIde herald state nfp a = do + (r, _) <- MaybeT $ runIde herald (show a) state $ IDE.useWithStale a nfp pure r @@ -118,14 +136,14 @@ properties :: Properties '[ 'PropertyKey "hole_severity" ('TEnum (Maybe DiagnosticSeverity)) , 'PropertyKey "max_use_ctor_actions" 'TInteger - , 'PropertyKey "features" 'TString , 'PropertyKey "timeout_duration" 'TInteger + , 'PropertyKey "auto_gas" 'TInteger ] properties = emptyProperties + & defineIntegerProperty #auto_gas + "The depth of the search tree when performing \"Attempt to fill hole\". Bigger values will be able to derive more solutions, but will take exponentially more time." 4 & defineIntegerProperty #timeout_duration "The timeout for Wingman actions, in seconds" 2 - & defineStringProperty #features - "Feature set used by Wingman" "" & defineIntegerProperty #max_use_ctor_actions "Maximum number of `Use constructor ` code actions that can appear" 5 & defineEnumProperty #hole_severity @@ -143,14 +161,9 @@ getTacticConfig :: MonadLsp Plugin.Config m => PluginId -> m Config getTacticConfig pId = Config - <$> (parseFeatureSet <$> usePropertyLsp #features pId properties) - <*> usePropertyLsp #max_use_ctor_actions pId properties + <$> usePropertyLsp #max_use_ctor_actions pId properties <*> usePropertyLsp #timeout_duration pId properties - ------------------------------------------------------------------------------- --- | Get the current feature set from the plugin config. -getFeatureSet :: MonadLsp Plugin.Config m => PluginId -> m FeatureSet -getFeatureSet = fmap cfg_feature_set . getTacticConfig + <*> usePropertyLsp #auto_gas pId properties getIdeDynflags @@ -160,10 +173,15 @@ getIdeDynflags state nfp = do -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. - msr <- unsafeRunStaleIde state nfp GetModSummaryWithoutTimestamps + msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps pure $ ms_hspp_opts $ msrModSummary msr +getAllMetaprograms :: Data a => a -> [String] +getAllMetaprograms = everything (<>) $ mkQ mempty $ \case + WingmanMetaprogram fs -> [ unpackFS fs ] + (_ :: HsExpr GhcTc) -> mempty + ------------------------------------------------------------------------------ -- | Find the last typechecked module, and find the most specific span, as well -- as the judgement at the given range. @@ -171,21 +189,27 @@ :: IdeState -> NormalizedFilePath -> Tracked 'Current Range - -> FeatureSet - -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags) -judgementForHole state nfp range features = do - TrackedStale asts amapping <- runStaleIde state nfp GetHieAst + -> Config + -> MaybeT IO HoleJudgment +judgementForHole state nfp range cfg = do + let stale a = runStaleIde "judgementForHole" state nfp a + + TrackedStale asts amapping <- stale GetHieAst case unTrack asts of HAR _ _ _ _ (HieFromDisk _) -> fail "Need a fresh hie file" HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do range' <- liftMaybe $ mapAgeFrom amapping range - binds <- runStaleIde state nfp GetBindings - tcg <- fmap (fmap tmrTypechecked) - $ runStaleIde state nfp TypeCheck - hscenv <- runStaleIde state nfp GhcSessionDeps + binds <- stale GetBindings + tcg@(TrackedStale tcg_t tcg_map) + <- fmap (fmap tmrTypechecked) + $ stale TypeCheck + hscenv <- stale GhcSessionDeps + (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf + new_rss <- liftMaybe $ mapAgeTo amapping rss + tcg_rss <- liftMaybe $ mapAgeFrom tcg_map new_rss -- KnownThings is just the instances in scope. There are no ranges -- involved, so it's not crucial to track ages. @@ -193,14 +217,25 @@ eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv kt <- knownThings (untrackedStaleValue tcg) henv - (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt + (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt + let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t dflags <- getIdeDynflags state nfp - pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags) + pure $ HoleJudgment + { hj_range = fmap realSrcSpanToRange new_rss + , hj_jdg = jdg + , hj_ctx = ctx + , hj_dflags = dflags + , hj_hole_sort = holeSortFor mp + } +holeSortFor :: Maybe T.Text -> HoleSort +holeSortFor = maybe Hole Metaprogram + + mkJudgementAndContext - :: FeatureSet + :: Config -> Type -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan @@ -208,12 +243,12 @@ -> ExternalPackageState -> KnownThings -> Maybe (Judgement, Context) -mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do +mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do binds_rss <- mapAgeFrom bmap rss tcg_rss <- mapAgeFrom tcgmap rss let tcs = fmap tcg_binds tcg - ctx = mkContext features + ctx = mkContext cfg (mapMaybe (sequenceA . (occName *** coerce)) $ unTrack $ getDefiningBindings <$> binds <*> binds_rss) @@ -227,10 +262,12 @@ $ hypothesisFromBindings binds_rss binds evidence = getEvidenceAtHole (fmap RealSrcSpan tcg_rss) tcs cls_hy = foldMap evidenceToHypothesis evidence - subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState + subst = ts_unifier $ evidenceToSubst evidence defaultTacticState pure $ ( disallowing AlreadyDestructed already_destructed - $ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement + $ fmap (CType . substTyAddInScope subst . unCType) $ + mkFirstJudgement + ctx (local_hy <> cls_hy) (isRhsHole tcg_rss tcs) g @@ -267,8 +304,12 @@ ty <- listToMaybe $ nodeType info guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info -- Ensure we're actually looking at a hole here - guard $ all (either (const False) $ isHole . occName) - $ M.keysSet $ nodeIdentifiers info + occ <- (either (const Nothing) (Just . occName) =<<) + . listToMaybe + . S.toList + . M.keysSet + $ nodeIdentifiers info + guard $ isHole occ pure (unsafeCopyAge r $ nodeSpan ast', ty) @@ -500,7 +541,7 @@ ) action $ do - files <- getFilesOfInterest + files <- getFilesOfInterestUntracked void $ uses WriteDiagnostics $ Map.keys files @@ -513,4 +554,69 @@ "Hole" (Just $ List [DtUnnecessary]) Nothing + + +------------------------------------------------------------------------------ +-- | Transform a 'Graft' over the AST into a 'WorkspaceEdit'. +mkWorkspaceEdits + :: DynFlags + -> ClientCapabilities + -> Uri + -> Annotated ParsedSource + -> Graft (Either String) ParsedSource + -> Either UserFacingMessage WorkspaceEdit +mkWorkspaceEdits dflags ccs uri pm g = do + let pm' = runIdentity $ transformA pm annotateMetaprograms + let response = transform dflags ccs uri g pm' + in first (InfrastructureError . T.pack) response + + +------------------------------------------------------------------------------ +-- | Add ExactPrint annotations to every metaprogram in the source tree. +-- Usually the ExactPrint module can do this for us, but we've enabled +-- QuasiQuotes, so the round-trip print/parse journey will crash. +annotateMetaprograms :: Data a => a -> Transform a +annotateMetaprograms = everywhereM $ mkM $ \case + L ss (WingmanMetaprogram mp) -> do + let x = L ss $ MetaprogramSyntax mp + let anns = addAnnotationsForPretty [] x mempty + modifyAnnsT $ mappend anns + pure x + (x :: LHsExpr GhcPs) -> pure x + + +------------------------------------------------------------------------------ +-- | Find the source of a tactic metaprogram at the given span. +getMetaprogramAtSpan + :: Tracked age SrcSpan + -> Tracked age TcGblEnv + -> Maybe T.Text +getMetaprogramAtSpan (unTrack -> ss) + = fmap snd + . listToMaybe + . metaprogramQ ss + . tcg_binds + . unTrack + + +------------------------------------------------------------------------------ +-- | The metaprogram parser needs the ability to lookup terms from the module +-- and imports. The 'ParserContext' contains everything we need to find that +-- stuff. +getParserState + :: IdeState + -> NormalizedFilePath + -> Context + -> MaybeT IO ParserContext +getParserState state nfp ctx = do + let stale a = runStaleIde "getParserState" state nfp a + + TrackedStale (unTrack -> tcmod) _ <- stale TypeCheck + TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps + + let tcgblenv = tmrTypechecked tcmod + modul = extractModule tcgblenv + rdrenv = tcg_rdr_env tcgblenv + + pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx diff --git a/src/Wingman/LanguageServer/Metaprogram.hs b/src/Wingman/LanguageServer/Metaprogram.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/LanguageServer/Metaprogram.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE OverloadedStrings #-} + +{-# LANGUAGE NoMonoLocalBinds #-} +{-# LANGUAGE RankNTypes #-} + +module Wingman.LanguageServer.Metaprogram + ( hoverProvider + ) where + +import Control.Applicative (empty) +import Control.Monad +import Control.Monad.Reader (runReaderT) +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Data.List (find) +import Data.Maybe +import qualified Data.Text as T +import Data.Traversable +import Development.IDE (positionToRealSrcLoc) +import Development.IDE (realSrcSpanToRange) +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Shake (IdeState (..)) +import Development.IDE.Core.UseStale +import Development.IDE.GHC.Compat +import GhcPlugins (containsSpan, realSrcLocSpan) +import Ide.Types +import Language.LSP.Types +import Prelude hiding (span) +import Prelude hiding (span) +import TcRnTypes (tcg_binds) +import Wingman.GHC +import Wingman.Judgements.SYB (metaprogramQ) +import Wingman.LanguageServer +import Wingman.Metaprogramming.Parser (attempt_it) +import Wingman.Types + + +------------------------------------------------------------------------------ +-- | Provide the "empty case completion" code lens +hoverProvider :: PluginMethodHandler IdeState TextDocumentHover +hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos + + cfg <- getTacticConfig plId + liftIO $ fromMaybeT (Right Nothing) $ do + holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc + + fmap (Right . Just) $ + case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of + Just (trss, program) -> do + let tr_range = fmap realSrcSpanToRange trss + HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg + ps <- getParserState state nfp ctx + z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program + pure $ Hover + { _contents = HoverContents + $ MarkupContent MkMarkdown + $ either T.pack T.pack z + , _range = Just $ unTrack tr_range + } + Nothing -> empty +hoverProvider _ _ _ = pure $ Right Nothing + + +fromMaybeT :: Functor m => a -> MaybeT m a -> m a +fromMaybeT def = fmap (fromMaybe def) . runMaybeT + + +getMetaprogramsAtSpan + :: IdeState + -> NormalizedFilePath + -> SrcSpan + -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)] +getMetaprogramsAtSpan state nfp ss = do + let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a + + TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck + + let scrutinees = traverse (metaprogramQ ss . tcg_binds) tcg + for scrutinees $ \aged@(unTrack -> (ss, program)) -> do + case ss of + RealSrcSpan r -> do + rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r + pure (rss', program) + UnhelpfulSpan _ -> empty + + diff --git a/src/Wingman/LanguageServer/TacticProviders.hs b/src/Wingman/LanguageServer/TacticProviders.hs --- a/src/Wingman/LanguageServer/TacticProviders.hs +++ b/src/Wingman/LanguageServer/TacticProviders.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -7,14 +8,14 @@ , tcCommandId , TacticParams (..) , TacticProviderData (..) + , useNameFromHypothesis ) where import Control.Monad -import Control.Monad.Error.Class (MonadError (throwError)) +import Control.Monad.Reader (runReaderT) import Data.Aeson import Data.Bool (bool) import Data.Coerce -import qualified Data.Map as M import Data.Maybe import Data.Monoid import qualified Data.Text as T @@ -29,27 +30,31 @@ import Language.LSP.Types import OccName import Prelude hiding (span) -import Refinery.Tactic (goal) import Wingman.Auto -import Wingman.FeatureSet import Wingman.GHC import Wingman.Judgements +import Wingman.Machinery (useNameFromHypothesis) +import Wingman.Metaprogramming.Lexer (ParserContext) +import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -commandTactic :: TacticCommand -> OccName -> TacticsM () -commandTactic Auto = const auto -commandTactic Intros = const intros -commandTactic Destruct = useNameFromHypothesis destruct -commandTactic Homomorphism = useNameFromHypothesis homo -commandTactic DestructLambdaCase = const destructLambdaCase -commandTactic HomomorphismLambdaCase = const homoLambdaCase -commandTactic DestructAll = const destructAll -commandTactic UseDataCon = userSplit -commandTactic Refine = const refine +commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ()) +commandTactic _ Auto = pure . const auto +commandTactic _ Intros = pure . const intros +commandTactic _ Destruct = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack +commandTactic _ DestructPun = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack +commandTactic _ Homomorphism = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack +commandTactic _ DestructLambdaCase = pure . const destructLambdaCase +commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase +commandTactic _ DestructAll = pure . const destructAll +commandTactic _ UseDataCon = pure . userSplit . mkVarOcc . T.unpack +commandTactic _ Refine = pure . const refine +commandTactic _ BeginMetaprogram = pure . const metaprogram +commandTactic c RunMetaprogram = flip runReaderT c . parseMetaprogram ------------------------------------------------------------------------------ @@ -58,12 +63,15 @@ tacticKind Auto = "fillHole" tacticKind Intros = "introduceLambda" tacticKind Destruct = "caseSplit" +tacticKind DestructPun = "caseSplitPun" tacticKind Homomorphism = "homomorphicCaseSplit" tacticKind DestructLambdaCase = "lambdaCase" tacticKind HomomorphismLambdaCase = "homomorphicLambdaCase" tacticKind DestructAll = "splitFuncArgs" tacticKind UseDataCon = "useConstructor" tacticKind Refine = "refine" +tacticKind BeginMetaprogram = "beginMetaprogram" +tacticKind RunMetaprogram = "runMetaprogram" ------------------------------------------------------------------------------ @@ -73,12 +81,15 @@ tacticPreferred Auto = True tacticPreferred Intros = True tacticPreferred Destruct = True +tacticPreferred DestructPun = False tacticPreferred Homomorphism = False tacticPreferred DestructLambdaCase = False tacticPreferred HomomorphismLambdaCase = False tacticPreferred DestructAll = True tacticPreferred UseDataCon = True tacticPreferred Refine = True +tacticPreferred BeginMetaprogram = False +tacticPreferred RunMetaprogram = True mkTacticKind :: TacticCommand -> CodeActionKind @@ -90,49 +101,77 @@ -- | Mapping from tactic commands to their contextual providers. See 'provide', -- 'filterGoalType' and 'filterBindingType' for the nitty gritty. commandProvider :: TacticCommand -> TacticProvider -commandProvider Auto = provide Auto "" +commandProvider Auto = + requireHoleSort (== Hole) $ + provide Auto "" commandProvider Intros = + requireHoleSort (== Hole) $ filterGoalType isFunction $ provide Intros "" commandProvider Destruct = + requireHoleSort (== Hole) $ filterBindingType destructFilter $ \occ _ -> provide Destruct $ T.pack $ occNameString occ +commandProvider DestructPun = + requireHoleSort (== Hole) $ + filterBindingType destructPunFilter $ \occ _ -> + provide DestructPun $ T.pack $ occNameString occ commandProvider Homomorphism = + requireHoleSort (== Hole) $ filterBindingType homoFilter $ \occ _ -> provide Homomorphism $ T.pack $ occNameString occ commandProvider DestructLambdaCase = + requireHoleSort (== Hole) $ requireExtension LambdaCase $ filterGoalType (isJust . lambdaCaseable) $ provide DestructLambdaCase "" commandProvider HomomorphismLambdaCase = + requireHoleSort (== Hole) $ requireExtension LambdaCase $ filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = - requireFeature FeatureDestructAll $ + requireHoleSort (== Hole) $ withJudgement $ \jdg -> case _jIsTopHole jdg && jHasBoundArgs jdg of True -> provide DestructAll "" False -> mempty commandProvider UseDataCon = + requireHoleSort (== Hole) $ withConfig $ \cfg -> - requireFeature FeatureUseDataCon $ - filterTypeProjection - ( guardLength (<= cfg_max_use_ctor_actions cfg) - . fromMaybe [] - . fmap fst - . tacticsGetDataCons - ) $ \dcon -> - provide UseDataCon - . T.pack - . occNameString - . occName - $ dataConName dcon + filterTypeProjection + ( guardLength (<= cfg_max_use_ctor_actions cfg) + . fromMaybe [] + . fmap fst + . tacticsGetDataCons + ) $ \dcon -> + provide UseDataCon + . T.pack + . occNameString + . occName + $ dataConName dcon commandProvider Refine = - requireFeature FeatureRefineHole $ + requireHoleSort (== Hole) $ provide Refine "" +commandProvider BeginMetaprogram = + requireGHC88OrHigher $ + requireHoleSort (== Hole) $ + provide BeginMetaprogram "" +commandProvider RunMetaprogram = + requireGHC88OrHigher $ + withMetaprogram $ \mp -> + provide RunMetaprogram mp +requireGHC88OrHigher :: TacticProvider -> TacticProvider +requireGHC88OrHigher tp tpd = +#if __GLASGOW_HASKELL__ >= 808 + tp tpd +#else + mempty +#endif + + ------------------------------------------------------------------------------ -- | Return an empty list if the given predicate doesn't hold over the length guardLength :: (Int -> Bool) -> [a] -> [a] @@ -146,6 +185,7 @@ = TacticProviderData -> IO [Command |? CodeAction] + data TacticProviderData = TacticProviderData { tpd_dflags :: DynFlags , tpd_config :: Config @@ -153,6 +193,7 @@ , tpd_uri :: Uri , tpd_range :: Tracked 'Current Range , tpd_jdg :: Judgement + , tpd_hole_sort :: HoleSort } @@ -165,16 +206,19 @@ deriving anyclass (ToJSON, FromJSON) ------------------------------------------------------------------------------- --- | Restrict a 'TacticProvider', making sure it appears only when the given --- 'Feature' is in the feature set. -requireFeature :: Feature -> TacticProvider -> TacticProvider -requireFeature f tp tpd = - case hasFeature f $ cfg_feature_set $ tpd_config tpd of +requireHoleSort :: (HoleSort -> Bool) -> TacticProvider -> TacticProvider +requireHoleSort p tp tpd = + case p $ tpd_hole_sort tpd of True -> tp tpd False -> pure [] +withMetaprogram :: (T.Text -> TacticProvider) -> TacticProvider +withMetaprogram tp tpd = + case tpd_hole_sort tpd of + Metaprogram mp -> tp mp tpd + _ -> pure [] + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. @@ -238,19 +282,7 @@ withConfig tp tpd = tp (tpd_config tpd) tpd - ------------------------------------------------------------------------------ --- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to --- look it up in the hypothesis. -useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a -useNameFromHypothesis f name = do - hy <- jHypothesis <$> goal - case M.lookup name $ hyByName hy of - Just hi -> f hi - Nothing -> throwError $ NotInScope name - - ------------------------------------------------------------------------------- -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> TacticProvider @@ -293,4 +325,13 @@ destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False + + +------------------------------------------------------------------------------ +-- | We should show destruct punning for bindings only when those bindings have +-- usual algebraic types, and when any of their data constructors are records. +destructPunFilter :: Type -> Type -> Bool +destructPunFilter _ (algebraicTyCon -> Just tc) = + any (not . null . dataConFieldLabels) $ tyConDataCons tc +destructPunFilter _ _ = False diff --git a/src/Wingman/Machinery.hs b/src/Wingman/Machinery.hs --- a/src/Wingman/Machinery.hs +++ b/src/Wingman/Machinery.hs @@ -3,11 +3,12 @@ module Wingman.Machinery where import Class (Class (classTyVars)) +import Control.Applicative (empty) import Control.Lens ((<>~)) import Control.Monad.Error.Class import Control.Monad.Reader import Control.Monad.State.Class (gets, modify) -import Control.Monad.State.Strict (StateT (..)) +import Control.Monad.State.Strict (StateT (..), execStateT) import Data.Bool (bool) import Data.Coerce import Data.Either @@ -22,13 +23,15 @@ import Data.Ord (Down (..), comparing) import Data.Set (Set) import qualified Data.Set as S +import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat -import OccName (HasOccName (occName)) +import GhcPlugins (GlobalRdrElt (gre_name), lookupOccEnv, varType) +import OccName (HasOccName (occName), OccEnv) import Refinery.ProofState import Refinery.Tactic import Refinery.Tactic.Internal import TcType -import Type +import Type (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe) import Unify import Wingman.Judgements import Wingman.Simplify (simplify) @@ -46,12 +49,19 @@ :: Judgement -> Rule newSubgoal j = do - unifier <- gets ts_unifier - subgoal - $ substJdg unifier - $ unsetIsTopHole j + ctx <- ask + unifier <- gets ts_unifier + subgoal + $ normalizeJudgement ctx + $ substJdg unifier + $ unsetIsTopHole + $ normalizeJudgement ctx j +tacticToRule :: Judgement -> TacticsM () -> Rule +tacticToRule jdg (TacticT tt) = RuleT $ flip execStateT jdg tt >>= flip Subgoal Axiom + + ------------------------------------------------------------------------------ -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. @@ -82,11 +92,12 @@ flip sortBy solns $ comparing $ \(ext, (_, holes)) -> Down $ scoreSolution ext jdg holes case sorted of - ((syn, _) : _) -> + ((syn, (_, subgoals)) : _) -> Right $ RunTacticResults - { rtr_trace = syn_trace syn - , rtr_extract = simplify $ syn_val syn + { rtr_trace = syn_trace syn + , rtr_extract = simplify $ syn_val syn + , rtr_subgoals = subgoals , rtr_other_solns = reverse . fmap fst $ sorted , rtr_jdg = jdg , rtr_ctx = ctx @@ -297,4 +308,69 @@ => TacticT jdg ext err s m () -> TacticT jdg ext err s m () try' t = commit t $ pure () + + +------------------------------------------------------------------------------ +-- | Sorry leaves a hole in its extract +exact :: HsExpr GhcPs -> TacticsM () +exact = rule . const . pure . pure . noLoc + +------------------------------------------------------------------------------ +-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to +-- look it up in the hypothesis. +useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a +useNameFromHypothesis f name = do + hy <- jHypothesis <$> goal + case M.lookup name $ hyByName hy of + Just hi -> f hi + Nothing -> throwError $ NotInScope name + +------------------------------------------------------------------------------ +-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to +-- look it up in the hypothesis. +useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a +useNameFromContext f name = do + lookupNameInContext name >>= \case + Just ty -> f $ createImportedHyInfo name ty + Nothing -> throwError $ NotInScope name + + +------------------------------------------------------------------------------ +-- | Find the type of an 'OccName' that is defined in the current module. +lookupNameInContext :: MonadReader Context m => OccName -> m (Maybe CType) +lookupNameInContext name = do + ctx <- asks ctxModuleFuncs + pure $ case find ((== name) . fst) ctx of + Just (_, ty) -> pure ty + Nothing -> empty + + +------------------------------------------------------------------------------ +-- | Build a 'HyInfo' for an imported term. +createImportedHyInfo :: OccName -> CType -> HyInfo CType +createImportedHyInfo on ty = HyInfo + { hi_name = on + , hi_provenance = ImportPrv + , hi_type = ty + } + + +------------------------------------------------------------------------------ +-- | Lookup the type of any 'OccName' that was imported. Necessarily done in +-- IO, so we only expose this functionality to the parser. Internal Haskell +-- code that wants to lookup terms should do it via 'KnownThings'. +getOccNameType + :: HscEnv + -> OccEnv [GlobalRdrElt] + -> Module + -> OccName + -> IO (Maybe Type) +getOccNameType hscenv rdrenv modul occ = + case lookupOccEnv rdrenv occ of + Just (elt : _) -> do + mvar <- lookupName hscenv modul $ gre_name elt + pure $ case mvar of + Just (AnId v) -> pure $ varType v + _ -> Nothing + _ -> pure Nothing diff --git a/src/Wingman/Metaprogramming/Lexer.hs b/src/Wingman/Metaprogramming/Lexer.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/Metaprogramming/Lexer.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +module Wingman.Metaprogramming.Lexer where + +import Control.Applicative +import Control.Monad +import Control.Monad.Reader (ReaderT) +import Data.Text (Text) +import qualified Data.Text as T +import Data.Void +import Development.IDE.GHC.Compat (HscEnv, Module) +import GhcPlugins (GlobalRdrElt) +import Name +import qualified Text.Megaparsec as P +import qualified Text.Megaparsec.Char as P +import qualified Text.Megaparsec.Char.Lexer as L +import Wingman.Types (Context) + + +------------------------------------------------------------------------------ +-- | Everything we need in order to call 'Wingman.Machinery.getOccNameType'. +data ParserContext = ParserContext + { ps_hscEnv :: HscEnv + , ps_occEnv :: OccEnv [GlobalRdrElt] + , ps_module :: Module + , ps_context :: Context + } + +type Parser = P.ParsecT Void Text (ReaderT ParserContext IO) + + + +lineComment :: Parser () +lineComment = L.skipLineComment "--" + +blockComment :: Parser () +blockComment = L.skipBlockComment "{-" "-}" + +sc :: Parser () +sc = L.space P.space1 lineComment blockComment + +ichar :: Parser Char +ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\'' + +lexeme :: Parser a -> Parser a +lexeme = L.lexeme sc + +symbol :: Text -> Parser Text +symbol = L.symbol sc + +symbol_ :: Text -> Parser () +symbol_ = void . symbol + +brackets :: Parser a -> Parser a +brackets = P.between (symbol "[") (symbol "]") + +braces :: Parser a -> Parser a +braces = P.between (symbol "{") (symbol "}") + +parens :: Parser a -> Parser a +parens = P.between (symbol "(") (symbol ")") + +identifier :: Text -> Parser () +identifier i = lexeme (P.string i *> P.notFollowedBy ichar) + +-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list +variable :: Parser OccName +variable = lexeme $ do + c <- P.alphaNumChar + cs <- P.many ichar + pure $ mkVarOcc (c:cs) + +-- FIXME [Reed M. 2020-10-18] Check to see if the variables are in the reserved list +name :: Parser Text +name = lexeme $ do + c <- P.alphaNumChar + cs <- P.many (ichar <|> P.char '-') + pure $ T.pack (c:cs) + +keyword :: Text -> Parser () +keyword = identifier + diff --git a/src/Wingman/Metaprogramming/Parser.hs b/src/Wingman/Metaprogramming/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/Metaprogramming/Parser.hs @@ -0,0 +1,434 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +module Wingman.Metaprogramming.Parser where + +import qualified Control.Monad.Combinators.Expr as P +import qualified Control.Monad.Error.Class as E +import Control.Monad.Reader (ReaderT, ask, MonadIO (liftIO), asks) +import Data.Functor +import Data.Maybe (listToMaybe) +import qualified Data.Text as T +import GhcPlugins (occNameString) +import qualified Refinery.Tactic as R +import qualified Text.Megaparsec as P +import Wingman.Auto +import Wingman.Context (getCurrentDefinitions) +import Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext) +import Wingman.Metaprogramming.Lexer +import Wingman.Metaprogramming.Parser.Documentation +import Wingman.Metaprogramming.ProofState (proofState, layout) +import Wingman.Tactics +import Wingman.Types + + +nullary :: T.Text -> TacticsM () -> Parser (TacticsM ()) +nullary name tac = identifier name $> tac + + +unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ()) +unary_occ name tac = tac <$> (identifier name *> variable) + + +------------------------------------------------------------------------------ +-- | Like 'unary_occ', but runs directly in the 'Parser' monad. +unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ()) +unary_occM name tac = tac =<< (identifier name *> variable) + + +variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ()) +variadic_occ name tac = tac <$> (identifier name *> P.many variable) + + +commands :: [SomeMetaprogramCommand] +commands = + [ command "assumption" Nondeterministic Nullary + "Use any term in the hypothesis that can unify with the current goal." + (pure assumption) + [ Example + Nothing + [] + [EHI "some_a_val" "a"] + (Just "a") + "some_a_val" + ] + + , command "assume" Deterministic (Ref One) + "Use the given term from the hypothesis, unifying it with the current goal" + (pure . assume) + [ Example + Nothing + ["some_a_val"] + [EHI "some_a_val" "a"] + (Just "a") + "some_a_val" + ] + + , command "intros" Deterministic (Bind Many) + ( mconcat + [ "Construct a lambda expression, using the specific names if given, " + , "generating unique names otherwise. When no arguments are given, " + , "all of the function arguments will be bound; otherwise, this " + , "tactic will bind only enough to saturate the given names. Extra " + , "names are ignored." + ]) + (pure . \case + [] -> intros + names -> intros' $ Just names + ) + [ Example + Nothing + [] + [] + (Just "a -> b -> c -> d") + "\\a b c -> (_ :: d)" + , Example + Nothing + ["aye"] + [] + (Just "a -> b -> c -> d") + "\\aye -> (_ :: b -> c -> d)" + , Example + Nothing + ["x", "y", "z", "w"] + [] + (Just "a -> b -> c -> d") + "\\x y z -> (_ :: d)" + ] + + , command "intro" Deterministic (Bind One) + "Construct a lambda expression, binding an argument with the given name." + (pure . intros' . Just . pure) + [ Example + Nothing + ["aye"] + [] + (Just "a -> b -> c -> d") + "\\aye -> (_ :: b -> c -> d)" + ] + + , command "destruct_all" Deterministic Nullary + "Pattern match on every function paramater, in original binding order." + (pure destructAll) + [ Example + (Just "Assume `a` and `b` were bound via `f a b = _`.") + [] + [EHI "a" "Bool", EHI "b" "Maybe Int"] + Nothing $ + T.pack $ init $ unlines + [ "case a of" + , " False -> case b of" + , " Nothing -> _" + , " Just i -> _" + , " True -> case b of" + , " Nothing -> _" + , " Just i -> _" + ] + ] + + , command "destruct" Deterministic (Ref One) + "Pattern match on the argument." + (pure . useNameFromHypothesis destruct) + [ Example + Nothing + ["a"] + [EHI "a" "Bool"] + Nothing $ + T.pack $ init $ unlines + [ "case a of" + , " False -> _" + , " True -> _" + ] + ] + + , command "homo" Deterministic (Ref One) + ( mconcat + [ "Pattern match on the argument, and fill the resulting hole in with " + , "the same data constructor." + ]) + (pure . useNameFromHypothesis homo) + [ Example + (Just $ mconcat + [ "Only applicable when the type constructor of the argument is " + , "the same as that of the hole." + ]) + ["e"] + [EHI "e" "Either a b"] + (Just "Either x y") $ + T.pack $ init $ unlines + [ "case e of" + , " Left a -> Left (_ :: x)" + , " Right b -> Right (_ :: y)" + ] + ] + + , command "application" Nondeterministic Nullary + "Apply any function in the hypothesis that returns the correct type." + (pure application) + [ Example + Nothing + [] + [EHI "f" "a -> b"] + (Just "b") + "f (_ :: a)" + ] + + , command "apply" Deterministic (Ref One) + "Apply the given function from *local* scope." + (pure . useNameFromHypothesis apply) + [ Example + Nothing + ["f"] + [EHI "f" "a -> b"] + (Just "b") + "f (_ :: a)" + ] + + , command "split" Nondeterministic Nullary + "Produce a data constructor for the current goal." + (pure split) + [ Example + Nothing + [] + [] + (Just "Either a b") + "Right (_ :: b)" + ] + + , command "ctor" Deterministic (Ref One) + "Use the given data cosntructor." + (pure . userSplit) + [ Example + Nothing + ["Just"] + [] + (Just "Maybe a") + "Just (_ :: a)" + ] + + , command "obvious" Nondeterministic Nullary + "Produce a nullary data constructor for the current goal." + (pure obvious) + [ Example + Nothing + [] + [] + (Just "[a]") + "[]" + ] + + , command "auto" Nondeterministic Nullary + ( mconcat + [ "Repeatedly attempt to split, destruct, apply functions, and " + , "recurse in an attempt to fill the hole." + ]) + (pure auto) + [ Example + Nothing + [] + [EHI "f" "a -> b", EHI "g" "b -> c"] + (Just "a -> c") + "g . f" + ] + + , command "sorry" Deterministic Nullary + "\"Solve\" the goal by leaving a hole." + (pure sorry) + [ Example + Nothing + [] + [] + (Just "b") + "_ :: b" + ] + + , command "unary" Deterministic Nullary + ( mconcat + [ "Produce a hole for a single-parameter function, as well as a hole for " + , "its argument. The argument holes are completely unconstrained, and " + , "will be solved before the function." + ]) + (pure $ nary 1) + [ Example + (Just $ mconcat + [ "In the example below, the variable `a` is free, and will unify " + , "to the resulting extract from any subsequent tactic." + ]) + [] + [] + (Just "Int") + "(_2 :: a -> Int) (_1 :: a)" + ] + + , command "binary" Deterministic Nullary + ( mconcat + [ "Produce a hole for a two-parameter function, as well as holes for " + , "its arguments. The argument holes have the same type but are " + , "otherwise unconstrained, and will be solved before the function." + ]) + (pure $ nary 2) + [ Example + (Just $ mconcat + [ "In the example below, the variable `a` is free, and will unify " + , "to the resulting extract from any subsequent tactic." + ]) + [] + [] + (Just "Int") + "(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)" + ] + + , command "recursion" Deterministic Nullary + "Fill the current hole with a call to the defining function." + ( pure $ + fmap listToMaybe getCurrentDefinitions >>= \case + Just (self, _) -> useNameFromContext apply self + Nothing -> E.throwError $ TacticPanic "no defining function" + ) + [ Example + (Just "In the context of `foo (a :: Int) (b :: b) = _`:") + [] + [] + Nothing + "foo (_ :: Int) (_ :: b)" + ] + + , command "use" Deterministic (Ref One) + "Apply the given function from *module* scope." + ( \occ -> do + ctx <- asks ps_context + ty <- case lookupNameInContext occ ctx of + Just ty -> pure ty + Nothing -> CType <$> getOccTy occ + pure $ apply $ createImportedHyInfo occ ty + ) + [ Example + (Just "`import Data.Char (isSpace)`") + ["isSpace"] + [] + (Just "Bool") + "isSpace (_ :: Char)" + ] + + , command "cata" Deterministic (Ref One) + "Destruct the given term, recursing on every resulting binding." + (pure . useNameFromHypothesis cata) + [ Example + (Just "Assume we're called in the context of a function `f.`") + ["x"] + [EHI "x" "(a, a)"] + Nothing $ + T.pack $ init $ unlines + [ "case x of" + , " (a1, a2) ->" + , " let a1_c = f a1" + , " a2_c = f a2" + , " in _" + ] + ] + + , command "collapse" Deterministic Nullary + "Collapse every term in scope with the same type as the goal." + (pure collapse) + [ Example + Nothing + [] + [ EHI "a1" "a" + , EHI "a2" "a" + , EHI "a3" "a" + ] + (Just "a") + "(_ :: a -> a -> a -> a) a1 a2 a3" + ] + + ] + + + +oneTactic :: Parser (TacticsM ()) +oneTactic = + P.choice + [ parens tactic + , makeParser commands + ] + + +tactic :: Parser (TacticsM ()) +tactic = flip P.makeExprParser operators oneTactic + +bindOne :: TacticsM a -> TacticsM a -> TacticsM a +bindOne t t1 = t R.<@> [t1] + +operators :: [[P.Operator Parser (TacticsM ())]] +operators = + [ [ P.Prefix (symbol "*" $> R.many_) ] + , [ P.Prefix (symbol "try" $> R.try) ] + , [ P.InfixR (symbol "|" $> (R.<%>) )] + , [ P.InfixL (symbol ";" $> (>>)) + , P.InfixL (symbol "," $> bindOne) + ] + ] + + +tacticProgram :: Parser (TacticsM ()) +tacticProgram = do + sc + r <- tactic P.<|> pure (pure ()) + P.eof + pure r + + +wrapError :: String -> String +wrapError err = "```\n" <> err <> "\n```\n" + + +------------------------------------------------------------------------------ +-- | Attempt to run a metaprogram tactic, returning the proof state, or the +-- errors. +attempt_it + :: Context + -> Judgement + -> String + -> ReaderT ParserContext IO (Either String String) +attempt_it ctx jdg program = + P.runParserT tacticProgram "" (T.pack program) <&> \case + Left peb -> Left $ wrapError $ P.errorBundlePretty peb + Right tt -> do + case runTactic + ctx + jdg + tt + of + Left tes -> Left $ wrapError $ show tes + Right rtr -> Right $ layout $ proofState rtr + + +parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ()) +parseMetaprogram + = fmap (either (const $ pure ()) id) + . P.runParserT tacticProgram "" + + +------------------------------------------------------------------------------ +-- | Like 'getOccNameType', but runs in the 'Parser' monad. +getOccTy :: OccName -> Parser Type +getOccTy occ = do + ParserContext hscenv rdrenv modul _ <- ask + mty <- liftIO $ getOccNameType hscenv rdrenv modul occ + maybe (fail $ occNameString occ <> " is not in scope") pure mty + + +------------------------------------------------------------------------------ +-- | Automatically generate the metaprogram command reference. +writeDocumentation :: IO () +writeDocumentation = + writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $ + unlines + [ "# Wingman Metaprogram Command Reference" + , "" + , prettyReadme commands + ] + diff --git a/src/Wingman/Metaprogramming/Parser/Documentation.hs b/src/Wingman/Metaprogramming/Parser/Documentation.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -0,0 +1,228 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Wingman.Metaprogramming.Parser.Documentation where + +import Data.Functor ((<&>)) +import Data.List (sortOn) +import Data.String (IsString) +import Data.Text (Text) +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.String (renderString) +import GhcPlugins (OccName) +import qualified Text.Megaparsec as P +import Wingman.Metaprogramming.Lexer (Parser, identifier, variable) +import Wingman.Types (TacticsM) + + +------------------------------------------------------------------------------ +-- | Is a tactic deterministic or not? +data Determinism + = Deterministic + | Nondeterministic + +prettyDeterminism :: Determinism -> Doc b +prettyDeterminism Deterministic = "deterministic" +prettyDeterminism Nondeterministic = "non-deterministic" + + +------------------------------------------------------------------------------ +-- | How many arguments does the tactic take? +data Count a where + One :: Count OccName + Many :: Count [OccName] + +prettyCount :: Count a -> Doc b +prettyCount One = "single" +prettyCount Many = "varadic" + + +------------------------------------------------------------------------------ +-- | What sorts of arguments does the tactic take? Currently there is no +-- distincion between 'Ref' and 'Bind', other than documentation. +-- +-- The type index here is used for the shape of the function the parser should +-- take. +data Syntax a where + Nullary :: Syntax (Parser (TacticsM ())) + Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) + Bind :: Count a -> Syntax (a -> Parser (TacticsM ())) + +prettySyntax :: Syntax a -> Doc b +prettySyntax Nullary = "none" +prettySyntax (Ref co) = prettyCount co <+> "reference" +prettySyntax (Bind co) = prettyCount co <+> "binding" + + +------------------------------------------------------------------------------ +-- | An example for the documentation. +data Example = Example + { ex_ctx :: Maybe Text -- ^ Specific context information about when the tactic is applicable + , ex_args :: [Var] -- ^ Arguments the tactic was called with + , ex_hyp :: [ExampleHyInfo] -- ^ The hypothesis + , ex_goal :: Maybe ExampleType -- ^ Current goal. Nothing indicates it's uninteresting. + , ex_result :: Text -- ^ Resulting extract. + } + + +------------------------------------------------------------------------------ +-- | An example 'HyInfo'. +data ExampleHyInfo = EHI + { ehi_name :: Var -- ^ Name of the variable + , ehi_type :: ExampleType -- ^ Type of the variable + } + + +------------------------------------------------------------------------------ +-- | A variable +newtype Var = Var + { getVar :: Text + } + deriving newtype (IsString, Pretty) + + +------------------------------------------------------------------------------ +-- | A type +newtype ExampleType = ExampleType + { getExampleType :: Text + } + deriving newtype (IsString, Pretty) + + +------------------------------------------------------------------------------ +-- | A command to expose to the parser +data MetaprogramCommand a = MC + { mpc_name :: Text -- ^ Name of the command. This is the token necessary to run the command. + , mpc_syntax :: Syntax a -- ^ The command's arguments + , mpc_det :: Determinism -- ^ Determinism of the command + , mpc_description :: Text -- ^ User-facing description + , mpc_tactic :: a -- ^ Tactic to run + , mpc_examples :: [Example] -- ^ Collection of documentation examples + } + +------------------------------------------------------------------------------ +-- | Existentialize the pain away +data SomeMetaprogramCommand where + SMC :: MetaprogramCommand a -> SomeMetaprogramCommand + + +------------------------------------------------------------------------------ +-- | Run the 'Parser' of a 'MetaprogramCommand' +makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ()) +makeMPParser (MC name Nullary _ _ tactic _) = do + identifier name + tactic +makeMPParser (MC name (Ref One) _ _ tactic _) = do + identifier name + variable >>= tactic +makeMPParser (MC name (Ref Many) _ _ tactic _) = do + identifier name + P.many variable >>= tactic +makeMPParser (MC name (Bind One) _ _ tactic _) = do + identifier name + variable >>= tactic +makeMPParser (MC name (Bind Many) _ _ tactic _) = do + identifier name + P.many variable >>= tactic + + +------------------------------------------------------------------------------ +-- | Compile a collection of metaprogram commands into a parser. +makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ()) +makeParser ps = P.choice $ ps <&> \(SMC mp) -> makeMPParser mp + + +------------------------------------------------------------------------------ +-- | Pretty print a command. +prettyCommand :: MetaprogramCommand a -> Doc b +prettyCommand (MC name syn det desc _ exs) = vsep + [ "##" <+> pretty name + , mempty + , "arguments:" <+> prettySyntax syn <> ". " + , prettyDeterminism det <> "." + , mempty + , ">" <+> align (pretty desc) + , mempty + , vsep $ fmap (prettyExample name) exs + ] + + +------------------------------------------------------------------------------ +-- | Pretty print a hypothesis. +prettyHyInfo :: ExampleHyInfo -> Doc a +prettyHyInfo hi = pretty (ehi_name hi) <+> "::" <+> pretty (ehi_type hi) + + +------------------------------------------------------------------------------ +-- | Append the given term only if the first argument has elements. +mappendIfNotNull :: [a] -> a -> [a] +mappendIfNotNull [] _ = [] +mappendIfNotNull as a = as <> [a] + + +------------------------------------------------------------------------------ +-- | Pretty print an example. +prettyExample :: Text -> Example -> Doc a +prettyExample name (Example m_txt args hys goal res) = + align $ vsep + [ mempty + , "### Example" + , maybe mempty ((line <>) . (<> line) . (">" <+>) . align . pretty) m_txt + , "Given:" + , mempty + , codeFence $ vsep + $ mappendIfNotNull (fmap prettyHyInfo hys) mempty + <> [ "_" <+> maybe mempty (("::" <+>). pretty) goal + ] + , mempty + , hsep + [ "running " + , enclose "`" "`" $ pretty name <> hsep (mempty : fmap pretty args) + , "will produce:" + ] + , mempty + , codeFence $ align $ pretty res + ] + + +------------------------------------------------------------------------------ +-- | Make a haskell code fence. +codeFence :: Doc a -> Doc a +codeFence d = align $ vsep + [ "```haskell" + , d + , "```" + ] + + +------------------------------------------------------------------------------ +-- | Render all of the commands. +prettyReadme :: [SomeMetaprogramCommand] -> String +prettyReadme + = renderString + . layoutPretty defaultLayoutOptions + . vsep + . fmap (\case SMC c -> prettyCommand c) + . sortOn (\case SMC c -> mpc_name c) + + + +------------------------------------------------------------------------------ +-- | Helper function to build a 'SomeMetaprogramCommand'. +command + :: Text + -> Determinism + -> Syntax a + -> Text + -> a + -> [Example] + -> SomeMetaprogramCommand +command txt det syn txt' a exs = SMC $ + MC + { mpc_name = txt + , mpc_det = det + , mpc_syntax = syn + , mpc_description = txt' + , mpc_tactic = a + , mpc_examples = exs + } + diff --git a/src/Wingman/Metaprogramming/ProofState.hs b/src/Wingman/Metaprogramming/ProofState.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/Metaprogramming/ProofState.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} + +module Wingman.Metaprogramming.ProofState where + +import Data.Bool (bool) +import Data.Functor ((<&>)) +import qualified Data.Text as T +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.Util.Panic +import Language.LSP.Types (sectionSeparator) +import Wingman.Judgements (jHypothesis) +import Wingman.Types + +renderSimplyDecorated + :: Monoid out + => (T.Text -> out) -- ^ Render plain 'Text' + -> (ann -> out) -- ^ How to render an annotation + -> (ann -> out) -- ^ How to render the removed annotation + -> SimpleDocStream ann + -> out +renderSimplyDecorated text push pop = go [] + where + go _ SFail = panicUncaughtFail + go [] SEmpty = mempty + go (_:_) SEmpty = panicInputNotFullyConsumed + go st (SChar c rest) = text (T.singleton c) <> go st rest + go st (SText _l t rest) = text t <> go st rest + go st (SLine i rest) = + text (T.singleton '\n') <> text (textSpaces i) <> go st rest + go st (SAnnPush ann rest) = push ann <> go (ann : st) rest + go (ann:st) (SAnnPop rest) = pop ann <> go st rest + go [] SAnnPop{} = panicUnpairedPop +{-# INLINE renderSimplyDecorated #-} + + +data Ann + = Goal + | Hypoth + | Status + deriving (Eq, Ord, Show, Enum, Bounded) + +forceMarkdownNewlines :: String -> String +forceMarkdownNewlines = unlines . fmap (<> " ") . lines + +layout :: Doc Ann -> String +layout + = forceMarkdownNewlines + . T.unpack + . renderSimplyDecorated id + renderAnn + renderUnann + . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6) + +renderAnn :: Ann -> T.Text +renderAnn Goal = "" +renderAnn Hypoth = "```haskell\n" +renderAnn Status = "" + +renderUnann :: Ann -> T.Text +renderUnann Goal = "" +renderUnann Hypoth = "\n```\n" +renderUnann Status = "" + +proofState :: RunTacticResults -> Doc Ann +proofState RunTacticResults{rtr_subgoals} = + vsep + $ ( annotate Status + . countFinished "goals accomplished 🎉" "goal" + $ length rtr_subgoals + ) + : pretty sectionSeparator + : fmap prettySubgoal rtr_subgoals + + +prettySubgoal :: Judgement -> Doc Ann +prettySubgoal jdg = + vsep $ + [ mempty | has_hy] <> + [ annotate Hypoth $ prettyHypothesis hy | has_hy] <> + [ "⊢" <+> annotate Goal (prettyType (_jGoal jdg)) + , pretty sectionSeparator + ] + where + hy = jHypothesis jdg + has_hy = not $ null $ unHypothesis hy + + +prettyHypothesis :: Hypothesis CType -> Doc Ann +prettyHypothesis hy = + vsep $ unHypothesis hy <&> \hi -> + prettyHyInfo hi + +prettyHyInfo :: HyInfo CType -> Doc Ann +prettyHyInfo hi = viaShow (hi_name hi) <+> "::" <+> prettyType (hi_type hi) + + +prettyType :: CType -> Doc Ann +prettyType (CType ty) = viaShow ty + + +countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann +countFinished finished _ 0 = finished +countFinished _ thing n = count thing n + +count :: Doc Ann -> Int -> Doc Ann +count thing n = + pretty n <+> thing <> bool "" "s" (n /= 1) + +textSpaces :: Int -> T.Text +textSpaces n = T.replicate n $ T.singleton ' ' + + diff --git a/src/Wingman/Naming.hs b/src/Wingman/Naming.hs --- a/src/Wingman/Naming.hs +++ b/src/Wingman/Naming.hs @@ -1,61 +1,207 @@ module Wingman.Naming where +import Control.Arrow import Control.Monad.State.Strict +import Data.Aeson (camelTo2) import Data.Bool (bool) import Data.Char +import Data.List (isPrefixOf) +import Data.List.Extra (split) import Data.Map (Map) import qualified Data.Map as M +import Data.Maybe (listToMaybe, fromMaybe) +import Data.Monoid import Data.Set (Set) import qualified Data.Set as S import Data.Traversable +import GhcPlugins (charTy, maybeTyCon) import Name import TcType +import Text.Hyphenation (hyphenate, english_US) import TyCon import Type -import TysWiredIn (listTyCon, pairTyCon, unitTyCon) +import TysWiredIn (listTyCon, unitTyCon) +import Wingman.GHC (tcTyVar_maybe) ------------------------------------------------------------------------------ --- | Use type information to create a reasonable name. -mkTyName :: Type -> String --- eg. mkTyName (a -> B) = "fab" -mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) - = "f" ++ mkTyName a ++ mkTyName b --- eg. mkTyName (a -> b -> C) = "f_C" -mkTyName (tcSplitFunTys -> (_:_, b)) - = "f_" ++ mkTyName b --- eg. mkTyName (Either A B) = "eab" -mkTyName (splitTyConApp_maybe -> Just (c, args)) - = mkTyConName c ++ foldMap mkTyName args --- eg. mkTyName (f a) = "fa" -mkTyName (tcSplitAppTys -> (t, args@(_:_))) - = mkTyName t ++ foldMap mkTyName args --- eg. mkTyName a = "a" -mkTyName (getTyVar_maybe -> Just tv) - = occNameString $ occName tv --- eg. mkTyName (forall x. y) = "y" -mkTyName (tcSplitSigmaTy -> (_:_, _, t)) - = mkTyName t -mkTyName _ = "x" +-- | A classification of a variable, for which we have specific naming rules. +-- A variable can have multiple purposes simultaneously. +data Purpose + = Function [Type] Type + | Predicate + | Continuation + | Integral + | Number + | String + | List Type + | Maybe Type + | TyConned TyCon [Type] + -- ^ Something of the form @TC a b c@ + | TyVarred TyVar [Type] + -- ^ Something of the form @m a b c@ +pattern IsPredicate :: Type +pattern IsPredicate <- + (tcSplitFunTys -> ([isFunTy -> False], isBoolTy -> True)) +pattern IsFunction :: [Type] -> Type -> Type +pattern IsFunction args res <- + (tcSplitFunTys -> (args@(_:_), res)) + +pattern IsString :: Type +pattern IsString <- + (splitTyConApp_maybe -> Just ((== listTyCon) -> True, [eqType charTy -> True])) + +pattern IsMaybe :: Type -> Type +pattern IsMaybe a <- + (splitTyConApp_maybe -> Just ((== maybeTyCon) -> True, [a])) + +pattern IsList :: Type -> Type +pattern IsList a <- + (splitTyConApp_maybe -> Just ((== listTyCon) -> True, [a])) + +pattern IsTyConned :: TyCon -> [Type] -> Type +pattern IsTyConned tc args <- + (splitTyConApp_maybe -> Just (id &&& isSymOcc . getOccName -> (tc, False), args)) + +pattern IsTyVarred :: TyVar -> [Type] -> Type +pattern IsTyVarred v args <- + (tcSplitAppTys -> (tcTyVar_maybe -> Just v, args)) + + ------------------------------------------------------------------------------ +-- | Get the 'Purpose's of a type. A type can have multiple purposes +-- simultaneously, so the order of purposes in this function corresponds to the +-- precedence of that naming rule. Which means, eg, that if a type is both +-- a 'Predicate' and a 'Function', we should prefer to use the predicate naming +-- rules, since they come first. +getPurposes :: Type -> [Purpose] +getPurposes ty = mconcat + [ [ Predicate | IsPredicate <- [ty] ] + , [ Function args res | IsFunction args res <- [ty] ] + , with (isIntegerTy ty) [ Integral, Number ] + , with (isIntTy ty) [ Integral, Number ] + , [ Number | isFloatingTy ty ] + , [ String | isStringTy ty ] + , [ Maybe a | IsMaybe a <- [ty] ] + , [ List a | IsList a <- [ty] ] + , [ TyVarred v args | IsTyVarred v args <- [ty] ] + , [ TyConned tc args | IsTyConned tc args <- [ty] + , not (isTupleTyCon tc) + , tc /= listTyCon ] + ] + + +------------------------------------------------------------------------------ +-- | Return 'mempty' if the give bool is false. +with :: Monoid a => Bool -> a -> a +with False _ = mempty +with True a = a + + +------------------------------------------------------------------------------ +-- | Names we can give functions +functionNames :: [String] +functionNames = ["f", "g", "h"] + + +------------------------------------------------------------------------------ +-- | Get a ranked ordering of names for a given purpose. +purposeToName :: Purpose -> [String] +purposeToName (Function args res) + | Just tv_args <- traverse tcTyVar_maybe $ args <> pure res + = fmap (<> foldMap (occNameString . occName) tv_args) functionNames +purposeToName (Function _ _) = functionNames +purposeToName Predicate = pure "p" +purposeToName Continuation = pure "k" +purposeToName Integral = ["n", "i", "j"] +purposeToName Number = ["x", "y", "z", "w"] +purposeToName String = ["s", "str"] +purposeToName (List t) = fmap (<> "s") $ purposeToName =<< getPurposes t +purposeToName (Maybe t) = fmap ("m_" <>) $ purposeToName =<< getPurposes t +purposeToName (TyVarred tv args) + | Just tv_args <- traverse tcTyVar_maybe args + = pure $ foldMap (occNameString . occName) $ tv : tv_args +purposeToName (TyVarred tv _) = pure $ occNameString $ occName tv +purposeToName (TyConned tc args@(_:_)) + | Just tv_args <- traverse tcTyVar_maybe args + = [ mkTyConName tc + -- We insert primes to everything later, but it gets the lowest + -- precedence. Here we'd like to prefer it over the more specific type + -- name. + , mkTyConName tc <> "'" + , mconcat + [ mkTyConName tc + , bool mempty "_" $ length (mkTyConName tc) > 1 + , foldMap (occNameString . occName) tv_args + ] + ] +purposeToName (TyConned tc _) + = pure + $ mkTyConName tc + + +mkTyName :: Type -> [String] +mkTyName = purposeToName <=< getPurposes + + +------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String mkTyConName tc - | tc == listTyCon = "l_" - | tc == pairTyCon = "p_" - | tc == unitTyCon = "unit" - | otherwise + | tc == unitTyCon = "u" + | isSymOcc occ = take 1 . fmap toLower . filterReplace isSymbol 's' . filterReplace isPunctuation 'p' - . occNameString - $ getOccName tc + $ name + | camels@(_:_:_) <- camelTerms name + = foldMap (fmap toLower . take 1) camels + | otherwise + = getStem + $ fmap toLower + $ name + where + occ = getOccName tc + name = occNameString occ ------------------------------------------------------------------------------ +-- | Split a string into its camel case components. +camelTerms :: String -> [String] +camelTerms = split (== '@') . camelTo2 '@' + + +------------------------------------------------------------------------------ +-- | A stem of a string is either a special-case shortened form, or a shortened +-- first syllable. If the string is one syllable, we take the full word if it's +-- short, or just the first two characters if it's long. Otherwise, just take +-- the first syllable. +-- +-- NOTE: There's no rhyme or reason here, I just experimented until I got +-- results that were reasonably consistent with the names I would give things. +getStem :: String -> String +getStem str = + let s = stem str + in case (s == str, length str) of + (False, _) -> s + (True, (<= 3) -> True) -> str + _ -> take 2 str + +------------------------------------------------------------------------------ +-- | Get a special-case stem, or, failing that, give back the first syllable. +stem :: String -> String +stem "char" = "c" +stem "function" = "func" +stem "bool" = "b" +stem "either" = "e" +stem "text" = "txt" +stem s = join $ take 1 $ hyphenate english_US s + + +------------------------------------------------------------------------------ -- | Maybe replace an element in the list if the predicate matches filterReplace :: (a -> Bool) -> a -> [a] -> [a] filterReplace f r = fmap (\a -> bool a r $ f a) @@ -67,22 +213,34 @@ :: Set OccName -- ^ Bindings in scope; used to ensure we don't shadow anything -> Type -- ^ The type to produce a name for -> OccName -mkGoodName in_scope t = - let tn = mkTyName t - in mkVarOcc $ case S.member (mkVarOcc tn) in_scope of - True -> tn ++ show (length in_scope) - False -> tn +mkGoodName in_scope (mkTyName -> tn) + = mkVarOcc + . fromMaybe (mkNumericSuffix in_scope $ fromMaybe "x" $ listToMaybe tn) + . getFirst + . foldMap (\n -> bool (pure n) mempty $ check n) + $ tn <> fmap (<> "'") tn + where + check n = S.member (mkVarOcc n) in_scope ------------------------------------------------------------------------------ +-- | Given a desired name, compute a new name for it based on how many names in +-- scope conflict with it. Eg, if we want to name something @x@, but already +-- have @x@, @x'@ and @x2@ in scope, we will give back @x3@. +mkNumericSuffix :: Set OccName -> String -> String +mkNumericSuffix s nm = + mappend nm . show . length . filter (isPrefixOf nm . occNameString) $ S.toList s + + +------------------------------------------------------------------------------ -- | Like 'mkGoodName' but creates several apart names. mkManyGoodNames - :: (Traversable t, Monad m) + :: (Traversable t) => Set OccName -> t Type - -> m (t OccName) + -> t OccName mkManyGoodNames in_scope args = - flip evalStateT in_scope $ for args $ \at -> do + flip evalState in_scope $ for args $ \at -> do in_scope <- get let n = mkGoodName in_scope at modify $ S.insert n diff --git a/src/Wingman/Plugin.hs b/src/Wingman/Plugin.hs --- a/src/Wingman/Plugin.hs +++ b/src/Wingman/Plugin.hs @@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} -- | A plugin that uses tactics to synthesize code module Wingman.Plugin @@ -12,7 +13,6 @@ import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson -import Data.Bifunctor (first) import Data.Data import Data.Foldable (for_) import Data.Maybe @@ -21,6 +21,7 @@ import Development.IDE.Core.UseStale (Tracked, TrackedStale(..), unTrack, mapAgeFrom, unsafeMkCurrent) import Development.IDE.GHC.Compat import Development.IDE.GHC.ExactPrint +import Generics.SYB.GHC import Ide.Types import Language.LSP.Server import Language.LSP.Types @@ -29,29 +30,44 @@ import Prelude hiding (span) import System.Timeout import Wingman.CaseSplit +import Wingman.EmptyCase import Wingman.GHC import Wingman.LanguageServer +import Wingman.LanguageServer.Metaprogram (hoverProvider) import Wingman.LanguageServer.TacticProviders import Wingman.Machinery (scoreSolution) import Wingman.Range +import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types +import Wingman.Metaprogramming.Lexer (ParserContext) descriptor :: PluginId -> PluginDescriptor IdeState descriptor plId = (defaultPluginDescriptor plId) { pluginCommands - = fmap (\tc -> - PluginCommand - (tcCommandId tc) - (tacticDesc $ tcCommandName tc) - (tacticCmd (commandTactic tc) plId)) - [minBound .. maxBound] - , pluginHandlers = - mkPluginHandler STextDocumentCodeAction codeActionProvider + = mconcat + [ fmap (\tc -> + PluginCommand + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd (flip commandTactic tc) plId)) + [minBound .. maxBound] + , pure $ + PluginCommand + emptyCaseLensCommandId + "Complete the empty case" + workspaceEditHandler + ] + , pluginHandlers = mconcat + [ mkPluginHandler STextDocumentCodeAction codeActionProvider + , mkPluginHandler STextDocumentCodeLens codeLensProvider + , mkPluginHandler STextDocumentHover hoverProvider + ] , pluginRules = wingmanRules plId - , pluginCustomConfig = - mkCustomConfig properties + , pluginConfigDescriptor = + defaultConfigDescriptor {configCustomConfig = mkCustomConfig properties} + , pluginModifyDynflags = staticPlugin } @@ -60,16 +76,17 @@ | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do cfg <- getTacticConfig plId liftIO $ fromMaybeT (Right $ List []) $ do - (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg + HoleJudgment{..} <- judgementForHole state nfp range cfg actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider [minBound .. maxBound] $ TacticProviderData - { tpd_dflags = dflags + { tpd_dflags = hj_dflags , tpd_config = cfg , tpd_plid = plId , tpd_uri = uri , tpd_range = range - , tpd_jdg = jdg + , tpd_jdg = hj_jdg + , tpd_hole_sort = hj_hole_sort } pure $ Right $ List actions codeActionProvider _ _ _ = pure $ Right $ List [] @@ -84,26 +101,34 @@ pure $ Left $ mkErr InternalError $ T.pack $ show ufm -tacticCmd :: (OccName -> TacticsM ()) -> PluginId -> CommandFunction IdeState TacticParams +tacticCmd + :: (ParserContext -> T.Text -> IO (TacticsM ())) + -> PluginId + -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - features <- getFeatureSet pId + let stale a = runStaleIde "tacticCmd" state nfp a + ccs <- getClientCapabilities cfg <- getTacticConfig pId res <- liftIO $ runMaybeT $ do - (range', jdg, ctx, dflags) <- judgementForHole state nfp range features - let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) range' - TrackedStale pm pmmap <- runStaleIde state nfp GetAnnotatedParsedSource + HoleJudgment{..} <- judgementForHole state nfp range cfg + let span = fmap (rangeToRealSrcSpan (fromNormalizedFilePath nfp)) hj_range + TrackedStale pm pmmap <- stale GetAnnotatedParsedSource pm_span <- liftMaybe $ mapAgeFrom pmmap span + pc <- getParserState state nfp hj_ctx + t <- liftIO $ tac pc var_name timingOut (cfg_timeout_seconds cfg * seconds) $ join $ - case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of - Left _ -> Left TacticErrors + case runTactic hj_ctx hj_jdg t of + Left errs -> do + traceMX "errs" errs + Left TacticErrors Right rtr -> case rtr_extract rtr of L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> Left NothingToDo - _ -> pure $ mkWorkspaceEdits pm_span dflags ccs uri pm rtr + _ -> pure $ mkTacticResultEdits pm_span hj_dflags ccs uri pm rtr case res of Nothing -> do @@ -140,7 +165,7 @@ ------------------------------------------------------------------------------ -- | Turn a 'RunTacticResults' into concrete edits to make in the source -- document. -mkWorkspaceEdits +mkTacticResultEdits :: Tracked age RealSrcSpan -> DynFlags -> ClientCapabilities @@ -148,14 +173,12 @@ -> Tracked age (Annotated ParsedSource) -> RunTacticResults -> Either UserFacingMessage WorkspaceEdit -mkWorkspaceEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do +mkTacticResultEdits (unTrack -> span) dflags ccs uri (unTrack -> pm) rtr = do for_ (rtr_other_solns rtr) $ \soln -> do traceMX "other solution" $ syn_val soln traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) [] traceMX "solution" $ rtr_extract rtr - let g = graftHole (RealSrcSpan span) rtr - response = transform dflags ccs uri g pm - in first (InfrastructureError . T.pack) response + mkWorkspaceEdits dflags ccs uri pm $ graftHole (RealSrcSpan span) rtr ------------------------------------------------------------------------------ @@ -209,8 +232,4 @@ pure alts _ -> lift $ Left "annotateDecl didn't produce a funbind" graftDecl _ _ _ _ x = pure $ pure x - - -fromMaybeT :: Functor m => a -> MaybeT m a -> m a -fromMaybeT def = fmap (fromMaybe def) . runMaybeT diff --git a/src/Wingman/Simplify.hs b/src/Wingman/Simplify.hs --- a/src/Wingman/Simplify.hs +++ b/src/Wingman/Simplify.hs @@ -11,7 +11,7 @@ import GHC.SourceGen (var) import GHC.SourceGen.Expr (lambda) import Wingman.CodeGen.Utils -import Wingman.GHC (containsHsVar, fromPatCompat) +import Wingman.GHC (containsHsVar, fromPatCompat, pattern SingleLet) ------------------------------------------------------------------------------ @@ -30,6 +30,7 @@ Lambda pats body = lambda pats body + ------------------------------------------------------------------------------ -- | Simlify an expression. simplify :: LHsExpr GhcPs -> LHsExpr GhcPs @@ -41,6 +42,7 @@ [ simplifyEtaReduce , simplifyRemoveParens , simplifyCompose + , simplifySingleLet ]) @@ -66,6 +68,13 @@ -- We can only perform this simplifiation if @pat@ is otherwise unused. , not (containsHsVar pat f) -> Lambda pats f + x -> x + +------------------------------------------------------------------------------ +-- | Eliminates the unnecessary binding in @let a = b in a@ +simplifySingleLet :: GenericT +simplifySingleLet = mkT $ \case + SingleLet bind [] val (HsVar _ (L _ a)) | a == bind -> val x -> x diff --git a/src/Wingman/StaticPlugin.hs b/src/Wingman/StaticPlugin.hs new file mode 100644 --- /dev/null +++ b/src/Wingman/StaticPlugin.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE CPP #-} + +module Wingman.StaticPlugin + ( staticPlugin + , metaprogramHoleName + , pattern WingmanMetaprogram + , pattern MetaprogramSyntax + ) where + +import Data.Data +import Development.IDE.GHC.Compat +import GHC.LanguageExtensions.Type (Extension(EmptyCase, QuasiQuotes)) +import Generics.SYB +import GhcPlugins hiding ((<>)) +import Ide.Types + + +staticPlugin :: DynFlagsModifications +staticPlugin = mempty + { dynFlagsModifyGlobal = + \df -> allowEmptyCaseButWithWarning + $ df +#if __GLASGOW_HASKELL__ >= 808 + { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] } + , dynFlagsModifyParser = enableQuasiQuotes +#endif + } + + +pattern MetaprogramSourceText :: SourceText +pattern MetaprogramSourceText = SourceText "wingman-meta-program" + + + +pattern WingmanMetaprogram :: FastString -> HsExpr p +pattern WingmanMetaprogram mp + <- HsSCC _ MetaprogramSourceText (StringLiteral NoSourceText mp) + (L _ ( HsVar _ _)) + + +enableQuasiQuotes :: DynFlags -> DynFlags +enableQuasiQuotes = flip xopt_set QuasiQuotes + + +-- | Wingman wants to support destructing of empty cases, but these are a parse +-- error by default. So we want to enable 'EmptyCase', but then that leads to +-- silent errors without 'Opt_WarnIncompletePatterns'. +allowEmptyCaseButWithWarning :: DynFlags -> DynFlags +allowEmptyCaseButWithWarning = + flip xopt_set EmptyCase . flip wopt_set Opt_WarnIncompletePatterns + + +#if __GLASGOW_HASKELL__ >= 808 +metaprogrammingPlugin :: StaticPlugin +metaprogrammingPlugin = + StaticPlugin $ PluginWithArgs (defaultPlugin { parsedResultAction = worker }) [] + where + worker :: [CommandLineOption] -> ModSummary -> HsParsedModule -> Hsc HsParsedModule + worker _ _ pm = pure $ pm { hpm_module = addMetaprogrammingSyntax $ hpm_module pm } +#endif + +metaprogramHoleName :: OccName +metaprogramHoleName = mkVarOcc "_$metaprogram" + + +mkMetaprogram :: SrcSpan -> FastString -> HsExpr GhcPs +mkMetaprogram ss mp = + HsSCC noExtField MetaprogramSourceText (StringLiteral NoSourceText mp) + $ L ss + $ HsVar noExtField + $ L ss + $ mkRdrUnqual + $ metaprogramHoleName + + +addMetaprogrammingSyntax :: Data a => a -> a +addMetaprogrammingSyntax = + everywhere $ mkT $ \case + L ss (MetaprogramSyntax mp) -> + L ss $ mkMetaprogram ss mp + (x :: LHsExpr GhcPs) -> x + + +pattern MetaprogramSyntax :: FastString -> HsExpr GhcPs +pattern MetaprogramSyntax mp <- + HsSpliceE _ (HsQuasiQuote _ _ (occNameString . rdrNameOcc -> "wingman") _ mp) + where + MetaprogramSyntax mp = + HsSpliceE noExtField $ + HsQuasiQuote + noExtField + (mkRdrUnqual $ mkVarOcc "splice") + (mkRdrUnqual $ mkVarOcc "wingman") + noSrcSpan + mp + diff --git a/src/Wingman/Tactics.hs b/src/Wingman/Tactics.hs --- a/src/Wingman/Tactics.hs +++ b/src/Wingman/Tactics.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE OverloadedStrings #-} + module Wingman.Tactics ( module Wingman.Tactics , runTactic @@ -9,7 +11,8 @@ import Control.Monad (unless) import Control.Monad.Except (throwError) import Control.Monad.Reader.Class (MonadReader (ask)) -import Control.Monad.State.Strict (StateT(..), runStateT) +import Control.Monad.State.Strict (StateT(..), runStateT, gets) +import Data.Bool (bool) import Data.Foldable import Data.Functor ((<&>)) import Data.Generics.Labels () @@ -21,18 +24,22 @@ import DataCon import Development.IDE.GHC.Compat import GHC.Exts +import GHC.SourceGen ((@@)) import GHC.SourceGen.Expr import Name (occNameString, occName) +import OccName (mkVarOcc) import Refinery.Tactic import Refinery.Tactic.Internal import TcType import Type hiding (Var) +import TysPrim (betaTy, alphaTy, betaTyVar, alphaTyVar) import Wingman.CodeGen import Wingman.Context import Wingman.GHC import Wingman.Judgements import Wingman.Machinery import Wingman.Naming +import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types @@ -76,7 +83,8 @@ unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty let hy' = recursiveHypothesis defs - localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy') + ctx <- ask + localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy') <@> fmap (localTactic assumption . filterPosition name) [0..] @@ -93,17 +101,26 @@ ------------------------------------------------------------------------------ -- | Introduce a lambda binding every variable. intros :: TacticsM () -intros = rule $ \jdg -> do +intros = intros' Nothing + +------------------------------------------------------------------------------ +-- | Introduce a lambda binding every variable. +intros' + :: Maybe [OccName] -- ^ When 'Nothing', generate a new name for every + -- variable. Otherwise, only bind the variables named. + -> TacticsM () +intros' names = rule $ \jdg -> do let g = jGoal jdg - ctx <- ask - case tcSplitFunTys $ unCType g of - ([], _) -> throwError $ GoalMismatch "intros" g - (as, b) -> do - vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as - let top_hole = isTopHole ctx jdg + case tacticsSplitFunTy $ unCType g of + (_, _, [], _) -> throwError $ GoalMismatch "intros" g + (_, _, as, b) -> do + ctx <- ask + let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names + num_args = length vs + top_hole = isTopHole ctx jdg hy' = lambdaHypothesis top_hole $ zip vs $ coerce as - jdg' = introduce hy' - $ withNewGoal (CType b) jdg + jdg' = introduce ctx hy' + $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg ext <- newSubgoal jdg' pure $ ext @@ -142,9 +159,9 @@ ty = unCType $ hi_type hi attemptWhen - (rule $ destruct' (\dc jdg -> + (rule $ destruct' False (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys g) hi) - (rule $ destruct' (const subgoal) hi) + (rule $ destruct' False (const newSubgoal) hi) $ case (splitTyConApp_maybe g, splitTyConApp_maybe ty) of (Just (gtc, _), Just (tytc, _)) -> gtc == tytc _ -> False @@ -154,20 +171,28 @@ -- | Case split, and leave holes in the matches. destruct :: HyInfo CType -> TacticsM () destruct hi = requireConcreteHole $ tracing "destruct(user)" $ - rule $ destruct' (const subgoal) hi + rule $ destruct' False (const newSubgoal) hi ------------------------------------------------------------------------------ +-- | Case split, and leave holes in the matches. Performs record punning. +destructPun :: HyInfo CType -> TacticsM () +destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $ + rule $ destruct' True (const newSubgoal) hi + + +------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: HyInfo CType -> TacticsM () -homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg -> +homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) ------------------------------------------------------------------------------ -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM () -destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal) +destructLambdaCase = + tracing "destructLambdaCase" $ rule $ destructLambdaCase' False (const newSubgoal) ------------------------------------------------------------------------------ @@ -175,7 +200,7 @@ homoLambdaCase :: TacticsM () homoLambdaCase = tracing "homoLambdaCase" $ - rule $ destructLambdaCase' $ \dc jdg -> + rule $ destructLambdaCase' False $ \dc jdg -> buildDataCon False jdg dc . snd . splitAppTys @@ -184,7 +209,7 @@ apply :: HyInfo CType -> TacticsM () -apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do +apply hi = tracing ("apply' " <> show (hi_name hi)) $ do jdg <- goal let g = jGoal jdg ty = unCType $ hi_type hi @@ -205,7 +230,10 @@ & #syn_used_vals %~ S.insert func & #syn_val %~ mkApply func . fmap unLoc +application :: TacticsM () +application = overFunctions apply + ------------------------------------------------------------------------------ -- | Choose between each of the goal's data constructors. split :: TacticsM () @@ -247,8 +275,26 @@ splitDataCon dc _ -> throwError $ GoalMismatch "splitSingle" g +------------------------------------------------------------------------------ +-- | Like 'split', but prunes any data constructors which have holes. +obvious :: TacticsM () +obvious = tracing "obvious" $ do + pruning split $ bool (Just NoProgress) Nothing . null + ------------------------------------------------------------------------------ +-- | Sorry leaves a hole in its extract +sorry :: TacticsM () +sorry = exact $ var' $ mkVarOcc "_" + + +------------------------------------------------------------------------------ +-- | Sorry leaves a hole in its extract +metaprogram :: TacticsM () +metaprogram = exact $ MetaprogramSyntax "" + + +------------------------------------------------------------------------------ -- | Allow the given tactic to proceed if and only if it introduces holes that -- have a different goal than current goal. requireNewHoles :: TacticsM () -> TacticsM () @@ -290,7 +336,7 @@ destructAll = do jdg <- goal let args = fmap fst - $ sortOn (Down . snd) + $ sortOn snd $ mapMaybe (\(hi, prov) -> case prov of TopLevelArgPrv _ idx _ -> pure (hi, idx) @@ -300,7 +346,9 @@ $ filter (isAlgType . unCType . hi_type) $ unHypothesis $ jHypothesis jdg - for_ args destruct + for_ args $ \arg -> do + subst <- gets ts_unifier + destruct $ fmap (coerce substTy subst) arg -------------------------------------------------------------------------------- -- | User-facing tactic to implement "Use constructor " @@ -338,10 +386,7 @@ refine :: TacticsM () -refine = do - try' intros - try' splitSingle - try' intros +refine = intros <%> splitSingle auto' :: Int -> TacticsM () @@ -351,7 +396,7 @@ try intros choice [ overFunctions $ \fname -> do - apply fname + requireConcreteHole $ apply fname loop , overAlgebraicTerms $ \aname -> do destructAuto aname @@ -394,4 +439,75 @@ True -> apply hi False -> empty + +------------------------------------------------------------------------------ +-- | Make a function application where the function being applied itself is +-- a hole. +applyByType :: Type -> TacticsM () +applyByType ty = tracing ("applyByType " <> show ty) $ do + jdg <- goal + let g = jGoal jdg + ty' <- freshTyvars ty + let (_, _, args, ret) = tacticsSplitFunTy ty' + rule $ \jdg -> do + unify g (CType ret) + ext + <- fmap unzipTrace + $ traverse ( newSubgoal + . blacklistingDestruct + . flip withNewGoal jdg + . CType + ) args + app <- newSubgoal . blacklistingDestruct $ withNewGoal (CType ty) jdg + pure $ + fmap noLoc $ + foldl' (@@) + <$> fmap unLoc app + <*> fmap (fmap unLoc) ext + + +------------------------------------------------------------------------------ +-- | Make an n-ary function call of the form +-- @(_ :: forall a b. a -> a -> b) _ _@. +nary :: Int -> TacticsM () +nary n = + applyByType $ + mkInvForAllTys [alphaTyVar, betaTyVar] $ + mkFunTys' (replicate n alphaTy) betaTy + +self :: TacticsM () +self = + fmap listToMaybe getCurrentDefinitions >>= \case + Just (self, _) -> useNameFromContext apply self + Nothing -> throwError $ TacticPanic "no defining function" + + +cata :: HyInfo CType -> TacticsM () +cata hi = do + diff <- hyDiff $ destruct hi + rule $ + letForEach + (mkVarOcc . flip mappend "_c" . occNameString) + (\hi -> self >> commit (apply hi) assumption) + diff + +collapse :: TacticsM () +collapse = do + g <- goal + let terms = unHypothesis $ hyFilter ((jGoal g ==) . hi_type) $ jLocalHypothesis g + case terms of + [hi] -> assume $ hi_name hi + _ -> nary (length terms) <@> fmap (assume . hi_name) terms + + +------------------------------------------------------------------------------ +-- | Determine the difference in hypothesis due to running a tactic. Also, it +-- runs the tactic. +hyDiff :: TacticsM () -> TacticsM (Hypothesis CType) +hyDiff m = do + g <- unHypothesis . jEntireHypothesis <$> goal + let g_len = length g + m + g' <- unHypothesis . jEntireHypothesis <$> goal + pure $ Hypothesis $ take (length g' - g_len) g' diff --git a/src/Wingman/Types.hs b/src/Wingman/Types.hs --- a/src/Wingman/Types.hs +++ b/src/Wingman/Types.hs @@ -26,8 +26,11 @@ import Data.Text (Text) import qualified Data.Text as T import Data.Tree +import Development.IDE (Range) +import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat hiding (Node) import Development.IDE.GHC.Orphans () +import FamInstEnv (FamInstEnvs) import GHC.Generics import GHC.SourceGen (var) import InstEnv (InstEnvs(..)) @@ -38,7 +41,6 @@ import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) import Wingman.Debug -import Wingman.FeatureSet ------------------------------------------------------------------------------ @@ -49,12 +51,15 @@ = Auto | Intros | Destruct + | DestructPun | Homomorphism | DestructLambdaCase | HomomorphismLambdaCase | DestructAll | UseDataCon | Refine + | BeginMetaprogram + | RunMetaprogram deriving (Eq, Ord, Show, Enum, Bounded) -- | Generate a title for the command. @@ -64,22 +69,33 @@ go Auto _ = "Attempt to fill hole" go Intros _ = "Introduce lambda" go Destruct var = "Case split on " <> var + go DestructPun var = "Split on " <> var <> " with NamedFieldPuns" go Homomorphism var = "Homomorphic case split on " <> var go DestructLambdaCase _ = "Lambda case split" go HomomorphismLambdaCase _ = "Homomorphic lambda case split" go DestructAll _ = "Split all function arguments" go UseDataCon dcon = "Use constructor " <> dcon go Refine _ = "Refine hole" + go BeginMetaprogram _ = "Use custom tactic block" + go RunMetaprogram _ = "Run custom tactic" ------------------------------------------------------------------------------ -- | Plugin configuration for tactics data Config = Config - { cfg_feature_set :: FeatureSet - , cfg_max_use_ctor_actions :: Int + { cfg_max_use_ctor_actions :: Int , cfg_timeout_seconds :: Int + , cfg_auto_gas :: Int } + deriving (Eq, Ord, Show) +emptyConfig :: Config +emptyConfig = Config + { cfg_max_use_ctor_actions = 5 + , cfg_timeout_seconds = 2 + , cfg_auto_gas = 4 + } + ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type } @@ -117,6 +133,9 @@ instance Show (HsExpr GhcPs) where show = unsafeRender +instance Show (HsExpr GhcTc) where + show = unsafeRender + instance Show (HsDecl GhcPs) where show = unsafeRender @@ -191,6 +210,8 @@ (Uniquely Class) -- ^ Class -- | A binding explicitly written by the user. | UserPrv + -- | A binding explicitly imported by the user. + | ImportPrv -- | The recursive hypothesis. Present only in the context of the recursion -- tactic. | RecursivePrv @@ -305,6 +326,7 @@ | UnhelpfulSplit OccName | TooPolymorphic | NotInScope OccName + | TacticPanic String deriving stock (Eq) instance Show TacticError where @@ -343,6 +365,8 @@ "The tactic isn't applicable because the goal is too polymorphic" show (NotInScope name) = "Tried to do something with the out of scope name " <> show name + show (TacticPanic err) = + "PANIC: " <> err ------------------------------------------------------------------------------ @@ -393,9 +417,10 @@ -- ^ The functions currently being defined , ctxModuleFuncs :: [(OccName, CType)] -- ^ Everything defined in the current module - , ctxFeatureSet :: FeatureSet + , ctxConfig :: Config , ctxKnownThings :: KnownThings , ctxInstEnvs :: InstEnvs + , ctxFamInstEnvs :: FamInstEnvs , ctxTheta :: Set CType } @@ -404,7 +429,7 @@ [ "Context " , showsPrec 10 ctxDefiningFuncs "" , showsPrec 10 ctxModuleFuncs "" - , showsPrec 10 ctxFeatureSet "" + , showsPrec 10 ctxConfig "" , showsPrec 10 ctxTheta "" ] @@ -424,8 +449,9 @@ = Context { ctxDefiningFuncs = mempty , ctxModuleFuncs = mempty - , ctxFeatureSet = mempty + , ctxConfig = emptyConfig , ctxKnownThings = error "empty known things from emptyContext" + , ctxFamInstEnvs = mempty , ctxInstEnvs = InstEnvs mempty mempty mempty , ctxTheta = mempty } @@ -461,6 +487,7 @@ data RunTacticResults = RunTacticResults { rtr_trace :: Trace , rtr_extract :: LHsExpr GhcPs + , rtr_subgoals :: [Judgement] , rtr_other_solns :: [Synthesized (LHsExpr GhcPs)] , rtr_jdg :: Judgement , rtr_ctx :: Context @@ -486,4 +513,16 @@ show TimedOut = "Wingman timed out while trying to find a solution" show NothingToDo = "Nothing to do" show (InfrastructureError t) = "Internal error: " <> T.unpack t + + +data HoleSort = Hole | Metaprogram T.Text + deriving (Eq, Ord, Show) + +data HoleJudgment = HoleJudgment + { hj_range :: Tracked 'Current Range + , hj_jdg :: Judgement + , hj_ctx :: Context + , hj_dflags :: DynFlags + , hj_hole_sort :: HoleSort + } diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs --- a/test/AutoTupleSpec.hs +++ b/test/AutoTupleSpec.hs @@ -36,6 +36,7 @@ runTactic emptyContext (mkFirstJudgement + emptyContext (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type) True out_type) diff --git a/test/CodeAction/AutoSpec.hs b/test/CodeAction/AutoSpec.hs --- a/test/CodeAction/AutoSpec.hs +++ b/test/CodeAction/AutoSpec.hs @@ -1,16 +1,10 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.AutoSpec where import Wingman.Types import Test.Hspec import Utils -import Wingman.FeatureSet (allFeatures) spec :: Spec @@ -19,72 +13,75 @@ autoTestNoWhitespace = goldenTestNoWhitespace Auto "" describe "golden" $ do - autoTest 11 8 "AutoSplitGADT.hs" - autoTest 2 11 "GoldenEitherAuto.hs" - autoTest 4 12 "GoldenJoinCont.hs" - autoTest 3 11 "GoldenIdentityFunctor.hs" - autoTest 7 11 "GoldenIdTypeFam.hs" - autoTest 2 15 "GoldenEitherHomomorphic.hs" - autoTest 2 8 "GoldenNote.hs" - autoTest 2 12 "GoldenPureList.hs" - autoTest 2 12 "GoldenListFmap.hs" - autoTest 2 13 "GoldenFromMaybe.hs" - autoTest 2 10 "GoldenFoldr.hs" - autoTest 2 8 "GoldenSwap.hs" - autoTest 4 11 "GoldenFmapTree.hs" - autoTest 7 13 "GoldenGADTAuto.hs" - autoTest 2 12 "GoldenSwapMany.hs" - autoTest 4 12 "GoldenBigTuple.hs" - autoTest 2 10 "GoldenShow.hs" - autoTest 2 15 "GoldenShowCompose.hs" - autoTest 2 8 "GoldenShowMapChar.hs" - autoTest 7 8 "GoldenSuperclass.hs" - autoTest 2 12 "GoldenSafeHead.hs" - autoTest 2 12 "FmapBoth.hs" - autoTest 7 8 "RecordCon.hs" - autoTest 6 8 "NewtypeRecord.hs" - autoTest 2 14 "FmapJoin.hs" - autoTest 2 9 "Fgmap.hs" - autoTest 4 19 "FmapJoinInLet.hs" - autoTest 9 12 "AutoEndo.hs" - autoTest 2 16 "AutoEmptyString.hs" - autoTest 7 35 "AutoPatSynUse.hs" - autoTest 2 28 "AutoZip.hs" - autoTest 2 17 "AutoInfixApply.hs" - autoTest 2 19 "AutoInfixApplyMany.hs" - autoTest 2 25 "AutoInfixInfix.hs" + autoTest 11 8 "AutoSplitGADT" + autoTest 2 11 "GoldenEitherAuto" + autoTest 4 12 "GoldenJoinCont" + autoTest 3 11 "GoldenIdentityFunctor" + autoTest 7 11 "GoldenIdTypeFam" + autoTest 2 15 "GoldenEitherHomomorphic" + autoTest 2 8 "GoldenNote" + autoTest 2 12 "GoldenPureList" + autoTest 2 12 "GoldenListFmap" + autoTest 2 13 "GoldenFromMaybe" + autoTest 2 10 "GoldenFoldr" + autoTest 2 8 "GoldenSwap" + autoTest 4 11 "GoldenFmapTree" + autoTest 7 13 "GoldenGADTAuto" + autoTest 2 12 "GoldenSwapMany" + autoTest 4 12 "GoldenBigTuple" + autoTest 2 10 "GoldenShow" + autoTest 2 15 "GoldenShowCompose" + autoTest 2 8 "GoldenShowMapChar" + autoTest 7 8 "GoldenSuperclass" + autoTest 2 12 "GoldenSafeHead" + autoTest 2 12 "FmapBoth" + autoTest 7 8 "RecordCon" + autoTest 6 8 "NewtypeRecord" + autoTest 2 14 "FmapJoin" + autoTest 2 9 "Fgmap" + autoTest 4 19 "FmapJoinInLet" + autoTest 9 12 "AutoEndo" + autoTest 2 16 "AutoEmptyString" + autoTest 7 35 "AutoPatSynUse" + autoTest 2 28 "AutoZip" + autoTest 2 17 "AutoInfixApply" + autoTest 2 19 "AutoInfixApplyMany" + autoTest 2 25 "AutoInfixInfix" failing "flaky in CI" $ - autoTest 2 11 "GoldenApplicativeThen.hs" + autoTest 2 11 "GoldenApplicativeThen" failing "not enough auto gas" $ - autoTest 5 18 "GoldenFish.hs" + autoTest 5 18 "GoldenFish" describe "theta" $ do - autoTest 12 10 "AutoThetaFix.hs" - autoTest 7 20 "AutoThetaRankN.hs" - autoTest 6 10 "AutoThetaGADT.hs" - autoTest 6 8 "AutoThetaGADTDestruct.hs" - autoTest 4 8 "AutoThetaEqCtx.hs" - autoTest 6 10 "AutoThetaEqGADT.hs" - autoTest 6 8 "AutoThetaEqGADTDestruct.hs" - autoTest 6 10 "AutoThetaRefl.hs" - autoTest 6 8 "AutoThetaReflDestruct.hs" + autoTest 12 10 "AutoThetaFix" + autoTest 7 20 "AutoThetaRankN" + autoTest 6 10 "AutoThetaGADT" + autoTest 6 8 "AutoThetaGADTDestruct" + autoTest 4 8 "AutoThetaEqCtx" + autoTest 6 10 "AutoThetaEqGADT" + autoTest 6 8 "AutoThetaEqGADTDestruct" + autoTest 6 10 "AutoThetaRefl" + autoTest 6 8 "AutoThetaReflDestruct" + autoTest 19 30 "AutoThetaMultipleUnification" + autoTest 16 9 "AutoThetaSplitUnification" describe "known" $ do - autoTest 25 13 "GoldenArbitrary.hs" + autoTest 25 13 "GoldenArbitrary" autoTestNoWhitespace - 6 10 "KnownBigSemigroup.hs" - autoTest 4 10 "KnownThetaSemigroup.hs" - autoTest 6 10 "KnownCounterfactualSemigroup.hs" - autoTest 10 10 "KnownModuleInstanceSemigroup.hs" - autoTest 4 22 "KnownDestructedSemigroup.hs" - autoTest 4 10 "KnownMissingSemigroup.hs" - autoTest 7 12 "KnownMonoid.hs" - autoTest 7 12 "KnownPolyMonoid.hs" - autoTest 7 12 "KnownMissingMonoid.hs" + 6 10 "KnownBigSemigroup" + autoTest 4 10 "KnownThetaSemigroup" + autoTest 6 10 "KnownCounterfactualSemigroup" + autoTest 10 10 "KnownModuleInstanceSemigroup" + autoTest 4 22 "KnownDestructedSemigroup" + autoTest 4 10 "KnownMissingSemigroup" + autoTest 7 12 "KnownMonoid" + autoTest 7 12 "KnownPolyMonoid" + autoTest 7 12 "KnownMissingMonoid" describe "messages" $ do - mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA.hs" TacticErrors + mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors + mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors diff --git a/test/CodeAction/DestructAllSpec.hs b/test/CodeAction/DestructAllSpec.hs --- a/test/CodeAction/DestructAllSpec.hs +++ b/test/CodeAction/DestructAllSpec.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.DestructAllSpec where @@ -18,25 +13,26 @@ describe "provider" $ do mkTest "Requires args on lhs of =" - "DestructAllProvider.hs" 3 21 + "DestructAllProvider" 3 21 [ (not, DestructAll, "") ] mkTest "Can't be a non-top-hole" - "DestructAllProvider.hs" 8 19 + "DestructAllProvider" 8 19 [ (not, DestructAll, "") , (id, Destruct, "a") , (id, Destruct, "b") ] mkTest "Provides a destruct all otherwise" - "DestructAllProvider.hs" 12 22 + "DestructAllProvider" 12 22 [ (id, DestructAll, "") ] describe "golden" $ do - destructAllTest 2 11 "DestructAllAnd.hs" - destructAllTest 4 23 "DestructAllMany.hs" - destructAllTest 2 18 "DestructAllNonVarTopMatch.hs" - destructAllTest 2 18 "DestructAllFunc.hs" + destructAllTest 2 11 "DestructAllAnd" + destructAllTest 4 23 "DestructAllMany" + destructAllTest 2 18 "DestructAllNonVarTopMatch" + destructAllTest 2 18 "DestructAllFunc" + destructAllTest 19 18 "DestructAllGADTEvidence" diff --git a/test/CodeAction/DestructPunSpec.hs b/test/CodeAction/DestructPunSpec.hs new file mode 100644 --- /dev/null +++ b/test/CodeAction/DestructPunSpec.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE OverloadedStrings #-} + +module CodeAction.DestructPunSpec where + +import Wingman.Types +import Test.Hspec +import Utils + + +spec :: Spec +spec = do + let destructTest = goldenTest DestructPun + + describe "golden" $ do + destructTest "x" 4 9 "PunSimple" + destructTest "x" 6 10 "PunMany" + destructTest "x" 11 11 "PunGADT" + destructTest "x" 17 11 "PunManyGADT" + destructTest "x" 4 12 "PunShadowing" + diff --git a/test/CodeAction/DestructSpec.hs b/test/CodeAction/DestructSpec.hs --- a/test/CodeAction/DestructSpec.hs +++ b/test/CodeAction/DestructSpec.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.DestructSpec where @@ -17,21 +12,26 @@ let destructTest = goldenTest Destruct describe "golden" $ do - destructTest "gadt" 7 17 "GoldenGADTDestruct.hs" - destructTest "gadt" 8 17 "GoldenGADTDestructCoercion.hs" - destructTest "a" 7 25 "SplitPattern.hs" + destructTest "gadt" 7 17 "GoldenGADTDestruct" + destructTest "gadt" 8 17 "GoldenGADTDestructCoercion" + destructTest "a" 7 25 "SplitPattern" + destructTest "a" 6 18 "DestructPun" + destructTest "fp" 31 14 "DestructCthulhu" + destructTest "b" 7 10 "DestructTyFam" + destructTest "b" 7 10 "DestructDataFam" + destructTest "b" 17 10 "DestructTyToDataFam" describe "layout" $ do - destructTest "b" 4 3 "LayoutBind.hs" - destructTest "b" 2 15 "LayoutDollarApp.hs" - destructTest "b" 2 18 "LayoutOpApp.hs" - destructTest "b" 2 14 "LayoutLam.hs" - destructTest "x" 11 15 "LayoutSplitWhere.hs" - destructTest "x" 3 12 "LayoutSplitClass.hs" - destructTest "b" 3 9 "LayoutSplitGuard.hs" - destructTest "b" 4 13 "LayoutSplitLet.hs" - destructTest "a" 4 7 "LayoutSplitIn.hs" - destructTest "a" 4 31 "LayoutSplitViewPat.hs" - destructTest "a" 7 17 "LayoutSplitPattern.hs" - destructTest "a" 8 26 "LayoutSplitPatSyn.hs" + destructTest "b" 4 3 "LayoutBind" + destructTest "b" 2 15 "LayoutDollarApp" + destructTest "b" 2 18 "LayoutOpApp" + destructTest "b" 2 14 "LayoutLam" + destructTest "x" 11 15 "LayoutSplitWhere" + destructTest "x" 3 12 "LayoutSplitClass" + destructTest "b" 3 9 "LayoutSplitGuard" + destructTest "b" 4 13 "LayoutSplitLet" + destructTest "a" 4 7 "LayoutSplitIn" + destructTest "a" 4 31 "LayoutSplitViewPat" + destructTest "a" 7 17 "LayoutSplitPattern" + destructTest "a" 8 26 "LayoutSplitPatSyn" diff --git a/test/CodeAction/IntrosSpec.hs b/test/CodeAction/IntrosSpec.hs --- a/test/CodeAction/IntrosSpec.hs +++ b/test/CodeAction/IntrosSpec.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.IntrosSpec where @@ -17,5 +12,8 @@ let introsTest = goldenTest Intros "" describe "golden" $ do - introsTest 2 8 "GoldenIntros.hs" + introsTest 2 8 "GoldenIntros" + + describe "layout" $ do + introsTest 4 24 "LayoutRec" diff --git a/test/CodeAction/RefineSpec.hs b/test/CodeAction/RefineSpec.hs --- a/test/CodeAction/RefineSpec.hs +++ b/test/CodeAction/RefineSpec.hs @@ -1,16 +1,10 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.RefineSpec where import Wingman.Types import Test.Hspec import Utils -import Wingman.FeatureSet (allFeatures) spec :: Spec @@ -18,11 +12,11 @@ let refineTest = goldenTest Refine "" describe "golden" $ do - refineTest 2 8 "RefineIntro.hs" - refineTest 2 8 "RefineCon.hs" - refineTest 4 8 "RefineReader.hs" - refineTest 8 8 "RefineGADT.hs" + refineTest 2 8 "RefineIntro" + refineTest 2 8 "RefineCon" + refineTest 4 10 "RefineReader" + refineTest 8 10 "RefineGADT" describe "messages" $ do - mkShowMessageTest allFeatures Refine "" 2 8 "MessageForallA.hs" NothingToDo + mkShowMessageTest Refine "" 2 8 "MessageForallA" TacticErrors diff --git a/test/CodeAction/RunMetaprogramSpec.hs b/test/CodeAction/RunMetaprogramSpec.hs new file mode 100644 --- /dev/null +++ b/test/CodeAction/RunMetaprogramSpec.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} + +module CodeAction.RunMetaprogramSpec where + +import Utils +import Test.Hspec +import Wingman.Types + + +spec :: Spec +spec = do + let metaTest l c f = +#if __GLASGOW_HASKELL__ >= 808 + goldenTest RunMetaprogram "" l c f +#else + pure () +#endif + +#if __GLASGOW_HASKELL__ >= 808 + describe "beginMetaprogram" $ do + goldenTest BeginMetaprogram "" 1 7 "MetaBegin" +#endif + + describe "golden" $ do + metaTest 6 11 "MetaMaybeAp" + metaTest 2 32 "MetaBindOne" + metaTest 2 32 "MetaBindAll" + metaTest 2 13 "MetaTry" + metaTest 2 74 "MetaChoice" + metaTest 5 40 "MetaUseImport" + metaTest 6 31 "MetaUseLocal" + metaTest 11 11 "MetaUseMethod" + metaTest 9 38 "MetaCataCollapse" + metaTest 7 16 "MetaCataCollapseUnary" + diff --git a/test/CodeAction/UseDataConSpec.hs b/test/CodeAction/UseDataConSpec.hs --- a/test/CodeAction/UseDataConSpec.hs +++ b/test/CodeAction/UseDataConSpec.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module CodeAction.UseDataConSpec where @@ -20,7 +15,7 @@ describe "provider" $ do mkTest "Suggests all data cons for Either" - "ConProviders.hs" 5 6 + "ConProviders" 5 6 [ (id, UseDataCon, "Left") , (id, UseDataCon, "Right") , (not, UseDataCon, ":") @@ -29,19 +24,19 @@ ] mkTest "Suggests no data cons for big types" - "ConProviders.hs" 11 17 $ do + "ConProviders" 11 17 $ do c <- [1 :: Int .. 10] pure $ (not, UseDataCon, T.pack $ show c) mkTest "Suggests only matching data cons for GADT" - "ConProviders.hs" 20 12 + "ConProviders" 20 12 [ (id, UseDataCon, "IntGADT") , (id, UseDataCon, "VarGADT") , (not, UseDataCon, "BoolGADT") ] describe "golden" $ do - useTest "(,)" 2 8 "UseConPair.hs" - useTest "Left" 2 8 "UseConLeft.hs" - useTest "Right" 2 8 "UseConRight.hs" + useTest "(,)" 2 8 "UseConPair" + useTest "Left" 2 8 "UseConLeft" + useTest "Right" 2 8 "UseConRight" diff --git a/test/CodeLens/EmptyCaseSpec.hs b/test/CodeLens/EmptyCaseSpec.hs new file mode 100644 --- /dev/null +++ b/test/CodeLens/EmptyCaseSpec.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE OverloadedStrings #-} + +module CodeLens.EmptyCaseSpec where + +import Test.Hspec +import Utils + + +spec :: Spec +spec = do + let test = mkCodeLensTest + + describe "golden" $ do + test "EmptyCaseADT" + test "EmptyCaseShadow" + test "EmptyCaseParens" + test "EmptyCaseNested" + test "EmptyCaseApply" + test "EmptyCaseGADT" + diff --git a/test/ProviderSpec.hs b/test/ProviderSpec.hs --- a/test/ProviderSpec.hs +++ b/test/ProviderSpec.hs @@ -1,9 +1,4 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE OverloadedStrings #-} module ProviderSpec where @@ -16,57 +11,58 @@ spec = do mkTest "Produces intros code action" - "T1.hs" 2 14 + "T1" 2 14 [ (id, Intros, "") ] mkTest "Produces destruct and homomorphism code actions" - "T2.hs" 2 21 + "T2" 2 21 [ (id, Destruct, "eab") , (id, Homomorphism, "eab") + , (not, DestructPun, "eab") ] mkTest "Won't suggest homomorphism on the wrong type" - "T2.hs" 8 8 + "T2" 8 8 [ (not, Homomorphism, "global") ] mkTest "Won't suggest intros on the wrong type" - "T2.hs" 8 8 + "T2" 8 8 [ (not, Intros, "") ] mkTest "Produces (homomorphic) lambdacase code actions" - "T3.hs" 4 24 + "T3" 4 24 [ (id, HomomorphismLambdaCase, "") , (id, DestructLambdaCase, "") ] mkTest "Produces lambdacase code actions" - "T3.hs" 7 13 + "T3" 7 13 [ (id, DestructLambdaCase, "") ] mkTest "Doesn't suggest lambdacase without -XLambdaCase" - "T2.hs" 11 25 + "T2" 11 25 [ (not, DestructLambdaCase, "") ] mkTest "Doesn't suggest destruct if already destructed" - "ProvideAlreadyDestructed.hs" 6 18 + "ProvideAlreadyDestructed" 6 18 [ (not, Destruct, "x") ] mkTest "...but does suggest destruct if destructed in a different branch" - "ProvideAlreadyDestructed.hs" 9 7 + "ProvideAlreadyDestructed" 9 7 [ (id, Destruct, "x") ] mkTest "Doesn't suggest destruct on class methods" - "ProvideLocalHyOnly.hs" 2 12 + "ProvideLocalHyOnly" 2 12 [ (not, Destruct, "mempty") ] diff --git a/test/Utils.hs b/test/Utils.hs --- a/test/Utils.hs +++ b/test/Utils.hs @@ -9,7 +9,7 @@ import Control.DeepSeq (deepseq) import qualified Control.Exception as E -import Control.Lens hiding (failing, (<.>), (.=)) +import Control.Lens hiding (List, failing, (<.>), (.=)) import Control.Monad (unless) import Control.Monad.IO.Class import Data.Aeson @@ -29,11 +29,10 @@ import Test.Hls import Test.Hspec import Test.Hspec.Formatters (FailureReason(ExpectedButGot)) -import Test.Tasty.HUnit (Assertion, HUnitFailure(..)) -import Wingman.FeatureSet (FeatureSet, allFeatures, prettyFeatureSet) import Wingman.LanguageServer (mkShowMessageParams) import Wingman.Types + plugin :: PluginDescriptor IdeState plugin = Tactic.descriptor "tactics" @@ -61,7 +60,7 @@ mkTest :: Foldable t => String -- ^ The test name - -> FilePath -- ^ The file to load + -> FilePath -- ^ The file name stem (without extension) to load -> Int -- ^ Cursor line -> Int -- ^ Cursor columnn -> t ( Bool -> Bool -- Use 'not' for actions that shouldnt be present @@ -71,8 +70,7 @@ -> SpecWith (Arg Bool) mkTest name fp line col ts = it name $ do runSessionWithServer plugin tacticPath $ do - setFeatureSet allFeatures - doc <- openDoc fp "haskell" + doc <- openDoc (fp <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col let titles = mapMaybe codeActionTitle actions @@ -82,36 +80,19 @@ (title `elem` titles) `shouldSatisfy` f -setFeatureSet :: FeatureSet -> Session () -setFeatureSet features = do - let unObject (Object obj) = obj - unObject _ = undefined - def_config = def :: Plugin.Config - config = - def_config - { Plugin.plugins = M.fromList [("tactics", - def { Plugin.plcConfig = unObject $ object ["features" .= prettyFeatureSet features] } - )] <> Plugin.plugins def_config } - sendNotification SWorkspaceDidChangeConfiguration $ - DidChangeConfigurationParams $ - toJSON config - - mkGoldenTest :: (Text -> Text -> Assertion) - -> FeatureSet -> TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith () -mkGoldenTest eq features tc occ line col input = +mkGoldenTest eq tc occ line col input = it (input <> " (golden)") $ do runSessionWithServer plugin tacticPath $ do - setFeatureSet features - doc <- openDoc input "haskell" + doc <- openDoc (input <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col Just (InR CodeAction {_command = Just c}) @@ -119,27 +100,54 @@ executeCommand c _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit) edited <- documentContents doc - let expected_name = input <.> "expected" + let expected_name = input <.> "expected" <.> "hs" -- Write golden tests if they don't already exist liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do T.writeFile expected_name edited expected <- liftIO $ T.readFile expected_name liftIO $ edited `eq` expected + +mkCodeLensTest + :: FilePath + -> SpecWith () +mkCodeLensTest input = + it (input <> " (golden)") $ do + runSessionWithServer plugin tacticPath $ do + doc <- openDoc (input <.> "hs") "haskell" + _ <- waitForDiagnostics + lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc + for_ lenses $ \(CodeLens _ (Just cmd) _) -> + executeCommand cmd + _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit) + edited <- documentContents doc + let expected_name = input <.> "expected" <.> "hs" + -- Write golden tests if they don't already exist + liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do + T.writeFile expected_name edited + expected <- liftIO $ T.readFile expected_name + liftIO $ edited `shouldBe` expected + + + +isWingmanLens :: CodeLens -> Bool +isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _) + = T.isInfixOf ":tactics:" cmd +isWingmanLens _ = False + + mkShowMessageTest - :: FeatureSet - -> TacticCommand + :: TacticCommand -> Text -> Int -> Int -> FilePath -> UserFacingMessage -> SpecWith () -mkShowMessageTest features tc occ line col input ufm = +mkShowMessageTest tc occ line col input ufm = it (input <> " (golden)") $ do runSessionWithServer plugin tacticPath $ do - setFeatureSet features - doc <- openDoc input "haskell" + doc <- openDoc (input <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col Just (InR CodeAction {_command = Just c}) @@ -150,10 +158,10 @@ goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith () -goldenTest = mkGoldenTest shouldBe allFeatures +goldenTest = mkGoldenTest shouldBe goldenTestNoWhitespace :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith () -goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces allFeatures +goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces shouldBeIgnoringSpaces :: Text -> Text -> Assertion diff --git a/test/golden/AutoEmptyString.expected.hs b/test/golden/AutoEmptyString.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoEmptyString.expected.hs @@ -0,0 +1,2 @@ +empty_string :: String +empty_string = "" diff --git a/test/golden/AutoEmptyString.hs.expected b/test/golden/AutoEmptyString.hs.expected deleted file mode 100644 --- a/test/golden/AutoEmptyString.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -empty_string :: String -empty_string = "" diff --git a/test/golden/AutoEndo.expected.hs b/test/golden/AutoEndo.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoEndo.expected.hs @@ -0,0 +1,11 @@ +data Synthesized b a = Synthesized + { syn_trace :: b + , syn_val :: a + } + deriving (Eq, Show) + + +mapTrace :: (b -> b) -> Synthesized b a -> Synthesized b a +mapTrace fbb (Synthesized b a) + = Synthesized {syn_trace = fbb b, syn_val = a} + diff --git a/test/golden/AutoEndo.hs.expected b/test/golden/AutoEndo.hs.expected deleted file mode 100644 --- a/test/golden/AutoEndo.hs.expected +++ /dev/null @@ -1,11 +0,0 @@ -data Synthesized b a = Synthesized - { syn_trace :: b - , syn_val :: a - } - deriving (Eq, Show) - - -mapTrace :: (b -> b) -> Synthesized b a -> Synthesized b a -mapTrace fbb (Synthesized b a) - = Synthesized {syn_trace = fbb b, syn_val = a} - diff --git a/test/golden/AutoInfixApply.expected.hs b/test/golden/AutoInfixApply.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoInfixApply.expected.hs @@ -0,0 +1,3 @@ +test :: (a -> b -> c) -> a -> (a -> b) -> c +test (/:) a f = a /: f a + diff --git a/test/golden/AutoInfixApply.hs.expected b/test/golden/AutoInfixApply.hs.expected deleted file mode 100644 --- a/test/golden/AutoInfixApply.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -test :: (a -> b -> c) -> a -> (a -> b) -> c -test (/:) a f = a /: f a - diff --git a/test/golden/AutoInfixApplyMany.expected.hs b/test/golden/AutoInfixApplyMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoInfixApplyMany.expected.hs @@ -0,0 +1,3 @@ +test :: (a -> b -> x -> c) -> a -> (a -> b) -> x -> c +test (/:) a f x = (a /: f a) x + diff --git a/test/golden/AutoInfixApplyMany.hs.expected b/test/golden/AutoInfixApplyMany.hs.expected deleted file mode 100644 --- a/test/golden/AutoInfixApplyMany.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -test :: (a -> b -> x -> c) -> a -> (a -> b) -> x -> c -test (/:) a f x = (a /: f a) x - diff --git a/test/golden/AutoInfixInfix.expected.hs b/test/golden/AutoInfixInfix.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoInfixInfix.expected.hs @@ -0,0 +1,2 @@ +test :: (a -> b -> c) -> (c -> d -> e) -> a -> (a -> b) -> d -> e +test (/:) (-->) a f x = (a /: f a) --> x diff --git a/test/golden/AutoInfixInfix.hs.expected b/test/golden/AutoInfixInfix.hs.expected deleted file mode 100644 --- a/test/golden/AutoInfixInfix.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -test :: (a -> b -> c) -> (c -> d -> e) -> a -> (a -> b) -> d -> e -test (/:) (-->) a f x = (a /: f a) --> x diff --git a/test/golden/AutoPatSynUse.expected.hs b/test/golden/AutoPatSynUse.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoPatSynUse.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE PatternSynonyms #-} + +pattern JustSingleton :: a -> Maybe [a] +pattern JustSingleton a <- Just [a] + +amIASingleton :: Maybe [a] -> Maybe a +amIASingleton (JustSingleton a) = Just a + diff --git a/test/golden/AutoPatSynUse.hs.expected b/test/golden/AutoPatSynUse.hs.expected deleted file mode 100644 --- a/test/golden/AutoPatSynUse.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE PatternSynonyms #-} - -pattern JustSingleton :: a -> Maybe [a] -pattern JustSingleton a <- Just [a] - -amIASingleton :: Maybe [a] -> Maybe a -amIASingleton (JustSingleton a) = Just a - diff --git a/test/golden/AutoSplitGADT.expected.hs b/test/golden/AutoSplitGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoSplitGADT.expected.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +data GADT b a where + GBool :: b -> GADT b Bool + GInt :: GADT b Int + +-- wingman would prefer to use GBool since then it can use its argument. But +-- that won't unify with GADT Int, so it is forced to pick GInt and ignore the +-- argument. +test :: b -> GADT b Int +test _ = GInt + diff --git a/test/golden/AutoSplitGADT.hs.expected b/test/golden/AutoSplitGADT.hs.expected deleted file mode 100644 --- a/test/golden/AutoSplitGADT.hs.expected +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data GADT b a where - GBool :: b -> GADT b Bool - GInt :: GADT b Int - --- wingman would prefer to use GBool since then it can use its argument. But --- that won't unify with GADT Int, so it is forced to pick GInt and ignore the --- argument. -test :: b -> GADT b Int -test _ = GInt - diff --git a/test/golden/AutoThetaEqCtx.expected.hs b/test/golden/AutoThetaEqCtx.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaEqCtx.expected.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE GADTs #-} + +fun2 :: (a ~ b) => a -> b +fun2 = id -- id + diff --git a/test/golden/AutoThetaEqCtx.hs.expected b/test/golden/AutoThetaEqCtx.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaEqCtx.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -{-# LANGUAGE GADTs #-} - -fun2 :: (a ~ b) => a -> b -fun2 = id -- id - diff --git a/test/golden/AutoThetaEqGADT.expected.hs b/test/golden/AutoThetaEqGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaEqGADT.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} + +data Y a b = a ~ b => Y + +fun3 :: Y a b -> a -> b +fun3 Y = id + diff --git a/test/golden/AutoThetaEqGADT.hs.expected b/test/golden/AutoThetaEqGADT.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaEqGADT.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data Y a b = a ~ b => Y - -fun3 :: Y a b -> a -> b -fun3 Y = id - diff --git a/test/golden/AutoThetaEqGADTDestruct.expected.hs b/test/golden/AutoThetaEqGADTDestruct.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaEqGADTDestruct.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-} + +data Y a b = a ~ b => Y + +fun3 :: Y a b -> a -> b +fun3 Y a = a + + diff --git a/test/golden/AutoThetaEqGADTDestruct.hs.expected b/test/golden/AutoThetaEqGADTDestruct.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaEqGADTDestruct.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data Y a b = a ~ b => Y - -fun3 :: Y a b -> a -> b -fun3 Y a = a - - diff --git a/test/golden/AutoThetaFix.expected.hs b/test/golden/AutoThetaFix.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaFix.expected.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +data Fix f a = Fix (f (Fix f a)) + +instance ( Functor f + -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire + -- on this case. By explicitly adding the @Functor (Fix f)@ + -- dictionary, we can get Wingman to generate the right definition. + , Functor (Fix f) + ) => Functor (Fix f) where + fmap fab (Fix f) = Fix (fmap (fmap fab) f) + diff --git a/test/golden/AutoThetaFix.hs.expected b/test/golden/AutoThetaFix.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaFix.hs.expected +++ /dev/null @@ -1,13 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE UndecidableInstances #-} - -data Fix f a = Fix (f (Fix f a)) - -instance ( Functor f - -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire - -- on this case. By explicitly adding the @Functor (Fix f)@ - -- dictionary, we can get Wingman to generate the right definition. - , Functor (Fix f) - ) => Functor (Fix f) where - fmap fab (Fix fffa) = Fix (fmap (fmap fab) fffa) - diff --git a/test/golden/AutoThetaGADT.expected.hs b/test/golden/AutoThetaGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaGADT.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} + +data X f = Monad f => X + +fun1 :: X f -> a -> f a +fun1 X = pure + diff --git a/test/golden/AutoThetaGADT.hs.expected b/test/golden/AutoThetaGADT.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaGADT.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data X f = Monad f => X - -fun1 :: X f -> a -> f a -fun1 X = pure - diff --git a/test/golden/AutoThetaGADTDestruct.expected.hs b/test/golden/AutoThetaGADTDestruct.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaGADTDestruct.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} + +data X f = Monad f => X + +fun1 :: X f -> a -> f a +fun1 X a = pure a + diff --git a/test/golden/AutoThetaGADTDestruct.hs.expected b/test/golden/AutoThetaGADTDestruct.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaGADTDestruct.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data X f = Monad f => X - -fun1 :: X f -> a -> f a -fun1 X a = pure a - diff --git a/test/golden/AutoThetaMultipleUnification.expected.hs b/test/golden/AutoThetaMultipleUnification.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaMultipleUnification.expected.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t _) = t +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/test/golden/AutoThetaMultipleUnification.hs b/test/golden/AutoThetaMultipleUnification.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaMultipleUnification.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t hl') = _ +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/test/golden/AutoThetaRankN.expected.hs b/test/golden/AutoThetaRankN.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaRankN.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE RankNTypes #-} + +showMe :: (forall x. Show x => x -> String) -> Int -> String +showMe f = f + +showedYou :: Int -> String +showedYou = showMe show + diff --git a/test/golden/AutoThetaRankN.hs.expected b/test/golden/AutoThetaRankN.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaRankN.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE RankNTypes #-} - -showMe :: (forall x. Show x => x -> String) -> Int -> String -showMe f = f - -showedYou :: Int -> String -showedYou = showMe show - diff --git a/test/golden/AutoThetaRefl.expected.hs b/test/golden/AutoThetaRefl.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaRefl.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} + +data Z a b where Z :: Z a a + +fun4 :: Z a b -> a -> b +fun4 Z = id -- id + diff --git a/test/golden/AutoThetaRefl.hs.expected b/test/golden/AutoThetaRefl.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaRefl.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data Z a b where Z :: Z a a - -fun4 :: Z a b -> a -> b -fun4 Z = id -- id - diff --git a/test/golden/AutoThetaReflDestruct.expected.hs b/test/golden/AutoThetaReflDestruct.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaReflDestruct.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-} + +data Z a b where Z :: Z a a + +fun4 :: Z a b -> a -> b +fun4 Z a = a -- id + + diff --git a/test/golden/AutoThetaReflDestruct.hs.expected b/test/golden/AutoThetaReflDestruct.hs.expected deleted file mode 100644 --- a/test/golden/AutoThetaReflDestruct.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data Z a b where Z :: Z a a - -fun4 :: Z a b -> a -> b -fun4 Z a = a -- id - - diff --git a/test/golden/AutoThetaSplitUnification.expected.hs b/test/golden/AutoThetaSplitUnification.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaSplitUnification.expected.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +data A = A +data B = B +data X = X +data Y = Y + + +data Pairrow ax by where + Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y) + +test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y) +test2 = Pairrow + diff --git a/test/golden/AutoThetaSplitUnification.hs b/test/golden/AutoThetaSplitUnification.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoThetaSplitUnification.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +data A = A +data B = B +data X = X +data Y = Y + + +data Pairrow ax by where + Pairrow :: (a -> b) -> (x -> y) -> Pairrow '(a, x) '(b, y) + +test2 :: (A -> B) -> (X -> Y) -> Pairrow '(A, X) '(B, Y) +test2 = _ + diff --git a/test/golden/AutoZip.expected.hs b/test/golden/AutoZip.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoZip.expected.hs @@ -0,0 +1,6 @@ +zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)] +zip_it_up_and_zip_it_out _ [] = [] +zip_it_up_and_zip_it_out [] (_ : _) = [] +zip_it_up_and_zip_it_out (a : as') (b : bs') + = (a, b) : zip_it_up_and_zip_it_out as' bs' + diff --git a/test/golden/AutoZip.hs.expected b/test/golden/AutoZip.hs.expected deleted file mode 100644 --- a/test/golden/AutoZip.hs.expected +++ /dev/null @@ -1,6 +0,0 @@ -zip_it_up_and_zip_it_out :: [a] -> [b] -> [(a, b)] -zip_it_up_and_zip_it_out _ [] = [] -zip_it_up_and_zip_it_out [] (_ : _) = [] -zip_it_up_and_zip_it_out (a : l_a5) (b : l_b3) - = (a, b) : zip_it_up_and_zip_it_out l_a5 l_b3 - diff --git a/test/golden/DestructAllAnd.expected.hs b/test/golden/DestructAllAnd.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllAnd.expected.hs @@ -0,0 +1,5 @@ +and :: Bool -> Bool -> Bool +and False False = _ +and False True = _ +and True False = _ +and True True = _ diff --git a/test/golden/DestructAllAnd.hs.expected b/test/golden/DestructAllAnd.hs.expected deleted file mode 100644 --- a/test/golden/DestructAllAnd.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -and :: Bool -> Bool -> Bool -and False False = _ -and True False = _ -and False True = _ -and True True = _ diff --git a/test/golden/DestructAllFunc.expected.hs b/test/golden/DestructAllFunc.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllFunc.expected.hs @@ -0,0 +1,4 @@ +has_a_func :: Bool -> (a -> b) -> Bool +has_a_func False y = _ +has_a_func True y = _ + diff --git a/test/golden/DestructAllFunc.hs.expected b/test/golden/DestructAllFunc.hs.expected deleted file mode 100644 --- a/test/golden/DestructAllFunc.hs.expected +++ /dev/null @@ -1,4 +0,0 @@ -has_a_func :: Bool -> (a -> b) -> Bool -has_a_func False y = _ -has_a_func True y = _ - diff --git a/test/golden/DestructAllGADTEvidence.expected.hs b/test/golden/DestructAllGADTEvidence.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllGADTEvidence.expected.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp AtZ (HCons t hl') = _ +lookMeUp (AtS ea') (HCons t hl') = _ + diff --git a/test/golden/DestructAllGADTEvidence.hs b/test/golden/DestructAllGADTEvidence.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllGADTEvidence.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +import Data.Kind + +data Nat = Z | S Nat + +data HList (ls :: [Type]) where + HNil :: HList '[] + HCons :: t -> HList ts -> HList (t ': ts) + +data ElemAt (n :: Nat) t (ts :: [Type]) where + AtZ :: ElemAt 'Z t (t ': ts) + AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts) + +lookMeUp :: ElemAt i ty tys -> HList tys -> ty +lookMeUp ea hl = _ + diff --git a/test/golden/DestructAllMany.expected.hs b/test/golden/DestructAllMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllMany.expected.hs @@ -0,0 +1,27 @@ +data ABC = A | B | C + +many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> () +many () (Left a) False Nothing A = _ +many () (Left a) False Nothing B = _ +many () (Left a) False Nothing C = _ +many () (Left a) False (Just abc') A = _ +many () (Left a) False (Just abc') B = _ +many () (Left a) False (Just abc') C = _ +many () (Left a) True Nothing A = _ +many () (Left a) True Nothing B = _ +many () (Left a) True Nothing C = _ +many () (Left a) True (Just abc') A = _ +many () (Left a) True (Just abc') B = _ +many () (Left a) True (Just abc') C = _ +many () (Right b') False Nothing A = _ +many () (Right b') False Nothing B = _ +many () (Right b') False Nothing C = _ +many () (Right b') False (Just abc') A = _ +many () (Right b') False (Just abc') B = _ +many () (Right b') False (Just abc') C = _ +many () (Right b') True Nothing A = _ +many () (Right b') True Nothing B = _ +many () (Right b') True Nothing C = _ +many () (Right b') True (Just abc') A = _ +many () (Right b') True (Just abc') B = _ +many () (Right b') True (Just abc') C = _ diff --git a/test/golden/DestructAllMany.hs.expected b/test/golden/DestructAllMany.hs.expected deleted file mode 100644 --- a/test/golden/DestructAllMany.hs.expected +++ /dev/null @@ -1,27 +0,0 @@ -data ABC = A | B | C - -many :: () -> Either a b -> Bool -> Maybe ABC -> ABC -> () -many () (Left a) False Nothing A = _ -many () (Right b5) False Nothing A = _ -many () (Left a) True Nothing A = _ -many () (Right b5) True Nothing A = _ -many () (Left a6) False (Just a) A = _ -many () (Right b6) False (Just a) A = _ -many () (Left a6) True (Just a) A = _ -many () (Right b6) True (Just a) A = _ -many () (Left a) False Nothing B = _ -many () (Right b5) False Nothing B = _ -many () (Left a) True Nothing B = _ -many () (Right b5) True Nothing B = _ -many () (Left a6) False (Just a) B = _ -many () (Right b6) False (Just a) B = _ -many () (Left a6) True (Just a) B = _ -many () (Right b6) True (Just a) B = _ -many () (Left a) False Nothing C = _ -many () (Right b5) False Nothing C = _ -many () (Left a) True Nothing C = _ -many () (Right b5) True Nothing C = _ -many () (Left a6) False (Just a) C = _ -many () (Right b6) False (Just a) C = _ -many () (Left a6) True (Just a) C = _ -many () (Right b6) True (Just a) C = _ diff --git a/test/golden/DestructAllNonVarTopMatch.expected.hs b/test/golden/DestructAllNonVarTopMatch.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructAllNonVarTopMatch.expected.hs @@ -0,0 +1,6 @@ +and :: (a, b) -> Bool -> Bool -> Bool +and (a, b) False False = _ +and (a, b) False True = _ +and (a, b) True False = _ +and (a, b) True True = _ + diff --git a/test/golden/DestructAllNonVarTopMatch.hs.expected b/test/golden/DestructAllNonVarTopMatch.hs.expected deleted file mode 100644 --- a/test/golden/DestructAllNonVarTopMatch.hs.expected +++ /dev/null @@ -1,6 +0,0 @@ -and :: (a, b) -> Bool -> Bool -> Bool -and (a, b) False False = _ -and (a, b) True False = _ -and (a, b) False True = _ -and (a, b) True True = _ - diff --git a/test/golden/DestructCthulhu.expected.hs b/test/golden/DestructCthulhu.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructCthulhu.expected.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE GADTs #-} + +data FreePro r c a b where + ID :: FreePro r c x x + Comp :: FreePro r c x y -> FreePro r c y z -> FreePro r c x z + Copy :: FreePro r c x (x, x) + Consume :: FreePro r c x () + Swap :: FreePro r c (a, b) (b, a) + SwapE :: FreePro r c (Either a b) (Either b a) + Fst :: FreePro r c (a, b) a + Snd :: FreePro r c (a, b) b + InjectL :: FreePro r c a (Either a b) + InjectR :: FreePro r c b (Either a b) + Unify :: FreePro r c (Either a a) a + First :: FreePro r c a b -> FreePro r c (a, m) (b, m) + Second :: FreePro r c a b -> FreePro r c (m, a) (m, b) + Alongside :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (a, a') (b, b') + Fanout :: FreePro r c a b -> FreePro r c a b' -> FreePro r c a (b, b') + Left' :: FreePro r c a b -> FreePro r c (Either a x) (Either b x) + Right' :: FreePro r c a b -> FreePro r c (Either x a) (Either x b) + EitherOf :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (Either a a') (Either b b') + Fanin :: FreePro r c a b -> FreePro r c a' b -> FreePro r c (Either a a') b + LiftC :: c a b -> FreePro r c a b + Zero :: FreePro r c x y + Plus :: FreePro r c x y -> FreePro r c x y -> FreePro r c x y + Unleft :: FreePro r c (Either a d) (Either b d) -> FreePro r c a b + Unright :: FreePro r c (Either d a) (Either d b) -> FreePro r c a b + + +cthulhu :: FreePro r c a b -> FreePro r c a b +cthulhu ID = _ +cthulhu (Comp fp' fp_rcyb) = _ +cthulhu Copy = _ +cthulhu Consume = _ +cthulhu Swap = _ +cthulhu SwapE = _ +cthulhu Fst = _ +cthulhu Snd = _ +cthulhu InjectL = _ +cthulhu InjectR = _ +cthulhu Unify = _ +cthulhu (First fp') = _ +cthulhu (Second fp') = _ +cthulhu (Alongside fp' fp_rca'b') = _ +cthulhu (Fanout fp' fp_rcab') = _ +cthulhu (Left' fp') = _ +cthulhu (Right' fp') = _ +cthulhu (EitherOf fp' fp_rca'b') = _ +cthulhu (Fanin fp' fp_rca'b) = _ +cthulhu (LiftC cab) = _ +cthulhu Zero = _ +cthulhu (Plus fp' fp_rcab) = _ +cthulhu (Unleft fp') = _ +cthulhu (Unright fp') = _ diff --git a/test/golden/DestructCthulhu.hs b/test/golden/DestructCthulhu.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructCthulhu.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE GADTs #-} + +data FreePro r c a b where + ID :: FreePro r c x x + Comp :: FreePro r c x y -> FreePro r c y z -> FreePro r c x z + Copy :: FreePro r c x (x, x) + Consume :: FreePro r c x () + Swap :: FreePro r c (a, b) (b, a) + SwapE :: FreePro r c (Either a b) (Either b a) + Fst :: FreePro r c (a, b) a + Snd :: FreePro r c (a, b) b + InjectL :: FreePro r c a (Either a b) + InjectR :: FreePro r c b (Either a b) + Unify :: FreePro r c (Either a a) a + First :: FreePro r c a b -> FreePro r c (a, m) (b, m) + Second :: FreePro r c a b -> FreePro r c (m, a) (m, b) + Alongside :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (a, a') (b, b') + Fanout :: FreePro r c a b -> FreePro r c a b' -> FreePro r c a (b, b') + Left' :: FreePro r c a b -> FreePro r c (Either a x) (Either b x) + Right' :: FreePro r c a b -> FreePro r c (Either x a) (Either x b) + EitherOf :: FreePro r c a b -> FreePro r c a' b' -> FreePro r c (Either a a') (Either b b') + Fanin :: FreePro r c a b -> FreePro r c a' b -> FreePro r c (Either a a') b + LiftC :: c a b -> FreePro r c a b + Zero :: FreePro r c x y + Plus :: FreePro r c x y -> FreePro r c x y -> FreePro r c x y + Unleft :: FreePro r c (Either a d) (Either b d) -> FreePro r c a b + Unright :: FreePro r c (Either d a) (Either d b) -> FreePro r c a b + + +cthulhu :: FreePro r c a b -> FreePro r c a b +cthulhu fp = _ diff --git a/test/golden/DestructDataFam.expected.hs b/test/golden/DestructDataFam.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructDataFam.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE TypeFamilies #-} + +data family Yo +data instance Yo = Heya Int + +test :: Yo -> Int +test (Heya n) = _ + diff --git a/test/golden/DestructDataFam.hs b/test/golden/DestructDataFam.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructDataFam.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE TypeFamilies #-} + +data family Yo +data instance Yo = Heya Int + +test :: Yo -> Int +test b = _ + diff --git a/test/golden/DestructPun.expected.hs b/test/golden/DestructPun.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructPun.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE NamedFieldPuns #-} + + +data Foo = Foo { a :: Bool, b :: Bool } + +foo Foo {a = False, b} = _ +foo Foo {a = True, b} = _ + diff --git a/test/golden/DestructPun.hs b/test/golden/DestructPun.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructPun.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE NamedFieldPuns #-} + + +data Foo = Foo { a :: Bool, b :: Bool } + +foo Foo {a, b} = _ + diff --git a/test/golden/DestructTyFam.expected.hs b/test/golden/DestructTyFam.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructTyFam.expected.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies #-} + +type family Yo where + Yo = Bool + +test :: Yo -> Int +test False = _ +test True = _ + diff --git a/test/golden/DestructTyFam.hs b/test/golden/DestructTyFam.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructTyFam.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE TypeFamilies #-} + +type family Yo where + Yo = Bool + +test :: Yo -> Int +test b = _ + diff --git a/test/golden/DestructTyToDataFam.expected.hs b/test/golden/DestructTyToDataFam.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructTyToDataFam.expected.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +type family T1 a where + T1 a = T2 Int + +type family T2 a +type instance T2 Int = T3 + +type family T3 where + T3 = Yo + +data family Yo +data instance Yo = Heya Int + +test :: T1 Bool -> Int +test (Heya n) = _ + diff --git a/test/golden/DestructTyToDataFam.hs b/test/golden/DestructTyToDataFam.hs new file mode 100644 --- /dev/null +++ b/test/golden/DestructTyToDataFam.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +type family T1 a where + T1 a = T2 Int + +type family T2 a +type instance T2 Int = T3 + +type family T3 where + T3 = Yo + +data family Yo +data instance Yo = Heya Int + +test :: T1 Bool -> Int +test b = _ + diff --git a/test/golden/EmptyCaseADT.expected.hs b/test/golden/EmptyCaseADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseADT.expected.hs @@ -0,0 +1,8 @@ +data Foo = A Int | B Bool | C + +foo :: Foo -> () +foo x = case x of + A n -> _ + B b -> _ + C -> _ + diff --git a/test/golden/EmptyCaseADT.hs b/test/golden/EmptyCaseADT.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseADT.hs @@ -0,0 +1,5 @@ +data Foo = A Int | B Bool | C + +foo :: Foo -> () +foo x = case x of + diff --git a/test/golden/EmptyCaseApply.expected.hs b/test/golden/EmptyCaseApply.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseApply.expected.hs @@ -0,0 +1,3 @@ +blah = case show 5 of + [] -> _ + c : s -> _ diff --git a/test/golden/EmptyCaseApply.hs b/test/golden/EmptyCaseApply.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseApply.hs @@ -0,0 +1,1 @@ +blah = case show 5 of diff --git a/test/golden/EmptyCaseGADT.expected.hs b/test/golden/EmptyCaseGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseGADT.expected.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + MyInt :: GADT Int + MyBool :: GADT Bool + MyVar :: GADT a + + +test :: GADT Int -> GADT Bool +test x = case x of + MyInt -> _ + MyVar -> _ + diff --git a/test/golden/EmptyCaseGADT.hs b/test/golden/EmptyCaseGADT.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseGADT.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + MyInt :: GADT Int + MyBool :: GADT Bool + MyVar :: GADT a + + +test :: GADT Int -> GADT Bool +test x = case x of + diff --git a/test/golden/EmptyCaseNested.expected.hs b/test/golden/EmptyCaseNested.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseNested.expected.hs @@ -0,0 +1,5 @@ +test = + case (case (Just "") of + Nothing -> _ + Just s -> _) of + True -> _ diff --git a/test/golden/EmptyCaseNested.hs b/test/golden/EmptyCaseNested.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseNested.hs @@ -0,0 +1,3 @@ +test = + case (case (Just "") of) of + True -> _ diff --git a/test/golden/EmptyCaseParens.expected.hs b/test/golden/EmptyCaseParens.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseParens.expected.hs @@ -0,0 +1,3 @@ +test = True && (case True of + False -> _ + True -> _) diff --git a/test/golden/EmptyCaseParens.hs b/test/golden/EmptyCaseParens.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseParens.hs @@ -0,0 +1,1 @@ +test = True && case True of diff --git a/test/golden/EmptyCaseShadow.expected.hs b/test/golden/EmptyCaseShadow.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseShadow.expected.hs @@ -0,0 +1,10 @@ +data Foo = A Int | B Bool | C + +-- Make sure we don't shadow the i and b bindings when we empty case +-- split +foo :: Int -> Bool -> Foo -> () +foo i b x = case x of + A n -> _ + B b' -> _ + C -> _ + diff --git a/test/golden/EmptyCaseShadow.hs b/test/golden/EmptyCaseShadow.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseShadow.hs @@ -0,0 +1,7 @@ +data Foo = A Int | B Bool | C + +-- Make sure we don't shadow the i and b bindings when we empty case +-- split +foo :: Int -> Bool -> Foo -> () +foo i b x = case x of + diff --git a/test/golden/Fgmap.expected.hs b/test/golden/Fgmap.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/Fgmap.expected.hs @@ -0,0 +1,2 @@ +fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b)) +fgmap = fmap . fmap diff --git a/test/golden/Fgmap.hs.expected b/test/golden/Fgmap.hs.expected deleted file mode 100644 --- a/test/golden/Fgmap.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b)) -fgmap = fmap . fmap diff --git a/test/golden/FmapBoth.expected.hs b/test/golden/FmapBoth.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/FmapBoth.expected.hs @@ -0,0 +1,3 @@ +fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b) +fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga) + diff --git a/test/golden/FmapBoth.hs.expected b/test/golden/FmapBoth.hs.expected deleted file mode 100644 --- a/test/golden/FmapBoth.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b) -fmapBoth fab (fa, ga) = (fmap fab fa, fmap fab ga) - diff --git a/test/golden/FmapJoin.expected.hs b/test/golden/FmapJoin.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/FmapJoin.expected.hs @@ -0,0 +1,2 @@ +fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a) +fJoin = fmap (\ m -> m >>= id) diff --git a/test/golden/FmapJoin.hs.expected b/test/golden/FmapJoin.hs.expected deleted file mode 100644 --- a/test/golden/FmapJoin.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a) -fJoin = fmap (\ mma -> mma >>= id) diff --git a/test/golden/FmapJoinInLet.expected.hs b/test/golden/FmapJoinInLet.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/FmapJoinInLet.expected.hs @@ -0,0 +1,4 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a) +fJoin = let f = ( (\ m -> m >>= id) :: m (m a) -> m a) in fmap f diff --git a/test/golden/FmapJoinInLet.hs.expected b/test/golden/FmapJoinInLet.hs.expected deleted file mode 100644 --- a/test/golden/FmapJoinInLet.hs.expected +++ /dev/null @@ -1,4 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables #-} - -fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a) -fJoin = let f = ( (\ mma -> mma >>= id) :: m (m a) -> m a) in fmap f diff --git a/test/golden/GoldenArbitrary.expected.hs b/test/golden/GoldenArbitrary.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenArbitrary.expected.hs @@ -0,0 +1,53 @@ +-- 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 (flip div 2) arbitrary) + <*> scale (flip 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)) + diff --git a/test/golden/GoldenArbitrary.hs.expected b/test/golden/GoldenArbitrary.hs.expected deleted file mode 100644 --- a/test/golden/GoldenArbitrary.hs.expected +++ /dev/null @@ -1,53 +0,0 @@ --- 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 (flip div 2) arbitrary) - <*> scale (flip 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)) - diff --git a/test/golden/GoldenBigTuple.expected.hs b/test/golden/GoldenBigTuple.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenBigTuple.expected.hs @@ -0,0 +1,4 @@ +-- There used to be a bug where we were unable to perform a nested split. The +-- more serious regression test of this is 'AutoTupleSpec'. +bigTuple :: (a, b, c, d) -> (a, b, (c, d)) +bigTuple (a, b, c, d) = (a, b, (c, d)) diff --git a/test/golden/GoldenBigTuple.hs.expected b/test/golden/GoldenBigTuple.hs.expected deleted file mode 100644 --- a/test/golden/GoldenBigTuple.hs.expected +++ /dev/null @@ -1,4 +0,0 @@ --- There used to be a bug where we were unable to perform a nested split. The --- more serious regression test of this is 'AutoTupleSpec'. -bigTuple :: (a, b, c, d) -> (a, b, (c, d)) -bigTuple (a, b, c, d) = (a, b, (c, d)) diff --git a/test/golden/GoldenEitherAuto.expected.hs b/test/golden/GoldenEitherAuto.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenEitherAuto.expected.hs @@ -0,0 +1,3 @@ +either' :: (a -> c) -> (b -> c) -> Either a b -> c +either' fac _ (Left a) = fac a +either' _ fbc (Right b) = fbc b diff --git a/test/golden/GoldenEitherAuto.hs.expected b/test/golden/GoldenEitherAuto.hs.expected deleted file mode 100644 --- a/test/golden/GoldenEitherAuto.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -either' :: (a -> c) -> (b -> c) -> Either a b -> c -either' fac _ (Left a) = fac a -either' _ fbc (Right b) = fbc b diff --git a/test/golden/GoldenEitherHomomorphic.expected.hs b/test/golden/GoldenEitherHomomorphic.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenEitherHomomorphic.expected.hs @@ -0,0 +1,3 @@ +eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c +eitherSplit a (Left fab) = Left (fab a) +eitherSplit a (Right fac) = Right (fac a) diff --git a/test/golden/GoldenEitherHomomorphic.hs.expected b/test/golden/GoldenEitherHomomorphic.hs.expected deleted file mode 100644 --- a/test/golden/GoldenEitherHomomorphic.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -eitherSplit :: a -> Either (a -> b) (a -> c) -> Either b c -eitherSplit a (Left fab) = Left (fab a) -eitherSplit a (Right fac) = Right (fac a) diff --git a/test/golden/GoldenFmapTree.expected.hs b/test/golden/GoldenFmapTree.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenFmapTree.expected.hs @@ -0,0 +1,5 @@ +data Tree a = Leaf a | Branch (Tree a) (Tree a) + +instance Functor Tree where + fmap fab (Leaf a) = Leaf (fab a) + fmap fab (Branch tr' tr_a) = Branch (fmap fab tr') (fmap fab tr_a) diff --git a/test/golden/GoldenFmapTree.hs.expected b/test/golden/GoldenFmapTree.hs.expected deleted file mode 100644 --- a/test/golden/GoldenFmapTree.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -data Tree a = Leaf a | Branch (Tree a) (Tree a) - -instance Functor Tree where - fmap fab (Leaf a) = Leaf (fab a) - fmap fab (Branch ta2 ta3) = Branch (fmap fab ta2) (fmap fab ta3) diff --git a/test/golden/GoldenFoldr.expected.hs b/test/golden/GoldenFoldr.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenFoldr.expected.hs @@ -0,0 +1,3 @@ +foldr2 :: (a -> b -> b) -> b -> [a] -> b +foldr2 _ b [] = b +foldr2 fabb b (a : as') = fabb a (foldr2 fabb b as') diff --git a/test/golden/GoldenFoldr.hs.expected b/test/golden/GoldenFoldr.hs.expected deleted file mode 100644 --- a/test/golden/GoldenFoldr.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -foldr2 :: (a -> b -> b) -> b -> [a] -> b -foldr2 _ b [] = b -foldr2 f_b b (a : l_a4) = f_b a (foldr2 f_b b l_a4) diff --git a/test/golden/GoldenFromMaybe.expected.hs b/test/golden/GoldenFromMaybe.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenFromMaybe.expected.hs @@ -0,0 +1,3 @@ +fromMaybe :: a -> Maybe a -> a +fromMaybe a Nothing = a +fromMaybe _ (Just a') = a' diff --git a/test/golden/GoldenFromMaybe.hs.expected b/test/golden/GoldenFromMaybe.hs.expected deleted file mode 100644 --- a/test/golden/GoldenFromMaybe.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -fromMaybe :: a -> Maybe a -> a -fromMaybe a Nothing = a -fromMaybe _ (Just a2) = a2 diff --git a/test/golden/GoldenGADTAuto.expected.hs b/test/golden/GoldenGADTAuto.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenGADTAuto.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTAuto where +data CtxGADT a where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a + +ctxGADT :: CtxGADT () +ctxGADT = MkCtxGADT () diff --git a/test/golden/GoldenGADTAuto.hs.expected b/test/golden/GoldenGADTAuto.hs.expected deleted file mode 100644 --- a/test/golden/GoldenGADTAuto.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} -module GoldenGADTAuto where -data CtxGADT a where - MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a - -ctxGADT :: CtxGADT () -ctxGADT = MkCtxGADT () diff --git a/test/golden/GoldenGADTDestruct.expected.hs b/test/golden/GoldenGADTDestruct.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenGADTDestruct.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data CtxGADT where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT + +ctxGADT :: CtxGADT -> String +ctxGADT (MkCtxGADT a) = _ diff --git a/test/golden/GoldenGADTDestruct.hs.expected b/test/golden/GoldenGADTDestruct.hs.expected deleted file mode 100644 --- a/test/golden/GoldenGADTDestruct.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE GADTs #-} -module GoldenGADTDestruct where -data CtxGADT where - MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT - -ctxGADT :: CtxGADT -> String -ctxGADT (MkCtxGADT a) = _ diff --git a/test/golden/GoldenGADTDestructCoercion.expected.hs b/test/golden/GoldenGADTDestructCoercion.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenGADTDestructCoercion.expected.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data E a b where + E :: forall a b. (b ~ a, Ord a) => b -> E a [a] + +ctxGADT :: E a b -> String +ctxGADT (E b) = _ diff --git a/test/golden/GoldenGADTDestructCoercion.hs.expected b/test/golden/GoldenGADTDestructCoercion.hs.expected deleted file mode 100644 --- a/test/golden/GoldenGADTDestructCoercion.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE GADTs #-} -module GoldenGADTDestruct where -data E a b where - E :: forall a b. (b ~ a, Ord a) => b -> E a [a] - -ctxGADT :: E a b -> String -ctxGADT (E b) = _ diff --git a/test/golden/GoldenIdTypeFam.expected.hs b/test/golden/GoldenIdTypeFam.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenIdTypeFam.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE TypeFamilies #-} + +type family TyFam +type instance TyFam = Int + +tyblah' :: TyFam -> Int +tyblah' = id diff --git a/test/golden/GoldenIdTypeFam.hs.expected b/test/golden/GoldenIdTypeFam.hs.expected deleted file mode 100644 --- a/test/golden/GoldenIdTypeFam.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -{-# LANGUAGE TypeFamilies #-} - -type family TyFam -type instance TyFam = Int - -tyblah' :: TyFam -> Int -tyblah' = id diff --git a/test/golden/GoldenIdentityFunctor.expected.hs b/test/golden/GoldenIdentityFunctor.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenIdentityFunctor.expected.hs @@ -0,0 +1,3 @@ +data Ident a = Ident a +instance Functor Ident where + fmap fab (Ident a) = Ident (fab a) diff --git a/test/golden/GoldenIdentityFunctor.hs.expected b/test/golden/GoldenIdentityFunctor.hs.expected deleted file mode 100644 --- a/test/golden/GoldenIdentityFunctor.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -data Ident a = Ident a -instance Functor Ident where - fmap fab (Ident a) = Ident (fab a) diff --git a/test/golden/GoldenIntros.expected.hs b/test/golden/GoldenIntros.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenIntros.expected.hs @@ -0,0 +1,2 @@ +blah :: Int -> Bool -> (a -> b) -> String -> Int +blah n b fab s = _ diff --git a/test/golden/GoldenIntros.hs.expected b/test/golden/GoldenIntros.hs.expected deleted file mode 100644 --- a/test/golden/GoldenIntros.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -blah :: Int -> Bool -> (a -> b) -> String -> Int -blah i b fab l_c = _ diff --git a/test/golden/GoldenJoinCont.expected.hs b/test/golden/GoldenJoinCont.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenJoinCont.expected.hs @@ -0,0 +1,4 @@ +type Cont r a = ((a -> r) -> r) + +joinCont :: Cont r (Cont r a) -> Cont r a +joinCont f far = f (\ g -> g far) diff --git a/test/golden/GoldenJoinCont.hs.expected b/test/golden/GoldenJoinCont.hs.expected deleted file mode 100644 --- a/test/golden/GoldenJoinCont.hs.expected +++ /dev/null @@ -1,4 +0,0 @@ -type Cont r a = ((a -> r) -> r) - -joinCont :: Cont r (Cont r a) -> Cont r a -joinCont f_r far = f_r (\ f_r2 -> f_r2 far) diff --git a/test/golden/GoldenListFmap.expected.hs b/test/golden/GoldenListFmap.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenListFmap.expected.hs @@ -0,0 +1,3 @@ +fmapList :: (a -> b) -> [a] -> [b] +fmapList _ [] = [] +fmapList fab (a : as') = fab a : fmapList fab as' diff --git a/test/golden/GoldenListFmap.hs.expected b/test/golden/GoldenListFmap.hs.expected deleted file mode 100644 --- a/test/golden/GoldenListFmap.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -fmapList :: (a -> b) -> [a] -> [b] -fmapList _ [] = [] -fmapList fab (a : l_a3) = fab a : fmapList fab l_a3 diff --git a/test/golden/GoldenNote.expected.hs b/test/golden/GoldenNote.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenNote.expected.hs @@ -0,0 +1,3 @@ +note :: e -> Maybe a -> Either e a +note e Nothing = Left e +note _ (Just a) = Right a diff --git a/test/golden/GoldenNote.hs.expected b/test/golden/GoldenNote.hs.expected deleted file mode 100644 --- a/test/golden/GoldenNote.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -note :: e -> Maybe a -> Either e a -note e Nothing = Left e -note _ (Just a) = Right a diff --git a/test/golden/GoldenPureList.expected.hs b/test/golden/GoldenPureList.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenPureList.expected.hs @@ -0,0 +1,2 @@ +pureList :: a -> [a] +pureList a = a : [] diff --git a/test/golden/GoldenPureList.hs.expected b/test/golden/GoldenPureList.hs.expected deleted file mode 100644 --- a/test/golden/GoldenPureList.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -pureList :: a -> [a] -pureList a = a : [] diff --git a/test/golden/GoldenSafeHead.expected.hs b/test/golden/GoldenSafeHead.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenSafeHead.expected.hs @@ -0,0 +1,3 @@ +safeHead :: [x] -> Maybe x +safeHead [] = Nothing +safeHead (x : _) = Just x diff --git a/test/golden/GoldenSafeHead.hs.expected b/test/golden/GoldenSafeHead.hs.expected deleted file mode 100644 --- a/test/golden/GoldenSafeHead.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -safeHead :: [x] -> Maybe x -safeHead [] = Nothing -safeHead (x : _) = Just x diff --git a/test/golden/GoldenShow.expected.hs b/test/golden/GoldenShow.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenShow.expected.hs @@ -0,0 +1,2 @@ +showMe :: Show a => a -> String +showMe = show diff --git a/test/golden/GoldenShow.hs.expected b/test/golden/GoldenShow.hs.expected deleted file mode 100644 --- a/test/golden/GoldenShow.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -showMe :: Show a => a -> String -showMe = show diff --git a/test/golden/GoldenShowCompose.expected.hs b/test/golden/GoldenShowCompose.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenShowCompose.expected.hs @@ -0,0 +1,2 @@ +showCompose :: Show a => (b -> a) -> b -> String +showCompose fba = show . fba diff --git a/test/golden/GoldenShowCompose.hs.expected b/test/golden/GoldenShowCompose.hs.expected deleted file mode 100644 --- a/test/golden/GoldenShowCompose.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -showCompose :: Show a => (b -> a) -> b -> String -showCompose fba = show . fba diff --git a/test/golden/GoldenShowMapChar.expected.hs b/test/golden/GoldenShowMapChar.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenShowMapChar.expected.hs @@ -0,0 +1,2 @@ +test :: Show a => a -> (String -> b) -> b +test a f = f (show a) diff --git a/test/golden/GoldenShowMapChar.hs.expected b/test/golden/GoldenShowMapChar.hs.expected deleted file mode 100644 --- a/test/golden/GoldenShowMapChar.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -test :: Show a => a -> (String -> b) -> b -test a fl_cb = fl_cb (show a) diff --git a/test/golden/GoldenSuperclass.expected.hs b/test/golden/GoldenSuperclass.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenSuperclass.expected.hs @@ -0,0 +1,8 @@ +class Super a where + super :: a + +class Super a => Sub a + +blah :: Sub a => a +blah = super + diff --git a/test/golden/GoldenSuperclass.hs.expected b/test/golden/GoldenSuperclass.hs.expected deleted file mode 100644 --- a/test/golden/GoldenSuperclass.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -class Super a where - super :: a - -class Super a => Sub a - -blah :: Sub a => a -blah = super - diff --git a/test/golden/GoldenSwap.expected.hs b/test/golden/GoldenSwap.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenSwap.expected.hs @@ -0,0 +1,2 @@ +swap :: (a, b) -> (b, a) +swap (a, b) = (b, a) diff --git a/test/golden/GoldenSwap.hs.expected b/test/golden/GoldenSwap.hs.expected deleted file mode 100644 --- a/test/golden/GoldenSwap.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -swap :: (a, b) -> (b, a) -swap (a, b) = (b, a) diff --git a/test/golden/GoldenSwapMany.expected.hs b/test/golden/GoldenSwapMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/GoldenSwapMany.expected.hs @@ -0,0 +1,2 @@ +swapMany :: (a, b, c, d, e) -> (e, d, c, b, a) +swapMany (a, b, c, d, e) = (e, d, c, b, a) diff --git a/test/golden/GoldenSwapMany.hs.expected b/test/golden/GoldenSwapMany.hs.expected deleted file mode 100644 --- a/test/golden/GoldenSwapMany.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -swapMany :: (a, b, c, d, e) -> (e, d, c, b, a) -swapMany (a, b, c, d, e) = (e, d, c, b, a) diff --git a/test/golden/KnownBigSemigroup.expected.hs b/test/golden/KnownBigSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownBigSemigroup.expected.hs @@ -0,0 +1,9 @@ +import Data.Monoid + +data Big a = Big [Bool] (Sum Int) String (Endo a) Any + +instance Semigroup (Big a) where + (<>) (Big bs sum s en any) (Big bs' sum' str en' any') + = Big + (bs <> bs') (sum <> sum') (s <> str) (en <> en') (any <> any') + diff --git a/test/golden/KnownBigSemigroup.hs.expected b/test/golden/KnownBigSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownBigSemigroup.hs.expected +++ /dev/null @@ -1,9 +0,0 @@ -import Data.Monoid - -data Big a = Big [Bool] (Sum Int) String (Endo a) Any - -instance Semigroup (Big a) where - (<>) (Big l_b7 si8 l_c9 ea10 a11) (Big l_b si l_c ea a) - = Big - (l_b7 <> l_b) (si8 <> si) (l_c9 <> l_c) (ea10 <> ea) (a11 <> a) - diff --git a/test/golden/KnownCounterfactualSemigroup.expected.hs b/test/golden/KnownCounterfactualSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownCounterfactualSemigroup.expected.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE UndecidableInstances #-} + +data Semi = Semi [String] Int + +instance Semigroup Int => Semigroup Semi where + (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) (n <> i) + diff --git a/test/golden/KnownCounterfactualSemigroup.hs.expected b/test/golden/KnownCounterfactualSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownCounterfactualSemigroup.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - -data Semi = Semi [String] Int - -instance Semigroup Int => Semigroup Semi where - (<>) (Semi l_l_c5 i6) (Semi l_l_c i) - = Semi (l_l_c5 <> l_l_c) (i6 <> i) - diff --git a/test/golden/KnownDestructedSemigroup.expected.hs b/test/golden/KnownDestructedSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownDestructedSemigroup.expected.hs @@ -0,0 +1,5 @@ +data Test a = Test [a] + +instance Semigroup (Test a) where + (<>) (Test a) (Test c) = Test (a <> c) + diff --git a/test/golden/KnownDestructedSemigroup.hs.expected b/test/golden/KnownDestructedSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownDestructedSemigroup.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -data Test a = Test [a] - -instance Semigroup (Test a) where - (<>) (Test a) (Test c) = Test (a <> c) - diff --git a/test/golden/KnownMissingMonoid.expected.hs b/test/golden/KnownMissingMonoid.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownMissingMonoid.expected.hs @@ -0,0 +1,8 @@ +data Mono a = Monoid [String] a + +instance Semigroup (Mono a) where + (<>) = undefined + +instance Monoid (Mono a) where + mempty = Monoid mempty _ + diff --git a/test/golden/KnownMissingMonoid.hs.expected b/test/golden/KnownMissingMonoid.hs.expected deleted file mode 100644 --- a/test/golden/KnownMissingMonoid.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -data Mono a = Monoid [String] a - -instance Semigroup (Mono a) where - (<>) = undefined - -instance Monoid (Mono a) where - mempty = Monoid mempty _ - diff --git a/test/golden/KnownMissingSemigroup.expected.hs b/test/golden/KnownMissingSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownMissingSemigroup.expected.hs @@ -0,0 +1,5 @@ +data Semi = Semi [String] Int + +instance Semigroup Semi where + (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) _ + diff --git a/test/golden/KnownMissingSemigroup.hs.expected b/test/golden/KnownMissingSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownMissingSemigroup.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -data Semi = Semi [String] Int - -instance Semigroup Semi where - (<>) (Semi l_l_c4 i5) (Semi l_l_c i) = Semi (l_l_c4 <> l_l_c) _ - diff --git a/test/golden/KnownModuleInstanceSemigroup.expected.hs b/test/golden/KnownModuleInstanceSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownModuleInstanceSemigroup.expected.hs @@ -0,0 +1,12 @@ +data Foo = Foo + +instance Semigroup Foo where + (<>) _ _ = Foo + + +data Bar = Bar Foo Foo + +instance Semigroup Bar where + (<>) (Bar foo foo') (Bar foo2 foo3) + = Bar (foo <> foo2) (foo' <> foo3) + diff --git a/test/golden/KnownModuleInstanceSemigroup.hs.expected b/test/golden/KnownModuleInstanceSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownModuleInstanceSemigroup.hs.expected +++ /dev/null @@ -1,11 +0,0 @@ -data Foo = Foo - -instance Semigroup Foo where - (<>) _ _ = Foo - - -data Bar = Bar Foo Foo - -instance Semigroup Bar where - (<>) (Bar f4 f5) (Bar f f3) = Bar (f4 <> f) (f5 <> f3) - diff --git a/test/golden/KnownMonoid.expected.hs b/test/golden/KnownMonoid.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownMonoid.expected.hs @@ -0,0 +1,8 @@ +data Mono = Monoid [String] + +instance Semigroup Mono where + (<>) = undefined + +instance Monoid Mono where + mempty = Monoid mempty + diff --git a/test/golden/KnownMonoid.hs.expected b/test/golden/KnownMonoid.hs.expected deleted file mode 100644 --- a/test/golden/KnownMonoid.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -data Mono = Monoid [String] - -instance Semigroup Mono where - (<>) = undefined - -instance Monoid Mono where - mempty = Monoid mempty - diff --git a/test/golden/KnownPolyMonoid.expected.hs b/test/golden/KnownPolyMonoid.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownPolyMonoid.expected.hs @@ -0,0 +1,8 @@ +data Mono a = Monoid [String] a + +instance Semigroup (Mono a) where + (<>) = undefined + +instance Monoid a => Monoid (Mono a) where + mempty = Monoid mempty mempty + diff --git a/test/golden/KnownPolyMonoid.hs.expected b/test/golden/KnownPolyMonoid.hs.expected deleted file mode 100644 --- a/test/golden/KnownPolyMonoid.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -data Mono a = Monoid [String] a - -instance Semigroup (Mono a) where - (<>) = undefined - -instance Monoid a => Monoid (Mono a) where - mempty = Monoid mempty mempty - diff --git a/test/golden/KnownThetaSemigroup.expected.hs b/test/golden/KnownThetaSemigroup.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/KnownThetaSemigroup.expected.hs @@ -0,0 +1,5 @@ +data Semi a = Semi a + +instance Semigroup a => Semigroup (Semi a) where + (<>) (Semi a) (Semi a') = Semi (a <> a') + diff --git a/test/golden/KnownThetaSemigroup.hs.expected b/test/golden/KnownThetaSemigroup.hs.expected deleted file mode 100644 --- a/test/golden/KnownThetaSemigroup.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -data Semi a = Semi a - -instance Semigroup a => Semigroup (Semi a) where - (<>) (Semi a4) (Semi a) = Semi (a4 <> a) - diff --git a/test/golden/LayoutBind.expected.hs b/test/golden/LayoutBind.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutBind.expected.hs @@ -0,0 +1,8 @@ +test :: Bool -> IO () +test b = do + putStrLn "hello" + case b of + False -> _ + True -> _ + pure () + diff --git a/test/golden/LayoutBind.hs.expected b/test/golden/LayoutBind.hs.expected deleted file mode 100644 --- a/test/golden/LayoutBind.hs.expected +++ /dev/null @@ -1,8 +0,0 @@ -test :: Bool -> IO () -test b = do - putStrLn "hello" - case b of - False -> _ - True -> _ - pure () - diff --git a/test/golden/LayoutDollarApp.expected.hs b/test/golden/LayoutDollarApp.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutDollarApp.expected.hs @@ -0,0 +1,5 @@ +test :: Bool -> Bool +test b = id $ (case b of + False -> _ + True -> _) + diff --git a/test/golden/LayoutDollarApp.hs.expected b/test/golden/LayoutDollarApp.hs.expected deleted file mode 100644 --- a/test/golden/LayoutDollarApp.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -test :: Bool -> Bool -test b = id $ (case b of - False -> _ - True -> _) - diff --git a/test/golden/LayoutLam.expected.hs b/test/golden/LayoutLam.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutLam.expected.hs @@ -0,0 +1,5 @@ +test :: Bool -> Bool +test = \b -> case b of + False -> _ + True -> _ + diff --git a/test/golden/LayoutLam.hs.expected b/test/golden/LayoutLam.hs.expected deleted file mode 100644 --- a/test/golden/LayoutLam.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -test :: Bool -> Bool -test = \b -> case b of - False -> _ - True -> _ - diff --git a/test/golden/LayoutOpApp.expected.hs b/test/golden/LayoutOpApp.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutOpApp.expected.hs @@ -0,0 +1,4 @@ +test :: Bool -> Bool +test b = True && (case b of + False -> _ + True -> _) diff --git a/test/golden/LayoutOpApp.hs.expected b/test/golden/LayoutOpApp.hs.expected deleted file mode 100644 --- a/test/golden/LayoutOpApp.hs.expected +++ /dev/null @@ -1,4 +0,0 @@ -test :: Bool -> Bool -test b = True && (case b of - False -> _ - True -> _) diff --git a/test/golden/LayoutRec.expected.hs b/test/golden/LayoutRec.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutRec.expected.hs @@ -0,0 +1,5 @@ +data Pair a b = Pair {pa :: a, pb :: b} + +p :: Pair (a -> a) (a -> b -> c -> b) +p = Pair {pa = _, pb = \ a b c -> _} + diff --git a/test/golden/LayoutRec.hs b/test/golden/LayoutRec.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutRec.hs @@ -0,0 +1,5 @@ +data Pair a b = Pair {pa :: a, pb :: b} + +p :: Pair (a -> a) (a -> b -> c -> b) +p = Pair {pa = _, pb = _} + diff --git a/test/golden/LayoutSplitClass.expected.hs b/test/golden/LayoutSplitClass.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitClass.expected.hs @@ -0,0 +1,5 @@ +class Test a where + test :: Bool -> a + test False = _ + test True = _ + diff --git a/test/golden/LayoutSplitClass.hs.expected b/test/golden/LayoutSplitClass.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitClass.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -class Test a where - test :: Bool -> a - test False = _ - test True = _ - diff --git a/test/golden/LayoutSplitGuard.expected.hs b/test/golden/LayoutSplitGuard.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitGuard.expected.hs @@ -0,0 +1,5 @@ +test :: Bool -> Bool -> Bool +test a b + | a = case b of + False -> _ + True -> _ diff --git a/test/golden/LayoutSplitGuard.hs.expected b/test/golden/LayoutSplitGuard.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitGuard.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -test :: Bool -> Bool -> Bool -test a b - | a = (case b of - False -> _ - True -> _) diff --git a/test/golden/LayoutSplitIn.expected.hs b/test/golden/LayoutSplitIn.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitIn.expected.hs @@ -0,0 +1,5 @@ +test :: a +test = + let a = (1,"bbb") + in case a of { (n, s) -> _ } + diff --git a/test/golden/LayoutSplitIn.hs.expected b/test/golden/LayoutSplitIn.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitIn.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -test :: a -test = - let a = (1,"bbb") - in case a of { (i, l_c) -> _ } - diff --git a/test/golden/LayoutSplitLet.expected.hs b/test/golden/LayoutSplitLet.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitLet.expected.hs @@ -0,0 +1,7 @@ +test :: a +test = + let t :: Bool -> a + t False = _ + t True = _ + in _ + diff --git a/test/golden/LayoutSplitLet.hs.expected b/test/golden/LayoutSplitLet.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitLet.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -test :: a -test = - let t :: Bool -> a - t False = _ - t True = _ - in _ - diff --git a/test/golden/LayoutSplitPatSyn.expected.hs b/test/golden/LayoutSplitPatSyn.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitPatSyn.expected.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PatternSynonyms #-} + +pattern JustSingleton :: a -> Maybe [a] +pattern JustSingleton a <- Just [a] + + +test :: Maybe [Bool] -> Maybe Bool +test (JustSingleton False) = _ +test (JustSingleton True) = _ + + diff --git a/test/golden/LayoutSplitPatSyn.hs.expected b/test/golden/LayoutSplitPatSyn.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitPatSyn.hs.expected +++ /dev/null @@ -1,11 +0,0 @@ -{-# LANGUAGE PatternSynonyms #-} - -pattern JustSingleton :: a -> Maybe [a] -pattern JustSingleton a <- Just [a] - - -test :: Maybe [Bool] -> Maybe Bool -test (JustSingleton False) = _ -test (JustSingleton True) = _ - - diff --git a/test/golden/LayoutSplitPattern.expected.hs b/test/golden/LayoutSplitPattern.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitPattern.expected.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE PatternSynonyms #-} + +pattern Blah :: a -> Maybe a +pattern Blah a = Just a + +test :: Maybe Bool -> a +test (Blah False) = _ +test (Blah True) = _ + diff --git a/test/golden/LayoutSplitPattern.hs.expected b/test/golden/LayoutSplitPattern.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitPattern.hs.expected +++ /dev/null @@ -1,9 +0,0 @@ -{-# LANGUAGE PatternSynonyms #-} - -pattern Blah :: a -> Maybe a -pattern Blah a = Just a - -test :: Maybe Bool -> a -test (Blah False) = _ -test (Blah True) = _ - diff --git a/test/golden/LayoutSplitViewPat.expected.hs b/test/golden/LayoutSplitViewPat.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitViewPat.expected.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE ViewPatterns #-} + +splitLookup :: [(Int, String)] -> String +splitLookup (lookup 5 -> Nothing) = _ +splitLookup (lookup 5 -> (Just s)) = _ + diff --git a/test/golden/LayoutSplitViewPat.hs.expected b/test/golden/LayoutSplitViewPat.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitViewPat.hs.expected +++ /dev/null @@ -1,6 +0,0 @@ -{-# LANGUAGE ViewPatterns #-} - -splitLookup :: [(Int, String)] -> String -splitLookup (lookup 5 -> Nothing) = _ -splitLookup (lookup 5 -> (Just l_c)) = _ - diff --git a/test/golden/LayoutSplitWhere.expected.hs b/test/golden/LayoutSplitWhere.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutSplitWhere.expected.hs @@ -0,0 +1,14 @@ +data A = A | B | C + +some :: A -> IO () +some a = do + foo + bar a + where + foo = putStrLn "Hi" + + bar :: A -> IO () + bar A = _ + bar B = _ + bar C = _ + diff --git a/test/golden/LayoutSplitWhere.hs.expected b/test/golden/LayoutSplitWhere.hs.expected deleted file mode 100644 --- a/test/golden/LayoutSplitWhere.hs.expected +++ /dev/null @@ -1,14 +0,0 @@ -data A = A | B | C - -some :: A -> IO () -some a = do - foo - bar a - where - foo = putStrLn "Hi" - - bar :: A -> IO () - bar A = _ - bar B = _ - bar C = _ - diff --git a/test/golden/MessageCantUnify.hs b/test/golden/MessageCantUnify.hs new file mode 100644 --- /dev/null +++ b/test/golden/MessageCantUnify.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE DataKinds, GADTs #-} + +data Z ab where + Z :: (a -> b) -> Z '(a, b) + +test :: Z ab +test = _ + diff --git a/test/golden/MetaBegin.expected.hs b/test/golden/MetaBegin.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBegin.expected.hs @@ -0,0 +1,1 @@ +foo = [wingman||] diff --git a/test/golden/MetaBegin.hs b/test/golden/MetaBegin.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBegin.hs @@ -0,0 +1,1 @@ +foo = _ diff --git a/test/golden/MetaBindAll.expected.hs b/test/golden/MetaBindAll.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBindAll.expected.hs @@ -0,0 +1,2 @@ +foo :: a -> (a, a) +foo a = (a, a) diff --git a/test/golden/MetaBindAll.hs b/test/golden/MetaBindAll.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBindAll.hs @@ -0,0 +1,2 @@ +foo :: a -> (a, a) +foo a = [wingman| split; assumption |] diff --git a/test/golden/MetaBindOne.expected.hs b/test/golden/MetaBindOne.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBindOne.expected.hs @@ -0,0 +1,2 @@ +foo :: a -> (a, a) +foo a = (a, _) diff --git a/test/golden/MetaBindOne.hs b/test/golden/MetaBindOne.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBindOne.hs @@ -0,0 +1,2 @@ +foo :: a -> (a, a) +foo a = [wingman| split, assumption |] diff --git a/test/golden/MetaCataCollapse.expected.hs b/test/golden/MetaCataCollapse.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataCollapse.expected.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE TypeOperators #-} + +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f, Yo g) => Yo (f :*: g) where + yo (fx :*: gx) + = let + fx_c = yo fx + gx_c = yo gx + in _ fx_c gx_c + diff --git a/test/golden/MetaCataCollapse.hs b/test/golden/MetaCataCollapse.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataCollapse.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE TypeOperators #-} + +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f, Yo g) => Yo (f :*: g) where + yo = [wingman| intros x, cata x, collapse |] + diff --git a/test/golden/MetaCataCollapseUnary.expected.hs b/test/golden/MetaCataCollapseUnary.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataCollapseUnary.expected.hs @@ -0,0 +1,8 @@ +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f) => Yo (M1 _1 _2 f) where + yo (M1 fx) = yo fx + diff --git a/test/golden/MetaCataCollapseUnary.hs b/test/golden/MetaCataCollapseUnary.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataCollapseUnary.hs @@ -0,0 +1,8 @@ +import GHC.Generics + +class Yo f where + yo :: f x -> Int + +instance (Yo f) => Yo (M1 _1 _2 f) where + yo = [wingman| intros x, cata x, collapse |] + diff --git a/test/golden/MetaChoice.expected.hs b/test/golden/MetaChoice.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaChoice.expected.hs @@ -0,0 +1,2 @@ +reassoc :: (a, (b, c)) -> ((a, b), c) +reassoc (a, (b, c)) = ((a, b), c) diff --git a/test/golden/MetaChoice.hs b/test/golden/MetaChoice.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaChoice.hs @@ -0,0 +1,2 @@ +reassoc :: (a, (b, c)) -> ((a, b), c) +reassoc (a, (b, c)) = [wingman| split; split | assume c; assume a | assume b |] diff --git a/test/golden/MetaMaybeAp.expected.hs b/test/golden/MetaMaybeAp.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaMaybeAp.expected.hs @@ -0,0 +1,5 @@ +maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b +maybeAp Nothing Nothing = Nothing +maybeAp Nothing (Just _) = Nothing +maybeAp (Just _) Nothing = Nothing +maybeAp (Just fab) (Just a) = Just (fab a) diff --git a/test/golden/MetaMaybeAp.hs b/test/golden/MetaMaybeAp.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaMaybeAp.hs @@ -0,0 +1,11 @@ +maybeAp :: Maybe (a -> b) -> Maybe a -> Maybe b +maybeAp = [wingman| + intros, + destruct_all, + obvious, + obvious, + obvious, + ctor Just, + application, + assumption + |] diff --git a/test/golden/MetaTry.expected.hs b/test/golden/MetaTry.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaTry.expected.hs @@ -0,0 +1,2 @@ +foo :: a -> (b, a) +foo a = (_, a) diff --git a/test/golden/MetaTry.hs b/test/golden/MetaTry.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaTry.hs @@ -0,0 +1,2 @@ +foo :: a -> (b, a) +foo a = [wingman| split; try assumption |] diff --git a/test/golden/MetaUseImport.expected.hs b/test/golden/MetaUseImport.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseImport.expected.hs @@ -0,0 +1,6 @@ +import Data.Char + + +result :: Char -> Bool +result = isAlpha + diff --git a/test/golden/MetaUseImport.hs b/test/golden/MetaUseImport.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseImport.hs @@ -0,0 +1,6 @@ +import Data.Char + + +result :: Char -> Bool +result = [wingman| intro c, use isAlpha, assume c |] + diff --git a/test/golden/MetaUseLocal.expected.hs b/test/golden/MetaUseLocal.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseLocal.expected.hs @@ -0,0 +1,7 @@ +test :: Int +test = 0 + + +resolve :: Int +resolve = test + diff --git a/test/golden/MetaUseLocal.hs b/test/golden/MetaUseLocal.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseLocal.hs @@ -0,0 +1,7 @@ +test :: Int +test = 0 + + +resolve :: Int +resolve = [wingman| use test |] + diff --git a/test/golden/MetaUseMethod.expected.hs b/test/golden/MetaUseMethod.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseMethod.expected.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses #-} + +class Test where + test :: Int + +instance Test where + test = 10 + + +resolve :: Int +resolve = test + diff --git a/test/golden/MetaUseMethod.hs b/test/golden/MetaUseMethod.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseMethod.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE MultiParamTypeClasses #-} + +class Test where + test :: Int + +instance Test where + test = 10 + + +resolve :: Int +resolve = [wingman| use test |] + diff --git a/test/golden/NewtypeRecord.expected.hs b/test/golden/NewtypeRecord.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/NewtypeRecord.expected.hs @@ -0,0 +1,7 @@ +newtype MyRecord a = Record + { field1 :: a + } + +blah :: (a -> Int) -> a -> MyRecord a +blah _ = Record + diff --git a/test/golden/NewtypeRecord.hs.expected b/test/golden/NewtypeRecord.hs.expected deleted file mode 100644 --- a/test/golden/NewtypeRecord.hs.expected +++ /dev/null @@ -1,7 +0,0 @@ -newtype MyRecord a = Record - { field1 :: a - } - -blah :: (a -> Int) -> a -> MyRecord a -blah _ = Record - diff --git a/test/golden/PunGADT.expected.hs b/test/golden/PunGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunGADT.expected.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + GADT :: + { blah :: Int + , bar :: a + } -> GADT a + + +split :: GADT a -> a +split GADT {blah, bar} = _ + diff --git a/test/golden/PunGADT.hs b/test/golden/PunGADT.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunGADT.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + GADT :: + { blah :: Int + , bar :: a + } -> GADT a + + +split :: GADT a -> a +split x = _ + diff --git a/test/golden/PunMany.expected.hs b/test/golden/PunMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunMany.expected.hs @@ -0,0 +1,8 @@ +data Many + = Hello { world :: String } + | Goodbye { a :: Int, b :: Bool, c :: Many } + +test :: Many -> Many +test Hello {world} = _ +test Goodbye {a, b, c} = _ + diff --git a/test/golden/PunMany.hs b/test/golden/PunMany.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunMany.hs @@ -0,0 +1,7 @@ +data Many + = Hello { world :: String } + | Goodbye { a :: Int, b :: Bool, c :: Many } + +test :: Many -> Many +test x = _ + diff --git a/test/golden/PunManyGADT.expected.hs b/test/golden/PunManyGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunManyGADT.expected.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + GADT :: + { blah :: Int + , bar :: a + } -> GADT a + Bar :: + { zoo :: Bool + , baxter :: a + , another :: a + } -> GADT Bool + Baz :: GADT Int + + +split :: GADT Bool -> a +split GADT {blah, bar} = _ +split Bar {zoo, baxter, another} = _ + diff --git a/test/golden/PunManyGADT.hs b/test/golden/PunManyGADT.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunManyGADT.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + GADT :: + { blah :: Int + , bar :: a + } -> GADT a + Bar :: + { zoo :: Bool + , baxter :: a + , another :: a + } -> GADT Bool + Baz :: GADT Int + + +split :: GADT Bool -> a +split x = _ + diff --git a/test/golden/PunShadowing.expected.hs b/test/golden/PunShadowing.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunShadowing.expected.hs @@ -0,0 +1,5 @@ +data Bar = Bar { ax :: Int, bax :: Bool } + +bar :: () -> Bar -> Int +bar ax Bar {ax = n, bax} = _ + diff --git a/test/golden/PunShadowing.hs b/test/golden/PunShadowing.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunShadowing.hs @@ -0,0 +1,5 @@ +data Bar = Bar { ax :: Int, bax :: Bool } + +bar :: () -> Bar -> Int +bar ax x = _ + diff --git a/test/golden/PunSimple.expected.hs b/test/golden/PunSimple.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunSimple.expected.hs @@ -0,0 +1,5 @@ +data Bar = Bar { ax :: Int, bax :: Bool } + +bar :: Bar -> Int +bar Bar {ax, bax} = _ + diff --git a/test/golden/PunSimple.hs b/test/golden/PunSimple.hs new file mode 100644 --- /dev/null +++ b/test/golden/PunSimple.hs @@ -0,0 +1,5 @@ +data Bar = Bar { ax :: Int, bax :: Bool } + +bar :: Bar -> Int +bar x = _ + diff --git a/test/golden/RecordCon.expected.hs b/test/golden/RecordCon.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RecordCon.expected.hs @@ -0,0 +1,9 @@ +data MyRecord a = Record + { field1 :: a + , field2 :: Int + } + +blah :: (a -> Int) -> a -> MyRecord a +blah f a = Record {field1 = a, field2 = f a} + + diff --git a/test/golden/RecordCon.hs.expected b/test/golden/RecordCon.hs.expected deleted file mode 100644 --- a/test/golden/RecordCon.hs.expected +++ /dev/null @@ -1,9 +0,0 @@ -data MyRecord a = Record - { field1 :: a - , field2 :: Int - } - -blah :: (a -> Int) -> a -> MyRecord a -blah fai a = Record {field1 = a, field2 = fai a} - - diff --git a/test/golden/RefineCon.expected.hs b/test/golden/RefineCon.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineCon.expected.hs @@ -0,0 +1,3 @@ +test :: ((), (b, c), d) +test = (_, _, _) + diff --git a/test/golden/RefineCon.hs.expected b/test/golden/RefineCon.hs.expected deleted file mode 100644 --- a/test/golden/RefineCon.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -test :: ((), (b, c), d) -test = (_, _, _) - diff --git a/test/golden/RefineGADT.expected.hs b/test/golden/RefineGADT.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineGADT.expected.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE GADTs #-} + +data GADT a where + One :: (b -> Int) -> GADT Int + Two :: GADT Bool + +test :: z -> GADT Int +test z = One _ + diff --git a/test/golden/RefineGADT.hs b/test/golden/RefineGADT.hs --- a/test/golden/RefineGADT.hs +++ b/test/golden/RefineGADT.hs @@ -5,5 +5,5 @@ Two :: GADT Bool test :: z -> GADT Int -test = _ +test z = _ diff --git a/test/golden/RefineGADT.hs.expected b/test/golden/RefineGADT.hs.expected deleted file mode 100644 --- a/test/golden/RefineGADT.hs.expected +++ /dev/null @@ -1,9 +0,0 @@ -{-# LANGUAGE GADTs #-} - -data GADT a where - One :: (b -> Int) -> GADT Int - Two :: GADT Bool - -test :: z -> GADT Int -test z = One (\ b -> _) - diff --git a/test/golden/RefineIntro.expected.hs b/test/golden/RefineIntro.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineIntro.expected.hs @@ -0,0 +1,2 @@ +test :: a -> Either a b +test a = _ diff --git a/test/golden/RefineIntro.hs.expected b/test/golden/RefineIntro.hs.expected deleted file mode 100644 --- a/test/golden/RefineIntro.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -test :: a -> Either a b -test a = _ diff --git a/test/golden/RefineReader.expected.hs b/test/golden/RefineReader.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/RefineReader.expected.hs @@ -0,0 +1,5 @@ +newtype Reader r a = Reader (r -> a) + +test :: b -> Reader r a +test b = Reader _ + diff --git a/test/golden/RefineReader.hs b/test/golden/RefineReader.hs --- a/test/golden/RefineReader.hs +++ b/test/golden/RefineReader.hs @@ -1,5 +1,5 @@ newtype Reader r a = Reader (r -> a) test :: b -> Reader r a -test = _ +test b = _ diff --git a/test/golden/RefineReader.hs.expected b/test/golden/RefineReader.hs.expected deleted file mode 100644 --- a/test/golden/RefineReader.hs.expected +++ /dev/null @@ -1,5 +0,0 @@ -newtype Reader r a = Reader (r -> a) - -test :: b -> Reader r a -test b = Reader (\ r -> _) - diff --git a/test/golden/SplitPattern.expected.hs b/test/golden/SplitPattern.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/SplitPattern.expected.hs @@ -0,0 +1,12 @@ +data ADT = One | Two Int | Three | Four Bool ADT | Five + +case_split :: ADT -> Int +case_split One = _ +case_split (Two i) = _ +case_split Three = _ +case_split (Four b One) = _ +case_split (Four b (Two n)) = _ +case_split (Four b Three) = _ +case_split (Four b (Four b' adt)) = _ +case_split (Four b Five) = _ +case_split Five = _ diff --git a/test/golden/SplitPattern.hs.expected b/test/golden/SplitPattern.hs.expected deleted file mode 100644 --- a/test/golden/SplitPattern.hs.expected +++ /dev/null @@ -1,12 +0,0 @@ -data ADT = One | Two Int | Three | Four Bool ADT | Five - -case_split :: ADT -> Int -case_split One = _ -case_split (Two i) = _ -case_split Three = _ -case_split (Four b One) = _ -case_split (Four b (Two i)) = _ -case_split (Four b Three) = _ -case_split (Four b (Four b3 a4)) = _ -case_split (Four b Five) = _ -case_split Five = _ diff --git a/test/golden/UseConLeft.expected.hs b/test/golden/UseConLeft.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/UseConLeft.expected.hs @@ -0,0 +1,3 @@ +test :: Either a b +test = Left _ + diff --git a/test/golden/UseConLeft.hs.expected b/test/golden/UseConLeft.hs.expected deleted file mode 100644 --- a/test/golden/UseConLeft.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -test :: Either a b -test = Left _ - diff --git a/test/golden/UseConPair.expected.hs b/test/golden/UseConPair.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/UseConPair.expected.hs @@ -0,0 +1,2 @@ +test :: (a, b) +test = (_, _) diff --git a/test/golden/UseConPair.hs.expected b/test/golden/UseConPair.hs.expected deleted file mode 100644 --- a/test/golden/UseConPair.hs.expected +++ /dev/null @@ -1,2 +0,0 @@ -test :: (a, b) -test = (_, _) diff --git a/test/golden/UseConRight.expected.hs b/test/golden/UseConRight.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/UseConRight.expected.hs @@ -0,0 +1,3 @@ +test :: Either a b +test = Right _ + diff --git a/test/golden/UseConRight.hs.expected b/test/golden/UseConRight.hs.expected deleted file mode 100644 --- a/test/golden/UseConRight.hs.expected +++ /dev/null @@ -1,3 +0,0 @@ -test :: Either a b -test = Right _ -