{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedLabels  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}

module Wingman.CodeGen
  ( module Wingman.CodeGen
  , module Wingman.CodeGen.Utils
  ) where


import           Control.Lens ((%~), (<>~), (&))
import           Control.Monad.Except
import           Control.Monad.Reader (ask)
import           Control.Monad.State
import           Data.Bifunctor (second)
import           Data.Bool (bool)
import           Data.Functor ((<&>))
import           Data.Generics.Labels ()
import           Data.List
import qualified Data.Set as S
import           Data.Traversable
import           Development.IDE.GHC.Compat
import           GHC.Exts
import           GHC.SourceGen (occNameToStr)
import           GHC.SourceGen.Binds
import           GHC.SourceGen.Expr
import           GHC.SourceGen.Overloaded
import           GHC.SourceGen.Pat
import           Wingman.CodeGen.Utils
import           Wingman.GHC
import           Wingman.Judgements
import           Wingman.Judgements.Theta
import           Wingman.Machinery
import           Wingman.Naming
import           Wingman.Types


destructMatches
    :: Bool
    -> (ConLike -> Judgement -> Rule)
       -- ^ How to construct each match
    -> Maybe OccName
       -- ^ Scrutinee
    -> CType
       -- ^ Type being destructed
    -> Judgement
    -> RuleM (Synthesized [RawMatch])
