From 4c5fee3e95bc7827758080ad7752fea124785fbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Mon, 25 Jul 2022 18:38:44 +0200 Subject: [PATCH] Compute name dependency graph and filter unreachable definitions (#1408) * Compute name dependency graph and filter unreachable declarations * bugfix: recurse into type signatures * positive tests * make ormolu happy * get starting nodes from ExportInfo * make ormolu happy * cosmetic refactoring of DependencyInfo * fix tests & style --- package.yaml | 1 + src/Juvix/Analysis/Scoping/Scoper.hs | 29 ++++- src/Juvix/Analysis/Scoping/ScoperResult.hs | 4 +- src/Juvix/DependencyInfo.hs | 49 ++++++++ src/Juvix/Pipeline.hs | 12 +- src/Juvix/Syntax/Abstract/AbstractResult.hs | 3 +- .../Syntax/Abstract/DependencyBuilder.hs | 116 ++++++++++++++++++ .../Syntax/Abstract/NameDependencyInfo.hs | 10 ++ .../Syntax/MicroJuvix/MicroJuvixResult.hs | 4 +- src/Juvix/Syntax/MicroJuvix/Reachability.hs | 37 ++++++ src/Juvix/Translation/AbstractToMicroJuvix.hs | 5 +- src/Juvix/Translation/ScopedToAbstract.hs | 1 + test/Main.hs | 2 + test/Reachability.hs | 10 ++ test/Reachability/Positive.hs | 94 ++++++++++++++ tests/positive/Reachability/Data/Bool.juvix | 21 ++++ tests/positive/Reachability/Data/Maybe.juvix | 8 ++ tests/positive/Reachability/Data/Nat.juvix | 17 +++ tests/positive/Reachability/Data/Ord.juvix | 7 ++ .../positive/Reachability/Data/Product.juvix | 8 ++ tests/positive/Reachability/M.juvix | 18 +++ tests/positive/Reachability/N.juvix | 13 ++ tests/positive/Reachability/O.juvix | 9 ++ tests/positive/Reachability/juvix.yaml | 0 24 files changed, 469 insertions(+), 9 deletions(-) create mode 100644 src/Juvix/DependencyInfo.hs create mode 100644 src/Juvix/Syntax/Abstract/DependencyBuilder.hs create mode 100644 src/Juvix/Syntax/Abstract/NameDependencyInfo.hs create mode 100644 src/Juvix/Syntax/MicroJuvix/Reachability.hs create mode 100644 test/Reachability.hs create mode 100644 test/Reachability/Positive.hs create mode 100644 tests/positive/Reachability/Data/Bool.juvix create mode 100644 tests/positive/Reachability/Data/Maybe.juvix create mode 100644 tests/positive/Reachability/Data/Nat.juvix create mode 100644 tests/positive/Reachability/Data/Ord.juvix create mode 100644 tests/positive/Reachability/Data/Product.juvix create mode 100644 tests/positive/Reachability/M.juvix create mode 100644 tests/positive/Reachability/N.juvix create mode 100644 tests/positive/Reachability/O.juvix create mode 100644 tests/positive/Reachability/juvix.yaml diff --git a/package.yaml b/package.yaml index 385720e07..fc86caa82 100644 --- a/package.yaml +++ b/package.yaml @@ -21,6 +21,7 @@ dependencies: - base == 4.16.* - blaze-html == 0.9.* - bytestring == 0.11.* +- containers == 0.6.* - directory == 1.3.* - edit-distance == 0.2.* - extra == 1.7.* diff --git a/src/Juvix/Analysis/Scoping/Scoper.hs b/src/Juvix/Analysis/Scoping/Scoper.hs index 52192f14b..620ae51ed 100644 --- a/src/Juvix/Analysis/Scoping/Scoper.hs +++ b/src/Juvix/Analysis/Scoping/Scoper.hs @@ -50,15 +50,16 @@ scopeCheck pr root modules = runReader scopeParameters $ evalState iniScoperState $ do mergeTable (pr ^. Parser.resultTable) - mapM checkTopModule_ modules + checkTopModules modules where - mkResult :: (Parser.InfoTable, (InfoTable, NonEmpty (Module 'Scoped 'ModuleTop))) -> ScoperResult - mkResult (pt, (st, ms)) = + mkResult :: (Parser.InfoTable, (InfoTable, (NonEmpty (Module 'Scoped 'ModuleTop), HashSet NameId))) -> ScoperResult + mkResult (pt, (st, (ms, exp))) = ScoperResult { _resultParserResult = pr, _resultParserTable = pt, _resultScoperTable = st, - _resultModules = ms + _resultModules = ms, + _resultExports = exp } iniScoperState :: ScoperState iniScoperState = @@ -475,6 +476,26 @@ checkInductiveDef ty@InductiveDef {..} = do _inductivePositive = ty ^. inductivePositive } +createExportsTable :: ExportInfo -> HashSet NameId +createExportsTable ei = foldr (HashSet.insert . getNameId) HashSet.empty (HashMap.elems (ei ^. exportSymbols)) + where + getNameId = \case + EntryAxiom r -> getNameRefId (r ^. axiomRefName) + EntryInductive r -> getNameRefId (r ^. inductiveRefName) + EntryFunction r -> getNameRefId (r ^. functionRefName) + EntryConstructor r -> getNameRefId (r ^. constructorRefName) + EntryModule r -> getNameRefId (getModuleRefNameType r) + +checkTopModules :: + forall r. + Members '[Error ScoperError, Reader ScopeParameters, Files, State ScoperState, InfoTableBuilder, Parser.InfoTableBuilder, NameIdGen] r => + NonEmpty (Module 'Parsed 'ModuleTop) -> + Sem r (NonEmpty (Module 'Scoped 'ModuleTop), HashSet NameId) +checkTopModules modules = do + r <- checkTopModule (head modules) + mods <- (r ^. moduleRefModule :|) <$> mapM checkTopModule_ (NonEmpty.tail modules) + return (mods, createExportsTable (r ^. moduleExportInfo)) + checkTopModule_ :: forall r. Members '[Error ScoperError, Reader ScopeParameters, Files, State ScoperState, InfoTableBuilder, Parser.InfoTableBuilder, NameIdGen] r => diff --git a/src/Juvix/Analysis/Scoping/ScoperResult.hs b/src/Juvix/Analysis/Scoping/ScoperResult.hs index ebf4b1d0d..5eb5f19c3 100644 --- a/src/Juvix/Analysis/Scoping/ScoperResult.hs +++ b/src/Juvix/Analysis/Scoping/ScoperResult.hs @@ -4,12 +4,14 @@ import Juvix.Parsing.Parser qualified as Parser import Juvix.Prelude import Juvix.Syntax.Concrete.Language import Juvix.Syntax.Concrete.Scoped.InfoTable qualified as Scoped +import Juvix.Syntax.NameId data ScoperResult = ScoperResult { _resultParserResult :: Parser.ParserResult, _resultParserTable :: Parser.InfoTable, _resultScoperTable :: Scoped.InfoTable, - _resultModules :: NonEmpty (Module 'Scoped 'ModuleTop) + _resultModules :: NonEmpty (Module 'Scoped 'ModuleTop), + _resultExports :: HashSet NameId } makeLenses ''ScoperResult diff --git a/src/Juvix/DependencyInfo.hs b/src/Juvix/DependencyInfo.hs new file mode 100644 index 000000000..0f7d35d12 --- /dev/null +++ b/src/Juvix/DependencyInfo.hs @@ -0,0 +1,49 @@ +module Juvix.DependencyInfo where + +import Data.Graph (Graph, Vertex) +import Data.Graph qualified as Graph +import Data.HashMap.Strict qualified as HashMap +import Data.HashSet qualified as HashSet +import Juvix.Prelude + +-- DependencyInfo is polymorphic to anticipate future use with other identifier +-- types in JuvixCore and further. The graph algorithms don't depend on the +-- exact type of names (the polymorphic type n), so there is no reason to +-- specialise DependencyInfo to any particular name type +data DependencyInfo n = DependencyInfo + { _depInfoGraph :: Graph, + _depInfoNodeFromVertex :: Vertex -> (n, HashSet n), + _depInfoVertexFromName :: n -> Maybe Vertex, + _depInfoReachable :: HashSet n + } + +makeLenses ''DependencyInfo + +createDependencyInfo :: forall n. (Hashable n, Ord n) => HashMap n (HashSet n) -> HashSet n -> DependencyInfo n +createDependencyInfo edges startNames = + DependencyInfo + { _depInfoGraph = graph, + _depInfoNodeFromVertex = \v -> let (_, x, y) = nodeFromVertex v in (x, HashSet.fromList y), + _depInfoVertexFromName = vertexFromName, + _depInfoReachable = reachableNames + } + where + graph :: Graph + nodeFromVertex :: Vertex -> (n, n, [n]) + vertexFromName :: n -> Maybe Vertex + (graph, nodeFromVertex, vertexFromName) = + Graph.graphFromEdges $ + map (\(x, y) -> (x, x, HashSet.toList y)) (HashMap.toList edges) + reachableNames :: HashSet n + reachableNames = + HashSet.fromList $ + map (\v -> case nodeFromVertex v of (_, x, _) -> x) $ + concatMap (Graph.reachable graph) startVertices + startVertices :: [Vertex] + startVertices = mapMaybe vertexFromName (HashSet.toList startNames) + +nameFromVertex :: DependencyInfo n -> Vertex -> n +nameFromVertex depInfo v = fst $ (depInfo ^. depInfoNodeFromVertex) v + +isReachable :: Hashable n => DependencyInfo n -> n -> Bool +isReachable depInfo n = HashSet.member n (depInfo ^. depInfoReachable) diff --git a/src/Juvix/Pipeline.hs b/src/Juvix/Pipeline.hs index 82a47306c..7edb0edc9 100644 --- a/src/Juvix/Pipeline.hs +++ b/src/Juvix/Pipeline.hs @@ -15,6 +15,7 @@ import Juvix.Pipeline.Setup qualified as Setup import Juvix.Prelude import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix +import Juvix.Syntax.MicroJuvix.Reachability qualified as MicroJuvix import Juvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC import Juvix.Translation.MicroJuvixToMonoJuvix qualified as MonoJuvix @@ -78,6 +79,12 @@ upToMicroJuvixTyped :: Sem r MicroJuvix.MicroJuvixTypedResult upToMicroJuvixTyped = upToMicroJuvixArity >=> pipelineMicroJuvixTyped +upToMicroJuvixReachability :: + Members '[Files, NameIdGen, Builtins, Error JuvixError] r => + EntryPoint -> + Sem r MicroJuvix.MicroJuvixTypedResult +upToMicroJuvixReachability = upToMicroJuvixTyped >=> pipelineMicroJuvixReachability + upToMonoJuvix :: Members '[Files, NameIdGen, Builtins, Error JuvixError] r => EntryPoint -> @@ -94,7 +101,7 @@ upToMiniC :: Members '[Files, NameIdGen, Builtins, Error JuvixError] r => EntryPoint -> Sem r MiniC.MiniCResult -upToMiniC = upToMicroJuvixTyped >=> pipelineMiniC +upToMiniC = upToMicroJuvixReachability >=> pipelineMiniC -------------------------------------------------------------------------------- @@ -135,6 +142,9 @@ pipelineMicroJuvixTyped :: pipelineMicroJuvixTyped = mapError (JuvixError @MicroJuvix.TypeCheckerError) . MicroJuvix.entryMicroJuvixTyped +pipelineMicroJuvixReachability :: MicroJuvix.MicroJuvixTypedResult -> Sem r MicroJuvix.MicroJuvixTypedResult +pipelineMicroJuvixReachability = return . MicroJuvix.filterUnreachable + pipelineMonoJuvix :: Members '[Files, NameIdGen] r => MicroJuvix.MicroJuvixTypedResult -> diff --git a/src/Juvix/Syntax/Abstract/AbstractResult.hs b/src/Juvix/Syntax/Abstract/AbstractResult.hs index 15b6953ef..569a50d15 100644 --- a/src/Juvix/Syntax/Abstract/AbstractResult.hs +++ b/src/Juvix/Syntax/Abstract/AbstractResult.hs @@ -14,7 +14,8 @@ import Juvix.Syntax.Abstract.Language data AbstractResult = AbstractResult { _resultScoper :: ScoperResult, _resultTable :: InfoTable, - _resultModules :: NonEmpty TopModule + _resultModules :: NonEmpty TopModule, + _resultExports :: HashSet NameId } makeLenses ''AbstractResult diff --git a/src/Juvix/Syntax/Abstract/DependencyBuilder.hs b/src/Juvix/Syntax/Abstract/DependencyBuilder.hs new file mode 100644 index 000000000..9e6760713 --- /dev/null +++ b/src/Juvix/Syntax/Abstract/DependencyBuilder.hs @@ -0,0 +1,116 @@ +module Juvix.Syntax.Abstract.DependencyBuilder (buildDependencyInfo) where + +import Data.HashMap.Strict qualified as HashMap +import Data.HashSet qualified as HashSet +import Juvix.Prelude +import Juvix.Syntax.Abstract.Language.Extra +import Juvix.Syntax.Abstract.NameDependencyInfo + +-- adjacency set representation +type DependencyGraph = HashMap Name (HashSet Name) + +type StartNodes = HashSet Name + +type VisitedModules = HashSet Name + +type ExportsTable = HashSet NameId + +buildDependencyInfo :: NonEmpty TopModule -> ExportsTable -> NameDependencyInfo +buildDependencyInfo ms tab = + createDependencyInfo graph startNodes + where + startNodes :: StartNodes + graph :: DependencyGraph + (startNodes, graph) = + run $ + evalState (HashSet.empty :: VisitedModules) $ + runState HashSet.empty $ + execState HashMap.empty $ + runReader tab $ + mapM_ goModule ms + +addStartNode :: Member (State StartNodes) r => Name -> Sem r () +addStartNode n = modify (HashSet.insert n) + +addEdge :: Member (State DependencyGraph) r => Name -> Name -> Sem r () +addEdge n1 n2 = + modify + ( HashMap.alter + ( \case + Just ns -> Just (HashSet.insert n2 ns) + Nothing -> Just (HashSet.singleton n2) + ) + n1 + ) + +checkStartNode :: Members '[Reader ExportsTable, State StartNodes] r => Name -> Sem r () +checkStartNode n = do + tab <- ask + when + (HashSet.member (n ^. nameId) tab) + (addStartNode n) + +guardNotVisited :: Member (State VisitedModules) r => Name -> Sem r () -> Sem r () +guardNotVisited n cont = + unlessM + (HashSet.member n <$> get) + (modify (HashSet.insert n) >> cont) + +goModule :: Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r => Module -> Sem r () +goModule m = do + checkStartNode (m ^. moduleName) + mapM_ (goStatement (m ^. moduleName)) (m ^. (moduleBody . moduleStatements)) + +goLocalModule :: Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r => Name -> Module -> Sem r () +goLocalModule mn m = do + addEdge (m ^. moduleName) mn + goModule m + +-- declarations in a module depend on the module, not the other way round (a +-- module is reachable if at least one of the declarations in it is reachable) +goStatement :: Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r => Name -> Statement -> Sem r () +goStatement mn = \case + StatementAxiom ax -> do + checkStartNode (ax ^. axiomName) + addEdge (ax ^. axiomName) mn + goExpression (ax ^. axiomName) (ax ^. axiomType) + StatementForeign {} -> return () + StatementFunction f -> do + checkStartNode (f ^. funDefName) + addEdge (f ^. funDefName) mn + goExpression (f ^. funDefName) (f ^. funDefTypeSig) + mapM_ (goFunctionClause (f ^. funDefName)) (f ^. funDefClauses) + StatementImport m -> guardNotVisited (m ^. moduleName) (goModule m) + StatementLocalModule m -> goLocalModule mn m + StatementInductive i -> do + checkStartNode (i ^. inductiveName) + addEdge (i ^. inductiveName) mn + mapM_ (goFunctionParameter (i ^. inductiveName)) (i ^. inductiveParameters) + goExpression (i ^. inductiveName) (i ^. inductiveType) + mapM_ (goConstructorDef (i ^. inductiveName)) (i ^. inductiveConstructors) + +-- constructors of an inductive type depend on the inductive type, not the other +-- way round +goConstructorDef :: Member (State DependencyGraph) r => Name -> InductiveConstructorDef -> Sem r () +goConstructorDef indName c = do + addEdge (c ^. constructorName) indName + goExpression (c ^. constructorName) (c ^. constructorType) + +goFunctionClause :: Member (State DependencyGraph) r => Name -> FunctionClause -> Sem r () +goFunctionClause p c = goExpression p (c ^. clauseBody) + +goExpression :: Member (State DependencyGraph) r => Name -> Expression -> Sem r () +goExpression p e = case e of + ExpressionIden i -> addEdge p (idenName i) + ExpressionUniverse {} -> return () + ExpressionFunction f -> do + goFunctionParameter p (f ^. funParameter) + goExpression p (f ^. funReturn) + ExpressionApplication (Application l r _) -> do + goExpression p l + goExpression p r + ExpressionLiteral {} -> return () + ExpressionHole {} -> return () + +goFunctionParameter :: Member (State DependencyGraph) r => Name -> FunctionParameter -> Sem r () +goFunctionParameter p param = goExpression p (param ^. paramType) diff --git a/src/Juvix/Syntax/Abstract/NameDependencyInfo.hs b/src/Juvix/Syntax/Abstract/NameDependencyInfo.hs new file mode 100644 index 000000000..018e69e2c --- /dev/null +++ b/src/Juvix/Syntax/Abstract/NameDependencyInfo.hs @@ -0,0 +1,10 @@ +module Juvix.Syntax.Abstract.NameDependencyInfo + ( module Juvix.Syntax.Abstract.NameDependencyInfo, + module Juvix.DependencyInfo, + ) +where + +import Juvix.DependencyInfo +import Juvix.Syntax.Abstract.Name + +type NameDependencyInfo = DependencyInfo Name diff --git a/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs b/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs index 37dc686a0..deff8d395 100644 --- a/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs +++ b/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs @@ -7,13 +7,15 @@ where import Juvix.Pipeline.EntryPoint qualified as E import Juvix.Prelude import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract +import Juvix.Syntax.Abstract.NameDependencyInfo qualified as DepInfo import Juvix.Syntax.MicroJuvix.InfoTable import Juvix.Syntax.MicroJuvix.Language data MicroJuvixResult = MicroJuvixResult { _resultAbstract :: Abstract.AbstractResult, -- _resultTable :: InfoTable, - _resultModules :: NonEmpty Module + _resultModules :: NonEmpty Module, + _resultDepInfo :: DepInfo.NameDependencyInfo } makeLenses ''MicroJuvixResult diff --git a/src/Juvix/Syntax/MicroJuvix/Reachability.hs b/src/Juvix/Syntax/MicroJuvix/Reachability.hs new file mode 100644 index 000000000..61bc42995 --- /dev/null +++ b/src/Juvix/Syntax/MicroJuvix/Reachability.hs @@ -0,0 +1,37 @@ +module Juvix.Syntax.MicroJuvix.Reachability where + +import Juvix.Prelude +import Juvix.Syntax.Abstract.NameDependencyInfo +import Juvix.Syntax.MicroJuvix.Language +import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult qualified as MicroArity +import Juvix.Syntax.MicroJuvix.MicroJuvixResult +import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroTyped + +filterUnreachable :: MicroTyped.MicroJuvixTypedResult -> MicroTyped.MicroJuvixTypedResult +filterUnreachable r = r {MicroTyped._resultModules = modules'} + where + depInfo = r ^. (MicroTyped.resultMicroJuvixArityResult . MicroArity.resultMicroJuvixResult . resultDepInfo) + modules = r ^. MicroTyped.resultModules + modules' = run $ runReader depInfo (mapM goModule modules) + +returnIfReachable :: Member (Reader NameDependencyInfo) r => Name -> a -> Sem r (Maybe a) +returnIfReachable n a = do + depInfo <- ask + return $ if isReachable depInfo n then Just a else Nothing + +goModule :: Member (Reader NameDependencyInfo) r => Module -> Sem r Module +goModule m = do + stmts <- mapM goStatement (body ^. moduleStatements) + return m {_moduleBody = body {_moduleStatements = catMaybes stmts}} + where + body = m ^. moduleBody + +goStatement :: Member (Reader NameDependencyInfo) r => Statement -> Sem r (Maybe Statement) +goStatement s = case s of + StatementInductive i -> returnIfReachable (i ^. inductiveName) s + StatementFunction f -> returnIfReachable (f ^. funDefName) s + StatementForeign {} -> return (Just s) + StatementAxiom ax -> returnIfReachable (ax ^. axiomName) s + StatementInclude i -> do + m <- goModule (i ^. includeModule) + return (Just (StatementInclude i {_includeModule = m})) diff --git a/src/Juvix/Translation/AbstractToMicroJuvix.hs b/src/Juvix/Translation/AbstractToMicroJuvix.hs index 1d7e60c39..5abf373d3 100644 --- a/src/Juvix/Translation/AbstractToMicroJuvix.hs +++ b/src/Juvix/Translation/AbstractToMicroJuvix.hs @@ -10,6 +10,7 @@ import Juvix.Analysis.Termination.Checker import Juvix.Pipeline.EntryPoint qualified as E import Juvix.Prelude import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract +import Juvix.Syntax.Abstract.DependencyBuilder import Juvix.Syntax.Abstract.Language qualified as Abstract import Juvix.Syntax.MicroJuvix.Error import Juvix.Syntax.MicroJuvix.Language @@ -51,7 +52,8 @@ entryMicroJuvix abstractResults = do return MicroJuvixResult { _resultAbstract = abstractResults, - _resultModules = _resultModules' + _resultModules = _resultModules', + _resultDepInfo = depInfo } where topModule = head (abstractResults ^. Abstract.resultModules) @@ -60,6 +62,7 @@ entryMicroJuvix abstractResults = do abstractResults ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination + depInfo = buildDependencyInfo (abstractResults ^. Abstract.resultModules) (abstractResults ^. Abstract.resultExports) goModule :: Members '[State TranslationState, Error TypeCheckerError] r => diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs index e25410864..2d3b086f6 100644 --- a/src/Juvix/Translation/ScopedToAbstract.hs +++ b/src/Juvix/Translation/ScopedToAbstract.hs @@ -29,6 +29,7 @@ unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported" entryAbstract :: Members '[Error ScoperError, Builtins, NameIdGen] r => Scoper.ScoperResult -> Sem r AbstractResult entryAbstract _resultScoper = do (_resultTable, _resultModules) <- runInfoTableBuilder (evalState (ModulesCache mempty) (mapM goTopModule ms)) + let _resultExports = _resultScoper ^. Scoper.resultExports return AbstractResult {..} where ms = _resultScoper ^. Scoper.resultModules diff --git a/test/Main.hs b/test/Main.hs index d780db06a..b72482e35 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -4,6 +4,7 @@ import Arity qualified import BackendC qualified import Base import MonoJuvix qualified +import Reachability qualified import Scope qualified import Termination qualified import TypeCheck qualified @@ -22,6 +23,7 @@ fastTests = Termination.allTests, Arity.allTests, TypeCheck.allTests, + Reachability.allTests, MonoJuvix.allTests ] diff --git a/test/Reachability.hs b/test/Reachability.hs new file mode 100644 index 000000000..ae1002019 --- /dev/null +++ b/test/Reachability.hs @@ -0,0 +1,10 @@ +module Reachability + ( allTests, + ) +where + +import Base +import Reachability.Positive qualified as P + +allTests :: TestTree +allTests = testGroup "Reachability tests" [P.allTests] diff --git a/test/Reachability/Positive.hs b/test/Reachability/Positive.hs new file mode 100644 index 000000000..49b2d405b --- /dev/null +++ b/test/Reachability/Positive.hs @@ -0,0 +1,94 @@ +module Reachability.Positive where + +import Base +import Data.HashSet qualified as HashSet +import Juvix.Pipeline +import Juvix.Syntax.MicroJuvix.Language qualified as Micro +import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as Micro + +data PosTest = PosTest + { _name :: String, + _relDir :: FilePath, + _stdlibMode :: StdlibMode, + _file :: FilePath, + _reachable :: HashSet String + } + +makeLenses ''PosTest + +root :: FilePath +root = "tests/positive" + +testDescr :: PosTest -> TestDescr +testDescr PosTest {..} = + let tRoot = root _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Steps $ \step -> do + cwd <- getCurrentDirectory + entryFile <- canonicalizePath _file + let noStdlib = _stdlibMode == StdlibExclude + entryPoint = + EntryPoint + { _entryPointRoot = cwd, + _entryPointNoTermination = False, + _entryPointNoPositivity = False, + _entryPointNoStdlib = noStdlib, + _entryPointModulePaths = pure entryFile + } + + step "Pipeline up to reachability" + p :: Micro.MicroJuvixTypedResult <- runIO (upToMicroJuvixReachability entryPoint) + + step "Check reachability results" + let names = concatMap getNames (p ^. Micro.resultModules) + mapM_ check names + } + where + check n = assertBool ("unreachable not filtered: " ++ unpack n) (HashSet.member (unpack n) _reachable) + +getNames :: Micro.Module -> [Text] +getNames m = concatMap getDeclName (m ^. (Micro.moduleBody . Micro.moduleStatements)) + where + getDeclName :: Micro.Statement -> [Text] + getDeclName = \case + Micro.StatementInductive i -> [i ^. (Micro.inductiveName . Micro.nameText)] + Micro.StatementFunction f -> [f ^. (Micro.funDefName . Micro.nameText)] + Micro.StatementForeign {} -> [] + Micro.StatementAxiom ax -> [ax ^. (Micro.axiomName . Micro.nameText)] + Micro.StatementInclude i -> getNames (i ^. Micro.includeModule) + +allTests :: TestTree +allTests = + testGroup + "Reachability positive tests" + (map (mkTest . testDescr) tests) + +tests :: [PosTest] +tests = + [ PosTest + "Reachability with modules" + "Reachability" + StdlibInclude + "M.juvix" + ( HashSet.fromList + ["f", "g", "h", "Bool", "Maybe"] + ), + PosTest + "Reachability with modules and standard library" + "Reachability" + StdlibInclude + "N.juvix" + ( HashSet.fromList + ["test", "Unit"] + ), + PosTest + "Reachability with public imports" + "Reachability" + StdlibInclude + "O.juvix" + ( HashSet.fromList + ["f", "g", "h", "k", "Bool", "Maybe"] + ) + ] diff --git a/tests/positive/Reachability/Data/Bool.juvix b/tests/positive/Reachability/Data/Bool.juvix new file mode 100644 index 000000000..a10e90af5 --- /dev/null +++ b/tests/positive/Reachability/Data/Bool.juvix @@ -0,0 +1,21 @@ +module Data.Bool; + inductive Bool { + true : Bool; + false : Bool; + }; + + not : Bool → Bool; + not true ≔ false; + not false ≔ true; + + -- infixr 2 ||; + -- || : Bool → Bool → Bool; + -- || false a ≔ a; + -- || true _ ≔ true; + + -- infixr 2 &&; + -- && : Bool → Bool → Bool; + -- && false _ ≔ false; + -- && true a ≔ a; + +end; diff --git a/tests/positive/Reachability/Data/Maybe.juvix b/tests/positive/Reachability/Data/Maybe.juvix new file mode 100644 index 000000000..384bbc003 --- /dev/null +++ b/tests/positive/Reachability/Data/Maybe.juvix @@ -0,0 +1,8 @@ +module Data.Maybe; + + inductive Maybe (a : Type) { + nothing : Maybe a; + just : a → Maybe a; + } + +end; diff --git a/tests/positive/Reachability/Data/Nat.juvix b/tests/positive/Reachability/Data/Nat.juvix new file mode 100644 index 000000000..fd26414ce --- /dev/null +++ b/tests/positive/Reachability/Data/Nat.juvix @@ -0,0 +1,17 @@ +module Data.Nat; + inductive ℕ { + zero : ℕ; + suc : ℕ → ℕ; + }; + + infixl 6 +; + + : ℕ → ℕ → ℕ; + + zero b ≔ b; + + (suc a) b ≔ suc (a + b); + + infixl 7 *; + * : ℕ → ℕ → ℕ; + * zero b ≔ zero; + * (suc a) b ≔ b + a * b; + +end; diff --git a/tests/positive/Reachability/Data/Ord.juvix b/tests/positive/Reachability/Data/Ord.juvix new file mode 100644 index 000000000..dd85147ef --- /dev/null +++ b/tests/positive/Reachability/Data/Ord.juvix @@ -0,0 +1,7 @@ +module Data.Ord; + inductive Ordering { + LT : Ordering; + EQ : Ordering; + GT : Ordering; + }; +end; diff --git a/tests/positive/Reachability/Data/Product.juvix b/tests/positive/Reachability/Data/Product.juvix new file mode 100644 index 000000000..99ffc1d51 --- /dev/null +++ b/tests/positive/Reachability/Data/Product.juvix @@ -0,0 +1,8 @@ +module Data.Product; + +infixr 2 ×; +inductive × (a : Type) (b : Type) { + , : a → b → a × b; +}; + +end; diff --git a/tests/positive/Reachability/M.juvix b/tests/positive/Reachability/M.juvix new file mode 100644 index 000000000..497a6a72f --- /dev/null +++ b/tests/positive/Reachability/M.juvix @@ -0,0 +1,18 @@ +module M; + +open import Data.Nat; +open import Data.Maybe; +open import Data.Product; +open import Data.Bool; +open import Data.Ord; + +f : Bool -> Bool; +f x := x; + +g : {A : Type} -> A -> Bool -> Bool; +g x y := f y; + +h : {A : Type} -> A -> Maybe Bool; +h x := nothing; + +end; diff --git a/tests/positive/Reachability/N.juvix b/tests/positive/Reachability/N.juvix new file mode 100644 index 000000000..e7b5925b2 --- /dev/null +++ b/tests/positive/Reachability/N.juvix @@ -0,0 +1,13 @@ +module N; + +open import M; +open import Stdlib.Prelude; + +test : {A : Type} -> A -> A; +test x := x; + +inductive Unit { + unit : Unit; +}; + +end; diff --git a/tests/positive/Reachability/O.juvix b/tests/positive/Reachability/O.juvix new file mode 100644 index 000000000..6963c47ff --- /dev/null +++ b/tests/positive/Reachability/O.juvix @@ -0,0 +1,9 @@ +module O; + +open import M public; +open import Stdlib.Prelude; + +k : Bool; +k := true; + +end; diff --git a/tests/positive/Reachability/juvix.yaml b/tests/positive/Reachability/juvix.yaml new file mode 100644 index 000000000..e69de29bb