a52bb30 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Separate compile time and run time inlinings

Run time can be more aggressive - compile time needs to be careful since over aggressive inline can make the termination check harder, especially for type class instances.

commita52bb30e6973efdedd18658cbed8dbd55608f029 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Oct 2012, 18:54 (14 years ago) parent9e58e28

7 files changed+51−42

compare with master

unifiedsplit

src/Core/CaseTree.hs+1−1 src/Core/Evaluate.hs+34−27 src/IRTS/Compiler.hs+2−2 src/Idris/Coverage.hs+2−2 src/Idris/ElabDecls.hs+5−5 src/Idris/IBC.hs+4−2 src/Idris/REPL.hs+3−3

src/Core/CaseTree.hs+1−1

@@ -69,7 +69,7 @@ instance TermSize CaseAlt where

6969

7070-- simple terms can be inlined trivially - good for primitives in particular

7171small :: Name -> SC -> Bool

72−small n t = False -- termsize n t < 10

72+small n t = termsize n t < 50

7373

7474namesUsed :: SC -> [Name]

7575namesUsed sc = nub $ nu' [] sc where

src/Core/Evaluate.hs+34−27

@@ -28,7 +28,7 @@ data EvalState = ES { limited :: [(Name, Int)],

2828

2929type Eval a = State EvalState a

3030

31−data EvalOpt = Spec | HNF | Simplify | AtREPL

31+data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

3232 deriving (Show, Eq)

3333

3434initEval = ES [] 0

@@ -107,11 +107,13 @@ specialise ctxt env limits t

107107-- Like normalise, but we only reduce functions that are marked as okay to

108108-- inline (and probably shouldn't reduce lets?)

109109

110−simplify :: Context -> Env -> TT Name -> TT Name

111−simplify ctxt env t

110+simplify :: Context -> Bool -> Env -> TT Name -> TT Name

111+simplify ctxt runtime env t

112112 = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),

113− (UN "par", 0)]

114− (map finalEntry env) (finalise t) [Simplify]

113+ (UN "par", 0),

114+ (UN "fork", 0)]

115+ (map finalEntry env) (finalise t)

116+ [Simplify runtime]

115117 quote 0 val) initEval

116118

117119hnf :: Context -> Env -> TT Name -> TT Name

@@ -153,9 +155,13 @@ eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->

153155 [EvalOpt] -> Eval Value

154156eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

155157 spec = Spec `elem` opts

156− simpl = Simplify `elem` opts

158+ simpl = Simplify True `elem` opts

157159 atRepl = AtREPL `elem` opts

158160

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+

159165 ev ntimes stk top env (P _ n ty)

160166 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

161167 ev ntimes stk top env v

@@ -168,8 +174,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

168174 ev ntimes (n:stk) True env tm

169175 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty

170176 return $ VP nt n vty

171− [(CaseOp inl _ _ _ [] tree _ _, Public)] -> -- unoptimised version

172− if simpl && (not inl || elem n stk)

177+ [(CaseOp inl inr _ _ _ [] tree _ _, Public)] -> -- unoptimised version

178+ if canSimplify inl inr n stk

173179 then liftM (VP Ref n) (ev ntimes stk top env ty)

174180 else do c <- evCase ntimes (n:stk) top env [] [] tree

175181 case c of

@@ -232,8 +238,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

232238 = traceWhen traceon (show stk) $

233239 do let val = lookupDefAcc Nothing n atRepl ctxt

234240 case val of

235− [(CaseOp inl _ _ _ ns tree _ _, Public)] ->

236− if simpl && (not inl || elem n stk)

241+ [(CaseOp inl inr _ _ _ ns tree _ _, Public)] ->

242+ if canSimplify inl inr n stk

237243 then return $ unload env (VP Ref n ty) args

238244 else do c <- evCase ntimes (n:stk) top env ns args tree

239245 case c of

@@ -392,7 +398,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

392398 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

393399 [Function _ t] -> ev env t

394400 [TyDecl nt ty] -> return $ HP nt n ty

395− [CaseOp inl _ _ _ [] tree _ _] ->

401+ [CaseOp inl _ _ _ _ [] tree _ _] ->

396402 do c <- evCase env [] [] tree

397403 case c of

398404 (Nothing, _, _) -> return $ HP Ref n ty

@@ -422,7 +428,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

422428 app <- apply env sc' as

423429 wknH (-1) app

424430 apply env (HP Ref n ty) args

