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/app/App.hs b/app/App.hs index 50b5f73f8b..30b3150406 100644 --- a/app/App.hs +++ b/app/App.hs @@ -261,19 +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 = do - args <- askArgs - entry <- getEntryPoint' args input_ - runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError +runPipelineHtml bNonRecursive input_ = runPipelineUpTo bNonRecursive () input_ upToInternalTyped + +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_ + 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..26459f93f4 100644 --- a/app/Commands/Isabelle.hs +++ b/app/Commands/Isabelle.hs @@ -12,22 +12,28 @@ 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 -> + renderStdOutLn (ppOutDefault comments thy) + | 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/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/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 87e48fb9c6..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 @@ -69,17 +68,19 @@ fromInternal res@Internal.InternalTypedResult {..} = do goModule :: Bool -> Internal.InfoTable -> Internal.Module -> Theory goModule onlyTypes infoTable Internal.Module {..} = Theory - { _theoryName = overNameText toIsabelleName _moduleName, - _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports), + { _theoryName = overNameText toIsabelleTheoryName _moduleName, + _theoryImports = + map + (overNameText toIsabelleTheoryName . (^. 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 - h : _ -> h - [] -> impossible + toIsabelleTheoryName :: Text -> Text + toIsabelleTheoryName name = + quote . Text.intercalate "_" $ filter (/= "") $ T.splitOn "." name isTypeDef :: Statement -> Bool isTypeDef = \case @@ -93,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 {..} = @@ -195,8 +210,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 @@ -241,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) @@ -273,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 @@ -376,18 +393,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 @@ -416,8 +433,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 @@ -430,8 +447,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 @@ -490,8 +507,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 {..} @@ -826,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 @@ -867,7 +873,7 @@ goModule onlyTypes infoTable Internal.Module {..} = Tuple { _tupleComponents = nonEmpty' vars' } - brs <- goLambdaClauses (toList _lambdaClauses) + brs <- goLambdaClauses _lambdaType (toList _lambdaClauses) return $ mkExprCase Case @@ -924,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 -> @@ -948,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, @@ -959,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 @@ -1131,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 @@ -1217,9 +1239,40 @@ 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 = 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/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/src/Juvix/Compiler/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index 3fcb3a508e..ad0e286b3f 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,13 @@ 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 (readGlobalPackage) +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 +281,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 +291,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,22 +306,27 @@ 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 + pkgInfo <- fromJust . HashMap.lookup (node ^. importNodePackageRoot) <$> getPackageInfos + pkg <- case pkgInfo ^. packagePackage of + PackageReal p -> return p + _ -> readGlobalPackage entry <- ask let entry' = entry - { _entryPointStdin = Nothing, + { _entryPointPackageId = pkg ^. packageId, + _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 b73424f7d9..a7be816c73 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -51,14 +51,15 @@ runPipelineHighlight :: Sem r HighlightInput runPipelineHighlight entry = fmap fst . runIOEitherHelper entry -runPipelineHtmlEither :: - forall r. +runPipelineRecursiveEither :: + forall a r. (Members PipelineAppEffects r) => EntryPoint -> - Sem r (Either JuvixError (Typed.InternalTypedResult, [Typed.InternalTypedResult])) -runPipelineHtmlEither 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 :: 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/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/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 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..34b80e2ab7 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; @@ -190,3 +193,58 @@ 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; + +-- 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/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..378a337691 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 @@ -15,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 = 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 @@ -42,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 \ @@ -68,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" @@ -82,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 @@ -238,4 +241,79 @@ 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)" + +(* 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