{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}

module Intensional (plugin, Benchmark(..)) where

import BinIface
import Binary
import Intensional.Constructors
import Intensional.Constraints
import Intensional.Types
import Control.Monad
import Data.Aeson
import qualified Data.Map as Map
import qualified Data.List as List
import GhcPlugins
import IfaceEnv
import IfaceSyn
import Intensional.InferCoreExpr
import Intensional.InferM
import System.CPUTime
import System.Directory
import TcIface
import TcRnMonad
import ToIface
import TyCoRep
import PprColour
import Pretty (Mode(..))
import OccName
import NameCache (OrigNameCache)
import GHC.Generics (Generic)
import System.IO
import qualified System.Console.Haskeline as Haskeline

{-|
  The GHC plugin is hardwired as @plugin@.  
-}
plugin :: Plugin
plugin :: Plugin
plugin = 
    Plugin
defaultPlugin {
      pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = [CommandLineOption] -> IO PluginRecompile
forall (m :: * -> *) (t :: * -> *).
(Monad m, Foldable t) =>
t CommandLineOption -> m PluginRecompile
recomp, 
      installCoreToDos :: CorePlugin
installCoreToDos = CorePlugin
forall (m :: * -> *).
Monad m =>
[CommandLineOption] -> [CoreToDo] -> m [CoreToDo]
install
    }
  where
    recomp :: t CommandLineOption -> m PluginRecompile
recomp cmd :: t CommandLineOption
cmd =
      PluginRecompile -> m PluginRecompile
forall (m :: * -> *) a. Monad m => a -> m a
return (PluginRecompile -> m PluginRecompile)
-> PluginRecompile -> m PluginRecompile
forall a b. (a -> b) -> a -> b
$ if "force" CommandLineOption -> t CommandLineOption -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t CommandLineOption
cmd then PluginRecompile
ForceRecompile else PluginRecompile
NoForceRecompile 
    todoPrefix :: [CommandLineOption] -> [CoreToDo]
todoPrefix cmd :: [CommandLineOption]
cmd = [ 
        CoreToDo
CoreDoStrictness, -- it is useful to know what is bottom for the purpose of pattern failures
        CommandLineOption -> CorePluginPass -> CoreToDo
CoreDoPluginPass "Intensional" ([CommandLineOption] -> CorePluginPass
inferGuts [CommandLineOption]
cmd)
      ]
    install :: [CommandLineOption] -> [CoreToDo] -> m [CoreToDo]
install cmd :: [CommandLineOption]
cmd todo :: [CoreToDo]
todo = [CoreToDo] -> m [CoreToDo]
forall (m :: * -> *) a. Monad m => a -> m a
return ([CommandLineOption] -> [CoreToDo]
todoPrefix [CommandLineOption]
cmd [CoreToDo] -> [CoreToDo] -> [CoreToDo]
forall a. [a] -> [a] -> [a]
++ [CoreToDo]
todo)

{-|
    Given a module name @m@, @interfaceName m@ is the file path
    that will be written with the corresponding serialised typings.
-}
interfaceName :: ModuleName -> FilePath
interfaceName :: ModuleName -> CommandLineOption
interfaceName = ("interface/" CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++) (CommandLineOption -> CommandLineOption)
-> (ModuleName -> CommandLineOption)
-> ModuleName
-> CommandLineOption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> CommandLineOption
moduleNameString

inferGuts :: [CommandLineOption] -> ModGuts -> CoreM ModGuts
inferGuts :: [CommandLineOption] -> CorePluginPass
inferGuts cmd :: [CommandLineOption]
cmd guts :: ModGuts
guts@ModGuts {mg_deps :: ModGuts -> Dependencies
mg_deps = Dependencies
d, mg_module :: ModGuts -> Module
mg_module = Module
m, mg_binds :: ModGuts -> CoreProgram
mg_binds = CoreProgram
p} = do
  Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ("debug-core" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
cmd) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc -> CoreM ()
forall (f :: * -> *).
Applicative f =>
CommandLineOption -> SDoc -> f ()
pprTraceM "Core Source:" (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ CoreProgram -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreProgram
p
  HscEnv
hask <- CoreM HscEnv
getHscEnv
  OrigNameCache
che <- CoreM OrigNameCache
getOrigNameCache 
  DynFlags
dflags <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags 
  IO ModGuts -> CoreM ModGuts
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ModGuts -> CoreM ModGuts) -> IO ModGuts -> CoreM ModGuts
forall a b. (a -> b) -> a -> b
$ do
    -- Reload saved typeschemes
    let gbl :: IfGblEnv