425− | [CaseOp _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

431+ | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

426432 = do c <- evCase env ns args tree

427433 case c of

428434 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -549,8 +555,8 @@ convEq ctxt = ceq [] where

549555 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of

550556 ([Function _ xdef], [Function _ ydef])

551557 -> ceq ((x,y):ps) xdef ydef

552− ([CaseOp _ _ _ _ _ xdef _ _],

553− [CaseOp _ _ _ _ _ ydef _ _])

558+ ([CaseOp _ _ _ _ _ _ xdef _ _],

559+ [CaseOp _ _ _ _ _ _ ydef _ _])

554560 -> caseeq ((x,y):ps) xdef ydef

555561 _ -> return False

556562

@@ -572,7 +578,8 @@ spec ctxt statics genv tm = error "spec undefined"

572578data Def = Function Type Term

573579 | TyDecl NameType Type

574580 | Operator Type Int ([Value] -> Maybe Value)

575− | CaseOp Bool Type -- bool for inlinable

581+ | CaseOp Bool Bool -- compile-time/run-time inlinable

582+ Type

576583 [Either Term (Term, Term)] -- original definition

577584 [([Name], Term, Term)] -- simplified definition

578585 [Name] SC -- Compile time case definition

@@ -585,7 +592,7 @@ instance Show Def where

585592 show (Function ty tm) = "Function: " ++ show (ty, tm)

586593 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

587594 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')

589596 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

590597 show ns ++ " " ++ show sc ++ "\n" ++

591598 show ns' ++ " " ++ show sc'

@@ -707,8 +714,9 @@ addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt

707714 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

708715 simpleCase tcase covering RunTime (FC "" 0) psrt) of

709716 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

710− let inl = alwaysInline || small n sc' in

711− addDef n (CaseOp inl ty ps_in ps args sc args' sc',

717+ let inl = alwaysInline in

718+ addDef n (CaseOp inl (inl || small n sc')

719+ ty ps_in ps args sc args' sc',

712720 access, Unchecked) ctxt in

713721 uctxt { definitions = ctxt' }

714722

@@ -716,15 +724,14 @@ simplifyCasedef :: Name -> Context -> Context

716724simplifyCasedef n uctxt

717725 = let ctxt = definitions uctxt

718726 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)] ->

720728 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)] ->

722730 let pdef = map debind $ map simpl ps_in in

723731 case simpleCase False True CompileTime (FC "" 0) pdef of

724732 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',

728735 acc, tot) ctxt

729736 _ -> ctxt in

730737 uctxt { definitions = ctxt' }

@@ -737,7 +744,7 @@ simplifyCasedef n uctxt

737744 (vs, x', y')

738745 debind (Left x) = let (vs, x') = depat [] x in

739746 (vs, x', Impossible)

740− simpl (Right (x, y)) = Right (x, simplify uctxt [] y)

747+ simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)

741748 simpl t = t

742749

743750addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

@@ -761,7 +768,7 @@ lookupTy root n ctxt

761768 (Function ty _) -> return ty

762769 (TyDecl _ ty) -> return ty

763770 (Operator ty _ _) -> return ty

764− (CaseOp _ ty _ _ _ _ _ _) -> return ty

771+ (CaseOp _ _ ty _ _ _ _ _ _) -> return ty

765772

766773isConName :: Maybe [String] -> Name -> Context -> Bool

767774isConName root n ctxt

@@ -777,7 +784,7 @@ isFnName root n ctxt

777784 case tfst def of

778785 (Function _ _) -> return True

779786 (Operator _ _ _) -> return True

780− (CaseOp _ _ _ _ _ _ _ _) -> return True

787+ (CaseOp _ _ _ _ _ _ _ _ _) -> return True

781788 _ -> return False

782789

783790lookupP :: Maybe [String] -> Name -> Context -> [Term]

@@ -786,7 +793,7 @@ lookupP root n ctxt

786793 p <- case def of

787794 (Function ty tm, a, _) -> return (P Ref n ty, a)

788795 (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)

790797 (Operator ty _ _, a, _) -> return (P Ref n ty, a)

791798 case snd p of

792799 Hidden -> []

src/IRTS/Compiler.hs+2−2

@@ -129,8 +129,8 @@ declArgs args n x = LFun n args x

129129

130130mkLDecl n (Function tm _) = do e <- ir tm

131131 return (declArgs [] n e)

132−mkLDecl n (CaseOp _ _ _ pats _ _ args sc) = do e <- ir (args, sc)

133− return (declArgs [] n e)

132+mkLDecl n (CaseOp _ _ _ _ pats _ _ args sc) = do e <- ir (args, sc)

133+ return (declArgs [] n e)

134134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

135135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

136136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))

