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

git.iko.soy/Idris-dev

on master help sign in

Inlining - Evaluator now supports run-time terms

9836a07Edwin Brady13 years ago

benchmarks/trivial/sortvec.idr+1

compare with master

unifiedsplit

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

19main : IO ()

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

21+-- let arg = "2000"

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

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

22 putStrLn "Made vector"

23 putStrLn "Made vector"

23 print (vsort vec)

24 print (vsort vec)

src/Core/Evaluate.hs+32−4

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

2 PatternGuards #-}

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

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

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

6 Def(..), CaseInfo(..), CaseDefs(..),

7 Accessibility(..), Totality(..), PReason(..),

8 Context, initContext, ctxtAlist, uconstraints, next_tvar,

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

45 | VApp Value Value

46 | VType UExp

47 | VErased

48+ | VImpossible

48 | VConstant Const

49 | VConstant Const

50+ | VProj Value Int

49-- | VLazy Env [Value] Term

51-- | VLazy Env [Value] Term

50 | VTmp Int

52 | VTmp Int

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

104 [Simplify]

106 [Simplify]

105 quote 0 val) initEval

107 quote 0 val) initEval

106

108

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+

107-- | Reduce a term to head normal form

121-- | Reduce a term to head normal form

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

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

109hnf ctxt env t

123hnf ctxt env t

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

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

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

171 -- normal evaluation should return false

185 -- normal evaluation should return false

172 blockSimplify (CaseInfo inl dict) n stk

186 blockSimplify (CaseInfo inl dict) n stk

187+ | RunTT `elem` opts

188+ = not inl || elem n stk

173 | Simplify `elem` opts

189 | Simplify `elem` opts

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

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

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

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

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

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

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

196 | acc == Public &&

212 | acc == Public &&

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

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

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

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

199 if blockSimplify ci n stk

215 if blockSimplify ci n stk

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

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

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

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

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

202 case c of

219 case c of

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

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

204 (Just v, _) -> return v

221 (Just v, _) -> return v

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

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

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

243 a' <- ev ntimes stk False env a

260 a' <- ev ntimes stk False env a

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

261 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+

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

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

246 ev ntimes stk top env Erased = return VErased

269 ev ntimes stk top env Erased = return VErased

270+ ev ntimes stk top env Impossible = return VImpossible

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

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

248

272

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

273 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

269 let (ns, tree) = getCases cd in

293 let (ns, tree) = getCases cd in

270 if blockSimplify ci n stk

294 if blockSimplify ci n stk

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

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

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

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

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

273 case c of

298 case c of

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

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

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

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

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

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

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

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

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

445 quote i VErased = return $ Erased

470 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)

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

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

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

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

448

476

src/IRTS/Bytecode.hs+2

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

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

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

82 ++ clean r

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

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

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

84 where getL (Loc x) = L x

85 where getL (Loc x) = L x

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

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

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

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

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

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

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

95 = conCase False reg (L l) alts r

96 = conCase False reg (L l) alts r

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

97isConst [] = False

99isConst [] = False

98isConst (SConstCase _ _ : xs) = True

100isConst (SConstCase _ _ : xs) = True

src/IRTS/CodegenJava.hs+3−1

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

485-- Bindings

486mkExp pp (SLet var newExp inExp) =

487 mkLet pp var newExp inExp

488−mkExp pp (SUpdate var newExp) =

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

489 mkUpdate pp var newExp

490+mkExp pp (SUpdate var newExp) =

491+ mkExp pp newExp

490

492

491-- Objects

493-- Objects

492mkExp pp (SCon conId _ args) =

494mkExp pp (SCon conId _ args) =

src/IRTS/CodegenJavaScript.hs+1−1

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

1044 , JSArray $ map JSVar vars

1045 ]

1046

1047−translateExpression (SUpdate var e) =

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

1048 JSAssign (JSVar var) (translateExpression e)

1049

1050translateExpression (SProj var i) =

src/IRTS/CodegenLLVM.hs+1

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

447 val <- cgExpr expr

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

449 return val

450+cgExpr (SUpdate x expr) = cgExpr expr

450cgExpr (SCon tag name args) = do

451cgExpr (SCon tag name args) = do

451 argSlots <- mapM var args

452 argSlots <- mapM var args

452 case sequence argSlots of

453 case sequence argSlots of

src/IRTS/Defunctionalise.hs+2−2

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

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

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

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

100− = do t' <- aa env t

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

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

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

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

103 return $ DProj (eEVAL t') i

104 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

642 let pcover = null pmissing

643

644 -- 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+

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

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

647

649

648 ist <- getIState

650 ist <- getIState

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

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

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

729 simple_lhs ctxt t = t

731 simple_lhs ctxt t = t

730

732

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

734+

731 specNames [] = Nothing

735 specNames [] = Nothing

732 specNames (Specialise ns : _) = Just ns

736 specNames (Specialise ns : _) = Just ns

733 specNames (_ : xs) = specNames xs

737 specNames (_ : xs) = specNames xs