{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE OverloadedStrings #-}
module ECTA.Plugin (plugin) where

import GhcPlugins hiding ((<>))
import TcHoleErrors
import TcHoleFitTypes
import TcRnTypes
import Constraint

import ECTA.Plugin.Utils

import Application.TermSearch.Dataset
import Application.TermSearch.Type
import Application.TermSearch.TermSearch hiding (allConstructors, generalize)
import Data.ECTA
import Data.ECTA.Term

import qualified Data.Map as Map
import Data.Text (pack, unpack, Text)
import Data.Maybe (fromMaybe, mapMaybe, isJust, fromJust)
import Data.Tuple (swap)
import Data.List (sortOn, groupBy, nub, nubBy, (\\))
import Data.Function (on)
import qualified Data.Monoid as M
import MonadUtils (concatMapM)
import TcRnMonad (writeTcRef, newTcRef, readTcRef, mapMaybeM, getTopEnv)
import TcEnv (tcLookupId, tcLookupIdMaybe, tcLookup)
import qualified Data.Bifunctor as Bi
import TcRnDriver (tcRnGetInfo)
import GHC (ClsInst)
import InstEnv (ClsInst(ClsInst, is_tvs, is_cls_nm, is_tys), is_dfun)
import ConLike (ConLike(RealDataCon))
import Data.ECTA.Paths (Path, mkEqConstraints)
import Application.TermSearch.Utils
import Data.Containers.ListUtils (nubOrd)
import Debug.Trace
import Data.Either (partitionEithers)
import Text.Read (readMaybe)
import qualified Data.Set as Set




plugin :: Plugin
plugin :: Plugin
plugin =
  Plugin
defaultPlugin
    { holeFitPlugin :: HoleFitPlugin
holeFitPlugin = \[CommandLineOption]
opts ->
        HoleFitPluginR -> Maybe HoleFitPluginR
forall a. a -> Maybe a
Just (HoleFitPluginR -> Maybe HoleFitPluginR)
-> HoleFitPluginR -> Maybe HoleFitPluginR
forall a b. (a -> b) -> a -> b
$
          HoleFitPluginR :: forall s.
TcM (TcRef s)
-> (TcRef s -> HoleFitPlugin)
-> (TcRef s -> TcM ())
-> HoleFitPluginR
HoleFitPluginR {
            hfPluginInit :: TcM (TcRef [HoleFitCandidate])
hfPluginInit = [HoleFitCandidate] -> TcM (TcRef [HoleFitCandidate])
forall a gbl lcl. a -> TcRnIf gbl lcl (TcRef a)
newTcRef [],
            hfPluginRun :: TcRef [HoleFitCandidate] -> HoleFitPlugin
hfPluginRun = \TcRef [HoleFitCandidate]
ref ->
                  ( HoleFitPlugin :: CandPlugin -> FitPlugin -> HoleFitPlugin
HoleFitPlugin
                   { candPlugin :: CandPlugin
candPlugin = \TypedHole
_ [HoleFitCandidate]
c -> TcRef [HoleFitCandidate] -> [HoleFitCandidate] -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef TcRef [HoleFitCandidate]
ref [HoleFitCandidate]
c TcM ()
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFitCandidate]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFitCandidate]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [HoleFitCandidate]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFitCandidate]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFitCandidate]
c,
                     fitPlugin :: FitPlugin
fitPlugin = \TypedHole
h [HoleFit]
fts -> TcRef [HoleFitCandidate]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFitCandidate]
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef TcRef [HoleFitCandidate]
ref IOEnv (Env TcGblEnv TcLclEnv) [HoleFitCandidate]
-> ([HoleFitCandidate] -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit])
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [CommandLineOption]
-> TypedHole
-> [HoleFit]
-> [HoleFitCandidate]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
ectaPlugin [CommandLineOption]
opts TypedHole
h [HoleFit]
fts
                                  }
                              ),
            hfPluginStop :: TcRef [HoleFitCandidate] -> TcM ()
hfPluginStop = TcM () -> TcRef [HoleFitCandidate] -> TcM ()
forall a b. a -> b -> a
const (() -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
          }
    }


