diff --git a/CHANGELOG.md b/CHANGELOG.md index de61a75ea..86499fe16 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Compiler/Opts/ConstantFold.idr b/src/Compiler/Opts/ConstantFold.idr index 87a60f3d7..c26a7820e 100644 --- a/src/Compiler/Opts/ConstantFold.idr +++ b/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' diff --git a/tests/Main.idr b/tests/Main.idr index b61b7aa7b..ca09e30f2 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -310,7 +310,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez) , "futures001" , "bitops" , "casts" - , "constfold", "constfold2" + , "constfold", "constfold2", "constfold3" , "memo" , "newints" , "integers" diff --git a/tests/chez/constfold3/Check.idr b/tests/chez/constfold3/Check.idr new file mode 100644 index 000000000..45c8b639b --- /dev/null +++ b/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" diff --git a/tests/chez/constfold3/Fold.idr b/tests/chez/constfold3/Fold.idr new file mode 100644 index 000000000..4504ae207 --- /dev/null +++ b/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) diff --git a/tests/chez/constfold3/expected b/tests/chez/constfold3/expected new file mode 100644 index 000000000..049d27828 --- /dev/null +++ b/tests/chez/constfold3/expected @@ -0,0 +1,3 @@ +1/1: Building Check (Check.idr) +Main> Constant expression correctly folded +Main> Bye for now! diff --git a/tests/chez/constfold3/input b/tests/chez/constfold3/input new file mode 100644 index 000000000..fc5992c29 --- /dev/null +++ b/tests/chez/constfold3/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/chez/constfold3/run b/tests/chez/constfold3/run new file mode 100644 index 000000000..302d8691d --- /dev/null +++ b/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 +