Merge branch 'main' into per-module-compilation

CHANGELOG.md

@@ -4,6 +4,30 @@
 <img align="right" width="300" height="300" alt="Juvix Mascot" src="../assets/images/tara-smiling.svg" />
 </a>
 
+## [v0.5.5](https://github.com/anoma/juvix/tree/v0.5.5) (2023-12-01)
+
+[Full Changelog](https://github.com/anoma/juvix/compare/v0.5.4...v0.5.5)
+
+**Implemented enhancements:**
+
+- Add new case for positivity checker: type cannot occur as arg of bound var [\#2542](https://github.com/anoma/juvix/pull/2542) ([jonaprieto](https://github.com/jonaprieto))
+- Add dependent defaults for the new typechecker [\#2541](https://github.com/anoma/juvix/pull/2541) ([janmasrovira](https://github.com/janmasrovira))
+- Extract builtin definitions for loading a Package into bundled package-base package [\#2535](https://github.com/anoma/juvix/pull/2535) ([paulcadman](https://github.com/paulcadman))
+- Update the Juvix lock file when the Package file changes [\#2522](https://github.com/anoma/juvix/pull/2522) ([paulcadman](https://github.com/paulcadman))
+- Add non-dependent default values to the new typechecking algorithm [\#2516](https://github.com/anoma/juvix/pull/2516) ([janmasrovira](https://github.com/janmasrovira))
+
+**Merged pull requests:**
+
+- Update to the latest juvix-stdlib [\#2546](https://github.com/anoma/juvix/pull/2546) ([paulcadman](https://github.com/paulcadman))
+- Remove old typechecker [\#2545](https://github.com/anoma/juvix/pull/2545) ([janmasrovira](https://github.com/janmasrovira))
+- Fix codeblocks indentation in Markdown output [\#2539](https://github.com/anoma/juvix/pull/2539) ([jonaprieto](https://github.com/jonaprieto))
+- runtime Makefile: Do not resolve variables when writing a dependency file [\#2538](https://github.com/anoma/juvix/pull/2538) ([paulcadman](https://github.com/paulcadman))
+- Fix location for aliases [\#2536](https://github.com/anoma/juvix/pull/2536) ([jonaprieto](https://github.com/jonaprieto))
+- Add Makefile to hyperfine benchmarks [\#2533](https://github.com/anoma/juvix/pull/2533) ([jonaprieto](https://github.com/jonaprieto))
+- Negative tests for `--new-typechecker` [\#2532](https://github.com/anoma/juvix/pull/2532) ([janmasrovira](https://github.com/janmasrovira))
+- Fix the global 'package' package so that modules within it can be type-checked independently [\#2526](https://github.com/anoma/juvix/pull/2526) ([paulcadman](https://github.com/paulcadman))
+- Improve inference for `--new-typechecker` [\#2524](https://github.com/anoma/juvix/pull/2524) ([janmasrovira](https://github.com/janmasrovira))
+
 ## [v0.5.4](https://github.com/anoma/juvix/tree/v0.5.4) (2023-11-17)
 
 [Full Changelog](https://github.com/anoma/juvix/compare/v0.5.3...v0.5.4)

Makefile

@@ -257,3 +257,10 @@ smoke: install submodules
 .PHONY : changelog
 changelog :
 	@github_changelog_generator
+
+HYPERFINEBIN := $(shell command -v hyperfine 2> /dev/null)
+
+.PHONY : hyperfine-benchmarks
+hyperfine-benchmarks:
+	@$(if $(HYPERFINEBIN),, $(error "hyperfine not found, please install it using cargo or from https://github.com/sharkdp/hyperfine"))
+	cd bench/hyperfine && ${MAKE}

app/App.hs

@@ -19,6 +19,7 @@ data App m a where
   ExitJuvixError :: JuvixError -> App m a
   PrintJuvixError :: JuvixError -> App m ()
   AskRoot :: App m Root
+  AskArgs :: App m RunAppIOArgs
   AskInvokeDir :: App m (Path Abs Dir)
   AskPkgDir :: App m (Path Abs Dir)
   AskBuildDir :: App m (Path Abs Dir)
@@ -36,38 +37,50 @@ data App m a where
   Say :: Text -> App m ()
   SayRaw :: ByteString -> App m ()
 
-makeSem ''App
-
 data RunAppIOArgs = RunAppIOArgs
   { _runAppIOArgsGlobalOptions :: GlobalOptions,
     _runAppIOArgsRoot :: Root
   }
 
+makeSem ''App
+makeLenses ''RunAppIOArgs
+
 runAppIO ::
   forall r a.
-  (Member (Embed IO) r) =>
+  (Members '[Embed IO, TaggedLock] r) =>
   RunAppIOArgs ->
   Sem (App ': r) a ->
   Sem r a
-runAppIO args@RunAppIOArgs {..} =
-  interpret $ \case
+runAppIO args = evalSingletonCache (readPackageRootIO root) . reAppIO args
+  where
+    root = args ^. runAppIOArgsRoot
+
+reAppIO ::
+  forall r a.
+  (Members '[Embed IO, TaggedLock] r) =>
+  RunAppIOArgs ->
+  Sem (App ': r) a ->
+  Sem (SCache Package ': r) a
+reAppIO args@RunAppIOArgs {..} =
+  reinterpret $ \case
     AskPackageGlobal -> return (_runAppIOArgsRoot ^. rootPackageType `elem` [GlobalStdlib, GlobalPackageDescription, GlobalPackageBase])
     FromAppPathFile p -> embed (prepathToAbsFile invDir (p ^. pathPath))
     GetMainFile m -> getMainFile' m
-    FromAppPathDir p -> embed (prepathToAbsDir invDir (p ^. pathPath))
+    FromAppPathDir p -> liftIO (prepathToAbsDir invDir (p ^. pathPath))
     RenderStdOut t
       | _runAppIOArgsGlobalOptions ^. globalOnlyErrors -> return ()
       | otherwise -> embed $ do
           sup <- Ansi.hSupportsANSIColor stdout
           renderIO (not (_runAppIOArgsGlobalOptions ^. globalNoColors) && sup) t
     AskGlobalOptions -> return _runAppIOArgsGlobalOptions
-    AskPackage -> return (_runAppIOArgsRoot ^. rootPackage)
+    AskPackage -> getPkg
+    AskArgs -> return args
     AskRoot -> return _runAppIOArgsRoot
     AskInvokeDir -> return invDir
     AskPkgDir -> return (_runAppIOArgsRoot ^. rootRootDir)
     AskBuildDir -> return (resolveAbsBuildDir (_runAppIOArgsRoot ^. rootRootDir) (_runAppIOArgsRoot ^. rootBuildDir))
     RunCorePipelineEither input -> do
-      entry <- embed (getEntryPoint' args input)
+      entry <- getEntryPoint' args input
       embed (corePipelineIOEither entry)
     RunPipelineEither input p -> do
       entry <- embed (getEntryPoint' args input)
@@ -89,15 +102,22 @@ runAppIO args@RunAppIOArgs {..} =
     ExitMsg exitCode t -> exitMsg' exitCode t
     SayRaw b -> embed (ByteString.putStr b)
   where
-    exitMsg' :: ExitCode -> Text -> Sem r x
-    exitMsg' exitCode t = embed (putStrLn t >> hFlush stdout >> exitWith exitCode)
-    getMainFile' :: Maybe (AppPath File) -> Sem r (Path Abs File)
+    getPkg :: (Members '[SCache Package] r') => Sem r' Package
+    getPkg = cacheSingletonGet
+
+    exitMsg' :: (Members '[Embed IO] r') => ExitCode -> Text -> Sem r' x
+    exitMsg' exitCode t = liftIO (putStrLn t >> hFlush stdout >> exitWith exitCode)
+
+    getMainFile' :: (Members '[SCache Package, Embed IO] r') => Maybe (AppPath File) -> Sem r' (Path Abs File)
     getMainFile' = \case
       Just p -> embed (prepathToAbsFile invDir (p ^. pathPath))
-      Nothing -> case pkg ^. packageMain of
-        Just p -> embed (prepathToAbsFile invDir p)
-        Nothing -> missingMainErr
-    missingMainErr :: Sem r x
+      Nothing -> do
+        pkg <- getPkg
+        case pkg ^. packageMain of
+          Just p -> embed (prepathToAbsFile invDir p)
+          Nothing -> missingMainErr
+
+    missingMainErr :: (Members '[Embed IO] r') => Sem r' x
     missingMainErr =
       exitMsg'
         (ExitFailure 1)
@@ -106,30 +126,40 @@ runAppIO args@RunAppIOArgs {..} =
             <> " file"
         )
     invDir = _runAppIOArgsRoot ^. rootInvokeDir
-    pkg :: Package
-    pkg = _runAppIOArgsRoot ^. rootPackage
     g :: GlobalOptions
     g = _runAppIOArgsGlobalOptions
     printErr e =
       embed $ hPutStrLn stderr $ run $ runReader (project' @GenericOptions g) $ Error.render (not (_runAppIOArgsGlobalOptions ^. globalNoColors)) (g ^. globalOnlyErrors) e
 
-getEntryPoint' :: RunAppIOArgs -> AppPath File -> IO EntryPoint
+getEntryPoint' :: (Members '[Embed IO, TaggedLock] r) => RunAppIOArgs -> AppPath File -> Sem r EntryPoint
 getEntryPoint' RunAppIOArgs {..} inputFile = do
   let opts = _runAppIOArgsGlobalOptions
       root = _runAppIOArgsRoot
   estdin <-
     if
-        | opts ^. globalStdin -> Just <$> getContents
+        | opts ^. globalStdin -> Just <$> liftIO getContents
         | otherwise -> return Nothing
   set entryPointStdin estdin <$> entryPointFromGlobalOptionsPre root (inputFile ^. pathPath) opts
 
-getEntryPointStdin' :: RunAppIOArgs -> IO EntryPoint
+runPipelineNoFileEither :: (Members '[Embed IO, TaggedLock, App] r) => Sem (PipelineEff r) a -> Sem r (Either JuvixError (ResolverState, a))
+runPipelineNoFileEither p = do
+  args <- askArgs
+  entry <- getEntryPointStdin' args
+  snd <$> runIOEither entry p
+
+runPipelineEither :: (Members '[Embed IO, TaggedLock, App] r) => AppPath File -> Sem (PipelineEff r) a -> Sem r (Either JuvixError (ResolverState, a))
+runPipelineEither input p = do
+  args <- askArgs
+  entry <- getEntryPoint' args input
+  snd <$> runIOEither entry p
+
+getEntryPointStdin' :: (Members '[Embed IO, TaggedLock] r) => RunAppIOArgs -> Sem r EntryPoint
 getEntryPointStdin' RunAppIOArgs {..} = do
   let opts = _runAppIOArgsGlobalOptions
       root = _runAppIOArgsRoot
   estdin <-
     if
-        | opts ^. globalStdin -> Just <$> getContents
+        | opts ^. globalStdin -> Just <$> liftIO getContents
         | otherwise -> return Nothing
   set entryPointStdin estdin <$> entryPointFromGlobalOptionsNoFile root opts
 
@@ -146,11 +176,11 @@ filePathToAbs fp = do
 askGenericOptions :: (Members '[App] r) => Sem r GenericOptions
 askGenericOptions = project <$> askGlobalOptions
 
-getEntryPoint :: (Members '[Embed IO, App] r) => AppPath File -> Sem r EntryPoint
+getEntryPoint :: (Members '[Embed IO, App, TaggedLock] r) => AppPath File -> Sem r EntryPoint
 getEntryPoint inputFile = do
   _runAppIOArgsGlobalOptions <- askGlobalOptions
   _runAppIOArgsRoot <- askRoot
-  embed (getEntryPoint' (RunAppIOArgs {..}) inputFile)
+  getEntryPoint' (RunAppIOArgs {..}) inputFile
 
 getEntryPointStdin :: (Members '[Embed IO, App] r) => Sem r EntryPoint
 getEntryPointStdin = do
@@ -165,14 +195,14 @@ runPipelineTermination input p = do
     Left err -> exitJuvixError err
     Right res -> return (snd res)
 
-runPipeline :: (Member App r) => AppPath File -> Sem PipelineEff a -> Sem r a
+runPipeline :: (Members '[App, Embed IO, TaggedLock] r) => AppPath File -> Sem (PipelineEff r) a -> Sem r a
 runPipeline input p = do
   r <- runPipelineEither input p
   case r of
     Left err -> exitJuvixError err
     Right res -> return (fst $ snd res)
 
-runPipelineNoFile :: (Member App r) => Sem PipelineEff a -> Sem r a
+runPipelineNoFile :: (Members '[App, Embed IO, TaggedLock] r) => Sem (PipelineEff r) a -> Sem r a
 runPipelineNoFile p = do
   r <- runPipelineNoFileEither p
   case r of

app/Commands/Compile.hs

@@ -9,7 +9,7 @@ import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 
-runCommand :: (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
+runCommand :: (Members '[Embed IO, App, TaggedLock] r) => CompileOptions -> Sem r ()
 runCommand opts@CompileOptions {..} = do
   inputFile <- getMainFile _compileInputFile
   Core.CoreResult {..} <- runPipeline (AppPath (preFileFromAbs inputFile) True) upToCore
@@ -27,7 +27,7 @@ runCommand opts@CompileOptions {..} = do
     TargetCore -> writeCoreFile arg
     TargetAsm -> Compile.runAsmPipeline arg
 
-writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
+writeCoreFile :: (Members '[Embed IO, App, TaggedLock] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile pa@Compile.PipelineArg {..} = do
   entryPoint <- Compile.getEntry pa
   coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile

app/Commands/Dependencies.hs

@@ -8,6 +8,6 @@ import Commands.Base
 import Commands.Dependencies.Options
 import Commands.Dependencies.Update qualified as Update
 
-runCommand :: (Members '[Embed IO, App] r) => DependenciesCommand -> Sem r ()
+runCommand :: (Members '[Embed IO, TaggedLock, App] r) => DependenciesCommand -> Sem r ()
 runCommand = \case
   Update -> Update.runCommand

app/Commands/Dev.hs

@@ -19,7 +19,7 @@ import Commands.Dev.Scope qualified as Scope
 import Commands.Dev.Termination qualified as Termination
 import Commands.Repl qualified as Repl
 
-runCommand :: (Members '[Embed IO, App] r) => DevCommand -> Sem r ()
+runCommand :: (Members '[Embed IO, App, TaggedLock] r) => DevCommand -> Sem r ()
 runCommand = \case
   Highlight opts -> Highlight.runCommand opts
   Parse opts -> Parse.runCommand opts

app/Commands/Dev/Asm.hs

@@ -6,7 +6,7 @@ import Commands.Dev.Asm.Options
 import Commands.Dev.Asm.Run as Run
 import Commands.Dev.Asm.Validate as Validate
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => AsmCommand -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, App, TaggedLock] r) => AsmCommand -> Sem r ()
 runCommand = \case
   Run opts -> Run.runCommand opts
   Validate opts -> Validate.runCommand opts

app/Commands/Dev/Asm/Compile.hs

@@ -8,7 +8,7 @@ import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => AsmCompileOptions -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, App, TaggedLock] r) => AsmCompileOptions -> Sem r ()
 runCommand opts = do
   file <- getFile
   ep <- getEntryPoint (AppPath (preFileFromAbs file) True)

app/Commands/Dev/Core.hs

@@ -11,7 +11,7 @@ import Commands.Dev.Core.Read as Read
 import Commands.Dev.Core.Repl as Repl
 import Commands.Dev.Core.Strip as Strip
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => CoreCommand -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, App, TaggedLock] r) => CoreCommand -> Sem r ()
 runCommand = \case
   Repl opts -> Repl.runCommand opts
   Eval opts -> Eval.runCommand opts

app/Commands/Dev/Core/Compile.hs

@@ -6,7 +6,7 @@ import Commands.Dev.Core.Compile.Options
 import Juvix.Compiler.Core.Data.Module qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, App, TaggedLock] r) => CompileOptions -> Sem r ()
 runCommand opts = do
   file <- getFile
   s <- readFile (toFilePath file)

app/Commands/Dev/Core/Compile/Base.hs

@@ -18,7 +18,7 @@ data PipelineArg = PipelineArg
     _pipelineArgModule :: Core.Module
   }
 
-getEntry :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r EntryPoint
+getEntry :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem r EntryPoint
 getEntry PipelineArg {..} = do
   ep <- getEntryPoint (AppPath (preFileFromAbs _pipelineArgFile) True)
   return $
@@ -46,7 +46,7 @@ getEntry PipelineArg {..} = do
 
 runCPipeline ::
   forall r.
-  (Members '[Embed IO, App] r) =>
+  (Members '[Embed IO, App, TaggedLock] r) =>
   PipelineArg ->
   Sem r ()
 runCPipeline pa@PipelineArg {..} = do
@@ -69,7 +69,7 @@ runCPipeline pa@PipelineArg {..} = do
 
 runGebPipeline ::
   forall r.
-  (Members '[Embed IO, App] r) =>
+  (Members '[Embed IO, App, TaggedLock] r) =>
   PipelineArg ->
   Sem r ()
 runGebPipeline pa@PipelineArg {..} = do
@@ -89,7 +89,7 @@ runGebPipeline pa@PipelineArg {..} = do
 
 runVampIRPipeline ::
   forall r.
-  (Members '[Embed IO, App] r) =>
+  (Members '[Embed IO, App, TaggedLock] r) =>
   PipelineArg ->
   Sem r ()
 runVampIRPipeline pa@PipelineArg {..} = do
@@ -98,7 +98,7 @@ runVampIRPipeline pa@PipelineArg {..} = do
   VampIR.Result {..} <- getRight (run (runReader entryPoint (runError (coreToVampIR _pipelineArgModule :: Sem '[Error JuvixError, Reader EntryPoint] VampIR.Result))))
   embed $ TIO.writeFile (toFilePath vampirFile) _resultCode
 
-runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
+runAsmPipeline :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem r ()
 runAsmPipeline pa@PipelineArg {..} = do
   entryPoint <- getEntry pa
   asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile

app/Commands/Dev/Core/FromConcrete.hs

@@ -11,7 +11,7 @@ import Juvix.Compiler.Core.Transformation qualified as Core
 import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames')
 import Juvix.Compiler.Core.Translation
 
-runCommand :: forall r. (Members '[Embed IO, App] r) => CoreFromConcreteOptions -> Sem r ()
+runCommand :: forall r. (Members '[Embed IO, TaggedLock, App] r) => CoreFromConcreteOptions -> Sem r ()
 runCommand localOpts = do
   gopts <- askGlobalOptions
   md <- (^. coreResultModule) <$> runPipeline (localOpts ^. coreFromConcreteInputFile) upToCore

app/Commands/Dev/Geb/Repl.hs

@@ -43,7 +43,7 @@ runCommand replOpts = do
         gopts <- State.gets (^. replStateGlobalOptions)
         absInputFile :: Path Abs File <- replMakeAbsolute inputFile
         set entryPointTarget Backend.TargetGeb
-          <$> liftIO (entryPointFromGlobalOptions root absInputFile gopts)
+          <$> liftIO (runM (runTaggedLockPermissive (entryPointFromGlobalOptions root absInputFile gopts)))
   embed
     ( State.evalStateT
         (replAction replOpts getReplEntryPoint)

app/Commands/Dev/Highlight.hs

@@ -5,12 +5,12 @@ import Commands.Dev.Highlight.Options
 import Juvix.Compiler.Concrete.Data.Highlight qualified as Highlight
 import Juvix.Compiler.Pipeline.Run
 
-runCommand :: (Members '[Embed IO, App] r) => HighlightOptions -> Sem r ()
+runCommand :: (Members '[Embed IO, App, TaggedLock] r) => HighlightOptions -> Sem r ()
 runCommand HighlightOptions {..} = do
   entry <- getEntryPoint _highlightInputFile
   inputFile <- fromAppPathFile _highlightInputFile
   hinput <-
     Highlight.filterInput
       inputFile
-      <$> liftIO (runPipelineHighlight entry upToInternalTyped)
+      <$> runPipelineHighlight entry upToInternalTyped
   sayRaw (Highlight.highlight _highlightBackend hinput)

app/Commands/Dev/Internal.hs

@@ -1,13 +1,11 @@
 module Commands.Dev.Internal where
 
 import Commands.Base
-import Commands.Dev.Internal.Arity qualified as Arity
 import Commands.Dev.Internal.Options
 import Commands.Dev.Internal.Pretty qualified as Pretty
 import Commands.Dev.Internal.Typecheck qualified as Typecheck
 
-runCommand :: (Members '[Embed IO, App] r) => InternalCommand -> Sem r ()
+runCommand :: (Members '[Embed IO, App, TaggedLock] r) => InternalCommand -> Sem r ()
 runCommand = \case
   Pretty opts -> Pretty.runCommand opts
-  Arity opts -> Arity.runCommand opts
   TypeCheck opts -> Typecheck.runCommand opts