candsToComps :: [HoleFitCandidate] -> TcM [((Either Text Text, TypeSkeleton), [Type])]
candsToComps :: [HoleFitCandidate]
-> TcM [((Either Text Text, TypeSkeleton), [Type])]
candsToComps = (HoleFitCandidate
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Maybe ((Either Text Text, TypeSkeleton), [Type])))
-> [HoleFitCandidate]
-> TcM [((Either Text Text, TypeSkeleton), [Type])]
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM ((Maybe (Either Text Text, (TypeSkeleton, [Type]))
 -> Maybe ((Either Text Text, TypeSkeleton), [Type]))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe (Either Text Text, (TypeSkeleton, [Type])))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe ((Either Text Text, TypeSkeleton), [Type]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Either Text Text, (TypeSkeleton, [Type]))
 -> ((Either Text Text, TypeSkeleton), [Type]))
-> Maybe (Either Text Text, (TypeSkeleton, [Type]))
-> Maybe ((Either Text Text, TypeSkeleton), [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either Text Text, (TypeSkeleton, [Type]))
-> ((Either Text Text, TypeSkeleton), [Type])
forall a b b. (a, (b, b)) -> ((a, b), b)
extract) (IOEnv
   (Env TcGblEnv TcLclEnv)
   (Maybe (Either Text Text, (TypeSkeleton, [Type])))
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Maybe ((Either Text Text, TypeSkeleton), [Type])))
-> (HoleFitCandidate
    -> IOEnv
         (Env TcGblEnv TcLclEnv)
         (Maybe (Either Text Text, (TypeSkeleton, [Type]))))
-> HoleFitCandidate
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe ((Either Text Text, TypeSkeleton), [Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFitCandidate
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe (Either Text Text, (TypeSkeleton, [Type])))
candToTN)
  where candToTN :: HoleFitCandidate -> TcM (Maybe (Either Text Text, (TypeSkeleton, [Type])))
        candToTN :: HoleFitCandidate
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe (Either Text Text, (TypeSkeleton, [Type])))
candToTN HoleFitCandidate
cand = (Maybe Type -> Maybe (Either Text Text, (TypeSkeleton, [Type])))
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Maybe (Either Text Text, (TypeSkeleton, [Type])))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((TypeSkeleton, [Type])
 -> (Either Text Text, (TypeSkeleton, [Type])))
-> Maybe (TypeSkeleton, [Type])
-> Maybe (Either Text Text, (TypeSkeleton, [Type]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either Text Text
nm,) (Maybe (TypeSkeleton, [Type])
 -> Maybe (Either Text Text, (TypeSkeleton, [Type])))
-> (Maybe Type -> Maybe (TypeSkeleton, [Type]))
-> Maybe Type
-> Maybe (Either Text Text, (TypeSkeleton, [Type]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Type
-> (Type -> Maybe (TypeSkeleton, [Type]))
-> Maybe (TypeSkeleton, [Type])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Maybe (TypeSkeleton, [Type])
typeToSkeleton)) (HoleFitCandidate -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
c2t HoleFitCandidate
cand)
          where nm :: Either Text Text
nm = (case HoleFitCandidate
cand of
                      IdHFCand Id
_ -> Text -> Either Text Text
forall a b. a -> Either a b
Left
                      HoleFitCandidate
_ -> Text -> Either Text Text
forall a b. b -> Either a b
Right) (Text -> Either Text Text) -> Text -> Either Text Text
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> Text
pack (CommandLineOption -> Text) -> CommandLineOption -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> CommandLineOption
occNameString (OccName -> CommandLineOption) -> OccName -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> OccName
forall name. HasOccName name => name -> OccName
occName HoleFitCandidate
cand
                c2t :: HoleFitCandidate -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
c2t HoleFitCandidate
cand =
                  case HoleFitCandidate
cand of
                    IdHFCand Id
id -> Maybe Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type))
-> Maybe Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
idType Id
id
                    NameHFCand Name