gbl =
          IfGblEnv :: SDoc -> Maybe (Module, IfG TypeEnv) -> IfGblEnv
IfGblEnv { 
            if_doc :: SDoc
if_doc = CommandLineOption -> SDoc
text "initIfaceLoad",
            if_rec_types :: Maybe (Module, IfG TypeEnv)
if_rec_types = Maybe (Module, IfG TypeEnv)
forall a. Maybe a
Nothing
          }
    Map Name (SchemeGen TyCon)
env <- 
      Char
-> HscEnv
-> IfGblEnv
-> IfLclEnv
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
-> IO (Map Name (SchemeGen TyCon))
forall gbl lcl a.
Char -> HscEnv -> gbl -> lcl -> TcRnIf gbl lcl a -> IO a
initTcRnIf 'i' HscEnv
hask IfGblEnv
gbl (Module -> SDoc -> Bool -> IfLclEnv
mkIfLclEnv Module
m SDoc
empty Bool
False) (TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
 -> IO (Map Name (SchemeGen TyCon)))
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
-> IO (Map Name (SchemeGen TyCon))
forall a b. (a -> b) -> a -> b
$ do
        NameCacheUpdater
cache <- TcRnIf IfGblEnv IfLclEnv NameCacheUpdater
forall a b. TcRnIf a b NameCacheUpdater
mkNameCacheUpdater
        (Map Name (SchemeGen TyCon)
 -> (ModuleName, Bool)
 -> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon)))
-> Map Name (SchemeGen TyCon)
-> [(ModuleName, Bool)]
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          ( \env :: Map Name (SchemeGen TyCon)
env (ModuleName -> CommandLineOption
interfaceName -> CommandLineOption
m_name, _) -> do
              Bool
exists <- IO Bool -> IOEnv (Env IfGblEnv IfLclEnv) Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> IOEnv (Env IfGblEnv IfLclEnv) Bool)
-> IO Bool -> IOEnv (Env IfGblEnv IfLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO Bool
doesFileExist CommandLineOption
m_name
              if Bool
exists
                then do
                  BinHandle
bh <- IO BinHandle -> IOEnv (Env IfGblEnv IfLclEnv) BinHandle
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO BinHandle -> IOEnv (Env IfGblEnv IfLclEnv) BinHandle)
-> IO BinHandle -> IOEnv (Env IfGblEnv IfLclEnv) BinHandle
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> IO BinHandle
readBinMem CommandLineOption
m_name
                  Map Name (SchemeGen IfaceTyCon)
ictx <- IO (Map Name (SchemeGen IfaceTyCon))
-> IOEnv (Env IfGblEnv IfLclEnv) (Map Name (SchemeGen IfaceTyCon))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Map Name (SchemeGen IfaceTyCon))
 -> IOEnv (Env IfGblEnv IfLclEnv) (Map Name (SchemeGen IfaceTyCon)))
-> IO (Map Name (SchemeGen IfaceTyCon))
-> IOEnv (Env IfGblEnv IfLclEnv) (Map Name (SchemeGen IfaceTyCon))
forall a b. (a -> b) -> a -> b
$ [(Name, SchemeGen IfaceTyCon)] -> Map Name (SchemeGen IfaceTyCon)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, SchemeGen IfaceTyCon)] -> Map Name (SchemeGen IfaceTyCon))
-> IO [(Name, SchemeGen IfaceTyCon)]
-> IO (Map Name (SchemeGen IfaceTyCon))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameCacheUpdater -> BinHandle -> IO [(Name, SchemeGen IfaceTyCon)]
forall a. Binary a => NameCacheUpdater -> BinHandle -> IO a
getWithUserData NameCacheUpdater
cache BinHandle
bh
                  Map Name (SchemeGen TyCon)
ctx <- (SchemeGen IfaceTyCon
 -> IOEnv (Env IfGblEnv IfLclEnv) (SchemeGen TyCon))
