Embed standard library in the minijuvix binary (#210)

* Embed stdlib in minijuvix library

We add a new step at the beginning of the pipeline called Setup that
registers the modules in the standard library with the Files effect. The
standard library is then used when the Scoper queries the Files effect
for modules as it resolves import statements.

Use of the standard library can be disabled using the global
`--no-stdlib` command-line option.

* CI: Checkout submodules recursively for stdlib

* Add a new `--no-stdlib` option to shell check

* Poke CI

* CI: Checkout submodules in the test job

.github/workflows/ci.yml

@@ -23,6 +23,8 @@ jobs:
     steps:
       - name: Checkout our repository
         uses: actions/checkout@v2
+        with:
+          submodules: recursive
 
       - uses: r-lib/actions/setup-pandoc@v1
         with:
@@ -162,6 +164,7 @@ jobs:
         uses: actions/checkout@v2
         with:
           path: main
+          submodules: recursive
       - name: Setup Stack GHC
         run : |
           cd main

app/GlobalOptions.hs

@@ -12,6 +12,7 @@ data GlobalOptions = GlobalOptions
     _globalShowNameIds :: Bool,
     _globalOnlyErrors :: Bool,
     _globalNoTermination :: Bool,
+    _globalNoStdlib :: Bool,
     _globalInputFiles :: [FilePath]
   }
   deriving stock (Eq, Show)
@@ -25,6 +26,7 @@ defaultGlobalOptions =
       _globalShowNameIds = False,
       _globalOnlyErrors = False,
       _globalNoTermination = False,
+      _globalNoStdlib = False,
       _globalInputFiles = []
     }
 
@@ -35,6 +37,7 @@ instance Semigroup GlobalOptions where
         _globalShowNameIds = o1 ^. globalShowNameIds || o2 ^. globalShowNameIds,
         _globalOnlyErrors = o1 ^. globalOnlyErrors || o2 ^. globalOnlyErrors,
         _globalNoTermination = o1 ^. globalNoTermination || o2 ^. globalNoTermination,
+        _globalNoStdlib = o1 ^. globalNoStdlib || o2 ^. globalNoStdlib,
         _globalInputFiles = o1 ^. globalInputFiles ++ o2 ^. globalInputFiles
       }
 
@@ -70,6 +73,12 @@ parseGlobalFlags b = do
           <> help "Disable termination checking"
           <> hidden b
       )
+  _globalNoStdlib <-
+    switch
+      ( long "no-stdlib"
+          <> help "Do not use the standard library"
+          <> hidden b
+      )
   return GlobalOptions {_globalInputFiles = [], ..}
 
 parseGlobalOptions :: Bool -> Parser GlobalOptions

app/Main.hs

@@ -73,6 +73,7 @@ getEntryPoint r opts = nonEmpty (opts ^. globalInputFiles) >>= Just <$> entryPoi
       EntryPoint
         { _entryPointRoot = r,
           _entryPointNoTermination = opts ^. globalNoTermination,
+          _entryPointNoStdlib = opts ^. globalNoStdlib,
           _entryPointModulePaths = l
         }
 

src/MiniJuvix/Pipeline.hs

@@ -7,6 +7,7 @@ where
 import MiniJuvix.Builtins
 import MiniJuvix.Internal.NameIdGen
 import MiniJuvix.Pipeline.EntryPoint
+import MiniJuvix.Pipeline.Setup qualified as Setup
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract
 import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
@@ -36,11 +37,17 @@ runIO = runIOEither >=> mayThrow
 
 --------------------------------------------------------------------------------
 
+upToSetup ::
+  Member Files r =>
+  EntryPoint ->
+  Sem r EntryPoint
+upToSetup = Setup.entrySetup
+
 upToParsing ::
   Members '[Files, Error MiniJuvixError] r =>
   EntryPoint ->
   Sem r Parser.ParserResult
-upToParsing = pipelineParser
+upToParsing = upToSetup >=> pipelineParser
 
 upToScoping ::
   Members '[Files, NameIdGen, Error MiniJuvixError] r =>

src/MiniJuvix/Pipeline/EntryPoint.hs