nm -> TcTyThing -> Maybe Type
tcTyThingTypeMaybe (TcTyThing -> Maybe Type)
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyThing
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyThing
tcLookup Name
nm
                    GreHFCand GRE{Bool
[ImportSpec]
Parent
Name
gre_name :: GlobalRdrElt -> Name
gre_par :: GlobalRdrElt -> Parent
gre_lcl :: GlobalRdrElt -> Bool
gre_imp :: GlobalRdrElt -> [ImportSpec]
gre_imp :: [ImportSpec]
gre_lcl :: Bool
gre_par :: Parent
gre_name :: Name
..} -> TcTyThing -> Maybe Type
tcTyThingTypeMaybe  (TcTyThing -> Maybe Type)
-> IOEnv (Env TcGblEnv TcLclEnv) TcTyThing
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> IOEnv (Env TcGblEnv TcLclEnv) TcTyThing
tcLookup Name
gre_name
        extract :: (a, (b, b)) -> ((a, b), b)
extract (a
a, (b
b,b
c)) = ((a
a,b
b), b
c)
        tcTyThingTypeMaybe :: TcTyThing -> Maybe Type
        tcTyThingTypeMaybe :: TcTyThing -> Maybe Type
tcTyThingTypeMaybe (ATcId Id
tttid IdBindingInfo
_) = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
idType Id
tttid
        tcTyThingTypeMaybe (AGlobal (AnId Id
ttid)) =Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
idType Id
ttid
        tcTyThingTypeMaybe (AGlobal (ATyCon TyCon
ttid)) | Type
t <- TyCon -> [Type] -> Type
mkTyConApp TyCon
ttid [],
                                                    (Type -> Bool
tcReturnsConstraintKind (Type -> Bool) -> (Type -> Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind) Type
t
                                                    = Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t
        tcTyThingTypeMaybe (AGlobal (AConLike (RealDataCon DataCon
con))) = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Id -> Type
idType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ DataCon -> Id
dataConWorkId DataCon
con
        tcTyThingTypeMaybe TcTyThing
_ =  Maybe Type
forall a. Maybe a
Nothing


instToTerm :: ClsInst -> Maybe (Text, TypeSkeleton)
instToTerm :: ClsInst -> Maybe (Text, TypeSkeleton)
instToTerm ClsInst{[Type]
[Id]
Id
Name
is_dfun :: Id
is_tys :: [Type]
is_tvs :: [Id]
is_cls_nm :: Name
is_dfun :: ClsInst -> Id
is_tys :: ClsInst -> [Type]
is_cls_nm :: ClsInst -> Name
is_tvs :: ClsInst -> [Id]
..} | -- length is_tvs <= 1, -- uncomment if you want explosion!
                        Just (TypeSkeleton
tyskel,[Type]
args) <- Type -> Maybe (TypeSkeleton, [Type])
typeToSkeleton (Type -> Maybe (TypeSkeleton, [Type]))
-> Type -> Maybe (TypeSkeleton, [Type])
forall a b. (a -> b) -> a -> b
$ Id -> Type
idType Id
is_dfun
                        = (Text, TypeSkeleton) -> Maybe (Text, TypeSkeleton)
forall a. a -> Maybe a
Just (Text -> Text
toDictStr (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
clsstr Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
tystr, TypeSkeleton
tyskel )
  where clsstr :: Text
clsstr =  CommandLineOption -> Text
pack (CommandLineOption -> Text) -> CommandLineOption -> Text
forall a b. (a -> b) -> a -> b
$  SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
is_cls_nm
        tystr :: Text
tystr = CommandLineOption -> Text
pack (CommandLineOption -> Text) -> CommandLineOption -> Text
forall a b. (a -> b) -> a -> b
$ SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
is_tys
instToTerm ClsInst
_ = Maybe (Text, TypeSkeleton)
forall a. Maybe a
Nothing

toDictStr :: Text -> Text
toDictStr :: Text -> Text
toDictStr Text
t = Text -> Text
spToUnderscore (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text
"<@" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"@>"

spToUnderscore :: Text -> Text
spToUnderscore :: Text -> Text
spToUnderscore = CommandLineOption -> Text
pack (CommandLineOption -> Text)
-> (Text -> CommandLineOption) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOption -> CommandLineOption
sp (CommandLineOption -> CommandLineOption)
-> (Text -> CommandLineOption) -> Text -> CommandLineOption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CommandLineOption
unpack
  where sp :: CommandLineOption -> CommandLineOption
sp (Char
' ':CommandLineOption
str) = Char
'_'Char -> CommandLineOption -> CommandLineOption
forall a. a -> [a] -> [a]
:CommandLineOption -> CommandLineOption
sp CommandLineOption
str
        sp (Char
s:CommandLineOption
str) = Char
sChar -> CommandLineOption -> CommandLineOption
forall a. a -> [a] -> [a]
:CommandLineOption -> CommandLineOption
sp CommandLineOption
str
        sp [] = []


defaultSize :: Int
defaultSize :: Int
defaultSize = Int
5

-- | Parses the options and returns the max expression size to use.
-- limited to 5 by default.
getExprSize :: [CommandLineOption] -> Int
getExprSize :: [CommandLineOption] -> Int
getExprSize (CommandLineOption
o:[CommandLineOption]
opts) | (CommandLineOption
"expr-size",Char
'=':CommandLineOption
n) <- (Char -> Bool)
-> CommandLineOption -> (CommandLineOption, CommandLineOption)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'=') CommandLineOption
o,
                       Just Int
x <- CommandLineOption -> Maybe Int
forall a. Read a => CommandLineOption -> Maybe a
readMaybe CommandLineOption
n = Int
x
getExprSize [CommandLineOption]
_ = Int
defaultSize
 

dedup :: [Text] -> [Text]
dedup :: [Text] -> [Text]
dedup [Text]
ts = Set Text -> [Text] -> [Text]
forall a. Ord a => Set a -> [a] -> [a]
dedup' Set Text
forall a. Set a
Set.empty [Text]
ts
  where dedup' :: Set a -> [a] -> [a]
dedup' Set a
seen [] = []
        dedup' Set a
seen (a
t:[a]
ts) | a -> Set a -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member a
t Set a
seen = Set a -> [a] -> [a]
dedup' Set a
seen [a]
ts
        dedup' Set a
seen (a
t:[a]
ts) = a
ta -> [a] -> [a]
forall a. a -> [a] -> [a]
:Set a -> [a] -> [a]
dedup' (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
t Set a
seen) [a]
ts

ectaPlugin :: [CommandLineOption] -> TypedHole
           -> [HoleFit] -> [HoleFitCandidate] -> TcM [HoleFit]
ectaPlugin :: [CommandLineOption]
-> TypedHole
-> [HoleFit]
-> [HoleFitCandidate]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
ectaPlugin [CommandLineOption]
opts TyH{[Implication]
Maybe Ct
Cts
tyHRelevantCts :: TypedHole -> Cts
tyHImplics :: TypedHole -> [Implication]
tyHCt :: TypedHole -> Maybe Ct
tyHCt :: Maybe Ct
tyHImplics :: [Implication]
tyHRelevantCts :: Cts
..} [HoleFit]
found_fits [HoleFitCandidate]
scope | Just Ct
hole <- Maybe Ct
tyHCt,
                                           Int
expr_size <- [CommandLineOption] -> Int
getExprSize [CommandLineOption]
opts,
                                           Type
ty <- Ct -> Type
ctPred Ct
hole = do
      ([(Either Text Text, TypeSkeleton)]
fun_comps, [Type]
scons) <- ([[Type]] -> [Type])
-> ([(Either Text Text, TypeSkeleton)], [[Type]])
-> ([(Either Text Text, TypeSkeleton)], [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Type -> Type -> Bool) -> [Type] -> [Type]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Type -> Type -> Bool
eqType ([Type] -> [Type]) -> ([[Type]] -> [Type]) -> [[Type]] -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) (([(Either Text Text, TypeSkeleton)], [[Type]])
 -> ([(Either Text Text, TypeSkeleton)], [Type]))
-> ([((Either Text Text, TypeSkeleton), [Type])]
    -> ([(Either Text Text, TypeSkeleton)], [[Type]]))
-> [((Either Text Text, TypeSkeleton), [Type])]
-> ([(Either Text Text, TypeSkeleton)], [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((Either Text Text, TypeSkeleton), [Type])]
-> ([(Either Text Text, TypeSkeleton)], [[Type]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Either Text Text, TypeSkeleton), [Type])]
 -> ([(Either Text Text, TypeSkeleton)], [Type]))
