{-# 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
    ]