{-# LANGUAGE ApplicativeDo #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} import Control.Monad.IRTree qualified as IRTree import ReduceC import Colog import Control.Applicative import Control.Monad import Control.Monad.IRTree qualified as RPath import Control.Monad.State import Data.Foldable import Data.Functor import Data.Text qualified as Text import Data.Time (getCurrentTime) import Data.Time qualified as Time 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 time <- getCurrentTime let fmt m = do t' <- getCurrentTime pure ( Text.pack ( Time.formatTime Time.defaultTimeLocale "%_3m:%04ES " (t' `Time.diffUTCTime` time) ) <> fmtMessage m ) usingLoggerT (filterBySeverity Info msgSeverity $ 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 l c = process D "Checking predictate" do when debug do pPrint (void c) when pedandic do liftIO $ copyFile f (f <.> "last") logDebug (Text.pack . show $ RPath.fromChoiceList $ map fst l) output f c v <- validiate f res <- if v then test f else do logWarning "Produced invalid code" liftIO $ copyFile f (f <.> "fail") when pedandic do cleanup f pure False logInfo ("Predicate was " <> Text.pack (show res)) pure res 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 IRTree.reduceExp else IRTree.reduce) (check' file) (ReduceC.defaultReduceC 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