module Wingman.KnownStrategies where

import Data.Foldable (for_)
import Development.IDE.GHC.Compat.Core
import Refinery.Tactic
import Wingman.Judgements (jGoal)
import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
import Wingman.Machinery (tracing, getKnownInstance, getCurrentDefinitions)
import Wingman.Tactics
import Wingman.Types


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
"mempty" TacticsM ()
deriveMempty
  , String -> TacticsM () -> TacticsM ()
known String
"arbitrary" TacticsM ()
deriveArbitrary
  , String -> TacticsM () -> TacticsM ()
known String
"<>" TacticsM ()
deriveMappend
  , String -> TacticsM () -> TacticsM ()
known String
"mappend" TacticsM ()
deriveMappend
  ]


known :: String -> TacticsM () -> TacticsM ()
known :: String -> TacticsM () -> TacticsM ()
known String
name TacticsM ()
t = do
  TacticsM [(OccName, CType)]
getCurrentDefinitions TacticsM [(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 (Synthesized ext) err s m a
-> TacticT jdg (Synthesized 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 err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure 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 (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated) TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> TacticsM ()
auto' Int
2
    , TacticsM ()
assumption
    , TacticsM ()
recursion
    ]


------------------------------------------------------------------------------
-- | We derive mappend by binding the arguments, introducing the constructor,
-- and then calling mappend recursively. At each recursive call, we filter away
-- any binding that isn't in an analogous position.
--
-- The recursive call first attempts to use an instace in scope. If that fails,
-- it fals back to trying a theta method from the hypothesis with the correct
-- name.
deriveMappend :: TacticsM ()
deriveMappend :: TacticsM ()
deriveMappend = 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
  TacticsM ()
destructAll
  TacticsM ()
split
  Judgement
g <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  Maybe (Class, PredType)
minst <- OccName -> [PredType] -> TacticsM (Maybe (Class, PredType))
getKnownInstance (String -> OccName
mkClsOcc String
"Semigroup")
         ([PredType] -> TacticsM (Maybe (Class, PredType)))
-> (CType -> [PredType])
-> CType
-> TacticsM (Maybe (Class, PredType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [PredType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
         (PredType -> [PredType])
-> (CType -> PredType) -> CType -> [PredType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> PredType
unCType
         (CType -> TacticsM (Maybe (Class, PredType)))
-> CType -> TacticsM (Maybe (Class, PredType))
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
g
  Maybe (Class, PredType)
-> ((Class, PredType) -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe (Class, PredType)
minst (((Class, PredType) -> TacticsM ()) -> TacticsM ())
-> ((Class, PredType) -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \(Class
cls, PredType
df) -> do
    TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication
      (Class -> PredType -> OccName -> TacticsM ()
applyMethod Class
cls PredType
df (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"<>")
      TacticsM ()
assumption
  TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try (TacticsM () -> TacticsM ()) -> TacticsM () -> TacticsM ()
forall a b. (a -> b) -> a -> b
$
    TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication
      (OccName -> TacticsM ()
applyByName (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"<>")
      TacticsM ()
assumption


------------------------------------------------------------------------------
-- | We derive mempty by introducing the constructor, and then trying to
-- 'mempty' everywhere. This smaller 'mempty' might come from an instance in
-- scope, or it might come from the hypothesis theta.
deriveMempty :: TacticsM ()
deriveMempty :: TacticsM ()
deriveMempty = do
  TacticsM ()
split
  Judgement
g <- TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Judgement
forall (m :: * -> *) jdg ext err s.
Functor m =>
TacticT jdg ext err s m jdg
goal
  Maybe (Class, PredType)
minst <- OccName -> [PredType] -> TacticsM (Maybe (Class, PredType))
getKnownInstance (String -> OccName
mkClsOcc String
"Monoid") [CType -> PredType
unCType (CType -> PredType) -> CType -> PredType
forall a b. (a -> b) -> a -> b
$ Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
g]
  Maybe (Class, PredType)
-> ((Class, PredType) -> TacticsM ()) -> TacticsM ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ Maybe (Class, PredType)
minst (((Class, PredType) -> TacticsM ()) -> TacticsM ())
-> ((Class, PredType) -> TacticsM ()) -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ \(Class
cls, PredType
df) -> do
    Class -> PredType -> OccName -> TacticsM ()
applyMethod Class
cls PredType
df (OccName -> TacticsM ()) -> OccName -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"mempty"
  TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
try TacticsM ()
assumption