diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 7fe898343d..4e179d91d3 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/src/Juvix/Compiler/Core/Language/Builtins.hs @@ -113,8 +113,13 @@ builtinIsFoldable = \case OpRandomEcPoint -> False builtinIsCairo :: BuiltinOp -> Bool -builtinIsCairo = \case - OpPoseidonHash -> True - OpEc -> True - OpRandomEcPoint -> True - _ -> False +builtinIsCairo op = op `elem` builtinsCairo + +builtinsString :: [BuiltinOp] +builtinsString = [OpStrConcat, OpStrToInt, OpShow] + +builtinsCairo :: [BuiltinOp] +builtinsCairo = [OpPoseidonHash, OpEc, OpRandomEcPoint] + +builtinsAnoma :: [BuiltinOp] +builtinsAnoma = [OpAnomaGet] diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs b/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs index 1575880b17..c15dfa589b 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs @@ -10,4 +10,4 @@ checkAnoma md = do checkMainExists md checkNoAxioms md mapAllNodesM checkNoIO md - mapAllNodesM (checkBuiltins' [OpStrConcat, OpStrToInt, OpShow] [PrimString]) md + mapAllNodesM (checkBuiltins' (builtinsString ++ builtinsCairo) [PrimString, PrimField]) md diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs index 87da4b4269..1898ffab49 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs @@ -55,9 +55,6 @@ checkBuiltins allowUntypedFail = dmapRM go throw $ unsupportedError "strings" node (getInfoLocation _typePrimInfo) NBlt BuiltinApp {..} -> case _builtinAppOp of - OpShow -> throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo) - OpStrConcat -> throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo) - OpStrToInt -> throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo) OpTrace -> throw $ unsupportedError "tracing" node (getInfoLocation _builtinAppInfo) OpFail | not allowUntypedFail -> do let ty = Info.getInfoType _builtinAppInfo @@ -67,7 +64,15 @@ checkBuiltins allowUntypedFail = dmapRM go return $ Recur node OpFail -> do return $ End node - _ -> return $ Recur node + _ + | _builtinAppOp `elem` builtinsString -> + throw $ unsupportedError "strings" node (getInfoLocation _builtinAppInfo) + | _builtinAppOp `elem` builtinsCairo -> + throw $ unsupportedError "cairo" node (getInfoLocation _builtinAppInfo) + | _builtinAppOp `elem` builtinsAnoma -> + throw $ unsupportedError "anoma" node (getInfoLocation _builtinAppInfo) + | otherwise -> + return $ Recur node _ -> return $ Recur node checkBuiltins' :: forall r. (Member (Error CoreError) r) => [BuiltinOp] -> [Primitive] -> Node -> Sem r Node diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs index 03d7081886..2184a43748 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Cairo.hs @@ -12,7 +12,7 @@ checkCairo md = do checkMainType checkNoAxioms md mapAllNodesM checkNoIO md - mapAllNodesM (checkBuiltins' [OpStrConcat, OpStrToInt, OpShow] [PrimString]) md + mapAllNodesM (checkBuiltins' builtinsString [PrimString]) md where checkMainType :: Sem r () checkMainType = diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs b/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs index 1ac2859742..0c3b0cffb7 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs @@ -9,33 +9,39 @@ import Juvix.Data.PPOutput checkExec :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module checkExec md = do checkNoAxioms md - case md ^. moduleInfoTable . infoMain of - Nothing -> - throw - CoreError - { _coreErrorMsg = ppOutput "no `main` function", - _coreErrorNode = Nothing, - _coreErrorLoc = defaultLoc - } - Just sym -> - case ii ^. identifierType of - NPi {} -> + checkMainExists md + checkMainType + mapAllNodesM (checkBuiltins' (builtinsCairo ++ builtinsAnoma) []) md + where + checkMainType :: Sem r () + checkMainType = + case md ^. moduleInfoTable . infoMain of + Nothing -> throw CoreError - { _coreErrorMsg = ppOutput "`main` cannot have a function type for this target", + { _coreErrorMsg = ppOutput "no `main` function", _coreErrorNode = Nothing, - _coreErrorLoc = loc + _coreErrorLoc = defaultLoc } - ty - | isTypeConstr md ty -> + Just sym -> + case ii ^. identifierType of + NPi {} -> throw CoreError - { _coreErrorMsg = ppOutput "`main` cannot be a type for this target", + { _coreErrorMsg = ppOutput "`main` cannot have a function type for this target", _coreErrorNode = Nothing, _coreErrorLoc = loc } - _ -> - return md - where - ii = lookupIdentifierInfo md sym - loc = fromMaybe defaultLoc (ii ^. identifierLocation) + ty + | isTypeConstr md ty -> + throw + CoreError + { _coreErrorMsg = ppOutput "`main` cannot be a type for this target", + _coreErrorNode = Nothing, + _coreErrorLoc = loc + } + _ -> + return () + where + ii = lookupIdentifierInfo md sym + loc = fromMaybe defaultLoc (ii ^. identifierLocation)