@@ -9,6 +9,7 @@ import MiniJuvix.Prelude
 data EntryPoint = EntryPoint
   { _entryPointRoot :: FilePath,
     _entryPointNoTermination :: Bool,
+    _entryPointNoStdlib :: Bool,
     _entryPointModulePaths :: NonEmpty FilePath
   }
   deriving stock (Eq, Show)
@@ -18,6 +19,7 @@ defaultEntryPoint mainFile =
   EntryPoint
     { _entryPointRoot = ".",
       _entryPointNoTermination = False,
+      _entryPointNoStdlib = False,
       _entryPointModulePaths = pure mainFile
     }
 

src/MiniJuvix/Pipeline/Setup.hs

@@ -0,0 +1,22 @@
+module MiniJuvix.Pipeline.Setup where
+
+import Data.FileEmbed qualified as FE
+import MiniJuvix.Pipeline.EntryPoint
+import MiniJuvix.Prelude
+
+stdlibDir :: [(FilePath, Text)]
+stdlibDir =
+  let stdlibFiles :: [(FilePath, Text)]
+      stdlibFiles = second decodeUtf8 <$> $(FE.makeRelativeToProject "minijuvix-stdlib" >>= FE.embedDir)
+      isMjuvixFile :: (FilePath, Text) -> Bool
+      isMjuvixFile (fp, _) = takeExtension fp == ".mjuvix"
+   in filter isMjuvixFile stdlibFiles
+
+entrySetup ::
+  Member Files r =>
+  EntryPoint ->
+  Sem r EntryPoint
+entrySetup e = do
+  let root = e ^. entryPointRoot
+  unless (e ^. entryPointNoStdlib) (registerStdlib (first (root </>) <$> stdlibDir))
+  return e

src/MiniJuvix/Prelude/Files.hs

@@ -6,16 +6,48 @@ import MiniJuvix.Prelude.Base
 data Files m a where
   ReadFile' :: FilePath -> Files m Text
   EqualPaths' :: FilePath -> FilePath -> Files m (Maybe Bool)
+  RegisterStdlib :: [(FilePath, Text)] -> Files m ()
 
 makeSem ''Files
 
-runFilesIO :: Member (Embed IO) r => Sem (Files ': r) a -> Sem r a
-runFilesIO = interpret $ \case
-  ReadFile' f -> embed (readFile f)
+newtype FilesState = FilesState
+  {_stdlibTable :: HashMap FilePath Text}
+
+makeLenses ''FilesState
+
+initState :: FilesState
+initState = FilesState mempty
+
+readStdLibOrFile :: FilePath -> HashMap FilePath Text -> IO Text
+readStdLibOrFile f stdlib = do
+  cf <- canonicalizePath f
+  case HashMap.lookup cf stdlib of
+    Nothing -> readFile f
+    Just c -> return c
+
+seqFst :: (IO a, b) -> IO (a, b)
+seqFst (ma, b) = do
+  a <- ma
+  return (a, b)
+
+canonicalizeStdlib :: [(FilePath, Text)] -> IO (HashMap FilePath Text)
+canonicalizeStdlib stdlib = HashMap.fromList <$> mapM seqFst (first canonicalizePath <$> stdlib)
+
+runFilesIO' :: forall r a. Member (Embed IO) r => Sem (Files ': r) a -> Sem (State FilesState ': r) a
+runFilesIO' = reinterpret $ \case
+  ReadFile' f -> do
+    stdlib <- gets (^. stdlibTable)
+    embed (readStdLibOrFile f stdlib)
   EqualPaths' f h -> embed $ do
     f' <- canonicalizePath f
     h' <- canonicalizePath h
     return (Just (equalFilePath f' h'))
+  RegisterStdlib stdlib -> do
+    s <- embed (FilesState <$> canonicalizeStdlib stdlib)
+    put s
+
+runFilesIO :: Member (Embed IO) r => Sem (Files ': r) a -> Sem r a
+runFilesIO = evalState initState . runFilesIO'
 
 runFilesEmpty :: Sem (Files ': r) a -> Sem r a
 runFilesEmpty = runFilesPure mempty
@@ -33,3 +65,4 @@ runFilesPure fs = interpret $ \case
             <> unlines (HashMap.keys fs)
     Just c -> return c
   EqualPaths' _ _ -> return Nothing
+  RegisterStdlib {} -> return ()

test/BackendC/Base.hs

@@ -28,8 +28,8 @@ clangCompile mkClangArgs cResult stdinText step =
         pack <$> P.readProcess "wasmer" [wasmOutputFile] (unpack stdinText)
     )
 
-clangAssertion :: FilePath -> FilePath -> Text -> ((String -> IO ()) -> Assertion)
-clangAssertion mainFile expectedFile stdinText step = do
+clangAssertion :: StdlibMode -> FilePath -> FilePath -> Text -> ((String -> IO ()) -> Assertion)
+clangAssertion stdlibMode mainFile expectedFile stdinText step = do
   step "Check clang and wasmer are on path"
   assertCmdExists "clang"
   assertCmdExists "wasmer"
@@ -41,7 +41,7 @@ clangAssertion mainFile expectedFile stdinText step = do
       "WASI_SYSROOT_PATH"
 
   step "C Generation"
-  let entryPoint = defaultEntryPoint mainFile
+  let entryPoint = (defaultEntryPoint mainFile) {_entryPointNoStdlib = stdlibMode == StdlibExclude}
   p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint)
 
   expected <- TIO.readFile expectedFile

test/BackendC/Examples.hs

@@ -24,7 +24,7 @@ testDescr ExampleTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = mainRoot,
-          _testAssertion = Steps $ clangAssertion _mainFile expectedFile _stdinText
+          _testAssertion = Steps $ clangAssertion StdlibExclude _mainFile expectedFile _stdinText
         }
 
 allTests :: TestTree