-> TcM [((Either Text Text, TypeSkeleton), [Type])]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     ([(Either Text Text, TypeSkeleton)], [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoleFitCandidate]
-> TcM [((Either Text Text, TypeSkeleton), [Type])]
candsToComps [HoleFitCandidate]
scope
      let ([(Text, TypeSkeleton)]
local_comps, [(Text, TypeSkeleton)]
global_comps) = [Either (Text, TypeSkeleton) (Text, TypeSkeleton)]
-> ([(Text, TypeSkeleton)], [(Text, TypeSkeleton)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (Text, TypeSkeleton) (Text, TypeSkeleton)]
 -> ([(Text, TypeSkeleton)], [(Text, TypeSkeleton)]))
-> [Either (Text, TypeSkeleton) (Text, TypeSkeleton)]
-> ([(Text, TypeSkeleton)], [(Text, TypeSkeleton)])
forall a b. (a -> b) -> a -> b
$ ((Either Text Text, TypeSkeleton)
 -> Either (Text, TypeSkeleton) (Text, TypeSkeleton))
-> [(Either Text Text, TypeSkeleton)]
-> [Either (Text, TypeSkeleton) (Text, TypeSkeleton)]
forall a b. (a -> b) -> [a] -> [b]
map (Either Text Text, TypeSkeleton)
-> Either (Text, TypeSkeleton) (Text, TypeSkeleton)
forall a a b. (Either a a, b) -> Either (a, b) (a, b)
to_e [(Either Text Text, TypeSkeleton)]
fun_comps
          to_e :: (Either a a, b) -> Either (a, b) (a, b)
to_e (Left a
t,b
ts) = (a, b) -> Either (a, b) (a, b)
forall a b. a -> Either a b
Left (a
t,b
ts)
          to_e (Right a
t, b
ts) = (a, b) -> Either (a, b) (a, b)
forall a b. b -> Either a b
Right (a
t,b
ts)
      -- The constraints are there and added to the graph... but we have to
      -- be more precise when we add them to the machine. Any time a
      -- function requires a constraint to hold for one of it's variables,
      -- we have to add a path equality to the ECTA.
      let constraints :: [Type]
constraints = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter (Type -> Bool
tcReturnsConstraintKind (Type -> Bool) -> (Type -> Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Type -> Type
Type -> Type
tcTypeKind) [Type]
scons
      let givens :: [Type]
givens = (Implication -> [Type]) -> [Implication] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
idType ([Id] -> [Type]) -> (Implication -> [Id]) -> Implication -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Implication -> [Id]
ic_given) [Implication]
tyHImplics
          g2c :: Type -> Maybe (Text, TypeSkeleton)
g2c Type
g = (TypeSkeleton -> (Text, TypeSkeleton))
-> Maybe TypeSkeleton -> Maybe (Text, TypeSkeleton)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Text
toDictStr (CommandLineOption -> Text
pack (CommandLineOption -> Text) -> CommandLineOption -> Text
forall a b. (a -> b) -> a -> b
$ SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
g),)
                      (Maybe TypeSkeleton -> Maybe (Text, TypeSkeleton))
