Skip to content

Commit

Permalink
[ codegen ] get rid of trivial let statements (#2961)
Browse files Browse the repository at this point in the history
  • Loading branch information
stefan-hoeck committed May 6, 2023
1 parent a00b7ee commit e34b5a6
Show file tree
Hide file tree
Showing 8 changed files with 67 additions and 6 deletions.
2 changes: 2 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
13 changes: 8 additions & 5 deletions src/Compiler/Opts/ConstantFold.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/Main.idr
Original file line number Diff line number Diff line change
Expand Up @@ -310,7 +310,7 @@ chezTests = MkTestPool "Chez backend" [] (Just Chez)
, "futures001"
, "bitops"
, "casts"
, "constfold"
, "constfold", "constfold2"
, "memo"
, "newints"
, "integers"
Expand Down
19 changes: 19 additions & 0 deletions tests/chez/constfold2/Check.idr
Original file line number Diff line number Diff line change
@@ -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"
27 changes: 27 additions & 0 deletions tests/chez/constfold2/Fold.idr
Original file line number Diff line number Diff line change
@@ -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]
3 changes: 3 additions & 0 deletions tests/chez/constfold2/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
1/1: Building Check (Check.idr)
Main> Constant expression correctly folded
Main> Bye for now!
2 changes: 2 additions & 0 deletions tests/chez/constfold2/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
:exec main
:q
5 changes: 5 additions & 0 deletions tests/chez/constfold2/run
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit e34b5a6

Please sign in to comment.