From 70cbdd0a302b874cccfac0244ecae158cbd7f858 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Wed, 4 Dec 2024 13:39:20 +0100
Subject: [PATCH] Global option `--no-check` (#3224)

The `--no-check` option disables the backend-specific sanity check in
Core (the transformations in `Check/*`, which check the type of main,
use of builtins, etc). This is useful for debugging.
---
 app/GlobalOptions.hs                      | 9 +++++++++
 src/Juvix/Compiler/Core/Pipeline.hs       | 8 ++++++--
 src/Juvix/Compiler/Pipeline/EntryPoint.hs | 3 +++
 3 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs
index 471717c691..23fa62c0f9 100644
--- a/app/GlobalOptions.hs
+++ b/app/GlobalOptions.hs
@@ -24,6 +24,7 @@ data GlobalOptions = GlobalOptions
     _globalNoPositivity :: Bool,
     _globalNoCoverage :: Bool,
     _globalNoStdlib :: Bool,
+    _globalNoCheck :: Bool,
     _globalUnrollLimit :: Int,
     _globalNumThreads :: NumThreads,
     _globalFieldSize :: Maybe Natural,
@@ -72,6 +73,7 @@ defaultGlobalOptions =
       _globalLogLevel = LogLevelProgress,
       _globalNoCoverage = False,
       _globalNoStdlib = False,
+      _globalNoCheck = False,
       _globalUnrollLimit = defaultUnrollLimit,
       _globalFieldSize = Nothing,
       _globalDevShowThreadIds = False,
@@ -162,6 +164,11 @@ parseGlobalFlags = do
                 <> intercalate " < " [show l | l <- allElements @LogLevel]
             )
       )
+  _globalNoCheck <-
+    switch
+      ( long "dev-no-check"
+          <> help "[DEV] Disable input sanity check in Core"
+      )
   _globalShowNameIds <-
     switch
       ( long "show-name-ids"
@@ -211,6 +218,7 @@ entryPointFromGlobalOptions root mainFile opts = do
         _entryPointNoPositivity = opts ^. globalNoPositivity,
         _entryPointNoCoverage = opts ^. globalNoCoverage,
         _entryPointNoStdlib = opts ^. globalNoStdlib,
+        _entryPointNoCheck = opts ^. globalNoCheck,
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
@@ -232,6 +240,7 @@ entryPointFromGlobalOptionsNoFile root opts = do
         _entryPointNoPositivity = opts ^. globalNoPositivity,
         _entryPointNoCoverage = opts ^. globalNoCoverage,
         _entryPointNoStdlib = opts ^. globalNoStdlib,
+        _entryPointNoCheck = opts ^. globalNoCheck,
         _entryPointUnrollLimit = opts ^. globalUnrollLimit,
         _entryPointGenericOptions = project opts,
         _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir,
diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs
index 51d4d50658..f762bc7278 100644
--- a/src/Juvix/Compiler/Core/Pipeline.hs
+++ b/src/Juvix/Compiler/Core/Pipeline.hs
@@ -7,7 +7,7 @@ where
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation
-import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint)
+import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint, entryPointNoCheck)
 
 toTypechecked :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
 toTypechecked = mapReader fromEntryPoint . applyTransformations toTypecheckTransformations
@@ -19,7 +19,11 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio
 -- | Perform transformations on stored Core necessary before the translation to
 -- Core.Stripped
 toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module
-toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId)
+toStripped checkId md = do
+  noCheck <- asks (^. entryPointNoCheck)
+  let checkId' = if noCheck then IdentityTrans else checkId
+  mapReader fromEntryPoint $
+    applyTransformations (toStrippedTransformations checkId') md
 
 -- | Perform transformations on stored Core necessary before the translation to VampIR
 toVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
index cf23d9892b..df487703b4 100644
--- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs
+++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs
@@ -33,6 +33,8 @@ data EntryPoint = EntryPoint
     _entryPointTarget :: Maybe Target,
     _entryPointDebug :: Bool,
     _entryPointUnsafe :: Bool,
+    -- | Skip the correctness check in the Core pipeline part.
+    _entryPointNoCheck :: Bool,
     _entryPointUnrollLimit :: Int,
     _entryPointOptimizationLevel :: Int,
     _entryPointInliningDepth :: Int,
@@ -76,6 +78,7 @@ defaultEntryPointNoFile pkg root =
       _entryPointTarget = Nothing,
       _entryPointDebug = False,
       _entryPointUnsafe = False,
+      _entryPointNoCheck = False,
       _entryPointUnrollLimit = defaultUnrollLimit,
       _entryPointOptimizationLevel = defaultOptimizationLevel,
       _entryPointInliningDepth = defaultInliningDepth,