Skip to content
Snippets Groups Projects
Select Git revision
  • d9cc3d598681f4a57de80a6cc25d6892904f62c3
  • master default protected
2 results

footer.html

Blame
  • 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