mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
3cbf6f5cb6
- Closes #2039 - Closes #2055 - Depends on #2053 Changes in this pr: - Local modules are removed (flattened) in the translation abstract -> internal. - In the translation abstract -> internal we group definitions in mutually recursive blocks. These blocks can contain function definitions and type definitions. Previously we only handled functions. - The translation of Internal has been enhanced to handle these mutually recursive blocks. - Some improvements the pretty printer for internal (e.g. we now print builtin tags properly). - A "hack" that puts the builtin bool definition at the beginning of a module if present. This was the easiest way to handle the implicit dependency of the builtin stringToNat with bool in the internal-to-core translation. - A moderately sized test defining a simple lambda calculus involving and an evaluator for it. This example showcases mutually recursive types in juvix. --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
90 lines
2.8 KiB
Haskell
90 lines
2.8 KiB
Haskell
module Reachability.Positive where
|
|
|
|
import Base
|
|
import Data.HashSet qualified as HashSet
|
|
import Juvix.Compiler.Internal.Language qualified as Internal
|
|
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal
|
|
|
|
data PosTest = PosTest
|
|
{ _name :: String,
|
|
_relDir :: Path Rel Dir,
|
|
_stdlibMode :: StdlibMode,
|
|
_file :: Path Rel File,
|
|
_reachable :: HashSet String
|
|
}
|
|
|
|
makeLenses ''PosTest
|
|
|
|
root :: Path Abs Dir
|
|
root = relToProject $(mkRelDir "tests/positive")
|
|
|
|
testDescr :: PosTest -> TestDescr
|
|
testDescr PosTest {..} =
|
|
let tRoot = root <//> _relDir
|
|
file' = tRoot <//> _file
|
|
in TestDescr
|
|
{ _testName = _name,
|
|
_testRoot = tRoot,
|
|
_testAssertion = Steps $ \step -> do
|
|
let noStdlib = _stdlibMode == StdlibExclude
|
|
entryPoint <-
|
|
set entryPointNoStdlib noStdlib
|
|
<$> defaultEntryPointCwdIO file'
|
|
|
|
step "Pipeline up to reachability"
|
|
p :: Internal.InternalTypedResult <- snd <$> runIO' entryPoint upToInternalReachability
|
|
|
|
step "Check reachability results"
|
|
let names = concatMap getNames (p ^. Internal.resultModules)
|
|
mapM_ check names
|
|
}
|
|
where
|
|
check n = assertBool ("unreachable not filtered: " ++ unpack n) (HashSet.member (unpack n) _reachable)
|
|
|
|
getNames :: Internal.Module -> [Text]
|
|
getNames m = concatMap getDeclName (m ^. (Internal.moduleBody . Internal.moduleStatements))
|
|
where
|
|
getDeclName :: Internal.Statement -> [Text]
|
|
getDeclName = \case
|
|
Internal.StatementMutual (Internal.MutualBlock f) -> map getMutualName (toList f)
|
|
Internal.StatementAxiom ax -> [ax ^. (Internal.axiomName . Internal.nameText)]
|
|
Internal.StatementInclude i -> getNames (i ^. Internal.includeModule)
|
|
getMutualName :: Internal.MutualStatement -> Text
|
|
getMutualName = \case
|
|
Internal.StatementFunction f -> f ^. Internal.funDefName . Internal.nameText
|
|
Internal.StatementInductive f -> f ^. Internal.inductiveName . Internal.nameText
|
|
|
|
allTests :: TestTree
|
|
allTests =
|
|
testGroup
|
|
"Reachability positive tests"
|
|
(map (mkTest . testDescr) tests)
|
|
|
|
tests :: [PosTest]
|
|
tests =
|
|
[ PosTest
|
|
"Reachability with modules"
|
|
$(mkRelDir "Reachability")
|
|
StdlibInclude
|
|
$(mkRelFile "M.juvix")
|
|
( HashSet.fromList
|
|
["f", "g", "h", "Bool", "Maybe"]
|
|
),
|
|
PosTest
|
|
"Reachability with modules and standard library"
|
|
$(mkRelDir "Reachability")
|
|
StdlibInclude
|
|
$(mkRelFile "N.juvix")
|
|
( HashSet.fromList
|
|
["test", "Unit", "Bool", "Nat", "Int"]
|
|
),
|
|
PosTest
|
|
"Reachability with public imports"
|
|
$(mkRelDir "Reachability")
|
|
StdlibInclude
|
|
$(mkRelFile "O.juvix")
|
|
( HashSet.fromList
|
|
["f", "g", "h", "k", "Bool", "Maybe", "Nat"]
|
|
)
|
|
]
|