git.iko.soy/Idris-dev
on master help sign in
Small tweak to inlining
7e800caEdwin Brady
src/IRTS/Compiler.hs+3−1
compare with master
unifiedsplit
@@ -506,7 +506,9 @@ doForeign vs env (ret : fname : world : args)
506 = do let l' = toFDesc l
506 = do let l' = toFDesc l
507 r' <- irTerm (sMN 0 "__foreignCall") vs env r
507 r' <- irTerm (sMN 0 "__foreignCall") vs env r
508 return (l', r')
508 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+
510
512
511 toFDesc (Constant (Str str)) = FStr str
513 toFDesc (Constant (Str str)) = FStr str
512 toFDesc tm
514 toFDesc tm
src/Idris/Core/CaseTree.hs+1−1
@@ -122,7 +122,7 @@ instance TermSize CaseAlt where
122small :: Name -> [Name] -> SC -> Bool
122small :: Name -> [Name] -> SC -> Bool
123small n args t = let as = findAllUsedArgs t args in
123small n args t = let as = findAllUsedArgs t args in
124 length as == length (nub as) &&
124 length as == length (nub as) &&
125− termsize n t < 10
125+ termsize n t < 20
126
126
127namesUsed :: SC -> [Name]
127namesUsed :: SC -> [Name]
128namesUsed sc = nub $ nu' [] sc where
128namesUsed sc = nub $ nu' [] sc where
src/Idris/Core/Evaluate.hs+1−1
@@ -951,7 +951,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
951 ( CaseDef args_ct sc_ct _,
951 ( CaseDef args_ct sc_ct _,
952 CaseDef args_rt sc_rt _) ->
952 CaseDef args_rt sc_rt _) ->
953 let inl = alwaysInline -- tcdict
953 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)
955 cdef = CaseDefs (args_ct, sc_ct)
955 cdef = CaseDefs (args_ct, sc_ct)
956 (args_rt, sc_rt)
956 (args_rt, sc_rt)
957 op = (CaseOp (ci { case_inlinable = inlc })
957 op = (CaseOp (ci { case_inlinable = inlc })
src/Idris/ElabDecls.hs+2
@@ -280,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)
280 ifail "You must turn on the DSLNotation extension to use a dsl block"
280 ifail "You must turn on the DSLNotation extension to use a dsl block"
281 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
281 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
282 addIBC (IBCDSL n)
282 addIBC (IBCDSL n)
283+elabDecl' what info (PDirective i@(DLogging _))
284+ = directiveAction i
283elabDecl' what info (PDirective i)
285elabDecl' what info (PDirective i)
284 | what /= EDefns = directiveAction i
286 | what /= EDefns = directiveAction i
285elabDecl' what info (PProvider doc syn fc nfc provWhat n)
287elabDecl' what info (PProvider doc syn fc nfc provWhat n)