1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-12 14:28:08 +03:00

Check for recursive inductive types in the GEB pipeline (#1909)

Currently, only recursion in functions is checked. This PR also adds
some utilities (TypeDependencyInfo) that will be useful for issue #1907.

---------

Co-authored-by: janmasrovira <janmasrovira@gmail.com>
This commit is contained in:
Łukasz Czajka 2023-03-23 14:08:10 +01:00 committed by GitHub
parent 839093cdbd
commit 906720cb02
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 56 additions and 10 deletions

View File

@ -0,0 +1,29 @@
module Juvix.Compiler.Core.Data.TypeDependencyInfo where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Extra.Utils
import Juvix.Compiler.Core.Language
type TypeDependencyInfo = DependencyInfo Symbol
createTypeDependencyInfo :: InfoTable -> TypeDependencyInfo
createTypeDependencyInfo tab = createDependencyInfo graph startVertices
where
graph :: HashMap Symbol (HashSet Symbol)
graph =
HashSet.fromList . (^.. inductiveSymbols)
<$> HashMap.filter (isNothing . (^. inductiveBuiltin)) (tab ^. infoInductives)
constructorTypes :: SimpleFold ConstructorInfo Type
constructorTypes = constructorType . to typeArgs . each
inductiveSymbols :: SimpleFold InductiveInfo Symbol
inductiveSymbols = inductiveConstructors . each . constructorTypes . nodeInductives
startVertices :: HashSet Symbol
startVertices = HashSet.fromList syms
syms :: [Symbol]
syms = map (^. inductiveSymbol) (HashMap.elems (tab ^. infoInductives))

View File

@ -55,6 +55,13 @@ nodeIdents f = ufoldA reassemble go
NIdt i -> NIdt <$> f i
n -> pure n
nodeInductives :: Traversal' Node Symbol
nodeInductives f = ufoldA reassemble go
where
go = \case
NTyp ty -> NTyp <$> traverseOf typeConstrSymbol f ty
n -> pure n
-- | Prism for NRec
_NRec :: SimpleFold Node LetRec
_NRec f = \case

View File

@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Transformation.CheckGeb where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Core.Data.IdentDependencyInfo
import Juvix.Compiler.Core.Data.TypeDependencyInfo
import Juvix.Compiler.Core.Error
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.LocationInfo (getInfoLocation)
@ -10,6 +11,7 @@ import Juvix.Compiler.Core.Transformation.Base
checkGeb :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
checkGeb tab =
checkNoRecursion
>> checkNoRecursiveTypes
>> mapAllNodesM checkNoIO tab
>> mapAllNodesM checkBuiltins tab
>> mapAllNodesM checkTypes tab
@ -68,16 +70,24 @@ checkGeb tab =
_ -> return node
checkNoRecursion :: Sem r ()
checkNoRecursion
| isCyclic (createIdentDependencyInfo tab) =
throw
CoreError
{ _coreErrorMsg = "recursion not supported for the GEB target",
_coreErrorNode = Nothing,
_coreErrorLoc = defaultLoc
}
| otherwise =
return ()
checkNoRecursion =
when (isCyclic (createIdentDependencyInfo tab)) $
throw
CoreError
{ _coreErrorMsg = "recursion not supported for the GEB target",
_coreErrorNode = Nothing,
_coreErrorLoc = defaultLoc
}
checkNoRecursiveTypes :: Sem r ()
checkNoRecursiveTypes =
when (isCyclic (createTypeDependencyInfo tab)) $
throw
CoreError
{ _coreErrorMsg = "recursive types not supported for the GEB target",
_coreErrorNode = Nothing,
_coreErrorLoc = defaultLoc
}
dynamicTypeError :: Node -> Maybe Location -> CoreError
dynamicTypeError node loc =