-> Map Name (SchemeGen IfaceTyCon)
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((IfaceTyCon -> IOEnv (Env IfGblEnv IfLclEnv) TyCon)
-> SchemeGen IfaceTyCon
-> IOEnv (Env IfGblEnv IfLclEnv) (SchemeGen TyCon)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM IfaceTyCon -> IOEnv (Env IfGblEnv IfLclEnv) TyCon
tcIfaceTyCon) Map Name (SchemeGen IfaceTyCon)
ictx
                  Map Name (SchemeGen TyCon)
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Name (SchemeGen TyCon)
-> Map Name (SchemeGen TyCon) -> Map Name (SchemeGen TyCon)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Name (SchemeGen TyCon)
ctx Map Name (SchemeGen TyCon)
env)
                else Map Name (SchemeGen TyCon)
-> TcRnIf IfGblEnv IfLclEnv (Map Name (SchemeGen TyCon))
forall (m :: * -> *) a. Monad m => a -> m a
return Map Name (SchemeGen TyCon)
env
          )
          Map Name (SchemeGen TyCon)
forall k a. Map k a
Map.empty
          (Dependencies -> [(ModuleName, Bool)]
dep_mods Dependencies
d)
    Integer
t0 <- IO Integer
getCPUTime
    -- Infer constraints
    let (!Map Name (SchemeGen TyCon)
gamma, ![Atomic]
errs, !Stats
stats) = InferM (Map Name (SchemeGen TyCon))
-> Module
-> Map Name (SchemeGen TyCon)
-> (Map Name (SchemeGen TyCon), [Atomic], Stats)
forall a.
InferM a
-> Module -> Map Name (SchemeGen TyCon) -> (a, [Atomic], Stats)
runInferM (CoreProgram -> InferM (Map Name (SchemeGen TyCon))
inferProg CoreProgram
p) Module
m Map Name (SchemeGen TyCon)
env
    Integer
t1 <- IO Integer
getCPUTime
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ("time" CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
cmd) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      CommandLineOption -> (Integer, Integer) -> Stats -> IO ()
recordBenchmarks (ModuleName -> CommandLineOption
moduleNameString (Module -> ModuleName
moduleName Module
m)) (Integer
t0, Integer
t1) Stats
stats
    -- Display type errors
    let printErrLn :: SDoc -> IO ()
printErrLn = 
          Mode -> DynFlags -> Handle -> PprStyle -> SDoc -> IO ()
printSDocLn Mode
PageMode DynFlags
dflags Handle
stderr (Bool -> PprStyle -> PprStyle
setStyleColoured Bool
True (PprStyle -> PprStyle) -> PprStyle -> PprStyle
forall a b. (a -> b) -> a -> b
$ DynFlags -> PprStyle
defaultErrStyle DynFlags
dflags)
    (Atomic -> IO ()) -> [Atomic] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\a :: Atomic
a -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Module
m Module -> Module -> Bool
forall a. Eq a => a -> a -> Bool
== Atomic -> Module
modInfo Atomic
a) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SDoc -> IO ()
printErrLn (Atomic -> SDoc
showTypeError Atomic
a)) [Atomic]
errs
    -- Save typeschemes to interface file
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleName -> CommandLineOption
moduleNameString (Module -> ModuleName
moduleName Module
m) CommandLineOption -> [CommandLineOption] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CommandLineOption]
cmd) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ 
      Map Name (SchemeGen TyCon)
-> Module -> CoreProgram -> OrigNameCache -> IO ()
repl (Map Name (SchemeGen TyCon)
gamma Map Name (SchemeGen TyCon)
-> Map Name (SchemeGen TyCon) -> Map Name (SchemeGen TyCon)
forall a. Semigroup a => a -> a -> a
Prelude.<> Map Name (SchemeGen TyCon)
env) Module
m CoreProgram
p OrigNameCache
che
    Bool
exist <- CommandLineOption -> IO Bool
doesDirectoryExist "interface"
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exist (CommandLineOption -> IO ()
createDirectory "interface")
    BinHandle
bh <- Int -> IO BinHandle
openBinMem (1024 Int -> Int -> Int
forall a. Num a => a -> a -> a
* 1024)
    (SDoc -> IO ())