test/BackendC/Positive.hs

@@ -5,7 +5,8 @@ import Base
 
 data PosTest = PosTest
   { _name :: String,
-    _relDir :: FilePath
+    _relDir :: FilePath,
+    _stdlibMode :: StdlibMode
   }
 
 makeLenses ''PosTest
@@ -25,7 +26,7 @@ testDescr PosTest {..} =
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ clangAssertion mainFile expectedFile ""
+          _testAssertion = Steps $ clangAssertion _stdlibMode mainFile expectedFile ""
         }
 
 allTests :: TestTree
@@ -36,16 +37,17 @@ allTests =
 
 tests :: [PosTest]
 tests =
-  [ PosTest "HelloWorld" "HelloWorld",
-    PosTest "Inductive types and pattern matching" "Nat",
-    PosTest "Polymorphic types" "Polymorphism",
-    PosTest "Multiple modules" "MultiModules",
-    PosTest "Higher Order Functions" "HigherOrder",
-    PosTest "Higher Order Functions and explicit holes" "PolymorphismHoles",
-    PosTest "Closures with no environment" "ClosureNoEnv",
-    PosTest "Closures with environment" "ClosureEnv",
-    PosTest "SimpleFungibleTokenImplicit" "SimpleFungibleTokenImplicit",
-    PosTest "Mutually recursive function" "MutuallyRecursive",
-    PosTest "Nested List type" "NestedList",
-    PosTest "Builtin types and functions" "Builtins"
+  [ PosTest "HelloWorld" "HelloWorld" StdlibExclude,
+    PosTest "Inductive types and pattern matching" "Nat" StdlibExclude,
+    PosTest "Polymorphic types" "Polymorphism" StdlibExclude,
+    PosTest "Multiple modules" "MultiModules" StdlibExclude,
+    PosTest "Higher Order Functions" "HigherOrder" StdlibExclude,
+    PosTest "Higher Order Functions and explicit holes" "PolymorphismHoles" StdlibExclude,
+    PosTest "Closures with no environment" "ClosureNoEnv" StdlibExclude,
+    PosTest "Closures with environment" "ClosureEnv" StdlibExclude,
+    PosTest "SimpleFungibleTokenImplicit" "SimpleFungibleTokenImplicit" StdlibExclude,
+    PosTest "Mutually recursive function" "MutuallyRecursive" StdlibExclude,
+    PosTest "Nested List type" "NestedList" StdlibExclude,
+    PosTest "Builtin types and functions" "Builtins" StdlibExclude,
+    PosTest "Import from embedded standard library" "StdlibImport" StdlibInclude
   ]

test/Base.hs

@@ -27,6 +27,9 @@ data TestDescr = TestDescr
 
 makeLenses ''TestDescr
 
+data StdlibMode = StdlibInclude | StdlibExclude
+  deriving stock (Show, Eq)
+
 mkTest :: TestDescr -> TestTree
 mkTest TestDescr {..} = case _testAssertion of
   Single assertion -> testCase _testName $ withCurrentDirectory _testRoot assertion

test/Scope/Positive.hs

@@ -4,6 +4,7 @@ import Base
 import Data.HashMap.Strict qualified as HashMap
 import MiniJuvix.Internal.NameIdGen
 import MiniJuvix.Pipeline
+import MiniJuvix.Pipeline.Setup
 import MiniJuvix.Prelude.Pretty
 import MiniJuvix.Syntax.Concrete.Parser qualified as Parser
 import MiniJuvix.Syntax.Concrete.Scoped.Pretty qualified as M
@@ -13,6 +14,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Utils
 data PosTest = PosTest
   { _name :: String,
     _relDir :: FilePath,
+    _stdlibMode :: StdlibMode,
     _file :: FilePath
   }
 
@@ -33,7 +35,20 @@ testDescr PosTest {..} =
           _testAssertion = Steps $ \step -> do
             cwd <- getCurrentDirectory
             entryFile <- canonicalizePath _file
-            let entryPoint = EntryPoint cwd False (pure entryFile)
+            let noStdlib = _stdlibMode == StdlibExclude
+                entryPoint =
+                  EntryPoint
+                    { _entryPointRoot = cwd,
+                      _entryPointNoTermination = False,
+                      _entryPointNoStdlib = noStdlib,
+                      _entryPointModulePaths = pure entryFile
+                    }
+                stdlibMap :: HashMap FilePath Text
+                stdlibMap = HashMap.mapKeys (cwd </>) (HashMap.fromList stdlibDir)
+                unionStdlib :: HashMap FilePath Text -> HashMap FilePath Text
+                unionStdlib fs
+                  | noStdlib = fs
+                  | otherwise = HashMap.union fs stdlibMap
 
             step "Parsing"
             p :: Parser.ParserResult <- runIO (upToParsing entryPoint)
@@ -41,28 +56,35 @@ testDescr PosTest {..} =
             let p2 = head (p ^. Parser.resultModules)
 
             step "Scoping"
-            s :: Scoper.ScoperResult <- runIO (pipelineScoper p)
+            s :: Scoper.ScoperResult <-
+              runIO
+                ( do
+                    void (entrySetup entryPoint)
+                    pipelineScoper p
+                )
 
             let s2 = head (s ^. Scoper.resultModules)
 
                 fs :: HashMap FilePath Text
                 fs =
-                  HashMap.fromList
-                    [ (getModuleFileAbsPath cwd m, renderCode m)
-                      | m <- toList (getAllModules s2)
-                    ]
+                  unionStdlib
+                    ( HashMap.fromList
+                        [ (getModuleFileAbsPath cwd m, renderCode m)
+                          | m <- toList (getAllModules s2)
+                        ]
+                    )
 
             let scopedPretty = renderCode s2
                 parsedPretty = renderCode p2
 
             step "Parsing pretty scoped"
-            let fs2 = HashMap.singleton entryFile scopedPretty
+            let fs2 = unionStdlib (HashMap.singleton entryFile scopedPretty)
             p' :: Parser.ParserResult <-
               (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs2)
                 (upToParsing entryPoint)
 
             step "Parsing pretty parsed"
-            let fs3 = HashMap.singleton entryFile parsedPretty
+            let fs3 = unionStdlib (HashMap.singleton entryFile parsedPretty)
             parsedPretty' :: Parser.ParserResult <-
               (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs3)
                 (upToParsing entryPoint)
@@ -96,69 +118,91 @@ tests =
   [ PosTest
       "Inductive"
       "."
+      StdlibInclude
       "Inductive.mjuvix",
     PosTest
       "Imports and qualified names"
       "Imports"
+      StdlibInclude
       "A.mjuvix",
     PosTest
       "Data.Bool from the stdlib"
       "StdlibList"
+      StdlibExclude
       "Data/Bool.mjuvix",
     PosTest
       "Data.Nat from the stdlib"
       "StdlibList"
+      StdlibExclude
       "Data/Nat.mjuvix",
     PosTest
       "Data.Ord from the stdlib"
       "StdlibList"
+      StdlibExclude
       "Data/Ord.mjuvix",
     PosTest
       "Data.Product from the stdlib"
       "StdlibList"
+      StdlibExclude
       "Data/Product.mjuvix",
     PosTest
       "Data.List and friends from the stdlib"
       "StdlibList"
+      StdlibExclude
       "Data/List.mjuvix",
     PosTest
       "Operators (+)"
       "."
+      StdlibExclude
       "Operators.mjuvix",
     PosTest
       "Literals"
       "."
+      StdlibExclude
       "Literals.mjuvix",
     PosTest
       "Hello World backends"
       "."
+      StdlibExclude
       "HelloWorld.mjuvix",
     PosTest
       "Axiom with backends"
       "."
+      StdlibExclude
       "Axiom.mjuvix",
     PosTest
       "Foreign block parsing"
       "."
+      StdlibExclude
       "Foreign.mjuvix",
     PosTest
       "Multiple modules non-ambiguous symbol - same file"
       "QualifiedSymbol"
+      StdlibExclude
       "M.mjuvix",
     PosTest
       "Multiple modules non-ambiguous symbol"
       "QualifiedSymbol2"
+      StdlibExclude
       "N.mjuvix",
     PosTest
       "Multiple modules constructor non-ambiguous symbol"
       "QualifiedConstructor"
+      StdlibExclude
       "M.mjuvix",
     PosTest
       "Parsing"
       "."
+      StdlibExclude
       "Parsing.mjuvix",
     PosTest
       "open overrides open public"
       "."
-      "ShadowPublicOpen.mjuvix"
+      StdlibExclude
+      "ShadowPublicOpen.mjuvix",
+    PosTest
+      "Import embedded standard library"
+      "StdlibImport"
+      StdlibInclude
+      "StdlibImport.mjuvix"
   ]

test/Termination/Negative.hs

@@ -20,7 +20,7 @@ testDescr NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = defaultEntryPoint _file
+            let entryPoint = (defaultEntryPoint _file) {_entryPointNoStdlib = True}
             result <- runIOEither (upToMicroJuvix entryPoint)
             case mapLeft fromMiniJuvixError result of
               Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure

test/Termination/Positive.hs

@@ -38,7 +38,7 @@ testDescrFlag N.NegTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            let entryPoint = EntryPoint "." True (pure _file)
+            let entryPoint = EntryPoint "." True True (pure _file)
             (void . runIO) (upToMicroJuvix entryPoint)
         }
 

