Check for unsupported builtins (#2757)

* Closes #2743
anoma · Apr 29, 2024 · 55dbcca · 55dbcca
1 parent 844f302
commit 55dbcca
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 32 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)