Support multiple modules in compilation (#100)

* translate MiniJuvix import statements to MicroJuvix include statements

src/MiniJuvix/Internal/Strings.hs

@@ -17,6 +17,9 @@ eval = "eval"
 hiding :: IsString s => s
 hiding = "hiding"
 
+include :: IsString s => s
+include = "include"
+
 import_ :: IsString s => s
 import_ = "import"
 

src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs

@@ -56,9 +56,12 @@ instance Monoid InfoTable where
 buildTable :: Foldable f => f Module -> InfoTable
 buildTable = mconcatMap buildTable1
 
+-- TODO avoid building a table for the same module twice
 buildTable1 :: Module -> InfoTable
-buildTable1 m = InfoTable {..}
+buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
   where
+    includes :: [Include]
+    includes = [i | StatementInclude i <- ss]
     _infoInductives :: HashMap Name InductiveInfo
     _infoInductives =
       HashMap.fromList

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -64,6 +64,10 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
+newtype Include = Include
+  { _includeModule :: Module
+  }
+
 newtype ModuleBody = ModuleBody
   { _moduleStatements :: [Statement]
   }
@@ -73,6 +77,7 @@ data Statement
   | StatementFunction FunctionDef
   | StatementForeign ForeignBlock
   | StatementAxiom AxiomDef
+  | StatementInclude Include
 
 data AxiomDef = AxiomDef
   { _axiomName :: AxiomName,
@@ -204,6 +209,7 @@ data FunctionArgType
   deriving stock (Show)
 
 makeLenses ''Module
+makeLenses ''Include
 makeLenses ''Function
 makeLenses ''FunctionExpression
 makeLenses ''FunctionDef

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -84,6 +84,9 @@ instance PrettyCode Expression where
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
 
+kwInclude :: Doc Ann
+kwInclude = keyword Str.include
+
 kwArrow :: Doc Ann
 kwArrow = keyword Str.toAscii
 
@@ -251,6 +254,11 @@ instance PrettyCode ForeignBlock where
         <> line
         <> rbrace
 
+instance PrettyCode Include where
+  ppCode i = do
+    name' <- ppCode (i ^. includeModule . moduleName)
+    return $ kwInclude <+> name'
+
 instance PrettyCode AxiomDef where
   ppCode AxiomDef {..} = do
     axiomName' <- ppCode _axiomName
@@ -263,6 +271,7 @@ instance PrettyCode Statement where
     StatementFunction f -> ppCode f
     StatementInductive f -> ppCode f
     StatementAxiom f -> ppCode f
+    StatementInclude i -> ppCode i
 
 instance PrettyCode ModuleBody where
   ppCode m = do

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -53,6 +53,12 @@ checkModuleBody ModuleBody {..} = do
       { _moduleStatements = _moduleStatements'
       }
 
+checkInclude ::
+  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Include ->
+  Sem r Include
+checkInclude = traverseOf includeModule checkModule
+
 checkStatement ::
   Members '[Reader InfoTable, Error TypeCheckerError] r =>
   Statement ->
@@ -61,6 +67,7 @@ checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
   StatementForeign {} -> return s
   StatementInductive {} -> return s
+  StatementInclude i -> StatementInclude <$> checkInclude i
   StatementAxiom {} -> return s
 
 checkFunctionDef ::

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -4,6 +4,7 @@ module MiniJuvix.Translation.AbstractToMicroJuvix
   )
 where
 
+import Data.HashSet qualified as HashSet
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
 import MiniJuvix.Syntax.Abstract.Language.Extra qualified as A
@@ -14,19 +15,35 @@ import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult
 import MiniJuvix.Syntax.Universe
 import MiniJuvix.Syntax.Usage qualified as A
 
+newtype TranslationState = TranslationState
+  { -- | Top modules are supposed to be included at most once.
+    _translationStateIncluded :: HashSet A.TopModuleName
+  }
+
+iniState :: TranslationState
+iniState =
+  TranslationState
+    { _translationStateIncluded = mempty
+    }
+
+makeLenses ''TranslationState
+
 entryMicroJuvix ::
   Abstract.AbstractResult ->
   Sem r MicroJuvixResult
 entryMicroJuvix ares = do
-  _resultModules' <- mapM translateModule (ares ^. Abstract.resultModules)
+  _resultModules' <-
+    evalState
+      iniState
+      (mapM goModule (ares ^. Abstract.resultModules))
   return
     MicroJuvixResult
       { _resultAbstract = ares,
         _resultModules = _resultModules'
       }
 
-translateModule :: A.TopModule -> Sem r Module
-translateModule m = do
+goModule :: Member (State TranslationState) r => A.TopModule -> Sem r Module
+goModule m = do
   _moduleBody' <- goModuleBody (m ^. A.moduleBody)
   return
     Module
@@ -53,20 +70,32 @@ goSymbol s =
 unsupported :: Text -> a
 unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)
 