tests/CLI/Commands/html.test

@@ -2,15 +2,15 @@ $ minijuvix html
 > /Provide.*/
 >= 1
 
-$ cd examples/milestone/Lib/ && minijuvix html Prelude.mjuvix && cat html/Prelude.html
+$ cd examples/milestone/Lib/ && minijuvix html --no-stdlib Prelude.mjuvix && cat html/Prelude.html
 > /<!DOCTYPE HTML>.*/
 >= 0
 
-$ rm -rf examples/html && minijuvix html examples/milestone/Lib/Prelude.mjuvix --output-dir=./../../html && [ -d examples/html/assets ] && [ -f examples/html/Prelude.html ]
+$ rm -rf examples/html && minijuvix html --no-stdlib examples/milestone/Lib/Prelude.mjuvix --output-dir=./../../html && [ -d examples/html/assets ] && [ -f examples/html/Prelude.html ]
 > 
 Writing Prelude.html
 >= 0
 
-$ rm -rf examples/html && minijuvix html examples/milestone/Lib/Prelude.mjuvix --recursive --output-dir=./../../html && (ls examples/html | wc -l) && cd examples/html && [ -f Data.String.html ] && [ -f Data.Maybe.html ] && [ -f Data.Int.html ] && [ -f System.IO.html ] && [ -f Data.List.html ] && [ -f Data.Pair.html ] && [ -f Data.Bool.html ] && [ -f Prelude.html ] && [ -f assets/highlight.js   ] && [ -f assets/source-ayu-light.css ] && [ -f assets/source-nord.css ]
+$ rm -rf examples/html && minijuvix html --no-stdlib examples/milestone/Lib/Prelude.mjuvix --recursive --output-dir=./../../html && (ls examples/html | wc -l) && cd examples/html && [ -f Data.String.html ] && [ -f Data.Maybe.html ] && [ -f Data.Int.html ] && [ -f System.IO.html ] && [ -f Data.List.html ] && [ -f Data.Pair.html ] && [ -f Data.Bool.html ] && [ -f Prelude.html ] && [ -f assets/highlight.js   ] && [ -f assets/source-ayu-light.css ] && [ -f assets/source-nord.css ]
 > /Writing.*/
 >= 0

