From dbd24f2f939b1fe769356438d9e932027f95ccce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Tue, 4 Apr 2023 11:58:36 +0200
Subject: [PATCH] Check for the executable (WASM/native) pipeline prerequisites
 (#1970)

* Closes #1959
---
 .../Compiler/Core/Data/TransformationId.hs    |  3 +-
 .../Core/Data/TransformationId/Parser.hs      |  4 ++
 src/Juvix/Compiler/Core/Transformation.hs     |  2 +
 .../Compiler/Core/Transformation/CheckExec.hs | 40 +++++++++++++++++++
 test/Compilation/Base.hs                      |  2 +-
 test/Compilation/Negative.hs                  |  6 ++-
 tests/Compilation/negative/test004.juvix      |  6 +++
 7 files changed, 60 insertions(+), 3 deletions(-)
 create mode 100644 src/Juvix/Compiler/Core/Transformation/CheckExec.hs
 create mode 100644 tests/Compilation/negative/test004.juvix

diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs
index 8012f1c10..276c836cf 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs
@@ -18,6 +18,7 @@ data TransformationId
   | EtaExpandApps
   | DisambiguateNames
   | CheckGeb
+  | CheckExec
   | LetFolding
   deriving stock (Data, Bounded, Enum, Show)
 
@@ -53,7 +54,7 @@ toEvalTransformations = [EtaExpandApps, MatchToCase, NatToInt, ConvertBuiltinTyp
 
 toStrippedTransformations :: [TransformationId]
 toStrippedTransformations =
-  toEvalTransformations ++ [LambdaLetRecLifting, LetFolding, TopEtaExpand, MoveApps, RemoveTypeArgs]
+  toEvalTransformations ++ [CheckExec, LambdaLetRecLifting, LetFolding, TopEtaExpand, MoveApps, RemoveTypeArgs]
 
 toGebTransformations :: [TransformationId]
 toGebTransformations = toEvalTransformations ++ [CheckGeb, LetRecLifting, LetFolding, UnrollRecursion, ComputeTypeInfo]
diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
index f6ead86e2..8a7e15727 100644
--- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
+++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
@@ -82,6 +82,7 @@ transformationText = \case
   UnrollRecursion -> strUnrollRecursion
   DisambiguateNames -> strDisambiguateNames
   CheckGeb -> strCheckGeb
+  CheckExec -> strCheckExec
   LetFolding -> strLetFolding
 
 parsePipeline :: MonadParsec e Text m => m PipelineId
@@ -147,5 +148,8 @@ strDisambiguateNames = "disambiguate-names"
 strCheckGeb :: Text
 strCheckGeb = "check-geb"
 
+strCheckExec :: Text
+strCheckExec = "check-exec"
+
 strLetFolding :: Text
 strLetFolding = "let-folding"
diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs
index 57415fbf2..b9102255d 100644
--- a/src/Juvix/Compiler/Core/Transformation.hs
+++ b/src/Juvix/Compiler/Core/Transformation.hs
@@ -12,6 +12,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.CheckExec
 import Juvix.Compiler.Core.Transformation.CheckGeb
 import Juvix.Compiler.Core.Transformation.ComputeTypeInfo
 import Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes
@@ -48,4 +49,5 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       EtaExpandApps -> return . etaExpansionApps
       DisambiguateNames -> return . disambiguateNames
       CheckGeb -> mapError (JuvixError @CoreError) . checkGeb
+      CheckExec -> mapError (JuvixError @CoreError) . checkExec
       LetFolding -> return . letFolding
diff --git a/src/Juvix/Compiler/Core/Transformation/CheckExec.hs b/src/Juvix/Compiler/Core/Transformation/CheckExec.hs
new file mode 100644
index 000000000..fd52cba3f
--- /dev/null
+++ b/src/Juvix/Compiler/Core/Transformation/CheckExec.hs
@@ -0,0 +1,40 @@
+module Juvix.Compiler.Core.Transformation.CheckExec where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Data.PPOutput
+
+checkExec :: forall r. Member (Error CoreError) r => InfoTable -> Sem r InfoTable
+checkExec tab =
+  case tab ^. infoMain of
+    Nothing -> return tab
+    Just sym ->
+      case ii ^. identifierType of
+        NPi {} ->
+          throw
+            CoreError
+              { _coreErrorMsg = ppOutput "`main` cannot have a function type for this target",
+                _coreErrorNode = Nothing,
+                _coreErrorLoc = loc
+              }
+        ty
+          | isTypeConstr tab ty ->
+              throw
+                CoreError
+                  { _coreErrorMsg = ppOutput "`main` cannot be a type for this target",
+                    _coreErrorNode = Nothing,
+                    _coreErrorLoc = loc
+                  }
+        _ ->
+          return tab
+      where
+        ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
+        loc = fromMaybe defaultLoc (ii ^. identifierLocation)
+
+        mockFile :: Path Abs File
+        mockFile = $(mkAbsFile "/core-to-exec")
+
+        defaultLoc :: Interval
+        defaultLoc = singletonInterval (mkInitialLoc mockFile)
diff --git a/test/Compilation/Base.hs b/test/Compilation/Base.hs
index 8597d1764..9a0408081 100644
--- a/test/Compilation/Base.hs
+++ b/test/Compilation/Base.hs
@@ -43,6 +43,6 @@ compileErrorAssertion mainFile step = do
   cwd <- getCurrentDir
   let entryPoint = defaultEntryPoint cwd mainFile
   tab <- (^. Core.coreResultTable) . snd <$> runIO' entryPoint upToCore
-  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toEval' tab of
+  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toStripped' tab of
     Left _ -> assertBool "" True
     Right _ -> assertFailure "no error"
diff --git a/test/Compilation/Negative.hs b/test/Compilation/Negative.hs
index 347b8ad04..711bc9fc2 100644
--- a/test/Compilation/Negative.hs
+++ b/test/Compilation/Negative.hs
@@ -41,5 +41,9 @@ tests =
     NegTest
       "Pattern matching coverage in lambdas"
       $(mkRelDir ".")
-      $(mkRelFile "test003.juvix")
+      $(mkRelFile "test003.juvix"),
+    NegTest
+      "The definition of main has a function type"
+      $(mkRelDir ".")
+      $(mkRelFile "test004.juvix")
   ]
diff --git a/tests/Compilation/negative/test004.juvix b/tests/Compilation/negative/test004.juvix
new file mode 100644
index 000000000..04a732e90
--- /dev/null
+++ b/tests/Compilation/negative/test004.juvix
@@ -0,0 +1,6 @@
+module test004;
+
+open import Stdlib.Prelude;
+
+main : Nat -> Nat;
+main x := x;