Main.hs

{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}

import Control.RTree
import Data.Valuation qualified as Val

import ReduceC

import Colog
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.Trans
import Data.Bool (bool)
import Data.Foldable
import Data.Functor
import Data.List (intercalate)
import Data.Map.Strict qualified as Map
import Data.Text qualified as Text
import Data.Time (getCurrentTime)
import Data.Time qualified as Time
import Data.Vector qualified as V
import GHC.Stack
import Language.C qualified as C
import Options.Applicative
import System.Directory
import System.Exit
import System.FilePath
import System.IO
import System.Process.Typed
import Text.Pretty.Simple
import Text.PrettyPrint qualified as P
import Prelude hiding (log)

main :: IO ()
main =
  join
    . execParser
    $ info (run <**> helper)
    . fold
    $ []

process :: (WithLog env (Msg sev) m, MonadIO m) => sev -> Text.Text -> m a -> m a
process sev p ma = do
  msg "Started "
  a <- ma
  msg "Done "
  pure a
 where
  s = withFrozenCallStack callStack
  msg t = Colog.logMsg (Msg sev s (t <> p))

run :: (HasCallStack) => Parser (IO ())
run = do
  expmode <-
    flag False True
      $ fold
        [ long "exp"
        , help "run in exponential mode"
        ]

  checkmode <-
    flag False True
      $ fold
        [ long "dry-run"
        , short 'n'
        , help "don't do any reduction"
        ]

  validity <-
    optional
      $ strOption
      $ fold
        [ long "validity"
        , short 'v'
        , help "check every output for validity"
        ]

  pedandic <-
    flag False True
      $ fold
        [ long "pedandic"
        , short 'P'
        , help "when checking for validity, throw error if command fails"
        ]
  debug <-
    flag False True
      $ fold
        [ long "debug"
        , help "enable debugging"
        ]

  cmd <- strArgument $ fold [metavar "COMMAND"]

  file <- strArgument $ fold [metavar "FILE"]

  pure do
    t <- getCurrentTime
    let
      fmt m = do
        t' <- getCurrentTime
        pure
          ( Text.pack
              ( Time.formatTime
                  Time.defaultTimeLocale
                  "%_3m:%04ES "
                  (t' `Time.diffUTCTime` t)
              )
              <> fmtMessage m
          )

    usingLoggerT (cmapM fmt logTextStderr) do
      let
        test f = process D ("test " <> Text.pack f) do
          err <- liftIO $ runProcess cmd
          log D (Text.pack $ show err)
          pure (err == ExitSuccess)

        validiate f = case validity of
          Just vcmd -> process D ("validiate " <> Text.pack f) do
            err <- liftIO $ runProcess vcmd
            log D (Text.pack $ show err)
            pure (err == ExitSuccess)
          Nothing -> pure True

        output f c = process D ("writing " <> Text.pack f) do
          let x = P.render (C.pretty (c $> C.undefNode))
          liftIO $ writeFile f x

        cleanup f = do
          logError "Cleaning up"
          liftIO do
            copyFile (f <.> "bak") f
            removeFile (f <.> "bak")
          liftIO exitFailure

        check' f (ReState ch i val) mc = process I "Checking predictate" do
          logDebug . Text.pack $ map (\j -> maybe '*' (bool '0' '1') (ch V.!? j)) [0 .. i]
          logDebug
            . Text.pack
            $ intercalate
              ", "
              [C.identToString k | (k, v) <- Val.toPairs val, v]
          logDebug
            . Text.pack
            $ intercalate
              ", "
              ["!" <> C.identToString k | (k, v) <- Val.toPairs val, not v]
          case mc of
            Nothing -> do
              logDebug "Empty input"
              pure False
            Just c -> do
              when debug do
                pPrint (void c)
              when pedandic do
                liftIO $ copyFile f (f <.> "last")
              output f c
              v <- validiate f
              if v
                then test f
                else do
                  logWarning "Produced invalid code"
                  when pedandic do
                    liftIO $ copyFile f (f <.> "fail")
                    cleanup f
                  pure False

      let bak = file <.> "bak"

      process D "backing up file" do
        liftIO $ copyFile file bak

      process I "validiating" do
        v <- validiate file
        unless v do
          logError "did not validiate program"
          liftIO exitFailure

      process I "check predicate" do
        t <- test file
        unless t do
          logError "did not satisify predicate"
          liftIO exitFailure

      c <- process D "parsing file" do
        parseCFile file

      when debug do
        pPrint (void c)

      output file c

      process I "sanity checks" do
        c' <- parseCFile file
        unless (void c' == void c) do
          liftIO do
            withFile "error.1.hs" WriteMode (`pHPrint` void c)
            withFile "error.2.hs" WriteMode (`pHPrint` void c')
          logError "Outputted a different file than I read... Please report original file and error.{1,2}.hs"
          liftIO exitFailure

        t <- test file
        unless t do
          logError "file did not satisfy predicate"
          cleanup file

      when checkmode do
        liftIO exitSuccess

      l <-
        (if expmode then ireduceExpT (`evalStateT` Map.empty) else ireduceT (`evalStateT` Map.empty))
          (check' file)
          (Val.singleton (Val.is $ C.internalIdent "main"))
          (ReduceC.reduceC c)

      when pedandic do
        liftIO $ copyFile file (file <.> "last")

      case l of
        Just l' ->
          output file l'
        Nothing -> do
          logError "Was unable to produce any output"
          cleanup file
 where
  parseCFile file = do
    res <- liftIO $ C.parseCFilePre file
    case res of
      Right c -> pure c
      Left err -> do
        logError (Text.pack (show err))
        liftIO exitFailure