9836a07 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Inlining - Evaluator now supports run-time terms

In particular this reduces type class overhead. NOTE: Breaks the javascript code generation because it doesn't seem to support projection from global names, which can now arise as a result of inlinings. A temporary fix for this would be to update ElabDecls.hs:733 to simple_rt ctxt t = t which disables the simplification of run time terms.

commit9836a07175935d53eb9fa3b837c98695cfe4d56f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Nov 2013, 18:48 (13 years ago) parent521dc75

8 files changed+47−9

compare with master

unifiedsplit

benchmarks/trivial/sortvec.idr+1 src/Core/Evaluate.hs+32−4 src/IRTS/Bytecode.hs+2 src/IRTS/CodegenJava.hs+3−1 src/IRTS/CodegenJavaScript.hs+1−1 src/IRTS/CodegenLLVM.hs+1 src/IRTS/Defunctionalise.hs+2−2 src/Idris/ElabDecls.hs+5−1

benchmarks/trivial/sortvec.idr+1

@@ -18,6 +18,7 @@ mkSortVec (S k) = return (fromInteger !(rndInt 0 10000) :: !(mkSortVec k))

1818

1919main : IO ()

2020main = do (_ :: arg :: _) <- getArgs

21+-- let arg = "2000"

2122 let vec = runPure [123456789] (mkSortVec (fromInteger (cast arg)))

2223 putStrLn "Made vector"

2324 print (vsort vec)

src/Core/Evaluate.hs+32−4

@@ -2,7 +2,7 @@

22 PatternGuards #-}

44module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5− simplify, specialise, hnf, convEq, convEq',

5+ rt_simplify, simplify, specialise, hnf, convEq, convEq',

66 Def(..), CaseInfo(..), CaseDefs(..),

77 Accessibility(..), Totality(..), PReason(..),

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

@@ -45,7 +45,9 @@ data Value = VP NameType Name Value

4545 | VApp Value Value

4646 | VType UExp

4747 | VErased

48+ | VImpossible

4849 | VConstant Const

50+ | VProj Value Int

4951-- | VLazy Env [Value] Term

5052 | VTmp Int

5153

@@ -104,6 +106,18 @@ simplify ctxt env t

104106 [Simplify]

105107 quote 0 val) initEval

106108

109+-- | Simplify for run-time (i.e. basic inlining)

110+rt_simplify :: Context -> Env -> TT Name -> TT Name

111+rt_simplify ctxt env t

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

113+ (UN "assert_smaller", 0),

114+ (UN "par", 0),

115+ (UN "prim__syntactic_eq", 0),

116+ (UN "prim_fork", 0)]

117+ (map finalEntry env) (finalise t)

118+ [RunTT]

119+ quote 0 val) initEval

120+

107121-- | Reduce a term to head normal form

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

109123hnf ctxt env t

@@ -170,6 +184,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

170184 -- returns 'True' if the function should block

171185 -- normal evaluation should return false

172186 blockSimplify (CaseInfo inl dict) n stk

187+ | RunTT `elem` opts

188+ = not inl || elem n stk

173189 | Simplify `elem` opts

174190 = (not (inl || dict) || elem n stk)

175191 || (n == UN "prim__syntactic_eq")

@@ -195,10 +211,11 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

195211 [(CaseOp ci _ _ _ cd, acc)]

196212 | acc == Public &&

197213 null (fst (cases_totcheck cd)) -> -- unoptimised version

198− let (_, tree) = getCases cd in

214+ let (ns, tree) = getCases cd in

199215 if blockSimplify ci n stk

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

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

217+ else -- traceWhen runtime (show (n, ns, tree)) $

218+ do c <- evCase ntimes n (n:stk) top env ns [] tree

202219 case c of

203220 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)

204221 (Just v, _) -> return v

@@ -242,8 +259,15 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

242259 = do f' <- ev ntimes stk False env f

243260 a' <- ev ntimes stk False env a

244261 evApply ntimes stk top env [a'] f'

262+ ev ntimes stk top env (Proj t i)

263+ = do t' <- ev ntimes stk top env t

264+ return (doProj t' (getValArgs t'))

265+ where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i

266+ doProj t' _ = VProj t' i

267+

245268 ev ntimes stk top env (Constant c) = return $ VConstant c

246269 ev ntimes stk top env Erased = return VErased

270+ ev ntimes stk top env Impossible = return VImpossible