-> BinHandle -> [(Name, SchemeGen IfaceTyCon)] -> IO ()
forall a. Binary a => (SDoc -> IO ()) -> BinHandle -> a -> IO ()
putWithUserData
      (IO () -> SDoc -> IO ()
forall a b. a -> b -> a
const (IO () -> SDoc -> IO ()) -> IO () -> SDoc -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
      BinHandle
bh
      (Map Name (SchemeGen IfaceTyCon) -> [(Name, SchemeGen IfaceTyCon)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name (SchemeGen IfaceTyCon) -> [(Name, SchemeGen IfaceTyCon)])
-> Map Name (SchemeGen IfaceTyCon)
-> [(Name, SchemeGen IfaceTyCon)]
forall a b. (a -> b) -> a -> b
$ (Name -> SchemeGen IfaceTyCon -> Bool)
-> Map Name (SchemeGen IfaceTyCon)
-> Map Name (SchemeGen IfaceTyCon)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\k :: Name
k _ -> Name -> Bool
isExternalName Name
k) ((TyCon -> IfaceTyCon) -> SchemeGen TyCon -> SchemeGen IfaceTyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCon -> IfaceTyCon
toIfaceTyCon (SchemeGen TyCon -> SchemeGen IfaceTyCon)
-> Map Name (SchemeGen TyCon) -> Map Name (SchemeGen IfaceTyCon)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Name (SchemeGen TyCon)
gamma))
    BinHandle -> CommandLineOption -> IO ()
writeBinMem BinHandle
bh (ModuleName -> CommandLineOption
interfaceName (Module -> ModuleName
moduleName Module
m))
    ModGuts -> IO ModGuts
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
guts

{-|
  When @cx@ is the type bindings for all the program so far and @md@
  is the currently processed module and @ch@ is GHC's name cache,
  @repl cx md ch@ is a read-eval-print-loop IO action, allowing the 
  user to inspect individual type bindings and output the raw core.
-}
repl :: Context -> Module -> CoreProgram -> OrigNameCache -> IO ()
repl :: Map Name (SchemeGen TyCon)
-> Module -> CoreProgram -> OrigNameCache -> IO ()
repl cx :: Map Name (SchemeGen TyCon)
cx md :: Module
md pr :: CoreProgram
pr ch :: OrigNameCache
ch =
  Settings IO -> InputT IO () -> IO ()
forall (m :: * -> *) a.
MonadException m =>
Settings m -> InputT m a -> m a
Haskeline.runInputT Settings IO
forall (m :: * -> *). MonadIO m => Settings m
Haskeline.defaultSettings InputT IO ()
loop
  where
    loop :: InputT IO ()
loop = 
      do  Maybe CommandLineOption
mbInput <- CommandLineOption -> InputT IO (Maybe CommandLineOption)
forall (m :: * -> *).
MonadException m =>
CommandLineOption -> InputT m (Maybe CommandLineOption)
Haskeline.getInputLine (CommandLineOption
modn CommandLineOption -> CommandLineOption -> CommandLineOption
forall a. [a] -> [a] -> [a]
++ "> ") 
          case CommandLineOption -> [CommandLineOption]
words (CommandLineOption -> [CommandLineOption])
-> Maybe CommandLineOption -> Maybe [CommandLineOption]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CommandLineOption
mbInput of
            Just [":q"]          -> () -> InputT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just [":c", strName :: CommandLineOption
strName] -> 
              do  case CommandLineOption -> Maybe Name
mkName CommandLineOption
strName of
                    Just n :: Name