-> Maybe TypeSkeleton -> Maybe (Text, TypeSkeleton)
forall a b. (a -> b) -> a -> b
$ ((TypeSkeleton, [Type]) -> TypeSkeleton)
-> Maybe (TypeSkeleton, [Type]) -> Maybe TypeSkeleton
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TypeSkeleton, [Type]) -> TypeSkeleton
forall a b. (a, b) -> a
fst (Maybe (TypeSkeleton, [Type]) -> Maybe TypeSkeleton)
-> Maybe (TypeSkeleton, [Type]) -> Maybe TypeSkeleton
forall a b. (a -> b) -> a -> b
$ Type -> Maybe (TypeSkeleton, [Type])
typeToSkeleton Type
g
          given_comps :: [(Text, TypeSkeleton)]
given_comps = (Type -> Maybe (Text, TypeSkeleton))
-> [Type] -> [(Text, TypeSkeleton)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Type -> Maybe (Text, TypeSkeleton)
g2c [Type]
givens
      HscEnv
hsc_env <- TcRnIf TcGblEnv TcLclEnv HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
getTopEnv
      [(Text, TypeSkeleton)]
instance_comps <- (ClsInst -> Maybe (Text, TypeSkeleton))
-> [ClsInst] -> [(Text, TypeSkeleton)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ClsInst -> Maybe (Text, TypeSkeleton)
instToTerm ([ClsInst] -> [(Text, TypeSkeleton)])
-> ([[ClsInst]] -> [ClsInst])
-> [[ClsInst]]
-> [(Text, TypeSkeleton)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[ClsInst]] -> [ClsInst]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[ClsInst]] -> [(Text, TypeSkeleton)])
-> IOEnv (Env TcGblEnv TcLclEnv) [[ClsInst]]
-> IOEnv (Env TcGblEnv TcLclEnv) [(Text, TypeSkeleton)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                             (Type -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe [ClsInst]))
-> [Type] -> IOEnv (Env TcGblEnv TcLclEnv) [[ClsInst]]
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM (((Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
 -> Maybe [ClsInst])
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe [ClsInst])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((TyThing, Fixity, [ClsInst], [FamInst], SDoc) -> [ClsInst])
-> Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)
-> Maybe [ClsInst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TyThing
_,Fixity
_,[ClsInst]
c,[FamInst]
_,SDoc
_) -> [ClsInst]
c) (Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)
 -> Maybe [ClsInst])
-> ((Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
    -> Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
-> (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
-> Maybe [ClsInst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
-> Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)
forall a b. (a, b) -> b
snd)
                                       (IOEnv
   (Env TcGblEnv TcLclEnv)
   (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
 -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe [ClsInst]))
-> (Type
    -> IOEnv
         (Env TcGblEnv TcLclEnv)
         (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)))
-> Type
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe [ClsInst])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO  (IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)))
-> (Type
    -> IO
         (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)))
-> Type
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HscEnv
-> Name
-> IO
     (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
tcRnGetInfo HscEnv
hsc_env (Name
 -> IO
      (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc)))
-> (Type -> Name)
-> Type
-> IO
     (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> Name
forall a. NamedThing a => a -> Name
getName
                                       (TyCon -> Name) -> (Type -> TyCon) -> Type -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TyCon
tyConAppTyCon) [Type]
constraints
      let local_scope_comps :: [(Text, TypeSkeleton)]
local_scope_comps = [(Text, TypeSkeleton)]
local_comps [(Text, TypeSkeleton)]
-> [(Text, TypeSkeleton)] -> [(Text, TypeSkeleton)]
forall a. [a] -> [a] -> [a]
++ [(Text, TypeSkeleton)]
given_comps
          global_scope_comps :: [(Text, TypeSkeleton)]
global_scope_comps = [(Text, TypeSkeleton)]
global_comps [(Text, TypeSkeleton)]
-> [(Text, TypeSkeleton)] -> [(Text, TypeSkeleton)]
forall a. [a] -> [a] -> [a]
++ [(Text, TypeSkeleton)]
instance_comps
          scope_comps :: [(Text, TypeSkeleton)]
scope_comps = [(Text, TypeSkeleton)]
local_scope_comps [(Text, TypeSkeleton)]
-> [(Text, TypeSkeleton)] -> [(Text, TypeSkeleton)]
forall a. [a] -> [a] -> [a]
++ [(Text, TypeSkeleton)]
global_scope_comps
      let (Node
scopeNode, Node
anyArg, [(Symbol, Node)]
argNodes, Map Text TypeSkeleton
skels, Map Text [Text]
groups) =
            let argNodes :: [(Symbol, Node)]
argNodes = [(Text, TypeSkeleton)] -> [(Symbol, Node)]
ngnodes [(Text, TypeSkeleton)]
local_scope_comps
                addSyms :: (a -> Text) -> (Node -> d) -> [(a, TypeSkeleton)] -> [(Symbol, d)]
