[ codegen ] get rid of trivial let statements (#2961)

CHANGELOG.md

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

src/Compiler/Opts/ConstantFold.idr

@@ -69,6 +69,11 @@ lookup fc (MkVar p) rho = case go p rho of
       Z => Left (MkVar First)
       S i' => bimap later weaken (go (dropLater p) (Wk ws' rho))
 
+replace : CExp vars -> Bool
+replace (CLocal _ _)   = True
+replace (CPrimVal _ _) = True
+replace _              = False
+
 -- constant folding of primitive functions
 -- if a primitive function is applied to only constant
 -- then replace with the result
@@ -83,11 +88,9 @@ constFold rho (CLam fc x y)
   = CLam fc x $ constFold (wk (mkSizeOf [x]) rho) y
 constFold rho (CLet fc x inl y z) =
     let val = constFold rho y
-     in case val of
-        CPrimVal _ _ => if inl == YesInline
-            then constFold (val :: rho) z
-            else CLet fc x inl val (constFold (wk (mkSizeOf [x]) rho) z)
-        _ => CLet fc x inl val (constFold (wk (mkSizeOf [x]) rho) z)
+     in if replace val
+          then constFold (val :: rho) z
+          else CLet fc x inl val (constFold (wk (mkSizeOf [x]) rho) z)
 constFold rho (CApp fc (CRef fc2 n) [x]) =
   if n == NS typesNS (UN $ Basic "prim__integerToNat")
      then case constFold rho x of

tests/Main.idr

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

tests/chez/constfold2/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-manyToSmall" `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/constfold2/Fold.idr

@@ -0,0 +1,27 @@
+import Data.Nat
+
+%default total
+
+record Small where
+  constructor S
+  value : Nat
+  {auto 0 prf : LTE value 20}
+
+Show Small where show = show . value
+
+record Smaller where
+  constructor XS
+  value : Nat
+  {auto 0 prf : LTE value 10}
+
+-- This is the identity function
+toSmall : Smaller -> Small
+toSmall (XS v @{prf}) = S v @{transitive prf %search}
+
+-- This is again the identity function
+manyToSmall : List Smaller -> List Small
+manyToSmall [] = []
+manyToSmall (x::xs) = toSmall x :: manyToSmall xs
+
+main : IO ()
+main = printLn $ manyToSmall [XS 1, XS 2, XS 3]

tests/chez/constfold2/expected

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

tests/chez/constfold2/input

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

tests/chez/constfold2/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
+