{-# 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 :: TacticsM () knownStrategies = [TacticsM ()] -> TacticsM () forall (m :: * -> *) jdg ext err s a. Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a choice [ String -> TacticsM () -> TacticsM () known String "fmap" TacticsM () deriveFmap , String -> TacticsM () -> TacticsM () known String "arbitrary" TacticsM () deriveArbitrary ] known :: String -> TacticsM () -> TacticsM () known :: String -> TacticsM () -> TacticsM () known String name TacticsM () t = do TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM [(OccName, CType)] forall (m :: * -> *). MonadReader Context m => m [(OccName, CType)] getCurrentDefinitions TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM [(OccName, CType)] -> ([(OccName, CType)] -> TacticsM ()) -> TacticsM () forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \case [(OccName def, CType _)] | OccName def OccName -> OccName -> Bool forall a. Eq a => a -> a -> Bool == String -> OccName mkVarOcc String name -> String -> TacticsM () -> TacticsM () forall (m :: * -> *) jdg ext err s a. Functor m => String -> TacticT jdg (Trace, ext) err s m a -> TacticT jdg (Trace, ext) err s m a tracing (String "known " String -> String -> String forall a. Semigroup a => a -> a -> a <> String name) TacticsM () t [(OccName, CType)] _ -> TacticError -> TacticsM () forall e (m :: * -> *) a. MonadError e m => e -> m a throwError TacticError NoApplicableTactic deriveFmap :: TacticsM () deriveFmap :: TacticsM () deriveFmap = do TacticsM () -> TacticsM () forall (m :: * -> *) jdg ext err s. Monad m => TacticT jdg ext err s m () -> TacticT jdg ext err s m () try TacticsM () intros (HyInfo CType -> TacticsM ()) -> TacticsM () overAlgebraicTerms HyInfo CType -> TacticsM () homo [TacticsM ()] -> TacticsM () forall (m :: * -> *) jdg ext err s a. Monad m => [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a choice [ (HyInfo CType -> TacticsM ()) -> TacticsM () overFunctions HyInfo CType -> TacticsM () apply TacticsM () -> TacticsM () -> TacticsM () forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> Int -> TacticsM () auto' Int 2 , TacticsM () assumption , TacticsM () recursion ]