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

@@ -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,

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

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,