Constant folding (#2450)

* Closes #2154 
* Evaluates closed applications with value arguments when the result
type is zero-order. For example, `3 + 4` is evaluated to `7`, and `id 3`
is evaluated to `3`, but `id id` is not evaluated because the target
type is not zero-order (it's a function type).

src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs

@@ -9,18 +9,21 @@ import Juvix.Compiler.Core.Language
 -- | Call graph type
 type IdentDependencyInfo = DependencyInfo Symbol
 
+createCallGraphMap :: InfoTable -> HashMap Symbol (HashSet Symbol)
+createCallGraphMap tab =
+  fmap
+    ( \IdentifierInfo {..} ->
+        HashSet.map (\Ident {..} -> _identSymbol) $
+          getIdents (lookupIdentifierNode tab _identifierSymbol)
+    )
+    (tab ^. infoIdentifiers)
+
 -- | Compute the call graph
 createCallGraph :: InfoTable -> IdentDependencyInfo
 createCallGraph tab = createDependencyInfo graph startVertices
   where
     graph :: HashMap Symbol (HashSet Symbol)
-    graph =
+    graph = createCallGraphMap tab
-      fmap
-        ( \IdentifierInfo {..} ->
-            HashSet.map (\Ident {..} -> _identSymbol) $
-              getIdents (lookupIdentifierNode tab _identifierSymbol)
-        )
-        (tab ^. infoIdentifiers)
 
     startVertices :: HashSet Symbol
     startVertices = HashSet.fromList syms
@@ -53,3 +56,45 @@ createSymbolDependencyInfo tab = createDependencyInfo graph startVertices
 
 recursiveIdents :: InfoTable -> HashSet Symbol
 recursiveIdents = nodesOnCycles . createCallGraph
+
+-- | identifiers from which some recursive identifier can be reached
+recursiveIdentsClosure :: InfoTable -> HashSet Symbol
+recursiveIdentsClosure tab =
+  -- unfortunately, there is no Graph library function which would allow to
+  -- compute this in linear time; hence, we implement this directly
+  run
+    . evalState (mempty :: HashSet Symbol)
+    $ foldM (dfs mempty) mempty (HashMap.keys graph)
+  where
+    graph = createCallGraphMap tab
+
+    dfs :: (Member (State (HashSet Symbol)) r) => HashSet Symbol -> HashSet Symbol -> Symbol -> Sem r (HashSet Symbol)
+    dfs path acc sym = do
+      visited <- get
+      if
+          | HashSet.member sym visited ->
+              return acc
+          | otherwise -> do
+              let path' = HashSet.insert sym path
+                  acc' =
+                    if
+                        | any (`HashSet.member` path') chlds ->
+                            HashSet.insert sym acc
+                        | otherwise ->
+                            acc
+              modify' (HashSet.insert sym)
+              acc'' <- foldM (dfs path') acc' chlds
+              if
+                  | any (`HashSet.member` acc'') chlds ->
+                      return $ HashSet.insert sym acc''
+                  | otherwise ->
+                      return acc''
+      where
+        chlds = fromJust $ HashMap.lookup sym graph
+
+-- | Complement of recursiveIdentsClosure
+nonRecursiveIdents :: InfoTable -> HashSet Symbol
+nonRecursiveIdents tab =
+  HashSet.difference
+    (HashSet.fromList (HashMap.keys (tab ^. infoIdentifiers)))
+    (recursiveIdentsClosure tab)

src/Juvix/Compiler/Core/Evaluator.hs

@@ -23,7 +23,8 @@ import Text.Read qualified as T
 
 data EvalOptions = EvalOptions
   { _evalOptionsNormalize :: Bool,
-    _evalOptionsNoFailure :: Bool
+    _evalOptionsNoFailure :: Bool,
+    _evalOptionsSilent :: Bool
   }
 
 makeLenses ''EvalOptions
@@ -32,7 +33,8 @@ defaultEvalOptions :: EvalOptions
 defaultEvalOptions =
   EvalOptions
     { _evalOptionsNormalize = False,
-      _evalOptionsNoFailure = False
+      _evalOptionsNoFailure = False,
+      _evalOptionsSilent = False
     }
 
 data EvalError = EvalError
@@ -278,7 +280,11 @@ geval opts herr ctx env0 = eval' env0
         traceOp :: [Node] -> Node
         traceOp = unary $ \msg ->
           let !v = eval' env msg
-           in unsafePerformIO (hPutStrLn herr (printNode v) >> return v)
+           in if
+                  | opts ^. evalOptionsSilent ->
+                      v
+                  | otherwise ->
+                      unsafePerformIO (hPutStrLn herr (printNode v) >> return v)
         {-# INLINE traceOp #-}
     {-# INLINE applyBuiltin #-}
 

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -93,6 +93,43 @@ isType tab bl node = case node of
         isTypeConstr tab (ii ^. identifierType)
   _ -> isType' node
 
+isZeroOrderType' :: HashSet Symbol -> InfoTable -> Type -> Bool
+isZeroOrderType' foinds tab = \case
+  NPi {} -> False
+  NDyn {} -> False
+  NTyp TypeConstr {..} ->
+    isFirstOrderInductive' foinds tab _typeConstrSymbol
+      && all (isZeroOrderType' foinds tab) _typeConstrArgs
+  ty -> isType' ty
+
+isFirstOrderType' :: HashSet Symbol -> InfoTable -> Type -> Bool
+isFirstOrderType' foinds tab ty = case ty of
+  NVar {} -> True
+  NPi Pi {..} ->
+    isZeroOrderType' foinds tab (_piBinder ^. binderType)
+      && isFirstOrderType' foinds tab _piBody
+  NUniv {} -> True
+  NPrim {} -> True
+  NTyp {} -> isZeroOrderType' foinds tab ty
+  NDyn {} -> False
+  _ -> assert (not (isType' ty)) False
+
+isFirstOrderInductive' :: HashSet Symbol -> InfoTable -> Symbol -> Bool
+isFirstOrderInductive' foinds tab sym
+  | HashSet.member sym foinds = True
+  | otherwise = case lookupInductiveInfo' tab sym of
+      Nothing -> False
+      Just ii ->
+        all
+          (isFirstOrderType' (HashSet.insert sym foinds) tab . (^. constructorType) . lookupConstructorInfo tab)
+          (ii ^. inductiveConstructors)
+
+isFirstOrderType :: InfoTable -> Type -> Bool
+isFirstOrderType = isFirstOrderType' mempty
+
+isZeroOrderType :: InfoTable -> Type -> Bool
+isZeroOrderType = isZeroOrderType' mempty
+
 -- | True for nodes whose evaluation immediately returns a value, i.e.,
 -- no reduction or memory allocation in the runtime is required.
 isImmediate :: InfoTable -> Node -> Bool
@@ -329,6 +366,14 @@ substVar idx t = umapN go
         | _varIndex > k + idx -> mkVar _varInfo (_varIndex - 1)
       _ -> n
 
+removeClosures :: Node -> Node
+removeClosures = dmap go
+  where
+    go :: Node -> Node
+    go = \case
+      Closure {..} -> substEnv _closureEnv _closureNode
+      node -> node
+
 etaExpand :: [Type] -> Node -> Node
 etaExpand [] n = n
 etaExpand argtys n =

src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs

@@ -17,6 +17,8 @@ kFreeVarsInfo = Proxy
 
 makeLenses ''FreeVarsInfo
 
+-- | Computes free variable info for each subnode. Assumption: no subnode is a
+-- closure.
 computeFreeVarsInfo :: Node -> Node
 computeFreeVarsInfo = umap go
   where
@@ -47,3 +49,6 @@ getFreeVarsInfo = fromJust . Info.lookup kFreeVarsInfo . getInfo
 
 freeVarOccurrences :: Index -> Node -> Int
 freeVarOccurrences idx n = fromMaybe 0 (Map.lookup idx (getFreeVarsInfo n ^. infoFreeVars))
+
+isClosed :: Node -> Bool
+isClosed node = sum (Map.elems (getFreeVarsInfo node ^. infoFreeVars)) == 0

src/Juvix/Compiler/Core/Transformation/Optimize/ConstantFolding.hs

@@ -0,0 +1,75 @@
+module Juvix.Compiler.Core.Transformation.Optimize.ConstantFolding (constantFolding, constantFolding') where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Core.Data.IdentDependencyInfo
+import Juvix.Compiler.Core.Evaluator
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.FreeVarsInfo as Info
+import Juvix.Compiler.Core.Transformation.Base
+
+convertNode :: HashSet Symbol -> InfoTable -> Node -> Node
+convertNode nonRecSyms tab = umap go
+  where
+    go :: Node -> Node
+    go node = case node of
+      NBlt BuiltinApp {..}
+        | Info.isClosed node
+            && _builtinAppOp /= OpFail
+            && _builtinAppOp /= OpTrace
+            && _builtinAppOp /= OpSeq
+            && all isNonRecValue _builtinAppArgs ->
+            doEval node
+      NApp {}
+        | Info.isClosed node ->
+            case h of
+              NIdt Ident {..}
+                | HashSet.member _identSymbol nonRecSyms
+                    && evalAllowed
+                    && length args == ii ^. identifierArgsNum
+                    && length tyargs == ii ^. identifierArgsNum
+                    && isZeroOrderType tab tgt'
+                    && all isNonRecValue args ->
+                    doEval node
+                where
+                  ii = lookupIdentifierInfo tab _identSymbol
+                  evalAllowed = maybe True (^. pragmaEval) (ii ^. identifierPragmas . pragmasEval)
+                  (tyargs, tgt) = unfoldPi' (ii ^. identifierType)
+                  n = length (takeWhile (isTypeConstr tab) tyargs)
+                  tys = reverse (take n args)
+                  tgt' = substs tys (shift (-(length tyargs - n)) tgt)
+              _ -> node
+        where
+          (h, args) = unfoldApps' node
+      _ -> node
+
+    isNonRecValue :: Node -> Bool
+    isNonRecValue node = case node of
+      NCst {} -> True
+      NIdt Ident {..} ->
+        HashSet.member _identSymbol nonRecSyms
+      NCtr Constr {..} -> all isNonRecValue _constrArgs
+      NApp {} ->
+        let (h, args) = unfoldApps' node
+         in isNonRecValue h && all isType' args
+      _ -> isType' node
+
+    doEval :: Node -> Node
+    doEval = removeClosures . geval opts stderr (tab ^. identContext) []
+      where
+        opts =
+          defaultEvalOptions
+            { _evalOptionsNoFailure = True,
+              _evalOptionsSilent = True
+            }
+
+constantFolding' :: HashSet Symbol -> InfoTable -> InfoTable
+constantFolding' nonRecSyms tab =
+  mapAllNodes
+    ( removeInfo kFreeVarsInfo
+        . convertNode nonRecSyms tab
+        . computeFreeVarsInfo
+    )
+    tab
+
+constantFolding :: InfoTable -> InfoTable
+constantFolding tab = constantFolding' (nonRecursiveIdents tab) tab

src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Main.hs

@@ -5,6 +5,7 @@ import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.Optimize.CaseFolding
 import Juvix.Compiler.Core.Transformation.Optimize.CasePermutation
+import Juvix.Compiler.Core.Transformation.Optimize.ConstantFolding
 import Juvix.Compiler.Core.Transformation.Optimize.FilterUnreachable
 import Juvix.Compiler.Core.Transformation.Optimize.Inlining
 import Juvix.Compiler.Core.Transformation.Optimize.LambdaFolding
@@ -18,17 +19,30 @@ optimize' CoreOptions {..} tab =
   filterUnreachable
     . compose
       (4 * _optOptimizationLevel)
-      ( doSimplification 2
+      ( doConstantFolding
+          . doSimplification 2
           . doInlining
           . doSimplification 1
           . specializeArgs
       )
+    . doConstantFolding
     . letFolding
     $ tab
   where
     recs :: HashSet Symbol
     recs = recursiveIdents tab
 
+    nonRecs :: HashSet Symbol
+    nonRecs = nonRecursiveIdents tab
+
+    doConstantFolding :: InfoTable -> InfoTable
+    doConstantFolding tab' = constantFolding' nonRecs' tab'
+      where
+        nonRecs' =
+          if
+              | _optOptimizationLevel > 1 -> nonRecursiveIdents tab'
+              | otherwise -> nonRecs
+
     doInlining :: InfoTable -> InfoTable
     doInlining tab' = inlining' _optInliningDepth recs' tab'
       where

src/Juvix/Data/Pragmas.hs

@@ -52,6 +52,11 @@ newtype PragmaSpecialiseBy = PragmaSpecialiseBy
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
+newtype PragmaEval = PragmaEval
+  { _pragmaEval :: Bool
+  }
+  deriving stock (Show, Eq, Ord, Data, Generic)
+
 data Pragmas = Pragmas
   { _pragmasInline :: Maybe PragmaInline,
     _pragmasUnroll :: Maybe PragmaUnroll,
@@ -60,7 +65,8 @@ data Pragmas = Pragmas
     _pragmasFormat :: Maybe PragmaFormat,
     _pragmasSpecialise :: Maybe PragmaSpecialise,
     _pragmasSpecialiseArgs :: Maybe PragmaSpecialiseArgs,
-    _pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy
+    _pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy,
+    _pragmasEval :: Maybe PragmaEval
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
@@ -70,6 +76,7 @@ makeLenses ''PragmaPublic
 makeLenses ''PragmaFormat
 makeLenses ''PragmaSpecialiseArgs
 makeLenses ''PragmaSpecialiseBy
+makeLenses ''PragmaEval
 makeLenses ''Pragmas
 
 instance Hashable PragmaInline
@@ -90,6 +97,8 @@ instance Hashable PragmaSpecialise
 
 instance Hashable PragmaSpecialiseBy
 
+instance Hashable PragmaEval
+
 instance Hashable Pragmas
 
 instance FromJSON Pragmas where
@@ -115,6 +124,7 @@ instance FromJSON Pragmas where
         specby <- keyMay "specialise-by" parseSpecialiseBy
         specby' <- keyMay "specialize-by" parseSpecialiseBy
         let _pragmasSpecialiseBy = specby <|> specby'
+        _pragmasEval <- keyMay "eval" parseEval
         return Pragmas {..}
 
       parseInline :: Parse YamlError PragmaInline
@@ -161,6 +171,11 @@ instance FromJSON Pragmas where
         _pragmaFormat <- asBool
         return PragmaFormat {..}
 
+      parseEval :: Parse YamlError PragmaEval
+      parseEval = do
+        _pragmaEval <- asBool
+        return PragmaEval {..}
+
       parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg
       parseSpecialiseArg =
         (SpecialiseArgNum <$> asIntegral)
@@ -199,6 +214,7 @@ instance Semigroup Pragmas where
         _pragmasArgNames = p2 ^. pragmasArgNames,
         _pragmasPublic = p2 ^. pragmasPublic,
         _pragmasFormat = p2 ^. pragmasFormat <|> p1 ^. pragmasFormat,
+        _pragmasEval = p2 ^. pragmasEval <|> p1 ^. pragmasEval,
         _pragmasSpecialise = p2 ^. pragmasSpecialise <|> p1 ^. pragmasSpecialise,
         _pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs,
         _pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy
@@ -214,7 +230,8 @@ instance Monoid Pragmas where
         _pragmasFormat = Nothing,
         _pragmasSpecialise = Nothing,
         _pragmasSpecialiseArgs = Nothing,
-        _pragmasSpecialiseBy = Nothing
+        _pragmasSpecialiseBy = Nothing,
+        _pragmasEval = Nothing
       }
 
 adjustPragmaInline :: Int -> PragmaInline -> PragmaInline

test/Asm/Compile/Base.hs

@@ -11,8 +11,8 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Pipeline qualified as Pipeline
 import Runtime.Base qualified as Runtime
 
-asmCompileAssertion' :: InfoTable -> Path Abs File -> Path Abs File -> Text -> (String -> IO ()) -> Assertion
+asmCompileAssertion' :: Int -> InfoTable -> Path Abs File -> Path Abs File -> Text -> (String -> IO ()) -> Assertion
-asmCompileAssertion' tab mainFile expectedFile stdinText step = do
+asmCompileAssertion' optLevel tab mainFile expectedFile stdinText step = do
   step "Generate C code"
   case run $ runReader asmOpts $ runError @JuvixError $ Pipeline.asmToMiniC' tab of
     Left e -> do
@@ -23,7 +23,7 @@ asmCompileAssertion' tab mainFile expectedFile stdinText step = do
         ( \dirPath -> do
             let cFile = dirPath <//> replaceExtension' ".c" (filename mainFile)
             TIO.writeFile (toFilePath cFile) _resultCCode
-            Runtime.clangAssertion cFile expectedFile stdinText step
+            Runtime.clangAssertion optLevel cFile expectedFile stdinText step
         )
   where
     -- TODO: In the future, the target supplied here might need to correspond to
@@ -39,4 +39,4 @@ asmCompileAssertion mainFile expectedFile stdinText step = do
   s <- readFile (toFilePath mainFile)
   case runParser (toFilePath mainFile) s of
     Left err -> assertFailure (show err)
-    Right tab -> asmCompileAssertion' tab mainFile expectedFile stdinText step
+    Right tab -> asmCompileAssertion' 3 tab mainFile expectedFile stdinText step

test/Compilation.hs

@@ -5,4 +5,4 @@ import Compilation.Negative qualified as N
 import Compilation.Positive qualified as P
 
 allTests :: TestTree
-allTests = testGroup "Juvix compilation pipeline tests" [P.allTests, N.allTests]
+allTests = testGroup "Juvix compilation pipeline tests" [P.allTestsNoOptimize, P.allTests, N.allTests]

test/Compilation/Base.hs

@@ -13,12 +13,13 @@ data CompileAssertionMode
   | EvalAndCompile
 
 compileAssertion ::
+  Int ->
   CompileAssertionMode ->
   Path Abs File ->
   Path Abs File ->
   (String -> IO ()) ->
   Assertion
-compileAssertion mode mainFile expectedFile step = do
+compileAssertion optLevel mode mainFile expectedFile step = do
   step "Translate to JuvixCore"
   entryPoint <- defaultEntryPointCwdIO mainFile
   tab <- (^. Core.coreResultTable) . snd <$> runIO' entryPoint upToCore
@@ -26,7 +27,7 @@ compileAssertion mode mainFile expectedFile step = do
     Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
     Right tab' -> do
       let evalAssertion = coreEvalAssertion' EvalModePlain tab' mainFile expectedFile step
-          compileAssertion' stdinText = coreCompileAssertion' tab' mainFile expectedFile stdinText step
+          compileAssertion' stdinText = coreCompileAssertion' optLevel tab' mainFile expectedFile stdinText step
       case mode of
         EvalOnly -> evalAssertion
         CompileOnly stdinText -> compileAssertion' stdinText

test/Compilation/Positive.hs

@@ -13,28 +13,31 @@ data PosTest = PosTest
 
 makeLenses ''PosTest
 
-fromTest :: PosTest -> TestTree
-fromTest = mkTest . toTestDescr
-
 root :: Path Abs Dir
 root = relToProject $(mkRelDir "tests/Compilation/positive/")
 
-toTestDescr :: PosTest -> TestDescr
+toTestDescr :: Int -> PosTest -> TestDescr
-toTestDescr PosTest {..} =
+toTestDescr optLevel PosTest {..} =
   let tRoot = _dir
       file' = _file
       expected' = _expectedFile
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ compileAssertion _assertionMode file' expected'
+          _testAssertion = Steps $ compileAssertion optLevel _assertionMode file' expected'
         }
 
 allTests :: TestTree
 allTests =
   testGroup
     "Juvix compilation pipeline positive tests"
-    (map (mkTest . toTestDescr) tests)
+    (map (mkTest . toTestDescr 3) tests)
+
+allTestsNoOptimize :: TestTree
+allTestsNoOptimize =
+  testGroup
+    "Juvix compilation pipeline positive tests (no optimization)"
+    (map (mkTest . toTestDescr 0) tests)
 
 posTest' :: CompileAssertionMode -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
 posTest' _assertionMode _name rdir rfile routfile =
@@ -374,5 +377,10 @@ tests =
       "Test063: Coercions"
       $(mkRelDir ".")
       $(mkRelFile "test063.juvix")
-      $(mkRelFile "out/test063.out")
+      $(mkRelFile "out/test063.out"),
+    posTest
+      "Test064: Constant folding"
+      $(mkRelDir ".")
+      $(mkRelFile "test064.juvix")
+      $(mkRelFile "out/test064.out")
   ]

test/Core/Compile/Base.hs

@@ -38,21 +38,24 @@ toTestDescr Test {..} =
         }
 
 coreCompileAssertion' ::
+  Int ->
   InfoTable ->
   Path Abs File ->
   Path Abs File ->
   Text ->
   (String -> IO ()) ->
   Assertion
-coreCompileAssertion' tab mainFile expectedFile stdinText step = do
+coreCompileAssertion' optLevel tab mainFile expectedFile stdinText step = do
   step "Translate to JuvixAsm"
-  case run $ runReader defaultCoreOptions $ runError $ toStripped' tab of
+  case run $ runReader opts $ runError $ toStripped' tab of
     Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
     Right tab0 -> do
       assertBool "Check info table" (checkInfoTable tab0)
       let tab' = Asm.fromCore $ Stripped.fromCore $ tab0
       length (fromText (Asm.ppPrint tab' tab') :: String) `seq`
-        Asm.asmCompileAssertion' tab' mainFile expectedFile stdinText step
+        Asm.asmCompileAssertion' optLevel tab' mainFile expectedFile stdinText step
+  where
+    opts = defaultCoreOptions {_optOptimizationLevel = optLevel}
 
 coreCompileAssertion ::
   Path Abs File ->
@@ -70,4 +73,4 @@ coreCompileAssertion mainFile expectedFile stdinText step = do
       expected <- TIO.readFile (toFilePath expectedFile)
       assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) "" expected
     Right (tabIni, Just node) ->
-      coreCompileAssertion' (setupMainFunction tabIni node) mainFile expectedFile stdinText step
+      coreCompileAssertion' 3 (setupMainFunction tabIni node) mainFile expectedFile stdinText step

test/Examples/Positive.hs

@@ -24,7 +24,7 @@ toTestDescr PosTest {..} =
   TestDescr
     { _testRoot = _dir,
       _testName = _name,
-      _testAssertion = Steps $ compileAssertion (CompileOnly _stdin) _file _expectedFile
+      _testAssertion = Steps $ compileAssertion 3 (CompileOnly _stdin) _file _expectedFile
     }
 
 allTests :: TestTree

test/Runtime/Base.hs

@@ -50,8 +50,8 @@ readProcess cmd args stdinText =
         return r
     )
 
-clangAssertion :: Path Abs File -> Path Abs File -> Text -> ((String -> IO ()) -> Assertion)
+clangAssertion :: Int -> Path Abs File -> Path Abs File -> Text -> ((String -> IO ()) -> Assertion)
-clangAssertion inputFile expectedFile stdinText step = do
+clangAssertion optLevel inputFile expectedFile stdinText step = do
   step "Check clang and wasmer are on path"
   assertCmdExists $(mkRelFile "clang")
   assertCmdExists $(mkRelFile "wasmer")
@@ -68,12 +68,12 @@ clangAssertion inputFile expectedFile stdinText step = do
       executeNative outputFile = readProcess (toFilePath outputFile) [] stdinText
 
   step "Compile C to WASM32-WASI"
-  actualWasm <- clangCompile (wasiArgs sysrootPath) inputFile $(mkRelFile "Program.wasm") executeWasm step
+  actualWasm <- clangCompile (wasiArgs optLevel sysrootPath) inputFile $(mkRelFile "Program.wasm") executeWasm step
   step "Compare expected and actual program output"
   assertEqDiffText ("check: WASM output = " <> toFilePath expectedFile) actualWasm expected
 
   step "Compile C to native 64-bit code"
-  actualNative <- clangCompile native64Args inputFile $(mkRelFile "Program") executeNative step
+  actualNative <- clangCompile (native64Args optLevel) inputFile $(mkRelFile "Program") executeNative step
   step "Compare expected and actual program output"
   assertEqDiffText ("check: native output = " <> toFilePath expectedFile) actualNative expected
 
@@ -95,13 +95,13 @@ commonArgs outputFile =
     runtimeInclude :: FilePath
     runtimeInclude = $(makeRelativeToProject "runtime/include" >>= strToExp)
 
-native64Args :: Path Abs File -> Path Abs File -> [String]
+native64Args :: Int -> Path Abs File -> Path Abs File -> [String]
-native64Args outputFile inputFile =
+native64Args optLevel outputFile inputFile =
   commonArgs outputFile
     <> [ "-DARCH_NATIVE64",
          "-DAPI_LIBC",
          "-m64",
-         "-O3",
+         "-O" <> show optLevel,
          "-L",
          juvixLibraryDir,
          toFilePath inputFile,
@@ -111,12 +111,12 @@ native64Args outputFile inputFile =
     juvixLibraryDir :: FilePath
     juvixLibraryDir = $(makeRelativeToProject "runtime/_build.native64-debug" >>= strToExp)
 
-wasiArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
+wasiArgs :: Int -> Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
-wasiArgs sysrootPath outputFile inputFile =
+wasiArgs optLevel sysrootPath outputFile inputFile =
   commonArgs outputFile
     <> [ "-DARCH_WASM32",
          "-DAPI_WASI",
-         "-O3",
+         "-O" <> show optLevel,
          "-nodefaultlibs",
          "--target=wasm32-wasi",
          "--sysroot",

test/Runtime/Positive.hs

@@ -20,10 +20,11 @@ testDescr PosTest {..} =
   let tRoot = root <//> _relDir
       file' = tRoot <//> _file
       expected' = tRoot <//> _expectedFile
+      optLevel :: Int = 3
    in TestDescr
         { _testName = _name,
           _testRoot = tRoot,
-          _testAssertion = Steps $ clangAssertion file' expected' ""
+          _testAssertion = Steps $ clangAssertion optLevel file' expected' ""
         }
 
 allTests :: TestTree

tests/Compilation/positive/out/test064.out

@@ -0,0 +1 @@
+37

tests/Compilation/positive/test064.juvix

@@ -0,0 +1,42 @@
+-- Constant folding
+module test064;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Fail as Debug;
+
+{-# inline: false #-}
+f (x y : Nat) : Nat := x + y;
+
+{-# inline: false #-}
+g (x : Bool) : Bool := if x (Debug.failwith "a") true;
+
+{-# inline: false #-}
+h (x : Bool) : Bool := if (g x) false true;
+
+{-# inline: false, eval: false #-}
+j (x : Nat) : Nat := x + 0;
+
+sum : Nat -> Nat
+  | zero := 0
+  | k@(suc n) := k + sum n;
+
+even : Nat -> Bool
+  | zero := true
+  | (suc n) := odd n;
+
+odd : Nat -> Bool
+  | zero := false
+  | (suc n) := even n;
+
+terminating
+loop : Nat := loop;
+
+{-# inline: false #-}
+even' : Nat -> Bool := even;
+
+main : Nat :=
+  sum 3
+    + case even' 6 || g true || h true of {
+        | true := if (g false) (f 1 2 + sum 7 + j 0) 0
+        | false := f (3 + 4) (f 0 8) + loop
+      };