Commit 6b155509 authored by Benjamin Chetioui's avatar Benjamin Chetioui
Browse files

Add a driver for the Myott compiler.

parent a7feb4f8
Pipeline #89582 failed with stages
in 54 minutes and 47 seconds
......@@ -71,9 +71,11 @@ library
,Util.Parser
,Util.PrettyPrint
,Util.Trace
,Argument
,Argument.Conventions
,Argument.Inference
,Driver
,Identifier
,Check
,Help
......@@ -122,18 +124,17 @@ executable myott
,Util.PrettyPrint
,Util.Trace
,Argument
,Argument.Inference
,Argument.Conventions
,Argument.Inference
,Driver
,Identifier
,Check
,Help
-- LANGUAGE extensions used by modules in this package.
other-extensions: FlexibleInstances, FlexibleContexts, TupleSections
-- Other library packages from which modules are imported.
build-depends: base >=4.12,
megaparsec, mtl, containers
megaparsec, mtl, containers, optparse-applicative
-- Directories containing source files.
hs-source-dirs: src
......
{-|
Module : Check
Description : The module containing the subcommand @check@ which checks specifications.
Stability : experimental
This module contains the 'check' function which loads some
specification files and runs them through a referee.
-}
module Check (Check.check) where
import Text.Megaparsec
import Control.Monad.Reader
import Control.Monad.State
import Data.Functor.Identity (runIdentity)
import System.IO
import System.Exit
import System.Environment
import qualified Data.List.NonEmpty as NonEmpty
import Control.Monad.Except
import Util.Trace
import Judgement.AST as JAST
import Judgement.Parser as Judgement
import Judgement.Referee as JRef
import Sequent.AST as SAST
import Sequent.Parser as Sequent
import Sequent.Referee as SRef
openRead = flip openFile ReadMode
unBundle = NonEmpty.head . bundleErrors
printUsage
= do
pname <- getProgName
hPutStrLn stderr
("Usage: " ++ pname ++ " check JUDGEMENT_SPEC TERM_SPEC")
printIndented istr s imax
= sequence (do
(l,i) <- zip s [0..]
let levels = min i imax
let indentation = concat (replicate levels istr)
return $ hPutStrLn
stderr
(indentation ++ l))
-- | Load a specification from file and through a referee.
check :: [String] -- ^ Files to load. Currently accepts only two files.
-> IO ()
check args = do
-- Open the source files.
(jfilename , sfilename) <- case args of
[jfilename, sfilename] -> return (jfilename , sfilename)
_ -> printUsage >> exitFailure
jfile <- openRead jfilename
sfile <- openRead sfilename
-- Read and check the specification of judgement forms
js <- hGetContents jfile
let jresult = do
ast <- tag ("Parsing the judgement specification: '"
++ jfilename ++ "'")
$ either (throwWithTrace . parseErrorPretty . unBundle) return
$ parse Judgement.specification jfilename js
tag ("Checking well-formedness of judgement specs: '"
++ jfilename ++ "'")
(runStateT (runReaderT (JAST.runSpecification ast) JRef.protokernel) mempty)
-- Read and check the specification of terms
ss <- hGetContents sfile
let spec = do
(jspec , jconv) <- jresult
ast <- tag ("Parsing the sequent specification: '"
++ sfilename ++ "'")
$ either (throwWithTrace . parseErrorPretty . unBundle) return
$ parse Sequent.specification sfilename ss
-- let sconv = SAST.extractConventions ast
tag ("Checking well-formedness of sequent specs: '"
++ sfilename ++ "'"
++ " using conventions:\n" ++ show jconv)
$ runStateT (runReaderT (SAST.runSpecification ast)
$ SRef.protokernel JRef.protokernel jspec) jconv
-- Display result of the checkings
case runIdentity (runReaderT (runExceptT spec) []) of
(Right _) -> putStrLn "OK"
(Left (s,e)) -> do
printIndented " " (reverse (e : s)) 10
exitFailure
{-# LANGUAGE FlexibleContexts #-}
{-|
Module : Driver
Description : The module exposing the subcommands of Myott.
Stability : experimental
This module contains the @runCheck@ and @runTest@ subcommands which can
respectively be invoked to check specifications through a referee and to test
particular passes of Myott.
-}
module Driver (
Config (..)
, Layer (..)
, LayerPass (..)
, runCheck
, runTest
) where
import Text.Megaparsec
import Control.Monad.Reader
import Control.Monad.State
import Data.Functor.Identity (runIdentity)
import System.IO
import System.Exit
import qualified Data.List.NonEmpty as NonEmpty
import Control.Monad.Except
import Util.Trace
import Judgement.AST as JAST
import Judgement.Parser as Judgement
import Judgement.Referee as JRef
import Sequent.AST as SAST
import Sequent.Parser as Sequent
import Sequent.Referee as SRef
-- * Test-related data structures
-- | A configuration to use when running Myott.
data Config = Config { _configLayer :: Layer
, _configLayerPass :: LayerPass
}
-- | The different layers of the Myott compiler.
data Layer = JudgementLayer | SequentLayer | TheoryLayer
-- | The passes run for each layer in Myott.
data LayerPass = ParsePass | CheckPass
-- * Exposed run functions
-- | Load a judgement and a sequent file and run consistency checks on the
-- loaded specifications using a referee. If errors are found, they are logged
-- to standard output.
runCheck :: FilePath -- ^ Judgement file to load.
-> FilePath -- ^ Sequent file to load.
-> IO ()
runCheck jfilepath sfilepath = do
jcontent <- openFile jfilepath ReadMode >>= hGetContents
scontent <- openFile sfilepath ReadMode >>= hGetContents
logErrs $ do
-- Parse and check the specification of judgement forms
(jspec, jconv) <- parseJudgementSpecification jfilepath jcontent
>>= checkJudgementSpecification jfilepath
-- Parse and check the specification of terms
parseSequentSpecification sfilepath scontent >>=
checkSequentSpecification jspec jconv sfilepath
-- | Load a judgement and a sequent file and run the tests specified by the
-- configuration on the loaded. If errors are found, they are logged
-- to standard output. Note that when testing parsing of a particular layer,
-- the relevant parsing operation is always done first.
runTest :: Config
-> FilePath -- ^ Judgement file to load.
-> FilePath -- ^ Sequent file to load.
-> IO ()
runTest config jfilepath sfilepath = do
jcontent <- openFile jfilepath ReadMode >>= hGetContents
scontent <- openFile sfilepath ReadMode >>= hGetContents
case _configLayer config of
JudgementLayer ->
let jspec = parseJudgementSpecification jfilepath jcontent
in case _configLayerPass config of
ParsePass -> logErrs jspec
CheckPass -> logErrs $
jspec >>= checkJudgementSpecification jfilepath
SequentLayer ->
let sspec = parseSequentSpecification sfilepath scontent
in case _configLayerPass config of
ParsePass -> logErrs sspec
CheckPass -> logErrs $
parseJudgementSpecification jfilepath jcontent
>>= checkJudgementSpecification jfilepath
>>= \(jspec, jconv) -> sspec
>>= checkSequentSpecification jspec jconv sfilepath
TheoryLayer -> error "theory layer is unimplemented"
-- * Pass-dependent functions
-- | Parses a judgement specification from a file.
parseJudgementSpecification
:: (MonadReader [String] m, MonadError ([String], String) m)
=> FilePath -> String -> m JAST.Specification
parseJudgementSpecification jfilename jfileContent =
tag ("Parsing the judgement specification: '" <> jfilename <> "'")
$ either (throwWithTrace . parseErrorPretty . unBundle) return
$ parse Judgement.specification jfilename jfileContent
-- | Checks the consistency of a judgement specification using a referee.
checkJudgementSpecification jfilename jspec =
tag ("Checking well-formedness of judgement specs: '" <> jfilename <> "'")
$ (`runStateT` mempty)
$ runReaderT (JAST.runSpecification jspec) JRef.protokernel
-- | Parses a sequent specification from a file.
parseSequentSpecification
:: (MonadReader [String] m, MonadError ([String], String) m)
=> FilePath -> String -> m SAST.Specification
parseSequentSpecification sfilename sfileContent =
tag ("Parsing the sequent specification: '" <> sfilename <> "'")
$ either (throwWithTrace . parseErrorPretty . unBundle) return
$ parse Sequent.specification sfilename sfileContent
-- | Checks the consistency of a sequent specification using a referee.
checkSequentSpecification jspec jconv sfilename sspec =
tag ("Checking well-formedness of sequent specs: '" <> sfilename <> "'" <>
" using conventions:\n" <> show jconv)
$ runStateT (runReaderT (SAST.runSpecification sspec)
$ SRef.protokernel JRef.protokernel jspec) jconv
-- * Miscellaneous utils
unBundle :: ParseErrorBundle s e -> ParseError s e
unBundle = NonEmpty.head . bundleErrors
printIndented :: String -> [String] -> Int -> IO [()]
printIndented istr s imax = sequence $ do
(l, i) <- zip s [0..]
let levels = min i imax
indentation = concat (replicate levels istr)
return $ hPutStrLn stderr (indentation ++ l)
logErrs r = case runIdentity (runExceptT r `runReaderT` []) of
Right _ -> putStrLn "OK"
Left (s, e) -> printIndented " " (reverse (e : s)) 10 >> exitFailure
\ No newline at end of file
{-|
Module : Help
Description : Provides help text for the Myott CLI.
Stability : experimental
This module provides help text for the @myott@ command line interface.
-}
module Help (help) where
-- | Print help for a specific sub-command.
help :: [String] -> IO ()
help _ = putStrLn "To be implemented."
{-|
Module : Main
Description : The main module of Myott, which calls sub-commands.
Description : The main module of Myott, which calls subcommands.
Stability : experimental
This module contains the 'main' function which reads
arguments from the command line and determines which subcommand
to execute.
This module contains the 'main' function which parses subcommands to execute
along with the relevant arguments from the command line.
-}
module Main (main,printUsage,runCommand) where
module Main where
import System.IO
import System.Environment
import qualified Data.List as L
import Options.Applicative
import Check
import Help
import Driver
-- | print usage text of the myott ClI.
printUsage :: IO ()
printUsage
= do
pname <- getProgName
hPutStrLn stderr
("Usage: " ++ pname ++ " SUBCOMMAND ARGUMENTS")
-- | The mode with which to run the Myott CLI.
data RunMode = CheckMode FilePath FilePath | TestMode Config FilePath FilePath
-- | 'main' function of the Myott CLI. Resolves subcommands.
main :: IO ()
main = do
args <- getArgs
case args of
[] -> printUsage
(command : cargs) -> runCommand command cargs
-- | Parses subcommands and relevant arguments for the Myott CLI.
parseRunMode :: ParserInfo RunMode
parseRunMode = info (subparser (checkCmd <> testCmd) <**> helper) mempty
where
checkCmd = command "check"
(info (helper <*> (CheckMode <$> jFilepath <*> sFilepath))
(progDesc "Check specification files using a referee"))
testCmd = command "test"
(info (helper <*> (TestMode <$> config <*> jFilepath <*> sFilepath))
(progDesc "Test specific passes of Myott"))
config = Config <$>
option (oneOf layerOpts)
(long "layer" <> short 'l' <>
help ("Layer to test: " <> dispOpts layerOpts)) <*>
option (oneOf layerPassOpts)
(long "layer-pass" <> short 'p' <>
help ("Pass to test in the layer: " <>
dispOpts layerPassOpts))
layerOpts = [ ("judgement", JudgementLayer)
, ("sequent", SequentLayer)
, ("theory", TheoryLayer )
]
-- | Run a subcomannd.
runCommand :: String -- ^ Name of the subcommand to execute
-> [String] -- ^ Arguments to the subcommand
-> IO () -- Resulting IO action.
runCommand "check" = Check.check
runCommand "help" = help
runCommand _ = const printUsage
layerPassOpts = [ ("parse", ParsePass)
, ("check", CheckPass)
]
jFilepath = argument str $
metavar "jfile" <> help "Source judgement file"
sFilepath = argument str $
metavar "sfile" <> help "Source sequent file"
oneOf :: [(String, a)] -> ReadM a
oneOf optPairs = eitherReader (\v -> case L.lookup v optPairs of
Just someOpt -> Right someOpt
_ -> Left $ "Option must be one of " <>
L.intercalate ", " (map (show . fst) optPairs))
dispOpts opts = L.intercalate " | " (map fst opts)
-- | 'main' function of the Myott CLI.
main :: IO ()
main = do
runMode <- customExecParser (prefs showHelpOnEmpty) parseRunMode
case runMode of
CheckMode jFilepath sFilepath -> runCheck jFilepath sFilepath
TestMode config jFilepath sFilepath ->
runTest config jFilepath sFilepath
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment