{-# 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 =
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 ()
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 :: 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
)
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) -> 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
)
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
buildDataCon
:: Judgement
-> DataCon
-> [Type]
-> 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
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
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
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
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
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)
appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
appDollar :: HsExpr' -> HsExpr' -> HsExpr'
appDollar = String -> HsExpr' -> HsExpr' -> HsExpr'
infixCall String
"$"