n | Just e :: Expr CoreBndr
e <- Name -> [(Name, Expr CoreBndr)] -> Maybe (Expr CoreBndr)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup Name
n (((CoreBndr, Expr CoreBndr) -> (Name, Expr CoreBndr))
-> [(CoreBndr, Expr CoreBndr)] -> [(Name, Expr CoreBndr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: CoreBndr
x,y :: Expr CoreBndr
y) -> (CoreBndr -> Name
forall a. NamedThing a => a -> Name
getName CoreBndr
x, Expr CoreBndr
y)) ([(CoreBndr, Expr CoreBndr)] -> [(Name, Expr CoreBndr)])
-> [(CoreBndr, Expr CoreBndr)] -> [(Name, Expr CoreBndr)]
forall a b. (a -> b) -> a -> b
$ CoreProgram -> [(CoreBndr, Expr CoreBndr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds CoreProgram
pr) ->
                      CommandLineOption -> InputT IO ()
forall (m :: * -> *). MonadIO m => CommandLineOption -> InputT m ()
Haskeline.outputStrLn (CommandLineOption -> InputT IO ())
-> CommandLineOption -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Expr CoreBndr -> SDoc
forall a. Outputable a => a -> SDoc
ppr Expr CoreBndr
e
                    _   -> () -> InputT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  InputT IO ()
loop
            Just [":t", strName :: CommandLineOption
strName] ->
              do  case CommandLineOption -> Maybe Name
mkName CommandLineOption
strName of
                    Just n :: Name
n | Just ts :: SchemeGen TyCon
ts <- Name -> Map Name (SchemeGen TyCon) -> Maybe (SchemeGen TyCon)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name (SchemeGen TyCon)
cx -> 
                      CommandLineOption -> InputT IO ()
forall (m :: * -> *). MonadIO m => CommandLineOption -> InputT m ()
Haskeline.outputStrLn (CommandLineOption -> InputT IO ())
-> CommandLineOption -> InputT IO ()
forall a b. (a -> b) -> a -> b
$ SDoc -> CommandLineOption
showSDocUnsafe (SDoc -> CommandLineOption) -> SDoc -> CommandLineOption
forall a b. (a -> b) -> a -> b
$ Name -> SchemeGen TyCon -> SDoc
forall a t. (Outputable a, Refined t) => a -> t -> SDoc
typingDoc Name
n SchemeGen TyCon
ts
                    _                                    -> () -> InputT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  InputT IO ()
loop
            _              -> InputT IO ()
loop
    typingDoc :: a -> t -> SDoc
typingDoc n :: a
n ts :: t
ts = a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
n SDoc -> SDoc -> SDoc
<+> SDoc
colon SDoc -> SDoc -> SDoc
<+> (Int -> SDoc) -> t -> SDoc
forall t. Refined t => (Int -> SDoc) -> t -> SDoc
prpr (SDoc -> Int -> SDoc
forall a b. a -> b -> a
const SDoc
empty) t
ts 
    modn :: CommandLineOption
modn = ModuleName -> CommandLineOption
moduleNameString (Module -> ModuleName
moduleName Module
md)
    mkName :: CommandLineOption -> Maybe Name
mkName s :: CommandLineOption
s = OrigNameCache -> Module -> OccName -> Maybe Name
lookupOrigNameCache OrigNameCache
ch Module
m OccName
n
      where 
        s' :: CommandLineOption
s' = CommandLineOption -> CommandLineOption
forall a. [a] -> [a]
reverse CommandLineOption
s
        (n' :: CommandLineOption
n', m' :: CommandLineOption
m') = (Char -> Bool)
-> CommandLineOption -> (CommandLineOption, CommandLineOption)
forall a. (a -> Bool) -> [a] -> ([a], [a])
Prelude.span (\c :: Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '.') CommandLineOption
s'
        n :: OccName
n = NameSpace -> CommandLineOption -> OccName
mkOccName NameSpace
OccName.varName (CommandLineOption -> CommandLineOption
forall a. [a] -> [a]
reverse CommandLineOption
n')
        m :: Module
m = if CommandLineOption -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null CommandLineOption
m' then 
              Module
md 
            else 
              Module
md {moduleName :: ModuleName
moduleName = CommandLineOption -> ModuleName
mkModuleName (CommandLineOption -> ModuleName)
-> CommandLineOption -> ModuleName
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> CommandLineOption
forall a. [a] -> [a]
reverse (Int -> CommandLineOption -> CommandLineOption
forall a. Int -> [a] -> [a]
drop 1 CommandLineOption
m')}



{-|
  Given a trivially unsat constraint @a@, @showTypeError a@ is the 
  message that we will print out to the user as an SDoc.
-}
showTypeError :: Atomic -> SDoc
showTypeError :: Atomic -> SDoc
showTypeError a :: Atomic
a =
    SDoc
blankLine 
      SDoc -> SDoc -> SDoc
$+$ (PprColour -> SDoc -> SDoc
coloured (PprColour
colBold PprColour -> PprColour -> PprColour
forall a. Semigroup a => a -> a -> a
Prelude.<> PprColour
colWhiteFg) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> Int -> SDoc -> SDoc
hang SDoc
topLine 2 (SDoc -> Int -> SDoc -> SDoc
hang SDoc
msgLine1 2 SDoc
msgLine2))
      SDoc -> SDoc -> SDoc
$+$ SDoc
blankLine
  where
    topLine :: SDoc
topLine = 
      (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SDoc) -> SrcSpan -> SDoc
forall a b. (a -> b) -> a -> b
$ Atomic -> SrcSpan
spanInfo Atomic
a) SDoc -> SDoc -> SDoc
GhcPlugins.<> SDoc
colon 
      SDoc -> SDoc -> SDoc
<+> PprColour -> SDoc -> SDoc
coloured (Scheme -> PprColour
sWarning Scheme
defaultScheme) (CommandLineOption -> SDoc
text "warning:")
      SDoc -> SDoc -> SDoc
<+> SDoc
lbrack SDoc -> SDoc -> SDoc
GhcPlugins.<> PprColour -> SDoc -> SDoc
coloured (Scheme -> PprColour
sWarning Scheme
defaultScheme) (CommandLineOption -> SDoc
text "Intensional") SDoc -> SDoc -> SDoc
GhcPlugins.<> SDoc
rbrack
    msgLine1 :: SDoc
msgLine1 = 
      CommandLineOption -> SDoc
text "Could not verify that" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (K 'L -> SDoc
forall a. Outputable a => a -> SDoc
ppr (K 'L -> SDoc) -> K 'L -> SDoc
forall a b. (a -> b) -> a -> b
$ Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a) 
        SDoc -> SDoc -> SDoc
<+> CommandLineOption -> SDoc
text "from" 
        SDoc -> SDoc -> SDoc
<+> (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SDoc) -> SrcSpan -> SDoc
forall a b. (a -> b) -> a -> b
$ K 'L -> SrcSpan
forall (a :: Side). K a -> SrcSpan
getLocation (Atomic -> K 'L
forall (l :: Side) (r :: Side). Constraint l r -> K l
left Atomic
a)) 
    msgLine2 :: SDoc
msgLine2 = CommandLineOption -> SDoc
text "cannot reach the incomplete match at"
        SDoc -> SDoc -> SDoc
<+> (SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SDoc) -> SrcSpan -> SDoc
forall a b. (a -> b) -> a -> b
$ K 'R -> SrcSpan
forall (a :: Side). K a -> SrcSpan
getLocation (Atomic -> K 'R
forall (l :: Side) (r :: Side). Constraint l r -> K r
right Atomic
a))

{-|
    Given a GHC interface tycon representation @iftc@,
    @tcIFaceTyCon iftc@ is the action that returns the original tycon.
-}
tcIfaceTyCon :: IfaceTyCon -> IfL TyCon
tcIfaceTyCon :: IfaceTyCon -> IOEnv (Env IfGblEnv IfLclEnv) TyCon
tcIfaceTyCon iftc :: IfaceTyCon
iftc = do
  Expr CoreBndr
e <- IfaceExpr -> IfL (Expr CoreBndr)
tcIfaceExpr (IfaceType -> IfaceExpr
IfaceType (IfaceTyCon -> IfaceAppArgs -> IfaceType
IfaceTyConApp IfaceTyCon
iftc IfaceAppArgs
IA_Nil))
  case Expr CoreBndr
e of
    Type (TyConApp tc :: TyCon
tc _) -> TyCon -> IOEnv (Env IfGblEnv IfLclEnv) TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
    _ -> CommandLineOption -> SDoc -> IOEnv (Env IfGblEnv IfLclEnv) TyCon
forall a. HasCallStack => CommandLineOption -> SDoc -> a
pprPanic "TyCon has been corrupted!" (Expr CoreBndr -> SDoc
forall a. Outputable a => a -> SDoc
ppr Expr CoreBndr
e)

data Benchmark = 
  Benchmark { 
      Benchmark -> [Integer]
times :: [Integer],
      Benchmark -> Integer
avg :: Integer,
      Benchmark -> Int
bigN :: Int,
      Benchmark -> Int
bigK :: Int,
      Benchmark -> Int
bigD :: Int,
      Benchmark -> Int
bigV :: Int,
      Benchmark -> Int
bigI :: Int
    }
  deriving ((forall x. Benchmark -> Rep Benchmark x)
-> (forall x. Rep Benchmark x -> Benchmark) -> Generic Benchmark
forall x. Rep Benchmark x -> Benchmark
forall x. Benchmark -> Rep Benchmark x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Benchmark x -> Benchmark
$cfrom :: forall x. Benchmark -> Rep Benchmark x
Generic)

instance ToJSON Benchmark
instance FromJSON Benchmark

{-|
    Given the name of a benchmark @n@ and a beginning @t0@ and end 
    time @t1@ and statistics @ss@ on the run, @recordBenchmarks n (t0, t1) ss@
    is the IO action that writes the benchmark data to a JSON file.
-}
recordBenchmarks :: String -> (Integer, Integer) -> Stats -> IO ()
recordBenchmarks :: CommandLineOption -> (Integer, Integer) -> Stats -> IO ()
recordBenchmarks name :: CommandLineOption
name (t0 :: Integer
t0, t1 :: Integer
t1) stats :: Stats
stats = do
  Bool
exist <- CommandLineOption -> IO Bool
doesFileExist "benchmark.json"
  if Bool
exist
    then
      CommandLineOption -> IO (Maybe (Map CommandLineOption Benchmark))
forall a. FromJSON a => CommandLineOption -> IO (Maybe a)
decodeFileStrict "benchmark.json" IO (Maybe (Map CommandLineOption Benchmark))
-> (Maybe (Map CommandLineOption Benchmark) -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Nothing ->
          CommandLineOption -> Map CommandLineOption Benchmark -> IO ()
forall a. ToJSON a => CommandLineOption -> a -> IO ()
encodeFile "benchmark.json" (CommandLineOption -> Benchmark -> Map CommandLineOption Benchmark
forall k a. k -> a -> Map k a
Map.singleton CommandLineOption
name Benchmark
new)
        Just bs :: Map CommandLineOption Benchmark
bs ->
          case CommandLineOption
-> Map CommandLineOption Benchmark -> Maybe Benchmark
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CommandLineOption
name Map CommandLineOption Benchmark
bs of
            Nothing ->
              CommandLineOption -> Map CommandLineOption Benchmark -> IO ()
forall a. ToJSON a => CommandLineOption -> a -> IO ()
encodeFile "benchmark.json" (CommandLineOption
-> Benchmark
-> Map CommandLineOption Benchmark
-> Map CommandLineOption Benchmark
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CommandLineOption
name Benchmark
new Map CommandLineOption Benchmark
bs)
            Just bench :: Benchmark
bench -> do
              let bench' :: Benchmark
bench' = Benchmark -> Benchmark
updateAverage (Benchmark -> Benchmark) -> Benchmark -> Benchmark
forall a b. (a -> b) -> a -> b
$ Benchmark
bench {times :: [Integer]
times = (Integer
t1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
t0) Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: Benchmark -> [Integer]
times Benchmark
bench}
              CommandLineOption -> Map CommandLineOption Benchmark -> IO ()
forall a. ToJSON a => CommandLineOption -> a -> IO ()
encodeFile "benchmark.json" (CommandLineOption
-> Benchmark
-> Map CommandLineOption Benchmark
-> Map CommandLineOption Benchmark
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CommandLineOption
name Benchmark
bench' Map CommandLineOption Benchmark
bs)
    else CommandLineOption -> Map CommandLineOption Benchmark -> IO ()
forall a. ToJSON a => CommandLineOption -> a -> IO ()
encodeFile "benchmark.json" (CommandLineOption -> Benchmark -> Map CommandLineOption Benchmark
forall k a. k -> a -> Map k a
Map.singleton CommandLineOption
name Benchmark
new)
  where
    updateAverage :: Benchmark -> Benchmark
updateAverage b :: Benchmark
b =
      Benchmark
b {avg :: Integer
avg = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Benchmark -> [Integer]
times Benchmark
b) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Int -> Integer
forall a. Integral a => a -> Integer
toInteger ([Integer] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Benchmark -> [Integer]
times Benchmark
b))}
    new :: Benchmark
new =
      Benchmark :: [Integer]
-> Integer -> Int -> Int -> Int -> Int -> Int -> Benchmark
Benchmark
        { 
          bigN :: Int
bigN = Stats -> Int
getN Stats
stats,
          bigD :: Int
bigD = Stats -> Int
getD Stats
stats,
          bigV :: Int
bigV = Stats -> Int
getV Stats
stats,
          bigK :: Int
bigK = Stats -> Int
getK Stats
stats,
          bigI :: Int
bigI = Stats -> Int
getI Stats
stats,
          times :: [Integer]
times = [Integer
t1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
t0],
          avg :: Integer
avg = Integer
t1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
t0
        }