copilot-verifier-0.1: exe/VerifyExamples.hs

{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
module Main (main) where

import qualified Data.CaseInsensitive as CI
import Data.CaseInsensitive (CI)
import Data.Foldable (for_)
import qualified Data.Map as Map
import qualified Data.Text as Text
import qualified Data.Text.IO as Text
import Data.Text (Text)
import Data.Traversable (for)
import Options.Applicative

import Copilot.Verifier (Verbosity(..))
import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)

newtype Options = Options
  { examples :: [CI Text]
  } deriving Show

optsParser :: Parser Options
optsParser = Options
  <$> (some . strArgument)
      (  metavar "EXAMPLE1 [EXAMPLE2 ...]"
      <> help "The names of the examples to run" )

main :: IO ()
main = execParser opts >>= verifyExamples
  where
    opts = info (optsParser <**> helper)
      ( fullDesc
     <> header "Run one or more copilot-verifier examples"
     <> progDesc (unlines [ "Run one or more examples from the copilot-verifier/examples directory."
                          , "Each EXAMPLE must correspond to an example name."
                          ]))

verifyExamples :: Options -> IO ()
verifyExamples Options{examples} = do
  -- Check that all requested examples exist
  examplesWithMain <- for examples $ \example ->
    case Map.lookup example (shouldFailExamples Default `Map.union` shouldPassExamples Default) of
      Just m  -> pure (example, m)
      Nothing -> fail $ "No example named " ++ Text.unpack (CI.original example)

  -- Run the examples
  for_ examplesWithMain $ \(example, exampleMain) -> do
    Text.putStrLn "====="
    Text.putStrLn $ "== Running the " <> CI.original example <> " example..."
    Text.putStrLn "====="
    Text.putStrLn ""
    exampleMain
    Text.putStrLn ""