src/Idris/Coverage.hs+2−2

@@ -338,7 +338,7 @@ checkTotality path fc n

338338 t' <- case t of

339339 Unchecked ->

340340 case lookupDef Nothing n ctxt of

341− [CaseOp _ _ _ pats _ _ _ _] ->

341+ [CaseOp _ _ _ _ pats _ _ _ _] ->

342342 do t' <- if AssertTotal `elem` opts

343343 then return $ Total []

344344 else calcTotality path fc n pats

@@ -401,7 +401,7 @@ buildSCG (_, n) = do

401401 ist <- get

402402 case lookupCtxt Nothing n (idris_callgraph ist) of

403403 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of

404− [CaseOp _ _ _ _ args sc _ _] ->

404+ [CaseOp _ _ _ _ _ args sc _ _] ->

405405 do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"

406406 ++ show sc

407407 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

299299-- show l ++ " = " ++

300300-- show r) pats))

301301 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

303303

304304 numArgs <- tclift $ sameLength pdef

305305

@@ -311,7 +311,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

311311 logLvl 5 $ "Patterns:\n" ++ show pats

312312 logLvl 5 $ "Optimised patterns:\n" ++ show optpats

313313

314− let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats

314+ let optpdef = map debind $ map (simpl True (tt_ctxt ist)) optpats

315315 tree@(CaseDef scargs sc _) <- tclift $

316316 simpleCase tcase False CompileTime fc pdef

317317 cov <- coverage

@@ -362,7 +362,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

362362 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

363363 i <- get

364364 case lookupDef Nothing n (tt_ctxt i) of

365− (CaseOp _ _ _ _ scargs sc scargs' sc' : _) ->

365+ (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

366366 do let calls = findCalls sc' scargs'

367367 let used = findUsedArgs sc' scargs'

368368 -- let scg = buildSCG i sc scargs

@@ -387,8 +387,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

387387

388388 getLHS (_, l, _) = l

389389

390− simpl ctxt (Right (x, y)) = Right (x, simplify ctxt [] y)

391− simpl ctxt t = t

390+ simpl rt ctxt (Right (x, y)) = Right (x, simplify ctxt rt [] y)

391+ simpl rt ctxt t = t

392392

393393 sameLength ((_, x, _) : xs)

394394 = do l <- sameLength xs

src/Idris/IBC.hs+4−2

@@ -612,11 +612,12 @@ instance Binary Def where

612612 put x1

613613 put x2

614614 put x3

615− CaseOp x1 x2 x3 x4 x5 x6 x7 x8 ->

615+ CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->

616616 do putWord8 3

617617 put x1

618618 put x2

619619 put x3

620+ -- no x3a

620621 put x4

621622 put x5

622623 put x6

@@ -638,12 +639,13 @@ instance Binary Def where

638639 3 -> do x1 <- get

639640 x2 <- get

640641 x3 <- get

642+ -- x3 <- get always []

641643 x4 <- get

642644 x5 <- get

643645 x6 <- get

644646 x7 <- get

645647 x8 <- get

646− return (CaseOp x1 x2 x3 x4 x5 x6 x7 x8)

648+ return (CaseOp x1 x2 x3 [] x4 x5 x6 x7 x8)

647649 _ -> error "Corrupted binary data for Def"

648650

649651instance Binary Accessibility where

src/Idris/REPL.hs+3−3

@@ -248,7 +248,7 @@ process fn (Search t) = iputStrLn "Not implemented"

248248process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

249249 ctxt <- getContext

250250 ist <- get

251− let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

251+ let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm

252252 iputStrLn (show (delab ist tm'))

253253

254254process fn (RmProof n')

@@ -312,7 +312,7 @@ process fn (Prove n')

312312process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

313313 ctxt <- getContext

314314 ist <- get

315− let tm' = simplify ctxt [] tm

315+ let tm' = simplify ctxt True [] tm

316316 iputStrLn (show (delab ist tm'))

317317process fn TTShell = do ist <- get

318318 let shst = initState (tt_ctxt ist)

@@ -349,7 +349,7 @@ process fn (Pattelab t)

349349

350350process fn (Missing n) = do i <- get

351351 case lookupDef Nothing n (tt_ctxt i) of

352− [CaseOp _ _ _ _ args t _ _]

352+ [CaseOp _ _ _ _ _ args t _ _]

353353 -> do tms <- genMissing n args t

354354 iputStrLn (showSep "\n" (map (showImp True) tms))

355355 [] -> iputStrLn $ show n ++ " undefined"