{-# 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 :: 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
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 <- Map OccName (HyInfo CType)
-> [Type]
-> RuleT
     Judgement
     (Trace, LHsExpr GhcPs)
     TacticError
     TacticState
     ExtractM
     [OccName]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
Map OccName a -> t Type -> m (t OccName)
mkManyGoodNames Map OccName (HyInfo 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) -> OccName -> Judgement -> Rule
destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
destruct' DataCon -> Judgement -> Rule
f OccName
term 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 hy :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg
  case OccName -> Map OccName (HyInfo CType) -> Maybe (HyInfo CType)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
term Map OccName (HyInfo CType)
hy of
    Maybe (HyInfo CType)
Nothing -> TacticError -> Rule
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> Rule) -> TacticError -> Rule
forall a b. (a -> b) -> a -> b
$ OccName -> TacticError
UndefinedHypothesis OccName
term
    Just (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type -> CType
t) -> do
      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)
               CType
t
               (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') -> [RawMatch] -> LHsExpr GhcPs)
-> ([RawMatch] -> HsExpr') -> [RawMatch] -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ [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]
apps = do
  let args :: [Type]
args = DataCon -> [Type] -> [Type]
dataConInstOrigArgTys' DataCon
dc [Type]
apps
  (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


mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs
mkCon DataCon
dcon ((LHsExpr GhcPs -> HsExpr') -> [LHsExpr GhcPs] -> [HsExpr']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHsExpr GhcPs -> HsExpr'
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc -> [HsExpr']
args)
  | DataCon -> Bool
isTupleDataCon DataCon
dcon =
      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'] -> HsExpr'
forall e. HasTuple e => [e] -> e
tuple [HsExpr']
args
  | DataCon -> Bool
dataConIsInfix DataCon
dcon
  , (HsExpr'
lhs : HsExpr'
rhs : [HsExpr']
args') <- [HsExpr']
args =
      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' -> HsExpr' -> HsExpr') -> HsExpr' -> [HsExpr'] -> HsExpr'
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsExpr' -> HsExpr' -> HsExpr'
forall e. App e => e -> e -> e
(@@) (HsExpr' -> RdrNameStr -> HsExpr' -> HsExpr'
forall e. App e => e -> RdrNameStr -> e -> e
op HsExpr'
lhs (Name -> RdrNameStr
forall a. HasOccName a => a -> RdrNameStr
coerceName Name
dcon_name) HsExpr'
rhs) [HsExpr']
args'
  | Bool
otherwise =
      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' -> HsExpr' -> HsExpr') -> HsExpr' -> [HsExpr'] -> HsExpr'
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HsExpr' -> HsExpr' -> HsExpr'
forall e. App e => e -> e -> e
(@@) (OccName -> HsExpr'
forall a. BVar a => OccName -> a
bvar' (OccName -> HsExpr') -> OccName -> HsExpr'
forall a b. (a -> b) -> a -> b
$ Name -> OccName
forall name. HasOccName name => name -> OccName
occName (Name -> OccName) -> Name -> OccName
forall a b. (a -> b) -> a -> b
$ Name
dcon_name) [HsExpr']
args
  where
    dcon_name :: Name
dcon_name = DataCon -> Name
dataConName DataCon
dcon



coerceName :: HasOccName a => a -> RdrNameStr
coerceName :: a -> RdrNameStr
coerceName = String -> RdrNameStr
forall a. IsString a => String -> a
fromString (String -> RdrNameStr) -> (a -> String) -> a -> RdrNameStr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString (OccName -> String) -> (a -> OccName) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> OccName
forall name. HasOccName name => name -> OccName
occName



------------------------------------------------------------------------------
-- | Like 'var', but works over standard GHC 'OccName's.
var' :: Var a => OccName -> a
var' :: OccName -> a
var' = RdrNameStr -> a
forall a. Var a => RdrNameStr -> a
var (RdrNameStr -> a) -> (OccName -> RdrNameStr) -> OccName -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> RdrNameStr
forall a. IsString a => String -> a
fromString (String -> RdrNameStr)
-> (OccName -> String) -> OccName -> RdrNameStr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString


------------------------------------------------------------------------------
-- | Like 'bvar', but works over standard GHC 'OccName's.
bvar' :: BVar a => OccName -> a
bvar' :: OccName -> a
bvar' = OccNameStr -> a
forall a. BVar a => OccNameStr -> a
bvar (OccNameStr -> a) -> (OccName -> OccNameStr) -> OccName -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccNameStr
forall a. IsString a => String -> a
fromString (String -> OccNameStr)
-> (OccName -> String) -> OccName -> OccNameStr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString


------------------------------------------------------------------------------
-- | Get an HsExpr corresponding to a function name.
mkFunc :: String -> HsExpr GhcPs
mkFunc :: String -> HsExpr'
mkFunc = OccName -> HsExpr'
forall a. Var a => OccName -> a
var' (OccName -> HsExpr') -> (String -> OccName) -> String -> HsExpr'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc


------------------------------------------------------------------------------
-- | Get an HsExpr corresponding to a value name.
mkVal :: String -> HsExpr GhcPs
mkVal :: String -> HsExpr'
mkVal = OccName -> HsExpr'
forall a. Var a => OccName -> a
var' (OccName -> HsExpr') -> (String -> OccName) -> String -> HsExpr'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> OccName
mkVarOcc


------------------------------------------------------------------------------
-- | Like 'op', but easier to call.
infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
infixCall :: String -> HsExpr' -> HsExpr' -> HsExpr'
infixCall String
s = (HsExpr' -> RdrNameStr -> HsExpr' -> HsExpr')
-> RdrNameStr -> HsExpr' -> HsExpr' -> HsExpr'
forall a b c. (a -> b -> c) -> b -> a -> c
flip HsExpr' -> RdrNameStr -> HsExpr' -> HsExpr'
forall e. App e => e -> RdrNameStr -> e -> e
op (String -> RdrNameStr
forall a. IsString a => String -> a
fromString String
s)


------------------------------------------------------------------------------
-- | Like '(@@)', but uses a dollar instead of parentheses.
appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
appDollar :: HsExpr' -> HsExpr' -> HsExpr'
appDollar = String -> HsExpr' -> HsExpr' -> HsExpr'
infixCall String
"$"