git.iko.soy/Idris-dev
on master help sign in
Separate compile time and run time inlinings
a52bb30Edwin Brady
src/Core/CaseTree.hs+1−1
compare with master
unifiedsplit
@@ -69,7 +69,7 @@ instance TermSize CaseAlt where
69
69
70-- simple terms can be inlined trivially - good for primitives in particular
70-- simple terms can be inlined trivially - good for primitives in particular
71small :: Name -> SC -> Bool
71small :: Name -> SC -> Bool
72−small n t = False -- termsize n t < 10
72+small n t = termsize n t < 50
73
73
74namesUsed :: SC -> [Name]
74namesUsed :: SC -> [Name]
75namesUsed sc = nub $ nu' [] sc where
75namesUsed sc = nub $ nu' [] sc where
src/Core/Evaluate.hs+34−27
@@ -28,7 +28,7 @@ data EvalState = ES { limited :: [(Name, Int)],
28
28
29type Eval a = State EvalState a
29type Eval a = State EvalState a
30
30
31−data EvalOpt = Spec | HNF | Simplify | AtREPL
31+data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
32 deriving (Show, Eq)
32 deriving (Show, Eq)
33
33
34initEval = ES [] 0
34initEval = ES [] 0
@@ -107,11 +107,13 @@ specialise ctxt env limits t
107-- Like normalise, but we only reduce functions that are marked as okay to
107-- Like normalise, but we only reduce functions that are marked as okay to
108-- inline (and probably shouldn't reduce lets?)
108-- inline (and probably shouldn't reduce lets?)
109
109
110−simplify :: Context -> Env -> TT Name -> TT Name
110+simplify :: Context -> Bool -> Env -> TT Name -> TT Name
111−simplify ctxt env t
111+simplify ctxt runtime env t
112 = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),
112 = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),
113− (UN "par", 0)]
113+ (UN "par", 0),
114+ (UN "fork", 0)]
114− (map finalEntry env) (finalise t) [Simplify]
115+ (map finalEntry env) (finalise t)
116+ [Simplify runtime]
115 quote 0 val) initEval
117 quote 0 val) initEval
116
118
117hnf :: Context -> Env -> TT Name -> TT Name
119hnf :: Context -> Env -> TT Name -> TT Name
@@ -153,9 +155,13 @@ eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
153 [EvalOpt] -> Eval Value
155 [EvalOpt] -> Eval Value
154eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
156eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
155 spec = Spec `elem` opts
157 spec = Spec `elem` opts
156− simpl = Simplify `elem` opts
158+ simpl = Simplify True `elem` opts
157 atRepl = AtREPL `elem` opts
159 atRepl = AtREPL `elem` opts
158
160
161+ canSimplify inl inr n stk
162+ = (Simplify False `elem` opts && (not inl || elem n stk))
163+ || (Simplify True `elem` opts && (not inr || elem n stk))
164+
159 ev ntimes stk top env (P _ n ty)
165 ev ntimes stk top env (P _ n ty)
160 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
166 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
161 ev ntimes stk top env v
167 ev ntimes stk top env v
@@ -168,8 +174,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
168 ev ntimes (n:stk) True env tm
174 ev ntimes (n:stk) True env tm
169 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
175 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
170 return $ VP nt n vty
176 return $ VP nt n vty
171− [(CaseOp inl _ _ _ [] tree _ _, Public)] -> -- unoptimised version
177+ [(CaseOp inl inr _ _ _ [] tree _ _, Public)] -> -- unoptimised version
172− if simpl && (not inl || elem n stk)
178+ if canSimplify inl inr n stk
173 then liftM (VP Ref n) (ev ntimes stk top env ty)
179 then liftM (VP Ref n) (ev ntimes stk top env ty)
174 else do c <- evCase ntimes (n:stk) top env [] [] tree
180 else do c <- evCase ntimes (n:stk) top env [] [] tree
175 case c of
181 case c of
@@ -232,8 +238,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
232 = traceWhen traceon (show stk) $
238 = traceWhen traceon (show stk) $
233 do let val = lookupDefAcc Nothing n atRepl ctxt
239 do let val = lookupDefAcc Nothing n atRepl ctxt
234 case val of
240 case val of
235− [(CaseOp inl _ _ _ ns tree _ _, Public)] ->
241+ [(CaseOp inl inr _ _ _ ns tree _ _, Public)] ->
236− if simpl && (not inl || elem n stk)
242+ if canSimplify inl inr n stk
237 then return $ unload env (VP Ref n ty) args
243 then return $ unload env (VP Ref n ty) args
238 else do c <- evCase ntimes (n:stk) top env ns args tree
244 else do c <- evCase ntimes (n:stk) top env ns args tree
239 case c of
245 case c of
@@ -392,7 +398,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where
392 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
398 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
393 [Function _ t] -> ev env t
399 [Function _ t] -> ev env t
394 [TyDecl nt ty] -> return $ HP nt n ty
400 [TyDecl nt ty] -> return $ HP nt n ty
395− [CaseOp inl _ _ _ [] tree _ _] ->
401+ [CaseOp inl _ _ _ _ [] tree _ _] ->
396 do c <- evCase env [] [] tree
402 do c <- evCase env [] [] tree
397 case c of
403 case c of
398 (Nothing, _, _) -> return $ HP Ref n ty
404 (Nothing, _, _) -> return $ HP Ref n ty
@@ -422,7 +428,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where
422 app <- apply env sc' as
428 app <- apply env sc' as
423 wknH (-1) app
429 wknH (-1) app
424 apply env (HP Ref n ty) args
430 apply env (HP Ref n ty) args
425− | [CaseOp _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
431+ | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
426 = do c <- evCase env ns args tree
432 = do c <- evCase env ns args tree
427 case c of
433 case c of
428 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
434 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
@@ -549,8 +555,8 @@ convEq ctxt = ceq [] where
549 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
555 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
550 ([Function _ xdef], [Function _ ydef])
556 ([Function _ xdef], [Function _ ydef])
551 -> ceq ((x,y):ps) xdef ydef
557 -> ceq ((x,y):ps) xdef ydef
552− ([CaseOp _ _ _ _ _ xdef _ _],
558+ ([CaseOp _ _ _ _ _ _ xdef _ _],
553− [CaseOp _ _ _ _ _ ydef _ _])
559+ [CaseOp _ _ _ _ _ _ ydef _ _])
554 -> caseeq ((x,y):ps) xdef ydef
560 -> caseeq ((x,y):ps) xdef ydef
555 _ -> return False
561 _ -> return False
556
562
@@ -572,7 +578,8 @@ spec ctxt statics genv tm = error "spec undefined"
572data Def = Function Type Term
578data Def = Function Type Term
573 | TyDecl NameType Type
579 | TyDecl NameType Type
574 | Operator Type Int ([Value] -> Maybe Value)
580 | Operator Type Int ([Value] -> Maybe Value)
575− | CaseOp Bool Type -- bool for inlinable
581+ | CaseOp Bool Bool -- compile-time/run-time inlinable
582+ Type
576 [Either Term (Term, Term)] -- original definition
583 [Either Term (Term, Term)] -- original definition
577 [([Name], Term, Term)] -- simplified definition
584 [([Name], Term, Term)] -- simplified definition
578 [Name] SC -- Compile time case definition
585 [Name] SC -- Compile time case definition
@@ -585,7 +592,7 @@ instance Show Def where
585 show (Function ty tm) = "Function: " ++ show (ty, tm)
592 show (Function ty tm) = "Function: " ++ show (ty, tm)
586 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
593 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
587 show (Operator ty _ _) = "Operator: " ++ show ty
594 show (Operator ty _ _) = "Operator: " ++ show ty
588− show (CaseOp _ ty ps_in ps ns sc ns' sc')
595+ show (CaseOp _ _ ty ps_in ps ns sc ns' sc')
589 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
596 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
590 show ns ++ " " ++ show sc ++ "\n" ++
597 show ns ++ " " ++ show sc ++ "\n" ++
591 show ns' ++ " " ++ show sc'
598 show ns' ++ " " ++ show sc'
@@ -707,8 +714,9 @@ addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt
707 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
714 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
708 simpleCase tcase covering RunTime (FC "" 0) psrt) of
715 simpleCase tcase covering RunTime (FC "" 0) psrt) of
709 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
716 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
710− let inl = alwaysInline || small n sc' in
717+ let inl = alwaysInline in
718+ addDef n (CaseOp inl (inl || small n sc')
711− addDef n (CaseOp inl ty ps_in ps args sc args' sc',
719+ ty ps_in ps args sc args' sc',
712 access, Unchecked) ctxt in
720 access, Unchecked) ctxt in
713 uctxt { definitions = ctxt' }
721 uctxt { definitions = ctxt' }
714
722
@@ -716,15 +724,14 @@ simplifyCasedef :: Name -> Context -> Context
716simplifyCasedef n uctxt
724simplifyCasedef n uctxt
717 = let ctxt = definitions uctxt
725 = let ctxt = definitions uctxt
718 ctxt' = case lookupCtxt Nothing n ctxt of
726 ctxt' = case lookupCtxt Nothing n ctxt of
719− [(CaseOp inl ty [] ps args sc args' sc', acc, tot)] ->
727+ [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
720 ctxt -- nothing to simplify (or already done...)
728 ctxt -- nothing to simplify (or already done...)
721− [(CaseOp inl ty ps_in ps args sc args' sc', acc, tot)] ->
729+ [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
722 let pdef = map debind $ map simpl ps_in in
730 let pdef = map debind $ map simpl ps_in in
723 case simpleCase False True CompileTime (FC "" 0) pdef of
731 case simpleCase False True CompileTime (FC "" 0) pdef of
724 OK (CaseDef args sc _) ->
732 OK (CaseDef args sc _) ->
725−-- Erase the original patterns, since we won't use them again and it
726−-- only clutters the .ibc
727− addDef n (CaseOp inl ty [] ps args sc args' sc',
733+ addDef n (CaseOp inl inr
734+ ty ps_in ps args sc args' sc',
728 acc, tot) ctxt
735 acc, tot) ctxt
729 _ -> ctxt in
736 _ -> ctxt in
730 uctxt { definitions = ctxt' }
737 uctxt { definitions = ctxt' }
@@ -737,7 +744,7 @@ simplifyCasedef n uctxt
737 (vs, x', y')
744 (vs, x', y')
738 debind (Left x) = let (vs, x') = depat [] x in
745 debind (Left x) = let (vs, x') = depat [] x in
739 (vs, x', Impossible)
746 (vs, x', Impossible)
740− simpl (Right (x, y)) = Right (x, simplify uctxt [] y)
747+ simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)
741 simpl t = t
748 simpl t = t
742
749
743addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
750addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
@@ -761,7 +768,7 @@ lookupTy root n ctxt
761 (Function ty _) -> return ty
768 (Function ty _) -> return ty
762 (TyDecl _ ty) -> return ty
769 (TyDecl _ ty) -> return ty
763 (Operator ty _ _) -> return ty
770 (Operator ty _ _) -> return ty
764− (CaseOp _ ty _ _ _ _ _ _) -> return ty
771+ (CaseOp _ _ ty _ _ _ _ _ _) -> return ty
765
772
766isConName :: Maybe [String] -> Name -> Context -> Bool
773isConName :: Maybe [String] -> Name -> Context -> Bool
767isConName root n ctxt
774isConName root n ctxt
@@ -777,7 +784,7 @@ isFnName root n ctxt
777 case tfst def of
784 case tfst def of
778 (Function _ _) -> return True
785 (Function _ _) -> return True
779 (Operator _ _ _) -> return True
786 (Operator _ _ _) -> return True
780− (CaseOp _ _ _ _ _ _ _ _) -> return True
787+ (CaseOp _ _ _ _ _ _ _ _ _) -> return True
781 _ -> return False
788 _ -> return False
782
789
783lookupP :: Maybe [String] -> Name -> Context -> [Term]
790lookupP :: Maybe [String] -> Name -> Context -> [Term]
@@ -786,7 +793,7 @@ lookupP root n ctxt
786 p <- case def of
793 p <- case def of
787 (Function ty tm, a, _) -> return (P Ref n ty, a)
794 (Function ty tm, a, _) -> return (P Ref n ty, a)
788 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
795 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
789− (CaseOp _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
796+ (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
790 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
797 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
791 case snd p of
798 case snd p of
792 Hidden -> []
799 Hidden -> []
src/IRTS/Compiler.hs+2−2
@@ -129,8 +129,8 @@ declArgs args n x = LFun n args x
129
129
130mkLDecl n (Function tm _) = do e <- ir tm
130mkLDecl n (Function tm _) = do e <- ir tm
131 return (declArgs [] n e)
131 return (declArgs [] n e)
132−mkLDecl n (CaseOp _ _ _ pats _ _ args sc) = do e <- ir (args, sc)
132+mkLDecl n (CaseOp _ _ _ _ pats _ _ args sc) = do e <- ir (args, sc)
133− return (declArgs [] n e)
133+ return (declArgs [] n e)
134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))
136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))
src/Idris/Coverage.hs+2−2
@@ -338,7 +338,7 @@ checkTotality path fc n
338 t' <- case t of
338 t' <- case t of
339 Unchecked ->
339 Unchecked ->
340 case lookupDef Nothing n ctxt of
340 case lookupDef Nothing n ctxt of
341− [CaseOp _ _ _ pats _ _ _ _] ->
341+ [CaseOp _ _ _ _ pats _ _ _ _] ->
342 do t' <- if AssertTotal `elem` opts
342 do t' <- if AssertTotal `elem` opts
343 then return $ Total []
343 then return $ Total []
344 else calcTotality path fc n pats
344 else calcTotality path fc n pats
@@ -401,7 +401,7 @@ buildSCG (_, n) = do
401 ist <- get
401 ist <- get
402 case lookupCtxt Nothing n (idris_callgraph ist) of
402 case lookupCtxt Nothing n (idris_callgraph ist) of
403 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of
403 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of
404− [CaseOp _ _ _ _ args sc _ _] ->
404+ [CaseOp _ _ _ _ _ args sc _ _] ->
405 do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"
405 do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"
406 ++ show sc
406 ++ show sc
407 let newscg = buildSCG' ist sc args
407 let newscg = buildSCG' ist sc args
src/Idris/ElabDecls.hs+5−5
@@ -299,7 +299,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
299-- show l ++ " = " ++
299-- show l ++ " = " ++
300-- show r) pats))
300-- show r) pats))
301 let tcase = opt_typecase (idris_options ist)
301 let tcase = opt_typecase (idris_options ist)
302− let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
302+ let pdef = map debind $ map (simpl False (tt_ctxt ist)) pats
303
303
304 numArgs <- tclift $ sameLength pdef
304 numArgs <- tclift $ sameLength pdef
305
305
@@ -311,7 +311,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
311 logLvl 5 $ "Patterns:\n" ++ show pats
311 logLvl 5 $ "Patterns:\n" ++ show pats
312 logLvl 5 $ "Optimised patterns:\n" ++ show optpats
312 logLvl 5 $ "Optimised patterns:\n" ++ show optpats
313
313
314− let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats
314+ let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats
315 tree@(CaseDef scargs sc _) <- tclift $
315 tree@(CaseDef scargs sc _) <- tclift $
316 simpleCase tcase False CompileTime fc pdef
316 simpleCase tcase False CompileTime fc pdef
317 cov <- coverage
317 cov <- coverage
@@ -362,7 +362,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
362 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
362 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)
363 i <- get
363 i <- get
364 case lookupDef Nothing n (tt_ctxt i) of
364 case lookupDef Nothing n (tt_ctxt i) of
365− (CaseOp _ _ _ _ scargs sc scargs' sc' : _) ->
365+ (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->
366 do let calls = findCalls sc' scargs'
366 do let calls = findCalls sc' scargs'
367 let used = findUsedArgs sc' scargs'
367 let used = findUsedArgs sc' scargs'
368 -- let scg = buildSCG i sc scargs
368 -- let scg = buildSCG i sc scargs
@@ -387,8 +387,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
387
387
388 getLHS (_, l, _) = l
388 getLHS (_, l, _) = l
389
389
390− simpl ctxt (Right (x, y)) = Right (x, simplify ctxt [] y)
390+ simpl rt ctxt (Right (x, y)) = Right (x, simplify ctxt rt [] y)
391− simpl ctxt t = t
391+ simpl rt ctxt t = t
392
392
393 sameLength ((_, x, _) : xs)
393 sameLength ((_, x, _) : xs)
394 = do l <- sameLength xs
394 = do l <- sameLength xs
src/Idris/IBC.hs+4−2
@@ -612,11 +612,12 @@ instance Binary Def where
612 put x1
612 put x1
613 put x2
613 put x2
614 put x3
614 put x3
615− CaseOp x1 x2 x3 x4 x5 x6 x7 x8 ->
615+ CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->
616 do putWord8 3
616 do putWord8 3
617 put x1
617 put x1
618 put x2
618 put x2
619 put x3
619 put x3
620+ -- no x3a
620 put x4
621 put x4
621 put x5
622 put x5
622 put x6
623 put x6
@@ -638,12 +639,13 @@ instance Binary Def where
638 3 -> do x1 <- get
639 3 -> do x1 <- get
639 x2 <- get
640 x2 <- get
640 x3 <- get
641 x3 <- get
642+ -- x3 <- get always []
641 x4 <- get
643 x4 <- get
642 x5 <- get
644 x5 <- get
643 x6 <- get
645 x6 <- get
644 x7 <- get
646 x7 <- get
645 x8 <- get
647 x8 <- get
646− return (CaseOp x1 x2 x3 x4 x5 x6 x7 x8)
648+ return (CaseOp x1 x2 x3 [] x4 x5 x6 x7 x8)
647 _ -> error "Corrupted binary data for Def"
649 _ -> error "Corrupted binary data for Def"
648
650
649instance Binary Accessibility where
651instance Binary Accessibility where
src/Idris/REPL.hs+3−3
@@ -248,7 +248,7 @@ process fn (Search t) = iputStrLn "Not implemented"
248process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
248process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
249 ctxt <- getContext
249 ctxt <- getContext
250 ist <- get
250 ist <- get
251− let tm' = simplify ctxt [] {- (idris_statics ist) -} tm
251+ let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
252 iputStrLn (show (delab ist tm'))
252 iputStrLn (show (delab ist tm'))
253
253
254process fn (RmProof n')
254process fn (RmProof n')
@@ -312,7 +312,7 @@ process fn (Prove n')
312process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
312process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
313 ctxt <- getContext
313 ctxt <- getContext
314 ist <- get
314 ist <- get
315− let tm' = simplify ctxt [] tm
315+ let tm' = simplify ctxt True [] tm
316 iputStrLn (show (delab ist tm'))
316 iputStrLn (show (delab ist tm'))
317process fn TTShell = do ist <- get
317process fn TTShell = do ist <- get
318 let shst = initState (tt_ctxt ist)
318 let shst = initState (tt_ctxt ist)
@@ -349,7 +349,7 @@ process fn (Pattelab t)
349
349
350process fn (Missing n) = do i <- get
350process fn (Missing n) = do i <- get
351 case lookupDef Nothing n (tt_ctxt i) of
351 case lookupDef Nothing n (tt_ctxt i) of
352− [CaseOp _ _ _ _ args t _ _]
352+ [CaseOp _ _ _ _ _ args t _ _]
353 -> do tms <- genMissing n args t
353 -> do tms <- genMissing n args t
354 iputStrLn (showSep "\n" (map (showImp True) tms))
354 iputStrLn (showSep "\n" (map (showImp True) tms))
355 [] -> iputStrLn $ show n ++ " undefined"
355 [] -> iputStrLn $ show n ++ " undefined"