{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TupleSections    #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns     #-}

module Ide.Plugin.Tactic.CodeGen
  ( module Ide.Plugin.Tactic.CodeGen
  , module Ide.Plugin.Tactic.CodeGen.Utils
  ) 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.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           Ide.Plugin.Tactic.CodeGen.Utils
import           Type hiding (Var)


useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
useOccName :: Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
name =
  -- Only score points if this is in the local hypothesis
  case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (HyInfo CType) -> Maybe (HyInfo CType))
-> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jLocalHypothesis Judgement
jdg of
    Just{}  -> (TacticState -> TacticState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
             ((TacticState -> TacticState) -> m ())
-> (TacticState -> TacticState) -> m ()
forall a b. (a -> b) -> a -> b
$ ((Set OccName -> Set OccName) -> TacticState -> TacticState
withUsedVals ((Set OccName -> Set OccName) -> TacticState -> TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall a b. (a -> b) -> a -> b
$ OccName -> Set OccName -> Set OccName
forall a. Ord a => a -> Set a -> Set a
S.insert OccName
name)
             (TacticState -> TacticState)
-> (TacticState -> TacticState) -> TacticState -> TacticState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s t a b.
HasField "ts_unused_top_vals" s t a b =>
Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"ts_unused_top_vals" ((Set OccName -> Identity (Set OccName))
 -> TacticState -> Identity TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ OccName -> Set OccName -> Set OccName
forall a. Ord a => a -> Set a -> Set a
S.delete OccName
name)
    Maybe (HyInfo CType)
Nothing -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


------------------------------------------------------------------------------
-- | Doing recursion incurs a small penalty in the score.
countRecursiveCall :: TacticState -> TacticState
countRecursiveCall :: TacticState -> TacticState
countRecursiveCall = forall s t a b.
HasField "ts_recursion_count" s t a b =>
Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"ts_recursion_count" ((Int -> Identity Int) -> TacticState -> Identity TacticState)
-> Int -> TacticState -> TacticState
forall a s t. Num a => ASetter s t a a -> a -> s -> t
+~ Int
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 :: Set OccName -> m ()
addUnusedTopVals Set OccName
vals = (TacticState -> TacticState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState) -> m ())
-> (TacticState -> TacticState) -> m ()
forall a b. (a -> b) -> a -> b
$ forall s t a b.
HasField "ts_unused_top_vals" s t a b =>
Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"ts_unused_top_vals" ((Set OccName -> Identity (Set OccName))
 -> TacticState -> Identity TacticState)
-> Set OccName -> TacticState -> TacticState
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Set OccName
vals


destructMatches
    :: (DataCon -> Judgement -> Rule)
       -- ^ How to construct each match
    -> Maybe OccName
       -- ^ Scrutinee
    -> CType
       -- ^ Type being destructed
    -> Judgement
    -> RuleM (Trace, [RawMatch])
destructMatches :: (DataCon -> Judgement -> Rule)
-> Maybe OccName -> CType -> Judgement -> RuleM (Trace, [RawMatch])
destructMatches DataCon -> Judgement -> Rule
f Maybe OccName
scrut CType
t Judgement
jdg = do
  let hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis Judgement
jdg
      g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (Type -> Maybe (TyCon, [Type])) -> Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
t of
    Maybe (TyCon, [Type])
Nothing -> TacticError -> RuleM (Trace, [RawMatch])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> RuleM (Trace, [RawMatch]))
-> TacticError -> RuleM (Trace, [RawMatch])
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"destruct" CType
g
    Just (TyCon
tc, [Type]
apps) -> do
      let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
      case [DataCon]
dcs of
        [] -> TacticError -> RuleM (Trace, [RawMatch])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> RuleM (Trace, [RawMatch]))
-> TacticError -> RuleM (Trace, [RawMatch])
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"destruct" CType
g
        [DataCon]
_ -> ([(Trace, RawMatch)] -> (Trace, [RawMatch]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, RawMatch)]
-> RuleM (Trace, [RawMatch])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Trace, RawMatch)] -> (Trace, [RawMatch])
forall a. [(Trace, a)] -> (Trace, [a])
unzipTrace (RuleT
   Judgement
   (Trace, LHsExpr GhcPs)
   TacticError
   TacticState
   ExtractM
   [(Trace, RawMatch)]
 -> RuleM (Trace, [RawMatch]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, RawMatch)]
