{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Trustworthy #-}
module ReWire.ModCache
      ( getDevice
      , LoadPath
      ) where

import ReWire.Config (Config)
import ReWire.Eidos.ToSynolon (purify)
import ReWire.GHC.Session (loadCore)
import ReWire.GHC.ToEidos (toEidos)
import ReWire.Error (AstError, MonadError, Warning (..), failAt, warnAt)
import ReWire.Pass (pass, verb')
import ReWire.Pretty (prettyPrint)
import ReWire.Synolon.ToHyle (synolonToHyle)

import Control.Lens ((^.))
import Control.Monad (when, (>=>))
import Control.Monad.IO.Class (liftIO, MonadIO)
import Control.Monad.State.Strict (MonadState)
import Data.Text (Text, pack)
import Numeric.Natural (Natural)
import System.Directory (renameFile)

import qualified Data.Text.IO                 as T
import qualified ReWire.Eidos.ANF             as Eidos
import qualified ReWire.Eidos.Externs         as Eidos
import qualified ReWire.Eidos.Inline          as Eidos
import qualified ReWire.Eidos.Lint            as Eidos
import qualified ReWire.Eidos.Pretty          as Eidos
import qualified ReWire.Eidos.Simplify        as Eidos
import qualified ReWire.Eidos.Spec            as Eidos
import qualified ReWire.Eidos.Syntax          as Eidos
import qualified ReWire.Synolon.Lint          as Synolon
import qualified ReWire.Synolon.Pretty        as Synolon
import qualified ReWire.Synolon.Syntax        as Synolon
import qualified ReWire.Synolon.Transform     as Synolon
import qualified ReWire.Hyle.Syntax           as Hyle
import qualified ReWire.Config                as C

type LoadPath = [FilePath]

-- | The numbered pass pipeline: run rwc -v to see the bracketed pass numbers;
--   -d N (or --dump-all) dumps the IR after pass N to a file beside the
--   output (e.g., MiniISA.6.eir, MiniISA.8.syn). Pass 1 is the front end: GHC
--   (parse\/typecheck\/desugar over the whole home module graph) followed by
--   the Core-to-Eidos bridge. Passes 2-6 are the Eidos passes (doc/eidos.md),
--   pass 7 is purification (Eidos to Synolon), pass 8 the Synolon
--   block-graph cleanup, and pass 9 the Synolon-to-Hyle fold; the Hyle-level
--   passes (10-11) run in ReWire.FrontEnd, numbered after these so -d
--   numbering is uniform.
getDevice :: (MonadIO m, MonadFail m, MonadError AstError m, MonadState AstError m) => Config -> FilePath -> m Hyle.Program
getDevice :: forall (m :: * -> *).
(MonadIO m, MonadFail m, MonadError AstError m,
 MonadState AstError m) =>
Config -> FilePath -> m Program
getDevice Config
conf FilePath
fp = do
      eir <- Natural -> Text -> (FilePath -> m Program) -> FilePath -> m Program
forall (n :: * -> *) a.
MonadIO n =>
Natural -> Text -> (a -> n Program) -> a -> n Program
passEidos Natural
1 Text
"GHC front end and Core-to-Eidos bridge."
            (Config -> FilePath -> m [ModGuts]
forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
Config -> FilePath -> m [ModGuts]
loadCore Config
conf (FilePath -> m [ModGuts])
-> ([ModGuts] -> m Program) -> FilePath -> m Program
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Config -> [ModGuts] -> m Program
forall (m :: * -> *).
MonadError AstError m =>
Config -> [ModGuts] -> m Program
toEidos Config
conf) FilePath
fp
      Eidos.lint Eidos.LintPoly eir
      -- The Eidos passes: specialize away
      -- polymorphism, inline INLINE-annotated definitions, neuter externs
      -- (before the partial evaluator, always), and partially evaluate to
      -- the synthable/dictionary-free fixpoint. The standing lints run
      -- between passes (poly mode after the bridge, then mono mode);
      -- --debug-lint adds a lint after the remaining Eidos passes.
      eirSpec <- passEidos 2 "Specializing polymorphic definitions (eidos)."
            (Eidos.specialize specDepth) eir
      lintDebug Eidos.LintMono eirSpec
      eirInl <- passEidos 3 "Inlining INLINE-annotated definitions (eidos)."
            Eidos.inlineAnnotated eirSpec
      Eidos.lint Eidos.LintMono eirInl
      eirExt <- passEidos 4 "Extracting extern models (eidos)."
            neuterExterns eirInl
      lintDebug Eidos.LintMono eirExt
      eirPE <- passEidos 5 "Partial evaluation (eidos)."
            (Eidos.simplify (conf^.C.depth)) eirExt
      Eidos.lint Eidos.LintMono eirPE
      -- Normalize the reactive fragment to ANF (the last Eidos pass; the
      -- --eidos dump is this program), then the machine level: purify to
      -- Synolon, clean the block graph, and check the machine rules.
      eirANF <- passEidos 6 "Normalizing to ANF (eidos)."
            Eidos.normalize eirPE
      Eidos.lint Eidos.LintMonoANF eirANF
      when (conf^.C.eidos) $ writeDump (C.eidosFile conf fp) "Eidos" $ Eidos.prettyProgram eirANF
      pr0 <- passSynolon 7 "Purifying (eidos to synolon)."
            purify eirANF
      -- The lint before the cleanup skips signal-guardedness, the one rule
      -- the cleanup may establish (it removes orphaned blocks).
      when (conf^.C.debugLint) $ Synolon.lintPre pr0
      pr <- passSynolon 8 "Cleaning the machine block graph (synolon)."
            (pure . optimizeProcs) pr0
      Synolon.lint pr
      mapM_ (flip verb () . Synolon.machineSummary) $ Synolon.progProcs pr
      -- The strict reachable-halt check (--no-halt): every block is
      -- reachable after the block-graph cleanup, so any halt terminator
      -- is a state the device can actually freeze in.
      when (conf^.C.noHalt) $ mapM_ noHaltCheck $ Synolon.progProcs pr
      -- --certify validates against exactly this dump (the Synolon program
      -- the fold consumes), so it implies --synolon.
      when (conf^.C.synolon || conf^.C.certify /= C.CertifyOff)
            $ writeDump (C.synolonFile conf fp) "Synolon" $ Synolon.prettyProgram pr
      -- The fold owns the lowering: Synolon straight to Hyle
      -- (ReWire.Synolon.ToHyle).
      pass conf fp 9 "Translating to Hyle." "rwc" prettyPrint (synolonToHyle conf) pr

      where passEidos :: MonadIO n => Natural -> Text -> (a -> n Eidos.Program) -> a -> n Eidos.Program
            passEidos :: forall (n :: * -> *) a.
MonadIO n =>
Natural -> Text -> (a -> n Program) -> a -> n Program
passEidos Natural
n Text
name = Config
-> FilePath
-> Natural
-> Text
-> FilePath
-> (Program -> Text)
-> (a -> n Program)
-> a
-> n Program
forall (m :: * -> *) a b.
(MonadIO m, Data b, Show b) =>
Config
-> FilePath
-> Natural
-> Text
-> FilePath
-> (b -> Text)
-> (a -> m b)
-> a
-> m b
pass Config
conf FilePath
fp Natural
n Text
name FilePath
"eir" Program -> Text
Eidos.prettyProgram

            passSynolon :: MonadIO n => Natural -> Text -> (a -> n Synolon.Program) -> a -> n Synolon.Program
            passSynolon :: forall (n :: * -> *) a.
MonadIO n =>
Natural -> Text -> (a -> n Program) -> a -> n Program
passSynolon Natural
n Text
name = Config
-> FilePath
-> Natural
-> Text
-> FilePath
-> (Program -> Text)
-> (a -> n Program)
-> a
-> n Program
forall (m :: * -> *) a b.
(MonadIO m, Data b, Show b) =>
Config
-> FilePath
-> Natural
-> Text
-> FilePath
-> (b -> Text)
-> (a -> m b)
-> a
-> m b
pass Config
conf FilePath
fp Natural
n Text
name FilePath
"syn" Program -> Text
Synolon.prettyProgram

            -- An IR dump beside the output, published by a same-directory
            -- temporary plus rename, so a crash can't leave a torn artifact
            -- that later validates or replays.
            writeDump :: MonadIO n => FilePath -> Text -> Text -> n ()
            writeDump :: forall (n :: * -> *). MonadIO n => FilePath -> Text -> Text -> n ()
writeDump FilePath
file Text
what Text
txt = do
                  Text -> () -> n ()
forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
verb (Text
"Writing " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
what Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" IR to file: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FilePath -> Text
pack FilePath
file) ()
                  IO () -> n ()
forall a. IO a -> n a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> n ()) -> IO () -> n ()
forall a b. (a -> b) -> a -> b
$ do
                        FilePath -> Text -> IO ()
T.writeFile (FilePath
file FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
".tmp") Text
txt
                        FilePath -> FilePath -> IO ()
renameFile (FilePath
file FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
".tmp") FilePath
file

            neuterExterns :: (MonadError AstError m', MonadIO m') => Eidos.Program -> m' Eidos.Program
            neuterExterns :: forall (m' :: * -> *).
(MonadError AstError m', MonadIO m') =>
Program -> m' Program
neuterExterns Program
p = do
                  (p', ws) <- Program -> m' (Program, [Warning])
forall (m :: * -> *).
MonadError AstError m =>
Program -> m (Program, [Warning])
Eidos.neuterExterns Program
p
                  mapM_ (\ (Warning Annote
a Text
m') -> Config -> Annote -> Text -> m' ()
forall (m :: * -> *) an.
(MonadError AstError m, MonadIO m, Annotation an) =>
Config -> an -> Text -> m ()
warnAt Config
conf Annote
a Text
m') ws
                  pure p'

            optimizeProcs :: Synolon.Program -> Synolon.Program
            optimizeProcs :: Program -> Program
optimizeProcs Program
p = Program
p { Synolon.progProcs = map Synolon.optimizeProc $ Synolon.progProcs p }

            -- The bound on the type-specialization fixpoint: at least the
            -- historical bound of 10; --depth raises it (e.g. for deep
            -- dictionary chains).
            specDepth :: Natural
            specDepth :: Natural
specDepth = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max Natural
10 (Natural -> Natural) -> Natural -> Natural
forall a b. (a -> b) -> a -> b
$ Config
confConfig -> Getting Natural Config Natural -> Natural
forall s a. s -> Getting a s a -> a
^.Getting Natural Config Natural
Lens' Config Natural
C.depth

            noHaltCheck :: MonadError AstError m => Synolon.Proc -> m ()
            noHaltCheck :: forall (m :: * -> *). MonadError AstError m => Proc -> m ()
noHaltCheck Proc
p = case (Block -> [Annote]) -> [Block] -> [Annote]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Term -> [Annote]
Synolon.haltSites (Term -> [Annote]) -> (Block -> Term) -> Block -> [Annote]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> Term
Synolon.blkTerm) ([Block] -> [Annote]) -> [Block] -> [Annote]
forall a b. (a -> b) -> a -> b
$ Proc -> [Block]
Synolon.allBlocks Proc
p of
                  Annote
an : [Annote]
_ -> Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m ()) -> Text -> m ()
forall a b. (a -> b) -> a -> b
$ Text
"process " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Proc -> Text
Synolon.procName Proc
p
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" can halt, and post-halt outputs are unspecified (rejected by --no-halt)."
                  []     -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

            -- The standing lints (post-bridge, post-inline, post-PE,
            -- post-ANF) run always; --debug-lint re-lints after the
            -- remaining Eidos passes too.
            lintDebug :: MonadError AstError m => Eidos.LintMode -> Eidos.Program -> m ()
            lintDebug :: forall (m :: * -> *).
MonadError AstError m =>
LintMode -> Program -> m ()
lintDebug LintMode
mode Program
p | Config
confConfig -> Getting Bool Config Bool -> Bool
forall s a. s -> Getting a s a -> a
^.Getting Bool Config Bool
Lens' Config Bool
C.debugLint = LintMode -> Program -> m ()
forall (m :: * -> *).
MonadError AstError m =>
LintMode -> Program -> m ()
Eidos.lint LintMode
mode Program
p
                             | Bool
otherwise         = () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

            verb :: MonadIO m => Text -> a -> m a
            verb :: forall (m :: * -> *) a. MonadIO m => Text -> a -> m a
verb = Config -> Text -> a -> m a
forall (m :: * -> *) a. MonadIO m => Config -> Text -> a -> m a
verb' Config
conf