mirror of
https://github.com/anoma/juvix.git
synced 2024-09-11 16:26:33 +03:00
Merge branch 'main' into isabelle-functions
This commit is contained in:
commit
b1315d47f3
@ -3,6 +3,8 @@ module Commands.Base
|
|||||||
module GlobalOptions,
|
module GlobalOptions,
|
||||||
module CommonOptions,
|
module CommonOptions,
|
||||||
module Juvix.Compiler.Pipeline,
|
module Juvix.Compiler.Pipeline,
|
||||||
|
module Juvix.Compiler.Pipeline.Run,
|
||||||
|
module Juvix.Compiler.Pipeline.Driver,
|
||||||
module Juvix.Prelude,
|
module Juvix.Prelude,
|
||||||
)
|
)
|
||||||
where
|
where
|
||||||
@ -11,4 +13,6 @@ import App
|
|||||||
import CommonOptions hiding (ensureLn, writeFileEnsureLn)
|
import CommonOptions hiding (ensureLn, writeFileEnsureLn)
|
||||||
import GlobalOptions
|
import GlobalOptions
|
||||||
import Juvix.Compiler.Pipeline
|
import Juvix.Compiler.Pipeline
|
||||||
|
import Juvix.Compiler.Pipeline.Driver
|
||||||
|
import Juvix.Compiler.Pipeline.Run
|
||||||
import Juvix.Prelude
|
import Juvix.Prelude
|
||||||
|
@ -3,7 +3,6 @@ module Commands.Dev.Highlight where
|
|||||||
import Commands.Base
|
import Commands.Base
|
||||||
import Commands.Dev.Highlight.Options
|
import Commands.Dev.Highlight.Options
|
||||||
import Juvix.Compiler.Concrete.Data.Highlight qualified as Highlight
|
import Juvix.Compiler.Concrete.Data.Highlight qualified as Highlight
|
||||||
import Juvix.Compiler.Pipeline.Run
|
|
||||||
|
|
||||||
runCommand :: (Members '[EmbedIO, App, TaggedLock] r) => HighlightOptions -> Sem r ()
|
runCommand :: (Members '[EmbedIO, App, TaggedLock] r) => HighlightOptions -> Sem r ()
|
||||||
runCommand HighlightOptions {..} = ignoreProgressLog . runPipelineOptions $ do
|
runCommand HighlightOptions {..} = ignoreProgressLog . runPipelineOptions $ do
|
||||||
|
@ -3,9 +3,7 @@ module Commands.Format where
|
|||||||
import Commands.Base
|
import Commands.Base
|
||||||
import Commands.Format.Options
|
import Commands.Format.Options
|
||||||
import Data.Text qualified as Text
|
import Data.Text qualified as Text
|
||||||
import Juvix.Compiler.Pipeline.Driver (processModule)
|
|
||||||
import Juvix.Compiler.Pipeline.Loader.PathResolver.ImportTree.Base
|
import Juvix.Compiler.Pipeline.Loader.PathResolver.ImportTree.Base
|
||||||
import Juvix.Compiler.Pipeline.ModuleInfoCache
|
|
||||||
import Juvix.Compiler.Store.Language (ModuleInfo)
|
import Juvix.Compiler.Store.Language (ModuleInfo)
|
||||||
import Juvix.Formatter
|
import Juvix.Formatter
|
||||||
|
|
||||||
@ -55,11 +53,7 @@ formatProject ::
|
|||||||
Sem r FormatResult
|
Sem r FormatResult
|
||||||
formatProject = runPipelineOptions . runPipelineSetup $ do
|
formatProject = runPipelineOptions . runPipelineSetup $ do
|
||||||
pkg <- askPackage
|
pkg <- askPackage
|
||||||
root <- (^. rootRootDir) <$> askRoot
|
res :: [(ImportNode, PipelineResult ModuleInfo)] <- processProject
|
||||||
nodes <- toList <$> asks (importTreeProjectNodes root)
|
|
||||||
res :: [(ImportNode, PipelineResult ModuleInfo)] <- forM nodes $ \node -> do
|
|
||||||
res <- mkEntryIndex node >>= processModule
|
|
||||||
return (node, res)
|
|
||||||
res' :: [(ImportNode, SourceCode)] <- runReader pkg . forM res $ \(node, nfo) -> do
|
res' :: [(ImportNode, SourceCode)] <- runReader pkg . forM res $ \(node, nfo) -> do
|
||||||
src <- formatModuleInfo node nfo
|
src <- formatModuleInfo node nfo
|
||||||
return (node, src)
|
return (node, src)
|
||||||
|
@ -27,7 +27,6 @@ import Juvix.Compiler.Core.Pretty qualified as Core
|
|||||||
import Juvix.Compiler.Internal.Language qualified as Internal
|
import Juvix.Compiler.Internal.Language qualified as Internal
|
||||||
import Juvix.Compiler.Internal.Pretty qualified as Internal
|
import Juvix.Compiler.Internal.Pretty qualified as Internal
|
||||||
import Juvix.Compiler.Pipeline.Repl
|
import Juvix.Compiler.Pipeline.Repl
|
||||||
import Juvix.Compiler.Pipeline.Run
|
|
||||||
import Juvix.Compiler.Store.Extra
|
import Juvix.Compiler.Store.Extra
|
||||||
import Juvix.Data.CodeAnn (Ann)
|
import Juvix.Data.CodeAnn (Ann)
|
||||||
import Juvix.Data.Error.GenericError qualified as Error
|
import Juvix.Data.Error.GenericError qualified as Error
|
||||||
|
@ -5,5 +5,7 @@ import Commands.Typecheck.Options
|
|||||||
|
|
||||||
runCommand :: (Members '[EmbedIO, TaggedLock, App] r) => TypecheckOptions -> Sem r ()
|
runCommand :: (Members '[EmbedIO, TaggedLock, App] r) => TypecheckOptions -> Sem r ()
|
||||||
runCommand localOpts = do
|
runCommand localOpts = do
|
||||||
void (runPipelineNoOptions (localOpts ^. typecheckInputFile) upToCoreTypecheck)
|
case localOpts ^. typecheckInputFile of
|
||||||
|
Just _inputFile -> void (runPipelineNoOptions (localOpts ^. typecheckInputFile) upToCoreTypecheck)
|
||||||
|
Nothing -> void (runPipelineOptions . runPipelineSetup $ processProject)
|
||||||
say "Well done! It type checks"
|
say "Well done! It type checks"
|
||||||
|
@ -4,6 +4,7 @@ module Juvix.Compiler.Pipeline.Driver
|
|||||||
JvoCache,
|
JvoCache,
|
||||||
evalJvoCache,
|
evalJvoCache,
|
||||||
processFileUpTo,
|
processFileUpTo,
|
||||||
|
processProject,
|
||||||
evalModuleInfoCache,
|
evalModuleInfoCache,
|
||||||
evalModuleInfoCacheSetup,
|
evalModuleInfoCacheSetup,
|
||||||
processFileToStoredCore,
|
processFileToStoredCore,
|
||||||
@ -37,6 +38,7 @@ import Juvix.Compiler.Pipeline.Loader.PathResolver
|
|||||||
import Juvix.Compiler.Pipeline.ModuleInfoCache
|
import Juvix.Compiler.Pipeline.ModuleInfoCache
|
||||||
import Juvix.Compiler.Store.Core.Extra
|
import Juvix.Compiler.Store.Core.Extra
|
||||||
import Juvix.Compiler.Store.Extra qualified as Store
|
import Juvix.Compiler.Store.Extra qualified as Store
|
||||||
|
import Juvix.Compiler.Store.Language
|
||||||
import Juvix.Compiler.Store.Language qualified as Store
|
import Juvix.Compiler.Store.Language qualified as Store
|
||||||
import Juvix.Compiler.Store.Options qualified as StoredModule
|
import Juvix.Compiler.Store.Options qualified as StoredModule
|
||||||
import Juvix.Compiler.Store.Options qualified as StoredOptions
|
import Juvix.Compiler.Store.Options qualified as StoredOptions
|
||||||
@ -123,6 +125,12 @@ processModuleCacheMiss entryIx = do
|
|||||||
Serialize.saveToFile absPath (res ^. pipelineResult)
|
Serialize.saveToFile absPath (res ^. pipelineResult)
|
||||||
return res
|
return res
|
||||||
|
|
||||||
|
processProject :: (Members '[ModuleInfoCache, Reader EntryPoint, Reader ImportTree] r) => Sem r [(ImportNode, PipelineResult ModuleInfo)]
|
||||||
|
processProject = do
|
||||||
|
rootDir <- asks (^. entryPointRoot)
|
||||||
|
nodes <- toList <$> asks (importTreeProjectNodes rootDir)
|
||||||
|
forWithM nodes (mkEntryIndex >=> processModule)
|
||||||
|
|
||||||
processRecursiveUpToTyped ::
|
processRecursiveUpToTyped ::
|
||||||
forall r.
|
forall r.
|
||||||
( Members
|
( Members
|
||||||
|
@ -250,6 +250,18 @@ traverseM ::
|
|||||||
f (m a2)
|
f (m a2)
|
||||||
traverseM f = fmap join . traverse f
|
traverseM f = fmap join . traverse f
|
||||||
|
|
||||||
|
forWith :: (Functor f) => f key -> (key -> val) -> f (key, val)
|
||||||
|
forWith = flip mapWith
|
||||||
|
|
||||||
|
forWithM :: (Traversable l, Applicative f) => l key -> (key -> f val) -> f (l (key, val))
|
||||||
|
forWithM = flip mapWithM
|
||||||
|
|
||||||
|
mapWith :: (Functor f) => (key -> val) -> f key -> f (key, val)
|
||||||
|
mapWith f = fmap (\x -> (x, f x))
|
||||||
|
|
||||||
|
mapWithM :: (Traversable l, Applicative f) => (key -> f val) -> l key -> f (l (key, val))
|
||||||
|
mapWithM f = traverse (\x -> (x,) <$> f x)
|
||||||
|
|
||||||
composeM :: (Monad m) => Int -> (a -> m a) -> a -> m a
|
composeM :: (Monad m) => Int -> (a -> m a) -> a -> m a
|
||||||
composeM 0 _ a = return a
|
composeM 0 _ a = return a
|
||||||
composeM n f a = composeM (n - 1) f a >>= f
|
composeM n f a = composeM (n - 1) f a >>= f
|
||||||
|
Loading…
Reference in New Issue
Block a user