{-# 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)
       -- ^ How to construct each match
    -> Maybe OccName
       -- ^ Scrutinee
    -> CType
       -- ^ Type being destructed
    -> 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
              -- We explicitly do not need to add the method hypothesis to
              -- #syn_scoped
              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


------------------------------------------------------------------------------
-- | Produces a pattern for a data con and the names of its fields.
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


-- | 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.
conLikeInstOrigArgTys'
  :: ConLike
      -- ^ '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 ConLike with returned type is instantiated with the second argument.
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
      -- 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.


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


------------------------------------------------------------------------------
-- | Combinator for performing case splitting, and running sub-rules on the
-- resulting matches.

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)


------------------------------------------------------------------------------
-- | Combinator for performign case splitting, and running sub-rules on the
-- resulting matches.
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


------------------------------------------------------------------------------
-- | Construct a data con with subgoals for each field.
buildDataCon
    :: Bool       -- Should we blacklist destruct?
    -> Judgement
    -> ConLike            -- ^ The data con to build
    -> [Type]             -- ^ Type arguments for the data con
    -> 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


------------------------------------------------------------------------------
-- | Make a function application, correctly handling the infix case.
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