From 2164845f73a8b005811f3e0fc947b14e1f5cbd7c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 28 Aug 2024 18:56:32 +0200 Subject: [PATCH 01/11] theory names --- app/App.hs | 11 +++-- .../Backend/Isabelle/Translation/FromTyped.hs | 44 ++++++++++++++----- src/Juvix/Compiler/Pipeline/Run.hs | 4 +- 3 files changed, 43 insertions(+), 16 deletions(-) diff --git a/app/App.hs b/app/App.hs index 50b5f73f8b..3bf5464951 100644 --- a/app/App.hs +++ b/app/App.hs @@ -270,10 +270,13 @@ runPipelineHtml bNonRecursive input_ | bNonRecursive = do r <- runPipelineNoOptions input_ upToInternalTyped return (r, []) - | otherwise = do - args <- askArgs - entry <- getEntryPoint' args input_ - runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError + | otherwise = runPipelineRecursive input_ + +runPipelineRecursive :: (Members '[App, EmbedIO, Logger, TaggedLock] r) => Maybe (AppPath File) -> Sem r (InternalTypedResult, [InternalTypedResult]) +runPipelineRecursive input_ = do + args <- askArgs + entry <- getEntryPoint' args input_ + runReader defaultPipelineOptions (runPipelineRecursiveEither entry) >>= fromRightJuvixError runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a runPipelineOptions m = do diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 87e48fb9c6..56cf0b71c1 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -51,36 +51,60 @@ 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 table _resultModule + go onlyTypes comments moduleNames table _resultModule where - go :: Bool -> [Comment] -> Internal.InfoTable -> Internal.Module -> Sem r Result - go onlyTypes comments tab md = + go :: Bool -> [Comment] -> [Name] -> Internal.InfoTable -> Internal.Module -> Sem r Result + go onlyTypes comments moduleNames tab md = return $ Result - { _resultTheory = goModule onlyTypes tab md, + { _resultTheory = goModule onlyTypes moduleNames tab md, _resultModuleId = md ^. Internal.moduleId, _resultComments = filter (\c -> c ^. commentInterval . intervalFile == file) comments } where file = getLoc md ^. intervalFile -goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory -goModule onlyTypes infoTable Internal.Module {..} = +goModule :: Bool -> [Name] -> Internal.InfoTable -> Internal.Module -> Theory +goModule onlyTypes moduleNames infoTable Internal.Module {..} = Theory - { _theoryName = overNameText toIsabelleName _moduleName, - _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), + { _theoryName = lookupTheoryName _moduleName, + _theoryImports = + map lookupTheoryName $ + map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of Just (PragmaIsabelleIgnore True) -> [] _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements) } where - toIsabelleName :: Text -> Text - toIsabelleName name = case reverse $ filter (/= "") $ T.splitOn "." name of + 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 + isTypeDef :: Statement -> Bool isTypeDef = \case StmtDefinition {} -> False diff --git a/src/Juvix/Compiler/Pipeline/Run.hs b/src/Juvix/Compiler/Pipeline/Run.hs index b73424f7d9..dd56ca1360 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -51,12 +51,12 @@ runPipelineHighlight :: Sem r HighlightInput runPipelineHighlight entry = fmap fst . runIOEitherHelper entry -runPipelineHtmlEither :: +runPipelineRecursiveEither :: forall r. (Members PipelineAppEffects r) => EntryPoint -> Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult])) -runPipelineHtmlEither entry = do +runPipelineRecursiveEither entry = do x <- runIOEitherPipeline' entry $ do processRecursiveUpToTyped return . mapRight snd $ snd x From e0037c612667a9b117716a691b1daec2caa2a845 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 29 Aug 2024 16:08:46 +0200 Subject: [PATCH 02/11] 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 3bf5464951..30b3150406 100644 --- a/app/App.hs +++ b/app/App.hs @@ -261,22 +261,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 3fcb3a508e..91cf474b61 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 ^. entryPointPackageId 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 dd56ca1360..a7be816c73 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 :: From 17ec9831d83af987ee6ba2d461a89c47f5c00d3f Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 30 Aug 2024 11:31:52 +0200 Subject: [PATCH 03/11] fix packages --- src/Juvix/Compiler/Pipeline/Driver.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index 91cf474b61..ffc83087a9 100644 --- a/src/Juvix/Compiler/Pipeline/Driver.hs +++ b/src/Juvix/Compiler/Pipeline/Driver.hs @@ -37,6 +37,7 @@ 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 (readGlobalPackage) import Juvix.Compiler.Pipeline.Package.Loader.EvalEff (EvalFileEff) import Juvix.Compiler.Store.Core.Extra import Juvix.Compiler.Store.Extra qualified as Store @@ -314,10 +315,15 @@ processRecursiveUpTo a = do where goImport :: ImportNode -> Sem r a goImport node = do + pkgInfo <- fromJust . HashMap.lookup (node ^. importNodePackageRoot) <$> getPackageInfos + pkg <- case pkgInfo ^. packagePackage of + PackageReal p -> return p + _ -> readGlobalPackage entry <- ask let entry' = entry - { _entryPointStdin = Nothing, + { _entryPointPackage = pkg, + _entryPointStdin = Nothing, _entryPointModulePath = Just (node ^. importNodeAbsFile) } (^. pipelineResult) <$> local (const entry') (processFileUpTo a) From f5150f709854e24b20b807da63e578dd48647f2b Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 30 Aug 2024 13:38:10 +0200 Subject: [PATCH 04/11] qualified names --- .../Backend/Isabelle/Translation/FromTyped.hs | 21 +++++++++++++++++-- src/Juvix/Parser/Error.hs | 2 +- tests/positive/Isabelle/M/Main.juvix | 6 ++++++ tests/positive/Isabelle/M/N.juvix | 5 +++++ tests/positive/Isabelle/N.juvix | 5 +++++ tests/positive/Isabelle/Program.juvix | 5 ++++- tests/positive/Isabelle/isabelle/M_Main.thy | 9 ++++++++ tests/positive/Isabelle/isabelle/M_N.thy | 8 +++++++ tests/positive/Isabelle/isabelle/N.thy | 8 +++++++ tests/positive/Isabelle/isabelle/Program.thy | 5 ++++- 10 files changed, 69 insertions(+), 5 deletions(-) create mode 100644 tests/positive/Isabelle/M/Main.juvix create mode 100644 tests/positive/Isabelle/M/N.juvix create mode 100644 tests/positive/Isabelle/N.juvix create mode 100644 tests/positive/Isabelle/isabelle/M_Main.thy create mode 100644 tests/positive/Isabelle/isabelle/M_N.thy create mode 100644 tests/positive/Isabelle/isabelle/N.thy diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index f5d524f650..3b3b255bd4 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -80,7 +80,7 @@ goModule onlyTypes infoTable Internal.Module {..} = where toIsabelleTheoryName :: Text -> Text toIsabelleTheoryName name = - Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name + quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name isTypeDef :: Statement -> Bool isTypeDef = \case @@ -1219,8 +1219,25 @@ goModule onlyTypes infoTable Internal.Module {..} = ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms)) quote :: Text -> Text - quote = quote' . Text.filter isLatin1 . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\'')) + quote txt0 + | Text.elem '.' txt0 = moduleName' <> "." <> idenName' + | otherwise = quote'' txt0 where + (moduleName, idenName) = Text.breakOnEnd "." txt0 + moduleName' = toIsabelleTheoryName (removeLastDot moduleName) + idenName' = quote'' idenName + + removeLastDot :: Text -> Text + removeLastDot txt + | Text.last txt == '.' = Text.init txt + | otherwise = txt + + quote'' :: Text -> Text + quote'' = + quote' + . Text.filter isLatin1 + . Text.filter (isLetter .||. isDigit .||. (== '_') .||. (== '\'')) + quote' :: Text -> Text quote' txt | HashSet.member txt reservedNames = quote' (prime txt) diff --git a/src/Juvix/Parser/Error.hs b/src/Juvix/Parser/Error.hs index af7277fd5e..8e3c2c0b08 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -178,7 +178,7 @@ instance ToGenericError StdinOrFileError where genericError StdinOrFileError = return GenericError - { _genericErrorLoc = singletonInterval (mkInitialLoc formatStdinPath), + { _genericErrorLoc = singletonInterval (mkInitialLoc noFile), _genericErrorMessage = prettyError "Neither JUVIX_FILE_OR_PROJECT nor --stdin option is chosen", _genericErrorIntervals = [] } diff --git a/tests/positive/Isabelle/M/Main.juvix b/tests/positive/Isabelle/M/Main.juvix new file mode 100644 index 0000000000..b8e8ac4086 --- /dev/null +++ b/tests/positive/Isabelle/M/Main.juvix @@ -0,0 +1,6 @@ +module M.Main; + +import Stdlib.Prelude open; +import M.N open; + +f (a : Nat) : Nat := g a; diff --git a/tests/positive/Isabelle/M/N.juvix b/tests/positive/Isabelle/M/N.juvix new file mode 100644 index 0000000000..092cfc76c8 --- /dev/null +++ b/tests/positive/Isabelle/M/N.juvix @@ -0,0 +1,5 @@ +module M.N; + +import Stdlib.Prelude open; + +g (a : Nat) : Nat := a + 1; diff --git a/tests/positive/Isabelle/N.juvix b/tests/positive/Isabelle/N.juvix new file mode 100644 index 0000000000..db6ae1ffe4 --- /dev/null +++ b/tests/positive/Isabelle/N.juvix @@ -0,0 +1,5 @@ +module N; + +import Stdlib.Prelude open; + +g (a : Nat) : Nat := a * 2; diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index c5afcaf9a9..07b43c703d 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -1,6 +1,9 @@ module Program; import Stdlib.Prelude open; +import N; +import M.N; +import M.Main as Main; id0 : Nat -> Nat := id; @@ -23,7 +26,7 @@ f (x y : Nat) : Nat -> Nat g (x y : Nat) : Bool := if - | x == y := false + | x == f x (N.g y) (M.N.g (Main.f y)) := false | else := true; inc (x : Nat) : Nat := suc x; diff --git a/tests/positive/Isabelle/isabelle/M_Main.thy b/tests/positive/Isabelle/isabelle/M_Main.thy new file mode 100644 index 0000000000..2a6d0c82a8 --- /dev/null +++ b/tests/positive/Isabelle/isabelle/M_Main.thy @@ -0,0 +1,9 @@ +theory M_Main +imports Main + M_N +begin + +fun f :: "nat \ nat" where + "f a = (g a)" + +end diff --git a/tests/positive/Isabelle/isabelle/M_N.thy b/tests/positive/Isabelle/isabelle/M_N.thy new file mode 100644 index 0000000000..76d2300fbd --- /dev/null +++ b/tests/positive/Isabelle/isabelle/M_N.thy @@ -0,0 +1,8 @@ +theory M_N +imports Main +begin + +fun g :: "nat \ nat" where + "g a = (a + 1)" + +end diff --git a/tests/positive/Isabelle/isabelle/N.thy b/tests/positive/Isabelle/isabelle/N.thy new file mode 100644 index 0000000000..1e706f594a --- /dev/null +++ b/tests/positive/Isabelle/isabelle/N.thy @@ -0,0 +1,8 @@ +theory N +imports Main +begin + +fun g :: "nat \ nat" where + "g a = (a * 2)" + +end diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 52c81005b8..c7bed18283 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -1,5 +1,8 @@ theory Program imports Main + N + M_N + M_Main begin definition id0 :: "nat \ nat" where @@ -25,7 +28,7 @@ fun f :: "nat \ nat \ nat \ nat" where "f x y z = ((z + 1) * x + y)" fun g :: "nat \ nat \ bool" where - "g x y = (if x = y then False else True)" + "g x y = (if x = f x (N.g y) (M_N.g (M_Main.f y)) then False else True)" fun inc :: "nat \ nat" where "inc x = (Suc x)" From 2ec830ebab2fa621f0679a7c58f81a3bc35e18fe Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 30 Aug 2024 18:20:19 +0200 Subject: [PATCH 05/11] use fully qualified names instead of aliases --- .../Backend/Isabelle/Translation/FromTyped.hs | 40 +++++++++++++------ 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index 3b3b255bd4..a738a80bb9 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -196,8 +196,8 @@ goModule onlyTypes infoTable Internal.Module {..} = } where argnames = - map (overNameText quote) $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo - name' = overNameText quote name + map quoteName $ filterTypeArgs 0 ty $ map (fromMaybe (defaultName (getLoc name) "_") . (^. Internal.argInfoName)) argsInfo + name' = quoteName name loc = getLoc name isFunction :: [Name] -> Internal.Expression -> Maybe Internal.Expression -> Bool @@ -377,18 +377,18 @@ goModule onlyTypes infoTable Internal.Module {..} = goTypeIden :: Internal.Iden -> Type goTypeIden = \case - Internal.IdenFunction name -> mkIndType (overNameText quote name) [] + Internal.IdenFunction name -> mkIndType (quoteName name) [] Internal.IdenConstructor name -> error ("unsupported type: constructor " <> Internal.ppTrace name) - Internal.IdenVar name -> TyVar $ TypeVar (overNameText quote name) - Internal.IdenAxiom name -> mkIndType (overNameText quote name) [] - Internal.IdenInductive name -> mkIndType (overNameText quote name) [] + Internal.IdenVar name -> TyVar $ TypeVar (quoteName name) + Internal.IdenAxiom name -> mkIndType (quoteName name) [] + Internal.IdenInductive name -> mkIndType (quoteName name) [] goTypeApp :: Internal.Application -> Type goTypeApp app = mkIndType name params where (ind, args) = Internal.unfoldApplication app params = map goType (toList args) - name = overNameText quote $ case ind of + name = quoteName $ case ind of Internal.ExpressionIden (Internal.IdenFunction n) -> n Internal.ExpressionIden (Internal.IdenAxiom n) -> n Internal.ExpressionIden (Internal.IdenInductive n) -> n @@ -417,8 +417,8 @@ goModule onlyTypes infoTable Internal.Module {..} = setNameText "None" name Just Internal.BuiltinMaybeJust -> setNameText "Some" name - _ -> overNameText quote name - Nothing -> overNameText quote name + _ -> quoteName name + Nothing -> quoteName name getArgtys :: Internal.ConstructorInfo -> [Internal.FunctionParameter] getArgtys ctrInfo = fst $ Internal.unfoldFunType $ ctrInfo ^. Internal.constructorInfoType @@ -431,8 +431,8 @@ goModule onlyTypes infoTable Internal.Module {..} = Just funInfo -> case funInfo ^. Internal.functionInfoPragmas . pragmasIsabelleFunction of Just PragmaIsabelleFunction {..} -> setNameText _pragmaIsabelleFunctionName name - Nothing -> overNameText quote name - Nothing -> overNameText quote name + Nothing -> quoteName name + Nothing -> quoteName name x -> x lookupName :: forall r. (Member (Reader NameMap) r) => Name -> Sem r Expression @@ -491,8 +491,8 @@ goModule onlyTypes infoTable Internal.Module {..} = Nothing -> return $ ExprIden (goConstrName name) Internal.IdenVar name -> do lookupName name - Internal.IdenAxiom name -> return $ ExprIden (overNameText quote name) - Internal.IdenInductive name -> return $ ExprIden (overNameText quote name) + Internal.IdenAxiom name -> return $ ExprIden (quoteName name) + Internal.IdenInductive name -> return $ ExprIden (quoteName name) goApplication :: Internal.Application -> Sem r Expression goApplication app@Internal.Application {..} @@ -1218,6 +1218,20 @@ goModule onlyTypes infoTable Internal.Module {..} = ++ map (^. Internal.inductiveInfoName . namePretty) (HashMap.elems (infoTable ^. Internal.infoInductives)) ++ map (^. Internal.axiomInfoDef . Internal.axiomName . namePretty) (HashMap.elems (infoTable ^. Internal.infoAxioms)) + quoteName :: Name -> Name + quoteName name = overNameText goNameText name + where + goNameText :: Text -> Text + goNameText txt + | Text.elem '.' txt = + let idenName = snd $ Text.breakOnEnd "." txt + modulePath = name ^. nameId . nameIdModuleId . moduleIdPath + modulePathText = Text.intercalate "." (modulePath ^. modulePathKeyDir ++ [modulePath ^. modulePathKeyName]) + moduleName' = toIsabelleTheoryName modulePathText + idenName' = quote idenName + in moduleName' <> "." <> idenName' + | otherwise = quote txt + quote :: Text -> Text quote txt0 | Text.elem '.' txt0 = moduleName' <> "." <> idenName' From bede8898c08595d43ef5c49db2b7a33e5d4d640e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 13 Sep 2024 19:51:36 +0200 Subject: [PATCH 06/11] fixes --- app/Commands/Isabelle.hs | 5 ++--- src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs | 5 +++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/app/Commands/Isabelle.hs b/app/Commands/Isabelle.hs index 7e34808246..26459f93f4 100644 --- a/app/Commands/Isabelle.hs +++ b/app/Commands/Isabelle.hs @@ -23,9 +23,8 @@ translateTyped opts pkg res comments = res ^. resultComments outputDir <- fromAppPathDir (opts ^. isabelleOutputDir) if - | opts ^. isabelleStdout -> do - renderStdOut (ppOutDefault comments thy) - putStrLn "" + | opts ^. isabelleStdout -> + renderStdOutLn (ppOutDefault comments thy) | otherwise -> do ensureDir outputDir let file :: Path Rel File diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index a738a80bb9..ec552dd177 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -71,8 +71,9 @@ goModule onlyTypes infoTable Internal.Module {..} = Theory { _theoryName = overNameText toIsabelleTheoryName _moduleName, _theoryImports = - map (overNameText toIsabelleTheoryName) $ - map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), + map + (overNameText toIsabelleTheoryName . (^. Internal.importModuleName)) + (_moduleBody ^. Internal.moduleImports), _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of Just (PragmaIsabelleIgnore True) -> [] _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements) From 784e399a484d81a6a7f4a3d302fd30a73ac1f396 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Fri, 13 Sep 2024 15:26:43 +0200 Subject: [PATCH 07/11] Update to GHC 9.10.1 (#2991) Since GHC 9.8.2 has a bug which blocks our development (see https://github.com/anoma/juvix/pull/2977#issuecomment-2325866056), I made a PR to update to GHC 9.10.1. Because stackage doesn't yet support GHC 9.10.1, I had to add some explicit dependencies and use `allow-newer-deps` in `stack.yaml`. I think we should merge this not to get blocked by the bug, and later clean up `stack.yaml` when GHC 9.10.1 becomes supported on stackage. --------- Co-authored-by: Paul Cadman --- .github/workflows/ci.yml | 2 +- package.yaml | 10 +++++----- src/Juvix/Data/Effect/Cache.hs | 1 + src/Juvix/Prelude.hs | 2 +- stack.yaml | 34 +++++++++++++++++++++++++++++++++- 5 files changed, 41 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 69c2e6d32f..f6e2eae54b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -28,7 +28,7 @@ env: RISC0_VM_VERSION: v1.0.1 ANOMA_VERSION: f52cd44235f35a907c22c428ce1fdf3237c97927 JUST_ARGS: runtimeCcArg=$CC runtimeLibtoolArg=$LIBTOOL - STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j + STACK_BUILD_ARGS: --pedantic -j4 --ghc-options=-j --stack-yaml=stack.yaml jobs: pre-commit: diff --git a/package.yaml b/package.yaml index 2702683257..aea66573a0 100644 --- a/package.yaml +++ b/package.yaml @@ -12,7 +12,7 @@ author: Lukasz Czajka, Github's contributors, ] -tested-with: ghc == 9.8.2 +tested-with: ghc == 9.10.1 homepage: https://juvix.org bug-reports: https://github.com/anoma/juvix/issues description: The Juvix compiler @@ -52,7 +52,7 @@ dependencies: - aeson-pretty == 0.8.* - ansi-terminal == 1.1.* - array == 0.5.* - - base == 4.19.* + - base == 4.20.* - base16-bytestring == 1.0.* - base64-bytestring == 1.2.* - bitvec == 1.1.* @@ -68,14 +68,14 @@ dependencies: - edit-distance == 0.2.* - effectful == 2.3.* - effectful-core == 2.3.* - - effectful-th == 1.0.* + - effectful-th == 1.0.0.2 - exceptions == 0.10.* - extra == 1.7.* - file-embed == 0.0.* - filelock == 0.1.* - filepath == 1.4.* - flatparse == 0.5.* - - ghc == 9.8.2 + - ghc == 9.10.1 - githash == 0.1.* - hashable == 1.4.* - language-c == 0.9.* @@ -102,7 +102,7 @@ dependencies: - stm == 2.5.* - Stream == 0.4.* - string-interpolate == 0.3.* - - template-haskell == 2.21.* + - template-haskell == 2.22.* - temporary == 1.3.* - text == 2.1.* - th-utilities == 0.2.* diff --git a/src/Juvix/Data/Effect/Cache.hs b/src/Juvix/Data/Effect/Cache.hs index cfa3e58d34..70fea93043 100644 --- a/src/Juvix/Data/Effect/Cache.hs +++ b/src/Juvix/Data/Effect/Cache.hs @@ -1,3 +1,4 @@ +{-# OPTIONS_GHC -Wno-redundant-constraints #-} {-# OPTIONS_GHC -Wno-unused-type-patterns #-} module Juvix.Data.Effect.Cache diff --git a/src/Juvix/Prelude.hs b/src/Juvix/Prelude.hs index e73f3c1ff2..2afa2c8806 100644 --- a/src/Juvix/Prelude.hs +++ b/src/Juvix/Prelude.hs @@ -10,7 +10,7 @@ module Juvix.Prelude where import Juvix.Data -import Juvix.Prelude.Base +import Juvix.Prelude.Base hiding (List) import Juvix.Prelude.Generic import Juvix.Prelude.Lens import Juvix.Prelude.Path diff --git a/stack.yaml b/stack.yaml index 4b65f7e81d..cf9fcc6ca0 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,14 +1,46 @@ ghc-options: "$locals": -optP-Wno-nonportable-include-path resolver: nightly-2024-05-31 +compiler: ghc-9.10.1 +compiler-check: match-exact extra-deps: - git: https://github.com/haskell-effectful/effectful.git - commit: 2037be9a4f4e8f8fd280d9359b1bc7feff9b29b9 + commit: 2a8f0b3a0536c578ee1ff83311863a27e9d3e2e1 subdirs: - effectful-th - git: https://github.com/Vekhir/aeson-better-errors.git commit: 1ec49ab7d1472046b680b5a64ae2930515b47714 + - Cabal-syntax-3.10.3.0@sha256:c2ca36499bf9365726968b1e11a757e6d846c47cdf0c2c26a003698fd3c300fe,7431 + - directory-1.3.8.5@sha256:fbeec9ec346e5272167f63dcb86af513b457a7b9fc36dc818e4c7b81608d612b,3166 + - filepath-1.4.300.2@sha256:345cbb1afe414a09e47737e4d14cbd51891a734e67c0ef3d77a1439518bb81e8,5900 + - haskeline-0.8.2.1@sha256:40096f75591b5391aa99c5ed87148da0e9288ca4be302dd9e5c4326f814089ba,6117 + - process-1.6.21.0@sha256:685bc68759da31b5f152092fe664e1644e84f6dc0ae7a6c143e8564a1d6dafe8,2644 + - unix-2.8.5.1@sha256:3f702a252a313a7bcb56e3908a14e7f9f1b40e41b7bdc8ae8a9605a1a8686f06,9808 + - containers-0.6.8@sha256:bb2bec1bbc6b39a7c97cd95e056a5698ec45beb5d8feb6caae12af64e4bd823c,2670 + - binary-0.8.9.2@sha256:03381e511429c44d13990c6d76281c4fc2468371cede4fe684b0c98d9b7d5f5a,6611 + - parsec-3.1.17.0@sha256:8407cbd428d7f640a0fff8891bd2f7aca13cebe70a5e654856f8abec9a648b56,5149 + - text-2.1.1@sha256:78c3fb91055d0607a80453327f087b9dc82168d41d0dca3ff410d21033b5e87d,10653 + - th-abstraction-0.6.0.0@sha256:313760d630851a0eba6bdcb1a1eb543c4c9c583072d704067fa3248a5252a8ae,2303 + - bytestring-0.12.1.0@sha256:98e79e1c97117143e4012983509ec95f7e5e4f6adff6914d07812a39f83404b9,9473 + - exceptions-0.10.8@sha256:c31fd9b35d36196cbb14ffa5fca4de49868fd39acfeddd601fb77e742554aa67,2892 + - template-haskell-2.22.0.0@sha256:463e87c76794859c861c95517329483282af8b079c02084755cc4bd1ae41d5ae,2151 + - th-desugar-1.17 + - polysemy-1.9.2.0 + - singletons-th-3.4 + - singletons-base-3.4 + - lens-5.3.2 allow-newer: true allow-newer-deps: - aeson-better-errors - effectful-th + - juvix + - cborg + - palette + - serialise + - string-interpolate + - tasty-hedgehog + - unicode-data + - unicode-transforms + - unliftio-core + - uuid-types + - versions From 644d5a2f9e4b7523f11461323bc6678a93ff9732 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 29 Nov 2024 16:11:26 +0100 Subject: [PATCH 08/11] fix Driver.hs --- src/Juvix/Compiler/Pipeline/Driver.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index ffc83087a9..ad0e286b3f 100644 --- a/src/Juvix/Compiler/Pipeline/Driver.hs +++ b/src/Juvix/Compiler/Pipeline/Driver.hs @@ -322,7 +322,7 @@ processRecursiveUpTo a = do entry <- ask let entry' = entry - { _entryPointPackage = pkg, + { _entryPointPackageId = pkg ^. packageId, _entryPointStdin = Nothing, _entryPointModulePath = Just (node ^. importNodeAbsFile) } From 41eef7ab633bde83040345f256c54dcc3908399e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 18 Sep 2024 17:06:29 +0200 Subject: [PATCH 09/11] fix nested pattern matching --- .../Backend/Isabelle/Translation/FromTyped.hs | 116 ++++++++++-------- tests/positive/Isabelle/Program.juvix | 41 +++++++ tests/positive/Isabelle/isabelle/Program.thy | 58 +++++++++ 3 files changed, 167 insertions(+), 48 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs index ec552dd177..72b2f94779 100644 --- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs @@ -2,7 +2,6 @@ module Juvix.Compiler.Backend.Isabelle.Translation.FromTyped where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet -import Data.List.NonEmpty.Extra qualified as NonEmpty import Data.Text qualified as T import Data.Text qualified as Text import Juvix.Compiler.Backend.Isabelle.Data.Result @@ -95,19 +94,33 @@ goModule onlyTypes infoTable Internal.Module {..} = mkExprCase c@Case {..} = case _caseValue of ExprIden v -> case _caseBranches of - CaseBranch {..} :| [] -> + CaseBranch {..} :| _ -> case _caseBranchPattern of PatVar v' -> substVar v' v _caseBranchBody _ -> ExprCase c - _ -> ExprCase c ExprTuple (Tuple (ExprIden v :| [])) -> case _caseBranches of - CaseBranch {..} :| [] -> + CaseBranch {..} :| _ -> case _caseBranchPattern of PatTuple (Tuple (PatVar v' :| [])) -> substVar v' v _caseBranchBody _ -> ExprCase c - _ -> ExprCase c - _ -> ExprCase c + _ -> + case _caseBranches of + br@CaseBranch {..} :| _ -> + case _caseBranchPattern of + PatVar _ -> + ExprCase + Case + { _caseValue = _caseValue, + _caseBranches = br :| [] + } + PatTuple (Tuple (PatVar _ :| [])) -> + ExprCase + Case + { _caseValue = _caseValue, + _caseBranches = br :| [] + } + _ -> ExprCase c goMutualBlock :: Internal.MutualBlock -> [Statement] goMutualBlock Internal.MutualBlock {..} = @@ -243,24 +256,25 @@ goModule onlyTypes infoTable Internal.Module {..} = : goClauses cls Nested pats npats -> let rhs = goExpression'' nset' nmap' _lambdaBody - argnames' = fmap getPatternArgName _lambdaPatterns + argnames' = fmap getPatternArgName lambdaPats vnames = - fmap - ( \(idx :: Int, mname) -> - maybe - ( defaultName - (getLoc cl) - ( disambiguate - (nset' ^. nameSet) - ("v_" <> show idx) - ) - ) - (overNameText (disambiguate (nset' ^. nameSet))) - mname - ) - (NonEmpty.zip (nonEmpty' [0 ..]) argnames') + nonEmpty' $ + fmap + ( \(idx :: Int, mname) -> + maybe + ( defaultName + (getLoc cl) + ( disambiguate + (nset' ^. nameSet) + ("v_" <> show idx) + ) + ) + (overNameText (disambiguate (nset' ^. nameSet))) + mname + ) + (zip [0 ..] argnames') nset'' = foldl' (flip (over nameSet . HashSet.insert . (^. namePretty))) nset' vnames - remainingBranches = goLambdaClauses'' nset'' nmap' cls + remainingBranches = goLambdaClauses'' nset'' nmap' (Just ty) cls valTuple = ExprTuple (Tuple (fmap ExprIden vnames)) patTuple = PatTuple (Tuple (nonEmpty' pats)) brs = goNestedBranches (getLoc cl) valTuple rhs remainingBranches patTuple (nonEmpty' npats) @@ -275,7 +289,8 @@ goModule onlyTypes infoTable Internal.Module {..} = } ] where - (npats0, nset', nmap') = goPatternArgsTop (filterTypeArgs 0 ty (toList _lambdaPatterns)) + lambdaPats = filterTypeArgs 0 ty (toList _lambdaPatterns) + (npats0, nset', nmap') = goPatternArgsTop lambdaPats [] -> [] goNestedBranches :: Interval -> Expression -> Expression -> [CaseBranch] -> Pattern -> NonEmpty (Expression, Nested Pattern) -> NonEmpty CaseBranch @@ -828,18 +843,7 @@ goModule onlyTypes infoTable Internal.Module {..} = | patsNum == 0 = goExpression (head _lambdaClauses ^. Internal.lambdaBody) | otherwise = goLams vars where - patsNum = - case _lambdaType of - Just ty -> - length - . filterTypeArgs 0 ty - . toList - $ head _lambdaClauses ^. Internal.lambdaPatterns - Nothing -> - length - . filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit)) - . toList - $ head _lambdaClauses ^. Internal.lambdaPatterns + patsNum = length $ filterLambdaPatternArgs _lambdaType $ head _lambdaClauses ^. Internal.lambdaPatterns vars = map (\i -> defaultName (getLoc lam) ("x" <> show i)) [0 .. patsNum - 1] goLams :: [Name] -> Sem r Expression @@ -869,7 +873,7 @@ goModule onlyTypes infoTable Internal.Module {..} = Tuple { _tupleComponents = nonEmpty' vars' } - brs <- goLambdaClauses (toList _lambdaClauses) + brs <- goLambdaClauses _lambdaType (toList _lambdaClauses) return $ mkExprCase Case @@ -926,17 +930,29 @@ goModule onlyTypes infoTable Internal.Module {..} = Internal.CaseBranchRhsExpression e -> goExpression e Internal.CaseBranchRhsIf {} -> error "unsupported: side conditions" - goLambdaClauses'' :: NameSet -> NameMap -> [Internal.LambdaClause] -> [CaseBranch] - goLambdaClauses'' nset nmap cls = - run $ runReader nset $ runReader nmap $ goLambdaClauses cls - - goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => [Internal.LambdaClause] -> Sem r [CaseBranch] - goLambdaClauses = \case + filterLambdaPatternArgs :: Maybe Internal.Expression -> NonEmpty Internal.PatternArg -> [Internal.PatternArg] + filterLambdaPatternArgs mty cls = case mty of + Just ty -> + filterTypeArgs 0 ty + . toList + $ cls + Nothing -> + filter ((/= Internal.Implicit) . (^. Internal.patternArgIsImplicit)) + . toList + $ cls + + goLambdaClauses'' :: NameSet -> NameMap -> Maybe Internal.Expression -> [Internal.LambdaClause] -> [CaseBranch] + goLambdaClauses'' nset nmap mty cls = + run $ runReader nset $ runReader nmap $ goLambdaClauses mty cls + + goLambdaClauses :: forall r. (Members '[Reader NameSet, Reader NameMap] r) => Maybe Internal.Expression -> [Internal.LambdaClause] -> Sem r [CaseBranch] + goLambdaClauses mty = \case cl@Internal.LambdaClause {..} : cls -> do - (npat, nset, nmap) <- case _lambdaPatterns of - p :| [] -> goPatternArgCase p + let lambdaPats = filterLambdaPatternArgs mty _lambdaPatterns + (npat, nset, nmap) <- case lambdaPats of + [p] -> goPatternArgCase p _ -> do - (npats, nset, nmap) <- goPatternArgsCase (toList _lambdaPatterns) + (npats, nset, nmap) <- goPatternArgsCase lambdaPats let npat = fmap ( \pats -> @@ -950,7 +966,7 @@ goModule onlyTypes infoTable Internal.Module {..} = case npat of Nested pat [] -> do body <- withLocalNames nset nmap $ goExpression _lambdaBody - brs <- goLambdaClauses cls + brs <- goLambdaClauses mty cls return $ CaseBranch { _caseBranchPattern = pat, @@ -961,7 +977,7 @@ goModule onlyTypes infoTable Internal.Module {..} = let vname = defaultName (getLoc cl) (disambiguate (nset ^. nameSet) "v") nset' = over nameSet (HashSet.insert (vname ^. namePretty)) nset rhs <- withLocalNames nset' nmap $ goExpression _lambdaBody - remainingBranches <- withLocalNames nset' nmap $ goLambdaClauses cls + remainingBranches <- withLocalNames nset' nmap $ goLambdaClauses mty cls let brs' = goNestedBranches (getLoc vname) (ExprIden vname) rhs remainingBranches pat (nonEmpty' npats) return [ CaseBranch @@ -1133,7 +1149,11 @@ goModule onlyTypes infoTable Internal.Module {..} = case HashMap.lookup name (infoTable ^. Internal.infoConstructors) of Just ctrInfo | ctrInfo ^. Internal.constructorInfoRecord -> - Just (indName, goRecordFields (getArgtys ctrInfo) args) + case HashMap.lookup indName (infoTable ^. Internal.infoInductives) of + Just indInfo + | length (indInfo ^. Internal.inductiveInfoConstructors) == 1 -> + Just (indName, goRecordFields (getArgtys ctrInfo) args) + _ -> Nothing where indName = ctrInfo ^. Internal.constructorInfoInductive _ -> Nothing diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 07b43c703d..16b028b2d1 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -193,3 +193,44 @@ funR4 : R -> R bf (b1 b2 : Bool) : Bool := not (b1 && b2); nf (n1 n2 : Int) : Bool := n1 - n2 >= n1 || n2 <= n1 + n2; + +-- Nested record patterns + +type MessagePacket (MessageType : Type) : Type := mkMessagePacket { + target : Nat; + mailbox : Maybe Nat; + message : MessageType; +}; + +type EnvelopedMessage (MessageType : Type) : Type := + mkEnvelopedMessage { + sender : Maybe Nat; + packet : MessagePacket MessageType; + }; + +type Timer (HandleType : Type): Type := mkTimer { + time : Nat; + handle : HandleType; +}; + +type Trigger (MessageType : Type) (HandleType : Type) := + | MessageArrived { envelope : EnvelopedMessage MessageType; } + | Elapsed { timers : List (Timer HandleType) }; + +getMessageFromTrigger : {M H : Type} -> Trigger M H -> Maybe M + | (MessageArrived@{ + envelope := (mkEnvelopedMessage@{ + packet := (mkMessagePacket@{ + message := m })})}) + := just m + | _ := nothing; + + +getMessageFromTrigger' {M H} (t : Trigger M H) : Maybe M := + case t of + | (MessageArrived@{ + envelope := (mkEnvelopedMessage@{ + packet := (mkMessagePacket@{ + message := m })})}) + := just m + | _ := nothing; diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index c7bed18283..59988ae8d7 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -241,4 +241,62 @@ fun bf :: "bool \ bool \ bool" where fun nf :: "int \ int \ bool" where "nf n1 n2 = (n1 - n2 \ n1 \ n2 \ n1 + n2)" +(* Nested record patterns *) +record 'MessageType MessagePacket = + target :: nat + mailbox :: "nat option" + message :: 'MessageType + +record 'MessageType EnvelopedMessage = + sender :: "nat option" + packet :: "'MessageType MessagePacket" + +record 'HandleType Timer = + time :: nat + handle :: 'HandleType + +datatype ('MessageType, 'HandleType) Trigger + = MessageArrived "'MessageType EnvelopedMessage" | + Elapsed "('HandleType Timer) list" + +fun target :: "'MessageType MessagePacket \ nat" where + "target (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) = + target'" + +fun mailbox :: "'MessageType MessagePacket \ nat option" where + "mailbox (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) = + mailbox'" + +fun message :: "'MessageType MessagePacket \ 'MessageType" where + "message (| MessagePacket.target = target', MessagePacket.mailbox = mailbox', MessagePacket.message = message' |) = + message'" + +fun sender :: "'MessageType EnvelopedMessage \ nat option" where + "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'" + +fun packet :: "'MessageType EnvelopedMessage \ 'MessageType MessagePacket" where + "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'" + +fun time :: "'HandleType Timer \ nat" where + "time (| Timer.time = time', Timer.handle = handle' |) = time'" + +fun handle :: "'HandleType Timer \ 'HandleType" where + "handle (| Timer.time = time', Timer.handle = handle' |) = handle'" + +fun getMessageFromTrigger :: "('M, 'H) Trigger \ 'M option" where + "getMessageFromTrigger v_0 = + (case (v_0) of + (MessageArrived v') \ + (case (EnvelopedMessage.packet v') of + (v'0) \ Some (MessagePacket.message v'0)) | + v'1 \ None)" + +fun getMessageFromTrigger' :: "('M, 'H) Trigger \ 'M option" where + "getMessageFromTrigger' t = + (case t of + (MessageArrived v') \ + (case (EnvelopedMessage.packet v') of + (v'0) \ Some (MessagePacket.message v'0)) | + v'2 \ None)" + end From 5da7a09b1b028a6bbce2ef60326aabf711aed4ac Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Sun, 1 Dec 2024 13:45:01 +0100 Subject: [PATCH 10/11] update Program.thy --- tests/positive/Isabelle/isabelle/Program.thy | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index 59988ae8d7..f19fe19e64 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -272,10 +272,12 @@ fun message :: "'MessageType MessagePacket \ 'MessageType" where message'" fun sender :: "'MessageType EnvelopedMessage \ nat option" where - "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = sender'" + "sender (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = + sender'" fun packet :: "'MessageType EnvelopedMessage \ 'MessageType MessagePacket" where - "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = packet'" + "packet (| EnvelopedMessage.sender = sender', EnvelopedMessage.packet = packet' |) = + packet'" fun time :: "'HandleType Timer \ nat" where "time (| Timer.time = time', Timer.handle = handle' |) = time'" From e8cd19347269c07da5c6c888720cde57f91e54f4 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 19 Sep 2024 12:39:54 +0200 Subject: [PATCH 11/11] Fix alias final names --- .../FromParsed/Analysis/Scoping.hs | 2 +- tests/positive/Isabelle/Program.juvix | 14 +++++ tests/positive/Isabelle/isabelle/Program.thy | 51 ++++++++++++------- 3 files changed, 48 insertions(+), 19 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index c26b0fdf05..643be45d90 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -850,7 +850,7 @@ entryToScopedIden name e = do return ScopedIden { _scopedIdenAlias = Just scopedName', - _scopedIdenFinal = helper (e' ^. symbolEntry) + _scopedIdenFinal = e' ^. symbolEntry } registerScopedIden si return si diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix index 16b028b2d1..34b80e2ab7 100644 --- a/tests/positive/Isabelle/Program.juvix +++ b/tests/positive/Isabelle/Program.juvix @@ -234,3 +234,17 @@ getMessageFromTrigger' {M H} (t : Trigger M H) : Maybe M := message := m })})}) := just m | _ := nothing; + +-- Syntax aliases + +Name : Type := Nat; + +syntax alias T := Name; + +idT (x : T) : T := x; + +t : T := 0; + +type RR := mkRR { + x : T +}; diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy index f19fe19e64..378a337691 100644 --- a/tests/positive/Isabelle/isabelle/Program.thy +++ b/tests/positive/Isabelle/isabelle/Program.thy @@ -18,25 +18,25 @@ definition id2 :: "'A \ 'A" where fun add_one :: "nat list \ nat list" where "add_one [] = []" | (* hello! *) - "add_one (x # xs) = ((x + 1) # add_one xs)" + "add_one (x' # xs) = ((x' + 1) # add_one xs)" fun sum :: "nat list \ nat" where "sum [] = 0" | - "sum (x # xs) = (x + sum xs)" + "sum (x' # xs) = (x' + sum xs)" fun f :: "nat \ nat \ nat \ nat" where - "f x y z = ((z + 1) * x + y)" + "f x' y z = ((z + 1) * x' + y)" fun g :: "nat \ nat \ bool" where - "g x y = (if x = f x (N.g y) (M_N.g (M_Main.f y)) then False else True)" + "g x' y = (if x' = f x' (N.g y) (M_N.g (M_Main.f y)) then False else True)" fun inc :: "nat \ nat" where - "inc x = (Suc x)" + "inc x' = (Suc x')" (* dec function *) fun dec :: "nat \ nat" where "dec 0 = 0" | - "dec (Suc x) = x" + "dec (Suc x') = x'" (* dec' function *) fun dec' :: "nat \ nat" where @@ -45,23 +45,23 @@ fun dec' :: "nat \ nat" where (* the zero case *) (* return zero *) (* the suc case *) - "dec' x = - (case x of + "dec' x' = + (case x' of 0 \ 0 | (Suc y) \ y)" fun optmap :: "('A \ 'A) \ 'A option \ 'A option" where "optmap f' None = None" | - "optmap f' (Some x) = (Some (f' x))" + "optmap f' (Some x') = (Some (f' x'))" fun pboth :: "('A \ 'A') \ ('B \ 'B') \ 'A \ 'B \ 'A' \ 'B'" where - "pboth f' g' (x, y) = (f' x, g' y)" + "pboth f' g' (x', y) = (f' x', g' y)" fun bool_fun :: "bool \ bool \ bool \ bool" where - "bool_fun x y z = (x \ (y \ z))" + "bool_fun x' y z = (x' \ (y \ z))" fun bool_fun' :: "bool \ bool \ bool \ bool" where - "bool_fun' x y z = (x \ y \ z)" + "bool_fun' x' y z = (x' \ y \ z)" (* Queues *) text \ @@ -71,7 +71,7 @@ datatype 'A Queue = queue "'A list" "'A list" fun qfst :: "'A Queue \ 'A list" where - "qfst (queue x v') = x" + "qfst (queue x' v') = x'" fun qsnd :: "'A Queue \ 'A list" where "qsnd (queue v' v'0) = v'0" @@ -85,10 +85,10 @@ fun pop_front :: "'A Queue \ 'A Queue" where v' \ q')" fun push_back :: "'A Queue \ 'A \ 'A Queue" where - "push_back q x = + "push_back q x' = (case qfst q of - [] \ queue [x] (qsnd q) | - q' \ queue q' (x # qsnd q))" + [] \ queue [x'] (qsnd q) | + q' \ queue q' (x' # qsnd q))" text \ Checks if the queue is empty @@ -294,11 +294,26 @@ fun getMessageFromTrigger :: "('M, 'H) Trigger \ 'M option" where v'1 \ None)" fun getMessageFromTrigger' :: "('M, 'H) Trigger \ 'M option" where - "getMessageFromTrigger' t = - (case t of + "getMessageFromTrigger' t' = + (case t' of (MessageArrived v') \ (case (EnvelopedMessage.packet v') of (v'0) \ Some (MessagePacket.message v'0)) | v'2 \ None)" +(* Syntax aliases *) +type_synonym Name = nat + +fun idT :: "nat \ Name" where + "idT x' = x'" + +definition t :: Name where + "t = 0" + +record RR = + x :: nat + +fun x :: "RR \ Name" where + "x (| RR.x = x' |) = x'" + end