mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-23 22:22:07 +03:00
[ performance ] constant fold prim__integerToNat
This commit is contained in:
parent
7eebeff905
commit
0543779200
@ -5,6 +5,7 @@ import Core.Context
|
|||||||
import Core.Context.Log
|
import Core.Context.Log
|
||||||
import Core.Primitives
|
import Core.Primitives
|
||||||
import Core.Value
|
import Core.Value
|
||||||
|
import Core.Name
|
||||||
import Data.List
|
import Data.List
|
||||||
import Data.Vect
|
import Data.Vect
|
||||||
|
|
||||||
@ -87,6 +88,13 @@ constFold rho (CLet fc x inlineOK y z) =
|
|||||||
then constFold (val :: rho) z
|
then constFold (val :: rho) z
|
||||||
else CLet fc x inlineOK val (constFold (wk (mkSizeOf [x]) rho) z)
|
else CLet fc x inlineOK val (constFold (wk (mkSizeOf [x]) rho) z)
|
||||||
_ => CLet fc x inlineOK val (constFold (wk (mkSizeOf [x]) rho) z)
|
_ => CLet fc x inlineOK 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
|
||||||
|
CPrimVal fc3 (BI v) =>
|
||||||
|
if v >= 0 then CPrimVal fc3 (BI v) else CPrimVal fc3 (BI 0)
|
||||||
|
v => CApp fc (CRef fc2 n) [v]
|
||||||
|
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 (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 (CCon fc x y tag xs) = CCon fc x y tag $ constFold rho <$> xs
|
||||||
constFold rho (COp {arity} fc fn xs) =
|
constFold rho (COp {arity} fc fn xs) =
|
||||||
|
@ -7,7 +7,9 @@ path = "build/exec/fold_app/fold.ss"
|
|||||||
|
|
||||||
mainLine : String -> Bool
|
mainLine : String -> Bool
|
||||||
mainLine str =
|
mainLine str =
|
||||||
("(define Main-main(" `isPrefixOf` str) && (" 99))))" `isSuffixOf` str)
|
("(define Main-main(" `isPrefixOf` str) &&
|
||||||
|
(" 99)" `isInfixOf` str) &&
|
||||||
|
not ("prim__integerToNat" `isInfixOf` str)
|
||||||
|
|
||||||
main : IO ()
|
main : IO ()
|
||||||
main = do
|
main = do
|
||||||
|
@ -1,2 +1,5 @@
|
|||||||
main : IO ()
|
main : IO ()
|
||||||
main = printLn (the Bits8 0xff + 100)
|
main = do
|
||||||
|
printLn (the Bits8 0xff + 100)
|
||||||
|
printLn (the Nat 12345)
|
||||||
|
printLn (the Nat (-12345))
|
||||||
|
Loading…
Reference in New Issue
Block a user