From edb4d9528f924e5d46f2606a3d44af8cc16245de Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 29 Aug 2024 16:08:46 +0200 Subject: [PATCH] recursive translation --- app/App.hs | 31 +++++++++---- app/Commands/Isabelle.hs | 45 +++++++++++-------- app/Commands/Isabelle/Options.hs | 8 +++- .../Compiler/Backend/Isabelle/Pretty/Base.hs | 2 +- .../Backend/Isabelle/Translation/FromTyped.hs | 43 +++++------------- src/Juvix/Compiler/Pipeline/Driver.hs | 26 ++++++----- src/Juvix/Compiler/Pipeline/Run.hs | 9 ++-- 7 files changed, 86 insertions(+), 78 deletions(-) diff --git a/app/App.hs b/app/App.hs index 02b86eadd1..281b26c97a 100644 --- a/app/App.hs +++ b/app/App.hs @@ -255,22 +255,37 @@ runPipeline opts input_ = runPipelineLogger opts input_ . inject +runPipelineUpTo :: + (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) => + Bool -> + opts -> + Maybe (AppPath File) -> + Sem (PipelineEff r) a -> + Sem r (a, [a]) +runPipelineUpTo bNonRecursive opts input_ a + | bNonRecursive = do + r <- runPipeline opts input_ a + return (r, []) + | otherwise = runPipelineUpToRecursive opts input_ a + runPipelineHtml :: (Members '[App, EmbedIO, Logger, TaggedLock] r) => Bool -> Maybe (AppPath File) -> Sem r (InternalTypedResult, [InternalTypedResult]) -runPipelineHtml bNonRecursive input_ - | bNonRecursive = do - r <- runPipelineNoOptions input_ upToInternalTyped - return (r, []) - | otherwise = runPipelineRecursive input_ +runPipelineHtml bNonRecursive input_ = runPipelineUpTo bNonRecursive () input_ upToInternalTyped -runPipelineRecursive :: (Members '[App, EmbedIO, Logger, TaggedLock] r) => Maybe (AppPath File) -> Sem r (InternalTypedResult, [InternalTypedResult]) -runPipelineRecursive input_ = do +runPipelineUpToRecursive :: + (Members '[App, EmbedIO, Logger, TaggedLock] r, EntryPointOptions opts) => + opts -> + Maybe (AppPath File) -> + Sem (PipelineEff r) a -> + Sem r (a, [a]) +runPipelineUpToRecursive opts input_ a = do args <- askArgs entry <- getEntryPoint' args input_ - runReader defaultPipelineOptions (runPipelineRecursiveEither entry) >>= fromRightJuvixError + let entry' = applyOptions opts entry + runReader defaultPipelineOptions (runPipelineRecursiveEither entry' (inject a)) >>= fromRightJuvixError runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a runPipelineOptions m = do diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs index 410855d7c9..7e34808246 100644 --- a/app/Commands/Isabelle.hs +++ b/app/Commands/Isabelle.hs @@ -12,22 +12,29 @@ runCommand :: Sem r () runCommand opts = do let inputFile = opts ^. isabelleInputFile - res <- runPipeline opts inputFile upToIsabelle - let thy = res ^. resultTheory - comments = res ^. resultComments - outputDir <- fromAppPathDir (opts ^. isabelleOutputDir) - if - | opts ^. isabelleStdout -> do - renderStdOut (ppOutDefault comments thy) - putStrLn "" - | otherwise -> do - ensureDir outputDir - let file :: Path Rel File - file = - relFile - ( unpack (thy ^. theoryName . namePretty) - <.> isabelleFileExt - ) - absPath :: Path Abs File - absPath = outputDir file - writeFileEnsureLn absPath (ppPrint comments thy <> "\n") + (r, rs) <- runPipelineUpTo (opts ^. isabelleNonRecursive) opts inputFile upToIsabelle + let pkg = r ^. resultModuleId . moduleIdPackage + mapM_ (translateTyped opts pkg) (r : rs) + +translateTyped :: (Members AppEffects r) => IsabelleOptions -> Text -> Result -> Sem r () +translateTyped opts pkg res + | res ^. resultModuleId . moduleIdPackage == pkg = do + let thy = res ^. resultTheory + comments = res ^. resultComments + outputDir <- fromAppPathDir (opts ^. isabelleOutputDir) + if + | opts ^. isabelleStdout -> do + renderStdOut (ppOutDefault comments thy) + putStrLn "" + | otherwise -> do + ensureDir outputDir + let file :: Path Rel File + file = + relFile + ( unpack (thy ^. theoryName . namePretty) + <.> isabelleFileExt + ) + absPath :: Path Abs File + absPath = outputDir file + writeFileEnsureLn absPath (ppPrint comments thy <> "\n") + | otherwise = return () diff --git a/app/Commands/Isabelle/Options.hs b/app/Commands/Isabelle/Options.hs index 047422cd2b..c6c2ffd4f3 100644 --- a/app/Commands/Isabelle/Options.hs +++ b/app/Commands/Isabelle/Options.hs @@ -4,7 +4,8 @@ import CommonOptions import Juvix.Compiler.Pipeline.EntryPoint data IsabelleOptions = IsabelleOptions - { _isabelleInputFile :: Maybe (AppPath File), + { _isabelleNonRecursive :: Bool, + _isabelleInputFile :: Maybe (AppPath File), _isabelleOutputDir :: AppPath Dir, _isabelleStdout :: Bool, _isabelleOnlyTypes :: Bool @@ -15,6 +16,11 @@ makeLenses ''IsabelleOptions parseIsabelle :: Parser IsabelleOptions parseIsabelle = do + _isabelleNonRecursive <- + switch + ( long "non-recursive" + <> help "Do not process imported modules recursively" + ) _isabelleOutputDir <- parseGenericOutputDir ( value "isabelle" diff --git a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs index 1d1a45c675..636d43c96f 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Pretty/Base.hs @@ -315,7 +315,7 @@ instance PrettyCode RecordField where ppImports :: [Name] -> Sem r [Doc Ann] ppImports ns = - return $ map (dquotes . pretty) $ filter (not . Text.isPrefixOf "Stdlib/") $ map (Text.replace "." "/" . (^. namePretty)) ns + return $ map pretty $ filter (not . Text.isPrefixOf "Stdlib_" . (^. namePretty)) ns instance PrettyCode Theory where ppCode Theory {..} = do diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 56cf0b71c1..f5d524f650 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -51,29 +51,27 @@ fromInternal res@Internal.InternalTypedResult {..} = do itab' = Internal.insertInternalModule itab md table :: Internal.InfoTable table = Internal.computeCombinedInfoTable itab' - moduleNames :: [Name] - moduleNames = map (^. Internal.internalModuleName) (HashMap.elems (itab' ^. Internal.internalModuleTable)) comments :: [Comment] comments = allComments (Internal.getInternalTypedResultComments res) - go onlyTypes comments moduleNames table _resultModule + go onlyTypes comments table _resultModule where - go :: Bool -> [Comment] -> [Name] -> Internal.InfoTable -> Internal.Module -> Sem r Result - go onlyTypes comments moduleNames tab md = + go :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result + go onlyTypes comments tab md = return $ Result - { _resultTheory = goModule onlyTypes moduleNames tab md, + { _resultTheory = goModule onlyTypes tab md, _resultModuleId = md ^. Internal.moduleId, _resultComments = filter (\c -> c ^. commentInterval . intervalFile == file) comments } where file = getLoc md ^. intervalFile -goModule :: Bool -> [Name] -> Internal.InfoTable -> Internal.Module -> Theory -goModule onlyTypes moduleNames infoTable Internal.Module {..} = +goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory +goModule onlyTypes infoTable Internal.Module {..} = Theory - { _theoryName = lookupTheoryName _moduleName, + { _theoryName = overNameText toIsabelleTheoryName _moduleName, _theoryImports = - map lookupTheoryName $ + map (overNameText toIsabelleTheoryName) $ map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of Just (PragmaIsabelleIgnore True) -> [] @@ -81,29 +79,8 @@ goModule onlyTypes moduleNames infoTable Internal.Module {..} = } where toIsabelleTheoryName :: Text -> Text - toIsabelleTheoryName name = case reverse $ filter (/= "") $ T.splitOn "." name of - h : _ -> h - [] -> impossible - - moduleNameMap :: HashMap Name Name - moduleNameMap = - HashMap.fromList $ concatMap mapGroup groups - where - groups = groupSortOn (toIsabelleTheoryName . (^. nameText)) moduleNames - - mapGroup :: NonEmpty Name -> [(Name, Name)] - mapGroup (name :| names) = - (name, overNameText toIsabelleTheoryName name) : names' - where - names' = - zipWith - (\n (idx :: Int) -> (n, overNameText (<> "_" <> show idx) n)) - names - [0 ..] - - lookupTheoryName :: Name -> Name - lookupTheoryName name = - fromMaybe (error "lookupTheoryName") $ HashMap.lookup name moduleNameMap + toIsabelleTheoryName name = + Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name isTypeDef :: Statement -> Bool isTypeDef = \case diff --git a/src/Juvix/Compiler/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index 139e9477b5..50fe3e8f11 100644 --- a/src/Juvix/Compiler/Pipeline/Driver.hs +++ b/src/Juvix/Compiler/Pipeline/Driver.hs @@ -12,7 +12,7 @@ module Juvix.Compiler.Pipeline.Driver processFileUpToParsing, processModule, processImport, - processRecursiveUpToTyped, + processRecursiveUpTo, processImports, processModuleToStoredCore, ) @@ -32,12 +32,12 @@ import Juvix.Compiler.Core.Data.Module qualified as Core import Juvix.Compiler.Core.Translation.FromInternal.Data.Context qualified as Core import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as InternalTyped -import Juvix.Compiler.Internal.Translation.FromInternal.Data (InternalTypedResult) import Juvix.Compiler.Pipeline import Juvix.Compiler.Pipeline.Driver.Data import Juvix.Compiler.Pipeline.JvoCache import Juvix.Compiler.Pipeline.Loader.PathResolver import Juvix.Compiler.Pipeline.ModuleInfoCache +import Juvix.Compiler.Pipeline.Package.Loader.EvalEff (EvalFileEff) import Juvix.Compiler.Store.Core.Extra import Juvix.Compiler.Store.Extra qualified as Store import Juvix.Compiler.Store.Language @@ -280,8 +280,8 @@ processProject = do nodes <- toList <$> asks (importTreeProjectNodes rootDir) forWithM nodes (mkEntryIndex >=> processModule) -processRecursiveUpToTyped :: - forall r. +processRecursiveUpTo :: + forall a r. ( Members '[ Reader EntryPoint, TopModuleNameChecker, @@ -290,12 +290,14 @@ processRecursiveUpToTyped :: Error JuvixError, Files, PathResolver, - ModuleInfoCache + ModuleInfoCache, + EvalFileEff ] r ) => - Sem r (InternalTypedResult, [InternalTypedResult]) -processRecursiveUpToTyped = do + Sem (Reader Parser.ParserResult ': Reader Store.ModuleTable ': NameIdGen ': r) a -> + Sem r (a, [a]) +processRecursiveUpTo a = do entry <- ask PipelineResult {..} <- processFileUpToParsing entry let imports = HashMap.keys (_pipelineResultImports ^. Store.moduleTable) @@ -303,14 +305,14 @@ processRecursiveUpToTyped = do withPathFile imp goImport let pkg = entry ^. entryPointPackage mid <- runReader pkg (getModuleId (_pipelineResult ^. Parser.resultModule . modulePath . to topModulePathKey)) - a <- + r <- evalTopNameIdGen mid . runReader _pipelineResultImports . runReader _pipelineResult - $ upToInternalTyped - return (a, ms) + $ a + return (r, ms) where - goImport :: ImportNode -> Sem r InternalTypedResult + goImport :: ImportNode -> Sem r a goImport node = do entry <- ask let entry' = @@ -318,7 +320,7 @@ processRecursiveUpToTyped = do { _entryPointStdin = Nothing, _entryPointModulePath = Just (node ^. importNodeAbsFile) } - (^. pipelineResult) <$> runReader entry' (processFileUpTo upToInternalTyped) + (^. pipelineResult) <$> local (const entry') (processFileUpTo a) processImport :: forall r. diff --git a/src/Juvix/Compiler/Pipeline/Run.hs b/src/Juvix/Compiler/Pipeline/Run.hs index 4f6a9a2a0c..1b8ec456b1 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -52,13 +52,14 @@ runPipelineHighlight :: runPipelineHighlight entry = fmap fst . runIOEitherHelper entry runPipelineRecursiveEither :: - forall r. + forall a r. (Members PipelineAppEffects r) => EntryPoint -> - Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult])) -runPipelineRecursiveEither entry = do + Sem (PipelineEff r) a -> + Sem r (Either JuvixError (a, [a])) +runPipelineRecursiveEither entry a = do x <- runIOEitherPipeline' entry $ do - processRecursiveUpToTyped + processRecursiveUpTo a return . mapRight snd $ snd x runIOEitherHelper ::