Allow rzk executable to take multiple files as inputs

rzk/app/Main.hs

@@ -3,18 +3,26 @@
 module Main where
 
 import           System.Environment (getArgs)
+import Control.Monad
 
 import           Rzk.Polylingual
 
 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 ()

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)