-
Notifications
You must be signed in to change notification settings - Fork 53
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
Showing
24 changed files
with
469 additions
and
9 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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})) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.