Small tweak to inlining
Choose whether to inline based on size of runtime thing (which might
have had partial evaluation applied, thus be very different) rather than
compile time thing. This seems to make little difference to run time,
but can prevent a lot of breaking of sharing and duplicated definitions
in defunctionalisation, thus making compile time much faster.
commit7e800ca01ae65b9f6e43ac77c5b394efe91f5fa4
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 17 Sep 2017, 17:33 (9 years ago)
parent8cb1337
src/IRTS/Compiler.hs+3−1
@@ -506,7 +506,9 @@ doForeign vs env (ret : fname : world : args)
506506 = do let l' = toFDesc l
507507 r' <- irTerm (sMN 0 "__foreignCall") vs env r
508508 return (l', r')
509− splitArg _ = ifail "Badly formed foreign function call"
509+ splitArg _ = ifail $ "Badly formed foreign function call: " ++
510+ show (ret : fname : world : args)
511+
510512
511513 toFDesc (Constant (Str str)) = FStr str
512514 toFDesc tm
src/Idris/Core/CaseTree.hs+1−1
@@ -122,7 +122,7 @@ instance TermSize CaseAlt where
122122small :: Name -> [Name] -> SC -> Bool
123123small n args t = let as = findAllUsedArgs t args in
124124 length as == length (nub as) &&
125− termsize n t < 10
125+ termsize n t < 20
126126
127127namesUsed :: SC -> [Name]
128128namesUsed sc = nub $ nu' [] sc where
src/Idris/Core/Evaluate.hs+1−1
@@ -951,7 +951,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
951951 ( CaseDef args_ct sc_ct _,
952952 CaseDef args_rt sc_rt _) ->
953953 let inl = alwaysInline -- tcdict
954− inlc = (inl || small n args_ct sc_ct) && (not asserted)
954+ inlc = (inl || small n args_rt sc_rt) && (not asserted)
955955 cdef = CaseDefs (args_ct, sc_ct)
956956 (args_rt, sc_rt)
957957 op = (CaseOp (ci { case_inlinable = inlc })
src/Idris/ElabDecls.hs+2
@@ -280,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)
280280 ifail "You must turn on the DSLNotation extension to use a dsl block"
281281 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
282282 addIBC (IBCDSL n)
283+elabDecl' what info (PDirective i@(DLogging _))
284+ = directiveAction i
283285elabDecl' what info (PDirective i)
284286 | what /= EDefns = directiveAction i
285287elabDecl' what info (PProvider doc syn fc nfc provWhat n)