idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-24 20:23:11 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #2794 ] Do not ignore notinline lets in identity detection (#2795)

Browse Source
This commit is contained in:
G. Allais 2022-12-06 11:41:30 +00:00 committed by GitHub
parent ff6afb0c59
commit fcbd9e9190
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 66 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/Compiler/CompileExpr.idr
View File

@ -227,7 +227,7 @@ natBranch _ = False
trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt nm SUCC _ [arg] sc)
= Just (CLet (getFC n) arg True (magic__natUnsuc (getFC n) (getFC n) [n]) sc)
= Just (CLet (getFC n) arg YesInline (magic__natUnsuc (getFC n) (getFC n) [n]) sc)
trySBranch _ _ = Nothing
tryZBranch : CConAlt vars -> Maybe (CExp vars)
@ -253,7 +253,7 @@ builtinNatTree (CConCase fc sc@(CLocal _ _) alts def)
else CConCase fc sc alts def
builtinNatTree (CConCase fc sc alts def)
= do x <- newMN "succ"
pure $ CLet fc x True sc
pure $ CLet fc x YesInline sc
!(builtinNatTree $ CConCase fc (CLocal fc First) (map weaken alts) (map weaken def))
builtinNatTree t = pure t
@ -283,7 +283,7 @@ unitTree exp@(CConCase fc sc alts def) = fromMaybe (pure exp)
| _ => Nothing
Just $ case sc of -- TODO: Check scrutinee has no effect, and skip let binding
CLocal _ _ => pure e
_ => pure $ CLet fc !(newMN "_unit") False sc (weaken e)
_ => pure $ CLet fc !(newMN "_unit") NotInline sc (weaken e)
unitTree t = pure t
-- See if the constructor is a special constructor type, e.g a nil or cons
@ -339,7 +339,7 @@ toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
toCExpTm n (Bind fc x (Let _ rig val _) sc)
= do sc' <- toCExp n sc
pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
(CLet fc x True !(toCExp n val) sc')
(CLet fc x YesInline !(toCExp n val) sc')
rig
toCExpTm n (Bind fc x (Pi _ c e ty) sc)
= pure $ CCon fc (UN (Basic "->")) TYCON Nothing
@ -467,7 +467,7 @@ mutual
{inner=vars}
{ns = [MN "eff" 0]}
(mkSizeOf _) (mkSizeOf _) sc'
let tm = CLet fc (MN "eff" 0) False scr (substs env scope)
let tm = CLet fc (MN "eff" 0) NotInline 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
@ -501,8 +501,8 @@ mutual
toCExpTree n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
= let fc = getLoc scTy in
pure $
CLet fc arg True (CForce fc LInf (CLocal (getLoc scTy) x)) $
CLet fc ty True (CErased fc)
CLet fc arg YesInline (CForce fc LInf (CLocal (getLoc scTy) x)) $
CLet fc ty YesInline (CErased fc)
!(toCExpTree n sc)
toCExpTree n alts
= toCExpTree' n alts

19
src/Compiler/Inline.idr
View File

@ -80,13 +80,13 @@ mutual
{idx : Nat} -> (0 p : IsVar n idx free) -> CExp free -> Int
used {idx} n (CLocal _ {idx=pidx} prf) = if idx == pidx then 1 else 0
used n (CLam _ _ sc) = used (Later n) sc
used n (CLet _ _ False val sc)
used n (CLet _ _ NotInline val sc)
= let usedl = used n val + used (Later n) sc in
if usedl > 0
then 1000 -- Don't do any inlining of the name, because if it's
-- used under a non-inlinable let things might go wrong
else usedl
used n (CLet _ _ True val sc) = used n val + used (Later n) sc
used n (CLet _ _ YesInline val sc) = used n val + used (Later n) sc
used n (CApp _ x args) = foldr (+) (used n x) (map (used n) args)
used n (CCon _ _ _ _ args) = foldr (+) 0 (map (used n) args)
used n (COp _ _ args) = foldr (+) 0 (map (used n) args)
@ -162,8 +162,9 @@ mutual
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)
CLet fc xn NotInline
(CApp fc act [world])
(refToLocal xn xn sc)
(True, [act, cont]) =>
do wn <- genName "world"
xn <- genName "act"
@ -171,7 +172,7 @@ mutual
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])
$ CLet fc xn NotInline (CApp fc act [world])
$ refToLocal xn xn
$ sc
(_,_) =>
@ -193,12 +194,12 @@ mutual
sc' <- eval rec (CRef fc xn :: env) [] sc
pure $ CLam fc x (refToLocal xn x sc')
eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
eval {vars} {free} rec env stk (CLet fc x False val sc)
eval {vars} {free} rec env stk (CLet fc x NotInline val sc)
= do xn <- genName "letv"
sc' <- eval rec (CRef fc xn :: env) [] sc
val' <- eval rec env [] val
pure (unload stk $ CLet fc x False val' (refToLocal xn x sc'))
eval {vars} {free} rec env stk (CLet fc x True val sc)
pure (unload stk $ CLet fc x NotInline val' (refToLocal xn x sc'))
eval {vars} {free} rec env stk (CLet fc x YesInline val sc)
= do let u = used First sc
if u < 1 -- TODO: Can make this <= as long as we know *all* inlinings
-- are guaranteed not to duplicate work. (We don't know
@ -208,7 +209,7 @@ mutual
else do xn <- genName "letv"
sc' <- eval rec (CRef fc xn :: env) stk sc
val' <- eval rec env [] val
pure (CLet fc x True val' (refToLocal xn x sc'))
pure (CLet fc x YesInline val' (refToLocal xn x sc'))
eval rec env stk (CApp fc f@(CRef nfc n) args)
= do -- If we don't know 'n' leave the arity alone, because it's
-- a name from another module where the job is already done

