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

@@ -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.*

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 :: (Parser.InfoTable, (InfoTable, (NonEmpty (Module 'Scoped 'ModuleTop), HashSet NameId))) -> ScoperResult
-    mkResult (pt, (st, ms)) =
+    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 =>

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

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)

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 ->

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

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)

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

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

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}))

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 =>

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

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
     ]
 

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]

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"]
+      )
+  ]

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;

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;

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;

tests/positive/Reachability/Data/Ord.juvix

@@ -0,0 +1,7 @@
+module Data.Ord;
+    inductive Ordering {
+      LT : Ordering;
+      EQ : Ordering;
+      GT : Ordering;
+    };
+end;

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;

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;

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;

tests/positive/Reachability/O.juvix

@@ -0,0 +1,9 @@
+module O;
+
+open import M public;
+open import Stdlib.Prelude;
+
+k : Bool;
+k := true;
+
+end;