{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
module Embedder.ModCache
      ( runCache
      , LoadPath
      , getModule
      ) where

import Embedder.Config (Config, verbose, dump, pDebug, getEmbedFile)
import Embedder.HSE.Desugar (desugar)
import qualified Embedder.Atmo.Syntax as A (Module (..))
import qualified Embedder.Atmo.ToIsabelle as AtmoIsabelle
import Embedder.HSE.ToAtmo (toAtmo)
import Language.Haskell.Exts.SrcLoc (SrcSpanInfo)
import ReWire.Error (AstError, MonadError)
import ReWire.HSE.Annotate (annotate)
import ReWire.HSE.Cache (LoadPath, getModuleWith)
import ReWire.HSE.Rename (Exports, Renamer, fixFixity)
import ReWire.HSE.PassInfo (printInfoTop, printInfoHSE)
import ReWire.Pretty (Pretty (..), prettyPrint, fastPrint)

import Control.Lens ((^.))
import Control.Monad ((>=>))
import Control.Monad.IO.Class (liftIO, MonadIO)
import Control.Monad.State.Strict (MonadState, lift)
import Data.Foldable (forM_)
import Data.Text (Text, pack)
import Numeric.Natural (Natural)
import System.FilePath (takeBaseName)

import qualified Data.Text.IO                 as T
import qualified Language.Haskell.Exts.Syntax as S (Module (..))
import qualified ReWire.HSE.Cache             as Cache
import qualified Embedder.Config              as C

type Cache m = Cache.Cache A.Module m

runCache :: (MonadIO m, MonadError AstError m) => Cache m a -> m a
runCache :: forall (m :: * -> *) a.
(MonadIO m, MonadError AstError m) =>
Cache m a -> m a
runCache = Cache Module m a -> m a
forall (m :: * -> *) mod a. Monad m => Cache mod m a -> m a
Cache.runCache

getModule :: (MonadIO m, MonadFail m, MonadError AstError m, MonadState AstError m) => Config -> FilePath -> FilePath -> Cache m (A.Module, Exports)
getModule :: forall (m :: * -> *).
(MonadIO m, MonadFail m, MonadError AstError m,
 MonadState AstError m) =>
Config -> FilePath -> FilePath -> Cache m (Module, Exports)
getModule Config
conf = (FilePath
 -> Renamer
 -> Module
 -> Module SrcSpanInfo
 -> Cache Module m (Module, Exports))
-> Config
-> FilePath
-> FilePath
-> Cache Module m (Module, Exports)
forall mod (m :: * -> *).
(MonadIO m, MonadError AstError m, Monoid mod) =>
(FilePath
 -> Renamer
 -> mod
 -> Module SrcSpanInfo
 -> Cache mod m (mod, Exports))
-> Config -> FilePath -> FilePath -> Cache mod m (mod, Exports)
getModuleWith FilePath
-> Renamer
-> Module
-> Module SrcSpanInfo
-> Cache Module m (Module, Exports)
forall (m :: * -> *).
(MonadIO m, MonadFail m, MonadError AstError m,
 MonadState AstError m) =>
FilePath
-> Renamer
-> Module
-> Module SrcSpanInfo
-> Cache m (Module, Exports)
translate Config
conf
      where translate :: (MonadIO m, MonadFail m, MonadError AstError m, MonadState AstError m) => FilePath -> Renamer -> A.Module -> S.Module SrcSpanInfo -> Cache m (A.Module, Exports)
            translate :: forall (m :: * -> *).
(MonadIO m, MonadFail m, MonadError AstError m,
 MonadState AstError m) =>
FilePath
-> Renamer
-> Module
-> Module SrcSpanInfo
-> Cache m (Module, Exports)
translate FilePath
fp Renamer
rn Module
imps Module SrcSpanInfo
m = do
                  let filename :: FilePath
filename = FilePath -> FilePath
takeBaseName FilePath
fp

                      pDebug' :: MonadIO m => Text -> a -> m a
                      pDebug' :: forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
s a
a = Config -> Text -> m ()
forall (m :: * -> *). MonadIO m => Config -> Text -> m ()
pDebug Config
conf (FilePath -> Text
pack FilePath
fp Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s) m () -> m a -> m a
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

                      whenDump :: Applicative m => Natural -> (Bool -> a -> m a) -> a -> m a
                      whenDump :: forall (m :: * -> *) a.
Applicative m =>
Natural -> (Bool -> a -> m a) -> a -> m a
whenDump Natural
n Bool -> a -> m a
f = if (Config
confConfig
-> Getting (Natural -> Bool) Config (Natural -> Bool)
-> Natural
-> Bool
forall s a. s -> Getting a s a -> a
^.Getting (Natural -> Bool) Config (Natural -> Bool)
Lens' Config (Natural -> Bool)
dump) Natural
n then Bool -> a -> m a
f (Bool -> a -> m a) -> Bool -> a -> m a
forall a b. (a -> b) -> a -> b
$ Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
verbose else a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

                  -- The haskell-src-exts passes, then the translation to Atmo
                  -- and the embedding into Isabelle.
                  (m', exps) <- Module SrcSpanInfo
-> StateT
     (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo)
forall a. a -> StateT (HashMap FilePath (Module, Exports)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                            (Module SrcSpanInfo
 -> StateT
      (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo))
-> (Module SrcSpanInfo
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module SrcSpanInfo
-> StateT
     (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"Fixing fixity."
                            (Module SrcSpanInfo
 -> StateT
      (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo))
-> (Module SrcSpanInfo
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> m (Module SrcSpanInfo)
-> StateT
     (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (HashMap FilePath (Module, Exports)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Module SrcSpanInfo)
 -> StateT
      (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo))
-> (Module SrcSpanInfo -> m (Module SrcSpanInfo))
-> Module SrcSpanInfo
-> StateT
     (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Renamer -> Module SrcSpanInfo -> m (Module SrcSpanInfo)
forall (m :: * -> *).
(MonadFail m, MonadState AstError m) =>
Renamer -> Module SrcSpanInfo -> m (Module SrcSpanInfo)
fixFixity Renamer
rn
                            (Module SrcSpanInfo
 -> StateT
      (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo))
-> (Module SrcSpanInfo
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module SrcSpanInfo
-> StateT
     (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"Annotating."
                            (Module SrcSpanInfo
 -> StateT
      (HashMap FilePath (Module, Exports)) m (Module SrcSpanInfo))
-> (Module SrcSpanInfo
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall a. a -> StateT (HashMap FilePath (Module, Exports)) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module SrcSpanInfo -> Module Annote)
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module SrcSpanInfo -> Module Annote
annotate
                            (Module SrcSpanInfo
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"[Pass 1] Pre-desugaring."
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Natural
-> (Bool
    -> Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a.
Applicative m =>
Natural -> (Bool -> a -> m a) -> a -> m a
whenDump Natural
1 (Text
-> Renamer
-> Text
-> Bool
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a.
MonadIO m =>
Text -> Renamer -> Text -> Bool -> Module a -> m (Module a)
printInfoHSE Text
"[Pass 1] Haskell: Pre-desugaring" Renamer
rn (Module -> Text
showtImps Module
imps))
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"HSE Desugaring."
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Renamer
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *).
MonadError AstError m =>
Renamer -> Module Annote -> m (Module Annote)
desugar Renamer
rn
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"[Pass 2] Post-desugaring."
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Natural
-> (Bool
    -> Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a.
Applicative m =>
Natural -> (Bool -> a -> m a) -> a -> m a
whenDump Natural
2 (Text
-> Renamer
-> Text
-> Bool
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a.
MonadIO m =>
Text -> Renamer -> Text -> Bool -> Module a -> m (Module a)
printInfoHSE Text
"[Pass 2] Haskell: Post-desugaring" Renamer
rn (Module -> Text
showtImps Module
imps))
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module Annote)
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
pDebug' Text
"[Pass 3] Translating to atmo."
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module Annote))
-> (Module Annote
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Renamer
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *).
MonadError AstError m =>
Renamer -> Module Annote -> m (Module, Exports)
toAtmo Renamer
rn
                            (Module Annote
 -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> ((Module, Exports)
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module Annote
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Natural
-> (Bool
    -> (Module, Exports)
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> (Module, Exports)
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a.
Applicative m =>
Natural -> (Bool -> a -> m a) -> a -> m a
whenDump Natural
3 (Text
-> Renamer
-> Module
-> Bool
-> (Module, Exports)
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *).
MonadIO m =>
Text
-> Renamer
-> Module
-> Bool
-> (Module, Exports)
-> m (Module, Exports)
printInfoAtmo Text
"[Pass 3] Atmo: Pre-embedding" Renamer
rn Module
imps)
                            ((Module, Exports)
 -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> ((Module, Exports)
    -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> (Module, Exports)
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> FilePath
-> (Module, Exports)
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
FilePath -> (Module, Exports) -> m (Module, Exports)
embedAtmo (Config -> FilePath -> FilePath
getEmbedFile Config
conf FilePath
filename)
                            (Module SrcSpanInfo
 -> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports))
-> Module SrcSpanInfo
-> StateT (HashMap FilePath (Module, Exports)) m (Module, Exports)
forall a b. (a -> b) -> a -> b
$ Module SrcSpanInfo
m

                  pure (m' <> imps, exps)

            embedAtmo :: (MonadError AstError m, MonadIO m) => FilePath -> (A.Module, Exports) -> m (A.Module, Exports)
            embedAtmo :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
FilePath -> (Module, Exports) -> m (Module, Exports)
embedAtmo FilePath
fout (Module
m, Exports
es) = do
                  a' <- FilePath -> Module -> m (Maybe Theory)
forall (m :: * -> *).
MonadError AstError m =>
FilePath -> Module -> m (Maybe Theory)
AtmoIsabelle.embedModule FilePath
fout Module
m
                  forM_ a' (embedAST fout)
                  pure (m, es)

            embedAST :: (MonadIO m, Pretty a) => FilePath -> a -> m ()
            embedAST :: forall (m :: * -> *) a.
(MonadIO m, Pretty a) =>
FilePath -> a -> m ()
embedAST FilePath
fout a
a =
                  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Text -> IO ()
T.writeFile FilePath
fout (if Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
C.pretty then a -> Text
forall a. Pretty a => a -> Text
prettyPrint a
a else a -> Text
forall a. Pretty a => a -> Text
fastPrint a
a)

-- | Derived Show rather than TextShow: generic TextShow instances for the
--   Atmo syntax types cost minutes of compile time, and the derived-Show
--   output is identical.
showtImps :: A.Module -> Text
showtImps :: Module -> Text
showtImps = FilePath -> Text
pack (FilePath -> Text) -> (Module -> FilePath) -> Module -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> FilePath
forall a. Show a => a -> FilePath
show

printInfoAtmo :: MonadIO m => Text -> Renamer -> A.Module -> Bool -> (A.Module, Exports) -> m (A.Module, Exports)
printInfoAtmo :: forall (m :: * -> *).
MonadIO m =>
Text
-> Renamer
-> Module
-> Bool
-> (Module, Exports)
-> m (Module, Exports)
printInfoAtmo Text
hd Renamer
rn Module
imps Bool
verbose (Module, Exports)
m = do
      Text -> Renamer -> Text -> Bool -> Text -> m ()
forall (m :: * -> *).
MonadIO m =>
Text -> Renamer -> Text -> Bool -> Text -> m ()
printInfoTop Text
hd Renamer
rn (Module -> Text
showtImps Module
imps) Bool
verbose (FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ (Module, Exports) -> FilePath
forall a. Show a => a -> FilePath
show (Module, Exports)
m)
      IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
T.putStrLn (Text -> IO ()) -> Text -> IO ()
forall a b. (a -> b) -> a -> b
$ Module -> Text
forall a. Pretty a => a -> Text
prettyPrint (Module -> Text) -> Module -> Text
forall a b. (a -> b) -> a -> b
$ (Module, Exports) -> Module
forall a b. (a, b) -> a
fst (Module, Exports)
m
      (Module, Exports) -> m (Module, Exports)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Module, Exports)
m