git.iko.soy/Idris-dev
on master help sign in
Don't inline for compilation (because the evaluator makes bad choices)

Instead, inline the compile-time representation to help the totality checker only. This can cause subexpressions to be duplicated, so should be avoided at run-time. For the run-time representation, inline later at IRTS level. Fixes #368

commitdad12e631bc829f0d55eefa8d5c38be2e474e47a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 2 Jul 2013, 13:40 (13 years ago) parent95d3577
4 files changed+13−6
compare with master
unifiedsplit
src/Core/CaseTree.hs+1−1 src/Core/Evaluate.hs+1−1 src/IRTS/Compiler.hs+8−1 src/Idris/ElabDecls.hs+3−3
src/Core/CaseTree.hs+1−1
@@ -80,7 +80,7 @@ instance TermSize CaseAlt where
8080small :: Name -> [Name] -> SC -> Bool
8181small n args t = let as = findAllUsedArgs t args in
8282 length as == length (nub as) &&
83− termsize n t < 5
83+ termsize n t < 10
8484
8585namesUsed :: SC -> [Name]
8686namesUsed sc = nub $ nu' [] sc where
src/Core/Evaluate.hs+1−1
@@ -178,7 +178,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
178178 = do v' <- ev ntimes stk top env v --(finalise v)
179179 sc' <- ev ntimes stk top (v' : env) sc
180180 wknV (-1) sc'
181− | otherwise -- put this back when the Bind works properly
181+ | otherwise
182182 = do t' <- ev ntimes stk top env t
183183 v' <- ev ntimes stk top env v --(finalise v)
184184 -- use Tmp as a placeholder, then make it a variable reference
src/IRTS/Compiler.hs+8−1
@@ -291,13 +291,20 @@ mkIty' (App (App (P _ (UN "FFunction") _) _) (App (P _ (UN "FAny") _) (App (P _
291291mkIty' (App (App (P _ (UN "FFunction") _) _) _) = FFunction
292292mkIty' _ = FAny
293293
294+-- would be better if these FInt types were evaluated at compile time
295+-- TODO: add %eval directive for such things
296+
294297mkIty "FFloat" = FDouble
295−mkIty "FChar" = FChar
298+mkIty "FInt" = mkIntIty "ITNative"
299+mkIty "FChar" = mkIntIty "IT8"
300+mkIty "FShort" = mkIntIty "IT16"
301+mkIty "FLong" = mkIntIty "IT64"
296302mkIty "FString" = FString
297303mkIty "FPtr" = FPtr
298304mkIty "FUnit" = FUnit
299305mkIty "FFunction" = FFunction
300306mkIty "FFunctionIO" = FFunctionIO
307+mkIty x = error $ "Unknown type " ++ x
301308
302309mkIntIty "ITNative" = FInt ITNative
303310mkIntIty "IT8" = FInt IT8
src/Idris/ElabDecls.hs+3−3
@@ -600,9 +600,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
600600
601601 getLHS (_, l, _) = l
602602
603− simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,
604− simplify ctxt rt [] y)
605−-- simpl rt ctxt (Right (x, y)) = Right (x, y)
603+-- simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,
604+-- simplify ctxt rt [] y)
605+ simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
606606 simpl rt ctxt t = t
607607
608608 sameLength ((_, x, _) : xs)