diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal new file mode 100644 --- /dev/null +++ b/hls-tactics-plugin.cabal @@ -0,0 +1,97 @@ +cabal-version: 2.2 +category: Development +name: hls-tactics-plugin +version: 0.5.1.0 +synopsis: Tactics plugin for Haskell Language Server +description: Please see README.md +author: Sandy Maguire, Reed Mullanix +maintainer: sandy@sandymaguire.me +copyright: Sandy Maguire, Reed Mullanix +license: Apache-2.0 +license-file: LICENSE +build-type: Simple +-- extra-source-files: +-- README.md +-- ChangeLog.md + +flag pedantic + description: Enable -Werror + default: False + manual: True + +library + hs-source-dirs: src + exposed-modules: + Ide.Plugin.Tactic + Ide.Plugin.Tactic.Auto + Ide.Plugin.Tactic.CodeGen + Ide.Plugin.Tactic.Context + Ide.Plugin.Tactic.Debug + Ide.Plugin.Tactic.GHC + Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.KnownStrategies + Ide.Plugin.Tactic.KnownStrategies.QuickCheck + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Naming + Ide.Plugin.Tactic.Range + Ide.Plugin.Tactic.Tactics + Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.TestTypes + Ide.TreeTransform + + ghc-options: + -Wno-name-shadowing -Wredundant-constraints + if flag(pedantic) + ghc-options: -Werror + + build-depends: + , aeson + , base >=4.12 && <5 + , containers + , directory + , extra + , filepath + , fingertree + , generic-lens + , ghc + , ghc-boot-th + , ghc-exactprint + , ghc-source-gen + , ghcide >=0.1 + , haskell-lsp ^>=0.22 + , hls-plugin-api + , lens + , mtl + , refinery ^>=0.3 + , retrie >=0.1.1.0 + , shake >=0.17.5 + , syb + , text + , transformers + , deepseq + + default-language: Haskell2010 + +test-suite tests + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + AutoTupleSpec + UnificationSpec + hs-source-dirs: + test + ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N + build-depends: + QuickCheck + , base + , checkers + , hspec + , mtl + , hls-tactics-plugin + , hls-plugin-api + , hie-bios + , ghc + , containers + build-tool-depends: hspec-discover:hspec-discover + default-language: Haskell2010 + diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic.hs @@ -0,0 +1,368 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NumDecimals #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +-- | A plugin that uses tactics to synthesize code +module Ide.Plugin.Tactic + ( descriptor + , tacticTitle + , TacticCommand (..) + ) where + +import Control.Arrow +import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Data.Aeson +import Data.Coerce +import Data.Functor ((<&>)) +import Data.Generics.Aliases (mkQ) +import Data.Generics.Schemes (everything) +import Data.List +import Data.Map (Map) +import qualified Data.Map as M +import Data.Maybe +import Data.Monoid +import qualified Data.Set as S +import qualified Data.Text as T +import Data.Traversable +import Development.IDE.Core.PositionMapping +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Service (runAction) +import Development.IDE.Core.Shake (useWithStale, IdeState (..)) +import Development.IDE.GHC.Compat +import Development.IDE.GHC.Error (realSrcSpanToRange) +import Development.IDE.Spans.LocalBindings (getDefiningBindings) +import Development.Shake (Action) +import DynFlags (xopt) +import qualified FastString +import GHC.Generics (Generic) +import GHC.LanguageExtensions.Type (Extension (LambdaCase)) +import Ide.Plugin.Tactic.Auto +import Ide.Plugin.Tactic.Context +import Ide.Plugin.Tactic.GHC +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Range +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.TestTypes +import Ide.Plugin.Tactic.Types +import Ide.PluginUtils +import Ide.TreeTransform (transform, graft, useAnnotatedSource) +import Ide.Types +import Language.Haskell.LSP.Core (clientCapabilities) +import Language.Haskell.LSP.Types +import OccName +import SrcLoc (containsSpan) +import System.Timeout +import TcRnTypes (tcg_binds) + + +descriptor :: PluginId -> PluginDescriptor IdeState +descriptor plId = (defaultPluginDescriptor plId) + { pluginCommands + = fmap (\tc -> + PluginCommand + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd $ commandTactic tc)) + [minBound .. maxBound] + , pluginCodeActionProvider = Just codeActionProvider + } + +tacticDesc :: T.Text -> T.Text +tacticDesc name = "fill the hole using the " <> name <> " tactic" + +------------------------------------------------------------------------------ +-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS +-- UI. +type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] + + +------------------------------------------------------------------------------ +-- | Construct a 'CommandId' +tcCommandId :: TacticCommand -> CommandId +tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" + + +------------------------------------------------------------------------------ +-- | The name of the command for the LS. +tcCommandName :: TacticCommand -> T.Text +tcCommandName = T.pack . show + +------------------------------------------------------------------------------ +-- | Mapping from tactic commands to their contextual providers. See 'provide', +-- 'filterGoalType' and 'filterBindingType' for the nitty gritty. +commandProvider :: TacticCommand -> TacticProvider +commandProvider Auto = provide Auto "" +commandProvider Intros = + filterGoalType isFunction $ + provide Intros "" +commandProvider Destruct = + filterBindingType destructFilter $ \occ _ -> + provide Destruct $ T.pack $ occNameString occ +commandProvider Homomorphism = + filterBindingType homoFilter $ \occ _ -> + provide Homomorphism $ T.pack $ occNameString occ +commandProvider DestructLambdaCase = + requireExtension LambdaCase $ + filterGoalType (isJust . lambdaCaseable) $ + provide DestructLambdaCase "" +commandProvider HomomorphismLambdaCase = + requireExtension LambdaCase $ + filterGoalType ((== Just True) . lambdaCaseable) $ + provide HomomorphismLambdaCase "" + + +------------------------------------------------------------------------------ +-- | A mapping from tactic commands to actual tactics for refinery. +commandTactic :: TacticCommand -> OccName -> TacticsM () +commandTactic Auto = const auto +commandTactic Intros = const intros +commandTactic Destruct = destruct +commandTactic Homomorphism = homo +commandTactic DestructLambdaCase = const destructLambdaCase +commandTactic HomomorphismLambdaCase = const homoLambdaCase + + +------------------------------------------------------------------------------ +-- | 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 + + +------------------------------------------------------------------------------ +-- | We should show destruct for bindings only when those bindings have usual +-- algebraic types. +destructFilter :: Type -> Type -> Bool +destructFilter _ (algebraicTyCon -> Just _) = True +destructFilter _ _ = False + + +runIde :: IdeState -> Action a -> IO a +runIde state = runAction "tactic" state + + +codeActionProvider :: CodeActionProvider IdeState +codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + fromMaybeT (Right $ List []) $ do + (_, jdg, _, dflags) <- judgementForHole state nfp range + actions <- lift $ + -- This foldMap is over the function monoid. + foldMap commandProvider [minBound .. maxBound] + dflags + plId + uri + range + jdg + pure $ Right $ List actions +codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] + + +codeActions :: [CodeAction] -> List CAResult +codeActions = List . fmap CACodeAction + + +------------------------------------------------------------------------------ +-- | Terminal constructor for providing context-sensitive tactics. Tactics +-- given by 'provide' are always available. +provide :: TacticCommand -> T.Text -> TacticProvider +provide tc name _ plId uri range _ = do + let title = tacticTitle tc name + params = TacticParams { file = uri , range = range , var_name = name } + cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing + $ Just cmd + + +------------------------------------------------------------------------------ +-- | Restrict a 'TacticProvider', making sure it appears only when the given +-- predicate holds for the goal. +requireExtension :: Extension -> TacticProvider -> TacticProvider +requireExtension ext tp dflags plId uri range jdg = + case xopt ext dflags of + True -> tp dflags plId uri range jdg + False -> pure [] + + +------------------------------------------------------------------------------ +-- | Restrict a 'TacticProvider', making sure it appears only when the given +-- predicate holds for the goal. +filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider +filterGoalType p tp dflags plId uri range jdg = + case p $ unCType $ jGoal jdg of + True -> tp dflags plId uri range jdg + False -> pure [] + + +------------------------------------------------------------------------------ +-- | Multiply a 'TacticProvider' for each binding, making sure it appears only +-- when the given predicate holds over the goal and binding types. +filterBindingType + :: (Type -> Type -> Bool) -- ^ Goal and then binding types. + -> (OccName -> Type -> TacticProvider) + -> TacticProvider +filterBindingType p tp dflags plId uri range jdg = + let hy = jHypothesis jdg + g = jGoal jdg + in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) -> + case p (unCType g) ty of + True -> tp occ ty dflags plId uri range jdg + False -> pure [] + + +data TacticParams = TacticParams + { file :: Uri -- ^ Uri of the file to fill the hole in + , range :: Range -- ^ The range of the hole + , var_name :: T.Text + } + deriving (Show, Eq, Generic, ToJSON, FromJSON) + + +------------------------------------------------------------------------------ +-- | Find the last typechecked module, and find the most specific span, as well +-- as the judgement at the given range. +judgementForHole + :: IdeState + -> NormalizedFilePath + -> Range + -> MaybeT IO (Range, Judgement, Context, DynFlags) +judgementForHole state nfp range = do + (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp + range' <- liftMaybe $ fromCurrentRange amapping range + + (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp + + -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' + -- which don't change very often. + ((modsum,_), _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp + let dflags = ms_hspp_opts modsum + + (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> + case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of + Nothing -> Nothing + Just ast' -> do + let info = nodeInfo ast' + ty <- listToMaybe $ nodeType info + guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info + pure (nodeSpan ast', ty) + + resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss + (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp + let tcg = tmrTypechecked tcmod + tcs = tcg_binds tcg + ctx = mkContext + (mapMaybe (sequenceA . (occName *** coerce)) + $ getDefiningBindings binds rss) + tcg + top_provs = getRhsPosVals rss tcs + local_hy = spliceProvenance top_provs + $ hypothesisFromBindings rss binds + cls_hy = contextMethodHypothesis ctx + pure ( resulting_range + , mkFirstJudgement + (local_hy <> cls_hy) + (isRhsHole rss tcs) + goal + , ctx + , dflags + ) + + +spliceProvenance + :: Map OccName Provenance + -> Map OccName (HyInfo a) + -> Map OccName (HyInfo a) +spliceProvenance provs = + M.mapWithKey $ \name hi -> + overProvenance (maybe id const $ M.lookup name provs) hi + + +tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams +tacticCmd tac lf state (TacticParams uri range var_name) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + fromMaybeT (Right Null, Nothing) $ do + (range', jdg, ctx, dflags) <- judgementForHole state nfp range + let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range' + pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp + x <- lift $ timeout 2e8 $ + case runTactic ctx jdg + $ tac + $ mkVarOcc + $ T.unpack var_name of + Left err -> + pure $ (, Nothing) + $ Left + $ ResponseError InvalidRequest (T.pack $ show err) Nothing + Right rtr -> do + traceMX "solns" $ rtr_other_solns rtr + let g = graft (RealSrcSpan span) $ rtr_extract rtr + response = transform dflags (clientCapabilities lf) uri g pm + pure $ case response of + Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) + Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) + pure $ case x of + Just y -> y + Nothing -> (, Nothing) + $ Left + $ ResponseError InvalidRequest "timed out" Nothing +tacticCmd _ _ _ _ = + pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing + , Nothing + ) + + +fromMaybeT :: Functor m => a -> MaybeT m a -> m a +fromMaybeT def = fmap (fromMaybe def) . runMaybeT + +liftMaybe :: Monad m => Maybe a -> MaybeT m a +liftMaybe a = MaybeT $ pure a + + +------------------------------------------------------------------------------ +-- | Is this hole immediately to the right of an equals sign? +isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool +isRhsHole rss tcs = everything (||) (mkQ False $ \case + TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span + _ -> False + ) tcs + + +------------------------------------------------------------------------------ +-- | Compute top-level position vals of a function +getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance +getRhsPosVals rss tcs + = M.fromList + $ join + $ maybeToList + $ getFirst + $ everything (<>) (mkQ mempty $ \case + TopLevelRHS name ps + (L (RealSrcSpan span) -- body with no guards and a single defn + (HsVar _ (L _ hole))) + | containsSpan rss span -- which contains our span + , isHole $ occName hole -- and the span is a hole + -> First $ do + patnames <- traverse getPatName ps + pure $ zip patnames $ [0..] <&> TopLevelArgPrv name + _ -> mempty + ) tcs + + + +-- TODO(sandy): Make this more robust +isHole :: OccName -> Bool +isHole = isPrefixOf "_" . occNameString + diff --git a/src/Ide/Plugin/Tactic/Auto.hs b/src/Ide/Plugin/Tactic/Auto.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Auto.hs @@ -0,0 +1,28 @@ +module Ide.Plugin.Tactic.Auto where + +import Control.Monad.State (gets) +import Ide.Plugin.Tactic.Context +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.KnownStrategies +import Ide.Plugin.Tactic.Machinery (tracing) +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types +import Refinery.Tactic + + +------------------------------------------------------------------------------ +-- | Automatically solve a goal. +auto :: TacticsM () +auto = do + jdg <- goal + skolems <- gets ts_skolems + current <- getCurrentDefinitions + traceMX "goal" jdg + traceMX "ctx" current + traceMX "skolems" skolems + commit knownStrategies + . tracing "auto" + . localTactic (auto' 4) + . disallowing RecursiveCall + $ fmap fst current + diff --git a/src/Ide/Plugin/Tactic/CodeGen.hs b/src/Ide/Plugin/Tactic/CodeGen.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/CodeGen.hs @@ -0,0 +1,262 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.CodeGen where + +import Control.Lens ((+~), (%~), (<>~)) +import Control.Monad.Except +import Control.Monad.State (MonadState) +import Control.Monad.State.Class (modify) +import Data.Generics.Product (field) +import Data.List +import qualified Data.Map as M +import qualified Data.Set as S +import Data.Traversable +import DataCon +import Development.IDE.GHC.Compat +import GHC.Exts +import GHC.SourceGen (RdrNameStr) +import GHC.SourceGen.Binds +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.GHC +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Naming +import Ide.Plugin.Tactic.Types +import Name +import Type hiding (Var) + + +useOccName :: MonadState TacticState m => Judgement -> OccName -> m () +useOccName jdg name = + -- Only score points if this is in the local hypothesis + case M.lookup name $ jLocalHypothesis jdg of + Just{} -> modify + $ (withUsedVals $ S.insert name) + . (field @"ts_unused_top_vals" %~ S.delete name) + Nothing -> pure () + + +------------------------------------------------------------------------------ +-- | Doing recursion incurs a small penalty in the score. +countRecursiveCall :: TacticState -> TacticState +countRecursiveCall = field @"ts_recursion_count" +~ 1 + + +------------------------------------------------------------------------------ +-- | Insert some values into the unused top values field. These are +-- subsequently removed via 'useOccName'. +addUnusedTopVals :: MonadState TacticState m => S.Set OccName -> m () +addUnusedTopVals vals = modify $ field @"ts_unused_top_vals" <>~ vals + + +destructMatches + :: (DataCon -> Judgement -> Rule) + -- ^ How to construct each match + -> Maybe OccName + -- ^ Scrutinee + -> CType + -- ^ Type being destructed + -> Judgement + -> RuleM (Trace, [RawMatch]) +destructMatches f scrut t jdg = do + let hy = jEntireHypothesis jdg + g = jGoal jdg + case splitTyConApp_maybe $ unCType t of + Nothing -> throwError $ GoalMismatch "destruct" g + Just (tc, apps) -> do + let dcs = tyConDataCons tc + case dcs of + [] -> throwError $ GoalMismatch "destruct" g + _ -> fmap unzipTrace $ for dcs $ \dc -> do + let args = dataConInstOrigArgTys' dc apps + names <- mkManyGoodNames hy args + let hy' = zip names $ coerce args + j = introducingPat scrut dc hy' + $ withNewGoal g jdg + (tr, sg) <- f dc j + modify $ withIntroducedVals $ mappend $ S.fromList names + pure ( rose ("match " <> show dc <> " {" <> + intercalate ", " (fmap show names) <> "}") + $ pure tr + , match [mkDestructPat dc names] $ unLoc sg + ) + + +------------------------------------------------------------------------------ +-- | Produces a pattern for a data con and the names of its fields. +mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs +mkDestructPat dcon names + | isTupleDataCon dcon = + tuple pat_args + | otherwise = + infixifyPatIfNecessary dcon $ + conP + (coerceName $ dataConName dcon) + pat_args + where + pat_args = fmap bvar' names + + +infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs +infixifyPatIfNecessary dcon x + | dataConIsInfix dcon = + case x of + ConPatIn op (PrefixCon [lhs, rhs]) -> + ConPatIn op $ InfixCon lhs rhs + y -> y + | otherwise = x + + + +unzipTrace :: [(Trace, a)] -> (Trace, [a]) +unzipTrace l = + let (trs, as) = unzip l + in (rose mempty trs, as) + + +-- | Essentially same as 'dataConInstOrigArgTys' in GHC, +-- but only accepts universally quantified types as the second arguments +-- and automatically introduces existentials. +-- +-- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'. +-- We need some tweaks if the compiler changes the implementation. +dataConInstOrigArgTys' + :: DataCon + -- ^ 'DataCon'structor + -> [Type] + -- ^ /Universally/ quantified type arguments to a result type. + -- It /MUST NOT/ contain any dictionaries, coercion and existentials. + -- + -- For example, for @MkMyGADT :: b -> MyGADT a c@, we + -- must pass @[a, c]@ as this argument but not @b@, as @b@ is an existential. + -> [Type] + -- ^ Types of arguments to the DataCon with returned type is instantiated with the second argument. +dataConInstOrigArgTys' con uniTys = + let exvars = dataConExTys con + in dataConInstOrigArgTys con $ + uniTys ++ fmap mkTyVarTy exvars + -- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys' + -- unifies the second argument with DataCon's universals followed by existentials. + -- If the definition of 'dataConInstOrigArgTys' changes, + -- this place must be changed accordingly. + +------------------------------------------------------------------------------ +-- | Combinator for performing case splitting, and running sub-rules on the +-- resulting matches. + +destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule +destruct' f term jdg = do + when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic + let hy = jHypothesis jdg + case M.lookup term hy of + Nothing -> throwError $ UndefinedHypothesis term + Just (hi_type -> t) -> do + useOccName jdg term + (tr, ms) + <- destructMatches + f + (Just term) + t + $ disallowing AlreadyDestructed [term] jdg + pure ( rose ("destruct " <> show term) $ pure tr + , noLoc $ case' (var' term) ms + ) + + +------------------------------------------------------------------------------ +-- | Combinator for performign case splitting, and running sub-rules on the +-- resulting matches. +destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule +destructLambdaCase' f jdg = do + when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic + let g = jGoal jdg + case splitFunTy_maybe (unCType g) of + Just (arg, _) | isAlgType arg -> + fmap (fmap noLoc $ lambdaCase) <$> + destructMatches f Nothing (CType arg) jdg + _ -> throwError $ GoalMismatch "destructLambdaCase'" g + + +------------------------------------------------------------------------------ +-- | Construct a data con with subgoals for each field. +buildDataCon + :: Judgement + -> DataCon -- ^ The data con to build + -> [Type] -- ^ Type arguments for the data con + -> RuleM (Trace, LHsExpr GhcPs) +buildDataCon jdg dc apps = do + let args = dataConInstOrigArgTys' dc apps + (tr, sgs) + <- fmap unzipTrace + $ traverse ( \(arg, n) -> + newSubgoal + . filterSameTypeFromOtherPositions dc n + . blacklistingDestruct + . flip withNewGoal jdg + $ CType arg + ) $ zip args [0..] + pure + . (rose (show dc) $ pure tr,) + $ mkCon dc sgs + + +mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs +mkCon dcon (fmap unLoc -> args) + | isTupleDataCon dcon = + noLoc $ tuple args + | dataConIsInfix dcon + , (lhs : rhs : args') <- args = + noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args' + | otherwise = + noLoc $ foldl' (@@) (bvar' $ occName $ dcon_name) args + where + dcon_name = dataConName dcon + + + +coerceName :: HasOccName a => a -> RdrNameStr +coerceName = fromString . occNameString . occName + + + +------------------------------------------------------------------------------ +-- | Like 'var', but works over standard GHC 'OccName's. +var' :: Var a => OccName -> a +var' = var . fromString . occNameString + + +------------------------------------------------------------------------------ +-- | Like 'bvar', but works over standard GHC 'OccName's. +bvar' :: BVar a => OccName -> a +bvar' = bvar . fromString . occNameString + + +------------------------------------------------------------------------------ +-- | Get an HsExpr corresponding to a function name. +mkFunc :: String -> HsExpr GhcPs +mkFunc = var' . mkVarOcc + + +------------------------------------------------------------------------------ +-- | Get an HsExpr corresponding to a value name. +mkVal :: String -> HsExpr GhcPs +mkVal = var' . mkVarOcc + + +------------------------------------------------------------------------------ +-- | Like 'op', but easier to call. +infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +infixCall s = flip op (fromString s) + + +------------------------------------------------------------------------------ +-- | Like '(@@)', but uses a dollar instead of parentheses. +appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs +appDollar = infixCall "$" + diff --git a/src/Ide/Plugin/Tactic/Context.hs b/src/Ide/Plugin/Tactic/Context.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Context.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} + +module Ide.Plugin.Tactic.Context where + +import Bag +import Control.Arrow +import Control.Monad.Reader +import Data.List +import Data.Map (Map) +import qualified Data.Map as M +import Data.Maybe (mapMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.GHC (tacticsThetaTy) +import Ide.Plugin.Tactic.Machinery (methodHypothesis) +import Ide.Plugin.Tactic.Types +import OccName +import TcRnTypes +import TcType (substTy, tcSplitSigmaTy) +import Unify (tcUnifyTy) + + +mkContext :: [(OccName, CType)] -> TcGblEnv -> Context +mkContext locals tcg = Context + { ctxDefiningFuncs = locals + , ctxModuleFuncs = fmap splitId + . (getFunBindId =<<) + . fmap unLoc + . bagToList + $ tcg_binds tcg + } + + +------------------------------------------------------------------------------ +-- | Find all of the class methods that exist from the givens in the context. +contextMethodHypothesis :: Context -> Map OccName (HyInfo CType) +contextMethodHypothesis ctx + = M.fromList + . excludeForbiddenMethods + . join + . concatMap + ( mapMaybe methodHypothesis + . tacticsThetaTy + . unCType + ) + . mapMaybe (definedThetaType ctx) + . fmap fst + $ ctxDefiningFuncs ctx + + +------------------------------------------------------------------------------ +-- | Many operations are defined in typeclasses for performance reasons, rather +-- than being a true part of the class. This function filters out those, in +-- order to keep our hypothesis space small. +excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)] +excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . fst) + where + forbiddenMethods :: Set OccName + forbiddenMethods = S.map mkVarOcc $ S.fromList + [ -- monadfail + "fail" + ] + + +------------------------------------------------------------------------------ +-- | Given the name of a function that exists in 'ctxDefiningFuncs', get its +-- theta type. +definedThetaType :: Context -> OccName -> Maybe CType +definedThetaType ctx name = do + (_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx + (_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx + let (_, _, poly') = tcSplitSigmaTy poly + subst <- tcUnifyTy poly' mono + pure $ CType $ substTy subst $ snd $ splitForAllTys poly + + +splitId :: Id -> (OccName, CType) +splitId = occName &&& CType . idType + + +getFunBindId :: HsBindLR GhcTc GhcTc -> [Id] +getFunBindId (AbsBinds _ _ _ abes _ _ _) + = abes >>= \case + ABE _ poly _ _ _ -> pure poly + _ -> [] +getFunBindId _ = [] + + +getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] +getCurrentDefinitions = asks $ ctxDefiningFuncs + +getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] +getModuleHypothesis = asks ctxModuleFuncs + diff --git a/src/Ide/Plugin/Tactic/Debug.hs b/src/Ide/Plugin/Tactic/Debug.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Debug.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE TypeApplications #-} + +module Ide.Plugin.Tactic.Debug + ( unsafeRender + , unsafeRender' + , traceM + , traceShowId + , trace + , traceX + , traceIdX + , traceMX + ) where + +import Control.DeepSeq +import Control.Exception +import Debug.Trace +import DynFlags (unsafeGlobalDynFlags) +import Outputable hiding ((<>)) +import System.IO.Unsafe (unsafePerformIO) + +#if __GLASGOW_HASKELL__ >= 808 +import PlainPanic (PlainGhcException) +type GHC_EXCEPTION = PlainGhcException +#else +import Panic (GhcException) +type GHC_EXCEPTION = GhcException +#endif + + +------------------------------------------------------------------------------ +-- | Print something +unsafeRender :: Outputable a => a -> String +unsafeRender = unsafeRender' . ppr + + +unsafeRender' :: SDoc -> String +unsafeRender' sdoc = unsafePerformIO $ do + let z = showSDoc unsafeGlobalDynFlags sdoc + -- We might not have unsafeGlobalDynFlags (like during testing), in which + -- case GHC panics. Instead of crashing, let's just fail to print. + !res <- try @GHC_EXCEPTION $ evaluate $ deepseq z z + pure $ either (const "") id res +{-# NOINLINE unsafeRender' #-} + +traceMX :: (Monad m, Show a) => String -> a -> m () +traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a + +traceX :: (Show a) => String -> a -> b -> b +traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) + +traceIdX :: (Show a) => String -> a -> a +traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a + diff --git a/src/Ide/Plugin/Tactic/GHC.hs b/src/Ide/Plugin/Tactic/GHC.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/GHC.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.GHC where + +import Control.Monad.State +import qualified Data.Map as M +import Data.Maybe (isJust) +import Data.Traversable +import qualified DataCon as DataCon +import Development.IDE.GHC.Compat +import Generics.SYB (mkT, everywhere) +import Ide.Plugin.Tactic.Types +import OccName +import TcType +import TyCoRep +import Type +import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon) +import Unique +import Var + +tcTyVar_maybe :: Type -> Maybe Var +tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' +tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty -- look through casts, as + -- this is only used for + -- e.g., FlexibleContexts +tcTyVar_maybe (TyVarTy v) = Just v +tcTyVar_maybe _ = Nothing + + +instantiateType :: Type -> ([TyVar], Type) +instantiateType t = do + let vs = tyCoVarsOfTypeList t + vs' = fmap cloneTyVar vs + subst = foldr (\(v,t) a -> extendTCvSubst a v $ TyVarTy t) emptyTCvSubst + $ zip vs vs' + in (vs', substTy subst t) + + +cloneTyVar :: TyVar -> TyVar +cloneTyVar t = + let uniq = getUnique t + some_magic_number = 49 + in setVarUnique t $ deriveUnique uniq some_magic_number + + +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tacticsSplitFunTy -> (_, _, [], _)) = False +isFunction _ = True + + +------------------------------------------------------------------------------ +-- | Split a function, also splitting out its quantified variables and theta +-- context. +tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type) +tacticsSplitFunTy t + = let (vars, theta, t') = tcSplitSigmaTy t + (args, res) = tcSplitFunTys t' + in (vars, theta, args, res) + + +------------------------------------------------------------------------------ +-- | Rip the theta context out of a regular type. +tacticsThetaTy :: Type -> ThetaType +tacticsThetaTy (tcSplitSigmaTy -> (_, theta, _)) = theta + + +------------------------------------------------------------------------------ +-- | Instantiate all of the quantified type variables in a type with fresh +-- skolems. +freshTyvars :: MonadState TacticState m => Type -> m Type +freshTyvars t = do + let (tvs, _, _, _) = tacticsSplitFunTy t + reps <- fmap M.fromList + $ for tvs $ \tv -> do + uniq <- freshUnique + pure $ (tv, setTyVarUnique tv uniq) + pure $ + everywhere + (mkT $ \tv -> + case M.lookup tv reps of + Just tv' -> tv' + Nothing -> tv + ) t + + +------------------------------------------------------------------------------ +-- | Is this an algebraic type? +algebraicTyCon :: Type -> Maybe TyCon +algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) + | tycon == intTyCon = Nothing + | tycon == floatTyCon = Nothing + | tycon == doubleTyCon = Nothing + | tycon == charTyCon = Nothing + | tycon == funTyCon = Nothing + | otherwise = Just tycon +algebraicTyCon _ = Nothing + +------------------------------------------------------------------------------ +-- | Can ths type be lambda-cased? +-- +-- Return: 'Nothing' if no +-- @Just False@ if it can't be homomorphic +-- @Just True@ if it can +lambdaCaseable :: Type -> Maybe Bool +lambdaCaseable (splitFunTy_maybe -> Just (arg, res)) + | isJust (algebraicTyCon arg) + = Just $ isJust $ algebraicTyCon res +lambdaCaseable _ = Nothing + +fromPatCompat :: PatCompat GhcTc -> Pat GhcTc +#if __GLASGOW_HASKELL__ == 808 +type PatCompat pass = Pat pass +fromPatCompat = id +#else +type PatCompat pass = LPat pass +fromPatCompat = unLoc +#endif + +------------------------------------------------------------------------------ +-- | Should make sure it's a fun bind +pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc) +pattern TopLevelRHS name ps body <- + Match _ + (FunRhs (L _ (occName -> name)) _ _) + ps + (GRHSs _ + [L _ (GRHS _ [] body)] _) + +getPatName :: PatCompat GhcTc -> Maybe OccName +getPatName (fromPatCompat -> p0) = + case p0 of + VarPat _ x -> Just $ occName $ unLoc x + LazyPat _ p -> getPatName p + AsPat _ x _ -> Just $ occName $ unLoc x + ParPat _ p -> getPatName p + BangPat _ p -> getPatName p + ViewPat _ _ p -> getPatName p +#if __GLASGOW_HASKELL__ >= 808 + SigPat _ p _ -> getPatName p +#endif +#if __GLASGOW_HASKELL__ == 808 + XPat p -> getPatName $ unLoc p +#endif + _ -> Nothing + +dataConExTys :: DataCon -> [TyCoVar] +#if __GLASGOW_HASKELL__ >= 808 +dataConExTys = DataCon.dataConExTyCoVars +#else +dataConExTys = DataCon.dataConExTyVars +#endif diff --git a/src/Ide/Plugin/Tactic/Judgements.hs b/src/Ide/Plugin/Tactic/Judgements.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Judgements.hs @@ -0,0 +1,380 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Judgements + ( blacklistingDestruct + , unwhitelistingSplit + , introducingLambda + , introducingRecursively + , introducingPat + , jGoal + , jHypothesis + , jEntireHypothesis + , jPatHypothesis + , substJdg + , unsetIsTopHole + , filterSameTypeFromOtherPositions + , isDestructBlacklisted + , withNewGoal + , jLocalHypothesis + , isSplitWhitelisted + , isPatternMatch + , filterPosition + , isTopHole + , disallowing + , mkFirstJudgement + , hypothesisFromBindings + , isTopLevel + ) where + +import Control.Lens hiding (Context) +import Data.Bool +import Data.Char +import Data.Coerce +import Data.Generics.Product (field) +import Data.Map (Map) +import qualified Data.Map as M +import Data.Maybe +import Data.Set (Set) +import qualified Data.Set as S +import DataCon (DataCon) +import Development.IDE.Spans.LocalBindings +import Ide.Plugin.Tactic.Types +import OccName +import SrcLoc +import Type + + +------------------------------------------------------------------------------ +-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. +hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType) +hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span + + +------------------------------------------------------------------------------ +-- | Convert a @Set Id@ into a hypothesis. +buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType) +buildHypothesis + = M.fromList + . mapMaybe go + where + go (occName -> occ, t) + | Just ty <- t + , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty) + | otherwise = Nothing + + +blacklistingDestruct :: Judgement -> Judgement +blacklistingDestruct = + field @"_jBlacklistDestruct" .~ True + + +unwhitelistingSplit :: Judgement -> Judgement +unwhitelistingSplit = + field @"_jWhitelistSplit" .~ False + + +isDestructBlacklisted :: Judgement -> Bool +isDestructBlacklisted = _jBlacklistDestruct + + +isSplitWhitelisted :: Judgement -> Bool +isSplitWhitelisted = _jWhitelistSplit + + +withNewGoal :: a -> Judgement' a -> Judgement' a +withNewGoal t = field @"_jGoal" .~ t + + +------------------------------------------------------------------------------ +-- | Helper function for implementing functions which introduce new hypotheses. +introducing + :: (Int -> Provenance) -- ^ A function from the position of the arg to its + -- provenance. + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a +introducing f ns = + field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&> + \(pos, (name, ty)) -> (name, HyInfo (f pos) ty)) + + +------------------------------------------------------------------------------ +-- | Introduce bindings in the context of a lamba. +introducingLambda + :: Maybe OccName -- ^ The name of the top level function. For any other + -- function, this should be 'Nothing'. + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a +introducingLambda func = introducing $ \pos -> + maybe UserPrv (\x -> TopLevelArgPrv x pos) func + + +------------------------------------------------------------------------------ +-- | Introduce a binding in a recursive context. +introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a +introducingRecursively = introducing $ const RecursivePrv + + +------------------------------------------------------------------------------ +-- | Check whether any of the given occnames are an ancestor of the term. +hasPositionalAncestry + :: Foldable t + => t OccName -- ^ Desired ancestors. + -> Judgement + -> OccName -- ^ Potential child + -> Maybe Bool -- ^ Just True if the result is the oldest positional ancestor + -- just false if it's a descendent + -- otherwise nothing +hasPositionalAncestry ancestors jdg name + | not $ null ancestors + = case any (== name) ancestors of + True -> Just True + False -> + case M.lookup name $ jAncestryMap jdg of + Just ancestry -> + bool Nothing (Just False) $ any (flip S.member ancestry) ancestors + Nothing -> Nothing + | otherwise = Nothing + + +------------------------------------------------------------------------------ +-- | Helper function for disallowing hypotheses that have the wrong ancestry. +filterAncestry + :: Foldable t + => t OccName + -> DisallowReason + -> Judgement + -> Judgement +filterAncestry ancestry reason jdg = + disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg + where + go name _ + = not + . isJust + $ hasPositionalAncestry ancestry jdg name + + +------------------------------------------------------------------------------ +-- | @filter defn pos@ removes any hypotheses which are bound in @defn@ to +-- a position other than @pos@. Any terms whose ancestry doesn't include @defn@ +-- remain. +filterPosition :: OccName -> Int -> Judgement -> Judgement +filterPosition defn pos jdg = + filterAncestry (findPositionVal jdg defn pos) (WrongBranch pos) jdg + + +------------------------------------------------------------------------------ +-- | Helper function for determining the ancestry list for 'filterPosition'. +findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName +findPositionVal jdg defn pos = listToMaybe $ do + -- It's important to inspect the entire hypothesis here, as we need to trace + -- ancstry through potentially disallowed terms in the hypothesis. + (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg + case hi_provenance hi of + TopLevelArgPrv defn' pos' + | defn == defn' + , pos == pos' -> pure name + PatternMatchPrv pv + | pv_scrutinee pv == Just defn + , pv_position pv == pos -> pure name + _ -> [] + + +------------------------------------------------------------------------------ +-- | Helper function for determining the ancestry list for +-- 'filterSameTypeFromOtherPositions'. +findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName] +findDconPositionVals jdg dcon pos = do + (name, hi) <- M.toList $ jHypothesis jdg + case hi_provenance hi of + PatternMatchPrv pv + | pv_datacon pv == Uniquely dcon + , pv_position pv == pos -> pure name + _ -> [] + + +------------------------------------------------------------------------------ +-- | Disallow any hypotheses who have the same type as anything bound by the +-- given position for the datacon. Used to ensure recursive functions like +-- 'fmap' preserve the relative ordering of their arguments by eliminating any +-- other term which might match. +filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement +filterSameTypeFromOtherPositions dcon pos jdg = + let hy = jHypothesis + $ filterAncestry + (findDconPositionVals jdg dcon pos) + (WrongBranch pos) + jdg + tys = S.fromList $ hi_type <$> M.elems hy + to_remove = + M.filter (flip S.member tys . hi_type) (jHypothesis jdg) + M.\\ hy + in disallowing Shadowed (M.keys to_remove) jdg + + +------------------------------------------------------------------------------ +-- | Return the ancestry of a 'PatVal', or 'mempty' otherwise. +getAncestry :: Judgement' a -> OccName -> Set OccName +getAncestry jdg name = + case M.lookup name $ jPatHypothesis jdg of + Just pv -> pv_ancestry pv + Nothing -> mempty + + +jAncestryMap :: Judgement' a -> Map OccName (Set OccName) +jAncestryMap jdg = + flip M.map (jPatHypothesis jdg) pv_ancestry + + +------------------------------------------------------------------------------ +-- TODO(sandy): THIS THING IS A BIG BIG HACK +-- +-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined +-- (eg, we might be in a where block). The head of this list is not guaranteed +-- to be the one we're interested in. +extremelyStupid__definingFunction :: Context -> OccName +extremelyStupid__definingFunction = + fst . head . ctxDefiningFuncs + + +------------------------------------------------------------------------------ +-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of +-- data sitting around in jPatternVals. +introducingPat + :: Maybe OccName + -> DataCon + -> [(OccName, a)] + -> Judgement' a + -> Judgement' a +introducingPat scrutinee dc ns jdg + = introducing (\pos -> + PatternMatchPrv $ + PatVal + scrutinee + (maybe mempty + (\scrut -> S.singleton scrut <> getAncestry jdg scrut) + scrutinee) + (Uniquely dc) + pos + ) ns jdg + + +------------------------------------------------------------------------------ +-- | Prevent some occnames from being used in the hypothesis. This will hide +-- them from 'jHypothesis', but not from 'jEntireHypothesis'. +disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a +disallowing reason (S.fromList -> ns) = + field @"_jHypothesis" %~ (M.mapWithKey $ \name hi -> + case S.member name ns of + True -> overProvenance (DisallowedPrv reason) hi + False -> hi + ) + + +------------------------------------------------------------------------------ +-- | The hypothesis, consisting of local terms and the ambient environment +-- (impors and class methods.) Hides disallowed values. +jHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis + + +------------------------------------------------------------------------------ +-- | The whole hypothesis, including things disallowed. +jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jEntireHypothesis = _jHypothesis + + +------------------------------------------------------------------------------ +-- | Just the local hypothesis. +jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a) +jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis + + +------------------------------------------------------------------------------ +-- | If we're in a top hole, the name of the defining function. +isTopHole :: Context -> Judgement' a -> Maybe OccName +isTopHole ctx = + bool Nothing (Just $ extremelyStupid__definingFunction ctx) . _jIsTopHole + + +unsetIsTopHole :: Judgement' a -> Judgement' a +unsetIsTopHole = field @"_jIsTopHole" .~ False + + +------------------------------------------------------------------------------ +-- | Only the hypothesis members which are pattern vals +jPatHypothesis :: Judgement' a -> Map OccName PatVal +jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis + + +getPatVal :: Provenance-> Maybe PatVal +getPatVal prov = + case prov of + PatternMatchPrv pv -> Just pv + _ -> Nothing + + +jGoal :: Judgement' a -> a +jGoal = _jGoal + + +substJdg :: TCvSubst -> Judgement -> Judgement +substJdg subst = fmap $ coerce . substTy subst . coerce + + +mkFirstJudgement + :: M.Map OccName (HyInfo CType) + -> Bool -- ^ are we in the top level rhs hole? + -> Type + -> Judgement' CType +mkFirstJudgement hy top goal = Judgement + { _jHypothesis = hy + , _jBlacklistDestruct = False + , _jWhitelistSplit = True + , _jIsTopHole = top + , _jGoal = CType goal + } + + +------------------------------------------------------------------------------ +-- | Is this a top level function binding? +isTopLevel :: Provenance -> Bool +isTopLevel TopLevelArgPrv{} = True +isTopLevel _ = False + + +------------------------------------------------------------------------------ +-- | Is this a local function argument, pattern match or user val? +isLocalHypothesis :: Provenance -> Bool +isLocalHypothesis UserPrv{} = True +isLocalHypothesis PatternMatchPrv{} = True +isLocalHypothesis TopLevelArgPrv{} = True +isLocalHypothesis _ = False + + +------------------------------------------------------------------------------ +-- | Is this a pattern match? +isPatternMatch :: Provenance -> Bool +isPatternMatch PatternMatchPrv{} = True +isPatternMatch _ = False + + +------------------------------------------------------------------------------ +-- | Was this term ever disallowed? +isDisallowed :: Provenance -> Bool +isDisallowed DisallowedPrv{} = True +isDisallowed _ = False + + +------------------------------------------------------------------------------ +-- | Eliminates 'DisallowedPrv' provenances. +expandDisallowed :: Provenance -> Provenance +expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv +expandDisallowed prv = prv + diff --git a/src/Ide/Plugin/Tactic/KnownStrategies.hs b/src/Ide/Plugin/Tactic/KnownStrategies.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE LambdaCase #-} + +module Ide.Plugin.Tactic.KnownStrategies where + +import Control.Monad.Error.Class +import Ide.Plugin.Tactic.Context (getCurrentDefinitions) +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types +import OccName (mkVarOcc) +import Refinery.Tactic +import Ide.Plugin.Tactic.Machinery (tracing) +import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary) + + +knownStrategies :: TacticsM () +knownStrategies = choice + [ known "fmap" deriveFmap + , known "arbitrary" deriveArbitrary + ] + + +known :: String -> TacticsM () -> TacticsM () +known name t = do + getCurrentDefinitions >>= \case + [(def, _)] | def == mkVarOcc name -> + tracing ("known " <> name) t + _ -> throwError NoApplicableTactic + + +deriveFmap :: TacticsM () +deriveFmap = do + try intros + overAlgebraicTerms homo + choice + [ overFunctions apply >> auto' 2 + , assumption + , recursion + ] + diff --git a/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} + +module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where + +import Control.Monad.Except (MonadError(throwError)) +import Data.Bool (bool) +import Data.List (partition) +import DataCon ( DataCon, dataConName ) +import Development.IDE.GHC.Compat (HsExpr, GhcPs, noLoc) +import GHC.Exts ( IsString(fromString) ) +import GHC.List ( foldl' ) +import GHC.SourceGen (int) +import GHC.SourceGen.Binds ( match, valBind ) +import GHC.SourceGen.Expr ( case', lambda, let' ) +import GHC.SourceGen.Overloaded ( App((@@)), HasList(list) ) +import GHC.SourceGen.Pat ( conP ) +import Ide.Plugin.Tactic.CodeGen +import Ide.Plugin.Tactic.Judgements (jGoal) +import Ide.Plugin.Tactic.Machinery (tracePrim) +import Ide.Plugin.Tactic.Types +import OccName (occNameString, mkVarOcc, HasOccName(occName) ) +import Refinery.Tactic (goal, rule ) +import TyCon (tyConName, TyCon, tyConDataCons ) +import Type ( splitTyConApp_maybe ) +import Data.Generics (mkQ, everything) + + +------------------------------------------------------------------------------ +-- | Known tactic for deriving @arbitrary :: Gen a@. This tactic splits the +-- type's data cons into terminal and inductive cases, and generates code that +-- produces a terminal if the QuickCheck size parameter is <=1, or any data con +-- otherwise. It correctly scales recursive parameters, ensuring termination. +deriveArbitrary :: TacticsM () +deriveArbitrary = do + ty <- jGoal <$> goal + case splitTyConApp_maybe $ unCType ty of + Just (gen_tc, [splitTyConApp_maybe -> Just (tc, apps)]) + | occNameString (occName $ tyConName gen_tc) == "Gen" -> do + rule $ \_ -> do + let dcs = tyConDataCons tc + (terminal, big) = partition ((== 0) . genRecursiveCount) + $ fmap (mkGenerator tc apps) dcs + terminal_expr = mkVal "terminal" + oneof_expr = mkVal "oneof" + pure + ( tracePrim "deriveArbitrary" + , noLoc $ + let' [valBind (fromString "terminal") $ list $ fmap genExpr terminal] $ + appDollar (mkFunc "sized") $ lambda [bvar' (mkVarOcc "n")] $ + case' (infixCall "<=" (mkVal "n") (int 1)) + [ match [conP (fromString "True") []] $ + oneof_expr @@ terminal_expr + , match [conP (fromString "False") []] $ + appDollar oneof_expr $ + infixCall "<>" + (list $ fmap genExpr big) + terminal_expr + ] + ) + _ -> throwError $ GoalMismatch "deriveArbitrary" ty + + +------------------------------------------------------------------------------ +-- | Helper data type for the generator of a specific data con. +data Generator = Generator + { genRecursiveCount :: Integer + , genExpr :: HsExpr GhcPs + } + + +------------------------------------------------------------------------------ +-- | Make a 'Generator' for a given tycon instantiated with the given @[Type]@. +mkGenerator :: TyCon -> [Type] -> DataCon -> Generator +mkGenerator tc apps dc = do + let dc_expr = var' $ occName $ dataConName dc + args = dataConInstOrigArgTys' dc apps + num_recursive_calls = sum $ fmap (bool 0 1 . doesTypeContain tc) args + mkArbitrary = mkArbitraryCall tc num_recursive_calls + Generator num_recursive_calls $ case args of + [] -> mkFunc "pure" @@ dc_expr + (a : as) -> + foldl' + (infixCall "<*>") + (infixCall "<$>" dc_expr $ mkArbitrary a) + (fmap mkArbitrary as) + + +------------------------------------------------------------------------------ +-- | Check if the given 'TyCon' exists anywhere in the 'Type'. +doesTypeContain :: TyCon -> Type -> Bool +doesTypeContain recursive_tc = + everything (||) $ mkQ False (== recursive_tc) + + +------------------------------------------------------------------------------ +-- | Generate the correct sort of call to @arbitrary@. For recursive calls, we +-- need to scale down the size parameter, either by a constant factor of 1 if +-- it's the only recursive parameter, or by @`div` n@ where n is the number of +-- recursive parameters. For all other types, just call @arbitrary@ directly. +mkArbitraryCall :: TyCon -> Integer -> Type -> HsExpr GhcPs +mkArbitraryCall recursive_tc n ty = + let arbitrary = mkFunc "arbitrary" + in case doesTypeContain recursive_tc ty of + True -> + mkFunc "scale" + @@ bool (mkFunc "flip" @@ mkFunc "div" @@ int n) + (mkFunc "subtract" @@ int 1) + (n == 1) + @@ arbitrary + False -> arbitrary + diff --git a/src/Ide/Plugin/Tactic/Machinery.hs b/src/Ide/Plugin/Tactic/Machinery.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Machinery.hs @@ -0,0 +1,254 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Ide.Plugin.Tactic.Machinery + ( module Ide.Plugin.Tactic.Machinery + ) where + +import Class (Class(classTyVars)) +import Control.Arrow +import Control.Monad.Error.Class +import Control.Monad.Reader +import Control.Monad.State (MonadState(..)) +import Control.Monad.State.Class (gets, modify) +import Control.Monad.State.Strict (StateT (..)) +import Data.Bool (bool) +import Data.Coerce +import Data.Either +import Data.Foldable +import Data.Functor ((<&>)) +import Data.Generics (mkQ, everything, gcount) +import Data.List (sortBy) +import qualified Data.Map as M +import Data.Ord (comparing, Down(..)) +import Data.Set (Set) +import qualified Data.Set as S +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Types +import OccName (HasOccName(occName)) +import Refinery.ProofState +import Refinery.Tactic +import Refinery.Tactic.Internal +import TcType +import Type +import Unify + + +substCTy :: TCvSubst -> CType -> CType +substCTy subst = coerce . substTy subst . coerce + + +------------------------------------------------------------------------------ +-- | Produce a subgoal that must be solved before we can solve the original +-- goal. +newSubgoal + :: Judgement + -> Rule +newSubgoal j = do + unifier <- gets ts_unifier + subgoal + $ substJdg unifier + $ unsetIsTopHole j + + +------------------------------------------------------------------------------ +-- | Attempt to generate a term of the right type using in-scope bindings, and +-- a given tactic. +runTactic + :: Context + -> Judgement + -> TacticsM () -- ^ Tactic to use + -> Either [TacticError] RunTacticResults +runTactic ctx jdg t = + let skolems = S.fromList + $ foldMap (tyCoVarsOfTypeWellScoped . unCType) + $ (:) (jGoal jdg) + $ fmap hi_type + $ toList + $ jHypothesis jdg + unused_topvals = M.keysSet + $ M.filter (isTopLevel . hi_provenance) + $ jHypothesis jdg + tacticState = + defaultTacticState + { ts_skolems = skolems + , ts_unused_top_vals = unused_topvals + } + in case partitionEithers + . flip runReader ctx + . unExtractM + $ runTacticT t jdg tacticState of + (errs, []) -> Left $ take 50 $ errs + (_, fmap assoc23 -> solns) -> do + let sorted = + flip sortBy solns $ comparing $ \((_, ext), (jdg, holes)) -> + Down $ scoreSolution ext jdg holes + case sorted of + (((tr, ext), _) : _) -> + Right + . RunTacticResults tr ext + . reverse + . fmap fst + $ take 5 sorted + -- guaranteed to not be empty + _ -> Left [] + +assoc23 :: (a, b, c) -> (a, (b, c)) +assoc23 (a, b, c) = (a, (b, c)) + + +tracePrim :: String -> Trace +tracePrim = flip rose [] + + +tracing + :: Functor m + => String + -> TacticT jdg (Trace, ext) err s m a + -> TacticT jdg (Trace, ext) err s m a +tracing s (TacticT m) + = TacticT $ StateT $ \jdg -> + mapExtract' (first $ rose s . pure) $ runStateT m jdg + + +------------------------------------------------------------------------------ +-- | Recursion is allowed only when we can prove it is on a structurally +-- smaller argument. The top of the 'ts_recursion_stack' witnesses the smaller +-- pattern val. +guardStructurallySmallerRecursion + :: TacticState + -> Maybe TacticError +guardStructurallySmallerRecursion s = + case head $ ts_recursion_stack s of + Just _ -> Nothing + Nothing -> Just NoProgress + + +------------------------------------------------------------------------------ +-- | Mark that the current recursive call is structurally smaller, due to +-- having been matched on a pattern value. +-- +-- Implemented by setting the top of the 'ts_recursion_stack'. +markStructuralySmallerRecursion :: MonadState TacticState m => PatVal -> m () +markStructuralySmallerRecursion pv = do + modify $ withRecursionStack $ \case + (_ : bs) -> Just pv : bs + [] -> [] + + +------------------------------------------------------------------------------ +-- | Given the results of running a tactic, score the solutions by +-- desirability. +-- +-- TODO(sandy): This function is completely unprincipled and was just hacked +-- together to produce the right test results. +scoreSolution + :: LHsExpr GhcPs + -> TacticState + -> [Judgement] + -> ( Penalize Int -- number of holes + , Reward Bool -- all bindings used + , Penalize Int -- unused top-level bindings + , Penalize Int -- number of introduced bindings + , Reward Int -- number used bindings + , Penalize Int -- number of recursive calls + , Penalize Int -- size of extract + ) +scoreSolution ext TacticState{..} holes + = ( Penalize $ length holes + , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals + , Penalize $ S.size ts_unused_top_vals + , Penalize $ S.size ts_intro_vals + , Reward $ S.size ts_used_vals + , Penalize $ ts_recursion_count + , Penalize $ solutionSize ext + ) + + +------------------------------------------------------------------------------ +-- | Compute the number of 'LHsExpr' nodes; used as a rough metric for code +-- size. +solutionSize :: LHsExpr GhcPs -> Int +solutionSize = everything (+) $ gcount $ mkQ False $ \case + (_ :: LHsExpr GhcPs) -> True + + +newtype Penalize a = Penalize a + deriving (Eq, Ord, Show) via (Down a) + +newtype Reward a = Reward a + 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 + + + +------------------------------------------------------------------------------ +-- | Attempt to unify two types. +unify :: CType -- ^ The goal type + -> CType -- ^ The type we are trying unify the goal type with + -> RuleM () +unify goal inst = do + skolems <- gets ts_skolems + case tryUnifyUnivarsButNotSkolems skolems goal inst of + Just subst -> + modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) }) + Nothing -> throwError (UnificationError inst goal) + + +------------------------------------------------------------------------------ +-- | Get the class methods of a 'PredType', correctly dealing with +-- instantiation of quantified class types. +methodHypothesis :: PredType -> Maybe [(OccName, 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 + sc_methods <- fmap join + $ traverse (methodHypothesis . substTy subst) + $ classSCTheta cls + pure $ mappend sc_methods $ methods <&> \method -> + let (_, _, ty) = tcSplitSigmaTy $ idType method + in ( occName method + , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty + ) + + +------------------------------------------------------------------------------ +-- | Run the given tactic iff the current hole contains no univars. Skolems and +-- already decided univars are OK though. +requireConcreteHole :: TacticsM a -> TacticsM a +requireConcreteHole m = do + jdg <- goal + skolems <- gets ts_skolems + let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg + case S.size $ vars S.\\ skolems of + 0 -> m + _ -> throwError TooPolymorphic + diff --git a/src/Ide/Plugin/Tactic/Naming.hs b/src/Ide/Plugin/Tactic/Naming.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Naming.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Naming where + +import Control.Monad.State.Strict +import Data.Bool (bool) +import Data.Char +import Data.Map (Map) +import qualified Data.Map as M +import Data.Traversable +import Name +import TcType +import TyCon +import Type +import TysWiredIn (listTyCon, pairTyCon, unitTyCon) + + +------------------------------------------------------------------------------ +-- | Use type information to create a reasonable name. +mkTyName :: Type -> String +-- eg. mkTyName (a -> B) = "fab" +mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) + = "f" ++ mkTyName a ++ mkTyName b +-- eg. mkTyName (a -> b -> C) = "f_C" +mkTyName (tcSplitFunTys -> ((_:_), b)) + = "f_" ++ mkTyName b +-- eg. mkTyName (Either A B) = "eab" +mkTyName (splitTyConApp_maybe -> Just (c, args)) + = mkTyConName c ++ foldMap mkTyName args +-- eg. mkTyName a = "a" +mkTyName (getTyVar_maybe -> Just tv) + = occNameString $ occName tv +-- eg. mkTyName (forall x. y) = "y" +mkTyName (tcSplitSigmaTy -> ((_:_), _, t)) + = mkTyName t +mkTyName _ = "x" + + +------------------------------------------------------------------------------ +-- | Get a good name for a type constructor. +mkTyConName :: TyCon -> String +mkTyConName tc + | tc == listTyCon = "l_" + | tc == pairTyCon = "p_" + | tc == unitTyCon = "unit" + | otherwise + = take 1 + . fmap toLower + . filterReplace isSymbol 's' + . filterReplace isPunctuation 'p' + . occNameString + $ getOccName tc + + +------------------------------------------------------------------------------ +-- | Maybe replace an element in the list if the predicate matches +filterReplace :: (a -> Bool) -> a -> [a] -> [a] +filterReplace f r = fmap (\a -> bool a r $ f a) + + +------------------------------------------------------------------------------ +-- | Produce a unique, good name for a type. +mkGoodName + :: [OccName] -- ^ Bindings in scope; used to ensure we don't shadow anything + -> Type -- ^ The type to produce a name for + -> OccName +mkGoodName in_scope t = + let tn = mkTyName t + in mkVarOcc $ case elem (mkVarOcc tn) in_scope of + True -> tn ++ show (length in_scope) + False -> tn + + +------------------------------------------------------------------------------ +-- | Like 'mkGoodName' but creates several apart names. +mkManyGoodNames + :: (Traversable t, Monad m) + => M.Map OccName a + -> t Type + -> m (t OccName) +mkManyGoodNames hy args = + flip evalStateT (getInScope hy) $ for args $ \at -> do + in_scope <- get + let n = mkGoodName in_scope at + modify (n :) + pure n + + +------------------------------------------------------------------------------ +-- | Which names are in scope? +getInScope :: Map OccName a -> [OccName] +getInScope = M.keys + diff --git a/src/Ide/Plugin/Tactic/Range.hs b/src/Ide/Plugin/Tactic/Range.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Range.hs @@ -0,0 +1,18 @@ +module Ide.Plugin.Tactic.Range where + +import qualified FastString as FS +import Development.IDE.Types.Location +import SrcLoc + +------------------------------------------------------------------------------ +-- | Convert a DAML compiler Range to a GHC SrcSpan +-- TODO(sandy): this doesn't belong here +rangeToSrcSpan :: String -> Range -> SrcSpan +rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range + +rangeToRealSrcSpan :: String -> Range -> RealSrcSpan +rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = + mkRealSrcSpan + (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) + (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) + diff --git a/src/Ide/Plugin/Tactic/Tactics.hs b/src/Ide/Plugin/Tactic/Tactics.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Tactics.hs @@ -0,0 +1,287 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Tactics + ( module Ide.Plugin.Tactic.Tactics + , runTactic + ) where + +import Control.Monad (when) +import Control.Monad.Except (throwError) +import Control.Monad.Reader.Class (MonadReader(ask)) +import Control.Monad.State.Class +import Control.Monad.State.Strict (StateT(..), runStateT) +import Data.Bool (bool) +import Data.Foldable +import Data.List +import qualified Data.Map as M +import Data.Maybe +import qualified Data.Set as S +import DataCon +import Development.IDE.GHC.Compat +import GHC.Exts +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import Ide.Plugin.Tactic.CodeGen +import Ide.Plugin.Tactic.Context +import Ide.Plugin.Tactic.GHC +import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Naming +import Ide.Plugin.Tactic.Types +import Name (occNameString) +import Refinery.Tactic +import Refinery.Tactic.Internal +import TcType +import Type hiding (Var) + + +------------------------------------------------------------------------------ +-- | Use something in the hypothesis to fill the hole. +assumption :: TacticsM () +assumption = attemptOn allNames assume + + +------------------------------------------------------------------------------ +-- | Use something named in the hypothesis to fill the hole. +assume :: OccName -> TacticsM () +assume name = rule $ \jdg -> do + let g = jGoal jdg + case M.lookup name $ jHypothesis jdg of + Just (hi_type -> ty) -> do + unify ty $ jGoal jdg + for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion + useOccName jdg name + pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name + Nothing -> throwError $ UndefinedHypothesis name + + +recursion :: TacticsM () +recursion = requireConcreteHole $ tracing "recursion" $ do + defs <- getCurrentDefinitions + attemptOn (const $ fmap fst defs) $ \name -> do + modify $ pushRecursionStack . countRecursiveCall + ensure guardStructurallySmallerRecursion popRecursionStack $ do + (localTactic (apply name) $ introducingRecursively defs) + <@> fmap (localTactic assumption . filterPosition name) [0..] + + +------------------------------------------------------------------------------ +-- | Introduce a lambda binding every variable. +intros :: TacticsM () +intros = rule $ \jdg -> do + let hy = jHypothesis jdg + g = jGoal jdg + ctx <- ask + case tcSplitFunTys $ unCType g of + ([], _) -> throwError $ GoalMismatch "intros" g + (as, b) -> do + vs <- mkManyGoodNames (jEntireHypothesis jdg) as + let top_hole = isTopHole ctx jdg + jdg' = introducingLambda top_hole (zip vs $ coerce as) + $ withNewGoal (CType b) jdg + modify $ withIntroducedVals $ mappend $ S.fromList vs + when (isJust top_hole) $ addUnusedTopVals $ S.fromList vs + (tr, sg) <- newSubgoal jdg' + pure + . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, ) + . noLoc + . lambda (fmap bvar' vs) + $ unLoc sg + + +------------------------------------------------------------------------------ +-- | Case split, and leave holes in the matches. +destructAuto :: OccName -> TacticsM () +destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do + jdg <- goal + case M.lookup name $ jHypothesis jdg of + Nothing -> throwError $ NotInScope name + Just hi -> + let subtactic = rule $ destruct' (const subgoal) name + in case isPatternMatch $ hi_provenance hi of + True -> + pruning subtactic $ \jdgs -> + let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis + new_hy = foldMap getHyTypes jdgs + old_hy = getHyTypes jdg + in case S.null $ new_hy S.\\ old_hy of + True -> Just $ UnhelpfulDestruct name + False -> Nothing + False -> subtactic + + +------------------------------------------------------------------------------ +-- | Case split, and leave holes in the matches. +destruct :: OccName -> TacticsM () +destruct name = requireConcreteHole $ tracing "destruct(user)" $ + rule $ destruct' (const subgoal) name + + +------------------------------------------------------------------------------ +-- | Case split, using the same data constructor in the matches. +homo :: OccName -> TacticsM () +homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg -> + buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) + + +------------------------------------------------------------------------------ +-- | LambdaCase split, and leave holes in the matches. +destructLambdaCase :: TacticsM () +destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal) + + +------------------------------------------------------------------------------ +-- | LambdaCase split, using the same data constructor in the matches. +homoLambdaCase :: TacticsM () +homoLambdaCase = + tracing "homoLambdaCase" $ + rule $ destructLambdaCase' $ \dc jdg -> + buildDataCon jdg dc + . snd + . splitAppTys + . unCType + $ jGoal jdg + + +apply :: OccName -> TacticsM () +apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do + jdg <- goal + let hy = jHypothesis jdg + g = jGoal jdg + case M.lookup func hy of + Just (hi_type -> CType ty) -> do + ty' <- freshTyvars ty + let (_, _, args, ret) = tacticsSplitFunTy ty' + requireNewHoles $ rule $ \jdg -> do + unify g (CType ret) + useOccName jdg func + (tr, sgs) + <- fmap unzipTrace + $ traverse ( newSubgoal + . blacklistingDestruct + . flip withNewGoal jdg + . CType + ) args + pure + . (tr, ) + . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + Nothing -> do + throwError $ GoalMismatch "apply" g + + +------------------------------------------------------------------------------ +-- | Choose between each of the goal's data constructors. +split :: TacticsM () +split = tracing "split(user)" $ do + jdg <- goal + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Nothing -> throwError $ GoalMismatch "split" g + Just (tc, _) -> do + let dcs = tyConDataCons tc + choice $ fmap splitDataCon dcs + + +------------------------------------------------------------------------------ +-- | Choose between each of the goal's data constructors. Different than +-- 'split' because it won't split a data con if it doesn't result in any new +-- goals. +splitAuto :: TacticsM () +splitAuto = requireConcreteHole $ tracing "split(auto)" $ do + jdg <- goal + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Nothing -> throwError $ GoalMismatch "split" g + Just (tc, _) -> do + let dcs = tyConDataCons tc + case isSplitWhitelisted jdg of + True -> choice $ fmap splitDataCon dcs + False -> do + choice $ flip fmap dcs $ \dc -> requireNewHoles $ + splitDataCon dc + + +------------------------------------------------------------------------------ +-- | Allow the given tactic to proceed if and only if it introduces holes that +-- have a different goal than current goal. +requireNewHoles :: TacticsM () -> TacticsM () +requireNewHoles m = do + jdg <- goal + pruning m $ \jdgs -> + case null jdgs || any (/= jGoal jdg) (fmap jGoal jdgs) of + True -> Nothing + False -> Just NoProgress + + +------------------------------------------------------------------------------ +-- | Attempt to instantiate the given data constructor to solve the goal. +splitDataCon :: DataCon -> TacticsM () +splitDataCon dc = + requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Just (tc, apps) -> do + case elem dc $ tyConDataCons tc of + True -> buildDataCon (unwhitelistingSplit jdg) dc apps + False -> throwError $ IncorrectDataCon dc + Nothing -> throwError $ GoalMismatch "splitDataCon" g + + +------------------------------------------------------------------------------ +-- | @matching f@ takes a function from a judgement to a @Tactic@, and +-- then applies the resulting @Tactic@. +matching :: (Judgement -> TacticsM ()) -> TacticsM () +matching f = TacticT $ StateT $ \s -> runStateT (unTacticT $ f s) s + + +attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM () +attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames) + + +localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a +localTactic t f = do + TacticT $ StateT $ \jdg -> + runStateT (unTacticT t) $ f jdg + + +auto' :: Int -> TacticsM () +auto' 0 = throwError NoProgress +auto' n = do + let loop = auto' (n - 1) + try intros + choice + [ overFunctions $ \fname -> do + apply fname + loop + , overAlgebraicTerms $ \aname -> do + destructAuto aname + loop + , splitAuto >> loop + , assumption >> loop + , recursion + ] + +overFunctions :: (OccName -> TacticsM ()) -> TacticsM () +overFunctions = + attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis + +overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM () +overAlgebraicTerms = + attemptOn $ + M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis + + +allNames :: Judgement -> [OccName] +allNames = M.keys . jHypothesis + diff --git a/src/Ide/Plugin/Tactic/TestTypes.hs b/src/Ide/Plugin/Tactic/TestTypes.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/TestTypes.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Ide.Plugin.Tactic.TestTypes where + +import qualified Data.Text as T + +------------------------------------------------------------------------------ +-- | The list of tactics exposed to the outside world. These are attached to +-- actual tactics via 'commandTactic' and are contextually provided to the +-- editor via 'commandProvider'. +data TacticCommand + = Auto + | Intros + | Destruct + | Homomorphism + | DestructLambdaCase + | HomomorphismLambdaCase + deriving (Eq, Ord, Show, Enum, Bounded) + +-- | Generate a title for the command. +tacticTitle :: TacticCommand -> T.Text -> T.Text +tacticTitle Auto _ = "Attempt to fill hole" +tacticTitle Intros _ = "Introduce lambda" +tacticTitle Destruct var = "Case split on " <> var +tacticTitle Homomorphism var = "Homomorphic case split on " <> var +tacticTitle DestructLambdaCase _ = "Lambda case split" +tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split" diff --git a/src/Ide/Plugin/Tactic/Types.hs b/src/Ide/Plugin/Tactic/Types.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Types.hs @@ -0,0 +1,367 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module Ide.Plugin.Tactic.Types + ( module Ide.Plugin.Tactic.Types + , module Ide.Plugin.Tactic.Debug + , OccName + , Name + , Type + , TyVar + , Span + , Range + ) where + +import Control.Lens hiding (Context) +import Control.Monad.Reader +import Control.Monad.State +import Data.Coerce +import Data.Function +import Data.Generics.Product (field) +import Data.Map (Map) +import Data.Set (Set) +import Data.Tree +import Development.IDE.GHC.Compat hiding (Node) +import Development.IDE.GHC.Orphans () +import Development.IDE.Types.Location +import GHC.Generics +import Ide.Plugin.Tactic.Debug +import OccName +import Refinery.Tactic +import System.IO.Unsafe (unsafePerformIO) +import Type +import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply) +import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique) + + +------------------------------------------------------------------------------ +-- | A wrapper around 'Type' which supports equality and ordering. +newtype CType = CType { unCType :: Type } + +instance Eq CType where + (==) = eqType `on` unCType + +instance Ord CType where + compare = nonDetCmpType `on` unCType + +instance Show CType where + show = unsafeRender . unCType + +instance Show OccName where + show = unsafeRender + +instance Show Var where + show = unsafeRender + +instance Show TCvSubst where + show = unsafeRender + +instance Show DataCon where + show = unsafeRender + +instance Show Class where + show = unsafeRender + + +------------------------------------------------------------------------------ +data TacticState = TacticState + { ts_skolems :: !(Set TyVar) + -- ^ The known skolems. + , ts_unifier :: !(TCvSubst) + -- ^ The current substitution of univars. + , ts_used_vals :: !(Set OccName) + -- ^ Set of values used by tactics. + , ts_intro_vals :: !(Set OccName) + -- ^ Set of values introduced by tactics. + , ts_unused_top_vals :: !(Set OccName) + -- ^ Set of currently unused arguments to the function being defined. + , ts_recursion_stack :: ![Maybe PatVal] + -- ^ Stack for tracking whether or not the current recursive call has + -- used at least one smaller pat val. Recursive calls for which this + -- value is 'False' are guaranteed to loop, and must be pruned. + , ts_recursion_count :: !Int + -- ^ Number of calls to recursion. We penalize each. + , ts_unique_gen :: !UniqSupply + } deriving stock (Show, Generic) + +instance Show UniqSupply where + show _ = "" + + +------------------------------------------------------------------------------ +-- | A 'UniqSupply' to use in 'defaultTacticState' +unsafeDefaultUniqueSupply :: UniqSupply +unsafeDefaultUniqueSupply = + unsafePerformIO $ mkSplitUniqSupply '🚒' +{-# NOINLINE unsafeDefaultUniqueSupply #-} + + +defaultTacticState :: TacticState +defaultTacticState = + TacticState + { ts_skolems = mempty + , ts_unifier = emptyTCvSubst + , ts_used_vals = mempty + , ts_intro_vals = mempty + , ts_unused_top_vals = mempty + , ts_recursion_stack = mempty + , ts_recursion_count = 0 + , ts_unique_gen = unsafeDefaultUniqueSupply + } + + +------------------------------------------------------------------------------ +-- | Generate a new 'Unique' +freshUnique :: MonadState TacticState m => m Unique +freshUnique = do + (uniq, supply) <- gets $ takeUniqFromSupply . ts_unique_gen + modify' $! field @"ts_unique_gen" .~ supply + pure uniq + + +withRecursionStack + :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState +withRecursionStack f = + field @"ts_recursion_stack" %~ f + +pushRecursionStack :: TacticState -> TacticState +pushRecursionStack = withRecursionStack (Nothing :) + +popRecursionStack :: TacticState -> TacticState +popRecursionStack = withRecursionStack tail + + +withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState +withUsedVals f = + field @"ts_used_vals" %~ f + + +withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState +withIntroducedVals f = + field @"ts_intro_vals" %~ f + + +------------------------------------------------------------------------------ +-- | Describes where hypotheses came from. Used extensively to prune stupid +-- solutions from the search space. +data Provenance + = -- | An argument given to the topmost function that contains the current + -- hole. Recursive calls are restricted to values whose provenance lines up + -- with the same argument. + TopLevelArgPrv + OccName -- ^ Binding function + Int -- ^ Argument Position + -- | A binding created in a pattern match. + | PatternMatchPrv PatVal + -- | A class method from the given context. + | ClassMethodPrv + (Uniquely Class) -- ^ Class + -- | A binding explicitly written by the user. + | UserPrv + -- | The recursive hypothesis. Present only in the context of the recursion + -- tactic. + | RecursivePrv + -- | A hypothesis which has been disallowed for some reason. It's important + -- 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) + + +------------------------------------------------------------------------------ +-- | Why was a hypothesis disallowed? +data DisallowReason + = WrongBranch Int + | Shadowed + | RecursiveCall + | AlreadyDestructed + deriving stock (Eq, Show, Generic, Ord) + + +------------------------------------------------------------------------------ +-- | Provenance of a pattern value. +data PatVal = PatVal + { pv_scrutinee :: Maybe OccName + -- ^ Original scrutinee which created this PatVal. Nothing, for lambda + -- case. + , pv_ancestry :: Set OccName + -- ^ The set of values which had to be destructed to discover this term. + -- Always contains the scrutinee. + , pv_datacon :: Uniquely DataCon + -- ^ 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) + + +------------------------------------------------------------------------------ +-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord' +-- instances. +newtype Uniquely a = Uniquely { getViaUnique :: a } + deriving Show via a + +instance Uniquable a => Eq (Uniquely a) where + (==) = (==) `on` getUnique . getViaUnique + +instance Uniquable a => Ord (Uniquely a) where + compare = nonDetCmpUnique `on` getUnique . getViaUnique + + +------------------------------------------------------------------------------ +-- | The provenance and type of a hypothesis term. +data HyInfo a = HyInfo + { hi_provenance :: Provenance + , hi_type :: a + } + deriving stock (Functor, Eq, Show, Generic, Ord) + + +------------------------------------------------------------------------------ +-- | Map a function over the provenance. +overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a +overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty + + +------------------------------------------------------------------------------ +-- | The current bindings and goal for a hole to be filled by refinery. +data Judgement' a = Judgement + { _jHypothesis :: !(Map OccName (HyInfo a)) + , _jBlacklistDestruct :: !(Bool) + , _jWhitelistSplit :: !(Bool) + , _jIsTopHole :: !Bool + , _jGoal :: !(a) + } + deriving stock (Eq, Generic, Functor, Show) + +type Judgement = Judgement' CType + + +newtype ExtractM a = ExtractM { unExtractM :: Reader Context a } + deriving (Functor, Applicative, Monad, MonadReader Context) + +------------------------------------------------------------------------------ +-- | Orphan instance for producing holes when attempting to solve tactics. +instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where + hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_") + + +------------------------------------------------------------------------------ +-- | Reasons a tactic might fail. +data TacticError + = UndefinedHypothesis OccName + | GoalMismatch String CType + | UnsolvedSubgoals [Judgement] + | UnificationError CType CType + | NoProgress + | NoApplicableTactic + | IncorrectDataCon DataCon + | RecursionOnWrongParam OccName Int OccName + | UnhelpfulDestruct OccName + | UnhelpfulSplit OccName + | TooPolymorphic + | NotInScope OccName + deriving stock (Eq) + +instance Show TacticError where + show (UndefinedHypothesis name) = + occNameString name <> " is not available in the hypothesis." + show (GoalMismatch tac (CType typ)) = + mconcat + [ "The tactic " + , tac + , " 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 (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 + + +------------------------------------------------------------------------------ +type TacticsM = TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM +type RuleM = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM +type Rule = RuleM (Trace, LHsExpr GhcPs) + +type Trace = Rose String + + +------------------------------------------------------------------------------ +-- | The Reader context of tactics and rules +data Context = Context + { ctxDefiningFuncs :: [(OccName, CType)] + -- ^ The functions currently being defined + , ctxModuleFuncs :: [(OccName, CType)] + -- ^ Everything defined in the current module + } + deriving stock (Eq, Ord) + + +------------------------------------------------------------------------------ +-- | An empty context +emptyContext :: Context +emptyContext = Context mempty mempty + + +newtype Rose a = Rose (Tree a) + deriving stock (Eq, Functor, Generic) + +instance Show (Rose String) where + show = unlines . dropEveryOther . lines . drawTree . coerce + +dropEveryOther :: [a] -> [a] +dropEveryOther [] = [] +dropEveryOther [a] = [a] +dropEveryOther (a : _ : as) = a : dropEveryOther as + +instance Semigroup a => Semigroup (Rose a) where + Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs) + +instance Monoid a => Monoid (Rose a) where + mempty = Rose $ Node mempty mempty + +rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a +rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs +rose a rs = Rose $ Node a $ coerce rs + + +------------------------------------------------------------------------------ +-- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic' +data RunTacticResults = RunTacticResults + { rtr_trace :: Trace + , rtr_extract :: LHsExpr GhcPs + , rtr_other_solns :: [(Trace, LHsExpr GhcPs)] + } deriving Show + diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs new file mode 100644 --- /dev/null +++ b/src/Ide/TreeTransform.hs @@ -0,0 +1,122 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ide.TreeTransform + ( Graft, graft, transform, useAnnotatedSource + ) where + +import BasicTypes (appPrec) +import Control.Monad +import Control.Monad.Trans.Class +import qualified Data.Text as T +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Rules +import Development.IDE.Core.Shake +import Development.IDE.GHC.Compat hiding (parseExpr) +import Development.IDE.Types.Location +import Generics.SYB +import Ide.PluginUtils +import Language.Haskell.GHC.ExactPrint +import Language.Haskell.GHC.ExactPrint.Parsers +import Language.Haskell.LSP.Types +import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) +import Outputable +import Retrie.ExactPrint hiding (parseExpr) + + +------------------------------------------------------------------------------ +-- | Get the latest version of the annotated parse source. +useAnnotatedSource + :: String + -> IdeState + -> NormalizedFilePath + -> IO (Maybe (Annotated ParsedSource)) +useAnnotatedSource herald state nfp = do + pm <- runAction herald state $ use GetParsedModule nfp + pure $ fmap fixAnns pm + + +------------------------------------------------------------------------------ +-- | A transformation for grafting source trees together. Use the semigroup +-- instance to combine 'Graft's, and run them via 'transform'. +newtype Graft a = Graft + { runGraft :: DynFlags -> a -> TransformT (Either String) a + } + +instance Semigroup (Graft a) where + Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags + +instance Monoid (Graft a) where + mempty = Graft $ const pure + + +------------------------------------------------------------------------------ +-- | Convert a 'Graft' into a 'WorkspaceEdit'. +transform + :: DynFlags + -> ClientCapabilities + -> Uri + -> Graft ParsedSource + -> Annotated ParsedSource + -> Either String WorkspaceEdit +transform dflags ccs uri f a = do + let src = printA a + a' <- transformA a $ runGraft f dflags + let res = printA a' + pure $ diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions + + +------------------------------------------------------------------------------ +-- | Construct a 'Graft', replacing the node at the given 'SrcSpan' with the +-- given 'LHSExpr'. The node at that position must already be a 'LHsExpr', or +-- this is a no-op. +graft + :: forall a + . Data a + => SrcSpan + -> LHsExpr GhcPs + -> Graft a +graft dst val = Graft $ \dflags a -> do + (anns, val') <- annotate dflags $ parenthesize val + modifyAnnsT $ mappend anns + pure $ everywhere' + ( mkT $ + \case + (L src _ :: LHsExpr GhcPs) | src == dst -> val' + l -> l + ) a + + +------------------------------------------------------------------------------ +-- | Dark magic I stole from retrie. No idea what it does. +fixAnns :: ParsedModule -> Annotated ParsedSource +fixAnns ParsedModule {..} = + let ranns = relativiseApiAnns pm_parsed_source pm_annotations + in unsafeMkA pm_parsed_source ranns 0 + + +------------------------------------------------------------------------------ +-- | Given an 'LHSExpr', compute its exactprint annotations. +annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs) +annotate dflags expr = do + uniq <- show <$> uniqueSrcSpanT + let rendered = render dflags expr + (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered + let anns' = setPrecedingLines expr' 0 1 anns + pure (anns', expr') + + +------------------------------------------------------------------------------ +-- | Print out something 'Outputable'. +render :: Outputable a => DynFlags -> a -> String +render dflags = showSDoc dflags . ppr + + +------------------------------------------------------------------------------ +-- | Put parentheses around an expression if required. +parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs +parenthesize = parenthesizeHsExpr appPrec + diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs new file mode 100644 --- /dev/null +++ b/test/AutoTupleSpec.hs @@ -0,0 +1,57 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module AutoTupleSpec where + +import Data.Either (isRight) +import qualified Data.Map as M +import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.Judgements (mkFirstJudgement) +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Tactics (auto') +import Ide.Plugin.Tactic.Types +import OccName (mkVarOcc) +import Test.Hspec +import Test.QuickCheck +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) + + +instance Show Type where + show = unsafeRender + + +spec :: Spec +spec = describe "auto for tuple" $ do + it "should always be able to discover an auto solution" $ do + property $ do + -- Pick some number of variables + n <- choose (1, 7) + let vars = fmap mkTyVarTy $ take n alphaTyVars + -- Pick a random ordering + in_vars <- shuffle vars + -- Randomly associate them into tuple types + in_type <- mkBoxedTupleTy + . fmap mkBoxedTupleTy + <$> randomGroups in_vars + out_type <- mkBoxedTupleTy + . fmap mkBoxedTupleTy + <$> randomGroups vars + pure $ + -- We should always be able to find a solution + runTactic + emptyContext + (mkFirstJudgement + (M.singleton (mkVarOcc "x") $ HyInfo UserPrv $ CType in_type) + True + out_type) + (auto' $ n * 2) `shouldSatisfy` isRight + + +randomGroups :: [a] -> Gen [[a]] +randomGroups [] = pure [] +randomGroups as = do + n <- choose (1, length as) + (:) <$> pure (take n as) + <*> randomGroups (drop n as) + diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover -optF --module-name=Main #-} diff --git a/test/UnificationSpec.hs b/test/UnificationSpec.hs new file mode 100644 --- /dev/null +++ b/test/UnificationSpec.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module UnificationSpec where + +import Control.Arrow +import Data.Bool (bool) +import Data.Functor ((<&>)) +import Data.Maybe (mapMaybe) +import qualified Data.Set as S +import Data.Traversable +import Data.Tuple (swap) +import Ide.Plugin.Tactic.Debug +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Types +import TcType (tcGetTyVar_maybe, substTy) +import Test.Hspec +import Test.QuickCheck +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) + + +instance Show Type where + show = unsafeRender + + +spec :: Spec +spec = describe "unification" $ do + it "should be able to unify univars with skolems on either side of the equality" $ do + property $ do + -- Pick some number of unification vars and skolem + n <- choose (1, 1) + let (skolems, take n -> univars) = splitAt n $ fmap mkTyVarTy alphaTyVars + -- Randomly pair them + skolem_uni_pairs <- + for (zip skolems univars) randomSwap + let (lhs, rhs) + = mkBoxedTupleTy *** mkBoxedTupleTy + $ unzip skolem_uni_pairs + pure $ + counterexample (show skolems) $ + counterexample (show lhs) $ + counterexample (show rhs) $ + case tryUnifyUnivarsButNotSkolems + (S.fromList $ mapMaybe tcGetTyVar_maybe skolems) + (CType lhs) + (CType rhs) of + Just subst -> + -- For each pair, running the unification over the univar should + -- result in the skolem + conjoin $ zip univars skolems <&> \(uni, skolem) -> + let substd = substTy subst uni + in counterexample (show substd) $ + counterexample (show skolem) $ + CType substd === CType skolem + Nothing -> True === False + + +randomSwap :: (a, a) -> Gen (a, a) +randomSwap ab = do + which <- arbitrary + pure $ bool swap id which ab + +