247271 ev ntimes stk top env (TType i) = return $ VType i

248272

249273 evApply ntimes stk top env args (VApp f a)

@@ -269,7 +293,8 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

269293 let (ns, tree) = getCases cd in

270294 if blockSimplify ci n stk

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

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

296+ else -- traceWhen runtime (show (n, ns, tree)) $

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

273298 case c of

274299 (Nothing, _) -> return $ unload env (VP Ref n ty) args

275300 (Just v, rest) -> evApply ntimes stk top env rest v

@@ -443,6 +468,9 @@ instance Quote Value where

443468 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

444469 quote i (VType u) = return $ TType u

445470 quote i VErased = return $ Erased

471+ quote i VImpossible = return $ Impossible

472+ quote i (VProj v j) = do v' <- quote i v

473+ return (Proj v' j)

446474 quote i (VConstant c) = return $ Constant c

447475 quote i (VTmp x) = return $ V (i - x - 1)

448476

src/IRTS/Bytecode.hs+2

@@ -80,6 +80,7 @@ bc reg (SForeign l t fname args) r

8080bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

8181bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]

8282 ++ clean r

83+-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it

8384bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

8485 where getL (Loc x) = L x

8586bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r

@@ -93,6 +94,7 @@ bc reg (SCase (Loc l) alts) r

9394 | otherwise = conCase True reg (L l) alts r

9495bc reg (SChkCase (Loc l) alts) r

9596 = conCase False reg (L l) alts r

97+bc reg t r = error $ "Can't compile " ++ show t

9698

9799isConst [] = False

98100isConst (SConstCase _ _ : xs) = True

src/IRTS/CodegenJava.hs+3−1

@@ -485,8 +485,10 @@ mkExp pp (SApp pushTail name args) =

485485-- Bindings

486486mkExp pp (SLet var newExp inExp) =

487487 mkLet pp var newExp inExp

488−mkExp pp (SUpdate var newExp) =

488+mkExp pp (SUpdate var@(Loc i) newExp) = -- can only update locals

489489 mkUpdate pp var newExp

490+mkExp pp (SUpdate var newExp) =

491+ mkExp pp newExp

490492

491493-- Objects

492494mkExp pp (SCon conId _ args) =

src/IRTS/CodegenJavaScript.hs+1−1

@@ -1044,7 +1044,7 @@ translateExpression (SCon i name vars) =

10441044 , JSArray $ map JSVar vars

10451045 ]

10461046

1047−translateExpression (SUpdate var e) =

1047+translateExpression (SUpdate var@(Loc i) e) =

10481048 JSAssign (JSVar var) (translateExpression e)

10491049

10501050translateExpression (SProj var i) =

src/IRTS/CodegenLLVM.hs+1

@@ -447,6 +447,7 @@ cgExpr (SUpdate (Loc level) expr) = do

447447 val <- cgExpr expr

448448 modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }

449449 return val

450+cgExpr (SUpdate x expr) = cgExpr expr

450451cgExpr (SCon tag name args) = do

451452 argSlots <- mapM var args

452453 case sequence argSlots of

src/IRTS/Defunctionalise.hs+2−2

@@ -97,8 +97,8 @@ addApps defs (n, LFun _ _ args e)

9797 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)

9898 aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)

9999 aa env (LProj t@(LV (Glob n)) i)

100− = do t' <- aa env t

101− return $ DProj (DUpdate n (eEVAL t')) i

100+ | n `elem` env = do t' <- aa env t

101+ return $ DProj (DUpdate n (eEVAL t')) i

102102 aa env (LProj t i) = do t' <- aa env t

103103 return $ DProj (eEVAL t') i

104104 aa env (LCase e alts) = do e' <- aa env e

src/Idris/ElabDecls.hs+5−1

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

642642 let pcover = null pmissing

643643

644644 -- pdef' is the version that gets compiled for run-time

645− pdef' <- applyOpts optpdef

645+ pdef_in' <- applyOpts optpdef

646+ let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'

647+

646648 logLvl 5 $ "After data structure transformations:\n" ++ show pdef'

647649

648650 ist <- getIState

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

728730 simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

729731 simple_lhs ctxt t = t

730732

733+ simple_rt ctxt (p, x, y) = (p, x, rt_simplify ctxt [] y)

734+

731735 specNames [] = Nothing

732736 specNames (Specialise ns : _) = Just ns

733737 specNames (_ : xs) = specNames xs