mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-08-16 16:50:46 +03:00
[ perf ] manually eta-expand unsaturated io_bind calls (#2785)
This commit is contained in:
parent
f96c5ca596
commit
85bb822f3b
@ -89,32 +89,32 @@ prim__getStr : PrimIO String
|
||||
prim__putStr : String -> PrimIO ()
|
||||
|
||||
||| Output a string to stdout without a trailing newline.
|
||||
export
|
||||
%inline export
|
||||
putStr : HasIO io => String -> io ()
|
||||
putStr str = primIO (prim__putStr str)
|
||||
|
||||
||| Output a string to stdout with a trailing newline.
|
||||
export
|
||||
putStrLn : HasIO io => String -> io ()
|
||||
%inline putStrLn : HasIO io => String -> io ()
|
||||
putStrLn str = putStr (prim__strAppend str "\n")
|
||||
|
||||
||| Read one line of input from stdin, without the trailing newline.
|
||||
export
|
||||
%inline export
|
||||
getLine : HasIO io => io String
|
||||
getLine = primIO prim__getStr
|
||||
|
||||
||| Write one single-byte character to stdout.
|
||||
export
|
||||
%inline export
|
||||
putChar : HasIO io => Char -> io ()
|
||||
putChar c = primIO (prim__putChar c)
|
||||
|
||||
||| Write one multi-byte character to stdout, with a trailing newline.
|
||||
export
|
||||
%inline export
|
||||
putCharLn : HasIO io => Char -> io ()
|
||||
putCharLn c = putStrLn (prim__cast_CharString c)
|
||||
|
||||
||| Read one single-byte character from stdin.
|
||||
export
|
||||
%inline export
|
||||
getChar : HasIO io => io Char
|
||||
getChar = primIO prim__getChar
|
||||
|
||||
@ -136,11 +136,11 @@ threadWait : (1 threadID : ThreadID) -> IO ()
|
||||
threadWait threadID = fromPrim (prim__threadWait threadID)
|
||||
|
||||
||| Output something showable to stdout, without a trailing newline.
|
||||
export
|
||||
print : (HasIO io, Show a) => a -> io ()
|
||||
%inline export
|
||||
print : HasIO io => Show a => a -> io ()
|
||||
print = putStr . show
|
||||
|
||||
||| Output something showable to stdout, with a trailing newline.
|
||||
export
|
||||
printLn : (HasIO io, Show a) => a -> io ()
|
||||
%inline export
|
||||
printLn : HasIO io => Show a => a -> io ()
|
||||
printLn = putStrLn . show
|
||||
|
@ -87,7 +87,7 @@ interface Functor f where
|
||||
||| in a parameterised type.
|
||||
||| @ f the parameterised type
|
||||
||| @ func the function to apply
|
||||
public export
|
||||
%inline public export
|
||||
(<$>) : Functor f => (func : a -> b) -> f a -> f b
|
||||
(<$>) func x = map func x
|
||||
|
||||
@ -95,23 +95,22 @@ public export
|
||||
||| everything of type 'a' in a parameterised type.
|
||||
||| @ f the parameterised type
|
||||
||| @ func the function to apply
|
||||
public export
|
||||
%inline public export
|
||||
(<&>) : Functor f => f a -> (func : a -> b) -> f b
|
||||
(<&>) x func = map func x
|
||||
|
||||
||| Run something for effects, replacing the return value with a given parameter.
|
||||
public export
|
||||
%inline public export
|
||||
(<$) : Functor f => b -> f a -> f b
|
||||
(<$) b = map (const b)
|
||||
|
||||
||| Flipped version of `<$`.
|
||||
public export
|
||||
%inline public export
|
||||
($>) : Functor f => f a -> b -> f b
|
||||
($>) fa b = map (const b) fa
|
||||
|
||||
||| Run something for effects, throwing away the return value.
|
||||
%inline
|
||||
public export
|
||||
%inline public export
|
||||
ignore : Functor f => f a -> f ()
|
||||
ignore = map (const ())
|
||||
|
||||
@ -217,12 +216,12 @@ interface Applicative m => Monad m where
|
||||
%allow_overloads (>>=)
|
||||
|
||||
||| Right-to-left monadic bind, flipped version of `>>=`.
|
||||
public export
|
||||
%inline public export
|
||||
(=<<) : Monad m => (a -> m b) -> m a -> m b
|
||||
(=<<) = flip (>>=)
|
||||
|
||||
||| Sequencing of effectful composition
|
||||
public export
|
||||
%inline public export
|
||||
(>>) : Monad m => m () -> Lazy (m b) -> m b
|
||||
a >> b = a >>= \_ => b
|
||||
|
||||
@ -302,13 +301,13 @@ interface Foldable t where
|
||||
foldMap f = foldr ((<+>) . f) neutral
|
||||
|
||||
||| Combine each element of a structure into a monoid.
|
||||
public export
|
||||
%inline public export
|
||||
concat : Monoid a => Foldable t => t a -> a
|
||||
concat = foldMap id
|
||||
|
||||
||| Combine into a monoid the collective results of applying a function to each
|
||||
||| element of a structure.
|
||||
public export
|
||||
%inline public export
|
||||
concatMap : Monoid m => Foldable t => (a -> m) -> t a -> m
|
||||
concatMap = foldMap
|
||||
|
||||
@ -366,13 +365,13 @@ namespace Bool
|
||||
|
||||
||| The disjunction of the collective results of applying a predicate to all
|
||||
||| elements of a structure. `any` short-circuits from left to right.
|
||||
public export
|
||||
%inline public export
|
||||
any : Foldable t => (a -> Bool) -> t a -> Bool
|
||||
any = foldMap @{%search} @{Any}
|
||||
|
||||
||| The conjunction of the collective results of applying a predicate to all
|
||||
||| elements of a structure. `all` short-circuits from left to right.
|
||||
public export
|
||||
%inline public export
|
||||
all : Foldable t => (a -> Bool) -> t a -> Bool
|
||||
all = foldMap @{%search} @{All}
|
||||
|
||||
@ -478,12 +477,12 @@ public export
|
||||
||| ```
|
||||
|||
|
||||
||| Note: In Haskell, `choice` is called `asum`.
|
||||
public export
|
||||
%inline public export
|
||||
choice : Alternative f => Foldable t => t (Lazy (f a)) -> f a
|
||||
choice = force . concat @{Lazy.MonoidAlternative}
|
||||
|
||||
||| A fused version of `choice` and `map`.
|
||||
public export
|
||||
%inline public export
|
||||
choiceMap : Alternative f => Foldable t => (a -> f b) -> t a -> f b
|
||||
choiceMap = foldMap @{%search} @{MonoidAlternative}
|
||||
|
||||
@ -534,7 +533,7 @@ sequence : Applicative f => Traversable t => t (f a) -> f (t a)
|
||||
sequence = traverse id
|
||||
|
||||
||| Like `traverse` but with the arguments flipped.
|
||||
public export
|
||||
%inline public export
|
||||
for : Applicative f => Traversable t => t a -> (a -> f b) -> f (t b)
|
||||
for = flip traverse
|
||||
|
||||
|
@ -3,6 +3,7 @@ module Compiler.CompileExpr
|
||||
import Core.Case.CaseTree
|
||||
import public Core.CompileExpr
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.Env
|
||||
import Core.Name
|
||||
import Core.Normalise
|
||||
@ -455,6 +456,7 @@ mutual
|
||||
then
|
||||
let env : SubstCEnv args vars
|
||||
= mkSubst 0 scr pos args in
|
||||
do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"
|
||||
pure $ Just (substs env !(toCExpTree n sc))
|
||||
else -- let bind the scrutinee, and substitute the
|
||||
-- name into the RHS
|
||||
@ -465,8 +467,9 @@ mutual
|
||||
{inner=vars}
|
||||
{ns = [MN "eff" 0]}
|
||||
(mkSizeOf _) (mkSizeOf _) sc'
|
||||
pure $ Just (CLet fc (MN "eff" 0) False scr
|
||||
(substs env scope))
|
||||
let tm = CLet fc (MN "eff" 0) False scr (substs env scope)
|
||||
log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}"
|
||||
pure (Just tm)
|
||||
_ => pure Nothing -- there's a normal match to do
|
||||
where
|
||||
mkSubst : Nat -> CExp vs ->
|
||||
|
@ -153,14 +153,27 @@ mutual
|
||||
-- in case they duplicate work. We should fix that, to decide more accurately
|
||||
-- whether they're safe to inline, but until then this gives such a huge
|
||||
-- boost by removing unnecessary lambdas that we'll keep the special case.
|
||||
eval rec env stk (CRef fc n)
|
||||
= case (n == NS primIONS (UN $ Basic "io_bind"), stk) of
|
||||
eval rec env stk (CRef fc n) = do
|
||||
when (n == NS primIONS (UN $ Basic "io_bind")) $
|
||||
log "compiler.inline.io_bind" 50 $
|
||||
"Attempting to inline io_bind, its stack is: \{show stk}"
|
||||
case (n == NS primIONS (UN $ Basic "io_bind"), stk) of
|
||||
(True, act :: cont :: world :: stk) =>
|
||||
do xn <- genName "act"
|
||||
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
|
||||
pure $ unload stk $
|
||||
CLet fc xn False (CApp fc act [world])
|
||||
(refToLocal xn xn sc)
|
||||
(True, [act, cont]) =>
|
||||
do wn <- genName "world"
|
||||
xn <- genName "act"
|
||||
let world : forall vars. CExp vars := CRef fc wn
|
||||
sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])
|
||||
pure $ CLam fc wn
|
||||
$ refToLocal wn wn
|
||||
$ CLet fc xn False (CApp fc act [world])
|
||||
$ refToLocal xn xn
|
||||
$ sc
|
||||
(_,_) =>
|
||||
do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
|
@ -57,8 +57,10 @@ knownTopics = [
|
||||
("compiler.identity", Just "Log definitions that are equivalent to identity at runtime."),
|
||||
("compiler.inline.eval", Just "Log function definitions before and after inlining."),
|
||||
("compiler.inline.heuristic", Just "Log names the inlining heuristic(s) have decided to inline."),
|
||||
("compiler.inline.io_bind", Just "Log the attempts to inline `io_bind`."),
|
||||
("compiler.interpreter", Just "Log the call-stack of the VMCode interpreter."),
|
||||
("compiler.javascript.doc", Just "Generating doc comments for the JS backend."),
|
||||
("compiler.newtype.world", Just "Inlining matches on newtypes."),
|
||||
("compiler.refc", Nothing),
|
||||
("compiler.refc.cc", Nothing),
|
||||
("compiler.scheme.chez", Nothing),
|
||||
|
@ -230,7 +230,7 @@ getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)
|
||||
rel)
|
||||
rig
|
||||
getRelevantArg defs i rel world tm
|
||||
= pure (maybe Nothing (\r => Just (world, r)) rel)
|
||||
= pure ((world,) <$> rel)
|
||||
|
||||
-- If there's one constructor with only one non-erased argument, flag it as
|
||||
-- a newtype for optimisation
|
||||
|
@ -7,7 +7,7 @@ path = "build/exec/fold_app/fold.ss"
|
||||
|
||||
mainLine : String -> Bool
|
||||
mainLine str =
|
||||
("(define Main-main(" `isPrefixOf` str) &&
|
||||
("(define Main-main" `isPrefixOf` str) &&
|
||||
(" 99)" `isInfixOf` str) &&
|
||||
not ("prim__integerToNat" `isInfixOf` str)
|
||||
|
||||
|
@ -7,7 +7,7 @@ path = "build/exec/test_app/test.ss"
|
||||
|
||||
mainLine : String -> Bool
|
||||
mainLine str =
|
||||
("(define Main-main(" `isPrefixOf` str) && (" 375))))" `isInfixOf` str)
|
||||
("(define Main-main" `isPrefixOf` str) && (" 375)" `isInfixOf` str)
|
||||
|
||||
main : IO ()
|
||||
main = do
|
||||
|
@ -7,7 +7,7 @@ path = "build/exec/enum_app/enum.ss"
|
||||
|
||||
mainLine : String -> Bool
|
||||
mainLine str =
|
||||
("(define Enum-main(" `isPrefixOf` str) && (" 120 17))))" `isInfixOf` str)
|
||||
("(define Enum-main" `isPrefixOf` str) && (" 120 17))" `isInfixOf` str)
|
||||
|
||||
main : IO ()
|
||||
main = do
|
||||
|
@ -1,2 +1,2 @@
|
||||
allocated (Ptr t) freed
|
||||
allocated AnyPtr freed
|
||||
allocated (Ptr t) freed
|
||||
|
Loading…
Reference in New Issue
Block a user