mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-02 08:35:07 +03:00
Recalculate call graph after inlining
This means we can eliminate unused definitions from the generated code. As usual, this doesn't make the generated code any faster, or the chez compilation, but it's still good for tidiness and it does make the generated scheme smaller.
This commit is contained in:
parent
73d374e435
commit
09c4b6cc03
@ -416,6 +416,43 @@ mergeLam (MkFun args def)
|
||||
pure $ MkFun args' exp'
|
||||
mergeLam d = pure d
|
||||
|
||||
mutual
|
||||
addRefs : NameMap Bool -> CExp vars -> NameMap Bool
|
||||
addRefs ds (CRef _ n) = insert n False ds
|
||||
addRefs ds (CLam _ _ sc) = addRefs ds sc
|
||||
addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc
|
||||
addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args
|
||||
addRefs ds (CCon _ _ _ args) = addRefsArgs ds args
|
||||
addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)
|
||||
addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args
|
||||
addRefs ds (CForce _ _ e) = addRefs ds e
|
||||
addRefs ds (CDelay _ _ e) = addRefs ds e
|
||||
addRefs ds (CConCase _ sc alts def)
|
||||
= let ds' = maybe ds (addRefs ds) def in
|
||||
addRefsConAlts (addRefs ds' sc) alts
|
||||
addRefs ds (CConstCase _ sc alts def)
|
||||
= let ds' = maybe ds (addRefs ds) def in
|
||||
addRefsConstAlts (addRefs ds' sc) alts
|
||||
addRefs ds tm = ds
|
||||
|
||||
addRefsArgs : NameMap Bool -> List (CExp vars) -> NameMap Bool
|
||||
addRefsArgs ds [] = ds
|
||||
addRefsArgs ds (a :: as) = addRefsArgs (addRefs ds a) as
|
||||
|
||||
addRefsConAlts : NameMap Bool -> List (CConAlt vars) -> NameMap Bool
|
||||
addRefsConAlts ds [] = ds
|
||||
addRefsConAlts ds (MkConAlt _ _ _ sc :: rest)
|
||||
= addRefsConAlts (addRefs ds sc) rest
|
||||
|
||||
addRefsConstAlts : NameMap Bool -> List (CConstAlt vars) -> NameMap Bool
|
||||
addRefsConstAlts ds [] = ds
|
||||
addRefsConstAlts ds (MkConstAlt _ sc :: rest)
|
||||
= addRefsConstAlts (addRefs ds sc) rest
|
||||
|
||||
getRefs : CDef -> NameMap Bool
|
||||
getRefs (MkFun args exp) = addRefs empty exp
|
||||
getRefs _ = empty
|
||||
|
||||
export
|
||||
inlineDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
@ -425,6 +462,17 @@ inlineDef n
|
||||
let Just cexpr = compexpr def | Nothing => pure ()
|
||||
setCompiled n !(inline n cexpr)
|
||||
|
||||
-- Update the names a function refers to at runtime based on the transformation
|
||||
-- results (saves generating code unnecessarily).
|
||||
updateCallGraph : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
updateCallGraph n
|
||||
= do defs <- get Ctxt
|
||||
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
|
||||
let Just cexpr = compexpr def | Nothing => pure ()
|
||||
let refs = getRefs cexpr
|
||||
ignore $ addDef n (record { refersToRuntimeM = Just refs } def)
|
||||
|
||||
export
|
||||
fixArityDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
@ -462,6 +510,8 @@ compileAndInlineAll
|
||||
traverse_ mergeLamDef cns
|
||||
traverse_ caseLamDef cns
|
||||
traverse_ fixArityDef cns
|
||||
|
||||
traverse_ updateCallGraph cns
|
||||
where
|
||||
nonErased : Name -> Core Bool
|
||||
nonErased n
|
||||
|
Loading…
Reference in New Issue
Block a user