[ codegen ] constant fold believe_me

CHANGELOG.md

@@ -83,7 +83,7 @@
   `TTImp.ProcessDef.genRunTime`. This allows us to track when incomplete `case`
   blocks get the runtime error added.
 
-* Constant folding of trivial let statements.
+* Constant folding of trivial let statements and `believe_me`.
 
 ### Library changes
 

src/Compiler/Opts/ConstantFold.idr

@@ -100,6 +100,7 @@ constFold rho (CApp fc (CRef fc2 n) [x]) =
      else CApp fc (CRef fc2 n) [constFold rho x]
 constFold rho (CApp fc x xs) = CApp fc (constFold rho x) (constFold rho <$> xs)
 constFold rho (CCon fc x y tag xs) = CCon fc x y tag $ constFold rho <$> xs
+constFold rho (COp fc BelieveMe [CErased _, CErased _ , x]) = constFold rho x
 constFold rho (COp {arity} fc fn xs) =
     let xs' = map (constFold rho) xs
         e = constRight fc fn xs'

tests/Main.idr

@@ -310,7 +310,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez)
     , "futures001"
     , "bitops"
     , "casts"
-    , "constfold", "constfold2"
+    , "constfold", "constfold2", "constfold3"
     , "memo"
     , "newints"
     , "integers"

tests/chez/constfold3/Check.idr

@@ -0,0 +1,19 @@
+import Data.List
+import Data.String
+import System.File
+
+path : String
+path = "build/exec/fold_app/fold.ss"
+
+mainLine : String -> Bool
+mainLine str =
+  ("(define Main-main" `isPrefixOf` str) &&
+  not ("Main-unsafeMkSingleton" `isInfixOf` str)
+
+main : IO ()
+main = do
+  Right str <- readFile path
+    | Left err => putStrLn "Error when reading \{path}"
+  case any mainLine (lines str) of
+    True  => putStrLn "Constant expression correctly folded"
+    False => putStrLn "Failed to fold constant expression"

tests/chez/constfold3/Fold.idr

@@ -0,0 +1,12 @@
+public export
+data Singleton : {0 a : Type} -> (x : a) -> Type where
+  MkSingleton : (x : a) -> Singleton x
+
+Show a => Show (Singleton {a} v) where show (MkSingleton v) = show v
+
+export
+unsafeMkSingleton : (y : a) -> Singleton {a} x
+unsafeMkSingleton y = believe_me (MkSingleton y)
+
+main : IO ()
+main = printLn $ unsafeMkSingleton {x = 12} (S Z)

tests/chez/constfold3/expected

@@ -0,0 +1,3 @@
+1/1: Building Check (Check.idr)
+Main> Constant expression correctly folded
+Main> Bye for now!

tests/chez/constfold3/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/constfold3/run

@@ -0,0 +1,5 @@
+rm -rf build
+
+$1 --no-banner --no-color --quiet -o fold Fold.idr
+$1 --no-banner --no-color --console-width 0 Check.idr < input
+