diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,6 +34,17 @@ [hls]: https://github.com/haskell/haskell-language-server/releases +## Usage + +When enabled, Wingman for Haskell will remove HLS support for hole-fit code +actions. These code actions are provided by GHC and make typechecking extremely +slow in the presence of typed holes. Because Wingman relies so heavily on typed +holes, these features are in great tension. + +The solution: we just remove the hole-fit actions. If you'd prefer to use these +actions, you can get them back by compiling HLS without the Wingman plugin. + + ## Editor Configuration ### Enabling Jump to Hole @@ -97,6 +108,33 @@ call CocAction('codeAction', a:type, ['refactor.wingman.useConstructor']) call GotoNextHole() endfunction +``` + +### Emacs + +When using Emacs, wingman actions should be available out-of-the-box and +show up e.g. when using `M-x helm-lsp-code-actions RET` provided by +[helm-lsp](https://github.com/emacs-lsp/helm-lsp) or as popups via +[lsp-ui-sideline](https://emacs-lsp.github.io/lsp-ui/#lsp-ui-sideline). + +Additionally, if you want to bind wingman actions directly to specific +keybindings or use them from Emacs Lisp, you can do so like this: + +``` emacs-lisp +;; will define elisp functions for the given lsp code actions, prefixing the +;; given function names with "lsp" +(lsp-make-interactive-code-action wingman-fill-hole "refactor.wingman.fillHole") +(lsp-make-interactive-code-action wingman-case-split "refactor.wingman.caseSplit") +(lsp-make-interactive-code-action wingman-refine "refactor.wingman.refine") +(lsp-make-interactive-code-action wingman-split-func-args "refactor.wingman.spltFuncArgs") +(lsp-make-interactive-code-action wingman-use-constructor "refactor.wingman.useConstructor") + +;; example key bindings +(define-key haskell-mode-map (kbd "C-c d") #'lsp-wingman-case-split) +(define-key haskell-mode-map (kbd "C-c n") #'lsp-wingman-fill-hole) +(define-key haskell-mode-map (kbd "C-c r") #'lsp-wingman-refine) +(define-key haskell-mode-map (kbd "C-c c") #'lsp-wingman-use-constructor) +(define-key haskell-mode-map (kbd "C-c a") #'lsp-wingman-split-func-args) ``` ### Other Editors diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal --- a/hls-tactics-plugin.cabal +++ b/hls-tactics-plugin.cabal @@ -1,9 +1,10 @@ cabal-version: 2.4 category: Development name: hls-tactics-plugin -version: 1.2.0.0 +version: 1.3.0.0 synopsis: Wingman plugin for Haskell Language Server -description: Please see README.md +description: + Please see the README on GitHub at author: Sandy Maguire, Reed Mullanix maintainer: sandy@sandymaguire.me copyright: Sandy Maguire, Reed Mullanix @@ -69,25 +70,25 @@ , containers , deepseq , directory - , extra + , extra >=1.7.8 , filepath , fingertree , generic-lens , ghc , ghc-boot-th , ghc-exactprint - , ghc-source-gen - , ghcide ^>=1.4 + , ghc-source-gen ^>=0.4.1 + , ghcide ^>=1.4.1 , hls-graph - , hls-plugin-api ^>=1.1 + , hls-plugin-api >=1.1 && <1.3 , hyphenation , lens , lsp - , megaparsec ^>=9 + , megaparsec >=8 && <10 , mtl , parser-combinators , prettyprinter - , refinery ^>=0.3 + , refinery ^>=0.4 , retrie >=0.1.1.0 , syb , text @@ -153,7 +154,7 @@ , ghcide , hls-plugin-api , hls-tactics-plugin - , hls-test-utils ^>=1.0 + , hls-test-utils >=1.0 && <1.2 , 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 @@ -5,10 +5,9 @@ import Control.Monad.State (gets) import qualified Data.Set as S import Refinery.Tactic -import Wingman.Context import Wingman.Judgements import Wingman.KnownStrategies -import Wingman.Machinery (tracing) +import Wingman.Machinery (tracing, getCurrentDefinitions) import Wingman.Tactics import Wingman.Types diff --git a/src/Wingman/CaseSplit.hs b/src/Wingman/CaseSplit.hs --- a/src/Wingman/CaseSplit.hs +++ b/src/Wingman/CaseSplit.hs @@ -11,7 +11,7 @@ import qualified Data.Set as S import Development.IDE.GHC.Compat import GHC.Exts (IsString (fromString)) -import GHC.SourceGen (funBinds, match, wildP) +import GHC.SourceGen (funBindsWithFixity, match, wildP) import OccName import Wingman.GHC import Wingman.Types @@ -30,10 +30,14 @@ -- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by -- splitting it into multiple matches: one for each alternative of the case. agdaSplit :: AgdaMatch -> [AgdaMatch] -agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do - (pat, body) <- matches - -- TODO(sandy): use an at pattern if necessary - pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body +agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) + -- Ensure the thing we're destructing is actually a pattern that's been + -- bound. + | containsVar var pats + = do + (pat, body) <- matches + -- TODO(sandy): use an at pattern if necessary + pure $ AgdaMatch (rewriteVarPat var pat pats) $ unLoc body agdaSplit x = [x] @@ -54,6 +58,19 @@ ------------------------------------------------------------------------------ +-- | Determine whether the given 'RdrName' exists as a 'VarPat' inside of @a@. +containsVar :: Data a => RdrName -> a -> Bool +containsVar name = everything (||) $ + mkQ False (\case + VarPat _ (L _ var) -> eqRdrName name var + (_ :: Pat GhcPs) -> False + ) + `extQ` \case + HsRecField lbl _ True -> eqRdrName name $ unLoc $ rdrNameFieldOcc $ unLoc lbl + (_ :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> False + + +------------------------------------------------------------------------------ -- | Replace a 'VarPat' with the given @'Pat' GhcPs@. rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a rewriteVarPat name rep = everywhere $ @@ -68,16 +85,19 @@ (x :: HsRecField' (FieldOcc GhcPs) (PatCompat GhcPs)) -> x - ------------------------------------------------------------------------------ -- | Construct an 'HsDecl' from a set of 'AgdaMatch'es. splitToDecl - :: OccName -- ^ The name of the function + :: Maybe LexicalFixity + -> OccName -- ^ The name of the function -> [AgdaMatch] -> LHsDecl GhcPs -splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do - AgdaMatch pats body <- ams - pure $ match pats body +splitToDecl fixity name ams = do + traceX "fixity" fixity $ + noLoc $ + funBindsWithFixity fixity (fromString . occNameString . occName $ name) $ do + AgdaMatch pats body <- ams + pure $ match pats body ------------------------------------------------------------------------------ diff --git a/src/Wingman/CodeGen.hs b/src/Wingman/CodeGen.hs --- a/src/Wingman/CodeGen.hs +++ b/src/Wingman/CodeGen.hs @@ -33,6 +33,7 @@ import OccName (occName) import PatSyn import Type hiding (Var) +import TysPrim (alphaTy) import Wingman.CodeGen.Utils import Wingman.GHC import Wingman.Judgements @@ -58,7 +59,7 @@ let hy = jEntireHypothesis jdg g = jGoal jdg case tacticsGetDataCons $ unCType t of - Nothing -> throwError $ GoalMismatch "destruct" g + Nothing -> cut -- throwError $ GoalMismatch "destruct" g Just (dcs, apps) -> fmap unzipTrace $ for dcs $ \dc -> do let con = RealDataCon dc @@ -67,8 +68,6 @@ -- #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 @@ -79,7 +78,7 @@ let hy' = patternHypothesis scrut con jdg $ zip names' $ coerce args - j = fmap (CType . substTyAddInScope subst . unCType) + j = withNewCoercions (evidenceToCoercions ev) $ introduce ctx hy' $ introduce ctx method_hy $ withNewGoal g jdg @@ -215,7 +214,7 @@ destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule destruct' use_field_puns f hi jdg = do - when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic + when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic let term = hi_name hi ext <- destructMatches @@ -235,13 +234,13 @@ -- resulting matches. destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule destructLambdaCase' use_field_puns f jdg = do - when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic + when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic let g = jGoal jdg case splitFunTy_maybe (unCType g) of Just (arg, _) | isAlgType arg -> fmap (fmap noLoc lambdaCase) <$> destructMatches use_field_puns f Nothing (CType arg) jdg - _ -> throwError $ GoalMismatch "destructLambdaCase'" g + _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g ------------------------------------------------------------------------------ @@ -268,7 +267,7 @@ -- -- Fortunately, this isn't an issue in practice, since 'PatSyn's are -- never in the hypothesis. - throwError $ TacticPanic "Can't build Pattern constructors yet" + cut -- throwError $ TacticPanic "Can't build Pattern constructors yet" ext <- fmap unzipTrace $ traverse ( \(arg, n) -> @@ -309,7 +308,8 @@ let g = jGoal jdg terms <- fmap sequenceA $ for hy $ \hi -> do let name = rename $ hi_name hi - res <- tacticToRule jdg $ solve hi + let generalized_let_ty = CType alphaTy + res <- tacticToRule (withNewGoal generalized_let_ty 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 diff --git a/src/Wingman/Context.hs b/src/Wingman/Context.hs --- a/src/Wingman/Context.hs +++ b/src/Wingman/Context.hs @@ -8,7 +8,7 @@ import Data.Maybe (fromMaybe, isJust, mapMaybe) import qualified Data.Set as S import Development.IDE.GHC.Compat -import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env) +import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env, extractModule) import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun) import OccName import TcRnTypes @@ -23,11 +23,11 @@ :: Config -> [(OccName, CType)] -> TcGblEnv + -> HscEnv -> ExternalPackageState - -> KnownThings -> [Evidence] -> Context -mkContext cfg locals tcg eps kt ev = fix $ \ctx -> +mkContext cfg locals tcg hscenv eps ev = fix $ \ctx -> Context { ctxDefiningFuncs = fmap (second $ coerce $ normalizeType ctx) locals @@ -46,8 +46,10 @@ (eps_inst_env eps) (tcg_inst_env tcg) (tcVisibleOrphanMods tcg) - , ctxKnownThings = kt , ctxTheta = evidenceToThetaType ev + , ctx_hscEnv = hscenv + , ctx_occEnv = tcg_rdr_env tcg + , ctx_module = extractModule tcg } @@ -69,24 +71,6 @@ ABE _ poly _ _ _ -> pure poly _ -> [] getFunBindId _ = [] - - -getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] -getCurrentDefinitions = asks ctxDefiningFuncs - - ------------------------------------------------------------------------------- --- | Extract something from 'KnownThings'. -getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a -getKnownThing f = asks $ f . ctxKnownThings - - ------------------------------------------------------------------------------- --- | Like 'getInstance', but uses a class from the 'KnownThings'. -getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType)) -getKnownInstance f tys = do - cls <- getKnownThing f - getInstance cls tys ------------------------------------------------------------------------------ diff --git a/src/Wingman/EmptyCase.hs b/src/Wingman/EmptyCase.hs --- a/src/Wingman/EmptyCase.hs +++ b/src/Wingman/EmptyCase.hs @@ -59,7 +59,6 @@ | 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 @@ -94,6 +93,13 @@ codeLensProvider _ _ _ = pure $ Right $ List [] +scrutinzedType :: EmptyCaseSort Type -> Maybe Type +scrutinzedType (EmptyCase ty) = pure ty +scrutinzedType (EmptyLamCase ty) = + case tacticsSplitFunTy ty of + (_, _, tys, _) -> listToMaybe tys + + ------------------------------------------------------------------------------ -- | The description for the empty case lens. mkEmptyCaseLensDesc :: Type -> T.Text @@ -120,6 +126,8 @@ hoistGraft (runExcept . runExceptString) $ graftExprWithM ss $ \case L span (HsCase ext scrut mg@_) -> do pure $ Just $ L span $ HsCase ext scrut $ mg { mg_alts = l } + L span (HsLamCase ext mg@_) -> do + pure $ Just $ L span $ HsLamCase ext $ mg { mg_alts = l } (_ :: LHsExpr GhcPs) -> pure Nothing @@ -142,19 +150,30 @@ 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 + fmap catMaybes $ for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do + ty <- MaybeT + . fmap (scrutinzedType <=< sequence) + . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg') + $ scrutinee + case null $ tacticsGetDataCons ty of + True -> pure empty + False -> + case ss of + RealSrcSpan r -> do + rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r + pure $ Just (rss', ty) + UnhelpfulSpan _ -> empty +data EmptyCaseSort a + = EmptyCase a + | EmptyLamCase a + deriving (Eq, Ord, Show, Functor, Foldable, Traversable) ------------------------------------------------------------------------------ -- | Get the 'SrcSpan' and scrutinee of every empty case. -emptyCaseQ :: GenericQ [(SrcSpan, HsExpr GhcTc)] +emptyCaseQ :: GenericQ [(SrcSpan, EmptyCaseSort (HsExpr GhcTc))] emptyCaseQ = everything (<>) $ mkQ mempty $ \case - L new_span (Case scrutinee []) -> pure (new_span, scrutinee) + L new_span (Case scrutinee []) -> pure (new_span, EmptyCase scrutinee) + L new_span (expr@(LamCase [])) -> pure (new_span, EmptyLamCase expr) (_ :: LHsExpr GhcTc) -> mempty diff --git a/src/Wingman/GHC.hs b/src/Wingman/GHC.hs --- a/src/Wingman/GHC.hs +++ b/src/Wingman/GHC.hs @@ -4,11 +4,12 @@ module Wingman.GHC where import Bag (bagToList) +import Class (classTyVars) import ConLike -import Control.Applicative (empty) import Control.Monad.State import Control.Monad.Trans.Maybe (MaybeT(..)) import CoreUtils (exprType) +import Data.Bool (bool) import Data.Function (on) import Data.Functor ((<&>)) import Data.List (isPrefixOf) @@ -18,8 +19,6 @@ import qualified Data.Set as S import Data.Traversable import DataCon -import Development.IDE (HscEnvEq (hscEnv)) -import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat hiding (exprType) import DsExpr (dsExpr) import DsMonad (initDs) @@ -27,15 +26,17 @@ import FamInstEnv (normaliseType) import GHC.SourceGen (lambda) import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT) -import GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal)) +import GhcPlugins (Role (Nominal)) import OccName import TcRnMonad import TcType import TyCoRep import Type import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon) +import Unify import Unique import Var +import Wingman.StaticPlugin (pattern MetaprogramSyntax) import Wingman.Types @@ -90,11 +91,15 @@ ------------------------------------------------------------------------------ -- | Get the data cons of a type, if it has any. tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type]) -tacticsGetDataCons ty | Just _ <- algebraicTyCon ty = - splitTyConApp_maybe ty <&> \(tc, apps) -> - ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc - , apps - ) +tacticsGetDataCons ty + | Just (_, ty') <- tcSplitForAllTy_maybe ty + = tacticsGetDataCons ty' +tacticsGetDataCons ty + | Just _ <- algebraicTyCon ty + = splitTyConApp_maybe ty <&> \(tc, apps) -> + ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc + , apps + ) tacticsGetDataCons _ = Nothing ------------------------------------------------------------------------------ @@ -113,7 +118,7 @@ case M.lookup tv reps of Just tv' -> tv' Nothing -> tv - ) t + ) $ snd $ tcSplitForAllTys t ------------------------------------------------------------------------------ @@ -131,6 +136,9 @@ ------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon +algebraicTyCon ty + | Just (_, ty') <- tcSplitForAllTy_maybe ty + = algebraicTyCon ty' algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) | tycon == intTyCon = Nothing | tycon == floatTyCon = Nothing @@ -171,6 +179,7 @@ containsHole x = not $ null $ listify ( \case ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name + MetaprogramSyntax _ -> True _ -> False ) x @@ -252,7 +261,14 @@ HsCase _ (L _ scrutinee) (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}) +------------------------------------------------------------------------------ +-- | Like 'Case', but for lambda cases. +pattern LamCase :: PatCompattable p => [(Pat p, LHsExpr p)] -> HsExpr p +pattern LamCase matches <- + HsLamCase _ + (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)}) + ------------------------------------------------------------------------------ -- | Can ths type be lambda-cased? -- @@ -323,40 +339,6 @@ unXPat pat = pat ------------------------------------------------------------------------------- --- | Build a 'KnownThings'. -knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings -knownThings tcg hscenv= do - let cls = knownClass tcg hscenv - KnownThings - <$> cls (mkClsOcc "Semigroup") - <*> cls (mkClsOcc "Monoid") - - ------------------------------------------------------------------------------- --- | Like 'knownThing' but specialized to classes. -knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class -knownClass = knownThing $ \case - ATyCon tc -> tyConClass_maybe tc - _ -> Nothing - - ------------------------------------------------------------------------------- --- | Helper function for defining 'knownThings'. -knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a -knownThing f tcg hscenv occ = do - let modul = extractModule tcg - rdrenv = tcg_rdr_env tcg - - case lookupOccEnv rdrenv occ of - Nothing -> empty - Just elts -> do - mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts - case mvar of - Just tt -> liftMaybe $ f tt - _ -> empty - - liftMaybe :: Monad m => Maybe a -> MaybeT m a liftMaybe a = MaybeT $ pure a @@ -395,4 +377,35 @@ expandTyFam :: Context -> Type -> Type expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal + +------------------------------------------------------------------------------ +-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. +tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst +tryUnifyUnivarsButNotSkolems skolems goal inst = + case tcUnifyTysFG + (bool BindMe Skolem . flip S.member skolems) + [unCType inst] + [unCType goal] of + Unifiable subst -> pure subst + _ -> Nothing + + +updateSubst :: TCvSubst -> TacticState -> TacticState +updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) } + + +------------------------------------------------------------------------------ +-- | Get the class methods of a 'PredType', correctly dealing with +-- instantiation of quantified class types. +methodHypothesis :: PredType -> Maybe [HyInfo CType] +methodHypothesis ty = do + (tc, apps) <- splitTyConApp_maybe ty + cls <- tyConClass_maybe tc + let methods = classMethods cls + tvs = classTyVars cls + subst = zipTvSubst tvs apps + pure $ methods <&> \method -> + let (_, _, ty) = tcSplitSigmaTy $ idType method + in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty + ) diff --git a/src/Wingman/Judgements.hs b/src/Wingman/Judgements.hs --- a/src/Wingman/Judgements.hs +++ b/src/Wingman/Judgements.hs @@ -18,6 +18,7 @@ import SrcLoc import Type import Wingman.GHC (algebraicTyCon, normalizeType) +import Wingman.Judgements.Theta import Wingman.Types @@ -69,6 +70,15 @@ withNewGoal t = field @"_jGoal" .~ t +------------------------------------------------------------------------------ +-- | Add some new type equalities to the local judgement. +withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement +withNewCoercions ev j = + let subst = allEvidenceToSubst mempty $ coerce ev + in fmap (CType . substTyAddInScope subst . unCType) j + & field @"j_coercion" %~ unionTCvSubst subst + + normalizeHypothesis :: Functor f => Context -> f CType -> f CType normalizeHypothesis = fmap . coerce . normalizeType @@ -365,6 +375,10 @@ . jLocalHypothesis +jNeedsToBindArgs :: Judgement' CType -> Bool +jNeedsToBindArgs = isFunTy . unCType . jGoal + + ------------------------------------------------------------------------------ -- | Fold a hypothesis into a single mapping from name to info. This -- unavoidably will cause duplicate names (things like methods) to shadow one @@ -414,6 +428,7 @@ , _jWhitelistSplit = True , _jIsTopHole = top , _jGoal = CType goal + , j_coercion = emptyTCvSubst } 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 @@ -5,14 +5,17 @@ ( Evidence , getEvidenceAtHole , mkEvidence + , evidenceToCoercions , evidenceToSubst , evidenceToHypothesis , evidenceToThetaType + , allEvidenceToSubst ) where import Class (classTyVars) import Control.Applicative (empty) import Control.Lens (preview) +import Data.Coerce (coerce) import Data.Maybe (fromMaybe, mapMaybe, maybeToList) import Data.Generics.Sum (_Ctor) import Data.Set (Set) @@ -32,7 +35,7 @@ import TcType (substTy) import TcType (tcTyConAppTyCon_maybe) import TysPrim (eqPrimTyCon) -import Wingman.Machinery +import Wingman.GHC import Wingman.Types @@ -110,13 +113,16 @@ $ fmap (substPair subst) evs ------------------------------------------------------------------------------ +-- | Given some 'Evidence', get a list of which types are now equal. +evidenceToCoercions :: [Evidence] -> [(CType, CType)] +evidenceToCoercions = coerce . mapMaybe (preview $ _Ctor @"EqualityOfTypes") + +------------------------------------------------------------------------------ -- | 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) + (allEvidenceToSubst (ts_skolems ts) . coerce $ evidenceToCoercions 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,15 +1,11 @@ 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 OccName (mkVarOcc, mkClsOcc) import Refinery.Tactic -import Wingman.Context (getCurrentDefinitions, getKnownInstance) import Wingman.Judgements (jGoal) import Wingman.KnownStrategies.QuickCheck (deriveArbitrary) -import Wingman.Machinery (tracing) +import Wingman.Machinery (tracing, getKnownInstance, getCurrentDefinitions) import Wingman.Tactics import Wingman.Types @@ -29,7 +25,7 @@ getCurrentDefinitions >>= \case [(def, _)] | def == mkVarOcc name -> tracing ("known " <> name) t - _ -> throwError NoApplicableTactic + _ -> failure NoApplicableTactic deriveFmap :: TacticsM () @@ -37,7 +33,7 @@ try intros overAlgebraicTerms homo choice - [ overFunctions apply >> auto' 2 + [ overFunctions (apply Saturated) >> auto' 2 , assumption , recursion ] @@ -57,7 +53,7 @@ destructAll split g <- goal - minst <- getKnownInstance kt_semigroup + minst <- getKnownInstance (mkClsOcc "Semigroup") . pure . unCType $ jGoal g @@ -79,7 +75,7 @@ deriveMempty = do split g <- goal - minst <- getKnownInstance kt_monoid [unCType $ jGoal g] + minst <- getKnownInstance (mkClsOcc "Monoid") [unCType $ jGoal g] for_ minst $ \(cls, df) -> do applyMethod cls df $ mkVarOcc "mempty" try assumption diff --git a/src/Wingman/KnownStrategies/QuickCheck.hs b/src/Wingman/KnownStrategies/QuickCheck.hs --- a/src/Wingman/KnownStrategies/QuickCheck.hs +++ b/src/Wingman/KnownStrategies/QuickCheck.hs @@ -1,7 +1,6 @@ module Wingman.KnownStrategies.QuickCheck where import ConLike (ConLike(RealDataCon)) -import Control.Monad.Except (MonadError (throwError)) import Data.Bool (bool) import Data.Generics (everything, mkQ) import Data.List (partition) @@ -15,7 +14,7 @@ import GHC.SourceGen.Overloaded (App ((@@)), HasList (list)) import GHC.SourceGen.Pat (conP) import OccName (HasOccName (occName), mkVarOcc, occNameString) -import Refinery.Tactic (goal, rule) +import Refinery.Tactic (goal, rule, failure) import TyCon (TyCon, tyConDataCons, tyConName) import Type (splitTyConApp_maybe) import Wingman.CodeGen @@ -61,7 +60,7 @@ (list $ fmap genExpr big) terminal_expr ] - _ -> throwError $ GoalMismatch "deriveArbitrary" ty + _ -> failure $ GoalMismatch "deriveArbitrary" ty ------------------------------------------------------------------------------ diff --git a/src/Wingman/LanguageServer.hs b/src/Wingman/LanguageServer.hs --- a/src/Wingman/LanguageServer.hs +++ b/src/Wingman/LanguageServer.hs @@ -44,7 +44,6 @@ import qualified FastString import GHC.Generics (Generic) 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 @@ -53,19 +52,21 @@ 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 hiding + (SemanticTokenAbsolute (length, line), + SemanticTokenRelative (length), + SemanticTokensEdit (_start)) import Language.LSP.Types.Capabilities import OccName import Prelude hiding (span) import Retrie (transformA) import SrcLoc (containsSpan) -import TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env)) +import TcRnTypes (tcg_binds, TcGblEnv) import Wingman.Context import Wingman.GHC import Wingman.Judgements 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 @@ -138,8 +139,11 @@ , 'PropertyKey "max_use_ctor_actions" 'TInteger , 'PropertyKey "timeout_duration" 'TInteger , 'PropertyKey "auto_gas" 'TInteger + , 'PropertyKey "proofstate_styling" 'TBoolean ] properties = emptyProperties + & defineBooleanProperty #proofstate_styling + "Should Wingman emit styling markup when showing metaprogram proof states?" True & 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 @@ -164,6 +168,7 @@ <$> usePropertyLsp #max_use_ctor_actions pId properties <*> usePropertyLsp #timeout_duration pId properties <*> usePropertyLsp #auto_gas pId properties + <*> usePropertyLsp #proofstate_styling pId properties getIdeDynflags @@ -215,9 +220,8 @@ -- involved, so it's not crucial to track ages. let henv = untrackedStaleValue $ hscenv eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv - kt <- knownThings (untrackedStaleValue tcg) henv - (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt + (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t dflags <- getIdeDynflags state nfp @@ -240,10 +244,10 @@ -> TrackedStale Bindings -> Tracked 'Current RealSrcSpan -> TrackedStale TcGblEnv + -> HscEnv -> ExternalPackageState - -> KnownThings -> Maybe (Judgement, Context) -mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do +mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps = do binds_rss <- mapAgeFrom bmap rss tcg_rss <- mapAgeFrom tcgmap rss @@ -253,8 +257,8 @@ $ unTrack $ getDefiningBindings <$> binds <*> binds_rss) (unTrack tcg) + hscenv eps - kt evidence top_provs = getRhsPosVals tcg_rss tcs already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs @@ -484,6 +488,7 @@ ufmSeverity :: UserFacingMessage -> MessageType +ufmSeverity NotEnoughGas = MtInfo ufmSeverity TacticErrors = MtError ufmSeverity TimedOut = MtInfo ufmSeverity NothingToDo = MtInfo @@ -597,26 +602,4 @@ . 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 --- a/src/Wingman/LanguageServer/Metaprogram.hs +++ b/src/Wingman/LanguageServer/Metaprogram.hs @@ -10,7 +10,6 @@ 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) @@ -23,7 +22,7 @@ import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat -import GhcPlugins (containsSpan, realSrcLocSpan) +import GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart) import Ide.Types import Language.LSP.Types import Prelude hiding (span) @@ -51,9 +50,9 @@ case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of Just (trss, program) -> do let tr_range = fmap realSrcSpanToRange trss + rsl = realSrcSpanStart $ unTrack 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 + z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program pure $ Hover { _contents = HoverContents $ MarkupContent MkMarkdown 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 @@ -12,12 +12,12 @@ ) where import Control.Monad -import Control.Monad.Reader (runReaderT) import Data.Aeson import Data.Bool (bool) import Data.Coerce import Data.Maybe import Data.Monoid +import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable import DataCon (dataConName) @@ -27,14 +27,16 @@ import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.PluginUtils import Ide.Types -import Language.LSP.Types +import Language.LSP.Types hiding + (SemanticTokenAbsolute (length, line), + SemanticTokenRelative (length), + SemanticTokensEdit (_start)) import OccName import Prelude hiding (span) import Wingman.Auto import Wingman.GHC import Wingman.Judgements -import Wingman.Machinery (useNameFromHypothesis) -import Wingman.Metaprogramming.Lexer (ParserContext) +import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types @@ -42,19 +44,19 @@ ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -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 +commandTactic :: TacticCommand -> T.Text -> TacticsM () +commandTactic Auto = const auto +commandTactic Intros = const intros +commandTactic Destruct = useNameFromHypothesis destruct . mkVarOcc . T.unpack +commandTactic DestructPun = useNameFromHypothesis destructPun . mkVarOcc . T.unpack +commandTactic Homomorphism = useNameFromHypothesis homo . mkVarOcc . T.unpack +commandTactic DestructLambdaCase = const destructLambdaCase +commandTactic HomomorphismLambdaCase = const homoLambdaCase +commandTactic DestructAll = const destructAll +commandTactic UseDataCon = userSplit . mkVarOcc . T.unpack +commandTactic Refine = const refine +commandTactic BeginMetaprogram = const metaprogram +commandTactic RunMetaprogram = parseMetaprogram ------------------------------------------------------------------------------ @@ -128,7 +130,7 @@ commandProvider HomomorphismLambdaCase = requireHoleSort (== Hole) $ requireExtension LambdaCase $ - filterGoalType ((== Just True) . lambdaCaseable) $ + filterGoalType (liftLambdaCase False homoFilter) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = requireHoleSort (== Hole) $ @@ -315,8 +317,20 @@ -- | We should show homos only when the goal type is the same as the binding -- type, and that both are usual algebraic types. homoFilter :: Type -> Type -> Bool -homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 -homoFilter _ _ = False +homoFilter codomain domain = + case uncoveredDataCons domain codomain of + Just s -> S.null s + _ -> False + + +------------------------------------------------------------------------------ +-- | Lift a function of (codomain, domain) over a lambda case. +liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r +liftLambdaCase nil f t = + case tacticsSplitFunTy t of + (_, _, arg : _, res) -> f res arg + _ -> nil + ------------------------------------------------------------------------------ diff --git a/src/Wingman/Machinery.hs b/src/Wingman/Machinery.hs --- a/src/Wingman/Machinery.hs +++ b/src/Wingman/Machinery.hs @@ -1,17 +1,15 @@ -{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} 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.Class (gets, modify, MonadState) import Control.Monad.State.Strict (StateT (..), execStateT) -import Data.Bool (bool) +import Control.Monad.Trans.Maybe import Data.Coerce -import Data.Either import Data.Foldable import Data.Functor ((<&>)) import Data.Generics (everything, gcount, mkQ) @@ -21,18 +19,18 @@ import Data.Maybe (mapMaybe) import Data.Monoid (getSum) import Data.Ord (Down (..), comparing) -import Data.Set (Set) import qualified Data.Set as S +import Data.Traversable (for) import Development.IDE.Core.Compile (lookupName) import Development.IDE.GHC.Compat 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 (tyCoVarsOfTypeWellScoped, splitTyConApp_maybe) -import Unify +import Type (tyCoVarsOfTypeWellScoped) +import Wingman.Context (getInstance) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -42,6 +40,17 @@ substCTy subst = coerce . substTy subst . coerce +getSubstForJudgement + :: MonadState TacticState m + => Judgement + -> m TCvSubst +getSubstForJudgement j = do + -- NOTE(sandy): It's OK to use mempty here, because coercions _can_ give us + -- substitutions for skolems. + let coercions = j_coercion j + unifier <- gets ts_unifier + pure $ unionTCvSubst unifier coercions + ------------------------------------------------------------------------------ -- | Produce a subgoal that must be solved before we can solve the original -- goal. @@ -50,7 +59,7 @@ -> Rule newSubgoal j = do ctx <- ask - unifier <- gets ts_unifier + unifier <- getSubstForJudgement j subgoal $ normalizeJudgement ctx $ substJdg unifier @@ -69,8 +78,8 @@ :: Context -> Judgement -> TacticsM () -- ^ Tactic to use - -> Either [TacticError] RunTacticResults -runTactic ctx jdg t = + -> IO (Either [TacticError] RunTacticResults) +runTactic ctx jdg t = do let skolems = S.fromList $ foldMap (tyCoVarsOfTypeWellScoped . unCType) $ (:) (jGoal jdg) @@ -82,23 +91,23 @@ defaultTacticState { ts_skolems = skolems } - in case partitionEithers - . flip runReader ctx - . unExtractM - $ runTacticT t jdg tacticState of - (errs, []) -> Left $ take 50 errs - (_, fmap assoc23 -> solns) -> do + res <- flip runReaderT ctx + . unExtractM + $ runTacticT t jdg tacticState + pure $ case res of + (Left errs) -> Left $ take 50 errs + (Right solns) -> do let sorted = - flip sortBy solns $ comparing $ \(ext, (_, holes)) -> - Down $ scoreSolution ext jdg holes + flip sortBy solns $ comparing $ \(Proof ext _ holes) -> + Down $ scoreSolution ext jdg $ fmap snd holes case sorted of - ((syn, (_, subgoals)) : _) -> + ((Proof syn _ subgoals) : _) -> Right $ RunTacticResults { rtr_trace = syn_trace syn , rtr_extract = simplify $ syn_val syn - , rtr_subgoals = subgoals - , rtr_other_solns = reverse . fmap fst $ sorted + , rtr_subgoals = fmap snd subgoals + , rtr_other_solns = reverse . fmap pf_extract $ sorted , rtr_jdg = jdg , rtr_ctx = ctx } @@ -143,7 +152,7 @@ -> TacticT jdg ext err s m a mappingExtract f (TacticT m) = TacticT $ StateT $ \jdg -> - mapExtract' f $ runStateT m jdg + mapExtract id f $ runStateT m jdg ------------------------------------------------------------------------------ @@ -204,23 +213,8 @@ deriving (Eq, Ord, Show) via a ------------------------------------------------------------------------------- --- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of. -tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst -tryUnifyUnivarsButNotSkolems skolems goal inst = - case tcUnifyTysFG - (bool BindMe Skolem . flip S.member skolems) - [unCType inst] - [unCType goal] of - Unifiable subst -> pure subst - _ -> Nothing -updateSubst :: TCvSubst -> TacticState -> TacticState -updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) } - - - ------------------------------------------------------------------------------ -- | Attempt to unify two types. unify :: CType -- ^ The goal type @@ -231,10 +225,27 @@ case tryUnifyUnivarsButNotSkolems skolems goal inst of Just subst -> modify $ updateSubst subst - Nothing -> throwError (UnificationError inst goal) + Nothing -> cut +cut :: RuleT jdg ext err s m a +cut = RuleT Empty + ------------------------------------------------------------------------------ +-- | Attempt to unify two types. +canUnify + :: MonadState TacticState m + => CType -- ^ The goal type + -> CType -- ^ The type we are trying unify the goal type with + -> m Bool +canUnify goal inst = do + skolems <- gets ts_skolems + case tryUnifyUnivarsButNotSkolems skolems goal inst of + Just _ -> pure True + Nothing -> pure False + + +------------------------------------------------------------------------------ -- | Prefer the first tactic to the second, if the bool is true. Otherwise, just run the second tactic. -- -- This is useful when you have a clever pruning solution that isn't always @@ -245,42 +256,6 @@ ------------------------------------------------------------------------------ --- | Get the class methods of a 'PredType', correctly dealing with --- instantiation of quantified class types. -methodHypothesis :: PredType -> Maybe [HyInfo CType] -methodHypothesis ty = do - (tc, apps) <- splitTyConApp_maybe ty - cls <- tyConClass_maybe tc - let methods = classMethods cls - tvs = classTyVars cls - subst = zipTvSubst tvs apps - pure $ methods <&> \method -> - let (_, _, ty) = tcSplitSigmaTy $ idType method - in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty - ) - - ------------------------------------------------------------------------------- --- | Mystical time-traveling combinator for inspecting the extracts produced by --- a tactic. We can use it to guard that extracts match certain predicates, for --- example. --- --- Note, that this thing is WEIRD. To illustrate: --- --- @@ --- peek f --- blah --- @@ --- --- Here, @f@ can inspect the extract _produced by @blah@,_ which means the --- causality appears to go backwards. --- --- 'peek' should be exposed directly by @refinery@ in the next release. -peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m () -peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j - - ------------------------------------------------------------------------------- -- | Run the given tactic iff the current hole contains no univars. Skolems and -- already decided univars are OK though. requireConcreteHole :: TacticsM a -> TacticsM a @@ -290,7 +265,7 @@ let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg case S.size $ vars S.\\ skolems of 0 -> m - _ -> throwError TooPolymorphic + _ -> failure TooPolymorphic ------------------------------------------------------------------------------ @@ -323,7 +298,7 @@ hy <- jHypothesis <$> goal case M.lookup name $ hyByName hy of Just hi -> f hi - Nothing -> throwError $ NotInScope name + Nothing -> failure $ NotInScope name ------------------------------------------------------------------------------ -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to @@ -332,7 +307,7 @@ useNameFromContext f name = do lookupNameInContext name >>= \case Just ty -> f $ createImportedHyInfo name ty - Nothing -> throwError $ NotInScope name + Nothing -> failure $ NotInScope name ------------------------------------------------------------------------------ @@ -345,6 +320,16 @@ Nothing -> empty +getDefiningType + :: TacticsM CType +getDefiningType = do + calling_fun_name <- fst . head <$> asks ctxDefiningFuncs + maybe + (failure $ NotInScope calling_fun_name) + pure + =<< lookupNameInContext calling_fun_name + + ------------------------------------------------------------------------------ -- | Build a 'HyInfo' for an imported term. createImportedHyInfo :: OccName -> CType -> HyInfo CType @@ -355,22 +340,67 @@ } +getTyThing + :: OccName + -> TacticsM (Maybe TyThing) +getTyThing occ = do + ctx <- ask + case lookupOccEnv (ctx_occEnv ctx) occ of + Just (elt : _) -> do + mvar <- lift + $ ExtractM + $ lift + $ lookupName (ctx_hscEnv ctx) (ctx_module ctx) + $ gre_name elt + pure mvar + _ -> pure Nothing + + ------------------------------------------------------------------------------ +-- | Like 'getTyThing' but specialized to classes. +knownClass :: OccName -> TacticsM (Maybe Class) +knownClass occ = + getTyThing occ <&> \case + Just (ATyCon tc) -> tyConClass_maybe tc + _ -> Nothing + + +------------------------------------------------------------------------------ +-- | Like 'getInstance', but uses a class that it just looked up. +getKnownInstance :: OccName -> [Type] -> TacticsM (Maybe (Class, PredType)) +getKnownInstance f tys = runMaybeT $ do + cls <- MaybeT $ knownClass f + MaybeT $ getInstance cls tys + + +------------------------------------------------------------------------------ -- | 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 + :: OccName + -> TacticsM Type +getOccNameType occ = do + getTyThing occ >>= \case + Just (AnId v) -> pure $ varType v + _ -> failure $ NotInScope occ + + +getCurrentDefinitions :: TacticsM [(OccName, CType)] +getCurrentDefinitions = do + ctx_funcs <- asks ctxDefiningFuncs + for ctx_funcs $ \res@(occ, _) -> + pure . maybe res (occ,) =<< lookupNameInContext occ + + +------------------------------------------------------------------------------ +-- | Given two types, see if we can construct a homomorphism by mapping every +-- data constructor in the domain to the same in the codomain. This function +-- returns 'Just' when all the lookups succeeded, and a non-empty value if the +-- homomorphism *is not* possible. +uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon)) +uncoveredDataCons domain codomain = do + (g_dcs, _) <- tacticsGetDataCons codomain + (hi_dcs, _) <- tacticsGetDataCons domain + pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) diff --git a/src/Wingman/Metaprogramming/Lexer.hs b/src/Wingman/Metaprogramming/Lexer.hs --- a/src/Wingman/Metaprogramming/Lexer.hs +++ b/src/Wingman/Metaprogramming/Lexer.hs @@ -7,29 +7,16 @@ import Control.Applicative import Control.Monad -import Control.Monad.Reader (ReaderT) +import Data.Foldable (asum) 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) +type Parser = P.Parsec Void Text @@ -45,6 +32,31 @@ ichar :: Parser Char ichar = P.alphaNumChar <|> P.char '_' <|> P.char '\'' +symchar :: Parser Char +symchar = asum + [ P.symbolChar + , P.char '!' + , P.char '#' + , P.char '$' + , P.char '%' + , P.char '^' + , P.char '&' + , P.char '*' + , P.char '-' + , P.char '=' + , P.char '+' + , P.char ':' + , P.char '<' + , P.char '>' + , P.char ',' + , P.char '.' + , P.char '/' + , P.char '?' + , P.char '~' + , P.char '|' + , P.char '\\' + ] + lexeme :: Parser a -> Parser a lexeme = L.lexeme sc @@ -66,14 +78,18 @@ 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) + c <- P.alphaNumChar <|> P.char '(' + fmap mkVarOcc $ case c of + '(' -> do + cs <- P.many symchar + void $ P.char ')' + pure cs + _ -> do + cs <- P.many ichar + pure $ 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 diff --git a/src/Wingman/Metaprogramming/Parser.hs b/src/Wingman/Metaprogramming/Parser.hs --- a/src/Wingman/Metaprogramming/Parser.hs +++ b/src/Wingman/Metaprogramming/Parser.hs @@ -7,17 +7,16 @@ 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 Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile) +import FastString (unpackFS) +import Refinery.Tactic (failure) 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.Machinery (useNameFromHypothesis, useNameFromContext, getCurrentDefinitions) import Wingman.Metaprogramming.Lexer import Wingman.Metaprogramming.Parser.Documentation import Wingman.Metaprogramming.ProofState (proofState, layout) @@ -176,9 +175,20 @@ "f (_ :: a)" ] + , command "pointwise" Deterministic Tactic + "Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings." + (pure . flip restrictPositionForApplication (pure ())) + [ Example + (Just "In the context of `f (a1, b1) (a2, b2) = _`. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.") + ["(use mappend)"] + [] + Nothing + "mappend _ _" + ] + , command "apply" Deterministic (Ref One) "Apply the given function from *local* scope." - (pure . useNameFromHypothesis apply) + (pure . useNameFromHypothesis (apply Saturated)) [ Example Nothing ["f"] @@ -285,8 +295,8 @@ "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" + Just (self, _) -> useNameFromContext (apply Saturated) self + Nothing -> failure $ TacticPanic "no defining function" ) [ Example (Just "In the context of `foo (a :: Int) (b :: b) = _`:") @@ -298,13 +308,7 @@ , 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 - ) + (pure . use Saturated) [ Example (Just "`import Data.Char (isSpace)`") ["isSpace"] @@ -344,6 +348,44 @@ "(_ :: a -> a -> a -> a) a1 a2 a3" ] + , command "try" Nondeterministic Tactic + "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states." + (pure . R.try) + [ Example + Nothing + ["(apply f)"] + [ EHI "f" "a -> b" + ] + (Just "b") + $ T.pack $ unlines + [ "-- BOTH of:\n" + , "f (_ :: a)" + , "\n-- and\n" + , "_ :: b" + ] + ] + + , command "nested" Nondeterministic (Ref One) + "Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context." + (pure . nested) + [ Example + Nothing + ["fmap"] + [] + (Just "[(Int, Either Bool a)] -> [(Int, Either Bool b)]") + "fmap (fmap (fmap _))" + ] + + , command "with_arg" Deterministic Nullary + "Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context." + (pure with_arg) + [ Example + (Just "Where `a` is a new unifiable type variable.") + [] + [] + (Just "r") + "(_2 :: a -> r) (_1 :: a)" + ] ] @@ -359,14 +401,9 @@ 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.InfixR (symbol "|" $> (R.<%>) )] , [ P.InfixL (symbol ";" $> (>>)) , P.InfixL (symbol "," $> bindOne) ] @@ -385,47 +422,53 @@ wrapError err = "```\n" <> err <> "\n```\n" +fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b +fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s)) + = P.ParseErrorBundle ne + $ P.PosState a n + (P.SourcePos + (unpackFS $ srcLocFile rsl) + ((<>) line $ P.mkPos $ srcLocLine rsl - 1) + ((<>) col $ P.mkPos $ srcLocCol rsl - 1 + length @[] "[wingman|") + ) + pos + s + ------------------------------------------------------------------------------ -- | Attempt to run a metaprogram tactic, returning the proof state, or the -- errors. attempt_it - :: Context + :: RealSrcLoc + -> 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 + -> IO (Either String String) +attempt_it rsl ctx jdg program = + case P.runParser tacticProgram "" (T.pack program) of + Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb + Right tt -> do + res <- runTactic + ctx + jdg + tt + pure $ case res of + Left tes -> Left $ wrapError $ show tes + Right rtr -> Right + $ layout (cfg_proofstate_styling $ ctxConfig ctx) + $ proofState rtr -parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ()) +parseMetaprogram :: T.Text -> 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 + = either (const $ pure ()) id + . P.runParser tacticProgram "" ------------------------------------------------------------------------------ -- | Automatically generate the metaprogram command reference. writeDocumentation :: IO () writeDocumentation = - writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $ + writeFile "COMMANDS.md" $ unlines [ "# Wingman Metaprogram Command Reference" , "" diff --git a/src/Wingman/Metaprogramming/Parser.hs-boot b/src/Wingman/Metaprogramming/Parser.hs-boot new file mode 100644 --- /dev/null +++ b/src/Wingman/Metaprogramming/Parser.hs-boot @@ -0,0 +1,7 @@ +module Wingman.Metaprogramming.Parser where + +import Wingman.Metaprogramming.Lexer +import Wingman.Types + +tactic :: Parser (TacticsM ()) + diff --git a/src/Wingman/Metaprogramming/Parser/Documentation.hs b/src/Wingman/Metaprogramming/Parser/Documentation.hs --- a/src/Wingman/Metaprogramming/Parser/Documentation.hs +++ b/src/Wingman/Metaprogramming/Parser/Documentation.hs @@ -6,14 +6,16 @@ import Data.List (sortOn) import Data.String (IsString) import Data.Text (Text) -import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc hiding (parens) 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.Metaprogramming.Lexer (Parser, identifier, variable, parens) import Wingman.Types (TacticsM) +import {-# SOURCE #-} Wingman.Metaprogramming.Parser (tactic) + ------------------------------------------------------------------------------ -- | Is a tactic deterministic or not? data Determinism @@ -46,11 +48,13 @@ Nullary :: Syntax (Parser (TacticsM ())) Ref :: Count a -> Syntax (a -> Parser (TacticsM ())) Bind :: Count a -> Syntax (a -> Parser (TacticsM ())) + Tactic :: Syntax (TacticsM () -> Parser (TacticsM ())) prettySyntax :: Syntax a -> Doc b prettySyntax Nullary = "none" prettySyntax (Ref co) = prettyCount co <+> "reference" prettySyntax (Bind co) = prettyCount co <+> "binding" +prettySyntax Tactic = "tactic" ------------------------------------------------------------------------------ @@ -108,21 +112,24 @@ ------------------------------------------------------------------------------ -- | Run the 'Parser' of a 'MetaprogramCommand' makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ()) -makeMPParser (MC name Nullary _ _ tactic _) = do +makeMPParser (MC name Nullary _ _ t _) = do identifier name - tactic -makeMPParser (MC name (Ref One) _ _ tactic _) = do + t +makeMPParser (MC name (Ref One) _ _ t _) = do identifier name - variable >>= tactic -makeMPParser (MC name (Ref Many) _ _ tactic _) = do + variable >>= t +makeMPParser (MC name (Ref Many) _ _ t _) = do identifier name - P.many variable >>= tactic -makeMPParser (MC name (Bind One) _ _ tactic _) = do + P.many variable >>= t +makeMPParser (MC name (Bind One) _ _ t _) = do identifier name - variable >>= tactic -makeMPParser (MC name (Bind Many) _ _ tactic _) = do + variable >>= t +makeMPParser (MC name (Bind Many) _ _ t _) = do identifier name - P.many variable >>= tactic + P.many variable >>= t +makeMPParser (MC name Tactic _ _ t _) = do + identifier name + parens tactic >>= t ------------------------------------------------------------------------------ @@ -143,6 +150,7 @@ , ">" <+> align (pretty desc) , mempty , vsep $ fmap (prettyExample name) exs + , mempty ] diff --git a/src/Wingman/Metaprogramming/ProofState.hs b/src/Wingman/Metaprogramming/ProofState.hs --- a/src/Wingman/Metaprogramming/ProofState.hs +++ b/src/Wingman/Metaprogramming/ProofState.hs @@ -43,24 +43,26 @@ forceMarkdownNewlines :: String -> String forceMarkdownNewlines = unlines . fmap (<> " ") . lines -layout :: Doc Ann -> String -layout +layout :: Bool -> Doc Ann -> String +layout use_styling = forceMarkdownNewlines . T.unpack . renderSimplyDecorated id - renderAnn - renderUnann + (renderAnn use_styling) + (renderUnann use_styling) . layoutPretty (LayoutOptions $ AvailablePerLine 80 0.6) -renderAnn :: Ann -> T.Text -renderAnn Goal = "" -renderAnn Hypoth = "```haskell\n" -renderAnn Status = "" +renderAnn :: Bool -> Ann -> T.Text +renderAnn False _ = "" +renderAnn _ Goal = "" +renderAnn _ Hypoth = "```haskell\n" +renderAnn _ Status = "" -renderUnann :: Ann -> T.Text -renderUnann Goal = "" -renderUnann Hypoth = "\n```\n" -renderUnann Status = "" +renderUnann :: Bool -> Ann -> T.Text +renderUnann False _ = "" +renderUnann _ Goal = "" +renderUnann _ Hypoth = "\n```\n" +renderUnann _ Status = "" proofState :: RunTacticResults -> Doc Ann proofState RunTacticResults{rtr_subgoals} = diff --git a/src/Wingman/Plugin.hs b/src/Wingman/Plugin.hs --- a/src/Wingman/Plugin.hs +++ b/src/Wingman/Plugin.hs @@ -8,7 +8,6 @@ , TacticCommand (..) ) where -import Control.Exception (evaluate) import Control.Monad import Control.Monad.Trans import Control.Monad.Trans.Maybe @@ -32,6 +31,7 @@ import Wingman.CaseSplit import Wingman.EmptyCase import Wingman.GHC +import Wingman.Judgements (jNeedsToBindArgs) import Wingman.LanguageServer import Wingman.LanguageServer.Metaprogram (hoverProvider) import Wingman.LanguageServer.TacticProviders @@ -40,7 +40,6 @@ import Wingman.StaticPlugin import Wingman.Tactics import Wingman.Types -import Wingman.Metaprogramming.Lexer (ParserContext) descriptor :: PluginId -> PluginDescriptor IdeState @@ -51,7 +50,7 @@ PluginCommand (tcCommandId tc) (tacticDesc $ tcCommandName tc) - (tacticCmd (flip commandTactic tc) plId)) + (tacticCmd (commandTactic tc) plId)) [minBound .. maxBound] , pure $ PluginCommand @@ -101,8 +100,14 @@ pure $ Left $ mkErr InternalError $ T.pack $ show ufm +mkUserFacingMessage :: [TacticError] -> UserFacingMessage +mkUserFacingMessage errs + | elem OutOfGas errs = NotEnoughGas +mkUserFacingMessage _ = TacticErrors + + tacticCmd - :: (ParserContext -> T.Text -> IO (TacticsM ())) + :: (T.Text -> TacticsM ()) -> PluginId -> CommandFunction IdeState TacticParams tacticCmd tac pId state (TacticParams uri range var_name) @@ -116,14 +121,14 @@ 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 + let t = tac var_name - timingOut (cfg_timeout_seconds cfg * seconds) $ join $ - case runTactic hj_ctx hj_jdg t of + timingOut (cfg_timeout_seconds cfg * seconds) $ do + res <- liftIO $ runTactic hj_ctx hj_jdg t + pure $ join $ case res of Left errs -> do traceMX "errs" errs - Left TacticErrors + Left $ mkUserFacingMessage errs Right rtr -> case rtr_extract rtr of L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) -> @@ -153,9 +158,9 @@ timingOut :: Int -- ^ Time in microseconds - -> a -- ^ Computation to run + -> IO a -- ^ Computation to run -> MaybeT IO a -timingOut t m = MaybeT $ timeout t $ evaluate m +timingOut t m = MaybeT $ timeout t m mkErr :: ErrorCode -> T.Text -> ResponseError @@ -191,18 +196,34 @@ -> Graft (Either String) ParsedSource graftHole span rtr | _jIsTopHole (rtr_jdg rtr) - = genericGraftWithSmallestM (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span $ \dflags -> - everywhereM' - $ mkBindListT $ \ix -> - graftDecl dflags span ix $ \name pats -> - splitToDecl (occName name) - $ iterateSplit - $ mkFirstAgda (fmap unXPat pats) - $ unLoc - $ rtr_extract rtr + = genericGraftWithSmallestM + (Proxy @(Located [LMatch GhcPs (LHsExpr GhcPs)])) span + $ \dflags matches -> + everywhereM' + $ mkBindListT $ \ix -> + graftDecl dflags span ix $ \name pats -> + splitToDecl + (case not $ jNeedsToBindArgs (rtr_jdg rtr) of + -- If the user has explicitly bound arguments, use the + -- fixity they wrote. + True -> matchContextFixity . m_ctxt . unLoc + =<< listToMaybe matches + -- Otherwise, choose based on the name of the function. + False -> Nothing + ) + (occName name) + $ iterateSplit + $ mkFirstAgda (fmap unXPat pats) + $ unLoc + $ rtr_extract rtr graftHole span rtr = graft span $ rtr_extract rtr + + +matchContextFixity :: HsMatchContext p -> Maybe LexicalFixity +matchContextFixity (FunRhs _ l _) = Just l +matchContextFixity _ = Nothing ------------------------------------------------------------------------------ diff --git a/src/Wingman/StaticPlugin.hs b/src/Wingman/StaticPlugin.hs --- a/src/Wingman/StaticPlugin.hs +++ b/src/Wingman/StaticPlugin.hs @@ -19,9 +19,17 @@ staticPlugin = mempty { dynFlagsModifyGlobal = \df -> allowEmptyCaseButWithWarning + $ flip gopt_unset Opt_SortBySubsumHoleFits + $ flip gopt_unset Opt_ShowValidHoleFits $ df + { refLevelHoleFits = Just 0 + , maxRefHoleFits = Just 0 + , maxValidHoleFits = Just 0 #if __GLASGOW_HASKELL__ >= 808 - { staticPlugins = staticPlugins df <> [metaprogrammingPlugin] } + , staticPlugins = staticPlugins df <> [metaprogrammingPlugin] +#endif + } +#if __GLASGOW_HASKELL__ >= 808 , dynFlagsModifyParser = enableQuasiQuotes #endif } diff --git a/src/Wingman/Tactics.hs b/src/Wingman/Tactics.hs --- a/src/Wingman/Tactics.hs +++ b/src/Wingman/Tactics.hs @@ -8,15 +8,17 @@ import ConLike (ConLike(RealDataCon)) import Control.Applicative (Alternative(empty)) import Control.Lens ((&), (%~), (<>~)) +import Control.Monad (filterM) import Control.Monad (unless) -import Control.Monad.Except (throwError) +import Control.Monad.Extra (anyM) import Control.Monad.Reader.Class (MonadReader (ask)) -import Control.Monad.State.Strict (StateT(..), runStateT, gets) +import Control.Monad.State.Strict (StateT(..), runStateT) import Data.Bool (bool) import Data.Foldable import Data.Functor ((<&>)) import Data.Generics.Labels () import Data.List +import Data.List.Extra (dropEnd, takeEnd) import qualified Data.Map as M import Data.Maybe import Data.Set (Set) @@ -34,7 +36,6 @@ 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 @@ -64,28 +65,43 @@ { syn_trace = tracePrim $ "assume " <> occNameString name , syn_used_vals = S.singleton name } - Nothing -> throwError $ UndefinedHypothesis name + Nothing -> cut +------------------------------------------------------------------------------ +-- | Like 'apply', but uses an 'OccName' available in the context +-- or the module +use :: Saturation -> OccName -> TacticsM () +use sat occ = do + ctx <- ask + ty <- case lookupNameInContext occ ctx of + Just ty -> pure ty + Nothing -> CType <$> getOccNameType occ + apply sat $ createImportedHyInfo occ ty + + recursion :: TacticsM () -- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test, -- presumably due to running afoul of 'requireConcreteHole'. Look into this! recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const defs) $ \(name, ty) -> markRecursion $ do + jdg <- goal -- Peek allows us to look at the extract produced by this block. - peek $ \ext -> do - jdg <- goal - let pat_vals = jPatHypothesis jdg - -- Make sure that the recursive call contains at least one already-bound - -- pattern value. This ensures it is structurally smaller, and thus - -- suggests termination. - unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty - - let hy' = recursiveHypothesis defs - ctx <- ask - localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy') - <@> fmap (localTactic assumption . filterPosition name) [0..] + peek + ( do + let hy' = recursiveHypothesis defs + ctx <- ask + localTactic (apply Saturated $ HyInfo name RecursivePrv ty) (introduce ctx hy') + <@> fmap (localTactic assumption . filterPosition name) [0..] + ) $ \ext -> do + let pat_vals = jPatHypothesis jdg + -- Make sure that the recursive call contains at least one already-bound + -- pattern value. This ensures it is structurally smaller, and thus + -- suggests termination. + case (any (flip M.member pat_vals) $ syn_used_vals ext) of + True -> Nothing + False -> Just UnhelpfulRecursion restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM () @@ -112,22 +128,24 @@ intros' names = rule $ \jdg -> do let g = jGoal jdg case tacticsSplitFunTy $ unCType g of - (_, _, [], _) -> throwError $ GoalMismatch "intros" g - (_, _, as, b) -> do + (_, _, [], _) -> cut -- failure $ GoalMismatch "intros" g + (_, _, args, res) -> do ctx <- ask - let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names - num_args = length vs + let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names + num_occs = length occs top_hole = isTopHole ctx jdg - hy' = lambdaHypothesis top_hole $ zip vs $ coerce as + bindings = zip occs $ coerce args + bound_occs = fmap fst bindings + hy' = lambdaHypothesis top_hole bindings jdg' = introduce ctx hy' - $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg + $ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg ext <- newSubgoal jdg' pure $ ext - & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") + & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}") . pure & #syn_scoped <>~ hy' - & #syn_val %~ noLoc . lambda (fmap bvar' vs) . unLoc + & #syn_val %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc ------------------------------------------------------------------------------ @@ -184,10 +202,25 @@ ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: HyInfo CType -> TacticsM () -homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg -> - buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) +homo hi = requireConcreteHole . tracing "homo" $ do + jdg <- goal + let g = jGoal jdg + -- Ensure that every data constructor in the domain type is covered in the + -- codomain; otherwise 'homo' will produce an ill-typed program. + case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of + Just uncovered_dcs -> + unless (S.null uncovered_dcs) $ + failure $ TacticPanic "Can't cover every datacon in domain" + _ -> failure $ TacticPanic "Unable to fetch datacons" + rule + $ destruct' + False + (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) + $ hi + + ------------------------------------------------------------------------------ -- | LambdaCase split, and leave holes in the matches. destructLambdaCase :: TacticsM () @@ -208,30 +241,39 @@ $ jGoal jdg -apply :: HyInfo CType -> TacticsM () -apply hi = tracing ("apply' " <> show (hi_name hi)) $ do +data Saturation = Unsaturated Int + deriving (Eq, Ord, Show) + +pattern Saturated :: Saturation +pattern Saturated = Unsaturated 0 + + +apply :: Saturation -> HyInfo CType -> TacticsM () +apply (Unsaturated n) hi = tracing ("apply' " <> show (hi_name hi)) $ do jdg <- goal let g = jGoal jdg ty = unCType $ hi_type hi func = hi_name hi ty' <- freshTyvars ty - let (_, _, args, ret) = tacticsSplitFunTy ty' + let (_, _, all_args, ret) = tacticsSplitFunTy ty' + saturated_args = dropEnd n all_args + unsaturated_args = takeEnd n all_args rule $ \jdg -> do - unify g (CType ret) + unify g (CType $ mkFunTys' unsaturated_args ret) ext <- fmap unzipTrace $ traverse ( newSubgoal . blacklistingDestruct . flip withNewGoal jdg . CType - ) args + ) saturated_args pure $ ext & #syn_used_vals %~ S.insert func & #syn_val %~ mkApply func . fmap unLoc application :: TacticsM () -application = overFunctions apply +application = overFunctions $ apply Saturated ------------------------------------------------------------------------------ @@ -241,7 +283,7 @@ jdg <- goal let g = jGoal jdg case tacticsGetDataCons $ unCType g of - Nothing -> throwError $ GoalMismatch "split" g + Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> choice $ fmap splitDataCon dcs @@ -254,7 +296,7 @@ jdg <- goal let g = jGoal jdg case tacticsGetDataCons $ unCType g of - Nothing -> throwError $ GoalMismatch "split" g + Nothing -> failure $ GoalMismatch "split" g Just (dcs, _) -> do case isSplitWhitelisted jdg of True -> choice $ fmap splitDataCon dcs @@ -273,7 +315,7 @@ case tacticsGetDataCons $ unCType g of Just ([dc], _) -> do splitDataCon dc - _ -> throwError $ GoalMismatch "splitSingle" g + _ -> failure $ GoalMismatch "splitSingle" g ------------------------------------------------------------------------------ -- | Like 'split', but prunes any data constructors which have holes. @@ -318,7 +360,7 @@ case splitTyConApp_maybe $ unCType g of Just (_, apps) -> do buildDataCon True (unwhitelistingSplit jdg) dc apps - Nothing -> throwError $ GoalMismatch "splitDataCon" g + Nothing -> cut -- failure $ GoalMismatch "splitDataCon" g ------------------------------------------------------------------------------ -- | Attempt to instantiate the given data constructor to solve the goal. @@ -347,7 +389,7 @@ $ unHypothesis $ jHypothesis jdg for_ args $ \arg -> do - subst <- gets ts_unifier + subst <- getSubstForJudgement =<< goal destruct $ fmap (coerce substTy subst) arg -------------------------------------------------------------------------------- @@ -364,8 +406,8 @@ case find (sloppyEqOccName occ . occName . dataConName) $ tyConDataCons tc of Just dc -> splitDataCon dc - Nothing -> throwError $ NotInScope occ - Nothing -> throwError $ NotInScope occ + Nothing -> failure $ NotInScope occ + Nothing -> failure $ NotInScope occ ------------------------------------------------------------------------------ @@ -390,13 +432,13 @@ auto' :: Int -> TacticsM () -auto' 0 = throwError NoProgress +auto' 0 = failure OutOfGas auto' n = do let loop = auto' (n - 1) try intros choice [ overFunctions $ \fname -> do - requireConcreteHole $ apply fname + requireConcreteHole $ apply Saturated fname loop , overAlgebraicTerms $ \aname -> do destructAuto aname @@ -427,8 +469,8 @@ Just method -> do let (_, apps) = splitAppTys df let ty = piResultTys (idType method) apps - apply $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty - Nothing -> throwError $ NotInScope method_name + apply Saturated $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty + Nothing -> failure $ NotInScope method_name applyByName :: OccName -> TacticsM () @@ -436,7 +478,7 @@ g <- goal choice $ (unHypothesis (jHypothesis g)) <&> \hi -> case hi_name hi == name of - True -> apply hi + True -> apply Saturated hi False -> empty @@ -475,22 +517,63 @@ 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" + Just (self, _) -> useNameFromContext (apply Saturated) self + Nothing -> failure $ TacticPanic "no defining function" +------------------------------------------------------------------------------ +-- | Perform a catamorphism when destructing the given 'HyInfo'. This will +-- result in let binding, making values that call the defining function on each +-- destructed value. cata :: HyInfo CType -> TacticsM () cata hi = do + (_, _, calling_args, _) + <- tacticsSplitFunTy . unCType <$> getDefiningType + freshened_args <- traverse freshTyvars calling_args diff <- hyDiff $ destruct hi + + -- For for every destructed term, check to see if it can unify with any of + -- the arguments to the calling function. If it doesn't, we don't try to + -- perform a cata on it. + unifiable_diff <- flip filterM (unHypothesis diff) $ \hi -> + flip anyM freshened_args $ \ty -> + canUnify (hi_type hi) $ CType ty + rule $ letForEach (mkVarOcc . flip mappend "_c" . occNameString) - (\hi -> self >> commit (apply hi) assumption) - diff + (\hi -> self >> commit (assume $ hi_name hi) assumption) + $ Hypothesis unifiable_diff + +------------------------------------------------------------------------------ +-- | Deeply nest an unsaturated function onto itself +nested :: OccName -> TacticsM () +nested = deepening . use (Unsaturated 1) + + +------------------------------------------------------------------------------ +-- | Repeatedly bind a tactic on its first hole +deep :: Int -> TacticsM () -> TacticsM () +deep 0 _ = pure () +deep n t = foldr1 bindOne $ replicate n t + + +------------------------------------------------------------------------------ +-- | Try 'deep' for arbitrary depths. +deepening :: TacticsM () -> TacticsM () +deepening t = + asum $ fmap (flip deep t) [0 .. 100] + + +bindOne :: TacticsM a -> TacticsM a -> TacticsM a +bindOne t t1 = t <@> [t1] + + collapse :: TacticsM () collapse = do g <- goal @@ -498,6 +581,15 @@ case terms of [hi] -> assume $ hi_name hi _ -> nary (length terms) <@> fmap (assume . hi_name) terms + + +with_arg :: TacticsM () +with_arg = rule $ \jdg -> do + let g = jGoal jdg + fresh_ty <- freshTyvars $ mkInvForAllTys [alphaTyVar] alphaTy + a <- newSubgoal $ withNewGoal (CType fresh_ty) jdg + f <- newSubgoal $ withNewGoal (coerce mkFunTys' [fresh_ty] g) jdg + pure $ fmap noLoc $ (@@) <$> fmap unLoc f <*> fmap unLoc a ------------------------------------------------------------------------------ diff --git a/src/Wingman/Types.hs b/src/Wingman/Types.hs --- a/src/Wingman/Types.hs +++ b/src/Wingman/Types.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -17,8 +18,11 @@ import Control.Lens hiding (Context) import Control.Monad.Reader import Control.Monad.State +import qualified Control.Monad.State.Strict as Strict import Data.Coerce import Data.Function +import Data.Generics (mkM, everywhereM, Data, Typeable) +import Data.Generics.Labels () import Data.Generics.Product (field) import Data.List.NonEmpty (NonEmpty (..)) import Data.Semigroup @@ -31,16 +35,21 @@ import Development.IDE.GHC.Compat hiding (Node) import Development.IDE.GHC.Orphans () import FamInstEnv (FamInstEnvs) +import GHC.Exts (fromString) import GHC.Generics import GHC.SourceGen (var) +import GhcPlugins (GlobalRdrElt, mkRdrUnqual) import InstEnv (InstEnvs(..)) import OccName +import Refinery.ProofState import Refinery.Tactic +import Refinery.Tactic.Internal (TacticT(TacticT), RuleT (RuleT)) import System.IO.Unsafe (unsafePerformIO) import Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst) import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) -import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) +import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique, mkUnique) import Wingman.Debug +import Data.IORef ------------------------------------------------------------------------------ @@ -86,6 +95,7 @@ { cfg_max_use_ctor_actions :: Int , cfg_timeout_seconds :: Int , cfg_auto_gas :: Int + , cfg_proofstate_styling :: Bool } deriving (Eq, Ord, Show) @@ -94,11 +104,13 @@ { cfg_max_use_ctor_actions = 5 , cfg_timeout_seconds = 2 , cfg_auto_gas = 4 + , cfg_proofstate_styling = True } ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type } + deriving stock (Data, Typeable) instance Eq CType where (==) = eqType `on` unCType @@ -109,9 +121,6 @@ instance Show CType where show = unsafeRender . unCType -instance Show OccName where - show = unsafeRender - instance Show Name where show = unsafeRender @@ -151,7 +160,10 @@ instance Show ConLike where show = unsafeRender +instance Show LexicalFixity where + show = unsafeRender + ------------------------------------------------------------------------------ -- | The state that should be shared between subgoals. Extracts move towards -- the root, judgments move towards the leaves, and the state moves *sideways*. @@ -170,7 +182,7 @@ -- | A 'UniqSupply' to use in 'defaultTacticState' unsafeDefaultUniqueSupply :: UniqSupply unsafeDefaultUniqueSupply = - unsafePerformIO $ mkSplitUniqSupply '🚒' + unsafePerformIO $ mkSplitUniqSupply 'w' {-# NOINLINE unsafeDefaultUniqueSupply #-} @@ -219,7 +231,7 @@ -- to keep these in the hypothesis set, rather than filtering it, in order -- to continue tracking downstream provenance. | DisallowedPrv DisallowReason Provenance - deriving stock (Eq, Show, Generic, Ord) + deriving stock (Eq, Show, Generic, Ord, Data, Typeable) ------------------------------------------------------------------------------ @@ -229,7 +241,7 @@ | Shadowed | RecursiveCall | AlreadyDestructed - deriving stock (Eq, Show, Generic, Ord) + deriving stock (Eq, Show, Generic, Ord, Data, Typeable) ------------------------------------------------------------------------------ @@ -245,7 +257,7 @@ -- ^ The datacon which introduced this term. , pv_position :: Int -- ^ The position of this binding in the datacon's arguments. - } deriving stock (Eq, Show, Generic, Ord) + } deriving stock (Eq, Show, Generic, Ord, Data, Typeable) ------------------------------------------------------------------------------ @@ -253,6 +265,7 @@ -- instances. newtype Uniquely a = Uniquely { getViaUnique :: a } deriving Show via a + deriving stock (Data, Typeable) instance Uniquable a => Eq (Uniquely a) where (==) = (==) `on` getUnique . getViaUnique @@ -268,7 +281,7 @@ newtype Hypothesis a = Hypothesis { unHypothesis :: [HyInfo a] } - deriving stock (Functor, Eq, Show, Generic, Ord) + deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable) deriving newtype (Semigroup, Monoid) @@ -279,7 +292,7 @@ , hi_provenance :: Provenance , hi_type :: a } - deriving stock (Functor, Eq, Show, Generic, Ord) + deriving stock (Functor, Eq, Show, Generic, Ord, Data, Typeable) ------------------------------------------------------------------------------ @@ -296,42 +309,71 @@ , _jWhitelistSplit :: !Bool , _jIsTopHole :: !Bool , _jGoal :: !a + , j_coercion :: TCvSubst } - deriving stock (Eq, Generic, Functor, Show) + deriving stock (Generic, Functor, Show) type Judgement = Judgement' CType -newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } +newtype ExtractM a = ExtractM { unExtractM :: ReaderT Context IO a } deriving newtype (Functor, Applicative, Monad, MonadReader Context) ------------------------------------------------------------------------------ --- | Orphan instance for producing holes when attempting to solve tactics. -instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where - hole = pure . pure . noLoc $ var "_" +-- | Used to ensure hole names are unique across invocations of runTactic +globalHoleRef :: IORef Int +globalHoleRef = unsafePerformIO $ newIORef 10 +{-# NOINLINE globalHoleRef #-} +instance MonadExtract Int (Synthesized (LHsExpr GhcPs)) TacticError TacticState ExtractM where + hole = do + u <- lift $ ExtractM $ lift $ + readIORef globalHoleRef <* modifyIORef' globalHoleRef (+ 1) + pure + ( u + , pure . noLoc $ var $ fromString $ occNameString $ occName $ mkMetaHoleName u + ) + unsolvableHole _ = hole + + +instance MonadReader r m => MonadReader r (TacticT jdg ext err s m) where + ask = TacticT $ lift $ Effect $ fmap pure ask + local f (TacticT m) = TacticT $ Strict.StateT $ \jdg -> + Effect $ local f $ pure $ Strict.runStateT m jdg + +instance MonadReader r m => MonadReader r (RuleT jdg ext err s m) where + ask = RuleT $ Effect $ fmap Axiom ask + local f (RuleT m) = RuleT $ Effect $ local f $ pure m + +mkMetaHoleName :: Int -> RdrName +mkMetaHoleName u = mkRdrUnqual $ mkVarOcc $ "_" <> show (mkUnique 'w' u) + +instance MetaSubst Int (Synthesized (LHsExpr GhcPs)) where + -- TODO(sandy): This join is to combine the synthesizeds + substMeta u val a = join $ a <&> + everywhereM (mkM $ \case + (L _ (HsVar _ (L _ name))) + | name == mkMetaHoleName u -> val + (t :: LHsExpr GhcPs) -> pure t) + + ------------------------------------------------------------------------------ -- | Reasons a tactic might fail. data TacticError - = UndefinedHypothesis OccName + = OutOfGas | GoalMismatch String CType - | UnsolvedSubgoals [Judgement] - | UnificationError CType CType | NoProgress | NoApplicableTactic - | IncorrectDataCon DataCon - | RecursionOnWrongParam OccName Int OccName + | UnhelpfulRecursion | UnhelpfulDestruct OccName - | UnhelpfulSplit OccName | TooPolymorphic | NotInScope OccName | TacticPanic String - deriving stock (Eq) + deriving (Eq) instance Show TacticError where - show (UndefinedHypothesis name) = - occNameString name <> " is not available in the hypothesis." + show OutOfGas = "Auto ran out of gas" show (GoalMismatch tac (CType typ)) = mconcat [ "The tactic " @@ -339,34 +381,20 @@ , " doesn't apply to goal type " , unsafeRender typ ] - show (UnsolvedSubgoals _) = - "There were unsolved subgoals" - show (UnificationError (CType t1) (CType t2)) = - mconcat - [ "Could not unify " - , unsafeRender t1 - , " and " - , unsafeRender t2 - ] show NoProgress = "Unable to make progress" show NoApplicableTactic = "No tactic could be applied" - show (IncorrectDataCon dcon) = - "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")" - show (RecursionOnWrongParam call p arg) = - "Recursion on wrong param (" <> show call <> ") on arg" - <> show p <> ": " <> show arg + show UnhelpfulRecursion = + "Recursion wasn't productive" show (UnhelpfulDestruct n) = "Destructing patval " <> show n <> " leads to no new types" - show (UnhelpfulSplit n) = - "Splitting constructor " <> show n <> " leads to no new goals" show TooPolymorphic = "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 + "Tactic panic: " <> err ------------------------------------------------------------------------------ @@ -394,8 +422,21 @@ -- ^ The number of recursive calls , syn_val :: a } - deriving (Eq, Show, Functor, Foldable, Traversable, Generic) + deriving stock (Eq, Show, Functor, Foldable, Traversable, Generic, Data, Typeable) +instance Monad Synthesized where + return = pure + Synthesized tr1 sc1 uv1 rc1 a >>= f = + case f a of + Synthesized tr2 sc2 uv2 rc2 b -> + Synthesized + { syn_trace = tr1 <> tr2 + , syn_scoped = sc1 <> sc2 + , syn_used_vals = uv1 <> uv2 + , syn_recursion_count = rc1 <> rc2 + , syn_val = b + } + mapTrace :: (Trace -> Trace) -> Synthesized a -> Synthesized a mapTrace f (Synthesized tr sc uv rc a) = Synthesized (f tr) sc uv rc a @@ -418,10 +459,12 @@ , ctxModuleFuncs :: [(OccName, CType)] -- ^ Everything defined in the current module , ctxConfig :: Config - , ctxKnownThings :: KnownThings , ctxInstEnvs :: InstEnvs , ctxFamInstEnvs :: FamInstEnvs , ctxTheta :: Set CType + , ctx_hscEnv :: HscEnv + , ctx_occEnv :: OccEnv [GlobalRdrElt] + , ctx_module :: Module } instance Show Context where @@ -435,14 +478,6 @@ ------------------------------------------------------------------------------ --- | Things we'd like to look up, that don't exist in TysWiredIn. -data KnownThings = KnownThings - { kt_semigroup :: Class - , kt_monoid :: Class - } - - ------------------------------------------------------------------------------- -- | An empty context emptyContext :: Context emptyContext @@ -450,15 +485,17 @@ { ctxDefiningFuncs = mempty , ctxModuleFuncs = mempty , ctxConfig = emptyConfig - , ctxKnownThings = error "empty known things from emptyContext" , ctxFamInstEnvs = mempty , ctxInstEnvs = InstEnvs mempty mempty mempty , ctxTheta = mempty + , ctx_hscEnv = error "empty hsc env from emptyContext" + , ctx_occEnv = emptyOccEnv + , ctx_module = error "empty module from emptyContext" } newtype Rose a = Rose (Tree a) - deriving stock (Eq, Functor, Generic) + deriving stock (Eq, Functor, Generic, Data, Typeable) instance Show (Rose String) where show = unlines . dropEveryOther . lines . drawTree . coerce @@ -502,16 +539,18 @@ data UserFacingMessage - = TacticErrors + = NotEnoughGas + | TacticErrors | TimedOut | NothingToDo | InfrastructureError Text deriving Eq instance Show UserFacingMessage where - show TacticErrors = "Wingman couldn't find a solution" - show TimedOut = "Wingman timed out while trying to find a solution" - show NothingToDo = "Nothing to do" + show NotEnoughGas = "Wingman ran out of gas when trying to find a solution. \nTry increasing the `auto_gas` setting." + show TacticErrors = "Wingman couldn't find a solution" + show TimedOut = "Wingman timed out while trying to find a solution" + show NothingToDo = "Nothing to do" show (InfrastructureError t) = "Internal error: " <> T.unpack t diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs --- a/test/AutoTupleSpec.hs +++ b/test/AutoTupleSpec.hs @@ -2,17 +2,18 @@ module AutoTupleSpec where -import Data.Either (isRight) -import Wingman.Judgements (mkFirstJudgement) -import Wingman.Machinery -import Wingman.Tactics (auto') -import Wingman.Types -import OccName (mkVarOcc) -import Test.Hspec -import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) -import TysWiredIn (mkBoxedTupleTy) +import Data.Either (isRight) +import OccName (mkVarOcc) +import System.IO.Unsafe +import Test.Hspec +import Test.QuickCheck +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) +import Wingman.Judgements (mkFirstJudgement) +import Wingman.Machinery +import Wingman.Tactics (auto') +import Wingman.Types spec :: Spec @@ -33,14 +34,15 @@ <$> randomGroups vars pure $ -- We should always be able to find a solution - runTactic - emptyContext - (mkFirstJudgement + unsafePerformIO + (runTactic emptyContext - (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type) - True - out_type) - (auto' $ n * 2) `shouldSatisfy` isRight + (mkFirstJudgement + emptyContext + (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type) + True + out_type) + (auto' $ n * 2)) `shouldSatisfy` isRight randomGroups :: [a] -> Gen [[a]] diff --git a/test/CodeAction/AutoSpec.hs b/test/CodeAction/AutoSpec.hs --- a/test/CodeAction/AutoSpec.hs +++ b/test/CodeAction/AutoSpec.hs @@ -47,6 +47,8 @@ autoTest 2 17 "AutoInfixApply" autoTest 2 19 "AutoInfixApplyMany" autoTest 2 25 "AutoInfixInfix" + autoTest 19 12 "AutoTypeLevel" + autoTest 11 9 "AutoForallClassMethod" failing "flaky in CI" $ autoTest 2 11 "GoldenApplicativeThen" @@ -82,6 +84,7 @@ describe "messages" $ do - mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors - mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors + mkShowMessageTest Auto "" 2 8 "MessageForallA" TacticErrors + mkShowMessageTest Auto "" 7 8 "MessageCantUnify" TacticErrors + mkShowMessageTest Auto "" 12 8 "MessageNotEnoughGas" NotEnoughGas diff --git a/test/CodeAction/DestructSpec.hs b/test/CodeAction/DestructSpec.hs --- a/test/CodeAction/DestructSpec.hs +++ b/test/CodeAction/DestructSpec.hs @@ -35,3 +35,85 @@ destructTest "a" 7 17 "LayoutSplitPattern" destructTest "a" 8 26 "LayoutSplitPatSyn" + describe "providers" $ do + mkTest + "Produces destruct and homomorphism code actions" + "T2" 2 21 + [ (id, Destruct, "eab") + , (id, Homomorphism, "eab") + , (not, DestructPun, "eab") + ] + + mkTest + "Won't suggest homomorphism on the wrong type" + "T2" 8 8 + [ (not, Homomorphism, "global") + ] + + mkTest + "Produces (homomorphic) lambdacase code actions" + "T3" 4 24 + [ (id, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + + mkTest + "Produces lambdacase code actions" + "T3" 7 13 + [ (id, DestructLambdaCase, "") + ] + + mkTest + "Doesn't suggest lambdacase without -XLambdaCase" + "T2" 11 25 + [ (not, DestructLambdaCase, "") + ] + + mkTest + "Doesn't suggest destruct if already destructed" + "ProvideAlreadyDestructed" 6 18 + [ (not, Destruct, "x") + ] + + mkTest + "...but does suggest destruct if destructed in a different branch" + "ProvideAlreadyDestructed" 9 7 + [ (id, Destruct, "x") + ] + + mkTest + "Doesn't suggest destruct on class methods" + "ProvideLocalHyOnly" 2 12 + [ (not, Destruct, "mempty") + ] + + mkTest + "Suggests homomorphism if the domain is bigger than the codomain" + "ProviderHomomorphism" 12 13 + [ (id, Homomorphism, "g") + ] + + mkTest + "Doesn't suggest homomorphism if the domain is smaller than the codomain" + "ProviderHomomorphism" 15 14 + [ (not, Homomorphism, "g") + , (id, Destruct, "g") + ] + + mkTest + "Suggests lambda homomorphism if the domain is bigger than the codomain" + "ProviderHomomorphism" 18 14 + [ (id, HomomorphismLambdaCase, "") + ] + + mkTest + "Doesn't suggest lambda homomorphism if the domain is smaller than the codomain" + "ProviderHomomorphism" 21 15 + [ (not, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + + -- test layouts that maintain user-written fixities + destructTest "b" 3 13 "LayoutInfixKeep" + destructTest "b" 2 12 "LayoutPrefixKeep" + diff --git a/test/CodeAction/RunMetaprogramSpec.hs b/test/CodeAction/RunMetaprogramSpec.hs --- a/test/CodeAction/RunMetaprogramSpec.hs +++ b/test/CodeAction/RunMetaprogramSpec.hs @@ -20,6 +20,7 @@ #if __GLASGOW_HASKELL__ >= 808 describe "beginMetaprogram" $ do goldenTest BeginMetaprogram "" 1 7 "MetaBegin" + goldenTest BeginMetaprogram "" 1 9 "MetaBeginNoWildify" #endif describe "golden" $ do @@ -33,4 +34,10 @@ metaTest 11 11 "MetaUseMethod" metaTest 9 38 "MetaCataCollapse" metaTest 7 16 "MetaCataCollapseUnary" + metaTest 10 32 "MetaCataAST" + metaTest 6 46 "MetaPointwise" + metaTest 4 28 "MetaUseSymbol" + metaTest 7 53 "MetaDeepOf" + metaTest 2 34 "MetaWithArg" + metaTest 2 12 "IntrosTooMany" diff --git a/test/CodeLens/EmptyCaseSpec.hs b/test/CodeLens/EmptyCaseSpec.hs --- a/test/CodeLens/EmptyCaseSpec.hs +++ b/test/CodeLens/EmptyCaseSpec.hs @@ -9,6 +9,7 @@ spec :: Spec spec = do let test = mkCodeLensTest + noTest = mkNoCodeLensTest describe "golden" $ do test "EmptyCaseADT" @@ -17,4 +18,8 @@ test "EmptyCaseNested" test "EmptyCaseApply" test "EmptyCaseGADT" + test "EmptyCaseLamCase" + + describe "no code lenses" $ do + noTest "EmptyCaseSpuriousGADT" diff --git a/test/ProviderSpec.hs b/test/ProviderSpec.hs --- a/test/ProviderSpec.hs +++ b/test/ProviderSpec.hs @@ -14,55 +14,9 @@ "T1" 2 14 [ (id, Intros, "") ] - mkTest - "Produces destruct and homomorphism code actions" - "T2" 2 21 - [ (id, Destruct, "eab") - , (id, Homomorphism, "eab") - , (not, DestructPun, "eab") - ] - mkTest - "Won't suggest homomorphism on the wrong type" - "T2" 8 8 - [ (not, Homomorphism, "global") - ] + mkTest "Won't suggest intros on the wrong type" "T2" 8 8 [ (not, Intros, "") ] - mkTest - "Produces (homomorphic) lambdacase code actions" - "T3" 4 24 - [ (id, HomomorphismLambdaCase, "") - , (id, DestructLambdaCase, "") - ] - mkTest - "Produces lambdacase code actions" - "T3" 7 13 - [ (id, DestructLambdaCase, "") - ] - mkTest - "Doesn't suggest lambdacase without -XLambdaCase" - "T2" 11 25 - [ (not, DestructLambdaCase, "") - ] - - mkTest - "Doesn't suggest destruct if already destructed" - "ProvideAlreadyDestructed" 6 18 - [ (not, Destruct, "x") - ] - - mkTest - "...but does suggest destruct if destructed in a different branch" - "ProvideAlreadyDestructed" 9 7 - [ (id, Destruct, "x") - ] - - mkTest - "Doesn't suggest destruct on class methods" - "ProvideLocalHyOnly" 2 12 - [ (not, Destruct, "mempty") - ] - diff --git a/test/UnificationSpec.hs b/test/UnificationSpec.hs --- a/test/UnificationSpec.hs +++ b/test/UnificationSpec.hs @@ -16,7 +16,7 @@ import Type (mkTyVarTy) import TysPrim (alphaTyVars) import TysWiredIn (mkBoxedTupleTy) -import Wingman.Machinery +import Wingman.GHC import Wingman.Types diff --git a/test/Utils.hs b/test/Utils.hs --- a/test/Utils.hs +++ b/test/Utils.hs @@ -15,12 +15,11 @@ import Data.Aeson import Data.Foldable import Data.Function (on) -import qualified Data.Map as M +import Data.IORef (writeIORef) import Data.Maybe import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T -import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic as Tactic import Language.LSP.Types import Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title) @@ -55,6 +54,19 @@ codeActionTitle (InR(CodeAction title _ _ _ _ _ _ _)) = Just title +resetGlobalHoleRef :: IO () +resetGlobalHoleRef = writeIORef globalHoleRef 0 + + +runSessionForTactics :: Session a -> IO a +runSessionForTactics = + runSessionWithServer' + [plugin] + def + (def { messageTimeout = 5 } ) + fullCaps + tacticPath + ------------------------------------------------------------------------------ -- | Make a tactic unit test. mkTest @@ -69,7 +81,8 @@ ) -- ^ A collection of (un)expected code actions. -> SpecWith (Arg Bool) mkTest name fp line col ts = it name $ do - runSessionWithServer plugin tacticPath $ do + resetGlobalHoleRef + runSessionForTactics $ do doc <- openDoc (fp <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col @@ -91,7 +104,8 @@ -> SpecWith () mkGoldenTest eq tc occ line col input = it (input <> " (golden)") $ do - runSessionWithServer plugin tacticPath $ do + resetGlobalHoleRef + runSessionForTactics $ do doc <- openDoc (input <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col @@ -113,7 +127,8 @@ -> SpecWith () mkCodeLensTest input = it (input <> " (golden)") $ do - runSessionWithServer plugin tacticPath $ do + resetGlobalHoleRef + runSessionForTactics $ do doc <- openDoc (input <.> "hs") "haskell" _ <- waitForDiagnostics lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc @@ -129,7 +144,22 @@ liftIO $ edited `shouldBe` expected +------------------------------------------------------------------------------ +-- | A test that no code lenses can be run in the file +mkNoCodeLensTest + :: FilePath + -> SpecWith () +mkNoCodeLensTest input = + it (input <> " (no code lenses)") $ do + resetGlobalHoleRef + runSessionForTactics $ do + doc <- openDoc (input <.> "hs") "haskell" + _ <- waitForDiagnostics + lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc + liftIO $ lenses `shouldBe` [] + + isWingmanLens :: CodeLens -> Bool isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _) = T.isInfixOf ":tactics:" cmd @@ -146,7 +176,8 @@ -> SpecWith () mkShowMessageTest tc occ line col input ufm = it (input <> " (golden)") $ do - runSessionWithServer plugin tacticPath $ do + resetGlobalHoleRef + runSessionForTactics $ do doc <- openDoc (input <.> "hs") "haskell" _ <- waitForDiagnostics actions <- getCodeActions doc $ pointRange line col diff --git a/test/golden/AutoForallClassMethod.expected.hs b/test/golden/AutoForallClassMethod.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoForallClassMethod.expected.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +import Data.Functor.Contravariant + +class Semigroupal cat t1 t2 to f where + combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y')) + +comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d) +comux = case combine of { (Op f) -> f } + diff --git a/test/golden/AutoForallClassMethod.hs b/test/golden/AutoForallClassMethod.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoForallClassMethod.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +import Data.Functor.Contravariant + +class Semigroupal cat t1 t2 to f where + combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y')) + +comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d) +comux = _ + diff --git a/test/golden/AutoTypeLevel.expected.hs b/test/golden/AutoTypeLevel.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoTypeLevel.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 _ hl') = lookMeUp ea' hl' + diff --git a/test/golden/AutoTypeLevel.hs b/test/golden/AutoTypeLevel.hs new file mode 100644 --- /dev/null +++ b/test/golden/AutoTypeLevel.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 = _ + diff --git a/test/golden/DestructAllAnd.expected.hs b/test/golden/DestructAllAnd.expected.hs --- a/test/golden/DestructAllAnd.expected.hs +++ b/test/golden/DestructAllAnd.expected.hs @@ -1,5 +1,5 @@ and :: Bool -> Bool -> Bool -and False False = _ -and False True = _ -and True False = _ -and True True = _ +and False False = _w0 +and False True = _w1 +and True False = _w2 +and True True = _w3 diff --git a/test/golden/DestructAllFunc.expected.hs b/test/golden/DestructAllFunc.expected.hs --- a/test/golden/DestructAllFunc.expected.hs +++ b/test/golden/DestructAllFunc.expected.hs @@ -1,4 +1,4 @@ has_a_func :: Bool -> (a -> b) -> Bool -has_a_func False y = _ -has_a_func True y = _ +has_a_func False y = _w0 +has_a_func True y = _w1 diff --git a/test/golden/DestructAllGADTEvidence.expected.hs b/test/golden/DestructAllGADTEvidence.expected.hs --- a/test/golden/DestructAllGADTEvidence.expected.hs +++ b/test/golden/DestructAllGADTEvidence.expected.hs @@ -16,6 +16,6 @@ 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') = _ +lookMeUp AtZ (HCons t hl') = _w0 +lookMeUp (AtS ea') (HCons t hl') = _w1 diff --git a/test/golden/DestructAllMany.expected.hs b/test/golden/DestructAllMany.expected.hs --- a/test/golden/DestructAllMany.expected.hs +++ b/test/golden/DestructAllMany.expected.hs @@ -1,27 +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 = _ +many () (Left a) False Nothing A = _w0 +many () (Left a) False Nothing B = _w1 +many () (Left a) False Nothing C = _w2 +many () (Left a) False (Just abc') A = _w3 +many () (Left a) False (Just abc') B = _w4 +many () (Left a) False (Just abc') C = _w5 +many () (Left a) True Nothing A = _w6 +many () (Left a) True Nothing B = _w7 +many () (Left a) True Nothing C = _w8 +many () (Left a) True (Just abc') A = _w9 +many () (Left a) True (Just abc') B = _wa +many () (Left a) True (Just abc') C = _wb +many () (Right b') False Nothing A = _wc +many () (Right b') False Nothing B = _wd +many () (Right b') False Nothing C = _we +many () (Right b') False (Just abc') A = _wf +many () (Right b') False (Just abc') B = _wg +many () (Right b') False (Just abc') C = _wh +many () (Right b') True Nothing A = _wi +many () (Right b') True Nothing B = _wj +many () (Right b') True Nothing C = _wk +many () (Right b') True (Just abc') A = _wl +many () (Right b') True (Just abc') B = _wm +many () (Right b') True (Just abc') C = _wn diff --git a/test/golden/DestructAllNonVarTopMatch.expected.hs b/test/golden/DestructAllNonVarTopMatch.expected.hs --- a/test/golden/DestructAllNonVarTopMatch.expected.hs +++ b/test/golden/DestructAllNonVarTopMatch.expected.hs @@ -1,6 +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 = _ +and (a, b) False False = _w0 +and (a, b) False True = _w1 +and (a, b) True False = _w2 +and (a, b) True True = _w3 diff --git a/test/golden/DestructCthulhu.expected.hs b/test/golden/DestructCthulhu.expected.hs --- a/test/golden/DestructCthulhu.expected.hs +++ b/test/golden/DestructCthulhu.expected.hs @@ -28,27 +28,27 @@ 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') = _ +cthulhu ID = _w0 +cthulhu (Comp fp' fp_rcyb) = _w1 +cthulhu Copy = _w2 +cthulhu Consume = _w3 +cthulhu Swap = _w4 +cthulhu SwapE = _w5 +cthulhu Fst = _w6 +cthulhu Snd = _w7 +cthulhu InjectL = _w8 +cthulhu InjectR = _w9 +cthulhu Unify = _wa +cthulhu (First fp') = _wb +cthulhu (Second fp') = _wc +cthulhu (Alongside fp' fp_rca'b') = _wd +cthulhu (Fanout fp' fp_rcab') = _we +cthulhu (Left' fp') = _wf +cthulhu (Right' fp') = _wg +cthulhu (EitherOf fp' fp_rca'b') = _wh +cthulhu (Fanin fp' fp_rca'b) = _wi +cthulhu (LiftC cab) = _wj +cthulhu Zero = _wk +cthulhu (Plus fp' fp_rcab) = _wl +cthulhu (Unleft fp') = _wm +cthulhu (Unright fp') = _wn diff --git a/test/golden/DestructDataFam.expected.hs b/test/golden/DestructDataFam.expected.hs --- a/test/golden/DestructDataFam.expected.hs +++ b/test/golden/DestructDataFam.expected.hs @@ -4,5 +4,5 @@ data instance Yo = Heya Int test :: Yo -> Int -test (Heya n) = _ +test (Heya n) = _w0 diff --git a/test/golden/DestructPun.expected.hs b/test/golden/DestructPun.expected.hs --- a/test/golden/DestructPun.expected.hs +++ b/test/golden/DestructPun.expected.hs @@ -3,6 +3,6 @@ data Foo = Foo { a :: Bool, b :: Bool } -foo Foo {a = False, b} = _ -foo Foo {a = True, b} = _ +foo Foo {a = False, b} = _w0 +foo Foo {a = True, b} = _w1 diff --git a/test/golden/DestructTyFam.expected.hs b/test/golden/DestructTyFam.expected.hs --- a/test/golden/DestructTyFam.expected.hs +++ b/test/golden/DestructTyFam.expected.hs @@ -4,6 +4,6 @@ Yo = Bool test :: Yo -> Int -test False = _ -test True = _ +test False = _w0 +test True = _w1 diff --git a/test/golden/DestructTyToDataFam.expected.hs b/test/golden/DestructTyToDataFam.expected.hs --- a/test/golden/DestructTyToDataFam.expected.hs +++ b/test/golden/DestructTyToDataFam.expected.hs @@ -14,5 +14,5 @@ data instance Yo = Heya Int test :: T1 Bool -> Int -test (Heya n) = _ +test (Heya n) = _w0 diff --git a/test/golden/EmptyCaseLamCase.expected.hs b/test/golden/EmptyCaseLamCase.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseLamCase.expected.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LambdaCase #-} + +test :: Bool -> Bool +test = \case + False -> _ + True -> _ diff --git a/test/golden/EmptyCaseLamCase.hs b/test/golden/EmptyCaseLamCase.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseLamCase.hs @@ -0,0 +1,4 @@ +{-# LANGUAGE LambdaCase #-} + +test :: Bool -> Bool +test = \case diff --git a/test/golden/EmptyCaseSpuriousGADT.hs b/test/golden/EmptyCaseSpuriousGADT.hs new file mode 100644 --- /dev/null +++ b/test/golden/EmptyCaseSpuriousGADT.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-} + +data Foo a where + Foo :: Foo Int + +foo :: Foo Bool -> () +foo x = case x of + diff --git a/test/golden/GoldenGADTDestruct.expected.hs b/test/golden/GoldenGADTDestruct.expected.hs --- a/test/golden/GoldenGADTDestruct.expected.hs +++ b/test/golden/GoldenGADTDestruct.expected.hs @@ -4,4 +4,4 @@ MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT ctxGADT :: CtxGADT -> String -ctxGADT (MkCtxGADT a) = _ +ctxGADT (MkCtxGADT a) = _w0 diff --git a/test/golden/GoldenGADTDestructCoercion.expected.hs b/test/golden/GoldenGADTDestructCoercion.expected.hs --- a/test/golden/GoldenGADTDestructCoercion.expected.hs +++ b/test/golden/GoldenGADTDestructCoercion.expected.hs @@ -5,4 +5,4 @@ E :: forall a b. (b ~ a, Ord a) => b -> E a [a] ctxGADT :: E a b -> String -ctxGADT (E b) = _ +ctxGADT (E b) = _w0 diff --git a/test/golden/GoldenIntros.expected.hs b/test/golden/GoldenIntros.expected.hs --- a/test/golden/GoldenIntros.expected.hs +++ b/test/golden/GoldenIntros.expected.hs @@ -1,2 +1,2 @@ blah :: Int -> Bool -> (a -> b) -> String -> Int -blah n b fab s = _ +blah n b fab s = _w0 diff --git a/test/golden/IntrosTooMany.expected.hs b/test/golden/IntrosTooMany.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntrosTooMany.expected.hs @@ -0,0 +1,2 @@ +too_many :: a -> b -> c +too_many a b = _w0 diff --git a/test/golden/IntrosTooMany.hs b/test/golden/IntrosTooMany.hs new file mode 100644 --- /dev/null +++ b/test/golden/IntrosTooMany.hs @@ -0,0 +1,2 @@ +too_many :: a -> b -> c +too_many = [wingman| intros a b c d e f g h i j k l m n o p q r s t u v w x y z |] diff --git a/test/golden/KnownBigSemigroup.expected.hs b/test/golden/KnownBigSemigroup.expected.hs --- a/test/golden/KnownBigSemigroup.expected.hs +++ b/test/golden/KnownBigSemigroup.expected.hs @@ -3,7 +3,7 @@ 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 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/KnownCounterfactualSemigroup.expected.hs b/test/golden/KnownCounterfactualSemigroup.expected.hs --- a/test/golden/KnownCounterfactualSemigroup.expected.hs +++ b/test/golden/KnownCounterfactualSemigroup.expected.hs @@ -3,5 +3,5 @@ data Semi = Semi [String] Int instance Semigroup Int => Semigroup Semi where - (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) (n <> i) + (Semi ss n) <> (Semi strs i) = Semi (ss <> strs) (n <> i) diff --git a/test/golden/KnownDestructedSemigroup.expected.hs b/test/golden/KnownDestructedSemigroup.expected.hs --- a/test/golden/KnownDestructedSemigroup.expected.hs +++ b/test/golden/KnownDestructedSemigroup.expected.hs @@ -1,5 +1,5 @@ data Test a = Test [a] instance Semigroup (Test a) where - (<>) (Test a) (Test c) = Test (a <> c) + (Test a) <> (Test c) = Test (a <> c) diff --git a/test/golden/KnownMissingMonoid.expected.hs b/test/golden/KnownMissingMonoid.expected.hs --- a/test/golden/KnownMissingMonoid.expected.hs +++ b/test/golden/KnownMissingMonoid.expected.hs @@ -4,5 +4,5 @@ (<>) = undefined instance Monoid (Mono a) where - mempty = Monoid mempty _ + mempty = Monoid mempty _w0 diff --git a/test/golden/KnownMissingSemigroup.expected.hs b/test/golden/KnownMissingSemigroup.expected.hs --- a/test/golden/KnownMissingSemigroup.expected.hs +++ b/test/golden/KnownMissingSemigroup.expected.hs @@ -1,5 +1,5 @@ data Semi = Semi [String] Int instance Semigroup Semi where - (<>) (Semi ss n) (Semi strs i) = Semi (ss <> strs) _ + (Semi ss n) <> (Semi strs i) = Semi (ss <> strs) _w0 diff --git a/test/golden/KnownModuleInstanceSemigroup.expected.hs b/test/golden/KnownModuleInstanceSemigroup.expected.hs --- a/test/golden/KnownModuleInstanceSemigroup.expected.hs +++ b/test/golden/KnownModuleInstanceSemigroup.expected.hs @@ -7,6 +7,6 @@ data Bar = Bar Foo Foo instance Semigroup Bar where - (<>) (Bar foo foo') (Bar foo2 foo3) + (Bar foo foo') <> (Bar foo2 foo3) = Bar (foo <> foo2) (foo' <> foo3) diff --git a/test/golden/KnownThetaSemigroup.expected.hs b/test/golden/KnownThetaSemigroup.expected.hs --- a/test/golden/KnownThetaSemigroup.expected.hs +++ b/test/golden/KnownThetaSemigroup.expected.hs @@ -1,5 +1,5 @@ data Semi a = Semi a instance Semigroup a => Semigroup (Semi a) where - (<>) (Semi a) (Semi a') = Semi (a <> a') + (Semi a) <> (Semi a') = Semi (a <> a') diff --git a/test/golden/LayoutBind.expected.hs b/test/golden/LayoutBind.expected.hs --- a/test/golden/LayoutBind.expected.hs +++ b/test/golden/LayoutBind.expected.hs @@ -2,7 +2,7 @@ test b = do putStrLn "hello" case b of - False -> _ - True -> _ + False -> _w0 + True -> _w1 pure () diff --git a/test/golden/LayoutDollarApp.expected.hs b/test/golden/LayoutDollarApp.expected.hs --- a/test/golden/LayoutDollarApp.expected.hs +++ b/test/golden/LayoutDollarApp.expected.hs @@ -1,5 +1,5 @@ test :: Bool -> Bool test b = id $ (case b of - False -> _ - True -> _) + False -> _w0 + True -> _w1) diff --git a/test/golden/LayoutInfixKeep.expected.hs b/test/golden/LayoutInfixKeep.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutInfixKeep.expected.hs @@ -0,0 +1,5 @@ +-- keep layout that was written by the user in infix +foo :: Bool -> a -> a +False `foo` a = _w0 +True `foo` a = _w1 + diff --git a/test/golden/LayoutInfixKeep.hs b/test/golden/LayoutInfixKeep.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutInfixKeep.hs @@ -0,0 +1,4 @@ +-- keep layout that was written by the user in infix +foo :: Bool -> a -> a +b `foo` a = _ + diff --git a/test/golden/LayoutLam.expected.hs b/test/golden/LayoutLam.expected.hs --- a/test/golden/LayoutLam.expected.hs +++ b/test/golden/LayoutLam.expected.hs @@ -1,5 +1,5 @@ test :: Bool -> Bool test = \b -> case b of - False -> _ - True -> _ + False -> _w0 + True -> _w1 diff --git a/test/golden/LayoutOpApp.expected.hs b/test/golden/LayoutOpApp.expected.hs --- a/test/golden/LayoutOpApp.expected.hs +++ b/test/golden/LayoutOpApp.expected.hs @@ -1,4 +1,4 @@ test :: Bool -> Bool test b = True && (case b of - False -> _ - True -> _) + False -> _w0 + True -> _w1) diff --git a/test/golden/LayoutPrefixKeep.expected.hs b/test/golden/LayoutPrefixKeep.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutPrefixKeep.expected.hs @@ -0,0 +1,4 @@ +(-/) :: Bool -> a -> a +(-/) False a = _w0 +(-/) True a = _w1 + diff --git a/test/golden/LayoutPrefixKeep.hs b/test/golden/LayoutPrefixKeep.hs new file mode 100644 --- /dev/null +++ b/test/golden/LayoutPrefixKeep.hs @@ -0,0 +1,3 @@ +(-/) :: Bool -> a -> a +(-/) b a = _ + diff --git a/test/golden/LayoutRec.expected.hs b/test/golden/LayoutRec.expected.hs --- a/test/golden/LayoutRec.expected.hs +++ b/test/golden/LayoutRec.expected.hs @@ -1,5 +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 -> _} +p = Pair {pa = _, pb = \ a b c -> _w0} diff --git a/test/golden/LayoutSplitClass.expected.hs b/test/golden/LayoutSplitClass.expected.hs --- a/test/golden/LayoutSplitClass.expected.hs +++ b/test/golden/LayoutSplitClass.expected.hs @@ -1,5 +1,5 @@ class Test a where test :: Bool -> a - test False = _ - test True = _ + test False = _w0 + test True = _w1 diff --git a/test/golden/LayoutSplitGuard.expected.hs b/test/golden/LayoutSplitGuard.expected.hs --- a/test/golden/LayoutSplitGuard.expected.hs +++ b/test/golden/LayoutSplitGuard.expected.hs @@ -1,5 +1,5 @@ test :: Bool -> Bool -> Bool test a b | a = case b of - False -> _ - True -> _ + False -> _w0 + True -> _w1 diff --git a/test/golden/LayoutSplitIn.expected.hs b/test/golden/LayoutSplitIn.expected.hs --- a/test/golden/LayoutSplitIn.expected.hs +++ b/test/golden/LayoutSplitIn.expected.hs @@ -1,5 +1,5 @@ test :: a test = let a = (1,"bbb") - in case a of { (n, s) -> _ } + in case a of { (n, s) -> _w0 } diff --git a/test/golden/LayoutSplitLet.expected.hs b/test/golden/LayoutSplitLet.expected.hs --- a/test/golden/LayoutSplitLet.expected.hs +++ b/test/golden/LayoutSplitLet.expected.hs @@ -1,7 +1,7 @@ test :: a test = let t :: Bool -> a - t False = _ - t True = _ + t False = _w0 + t True = _w1 in _ diff --git a/test/golden/LayoutSplitPatSyn.expected.hs b/test/golden/LayoutSplitPatSyn.expected.hs --- a/test/golden/LayoutSplitPatSyn.expected.hs +++ b/test/golden/LayoutSplitPatSyn.expected.hs @@ -5,7 +5,7 @@ test :: Maybe [Bool] -> Maybe Bool -test (JustSingleton False) = _ -test (JustSingleton True) = _ +test (JustSingleton False) = _w0 +test (JustSingleton True) = _w1 diff --git a/test/golden/LayoutSplitPattern.expected.hs b/test/golden/LayoutSplitPattern.expected.hs --- a/test/golden/LayoutSplitPattern.expected.hs +++ b/test/golden/LayoutSplitPattern.expected.hs @@ -4,6 +4,6 @@ pattern Blah a = Just a test :: Maybe Bool -> a -test (Blah False) = _ -test (Blah True) = _ +test (Blah False) = _w0 +test (Blah True) = _w1 diff --git a/test/golden/LayoutSplitViewPat.expected.hs b/test/golden/LayoutSplitViewPat.expected.hs --- a/test/golden/LayoutSplitViewPat.expected.hs +++ b/test/golden/LayoutSplitViewPat.expected.hs @@ -1,6 +1,6 @@ {-# LANGUAGE ViewPatterns #-} splitLookup :: [(Int, String)] -> String -splitLookup (lookup 5 -> Nothing) = _ -splitLookup (lookup 5 -> (Just s)) = _ +splitLookup (lookup 5 -> Nothing) = _w0 +splitLookup (lookup 5 -> (Just s)) = _w1 diff --git a/test/golden/LayoutSplitWhere.expected.hs b/test/golden/LayoutSplitWhere.expected.hs --- a/test/golden/LayoutSplitWhere.expected.hs +++ b/test/golden/LayoutSplitWhere.expected.hs @@ -8,7 +8,7 @@ foo = putStrLn "Hi" bar :: A -> IO () - bar A = _ - bar B = _ - bar C = _ + bar A = _w0 + bar B = _w1 + bar C = _w2 diff --git a/test/golden/MessageNotEnoughGas.hs b/test/golden/MessageNotEnoughGas.hs new file mode 100644 --- /dev/null +++ b/test/golden/MessageNotEnoughGas.hs @@ -0,0 +1,13 @@ +test + :: (a1 -> a2) + -> (a2 -> a3) + -> (a3 -> a4) + -> (a4 -> a5) + -> (a5 -> a6) + -> (a6 -> a7) + -> (a7 -> a8) + -> (a8 -> a9) + -> (a9 -> a10) + -> a1 -> a10 +test = _ + diff --git a/test/golden/MetaBeginNoWildify.expected.hs b/test/golden/MetaBeginNoWildify.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBeginNoWildify.expected.hs @@ -0,0 +1,2 @@ +foo v = [wingman||] + diff --git a/test/golden/MetaBeginNoWildify.hs b/test/golden/MetaBeginNoWildify.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaBeginNoWildify.hs @@ -0,0 +1,2 @@ +foo v = _ + diff --git a/test/golden/MetaBindOne.expected.hs b/test/golden/MetaBindOne.expected.hs --- a/test/golden/MetaBindOne.expected.hs +++ b/test/golden/MetaBindOne.expected.hs @@ -1,2 +1,2 @@ foo :: a -> (a, a) -foo a = (a, _) +foo a = (a, _w0) diff --git a/test/golden/MetaCataAST.expected.hs b/test/golden/MetaCataAST.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataAST.expected.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE GADTs #-} + +data AST a where + BoolLit :: Bool -> AST Bool + IntLit :: Int -> AST Int + If :: AST Bool -> AST a -> AST a -> AST a + Equal :: AST a -> AST a -> AST Bool + +eval :: AST a -> a +eval (BoolLit b) = b +eval (IntLit n) = n +eval (If ast ast' ast_a) + = let + ast_c = eval ast + ast'_c = eval ast' + ast_a_c = eval ast_a + in _w0 ast_c ast'_c ast_a_c +eval (Equal ast ast') + = let + ast_c = eval ast + ast'_c = eval ast' + in _w1 ast_c ast'_c + diff --git a/test/golden/MetaCataAST.hs b/test/golden/MetaCataAST.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaCataAST.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE GADTs #-} + +data AST a where + BoolLit :: Bool -> AST Bool + IntLit :: Int -> AST Int + If :: AST Bool -> AST a -> AST a -> AST a + Equal :: AST a -> AST a -> AST Bool + +eval :: AST a -> a +eval = [wingman| intros x, cata x; collapse |] + diff --git a/test/golden/MetaCataCollapse.expected.hs b/test/golden/MetaCataCollapse.expected.hs --- a/test/golden/MetaCataCollapse.expected.hs +++ b/test/golden/MetaCataCollapse.expected.hs @@ -10,5 +10,5 @@ = let fx_c = yo fx gx_c = yo gx - in _ fx_c gx_c + in _w0 fx_c gx_c diff --git a/test/golden/MetaDeepOf.expected.hs b/test/golden/MetaDeepOf.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaDeepOf.expected.hs @@ -0,0 +1,8 @@ +whats_it_deep_of + :: (a -> a) + -> [(Int, Either Bool (Maybe [a]))] + -> [(Int, Either Bool (Maybe [a]))] +-- The assumption here is necessary to tie-break in favor of the longest +-- nesting of fmaps. +whats_it_deep_of f = fmap (fmap (fmap (fmap (fmap f)))) + diff --git a/test/golden/MetaDeepOf.hs b/test/golden/MetaDeepOf.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaDeepOf.hs @@ -0,0 +1,8 @@ +whats_it_deep_of + :: (a -> a) + -> [(Int, Either Bool (Maybe [a]))] + -> [(Int, Either Bool (Maybe [a]))] +-- The assumption here is necessary to tie-break in favor of the longest +-- nesting of fmaps. +whats_it_deep_of f = [wingman| nested fmap, assumption |] + diff --git a/test/golden/MetaPointwise.expected.hs b/test/golden/MetaPointwise.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaPointwise.expected.hs @@ -0,0 +1,8 @@ +import Data.Monoid + +data Foo = Foo (Sum Int) (Sum Int) + +mappend2 :: Foo -> Foo -> Foo +mappend2 (Foo sum sum') (Foo sum2 sum3) + = Foo (mappend sum sum2) (mappend sum' sum3) + diff --git a/test/golden/MetaPointwise.hs b/test/golden/MetaPointwise.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaPointwise.hs @@ -0,0 +1,7 @@ +import Data.Monoid + +data Foo = Foo (Sum Int) (Sum Int) + +mappend2 :: Foo -> Foo -> Foo +mappend2 = [wingman| intros f1 f2, destruct_all, ctor Foo; pointwise (use mappend); assumption|] + diff --git a/test/golden/MetaTry.expected.hs b/test/golden/MetaTry.expected.hs --- a/test/golden/MetaTry.expected.hs +++ b/test/golden/MetaTry.expected.hs @@ -1,2 +1,2 @@ foo :: a -> (b, a) -foo a = (_, a) +foo a = (_w0, a) diff --git a/test/golden/MetaTry.hs b/test/golden/MetaTry.hs --- a/test/golden/MetaTry.hs +++ b/test/golden/MetaTry.hs @@ -1,2 +1,2 @@ foo :: a -> (b, a) -foo a = [wingman| split; try assumption |] +foo a = [wingman| split; try (assumption) |] diff --git a/test/golden/MetaUseSymbol.expected.hs b/test/golden/MetaUseSymbol.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseSymbol.expected.hs @@ -0,0 +1,4 @@ +import Data.Monoid + +resolve :: Sum Int +resolve = _w0 <> _w1 diff --git a/test/golden/MetaUseSymbol.hs b/test/golden/MetaUseSymbol.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaUseSymbol.hs @@ -0,0 +1,4 @@ +import Data.Monoid + +resolve :: Sum Int +resolve = [wingman| use (<>) |] diff --git a/test/golden/MetaWithArg.expected.hs b/test/golden/MetaWithArg.expected.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaWithArg.expected.hs @@ -0,0 +1,2 @@ +wat :: a -> b +wat a = _w0 a diff --git a/test/golden/MetaWithArg.hs b/test/golden/MetaWithArg.hs new file mode 100644 --- /dev/null +++ b/test/golden/MetaWithArg.hs @@ -0,0 +1,2 @@ +wat :: a -> b +wat a = [wingman| with_arg, assumption |] diff --git a/test/golden/ProviderHomomorphism.hs b/test/golden/ProviderHomomorphism.hs new file mode 100644 --- /dev/null +++ b/test/golden/ProviderHomomorphism.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} + +data GADT a where + B1 :: GADT Bool + B2 :: GADT Bool + Int :: GADT Int + Var :: GADT a + + +hasHomo :: GADT Bool -> GADT a +hasHomo g = _ + +cantHomo :: GADT a -> GADT Int +cantHomo g = _ + +hasHomoLam :: GADT Bool -> GADT a +hasHomoLam = _ + +cantHomoLam :: GADT a -> GADT Int +cantHomoLam = _ + diff --git a/test/golden/PunGADT.expected.hs b/test/golden/PunGADT.expected.hs --- a/test/golden/PunGADT.expected.hs +++ b/test/golden/PunGADT.expected.hs @@ -8,5 +8,5 @@ split :: GADT a -> a -split GADT {blah, bar} = _ +split GADT {blah, bar} = _w0 diff --git a/test/golden/PunMany.expected.hs b/test/golden/PunMany.expected.hs --- a/test/golden/PunMany.expected.hs +++ b/test/golden/PunMany.expected.hs @@ -3,6 +3,6 @@ | Goodbye { a :: Int, b :: Bool, c :: Many } test :: Many -> Many -test Hello {world} = _ -test Goodbye {a, b, c} = _ +test Hello {world} = _w0 +test Goodbye {a, b, c} = _w1 diff --git a/test/golden/PunManyGADT.expected.hs b/test/golden/PunManyGADT.expected.hs --- a/test/golden/PunManyGADT.expected.hs +++ b/test/golden/PunManyGADT.expected.hs @@ -14,6 +14,6 @@ split :: GADT Bool -> a -split GADT {blah, bar} = _ -split Bar {zoo, baxter, another} = _ +split GADT {blah, bar} = _w0 +split Bar {zoo, baxter, another} = _w1 diff --git a/test/golden/PunShadowing.expected.hs b/test/golden/PunShadowing.expected.hs --- a/test/golden/PunShadowing.expected.hs +++ b/test/golden/PunShadowing.expected.hs @@ -1,5 +1,5 @@ data Bar = Bar { ax :: Int, bax :: Bool } bar :: () -> Bar -> Int -bar ax Bar {ax = n, bax} = _ +bar ax Bar {ax = n, bax} = _w0 diff --git a/test/golden/PunSimple.expected.hs b/test/golden/PunSimple.expected.hs --- a/test/golden/PunSimple.expected.hs +++ b/test/golden/PunSimple.expected.hs @@ -1,5 +1,5 @@ data Bar = Bar { ax :: Int, bax :: Bool } bar :: Bar -> Int -bar Bar {ax, bax} = _ +bar Bar {ax, bax} = _w0 diff --git a/test/golden/RefineCon.expected.hs b/test/golden/RefineCon.expected.hs --- a/test/golden/RefineCon.expected.hs +++ b/test/golden/RefineCon.expected.hs @@ -1,3 +1,3 @@ test :: ((), (b, c), d) -test = (_, _, _) +test = (_w0, _w1, _w2) diff --git a/test/golden/RefineGADT.expected.hs b/test/golden/RefineGADT.expected.hs --- a/test/golden/RefineGADT.expected.hs +++ b/test/golden/RefineGADT.expected.hs @@ -5,5 +5,5 @@ Two :: GADT Bool test :: z -> GADT Int -test z = One _ +test z = One _w0 diff --git a/test/golden/RefineIntro.expected.hs b/test/golden/RefineIntro.expected.hs --- a/test/golden/RefineIntro.expected.hs +++ b/test/golden/RefineIntro.expected.hs @@ -1,2 +1,2 @@ test :: a -> Either a b -test a = _ +test a = _w0 diff --git a/test/golden/RefineReader.expected.hs b/test/golden/RefineReader.expected.hs --- a/test/golden/RefineReader.expected.hs +++ b/test/golden/RefineReader.expected.hs @@ -1,5 +1,5 @@ newtype Reader r a = Reader (r -> a) test :: b -> Reader r a -test b = Reader _ +test b = Reader _w0 diff --git a/test/golden/SplitPattern.expected.hs b/test/golden/SplitPattern.expected.hs --- a/test/golden/SplitPattern.expected.hs +++ b/test/golden/SplitPattern.expected.hs @@ -4,9 +4,9 @@ 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 (Four b One) = _w0 +case_split (Four b (Two n)) = _w1 +case_split (Four b Three) = _w2 +case_split (Four b (Four b' adt)) = _w3 +case_split (Four b Five) = _w4 case_split Five = _ diff --git a/test/golden/UseConLeft.expected.hs b/test/golden/UseConLeft.expected.hs --- a/test/golden/UseConLeft.expected.hs +++ b/test/golden/UseConLeft.expected.hs @@ -1,3 +1,3 @@ test :: Either a b -test = Left _ +test = Left _w0 diff --git a/test/golden/UseConPair.expected.hs b/test/golden/UseConPair.expected.hs --- a/test/golden/UseConPair.expected.hs +++ b/test/golden/UseConPair.expected.hs @@ -1,2 +1,2 @@ test :: (a, b) -test = (_, _) +test = (_w0, _w1) diff --git a/test/golden/UseConRight.expected.hs b/test/golden/UseConRight.expected.hs --- a/test/golden/UseConRight.expected.hs +++ b/test/golden/UseConRight.expected.hs @@ -1,3 +1,3 @@ test :: Either a b -test = Right _ +test = Right _w0