diff --git a/app/App.hs b/app/App.hs index 0f61308be5..281b26c97a 100644 --- a/app/App.hs +++ b/app/App.hs @@ -255,19 +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 = 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/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/Pipeline/Driver.hs b/src/Juvix/Compiler/Pipeline/Driver.hs index 139e9477b5..7b73cd9ee3 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 ^. 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 + 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) <$> 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 e70f99d2d0..1b8ec456b1 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/Parser/Error.hs b/src/Juvix/Parser/Error.hs index d464a50115..8c88ea85e1 100644 --- a/src/Juvix/Parser/Error.hs +++ b/src/Juvix/Parser/Error.hs @@ -177,7 +177,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 7e7db6324b..0d1b313db0 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; @@ -151,3 +154,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/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 2d7324f431..3ef6bb3b09 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)" @@ -237,4 +240,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