diff --git a/rzk/app/Main.hs b/rzk/app/Main.hs index 67fc4377d..19e4e808f 100644 --- a/rzk/app/Main.hs +++ b/rzk/app/Main.hs @@ -3,6 +3,7 @@ module Main where import System.Environment (getArgs) +import Control.Monad import Rzk.Polylingual @@ -10,11 +11,18 @@ main :: IO () main = do args <- getArgs case args of - ["typecheck", path] -> do - result <- safeParseSomeModule <$> readFile path - case result of - Left err -> putStrLn err - Right m -> putStrLn (compileSomeModule m) + "typecheck" : paths -> do + modules <- forM paths $ \path -> do + result <- safeParseSomeModule <$> readFile path + case result of + Left err -> do + putStrLn ("An error occurred when parsing file " <> path) + error err + Right m -> return m + case combineModules modules of + Left err -> do + error err + Right m -> putStrLn (compileSomeModule m) _ -> ppUsage ppUsage :: IO () diff --git a/rzk/src/Rzk/Polylingual.hs b/rzk/src/Rzk/Polylingual.hs index 4a25bf5e3..eb4f5b388 100644 --- a/rzk/src/Rzk/Polylingual.hs +++ b/rzk/src/Rzk/Polylingual.hs @@ -71,6 +71,9 @@ data Module var term = Module { moduleCommands :: [Command var term] } deriving (Show, Eq) +instance Semigroup (Module var term) where + Module cs1 <> Module cs2 = Module (cs1 <> cs2) + data LangMode = Rzk1 | STLC @@ -85,6 +88,23 @@ data SomeModule | Module_MLTT (Module Var MLTT.Term') deriving (Show) +combineModules :: [SomeModule] -> Either String SomeModule +combineModules [] = Left "no modules provided" +combineModules (m : ms) = combineModules1 m ms + +combineModules1 :: SomeModule -> [SomeModule] -> Either String SomeModule +combineModules1 m [] = return m +combineModules1 (Module_Rzk1 m1) (Module_Rzk1 m2 : ms) = + combineModules1 (Module_Rzk1 (m1 <> m2)) ms +combineModules1 (Module_STLC m1) (Module_STLC m2 : ms) = + combineModules1 (Module_STLC (m1 <> m2)) ms +combineModules1 (Module_PCF m1) (Module_PCF m2 : ms) = + combineModules1 (Module_PCF (m1 <> m2)) ms +combineModules1 (Module_MLTT m1) (Module_MLTT m2 : ms) = + combineModules1 (Module_MLTT (m1 <> m2)) ms +combineModules1 _ _ = + Left "trying to combine modules for different languages!" + compileSomeModule :: SomeModule -> String compileSomeModule = \case Module_Rzk1 m -> compileModuleRzk1 (moduleToRzk1 m)