addSyms a -> Text
st Node -> d
tt = ((a, TypeSkeleton) -> (Symbol, d))
-> [(a, TypeSkeleton)] -> [(Symbol, d)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Symbol)
-> (TypeSkeleton -> d) -> (a, TypeSkeleton) -> (Symbol, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
Bi.bimap (Text -> Symbol
Symbol (Text -> Symbol) -> (a -> Text) -> a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Text
st) (Node -> d
tt (Node -> d) -> (TypeSkeleton -> Node) -> TypeSkeleton -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSkeleton -> Node
typeToFta))
                                ([(a, TypeSkeleton)] -> [(Symbol, d)])
-> ([(a, TypeSkeleton)] -> [(a, TypeSkeleton)])
-> [(a, TypeSkeleton)]
-> [(Symbol, d)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, TypeSkeleton) -> Bool)
-> [(a, TypeSkeleton)] -> [(a, TypeSkeleton)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
_,TypeSkeleton
t) -> TypeSkeleton -> Bool
isSafe TypeSkeleton
t)
                gnodes :: [(Text, TypeSkeleton)] -> [(Symbol, Node)]
gnodes = (Text -> Text)
-> (Node -> Node) -> [(Text, TypeSkeleton)] -> [(Symbol, Node)]
forall a d.
(a -> Text) -> (Node -> d) -> [(a, TypeSkeleton)] -> [(Symbol, d)]
addSyms Text -> Text
forall a. a -> a
id ([(Text, TypeSkeleton)] -> Node -> Node
generalize [(Text, TypeSkeleton)]
global_scope_comps)
                ngnodes :: [(Text, TypeSkeleton)] -> [(Symbol, Node)]
ngnodes = (Text -> Text)
-> (Node -> Node) -> [(Text, TypeSkeleton)] -> [(Symbol, Node)]
forall a d.
(a -> Text) -> (Node -> d) -> [(a, TypeSkeleton)] -> [(Symbol, d)]
addSyms Text -> Text
forall a. a -> a
id Node -> Node
forall a. a -> a
id
                anyArg :: Node
anyArg = [Edge] -> Node
Node ([Edge] -> Node) -> [Edge] -> Node
forall a b. (a -> b) -> a -> b
$ ((Symbol, Node) -> Edge) -> [(Symbol, Node)] -> [Edge]
forall a b. (a -> b) -> [a] -> [b]
map (\(Symbol
s,Node
t) -> Symbol -> [Node] -> Edge
Edge Symbol
s [Node
t]) ([(Symbol, Node)] -> [Edge]) -> [(Symbol, Node)] -> [Edge]
forall a b. (a -> b) -> a -> b
$ 
                        ([(Text, TypeSkeleton)] -> [(Symbol, Node)]
gnodes [(Text, TypeSkeleton)]
global_scope_comps) [(Symbol, Node)] -> [(Symbol, Node)] -> [(Symbol, Node)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Node)]
argNodes
                scopeNode :: Node
scopeNode = Node
anyArg
                skels :: Map Text TypeSkeleton
skels = [(Text, TypeSkeleton)] -> Map Text TypeSkeleton
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, TypeSkeleton)] -> Map Text TypeSkeleton)
-> [(Text, TypeSkeleton)] -> Map Text TypeSkeleton
forall a b. (a -> b) -> a -> b
$ [(Text, TypeSkeleton)]
scope_comps
                groups :: Map Text [Text]
groups = [(Text, [Text])] -> Map Text [Text]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Text, [Text])] -> Map Text [Text])
-> [(Text, [Text])] -> Map Text [Text]
forall a b. (a -> b) -> a -> b
$ ((Text, TypeSkeleton) -> (Text, [Text]))
-> [(Text, TypeSkeleton)] -> [(Text, [Text])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
t,TypeSkeleton
_) -> (Text
t,[Text
t])) [(Text, TypeSkeleton)]
scope_comps
            in (Node
scopeNode, Node
anyArg, [(Symbol, Node)]
argNodes, Map Text TypeSkeleton
skels, Map Text [Text]
groups)
      case Type -> Maybe (TypeSkeleton, [Type])
typeToSkeleton Type
ty of
         Just (TypeSkeleton
t, [Type]
cons) | TypeSkeleton -> Bool
isSafe TypeSkeleton
t,
                          Node
resNode <- TypeSkeleton -> Node
typeToFta TypeSkeleton
t -> do
             let res :: [Term]
