{-# 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 =
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 ()
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
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)
-> Maybe OccName
-> CType
-> 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
)
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)
dataConInstOrigArgTys'
:: DataCon
-> [Type]
-> [Type]
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
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
)
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
buildDataCon
:: Judgement
-> DataCon
-> [Type]
-> 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