Skip to content
Snippets Groups Projects
Main.hs 5.18 KiB
Newer Older
  • Learn to ignore specific revisions
  • chrg's avatar
    chrg committed
    {-# LANGUAGE ApplicativeDo #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE DerivingVia #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE FlexibleContexts #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE ImportQualifiedPost #-}
    
    chrg's avatar
    chrg committed
    {-# LANGUAGE OverloadedStrings #-}
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
    import Control.Monad.IRTree qualified as IRTree
    
    chrg's avatar
    chrg committed
    import ReduceC
    
    
    chrg's avatar
    chrg committed
    import Colog
    import Control.Applicative
    import Control.Monad
    
    import Control.Monad.State
    
    chrg's avatar
    chrg committed
    import Data.Foldable
    import Data.Functor
    
    chrg's avatar
    chrg committed
    import Data.Text qualified as Text
    
    import Data.Time (getCurrentTime)
    import Data.Time qualified as Time
    
    chrg's avatar
    chrg committed
    import GHC.Stack
    
    chrg's avatar
    chrg committed
    import Language.C qualified as C
    
    chrg's avatar
    chrg committed
    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)
    
    chrg's avatar
    chrg committed
    
    main :: IO ()
    
    chrg's avatar
    chrg committed
    main =
      join
        . execParser
    
    chrg's avatar
    chrg committed
        $ info (run <**> helper)
    
    chrg's avatar
    chrg committed
          . fold
    
    chrg's avatar
    chrg committed
        $ []
    
    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
    
    chrg's avatar
    chrg committed
     where
    
    chrg's avatar
    chrg committed
      s = withFrozenCallStack callStack
      msg t = Colog.logMsg (Msg sev s (t <> p))
    
    run :: (HasCallStack) => Parser (IO ())
    run = do
    
    chrg's avatar
    chrg committed
      expmode <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
    chrg's avatar
    chrg committed
            [ long "exp"
            , help "run in exponential mode"
            ]
    
    chrg's avatar
    chrg committed
    
    
      checkmode <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
            [ long "dry-run"
            , short 'n'
            , help "don't do any reduction"
            ]
    
    
    chrg's avatar
    chrg committed
      validity <-
    
    chrg's avatar
    chrg committed
        optional $
          strOption $
            fold
              [ long "validity"
              , short 'v'
              , help "check every output for validity"
              ]
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
      pedandic <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
    chrg's avatar
    chrg committed
            [ long "pedandic"
            , short 'P'
            , help "when checking for validity, throw error if command fails"
    
    chrg's avatar
    chrg committed
            ]
    
    chrg's avatar
    chrg committed
      debug <-
    
    chrg's avatar
    chrg committed
        flag False True $
          fold
    
    chrg's avatar
    chrg committed
            [ long "debug"
            , help "enable debugging"
            ]
    
      cmd <- strArgument $ fold [metavar "COMMAND"]
    
      file <- strArgument $ fold [metavar "FILE"]
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
        time <- getCurrentTime
    
        let
          fmt m = do
            t' <- getCurrentTime
            pure
              ( Text.pack
                  ( Time.formatTime
                      Time.defaultTimeLocale
                      "%_3m:%04ES "
    
    chrg's avatar
    chrg committed
                      (t' `Time.diffUTCTime` time)
    
                  )
                  <> fmtMessage m
              )
    
        usingLoggerT (cmapM fmt logTextStderr) do
    
    chrg's avatar
    chrg committed
          let
            test f = process D ("test " <> Text.pack f) do
    
    chrg's avatar
    chrg committed
              err <- liftIO $ runProcess cmd
    
    chrg's avatar
    chrg committed
              log D (Text.pack $ show err)
              pure (err == ExitSuccess)
    
    
    chrg's avatar
    chrg committed
            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
    
    
    chrg's avatar
    chrg committed
            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
    
    
    chrg's avatar
    chrg committed
            check' f _ c = process I "Checking predictate" 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
    
    chrg's avatar
    chrg committed
                    liftIO $ copyFile f (f <.> "fail")
                    cleanup f
                  pure False
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
          let bak = file <.> "bak"
    
          process D "backing up file" do
            liftIO $ copyFile file bak
    
    
    chrg's avatar
    chrg committed
          process I "validiating" do
            v <- validiate file
            unless v do
              logError "did not validiate program"
              liftIO exitFailure
    
    
    chrg's avatar
    chrg committed
          process I "check predicate" do
            t <- test file
            unless t do
    
    chrg's avatar
    chrg committed
              logError "did not satisify predicate"
    
    chrg's avatar
    chrg committed
              liftIO exitFailure
    
          c <- process D "parsing file" do
            parseCFile file
    
    
    chrg's avatar
    chrg committed
          when debug do
            pPrint (void c)
    
    
    chrg's avatar
    chrg committed
          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"
    
    chrg's avatar
    chrg committed
              liftIO exitFailure
    
            t <- test file
            unless t do
    
              logError "file did not satisfy predicate"
              cleanup file
    
          when checkmode do
            liftIO exitSuccess
    
    chrg's avatar
    chrg committed
    
    
    chrg's avatar
    chrg committed
          l <-
    
    chrg's avatar
    chrg committed
            (if expmode then IRTree.reduceExpT id else IRTree.reduceT id)
    
    chrg's avatar
    chrg committed
              (check' file)
    
    chrg's avatar
    chrg committed
              (ReduceC.defaultReduceC c)
    
    chrg's avatar
    chrg committed
    
    
          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
    
    chrg's avatar
    chrg committed
     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