Select Git revision
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
Main.hs 6.38 KiB
{-# 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
| Fib
deriving (Show, Read, Eq, Ord, Enum)
run :: (HasCallStack) => Parser (IO ())
run = do
mode <-
option auto $
fold
[ long "mode"
, help "search mode (Lin, Exp, Fib)"
, value Lin
]
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 fst l)
logInfo
( "Checking D="
<> Text.pack (show (maybe 0 NE.length xs))
<> ": "
<> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . snd . 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
mc' <-
( case mode of
Lin -> IRTree.reduce
Exp -> IRTree.reduceExp
Fib -> IRTree.reduceFib
)
(check' file)
(ReduceC.defaultReduceC prevc)
case mc' of
Just c' ->
if fixpoint && (c' $> ()) /= (prevc $> ())
then do
logInfo "Running again until fixpoint"
rec c'
else pure c'
Nothing -> do
logError "Was unable to produce any output"
cleanup file
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