-- TODO(sandy): In an ideal world, this would be the same codepath as
-- 'destructionFor'. Make sure to change that if you ever change this.
destructMatches :: Bool
-> (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches Bool
use_field_puns 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 Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons (Type -> Maybe ([DataCon], [Type]))
-> Type -> Maybe ([DataCon], [Type])
forall a b. (a -> b) -> a -> b
$ CType -> Type
unCType CType
t of
    Maybe ([DataCon], [Type])
Nothing -> RuleM (Synthesized [RawMatch])
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- throwError $ GoalMismatch "destruct" g
    Just ([DataCon]
dcs, [Type]
apps) ->
      ([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 -> Type) -> Type -> [Evidence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. Scaled a -> Scaled a
scaledThing) ([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
        Context
ctx <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask

        let names_in_scope :: Set OccName
names_in_scope = Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope Hypothesis CType
hy
            names :: [OccName]
names = Set OccName -> [Type] -> [OccName]
forall (t :: * -> *).
Traversable t =>
Set OccName -> t Type -> t OccName
mkManyGoodNames (Hypothesis CType -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope Hypothesis CType
hy) [Type]
args
            ([OccName]
names', Pat GhcPs
destructed) =
              Maybe (Set OccName)
-> ConLike -> [OccName] -> ([OccName], Pat GhcPs)
mkDestructPat (Maybe (Set OccName)
-> Maybe (Set OccName) -> Bool -> Maybe (Set OccName)
forall a. a -> a -> Bool -> a
bool Maybe (Set OccName)
forall a. Maybe a
Nothing (Set OccName -> Maybe (Set OccName)
forall a. a -> Maybe a
Just Set OccName
names_in_scope) Bool
use_field_puns) ConLike
con [OccName]
names

        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
withNewCoercions ([Evidence] -> [(CType, CType)]
evidenceToCoercions [Evidence]
ev)
              (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy'
              (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx 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 GhcPs] -> HsExpr' -> RawMatch
match [Pat GhcPs
destructed] (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


------------------------------------------------------------------------------
-- | Generate just the 'Match'es for a case split on a specific type.
destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
-- TODO(sandy): In an ideal world, this would be the same codepath as
-- 'destructMatches'. Make sure to change that if you ever change this.
destructionFor :: Hypothesis a -> Type -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
destructionFor Hypothesis a
hy Type
t = do
  case Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons Type
t of
    Maybe ([DataCon], [Type])
Nothing -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
forall a. Maybe a
Nothing
    Just ([], [Type]
_) -> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
forall a. Maybe a
Nothing
    Just ([DataCon]
dcs, [Type]
apps) -> do
      [DataCon]
-> (DataCon -> Maybe (LMatch GhcPs (LHsExpr GhcPs)))
-> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [DataCon]
dcs ((DataCon -> Maybe (LMatch GhcPs (LHsExpr GhcPs)))
 -> Maybe [LMatch GhcPs (LHsExpr GhcPs)])
-> (DataCon -> Maybe (LMatch GhcPs (LHsExpr GhcPs)))
-> Maybe [LMatch GhcPs (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ \DataCon
dc -> do
        let con :: ConLike
con   = DataCon -> ConLike
RealDataCon DataCon
dc
            args :: [Type]
args  = ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys' ConLike
con [Type]
apps
            names :: [OccName]
names = Set OccName -> [Type] -> [OccName]
forall (t :: * -> *).
Traversable t =>
Set OccName -> t Type -> t OccName
mkManyGoodNames (Hypothesis a -> Set OccName
forall a. Hypothesis a -> Set OccName
hyNamesInScope Hypothesis a
hy) [Type]
args
        LMatch GhcPs (LHsExpr GhcPs)
-> Maybe (LMatch GhcPs (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          (LMatch GhcPs (LHsExpr GhcPs)
 -> Maybe (LMatch GhcPs (LHsExpr GhcPs)))
-> (HsLocalBindsLR GhcPs GhcPs -> LMatch GhcPs (LHsExpr GhcPs))
-> HsLocalBindsLR GhcPs GhcPs
-> Maybe (LMatch GhcPs (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Match GhcPs (LHsExpr GhcPs) -> LMatch GhcPs (LHsExpr GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
          (Match GhcPs (LHsExpr GhcPs) -> LMatch GhcPs (LHsExpr GhcPs))
-> (HsLocalBindsLR GhcPs GhcPs -> Match GhcPs (LHsExpr GhcPs))
-> HsLocalBindsLR GhcPs GhcPs
-> LMatch GhcPs (LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XCMatch GhcPs (LHsExpr GhcPs)
-> HsMatchContext (NameOrRdrName (IdP GhcPs))
-> [LPat GhcPs]
-> GRHSs GhcPs (LHsExpr GhcPs)
-> Match GhcPs (LHsExpr GhcPs)
forall p body.
XCMatch p body
-> HsMatchContext (NameOrRdrName (IdP p))
-> [LPat p]
-> GRHSs p body
-> Match p body
Match
              NoExtField
XCMatch GhcPs (LHsExpr GhcPs)
noExtField
              HsMatchContext (NameOrRdrName (IdP GhcPs))
forall id. HsMatchContext id
CaseAlt
              [Pat GhcPs -> LPat GhcPs
forall p. PatCompattable p => Pat p -> PatCompat p
toPatCompat (Pat GhcPs -> LPat GhcPs) -> Pat GhcPs -> LPat GhcPs
forall a b. (a -> b) -> a -> b
$ ([OccName], Pat GhcPs) -> Pat GhcPs
forall a b. (a, b) -> b
snd (([OccName], Pat GhcPs) -> Pat GhcPs)
-> ([OccName], Pat GhcPs) -> Pat GhcPs
forall a b. (a -> b) -> a -> b
$ Maybe (Set OccName)
-> ConLike -> [OccName] -> ([OccName], Pat GhcPs)
mkDestructPat Maybe (Set OccName)
forall a. Maybe a
Nothing ConLike
con [OccName]
names]
          (GRHSs GhcPs (LHsExpr GhcPs) -> Match GhcPs (LHsExpr GhcPs))
-> (HsLocalBindsLR GhcPs GhcPs -> GRHSs GhcPs (LHsExpr GhcPs))
-> HsLocalBindsLR GhcPs GhcPs
-> Match GhcPs (LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XCGRHSs GhcPs (LHsExpr GhcPs)
-> [LGRHS GhcPs (LHsExpr GhcPs)]
-> LHsLocalBinds GhcPs
-> GRHSs GhcPs (LHsExpr GhcPs)
forall p body.
XCGRHSs p body -> [LGRHS p body] -> LHsLocalBinds p -> GRHSs p body
GRHSs NoExtField
XCGRHSs GhcPs (LHsExpr GhcPs)
noExtField (LGRHS GhcPs (LHsExpr GhcPs) -> [LGRHS GhcPs (LHsExpr GhcPs)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LGRHS GhcPs (LHsExpr GhcPs) -> [LGRHS GhcPs (LHsExpr GhcPs)])
-> LGRHS GhcPs (LHsExpr GhcPs) -> [LGRHS GhcPs (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (LGRHS GhcPs (LHsExpr GhcPs))
-> LGRHS GhcPs (LHsExpr GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LGRHS GhcPs (LHsExpr GhcPs))
 -> LGRHS GhcPs (LHsExpr GhcPs))
-> SrcSpanLess (LGRHS GhcPs (LHsExpr GhcPs))
-> LGRHS GhcPs (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ XCGRHS GhcPs (LHsExpr GhcPs)
-> [GuardLStmt GhcPs]
-> LHsExpr GhcPs
-> GRHS GhcPs (LHsExpr GhcPs)
forall p body.
XCGRHS p body -> [GuardLStmt p] -> body -> GRHS p body
GRHS NoExtField
XCGRHS GhcPs (LHsExpr GhcPs)
noExtField [] (LHsExpr GhcPs -> GRHS GhcPs (LHsExpr GhcPs))
-> LHsExpr GhcPs -> GRHS GhcPs (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ 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
$ RdrNameStr -> HsExpr'
forall a. Var a => RdrNameStr -> a
var RdrNameStr
"_")
          (LHsLocalBinds GhcPs -> GRHSs GhcPs (LHsExpr GhcPs))
-> (HsLocalBindsLR GhcPs GhcPs -> LHsLocalBinds GhcPs)
-> HsLocalBindsLR GhcPs GhcPs
-> GRHSs GhcPs (LHsExpr GhcPs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsLocalBindsLR GhcPs GhcPs -> LHsLocalBinds GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
          (HsLocalBindsLR GhcPs GhcPs
 -> Maybe (LMatch GhcPs (LHsExpr GhcPs)))
-> HsLocalBindsLR GhcPs GhcPs
-> Maybe (LMatch GhcPs (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ XEmptyLocalBinds GhcPs GhcPs -> HsLocalBindsLR GhcPs GhcPs
forall idL idR. XEmptyLocalBinds idL idR -> HsLocalBindsLR idL idR
EmptyLocalBinds NoExtField
XEmptyLocalBinds GhcPs GhcPs
noExtField



------------------------------------------------------------------------------
-- | Produces a pattern for a data con and the names of its fields.
mkDestructPat :: Maybe (S.Set OccName) -> ConLike -> [OccName] -> ([OccName], Pat GhcPs)
mkDestructPat :: Maybe (Set OccName)
-> ConLike -> [OccName] -> ([OccName], Pat GhcPs)
mkDestructPat Maybe (Set OccName)
already_in_scope ConLike
con [OccName]
names
  | RealDataCon DataCon
dcon <- ConLike
con
  , DataCon -> Bool
isTupleDataCon DataCon
dcon =
      ([OccName]
names, [Pat GhcPs] -> Pat GhcPs
forall e. HasTuple e => [e] -> e
tuple [Pat GhcPs]
pat_args)
  | fields :: [(FieldLabel, OccName)]
fields@((FieldLabel, OccName)
_:[(FieldLabel, OccName)]
_) <- [FieldLabel] -> [OccName] -> [(FieldLabel, OccName)]
forall a b. [a] -> [b] -> [(a, b)]
zip (ConLike -> [FieldLabel]
conLikeFieldLabels ConLike
con) [OccName]
names
  , Just Set OccName
in_scope <- Maybe (Set OccName)
already_in_scope =
      let ([OccName]
names', [LHsRecField GhcPs (Located (Pat GhcPs))]
rec_fields) =
            [(OccName, LHsRecField GhcPs (Located (Pat GhcPs)))]
-> ([OccName], [LHsRecField GhcPs (Located (Pat GhcPs))])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(OccName, LHsRecField GhcPs (Located (Pat GhcPs)))]
 -> ([OccName], [LHsRecField GhcPs (Located (Pat GhcPs))]))
-> [(OccName, LHsRecField GhcPs (Located (Pat GhcPs)))]
-> ([OccName], [LHsRecField GhcPs (Located (Pat GhcPs))])
forall a b. (a -> b) -> a -> b
$ [(FieldLabel, OccName)]
fields [(FieldLabel, OccName)]
-> ((FieldLabel, OccName)
    -> (OccName, LHsRecField GhcPs (Located (Pat GhcPs))))
-> [(OccName, LHsRecField GhcPs (Located (Pat GhcPs)))]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(FieldLabel
label, OccName
name) -> do
              let label_occ :: OccName
label_occ = FastString -> OccName
mkVarOccFS (FastString -> OccName) -> FastString -> OccName
forall a b. (a -> b) -> a -> b
$ FieldLabel -> FastString
forall a. FieldLbl a -> FastString
flLabel FieldLabel
label
              case OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member OccName
label_occ Set OccName
in_scope of
                -- We have a shadow, so use the generated name instead
                Bool
True ->
                  (OccName
name,) (LHsRecField GhcPs (Located (Pat GhcPs))
 -> (OccName, LHsRecField GhcPs (Located (Pat GhcPs))))
-> LHsRecField GhcPs (Located (Pat GhcPs))
-> (OccName, LHsRecField GhcPs (Located (Pat GhcPs)))
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
-> LHsRecField GhcPs (Located (Pat GhcPs))
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
 -> LHsRecField GhcPs (Located (Pat GhcPs)))
-> SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
-> LHsRecField GhcPs (Located (Pat GhcPs))
forall a b. (a -> b) -> a -> b
$
                    Located (FieldOcc GhcPs)
-> Located (Pat GhcPs)
-> Bool
-> HsRecField' (FieldOcc GhcPs) (Located (Pat GhcPs))
forall id arg. Located id -> arg -> Bool -> HsRecField' id arg
HsRecField
                      (SrcSpanLess (Located (FieldOcc GhcPs)) -> Located (FieldOcc GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located (FieldOcc GhcPs))
 -> Located (FieldOcc GhcPs))
-> SrcSpanLess (Located (FieldOcc GhcPs))
-> Located (FieldOcc GhcPs)
forall a b. (a -> b) -> a -> b
$ Located RdrName -> FieldOcc GhcPs
mkFieldOcc (Located RdrName -> FieldOcc GhcPs)
-> Located RdrName -> FieldOcc GhcPs
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (Located RdrName) -> Located RdrName
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located RdrName) -> Located RdrName)
-> SrcSpanLess (Located RdrName) -> Located RdrName
forall a b. (a -> b) -> a -> b
$ OccName -> RdrName
Unqual OccName
label_occ)
                      (SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs))
-> SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs)
forall a b. (a -> b) -> a -> b
$ OccName -> Pat GhcPs
forall a. BVar a => OccName -> a
bvar' OccName
name)
                      Bool
False
                -- No shadow, safe to use a pun
                Bool
False ->
                  (OccName
label_occ,) (LHsRecField GhcPs (Located (Pat GhcPs))
 -> (OccName, LHsRecField GhcPs (Located (Pat GhcPs))))
-> LHsRecField GhcPs (Located (Pat GhcPs))
-> (OccName, LHsRecField GhcPs (Located (Pat GhcPs)))
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
-> LHsRecField GhcPs (Located (Pat GhcPs))
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
 -> LHsRecField GhcPs (Located (Pat GhcPs)))
-> SrcSpanLess (LHsRecField GhcPs (Located (Pat GhcPs)))
-> LHsRecField GhcPs (Located (Pat GhcPs))
forall a b. (a -> b) -> a -> b
$
                    Located (FieldOcc GhcPs)
-> Located (Pat GhcPs)
-> Bool
-> HsRecField' (FieldOcc GhcPs) (Located (Pat GhcPs))
forall id arg. Located id -> arg -> Bool -> HsRecField' id arg
HsRecField
                      (SrcSpanLess (Located (FieldOcc GhcPs)) -> Located (FieldOcc GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located (FieldOcc GhcPs))
 -> Located (FieldOcc GhcPs))
-> SrcSpanLess (Located (FieldOcc GhcPs))
-> Located (FieldOcc GhcPs)
forall a b. (a -> b) -> a -> b
$ Located RdrName -> FieldOcc GhcPs
mkFieldOcc (Located RdrName -> FieldOcc GhcPs)
-> Located RdrName -> FieldOcc GhcPs
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (Located RdrName) -> Located RdrName
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located RdrName) -> Located RdrName)
-> SrcSpanLess (Located RdrName) -> Located RdrName
forall a b. (a -> b) -> a -> b
$ OccName -> RdrName
Unqual OccName
label_occ)
                      (SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs)
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs))
-> SrcSpanLess (Located (Pat GhcPs)) -> Located (Pat GhcPs)
forall a b. (a -> b) -> a -> b
$ OccName -> Pat GhcPs
forall a. BVar a => OccName -> a
bvar' OccName
label_occ)
                      Bool
True

        in ([OccName]
names', )
         (Pat GhcPs -> ([OccName], Pat GhcPs))
-> Pat GhcPs -> ([OccName], Pat GhcPs)
forall a b. (a -> b) -> a -> b
$ Located (IdP GhcPs) -> HsConPatDetails GhcPs -> Pat GhcPs
forall p. Located (IdP p) -> HsConPatDetails p -> Pat p
ConPatIn (SrcSpanLess (Located RdrName) -> Located RdrName
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located RdrName) -> Located RdrName)
-> SrcSpanLess (Located RdrName) -> Located RdrName
forall a b. (a -> b) -> a -> b
$ OccName -> RdrName
Unqual (OccName -> RdrName) -> OccName -> RdrName
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
$ ConLike -> Name
conLikeName ConLike
con)
         (HsConPatDetails GhcPs -> Pat GhcPs)
-> HsConPatDetails GhcPs -> Pat GhcPs
forall a b. (a -> b) -> a -> b
$ HsRecFields GhcPs (Located (Pat GhcPs))
-> HsConDetails
     (Located (Pat GhcPs)) (HsRecFields GhcPs (Located (Pat GhcPs)))
forall arg rec. rec -> HsConDetails arg rec
RecCon
         (HsRecFields GhcPs (Located (Pat GhcPs))
 -> HsConDetails
      (Located (Pat GhcPs)) (HsRecFields GhcPs (Located (Pat GhcPs))))
-> HsRecFields GhcPs (Located (Pat GhcPs))
-> HsConDetails
     (Located (Pat GhcPs)) (HsRecFields GhcPs (Located (Pat GhcPs)))
forall a b. (a -> b) -> a -> b
$ [LHsRecField GhcPs (Located (Pat GhcPs))]
-> Maybe (Located Int) -> HsRecFields GhcPs (Located (Pat GhcPs))
forall p arg.
[LHsRecField p arg] -> Maybe (Located Int) -> HsRecFields p arg
HsRecFields [LHsRecField GhcPs (Located (Pat GhcPs))]
rec_fields Maybe (Located Int)
forall a. Maybe a
Nothing
  | Bool
otherwise =
      ([OccName]
names, ) (Pat GhcPs -> ([OccName], Pat GhcPs))
-> Pat GhcPs -> ([OccName], Pat GhcPs)
forall a b. (a -> b) -> a -> b
$ ConLike -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary ConLike
con (Pat GhcPs -> Pat GhcPs) -> Pat GhcPs -> Pat GhcPs
forall a b. (a -> b) -> a -> b
$
        RdrNameStr -> [Pat GhcPs] -> Pat GhcPs
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 GhcPs]
pat_args
  where
    pat_args :: [Pat GhcPs]
pat_args = (OccName -> Pat GhcPs) -> [OccName] -> [Pat GhcPs]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OccName -> Pat GhcPs
forall a. BVar a => OccName -> a
bvar' [OccName]
names


infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs
infixifyPatIfNecessary ConLike
dcon Pat GhcPs
x
  | ConLike -> Bool
conLikeIsInfix ConLike
dcon =
      case Pat GhcPs
x of
        ConPatIn Located (IdP GhcPs)
op (PrefixCon [LPat GhcPs
lhs, LPat GhcPs
rhs]) ->
          Located (IdP GhcPs) -> HsConPatDetails GhcPs -> Pat GhcPs
forall p. Located (IdP p) -> HsConPatDetails p -> Pat p
ConPatIn Located (IdP GhcPs)
op (HsConPatDetails GhcPs -> Pat GhcPs)
-> HsConPatDetails GhcPs -> Pat GhcPs
forall a b. (a -> b) -> a -> b
$ Located (Pat GhcPs)
-> Located (Pat GhcPs)
-> HsConDetails
     (Located (Pat GhcPs)) (HsRecFields GhcPs (Located (Pat GhcPs)))
forall arg rec. arg -> arg -> HsConDetails arg rec
InfixCon LPat GhcPs
Located (Pat GhcPs)
lhs LPat GhcPs
Located (Pat GhcPs)
rhs
        Pat GhcPs
y -> Pat GhcPs
y
  | Bool
otherwise = Pat GhcPs
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 (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> Type
forall a. Scaled a -> Scaled a
scaledThing ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ 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]
dataConExTyCoVars 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' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
destruct' :: Bool
-> (ConLike -> Judgement -> Rule)
-> HyInfo CType
-> Judgement
-> Rule
destruct' Bool
use_field_puns 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
  ()
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- throwError NoApplicableTactic
  let term :: OccName
term = HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
  Synthesized [RawMatch]
ext
      <- Bool
-> (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches
           Bool
use_field_puns
           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 (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' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
destructLambdaCase' Bool
use_field_puns 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
  ()
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- throwError 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
#if __GLASGOW_HASKELL__ >= 900
    Just (_multiplicity, arg, _) | isAlgType arg ->
#else
    Just (Type
arg, Type
_) | Type -> Bool
isAlgType Type
arg ->
#endif
      ([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
<$>
        Bool
-> (ConLike -> Judgement -> Rule)
-> Maybe OccName
-> CType
-> Judgement
-> RuleM (Synthesized [RawMatch])
destructMatches Bool
use_field_puns ConLike -> Judgement -> Rule
f Maybe OccName
forall a. Maybe a
Nothing (Type -> CType
CType Type
arg) Judgement
jdg
    Maybe (Type, Type)
_ -> Rule
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- throwError $ GoalMismatch "destructLambdaCase'" 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
  [Type]
args <- case ConLike
dc of
    RealDataCon DataCon
dc' -> do
      let ([TyCoVar]
skolems', [Type]
theta, [Type]
args) = DataCon -> [Type] -> ([TyCoVar], [Type], [Type])
dataConInstSig DataCon
dc' [Type]
tyapps
      (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
$ \TacticState
ts ->
        [Evidence] -> TacticState -> TacticState
evidenceToSubst ((Type -> [Evidence]) -> [Type] -> [Evidence]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> [Evidence]
mkEvidence [Type]
theta) TacticState
ts
          TacticState -> (TacticState -> TacticState) -> TacticState
forall a b. a -> (a -> b) -> b
& IsLabel
  "ts_skolems"
  (ASetter TacticState TacticState (Set TyCoVar) (Set TyCoVar))
ASetter TacticState TacticState (Set TyCoVar) (Set TyCoVar)
#ts_skolems ASetter TacticState TacticState (Set TyCoVar) (Set TyCoVar)
-> Set TyCoVar -> TacticState -> TacticState
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ [TyCoVar] -> Set TyCoVar
forall a. Ord a => [a] -> Set a
S.fromList [TyCoVar]
skolems'
      [Type]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Type]
args
    ConLike
_ ->
      -- If we have a 'PatSyn', we can't continue, since there is no
      -- 'dataConInstSig' equivalent for 'PatSyn's. I don't think this is
      -- a fundamental problem, but I don't know enough about the GHC internals
      -- to implement it myself.
      --
      -- Fortunately, this isn't an issue in practice, since 'PatSyn's are
      -- never in the hypothesis.
      RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [Type]
forall jdg ext err s (m :: * -> *) a. RuleT jdg ext err s m a
cut -- throwError $ TacticPanic "Can't build Pattern constructors yet"
  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. Scaled a -> Scaled 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


------------------------------------------------------------------------------
-- | Run a tactic over each term in the given 'Hypothesis', binding the results
-- of each in a let expression.
letForEach
    :: (OccName -> OccName)           -- ^ How to name bound variables
    -> (HyInfo CType -> TacticsM ())  -- ^ The tactic to run
    -> Hypothesis CType               -- ^ Terms to generate bindings for
    -> Judgement                      -- ^ The goal of original hole
    -> RuleM (Synthesized (LHsExpr GhcPs))
letForEach :: (OccName -> OccName)
-> (HyInfo CType -> TacticsM ())
-> Hypothesis CType
-> Judgement
-> Rule
letForEach OccName -> OccName
rename HyInfo CType -> TacticsM ()
solve (Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis -> [HyInfo CType]
hy) Judgement
jdg = do
  case [HyInfo CType]
hy of
    [] -> Judgement -> Rule
newSubgoal Judgement
jdg
    [HyInfo CType]
_ -> do
      Context
ctx <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
      let g :: CType
g = Judgement -> CType
forall a. Judgement' a -> a
jGoal Judgement
jdg
      Synthesized [(OccName, HsExpr')]
terms <- ([Synthesized (OccName, HsExpr')]
 -> Synthesized [(OccName, HsExpr')])
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (OccName, HsExpr')]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [(OccName, HsExpr')])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Synthesized (OccName, HsExpr')]
-> Synthesized [(OccName, HsExpr')]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (RuleT
   Judgement
   (Synthesized (LHsExpr GhcPs))
   TacticError
   TacticState
   ExtractM
   [Synthesized (OccName, HsExpr')]
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized [(OccName, HsExpr')]))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (OccName, HsExpr')]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized [(OccName, HsExpr')])
forall a b. (a -> b) -> a -> b
$ [HyInfo CType]
-> (HyInfo CType
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (OccName, HsExpr')))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (OccName, HsExpr')]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [HyInfo CType]
hy ((HyInfo CType
  -> RuleT
       Judgement
       (Synthesized (LHsExpr GhcPs))
       TacticError
       TacticState
       ExtractM
       (Synthesized (OccName, HsExpr')))
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [Synthesized (OccName, HsExpr')])
-> (HyInfo CType
    -> RuleT
         Judgement
         (Synthesized (LHsExpr GhcPs))
         TacticError
         TacticState
         ExtractM
         (Synthesized (OccName, HsExpr')))
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (OccName, HsExpr')]
forall a b. (a -> b) -> a -> b
$ \HyInfo CType
hi -> do
        let name :: OccName
name = OccName -> OccName
rename (OccName -> OccName) -> OccName -> OccName
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi
        let generalized_let_ty :: CType
generalized_let_ty = Type -> CType
CType Type
alphaTy
        Synthesized (LHsExpr GhcPs)
res <- Judgement -> TacticsM () -> Rule
tacticToRule (CType -> Judgement -> Judgement
forall a. a -> Judgement' a -> Judgement' a
withNewGoal CType
generalized_let_ty Judgement
jdg) (TacticsM () -> Rule) -> TacticsM () -> Rule
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> TacticsM ()
solve HyInfo CType
hi
        Synthesized (OccName, HsExpr')
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (OccName, HsExpr'))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (OccName, HsExpr')
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized (OccName, HsExpr')))
-> Synthesized (OccName, HsExpr')
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized (OccName, HsExpr'))
forall a b. (a -> b) -> a -> b
$ (LHsExpr GhcPs -> (OccName, HsExpr'))
-> Synthesized (LHsExpr GhcPs) -> Synthesized (OccName, HsExpr')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((OccName
name,) (HsExpr' -> (OccName, HsExpr'))
-> (LHsExpr GhcPs -> HsExpr')
-> LHsExpr GhcPs
-> (OccName, HsExpr')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHsExpr GhcPs -> HsExpr'
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc) Synthesized (LHsExpr GhcPs)
res
      let hy' :: [(OccName, CType)]
hy' = ((OccName, HsExpr') -> (OccName, CType))
-> [(OccName, HsExpr')] -> [(OccName, CType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CType
g CType -> (OccName, HsExpr') -> (OccName, CType)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) ([(OccName, HsExpr')] -> [(OccName, CType)])
-> [(OccName, HsExpr')] -> [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ Synthesized [(OccName, HsExpr')] -> [(OccName, HsExpr')]
forall a. Synthesized a -> a
syn_val Synthesized [(OccName, HsExpr')]
terms
          matches :: Synthesized [RawValBind]
matches = ([(OccName, HsExpr')] -> [RawValBind])
-> Synthesized [(OccName, HsExpr')] -> Synthesized [RawValBind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((OccName, HsExpr') -> RawValBind)
-> [(OccName, HsExpr')] -> [RawValBind]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(OccName
occ, HsExpr'
expr) -> OccNameStr -> HsExpr' -> RawValBind
forall t. HasValBind t => OccNameStr -> HsExpr' -> t
valBind (OccName -> OccNameStr
occNameToStr OccName
occ) HsExpr'
expr)) Synthesized [(OccName, HsExpr')]
terms
      Synthesized HsExpr'
g <- (Synthesized (LHsExpr GhcPs) -> Synthesized HsExpr')
-> Rule
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized HsExpr')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LHsExpr GhcPs -> HsExpr')
-> Synthesized (LHsExpr GhcPs) -> Synthesized 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) (Rule
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      (Synthesized HsExpr'))
-> Rule
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Synthesized HsExpr')
forall a b. (a -> b) -> a -> b
$ Judgement -> Rule
newSubgoal (Judgement -> Rule) -> Judgement -> Rule
forall a b. (a -> b) -> a -> b
$ Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx ([(OccName, CType)] -> Hypothesis CType
forall a. [(OccName, a)] -> Hypothesis a
userHypothesis [(OccName, CType)]
hy') 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
$ (HsExpr' -> LHsExpr GhcPs)
-> Synthesized HsExpr' -> Synthesized (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 (Synthesized HsExpr' -> Synthesized (LHsExpr GhcPs))
-> Synthesized HsExpr' -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ [RawValBind] -> HsExpr' -> HsExpr'
let' ([RawValBind] -> HsExpr' -> HsExpr')
-> Synthesized [RawValBind] -> Synthesized (HsExpr' -> HsExpr')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Synthesized [RawValBind]
matches Synthesized (HsExpr' -> HsExpr')
-> Synthesized HsExpr' -> Synthesized HsExpr'
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Synthesized HsExpr'
g


------------------------------------------------------------------------------
-- | Let-bind the given occname judgement pairs.
nonrecLet
    :: [(OccName, Judgement)]
    -> Judgement
    -> RuleM (Synthesized (LHsExpr GhcPs))
nonrecLet :: [(OccName, Judgement)] -> Judgement -> Rule
nonrecLet [(OccName, Judgement)]
occjdgs Judgement
jdg = do
  [Synthesized (LHsExpr GhcPs)]
occexts <- (Judgement -> Rule)
-> [Judgement]
-> 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 Judgement -> Rule
newSubgoal ([Judgement]
 -> RuleT
      Judgement
      (Synthesized (LHsExpr GhcPs))
      TacticError
      TacticState
      ExtractM
      [Synthesized (LHsExpr GhcPs)])
-> [Judgement]
-> RuleT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [Synthesized (LHsExpr GhcPs)]
forall a b. (a -> b) -> a -> b
$ ((OccName, Judgement) -> Judgement)
-> [(OccName, Judgement)] -> [Judgement]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, Judgement) -> Judgement
forall a b. (a, b) -> b
snd [(OccName, Judgement)]
occjdgs
  Context
ctx     <- RuleT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  Context
forall r (m :: * -> *). MonadReader r m => m r
ask
  Synthesized (LHsExpr GhcPs)
ext     <- Judgement -> Rule
newSubgoal
           (Judgement -> Rule) -> Judgement -> Rule
forall a b. (a -> b) -> a -> b
$ Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx ([(OccName, CType)] -> Hypothesis CType
forall a. [(OccName, a)] -> Hypothesis a
userHypothesis ([(OccName, CType)] -> Hypothesis CType)
-> [(OccName, CType)] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ ((OccName, Judgement) -> (OccName, CType))
-> [(OccName, Judgement)] -> [(OccName, CType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Judgement -> CType) -> (OccName, Judgement) -> (OccName, CType)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Judgement -> CType
forall a. Judgement' a -> a
jGoal) [(OccName, Judgement)]
occjdgs) 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
$ (HsExpr' -> LHsExpr GhcPs)
-> Synthesized HsExpr' -> Synthesized (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 (Synthesized HsExpr' -> Synthesized (LHsExpr GhcPs))
-> Synthesized HsExpr' -> Synthesized (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$
    [RawValBind] -> HsExpr' -> HsExpr'
let'
      ([RawValBind] -> HsExpr' -> HsExpr')
-> Synthesized [RawValBind] -> Synthesized (HsExpr' -> HsExpr')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((OccName, Synthesized (LHsExpr GhcPs)) -> Synthesized RawValBind)
-> [(OccName, Synthesized (LHsExpr GhcPs))]
-> Synthesized [RawValBind]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
            (\(OccName
occ, Synthesized (LHsExpr GhcPs)
ext) -> OccNameStr -> HsExpr' -> RawValBind
forall t. HasValBind t => OccNameStr -> HsExpr' -> t
valBind (OccName -> OccNameStr
occNameToStr OccName
occ) (HsExpr' -> RawValBind)
-> Synthesized HsExpr' -> Synthesized RawValBind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LHsExpr GhcPs -> HsExpr')
-> Synthesized (LHsExpr GhcPs) -> Synthesized 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 Synthesized (LHsExpr GhcPs)
ext)
            ([OccName]
-> [Synthesized (LHsExpr GhcPs)]
-> [(OccName, Synthesized (LHsExpr GhcPs))]
forall a b. [a] -> [b] -> [(a, b)]
zip (((OccName, Judgement) -> OccName)
-> [(OccName, Judgement)] -> [OccName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (OccName, Judgement) -> OccName
forall a b. (a, b) -> a
fst [(OccName, Judgement)]
occjdgs) [Synthesized (LHsExpr GhcPs)]
occexts)
      Synthesized (HsExpr' -> HsExpr')
-> Synthesized HsExpr' -> Synthesized HsExpr'
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (LHsExpr GhcPs -> HsExpr')
-> Synthesized (LHsExpr GhcPs) -> Synthesized 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 Synthesized (LHsExpr GhcPs)
ext


------------------------------------------------------------------------------
-- | Converts a function application into applicative form
idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs
idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs
idiomize LHsExpr GhcPs
x = 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
$ case LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
x of
  HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 ->
    HsExpr' -> RdrNameStr -> HsExpr' -> HsExpr'
forall e. App e => e -> RdrNameStr -> e -> e
op (OccName -> HsExpr'
forall a. BVar a => OccName -> a
bvar' (OccName -> HsExpr') -> OccName -> HsExpr'
forall a b. (a -> b) -> a -> b
$ RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName IdP GhcPs
RdrName
x) RdrNameStr
"<$>" (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
gshgp3)
  HsApp _ gsigp gshgp3 ->
    HsExpr' -> RdrNameStr -> HsExpr' -> HsExpr'
forall e. App e => e -> RdrNameStr -> e -> e
op (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs))
-> LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> LHsExpr GhcPs
idiomize LHsExpr GhcPs
gsigp) RdrNameStr
"<*>" (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcPs
gshgp3)
  RecordCon _ con flds ->
    LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs))
-> LHsExpr GhcPs -> SrcSpanLess (LHsExpr GhcPs)
forall a b. (a -> b) -> a -> b
$ LHsExpr GhcPs -> LHsExpr GhcPs
idiomize (LHsExpr GhcPs -> LHsExpr GhcPs) -> LHsExpr GhcPs -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ 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' -> HsRecFields GhcPs 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
(@@) (XVar GhcPs -> Located (IdP GhcPs) -> HsExpr'
forall p. XVar p -> Located (IdP p) -> HsExpr p
HsVar NoExtField
XVar GhcPs
noExtField Located (IdP GhcPs)
con) (HsRecFields GhcPs HsExpr' -> HsExpr')
-> HsRecFields GhcPs HsExpr' -> HsExpr'
forall a b. (a -> b) -> a -> b
$ (LHsExpr GhcPs -> HsExpr')
-> HsRecFields GhcPs (LHsExpr GhcPs) -> HsRecFields 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 HsRecFields GhcPs (LHsExpr GhcPs)
flds
  SrcSpanLess (LHsExpr GhcPs)
y -> SrcSpanLess (LHsExpr GhcPs)
y