8
src/Compiler/Opts/ConstantFold.idr
View File

@ -81,13 +81,13 @@ constFold rho (CLocal fc p) = lookup fc (MkVar p) rho
constFold rho e@(CRef fc x) = CRef fc x
constFold rho (CLam fc x y)
= CLam fc x $ constFold (wk (mkSizeOf [x]) rho) y
constFold rho (CLet fc x inlineOK y z) =
constFold rho (CLet fc x inl y z) =
let val = constFold rho y
in case val of
CPrimVal _ _ => if inlineOK
CPrimVal _ _ => if inl == YesInline
then constFold (val :: 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)
else CLet fc x inl val (constFold (wk (mkSizeOf [x]) rho) z)
_ => 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

1
src/Compiler/Opts/Identity.idr
View File

@ -32,6 +32,7 @@ parameters (fn1 : Name) (idIdx : Nat)
cexpIdentity (MkVar {i} _) _ _ (CLocal {idx} fc p) = idx == i
cexpIdentity var _ _ (CRef _ _) = False
cexpIdentity var _ _ (CLam _ _ _) = False
cexpIdentity var con const (CLet _ _ NotInline val sc) = False
cexpIdentity var con const (CLet _ _ _ val sc) = (case isUnsucc var val of
Just (c, var') => unsuccIdentity c var' sc
Nothing => False)

13
src/Core/CompileExpr.idr
View File

@ -56,6 +56,16 @@ Eq ConInfo where
UNIT == UNIT = True
_ == _ = False
||| Tagging let binders with whether it is safe to inline them
public export
data InlineOk = YesInline | NotInline
export
Eq InlineOk where
YesInline == YesInline = True
NotInline == NotInline = True
_ == _ = False
mutual
||| CExp - an expression ready for compiling.
public export
@ -65,7 +75,8 @@ mutual
-- Lambda expression
CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars
-- Let bindings
CLet : FC -> (x : Name) -> (inlineOK : Bool) -> -- Don't inline if set
CLet : FC -> (x : Name) ->
InlineOk -> -- Don't inline if set
CExp vars -> CExp (x :: vars) -> CExp vars
-- Application of a defined function. The length of the argument list is
-- exactly the same length as expected by its definition (so saturate with

5
src/Core/TTC.idr
View File

@ -21,6 +21,11 @@ import Libraries.Utils.Scheme
%default covering
export
TTC InlineOk where
toBuf b = toBuf b . (YesInline ==)
fromBuf = Core.map (\ b => ifThenElse b YesInline NotInline) . fromBuf
export
TTC Namespace where
toBuf b = toBuf b . unsafeUnfoldNamespace

1
tests/Main.idr
View File

@ -148,6 +148,7 @@ idrisTestsPerformance = MkTestPool "Performance" [] Nothing
-- pose interesting challenges for the elaborator
["perf001", "perf002", "perf003", "perf004", "perf005",
"perf007", "perf008", "perf009", "perf010", "perf011",
"perf012",
"perf2202"]
idrisTestsRegression : TestPool

14
tests/idris2/perf012/Main.idr Normal file
View File

@ -0,0 +1,14 @@
%logging "compiler.identity" 5
-- This SHOULD give us the identity flag
id : Nat -> Nat
id Z = Z
id (S n) = S (id n)
-- This should NOT give us anything: `main` is not the identity
-- because it is effectful
main : IO ()
main = do
s <- getLine
putStrLn s
main

9
tests/idris2/perf012/expected Normal file
View File

@ -0,0 +1,9 @@
LOG compiler.identity:5: found identity flag for: Main.id, 0
old def: Just [{arg:0}]: (%case !{arg:0} [(%constcase 0 0)] Just (%let {e:0} (-Integer [!{arg:0}, 1]) (+Integer [(Main.id [!{e:0}]), 1])))
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0}
LOG compiler.identity:5: found identity flag for: Main.id, 0
old def: Just [{arg:0}]: !{arg:0}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0}
LOG compiler.identity:5: found identity flag for: Main.id, 0
old def: Just [{arg:0}]: !{arg:0}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0}

3
tests/idris2/perf012/run Normal file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 Main.idr -o main