res = Node -> [Term]
getAllTerms (Node -> [Term]) -> Node -> [Term]
forall a b. (a -> b) -> a -> b
$ Node -> Node
refold (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node
reduceFully (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ Node -> Node -> Node
filterType Node
scopeNode Node
resNode
             -- We ignore ppterms for now, because they need to be printed differently.
             -- ppterms <- concatMapM (prettyMatch skels groups . prettyTerm ) res
             let even_more_terms :: [Text]
even_more_terms =
                  (Term -> Text) -> [Term] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Text
ppNoPar (Term -> Text) -> (Term -> Term) -> Term -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
prettyTerm) ([Term] -> [Text]) -> [Term] -> [Text]
forall a b. (a -> b) -> a -> b
$
                    (Node -> [Term]) -> [Node] -> [Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Node -> [Term]
getAllTerms (Node -> [Term]) -> (Node -> Node) -> Node -> [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Node
refold (Node -> Node) -> (Node -> Node) -> Node -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Node
reduceFully (Node -> Node) -> (Node -> Node) -> Node -> Node
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Node -> Node -> Node) -> Node -> Node -> Node
forall a b c. (a -> b -> c) -> b -> a -> c
flip Node -> Node -> Node
filterType Node
resNode )
                              ([(Symbol, Node)]
-> [(Text, TypeSkeleton)] -> Node -> Bool -> Int -> [Node]
rtkUpToKAtLeast1 [(Symbol, Node)]
argNodes [(Text, TypeSkeleton)]
scope_comps Node
anyArg Bool
True Int
expr_size)
                 --text_fits = ppterms  ++ even_more_terms
                 ecta_fits :: [Text]
ecta_fits = [Text] -> [Text]
dedup [Text]
even_more_terms
                 fit_set :: Set Text
fit_set = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList ([Text] -> Set Text) -> [Text] -> Set Text
forall a b. (a -> b) -> a -> b
$ (HoleFit -> Maybe Text) -> [HoleFit] -> [Text]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe HoleFit -> Maybe Text
f [HoleFit]
found_fits
                   where f :: HoleFit -> Maybe Text
f (HoleFit {hfCand :: HoleFit -> HoleFitCandidate
hfCand=HoleFitCandidate
c}) = Text -> Maybe Text
forall a. a -> Maybe a
Just (CommandLineOption -> Text
pack (CommandLineOption -> Text) -> CommandLineOption -> Text
forall a b. (a -> b) -> a -> b
$ OccName -> CommandLineOption
occNameString (OccName -> CommandLineOption) -> OccName -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> OccName
forall name. HasOccName name => name -> OccName
occName HoleFitCandidate
c)
                         f HoleFit
_ = Maybe Text
forall a. Maybe a
Nothing
                 filtered_fits :: [HoleFit]
filtered_fits = (Text -> HoleFit) -> [Text] -> [HoleFit]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc -> HoleFit
RawHoleFit (SDoc -> HoleFit) -> (Text -> SDoc) -> Text -> HoleFit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandLineOption -> SDoc
text (CommandLineOption -> SDoc)
-> (Text -> CommandLineOption) -> Text -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> CommandLineOption
unpack (Text -> CommandLineOption)
-> (Text -> Text) -> Text -> CommandLineOption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
parIfReq) ([Text] -> [HoleFit]) -> [Text] -> [HoleFit]
forall a b. (a -> b) -> a -> b
$
                                 (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Text -> Bool) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Set Text -> Bool) -> Set Text -> Text -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Set Text -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set Text
fit_set) [Text]
ecta_fits
             [HoleFit] -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return ([HoleFit] -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit])
-> [HoleFit] -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall a b. (a -> b) -> a -> b
$ [HoleFit]
found_fits [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
++ [HoleFit]
filtered_fits
         Maybe (TypeSkeleton, [Type])
_ ->  [HoleFit] -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
found_fits
         -- liftIO $ putStrLn $  "Could not skeleton `" ++ showSDocUnsafe (ppr ty) ++"`"
         --          return []


-- TODO:
-- 1. I think we need to add type applications, i.e. [] @a or similar, let's see.