-goImport :: A.TopModule -> Sem r ModuleBody
-goImport m = goModuleBody (m ^. A.moduleBody)
+goModuleBody :: Member (State TranslationState) r => A.ModuleBody -> Sem r ModuleBody
+goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. A.moduleStatements)
 
-goModuleBody :: A.ModuleBody -> Sem r ModuleBody
-goModuleBody b = ModuleBody <$> mapM goStatement (b ^. A.moduleStatements)
+goImport :: Member (State TranslationState) r => A.TopModule -> Sem r (Maybe Include)
+goImport m = do
+  inc <- gets (HashSet.member (m ^. A.moduleName) . (^. translationStateIncluded))
+  if
+      | inc -> return Nothing
+      | otherwise -> do
+          modify (over translationStateIncluded (HashSet.insert (m ^. A.moduleName)))
+          m' <- goModule m
+          return
+            ( Just
+                Include
+                  { _includeModule = m'
+                  }
+            )
 
-goStatement :: A.Statement -> Sem r Statement
+goStatement :: Member (State TranslationState) r => A.Statement -> Sem r (Maybe Statement)
 goStatement = \case
-  A.StatementAxiom d -> StatementAxiom <$> goAxiomDef d
-  A.StatementForeign f -> return (StatementForeign f)
-  A.StatementFunction f -> StatementFunction <$> goFunctionDef f
-  A.StatementImport {} -> unsupported "imports"
+  A.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d
+  A.StatementForeign f -> return (Just (StatementForeign f))
+  A.StatementFunction f -> Just . StatementFunction <$> goFunctionDef f
+  A.StatementImport i -> fmap StatementInclude <$> goImport i
   A.StatementLocalModule {} -> unsupported "local modules"
-  A.StatementInductive i -> StatementInductive <$> goInductiveDef i
+  A.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i
 
 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix.hs

@@ -179,8 +179,15 @@ goModuleBody ::
   Members '[Error Err, Reader ConcreteTable, NameIdGen, Reader Micro.InfoTable] r =>
   Micro.ModuleBody ->
   Sem r ModuleBody
-goModuleBody Micro.ModuleBody {..} =
-  ModuleBody <$> concatMapM goStatement _moduleStatements
+goModuleBody b =
+  ModuleBody <$> concatMapM goStatement (b ^. Micro.moduleStatements)
+
+goInclude ::
+  Members '[Error Err, Reader ConcreteTable, NameIdGen, Reader Micro.InfoTable] r =>
+  Micro.Include ->
+  Sem r [Statement]
+goInclude i =
+  (^. moduleStatements) <$> goModuleBody (i ^. Micro.includeModule . Micro.moduleBody)
 
 goStatement ::
   Members '[Error Err, Reader ConcreteTable, NameIdGen, Reader Micro.InfoTable] r =>
@@ -191,6 +198,7 @@ goStatement = \case
   Micro.StatementFunction d -> map StatementFunction <$> goFunctionDef d
   Micro.StatementForeign d -> return [StatementForeign d]
   Micro.StatementAxiom a -> pure . StatementAxiom <$> goAxiomDef a
+  Micro.StatementInclude i -> goInclude i
 
 goAxiomDef :: Members '[Error Err, Reader ConcreteTable] r => Micro.AxiomDef -> Sem r AxiomDef
 goAxiomDef Micro.AxiomDef {..} = do

src/MiniJuvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs

@@ -28,8 +28,12 @@ goStatement = \case
   StatementInductive d -> goInductiveDef d
   StatementFunction f -> goFunctionDef f
   StatementForeign {} -> return ()
+  StatementInclude i -> goInclude i
   StatementAxiom a -> goAxiomDef a
 
+goInclude :: Members '[State TypeCallsMap, Reader InfoTable] r => Include -> Sem r ()
+goInclude i = goModule (i ^. includeModule)
+
 goAxiomDef :: Members '[State TypeCallsMap] r => AxiomDef -> Sem r ()
 goAxiomDef a =
   runReader

test/BackendC/Positive.hs

@@ -20,6 +20,9 @@ root = "tests/positive/MiniC"
 mainFile :: FilePath
 mainFile = "Input.mjuvix"
 