tests/CLI/help.test

@@ -1,7 +1,7 @@
 $ minijuvix --help
 > /.*
 Usage\: minijuvix \(\(\-v\|\-\-version\) \| \(\-h\|\-\-help\) \| \[\-\-no\-colors\] \[\-\-show\-name\-ids\]
-                   \[\-\-only\-errors\] \[\-\-no\-termination\] COMMAND\)
+                   \[\-\-only\-errors\] \[\-\-no\-termination\] \[\-\-no\-stdlib\] COMMAND\)
 .*
 /
 >= 0

tests/positive/MiniC/StdlibImport/Input.mjuvix

@@ -0,0 +1,86 @@
+module Input;
+
+
+-- import from stdlib
+open import Data.Nat;
+
+
+--------------------------------------------------------------------------------
+-- Strings
+--------------------------------------------------------------------------------
+
+axiom String : Type;
+
+compile String {
+  c ↦ "char*";
+};
+
+
+--------------------------------------------------------------------------------
+-- Integers
+--------------------------------------------------------------------------------
+
+axiom Int : Type;
+
+compile Int {
+  c ↦ "int";
+};
+
+foreign c {
+  int plus(int l, int r) {
+    return l + r;
+  \}
+};
+
+infixl 6 +int;
+axiom +int : Int -> Int -> Int;
+
+compile +int {
+  c ↦ "plus";
+};
+
+axiom intToStr : Int → String;
+
+compile intToStr {
+  c ↦ "intToStr";
+};
+
+natToInt : ℕ → Int;
+natToInt zero ≔ 0;
+natToInt (suc n) ≔ 1 +int (natToInt n);
+
+natToStr : ℕ → String;
+natToStr n ≔ intToStr (natToInt n);
+
+
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
+
+axiom Action : Type;
+
+compile Action {
+  c ↦ "int";
+};
+
+axiom putStrLn : String → Action;
+
+compile putStrLn {
+  c ↦ "putStrLn";
+};
+
+
+--------------------------------------------------------------------------------
+-- IO
+--------------------------------------------------------------------------------
+
+two : ℕ;
+two ≔ suc (suc zero);
+
+three : ℕ;
+three ≔ two + (suc zero);
+
+main : Action;
+main ≔ putStrLn (natToStr (two + three));
+
+end;

tests/positive/MiniC/StdlibImport/expected.golden

@@ -0,0 +1 @@
+5

tests/positive/StdlibImport/A.mjuvix

@@ -0,0 +1,7 @@
+module A;
+
+inductive Foo {
+  bar : Foo;
+};
+
+end;

tests/positive/StdlibImport/StdlibImport.mjuvix

@@ -0,0 +1,14 @@
+module StdlibImport;
+
+open import Prelude;
+
+open import Data.Nat;
+import A;
+
+two : ℕ;
+two ≔ 1 + 1;
+
+foo : A.Foo;
+foo ≔ A.bar;
+
+end;