Newer
Older
import Colog
import Control.Applicative
import Control.Monad
import Data.Time (getCurrentTime)
import Data.Time qualified as Time
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)
$ []
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
s = withFrozenCallStack callStack
msg t = Colog.logMsg (Msg sev s (t <> p))
run :: (HasCallStack) => Parser (IO ())
run = do
[ long "dry-run"
, short 'n'
, help "don't do any reduction"
]
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"
]
[ long "pedandic"
, short 'P'
, help "when checking for validity, throw error if command fails"
[ long "debug"
, help "enable debugging"
]
cmd <- strArgument $ fold [metavar "COMMAND"]
file <- strArgument $ fold [metavar "FILE"]
let
fmt m = do
t' <- getCurrentTime
pure
( Text.pack
( Time.formatTime
Time.defaultTimeLocale
"%_3m:%04ES "
usingLoggerT (filterBySeverity Info msgSeverity $ cmapM fmt logTextStderr) do
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
when debug do
pPrint (void c)
when pedandic do
liftIO $ copyFile f (f <.> "last")
logDebug (Text.pack . show $ RPath.fromChoiceList $ map fst l)
res <-
if v
then test f
else do
logWarning "Produced invalid code"
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
liftIO exitFailure
c <- process D "parsing file" do
parseCFile file
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"
logError "file did not satisfy predicate"
cleanup file
when checkmode do
liftIO exitSuccess
c & fix \rec prevc -> do
mc' <-
(if expmode then IRTree.reduceExp else IRTree.reduce)
(check' file)
(ReduceC.defaultReduceC prevc)
case mc' of
Just c' ->
if fixpoint && c' /= c
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")