-> RuleM (Trace, [RawMatch])
forall a b. (a -> b) -> a -> b
$ [DataCon]
-> (DataCon
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, RawMatch))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, RawMatch)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataCon]
dcs ((DataCon
  -> RuleT
       Judgement
       (Trace, LHsExpr GhcPs)
       TacticError
       TacticState
       ExtractM
       (Trace, RawMatch))
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      [(Trace, RawMatch)])
-> (DataCon
    -> RuleT
         Judgement
         (Trace, LHsExpr GhcPs)
         TacticError
         TacticState
         ExtractM
         (Trace, RawMatch))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, RawMatch)]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> do
          let args :: [Type]
args = DataCon -> [Type] -> [Type]
dataConInstOrigArgTys' DataCon
dc [Type]
apps
          [OccName]
names <- Set OccName
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [OccName]
forall (t :: * -> *) (m :: * -> *).
(Traversable t, Monad m) =>
Set OccName -> t Type -> m (t OccName)
mkManyGoodNames (Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope Hypothesis CType
hy) [Type]
args
          let hy' :: [(OccName, CType)]
hy' = [OccName] -> [CType] -> [(OccName, CType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [OccName]
names ([CType] -> [(OccName, CType)]) -> [CType] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ [Type] -> [CType]
coerce [Type]
args
              j :: Judgement