+expectedFile :: FilePath
+expectedFile = "expected.golden"
+
 testDescr :: PosTest -> TestDescr
 testDescr PosTest {..} =
   let tRoot = root </> _relDir
@@ -32,7 +35,7 @@ testDescr PosTest {..} =
             assertCmdExists "wasmer"
 
             step "C Generation"
-            let entryPoint = EntryPoint "." (return "Input.mjuvix")
+            let entryPoint = EntryPoint "." (pure mainFile)
             p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
 
             actual <-
@@ -47,9 +50,9 @@ testDescr PosTest {..} =
                     pack <$> P.readProcess "wasmer" [wasmOutputFile] ""
                 )
 
-            expected <- TIO.readFile "expected.golden"
+            expected <- TIO.readFile expectedFile
             step "Compare expected and actual program output"
-            assertEqDiff "check: WASM output = expected.golden" actual expected
+            assertEqDiff ("check: WASM output = " <> expectedFile) actual expected
         }
 
 allTests :: TestTree
@@ -62,5 +65,6 @@ tests :: [PosTest]
 tests =
   [ PosTest "HelloWorld" "HelloWorld",
     PosTest "Inductive types and pattern matching" "Nat",
-    PosTest "Polymorphic types" "Polymorphism"
+    PosTest "Polymorphic types" "Polymorphism",
+    PosTest "Multiple modules" "MultiModules"
   ]

tests/positive/MiniC/MultiModules/Bool.mjuvix

@@ -0,0 +1,9 @@
+module Bool;
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+
+end;

tests/positive/MiniC/MultiModules/IO.mjuvix

@@ -0,0 +1,45 @@
+module IO;
+
+import String;
+open String;
+
+axiom Action : Type;
+
+compile Action {
+  ghc ↦ "IO ()";
+  c ↦ "int";
+};
+
+foreign c {
+  int sequence(int a, int b) {
+    return a + b;
+  \}
+
+  int putStr(char* s) {
+    return fputs(s, stdout);
+  \}
+};
+
+infixl 1 >>;
+axiom >> : Action → Action → Action;
+
+compile >> {
+  ghc ↦ "(>>)";
+  c ↦ "sequence";
+};
+
+axiom put-str : String → Action;
+
+compile put-str {
+  ghc ↦ "putStr";
+  c ↦ "putStr";
+};
+
+axiom put-str-ln : String → Action;
+
+compile put-str-ln {
+  ghc ↦ "putStrLn";
+  c ↦ "puts";
+};
+
+end;

tests/positive/MiniC/MultiModules/Input.mjuvix

@@ -0,0 +1,35 @@
+module Input;
+
+import String;
+open String;
+
+import Bool;
+open Bool;
+
+import Pair;
+open Pair;
+
+import IO;
+open IO;
+
+-- Not needed but useful for testing
+import Prelude;
+open Prelude;
+
+bool-to-str : Bool → String;
+bool-to-str true ≔ "True";
+bool-to-str false ≔ "False";
+
+
+--------------------------------------------------------------------------------
+-- Main
+--------------------------------------------------------------------------------
+
+fst-of-pair : Action;
+fst-of-pair ≔ (put-str "fst (True, False) = ")
+               >> put-str-ln (bool-to-str (fst Bool Bool (mkPair Bool Bool true false)));
+
+main : Action;
+main ≔ fst-of-pair;
+
+end;

tests/positive/MiniC/MultiModules/Pair.mjuvix

@@ -0,0 +1,11 @@
+module Pair;
+
+inductive Pair (A : Type) (B : Type) {
+ mkPair : A → B → Pair A B;
+};
+
+fst : (A : Type) → (B : Type) → Pair A B → A;
+fst _ _ (mkPair a b) ≔ a;
+
+
+end;

tests/positive/MiniC/MultiModules/Prelude.mjuvix

@@ -0,0 +1,15 @@
+module Prelude;
+
+import String;
+open String public;
+
+import Bool;
+open Bool public;
+
+import Pair;
+open Pair public;
+
+import IO;
+open IO public;
+
+end;

tests/positive/MiniC/MultiModules/String.mjuvix

@@ -0,0 +1,10 @@
+module String;
+
+axiom String : Type;
+
+compile String {
+  ghc ↦ "[Char]";
+  c ↦ "char*";
+};
+
+end;

tests/positive/MiniC/MultiModules/expected.golden

@@ -0,0 +1 @@
+fst (True, False) = True