Main.hs

{-# 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.Function
import Data.Functor
import Data.List.NonEmpty qualified as NE
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))

data Mode
  = Lin
  | Exp
  deriving (Show, Read, Eq, Ord, Enum)

run :: (HasCallStack) => Parser (IO ())
run = do
  mode <-
    option auto $
      fold
        [ long "mode"
        , help "search mode (Lin, Exp)"
        , value Exp
        ]

  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"
          ]

  fixpoint <-
    flag False True $
      fold
        [ long "fixpoint"
        , short 'F'
        , help "run the computation to a fixpoint"
        ]

  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
          let xs = NE.nonEmpty (filter ((RPath.Yes ==) . RPath.choice) l)
          logInfo
            ( "Checking D="
                <> Text.pack (show (RPath.numberOfUndecided l) <> "/" <> show (length l))
                <> ": "
                <> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . RPath.label . NE.last) xs)
            )
          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 <-
        c & fix \rec prevc -> do
          c' <-
            ( case mode of
                Lin -> IRTree.reduce
                Exp -> IRTree.reduceAdaptive
              )
              (check' file)
              (ReduceC.defaultReduceC prevc)
          if fixpoint && (c' $> ()) /= (prevc $> ())
            then do
              logInfo "Running again until fixpoint"
              rec c'
            else pure c'

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

      output file l
 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