j = Maybe OccName
-> DataCon -> [(OccName, CType)] -> Judgement -> Judgement
forall a.
Maybe OccName
-> DataCon -> [(OccName, a)] -> Judgement' a -> Judgement' a
introducingPat Maybe OccName
scrut DataCon
dc [(OccName, CType)]
hy'
                (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal CType
g Judgement
jdg
          (Trace
tr, LHsExpr GhcPs
sg) <- DataCon -> Judgement -> Rule
f DataCon
dc Judgement
j
          (TacticState -> TacticState)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState)
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      ())
-> (TacticState -> TacticState)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall a b. (a -> b) -> a -> b
$ (Set OccName -> Set OccName) -> TacticState -> TacticState
withIntroducedVals ((Set OccName -> Set OccName) -> TacticState -> TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall a b. (a -> b) -> a -> b
$ Set OccName -> Set OccName -> Set OccName
forall a. Monoid a => a -> a -> a
mappend (Set OccName -> Set OccName -> Set OccName)
-> Set OccName -> Set OccName -> Set OccName
forall a b. (a -> b) -> a -> b
$ [OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList [OccName]
names
          (Trace, RawMatch)
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, RawMatch)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (String
"match " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> DataCon -> String
forall a. Show a => a -> String
show DataCon
dc String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" {" String -> String -> String
forall a. Semigroup a => a -> a -> a
<>
                          String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((OccName -> String) -> [OccName] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> String
forall a. Show a => a -> String
show [OccName]
names) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"}")
                    ([Trace] -> Trace) -> [Trace] -> Trace
forall a b. (a -> b) -> a -> b
$ Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
tr
               , [Pat'] -> HsExpr' -> RawMatch
match [DataCon -> [OccName] -> Pat'
mkDestructPat DataCon
dc [OccName]
names] (HsExpr' -> RawMatch) -> HsExpr' -> RawMatch
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
sg
               )


------------------------------------------------------------------------------
-- | Produces a pattern for a data con and the names of its fields.
mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs
mkDestructPat :: DataCon -> [OccName] -> Pat'
mkDestructPat DataCon
dcon [OccName]
names
  | DataCon -> Bool
isTupleDataCon DataCon
dcon =
      [Pat'] -> Pat'
forall e. HasTuple e => [e] -> e
tuple [Pat']
pat_args
  | Bool
otherwise =
      DataCon -> Pat' -> Pat'
infixifyPatIfNecessary DataCon
dcon (Pat' -> Pat') -> Pat' -> Pat'
forall a b. (a -> b) -> a -> b
$
        RdrNameStr -> [Pat'] -> Pat'
conP
          (Name -> RdrNameStr
forall a. HasOccName a => a -> RdrNameStr
coerceName (Name -> RdrNameStr) -> Name -> RdrNameStr
forall a b. (a -> b) -> a -> b
$ DataCon -> Name
dataConName DataCon
dcon)
          [Pat']
pat_args
  where
    pat_args :: [Pat']
pat_args = (OccName -> Pat') -> [OccName] -> [Pat']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> Pat'
forall a. BVar a => OccName -> a
bvar' [OccName]
names


infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary :: DataCon -> Pat' -> Pat'
infixifyPatIfNecessary DataCon
dcon Pat'
x
  | DataCon -> Bool
dataConIsInfix DataCon
dcon =
      case Pat'
x of
        ConPatIn Located (IdP GhcPs)
op (PrefixCon [LPat GhcPs
lhs, LPat GhcPs
rhs]) ->
          Located (IdP GhcPs)
-> HsConDetails (LPat GhcPs) (HsRecFields GhcPs (LPat GhcPs))
-> Pat'
forall p. Located (IdP p) -> HsConPatDetails p -> Pat p
ConPatIn Located (IdP GhcPs)
op (HsConDetails (LPat GhcPs) (HsRecFields GhcPs (LPat GhcPs))
 -> Pat')
-> HsConDetails (LPat GhcPs) (HsRecFields GhcPs (LPat GhcPs))
-> Pat'
forall a b. (a -> b) -> a -> b
$ Located Pat'
-> Located Pat'
-> HsConDetails (Located Pat') (HsRecFields GhcPs (Located Pat'))
forall arg rec. arg -> arg -> HsConDetails arg rec
InfixCon LPat GhcPs
Located Pat'
lhs LPat GhcPs
Located Pat'
rhs
        Pat'
y -> Pat'
y
  | Bool
otherwise = Pat'
x



unzipTrace :: [(Trace, a)] -> (Trace, [a])
unzipTrace :: [(Trace, a)] -> (Trace, [a])
unzipTrace [(Trace, a)]
l =
  let ([Trace]
trs, [a]
as) = [(Trace, a)] -> ([Trace], [a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Trace, a)]
l
   in (String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose String
forall a. Monoid a => a
mempty [Trace]
trs, [a]
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' :: DataCon -> [Type] -> [Type]
dataConInstOrigArgTys' DataCon
con [Type]
uniTys =
  let exvars :: [TyCoVar]
exvars = DataCon -> [TyCoVar]
dataConExTys DataCon
con
   in DataCon -> [Type] -> [Type]
dataConInstOrigArgTys DataCon
con ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
        [Type]
uniTys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (TyCoVar -> Type) -> [TyCoVar] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCoVar -> Type
mkTyVarTy [TyCoVar]
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) -> HyInfo CType -> Judgement -> Rule
destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destruct' DataCon -> Judgement -> Rule
f HyInfo CType
hi Judgement
jdg = do
  Bool
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Judgement -> Bool
isDestructBlacklisted Judgement
jdg) (RuleT
   Judgement
   (Trace, LHsExpr GhcPs)
   TacticError
   TacticState
   ExtractM
   ()
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      ())
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall a b. (a -> b) -> a -> b
$ TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TacticError
NoApplicableTactic
  let term :: OccName
term = HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
  Judgement
-> OccName
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall (m :: * -> *).
MonadState TacticState m =>
Judgement -> OccName -> m ()
useOccName Judgement
jdg OccName
term
  (Trace
tr, [RawMatch]
ms)
      <- (DataCon -> Judgement -> Rule)
-> Maybe OccName -> CType -> Judgement -> RuleM (Trace, [RawMatch])
destructMatches
           DataCon -> Judgement -> Rule
f
           (OccName -> Maybe OccName
forall a. a -> Maybe a
Just OccName
term)
           (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi)
           (Judgement -> RuleM (Trace, [RawMatch]))
-> Judgement -> RuleM (Trace, [RawMatch])
forall a b. (a -> b) -> a -> b
$ DisallowReason -> [OccName] -> Judgement -> Judgement
forall a.
DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing DisallowReason
AlreadyDestructed [OccName
term] Judgement
jdg
  (Trace, LHsExpr GhcPs) -> Rule
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (String
"destruct " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
term) ([Trace] -> Trace) -> [Trace] -> Trace
forall a b. (a -> b) -> a -> b
$ Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
tr
       , SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs)
-> SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ HsExpr' -> [RawMatch] -> HsExpr'
case' (OccName -> HsExpr'
forall a. Var a => OccName -> a
var' OccName
term) [RawMatch]
ms
       )


------------------------------------------------------------------------------
-- | Combinator for performign case splitting, and running sub-rules on the
-- resulting matches.
destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' DataCon -> Judgement -> Rule
f Judgement
jdg = do
  Bool
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Judgement -> Bool
isDestructBlacklisted Judgement
jdg) (RuleT
   Judgement
   (Trace, LHsExpr GhcPs)
   TacticError
   TacticState
   ExtractM
   ()
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      ())
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall a b. (a -> b) -> a -> b
$ TacticError
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TacticError
NoApplicableTactic
  let g :: CType
g  = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
  case Type -> Maybe (Type, Type)
splitFunTy_maybe (CType -> Type
unCType CType
g) of
    Just (Type
arg, Type
_) | Type -> Bool
isAlgType Type
arg ->
      ([RawMatch] -> LHsExpr GhcPs)
-> (Trace, [RawMatch]) -> (Trace, LHsExpr GhcPs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((HsExpr' -> LHsExpr GhcPs)
-> ([RawMatch] -> HsExpr') -> [RawMatch] -> LHsExpr GhcPs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HsExpr' -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc [RawMatch] -> HsExpr'
lambdaCase) ((Trace, [RawMatch]) -> (Trace, LHsExpr GhcPs))
-> RuleM (Trace, [RawMatch]) -> Rule
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (DataCon -> Judgement -> Rule)
-> Maybe OccName -> CType -> Judgement -> RuleM (Trace, [RawMatch])
destructMatches DataCon -> Judgement -> Rule
f Maybe OccName
forall a. Maybe a
Nothing (Type -> CType
CType Type
arg) Judgement
jdg
    Maybe (Type, Type)
_ -> TacticError -> Rule
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> Rule) -> TacticError -> Rule
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"destructLambdaCase'" CType
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 :: Judgement -> DataCon -> [Type] -> Rule
buildDataCon Judgement
jdg DataCon
dc [Type]
tyapps = do
  let args :: [Type]
args = DataCon -> [Type] -> [Type]
dataConInstOrigArgTys' DataCon
dc [Type]
tyapps
  (Trace
tr, [LHsExpr GhcPs]
sgs)
      <- ([(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Trace, LHsExpr GhcPs)] -> (Trace, [LHsExpr GhcPs])
forall a. [(Trace, a)] -> (Trace, [a])
unzipTrace
       (RuleT
   Judgement
   (Trace, LHsExpr GhcPs)
   TacticError
   TacticState
   ExtractM
   [(Trace, LHsExpr GhcPs)]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      (Trace, [LHsExpr GhcPs]))
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     (Trace, [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ ((Type, Int) -> Rule)
-> [(Type, Int)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ( \(Type
arg, Int
n) ->
                    Judgement -> Rule
newSubgoal
                  (Judgement -> Rule) -> (CType -> Judgement) -> CType -> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions DataCon
dc Int
n
                  (Judgement -> Judgement)
-> (CType -> Judgement) -> CType -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Judgement
blacklistingDestruct
                  (Judgement -> Judgement)
-> (CType -> Judgement) -> CType -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CType -> Judgement -> Judgement)
-> Judgement -> CType -> Judgement
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal Judgement
jdg
                  (CType -> Rule) -> CType -> Rule
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
arg
                  ) ([(Type, Int)]
 -> RuleT
      Judgement
      (Trace, LHsExpr GhcPs)
      TacticError
      TacticState
      ExtractM
      [(Trace, LHsExpr GhcPs)])
-> [(Type, Int)]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [(Trace, LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ [Type] -> [Int] -> [(Type, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
args [Int
0..]
  (Trace, LHsExpr GhcPs) -> Rule
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ((Trace, LHsExpr GhcPs) -> Rule)
-> (LHsExpr GhcPs -> (Trace, LHsExpr GhcPs))
-> LHsExpr GhcPs
-> Rule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [Trace] -> Trace
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (DataCon -> String
forall a. Show a => a -> String
show DataCon
dc) ([Trace] -> Trace) -> [Trace] -> Trace
forall a b. (a -> b) -> a -> b
$ Trace -> [Trace]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Trace
tr,)
    (LHsExpr GhcPs -> Rule) -> LHsExpr GhcPs -> Rule
forall a b. (a -> b) -> a -> b
$ DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
mkCon DataCon
dc [LHsExpr GhcPs]
sgs