{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
module Wingman.CodeGen
( module Wingman.CodeGen
, module Wingman.CodeGen.Utils
) where
import ConLike
import Control.Lens ((%~), (<>~), (&))
import Control.Monad.Except
import Control.Monad.State
import Data.Bool (bool)
import Data.Generics.Labels ()
import Data.List
import Data.Monoid (Endo(..))
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 GhcPlugins (isSymOcc)
import PatSyn
import Type hiding (Var)
import Wingman.CodeGen.Utils
import Wingman.GHC
import Wingman.Judgements
import Wingman.Judgements.Theta
import Wingman.Machinery
import Wingman.Naming
import Wingman.Types
destructMatches
:: (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches :: (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches ConLike -> 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 (Synthesized [RawMatch])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> RuleM (Synthesized [RawMatch]))
-> TacticError -> RuleM (Synthesized [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 (Synthesized [RawMatch])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TacticError -> RuleM (Synthesized [RawMatch]))
-> TacticError -> RuleM (Synthesized [RawMatch])
forall a b. (a -> b) -> a -> b
$ String -> CType -> TacticError
GoalMismatch String
"destruct" CType
g
[DataCon]
_ -> ([Synthesized RawMatch] -> Synthesized [RawMatch])
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch]
-> RuleM (Synthesized [RawMatch])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized RawMatch] -> Synthesized [RawMatch]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace (RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch]
-> RuleM (Synthesized [RawMatch]))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch]
-> RuleM (Synthesized [RawMatch])
forall a b. (a -> b) -> a -> b
$ [DataCon]
-> (DataCon
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataCon]
dcs ((DataCon
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch])
-> (DataCon
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized RawMatch]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> do
let con :: ConLike
con = DataCon -> ConLike
RealDataCon DataCon
dc
ev :: [Evidence]
ev = (Type -> [Evidence]) -> [Type] -> [Evidence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Evidence]
mkEvidence ([Type] -> [Evidence]) -> [Type] -> [Evidence]
forall a b. (a -> b) -> a -> b
$ DataCon -> [Type] -> [Type]
dataConInstArgTys DataCon
dc [Type]
apps
method_hy :: Hypothesis CType
method_hy = (Evidence -> Hypothesis CType) -> [Evidence] -> Hypothesis CType
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Evidence -> Hypothesis CType
evidenceToHypothesis [Evidence]
ev
args :: [Type]
args = ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys' ConLike
con [Type]
apps
(TacticState -> TacticState)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TacticState -> TacticState)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
())
-> (TacticState -> TacticState)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall a b. (a -> b) -> a -> b
$ Endo TacticState -> TacticState -> TacticState
forall a. Endo a -> a -> a
appEndo (Endo TacticState -> TacticState -> TacticState)
-> Endo TacticState -> TacticState -> TacticState
forall a b. (a -> b) -> a -> b
$ (Evidence -> Endo TacticState) -> [Evidence] -> Endo TacticState
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((TacticState -> TacticState) -> Endo TacticState
forall a. (a -> a) -> Endo a
Endo ((TacticState -> TacticState) -> Endo TacticState)
-> (Evidence -> TacticState -> TacticState)
-> Evidence
-> Endo TacticState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Evidence -> TacticState -> TacticState
evidenceToSubst) [Evidence]
ev
TCvSubst
subst <- (TacticState -> TCvSubst)
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
TCvSubst
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TacticState -> TCvSubst
ts_unifier
[OccName]
names <- Set OccName
-> [Type]
-> RuleT
Judgement
(Synthesized (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' :: Hypothesis CType
hy' = Maybe OccName
-> ConLike -> Judgement -> [(OccName, CType)] -> Hypothesis CType
forall a.
Maybe OccName
-> ConLike -> Judgement' a -> [(OccName, a)] -> Hypothesis a
patternHypothesis Maybe OccName
scrut ConLike
con Judgement
jdg
([(OccName, CType)] -> Hypothesis CType)
-> [(OccName, CType)] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ [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 = (CType -> CType) -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> CType
CType (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCvSubst -> Type -> Type
substTyAddInScope TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType)
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Judgement -> Judgement
forall a. Hypothesis a -> Judgement' a -> Judgement' a
introduce Hypothesis CType
hy'
(Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Judgement -> Judgement
forall a. Hypothesis a -> Judgement' a -> Judgement' a
introduce Hypothesis CType
method_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
Synthesized (LHsExpr GhcPs)
ext <- ConLike -> Judgement -> Rule
f ConLike
con Judgement
j
Synthesized RawMatch
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized RawMatch
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch))
-> Synthesized RawMatch
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized RawMatch)
forall a b. (a -> b) -> a -> b
$ Synthesized (LHsExpr GhcPs)
ext
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_trace"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Rose String)
(Rose String))
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Rose String)
(Rose String)
#syn_trace ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Rose String)
(Rose String)
-> (Rose String -> Rose String)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ String -> [Rose String] -> Rose String
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
"}")
([Rose String] -> Rose String)
-> (Rose String -> [Rose String]) -> Rose String -> Rose String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rose String -> [Rose String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_scoped"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType))
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType)
#syn_scoped ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized (LHsExpr GhcPs))
(Hypothesis CType)
(Hypothesis CType)
-> Hypothesis CType
-> Synthesized (LHsExpr GhcPs)
-> Synthesized (LHsExpr GhcPs)
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ Hypothesis CType
hy'
Synthesized (LHsExpr GhcPs)
-> (Synthesized (LHsExpr GhcPs) -> Synthesized RawMatch)
-> Synthesized RawMatch
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_val"
(ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized RawMatch)
(LHsExpr GhcPs)
RawMatch)
ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized RawMatch)
(LHsExpr GhcPs)
RawMatch
#syn_val ASetter
(Synthesized (LHsExpr GhcPs))
(Synthesized RawMatch)
(LHsExpr GhcPs)
RawMatch
-> (LHsExpr GhcPs -> RawMatch)
-> Synthesized (LHsExpr GhcPs)
-> Synthesized RawMatch
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ [Pat'] -> HsExpr' -> RawMatch
match [ConLike -> [OccName] -> Pat'
mkDestructPat ConLike
con [OccName]
names] (HsExpr' -> RawMatch)
-> (LHsExpr GhcPs -> HsExpr') -> LHsExpr GhcPs -> RawMatch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsExpr GhcPs -> HsExpr'
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs
mkDestructPat :: ConLike -> [OccName] -> Pat'
mkDestructPat ConLike
con [OccName]
names
| RealDataCon DataCon
dcon <- ConLike
con
, DataCon -> Bool
isTupleDataCon DataCon
dcon =
[Pat'] -> Pat'
forall e. HasTuple e => [e] -> e
tuple [Pat']
pat_args
| Bool
otherwise =
ConLike -> Pat' -> Pat'
infixifyPatIfNecessary ConLike
con (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
$ ConLike -> Name
conLikeName ConLike
con)
[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 :: ConLike -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary :: ConLike -> Pat' -> Pat'
infixifyPatIfNecessary ConLike
dcon Pat'
x
| ConLike -> Bool
conLikeIsInfix ConLike
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 :: [Synthesized a] -> Synthesized [a]
unzipTrace :: [Synthesized a] -> Synthesized [a]
unzipTrace = [Synthesized a] -> Synthesized [a]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA
conLikeInstOrigArgTys'
:: ConLike
-> [Type]
-> [Type]
conLikeInstOrigArgTys' :: ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys' ConLike
con [Type]
uniTys =
let exvars :: [TyCoVar]
exvars = ConLike -> [TyCoVar]
conLikeExTys ConLike
con
in ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys ConLike
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
conLikeExTys :: ConLike -> [TyCoVar]
conLikeExTys :: ConLike -> [TyCoVar]
conLikeExTys (RealDataCon DataCon
d) = DataCon -> [TyCoVar]
dataConExTys DataCon
d
conLikeExTys (PatSynCon PatSyn
p) = PatSyn -> [TyCoVar]
patSynExTys PatSyn
p
patSynExTys :: PatSyn -> [TyCoVar]
patSynExTys :: PatSyn -> [TyCoVar]
patSynExTys PatSyn
ps = PatSyn -> [TyCoVar]
patSynExTyVars PatSyn
ps
destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destruct' ConLike -> Judgement -> Rule
f HyInfo CType
hi Judgement
jdg = do
Bool
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Judgement -> Bool
isDestructBlacklisted Judgement
jdg) (RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
())
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall a b. (a -> b) -> a -> b
$ TacticError
-> RuleT
Judgement
(Synthesized (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
Synthesized [RawMatch]
ext
<- (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches
ConLike -> 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 (Synthesized [RawMatch]))
-> Judgement -> RuleM (Synthesized [RawMatch])
forall a b. (a -> b) -> a -> b
$ DisallowReason -> Set OccName -> Judgement -> Judgement
forall a.
DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
AlreadyDestructed (OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
term) Judgement
jdg
Synthesized (LHsExpr GhcPs) -> Rule
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs) -> Rule)
-> Synthesized (LHsExpr GhcPs) -> Rule
forall a b. (a -> b) -> a -> b
$ Synthesized [RawMatch]
ext
Synthesized [RawMatch]
-> (Synthesized [RawMatch] -> Synthesized [RawMatch])
-> Synthesized [RawMatch]
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_trace"
(ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Rose String)
(Rose String))
ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Rose String)
(Rose String)
#syn_trace ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Rose String)
(Rose String)
-> (Rose String -> Rose String)
-> Synthesized [RawMatch]
-> Synthesized [RawMatch]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ String -> [Rose String] -> Rose String
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) ([Rose String] -> Rose String)
-> (Rose String -> [Rose String]) -> Rose String -> Rose String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rose String -> [Rose String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Synthesized [RawMatch]
-> (Synthesized [RawMatch] -> Synthesized [RawMatch])
-> Synthesized [RawMatch]
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_used_vals"
(ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Set OccName)
(Set OccName))
ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Set OccName)
(Set OccName)
#syn_used_vals ASetter
(Synthesized [RawMatch])
(Synthesized [RawMatch])
(Set OccName)
(Set OccName)
-> (Set OccName -> Set OccName)
-> Synthesized [RawMatch]
-> Synthesized [RawMatch]
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.insert OccName
term
Synthesized [RawMatch]
-> (Synthesized [RawMatch] -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_val"
(ASetter
(Synthesized [RawMatch])
(Synthesized (LHsExpr GhcPs))
[RawMatch]
(LHsExpr GhcPs))
ASetter
(Synthesized [RawMatch])
(Synthesized (LHsExpr GhcPs))
[RawMatch]
(LHsExpr GhcPs)
#syn_val ASetter
(Synthesized [RawMatch])
(Synthesized (LHsExpr GhcPs))
[RawMatch]
(LHsExpr GhcPs)
-> ([RawMatch] -> LHsExpr GhcPs)
-> Synthesized [RawMatch]
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HsExpr' -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (HsExpr' -> LHsExpr GhcPs)
-> ([RawMatch] -> HsExpr') -> [RawMatch] -> LHsExpr GhcPs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr' -> [RawMatch] -> HsExpr'
case' (OccName -> HsExpr'
forall a. Var a => OccName -> a
var' OccName
term)
destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' ConLike -> Judgement -> Rule
f Judgement
jdg = do
Bool
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Judgement -> Bool
isDestructBlacklisted Judgement
jdg) (RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
())
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
()
forall a b. (a -> b) -> a -> b
$ TacticError
-> RuleT
Judgement
(Synthesized (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)
-> Synthesized [RawMatch] -> Synthesized (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) (Synthesized [RawMatch] -> Synthesized (LHsExpr GhcPs))
-> RuleM (Synthesized [RawMatch]) -> Rule
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches ConLike -> 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
:: Bool
-> Judgement
-> ConLike
-> [Type]
-> RuleM (Synthesized (LHsExpr GhcPs))
buildDataCon :: Bool -> Judgement -> ConLike -> [Type] -> Rule
buildDataCon Bool
should_blacklist Judgement
jdg ConLike
dc [Type]
tyapps = do
let args :: [Type]
args = ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys' ConLike
dc [Type]
tyapps
Synthesized [LHsExpr GhcPs]
ext
<- ([Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs])
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (LHsExpr GhcPs)] -> Synthesized [LHsExpr GhcPs]
forall a. [Synthesized a] -> Synthesized [a]
unzipTrace
(RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs]))
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
(Synthesized [LHsExpr GhcPs])
forall a b. (a -> b) -> a -> b
$ ((Type, Int) -> Rule)
-> [(Type, Int)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (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
. ConLike -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions ConLike
dc Int
n
(Judgement -> Judgement)
-> (CType -> Judgement) -> CType -> Judgement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Judgement -> Judgement)
-> (Judgement -> Judgement) -> Bool -> Judgement -> Judgement
forall a. a -> a -> Bool -> a
bool Judgement -> Judgement
forall a. a -> a
id Judgement -> Judgement
blacklistingDestruct Bool
should_blacklist
(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
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (LHsExpr GhcPs)])
-> [(Type, Int)]
-> RuleT
Judgement
(Synthesized (LHsExpr GhcPs))
TacticError
TacticState
ExtractM
[Synthesized (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..]
Synthesized (LHsExpr GhcPs) -> Rule
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs) -> Rule)
-> Synthesized (LHsExpr GhcPs) -> Rule
forall a b. (a -> b) -> a -> b
$ Synthesized [LHsExpr GhcPs]
ext
Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized [LHsExpr GhcPs])
-> Synthesized [LHsExpr GhcPs]
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_trace"
(ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Rose String)
(Rose String))
ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Rose String)
(Rose String)
#syn_trace ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized [LHsExpr GhcPs])
(Rose String)
(Rose String)
-> (Rose String -> Rose String)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized [LHsExpr GhcPs]
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ String -> [Rose String] -> Rose String
forall a. (Eq a, Monoid a) => a -> [Rose a] -> Rose a
rose (ConLike -> String
forall a. Show a => a -> String
show ConLike
dc) ([Rose String] -> Rose String)
-> (Rose String -> [Rose String]) -> Rose String -> Rose String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rose String -> [Rose String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Synthesized [LHsExpr GhcPs]
-> (Synthesized [LHsExpr GhcPs] -> Synthesized (LHsExpr GhcPs))
-> Synthesized (LHsExpr GhcPs)
forall a b. a -> (a -> b) -> b
& IsLabel
"syn_val"
(ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs))
ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs)
#syn_val ASetter
(Synthesized [LHsExpr GhcPs])
(Synthesized (LHsExpr GhcPs))
[LHsExpr GhcPs]
(LHsExpr GhcPs)
-> ([LHsExpr GhcPs] -> LHsExpr GhcPs)
-> Synthesized [LHsExpr GhcPs]
-> Synthesized (LHsExpr GhcPs)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ConLike -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs
mkCon ConLike
dc [Type]
tyapps
mkApply :: OccName -> [HsExpr GhcPs] -> LHsExpr GhcPs
mkApply :: OccName -> [HsExpr'] -> LHsExpr GhcPs
mkApply OccName
occ (HsExpr'
lhs : HsExpr'
rhs : [HsExpr']
more)
| OccName -> Bool
isSymOcc OccName
occ
= 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 (OccName -> RdrNameStr
forall a. HasOccName a => a -> RdrNameStr
coerceName OccName
occ) HsExpr'
rhs) [HsExpr']
more
mkApply OccName
occ [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
(@@) (OccName -> HsExpr'
forall a. Var a => OccName -> a
var' OccName
occ) [HsExpr']
args