{-# 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, tryAllM)
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

import Control.Exception (evaluate, displayException)
import System.IO (hPutStrLn, stderr)



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
  let hM :: IOEnv env [HoleFit] -> IOEnv env [HoleFit]
hM IOEnv env [HoleFit]
act = do Either SomeException [HoleFit]
io_r <- IOEnv env [HoleFit] -> IOEnv env (Either SomeException [HoleFit])
forall env r. IOEnv env r -> IOEnv env (Either SomeException r)
tryAllM (IOEnv env [HoleFit] -> IOEnv env (Either SomeException [HoleFit]))
-> IOEnv env [HoleFit]
-> IOEnv env (Either SomeException [HoleFit])
forall a b. (a -> b) -> a -> b
$ do [HoleFit]
inner_r <- IOEnv env [HoleFit]
act
                                       -- we have to force the evaluation of
                                       -- the elements in the list,  otherwise
                                       -- the error doesn't show up... and then
                                       -- we can't catch it.
                                       [HoleFit]
_ <- IO [HoleFit] -> IOEnv env [HoleFit]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [HoleFit] -> IOEnv env [HoleFit])
-> IO [HoleFit] -> IOEnv env [HoleFit]
forall a b. (a -> b) -> a -> b
$ (HoleFit -> IO HoleFit) -> [HoleFit] -> IO [HoleFit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HoleFit -> IO HoleFit
forall a. a -> IO a
evaluate [HoleFit]
inner_r
                                       [HoleFit] -> IOEnv env [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
inner_r
                  case Either SomeException [HoleFit]
io_r of
                    Left SomeException
e -> do IO () -> IOEnv env ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IOEnv env ()) -> IO () -> IOEnv env ()
forall a b. (a -> b) -> a -> b
$ do Handle -> CommandLineOption -> IO ()
hPutStrLn Handle
stderr (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption
"Hectare error:"
                                             Handle -> CommandLineOption -> IO ()
hPutStrLn Handle
stderr (CommandLineOption -> IO ()) -> CommandLineOption -> IO ()
forall a b. (a -> b) -> a -> b
$ (SomeException -> CommandLineOption
forall e. Exception e => e -> CommandLineOption
displayException SomeException
e)
                                 [HoleFit] -> IOEnv env [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
found_fits
                    Right [HoleFit]
r -> [HoleFit] -> IOEnv env [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
r
  IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall env. IOEnv env [HoleFit] -> IOEnv env [HoleFit]
hM (IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
 -> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit])
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFit]
forall a b. (a -> b) -> a -> b
$ 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
      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
      case Type -> Maybe (TypeSkeleton, [Type])
typeToSkeleton Type
ty of
            Just (TypeSkeleton
t, [Type]
cons) | -- isSafe t,
                             Node
resNode <- TypeSkeleton -> Node
typeToFta TypeSkeleton
t -> do
                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
                    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 (scopeNode, anyArg, argNodes, skels, groups) =
                    argNodes :: [(Symbol, Node)]
argNodes = [(Text, TypeSkeleton)] -> [(Symbol, Node)]
ngnodes [(Text, TypeSkeleton)]
local_scope_comps
                    addSyms :: (a -> Text) -> (Node -> d) -> [p a TypeSkeleton] -> [p Symbol d]
addSyms a -> Text
st Node -> d
tt = (p a TypeSkeleton -> p Symbol d)
-> [p a TypeSkeleton] -> [p Symbol d]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Symbol)
-> (TypeSkeleton -> d) -> p a TypeSkeleton -> p 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))
                                    -- . filter (\(_,t) -> isSafe t)
                    gnodes :: [(Text, TypeSkeleton)] -> [(Symbol, Node)]
gnodes = (Text -> Text)
-> (Node -> Node) -> [(Text, TypeSkeleton)] -> [(Symbol, Node)]
forall (p :: * -> * -> *) a d.
Bifunctor p =>
(a -> Text) -> (Node -> d) -> [p a TypeSkeleton] -> [p 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 (p :: * -> * -> *) a d.
Bifunctor p =>
(a -> Text) -> (Node -> d) -> [p a TypeSkeleton] -> [p 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 (scopeNode, anyArg, argNodes, skels, groups)
                -- We ignore ppterms for now, because they need to be printed differently.
                -- let res = getAllTerms $ refold $ reduceFully $ filterType scopeNode resNode
                -- 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


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