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))
data Mode
= Lin
| Exp
deriving (Show, Read, Eq, Ord, Enum)
verbose <-
flag False True $
fold
[ long "verbose"
, short 'v'
, help "log more"
]
[ long "dry-run"
, short 'n'
, help "don't do any reduction"
]
keywords <-
many . option auto $
fold
[ long "keyword"
, short 'k'
, short 'V'
, help "check the output for the validity code and output debug information"
debug <-
flag False True $
fold
[ long "debug"
, short 'D'
, help "keep debug versions of all copies"
]
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"
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 "
let logger =
filterBySeverity (if verbose then Debug else Info) msgSeverity $
cmapM fmt logTextStderr
usingLoggerT logger do
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 ::
FilePath ->
[RPath.AnnotatedChoice (String, C.Position)] ->
C.CTranslationUnit C.NodeInfo ->
LoggerT (Msg Severity) IO Bool
<> Text.pack (maybe "-" ((\(r, p) -> r <> " at " <> show p) . RPath.label . NE.last) xs)
when debug $ liftIO do
copyFile f ("case-" <> show count <.> "c")
ret <- case res of
ExitSuccess -> do
liftIO $ copyFile f (f <.> "last")
pure True
ExitFailure x
| Just x == validity -> do
folder <- liftIO do
createTempDirectory temp "rtree-c"
logWarning $ "Produced invalid code, see " <> Text.pack folder <> " for details"
liftIO do
withFile (folder </> "reduction.path") WriteMode \h -> do
forM (takeWhile ((/= RPath.Undecided) . RPath.choice) l) \(RPath.AnnotatedChoice c' (msg, pos)) -> do
hPutStr h [RPath.debugShowChoice c']
hPutStr h " "
hPutStr h msg
hPutStr h " at "
hPrint h pos
tryIOError do
copyFile (f <.> "last") (folder </> takeFileName (f <.> "last"))
pure folder
when pedandic do
logError "Pedandic, stoping now."
liftIO exitFailure
pure False
| otherwise -> pure False
logInfo ("Predicate was " <> Text.pack (show ret))
pure ret
let bak = file <.> "bak"
process D "backing up file" do
liftIO $ copyFile file bak
process I "check predicate" do
t <- test file
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"
let rtree = ReduceC.defaultReduceCWithKeywords keywords c
t <- check file [] (IRTree.extract rtree)
logError "file did not satisfy predicate"
let rtree = ReduceC.defaultReduceCWithKeywords keywords prevc
c' <- case mode of
Lin -> IRTree.reduce (check file) rtree
Exp -> IRTree.reduceAdaptive (check file) rtree
if fixpoint && (c' $> ()) /= (prevc $> ())
then do
logInfo "Running again until fixpoint"
rec c'
else pure c'