a1fb7a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Inline with blocks

a1fb7a3Edwin Brady12 years ago

src/IRTS/Compiler.hs+1

compare with master

unifiedsplit

@@ -204,6 +204,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

204

205 -- Always attempt to inline functions arising from 'case' expressions

206 caseName (SN (CaseN _)) = True

207+ caseName (SN (WithN _ _)) = True

207 caseName (NS n _) = caseName n

208 caseName (NS n _) = caseName n

208 caseName _ = False

209 caseName _ = False

209

210

src/IRTS/Lang.hs+33−33

@@ -14,6 +14,7 @@ data Endianness = Native | BE | LE deriving (Show, Eq)

14data LVar = Loc Int | Glob Name

15 deriving (Show, Eq)

17+-- ASSUMPTION: All variable bindings have unique names here

17data LExp = LV LVar

18data LExp = LV LVar

18 | LApp Bool LExp [LExp] -- True = tail call

19 | LApp Bool LExp [LExp] -- True = tail call

19 | LLazyApp Name [LExp] -- True = tail call

20 | LLazyApp Name [LExp] -- True = tail call

@@ -217,57 +218,56 @@ nextN = do i <- get

217doInline :: LDefs -> LDecl -> LDecl

218doInline :: LDefs -> LDecl -> LDecl

218doInline defs d@(LConstructor _ _ _) = d

219doInline defs d@(LConstructor _ _ _) = d

219doInline defs (LFun opts topn args exp)

220doInline defs (LFun opts topn args exp)

220− = let res = evalState (inlineWith (map (\n -> (n, LV (Glob n))) args) exp) 0 in

221+ = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in

221 LFun opts topn args res

222 LFun opts topn args res

222 where

223 where

223− inlineWith :: [(Name, LExp)] -> LExp -> State Int LExp

224+ inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp

224− inlineWith env var@(LV (Glob n)) = case lookup n env of

225+ inlineWith done env var@(LV (Glob n))

226+ = case lookup n env of

225 Just t -> return t

227 Just t -> return t

226 Nothing -> return var

228 Nothing -> return var

227− inlineWith env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith env) es)

229+ inlineWith done env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith done env) es)

228− inlineWith env (LForce e) = LForce <$> inlineWith env e

230+ inlineWith done env (LForce e) = LForce <$> inlineWith done env e

229− inlineWith env (LLazyExp e) = LLazyExp <$> inlineWith env e

231+ inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e

230 -- Extend the environment for Let and Lam so that bound names aren't

232 -- Extend the environment for Let and Lam so that bound names aren't

231 -- expanded with any top level argument definitions they shadow

233 -- expanded with any top level argument definitions they shadow

232− inlineWith env (LLet n val sc)

234+ inlineWith done env (LLet n val sc)

233 = do n' <- nextN

235 = do n' <- nextN

234− LLet n' <$> inlineWith env val <*>

236+ LLet n' <$> inlineWith done env val <*>

235− inlineWith ((n, LV (Glob n')) : env) sc

237+ inlineWith done ((n, LV (Glob n')) : env) sc

236− inlineWith env (LLam args sc)

238+ inlineWith done env (LLam args sc)

237 = do ns' <- mapM (\n -> do n' <- nextN

239 = do ns' <- mapM (\n -> do n' <- nextN

238 return (n, n')) args

240 return (n, n')) args

239 LLam (map snd ns') <$>

241 LLam (map snd ns') <$>

240− inlineWith (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) sc

242+ inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) sc

241− inlineWith env (LProj exp i) = LProj <$> inlineWith env exp <*> return i

243+ inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i

242− inlineWith env (LCon loc i n es)

244+ inlineWith done env (LCon loc i n es)

243− = LCon loc i n <$> mapM (inlineWith env) es

245+ = LCon loc i n <$> mapM (inlineWith done env) es

244− inlineWith env (LCase ty e alts)

246+ inlineWith done env (LCase ty e alts)

245− = LCase ty <$> inlineWith env e <*> mapM (inlineWithAlt env) alts

247+ = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts

246− inlineWith env (LOp f es) = LOp f <$> mapM (inlineWith env) es

248+ inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es

247 -- the interesting case!

249 -- the interesting case!

248− inlineWith env (LApp t (LV (Glob n)) es)

250+ inlineWith done env (LApp t (LV (Glob n)) es)

251+ | n `notElem` done,

249− | [LFun opts _ args body] <- lookupCtxt n defs,

252+ [LFun opts _ args body] <- lookupCtxt n defs,

250 Inline `elem` opts,

253 Inline `elem` opts,

251 length es == length args

254 length es == length args

252− = do es' <- mapM (inlineWith env) es

255+ = do es' <- mapM (inlineWith done env) es

253− inlineWith (zip args es' ++ env) body

256+ inlineWith (n : done) (zip args es' ++ env) body

254−-- inlineWith

255−-- -- inlineWith env

256−-- (substLExp (zip args es) body)

257− inlineWith env (LApp t f es)

257+ inlineWith done env (LApp t f es)

258− = LApp t <$> inlineWith env f <*> mapM (inlineWith env) es

258+ = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es

259− inlineWith env (LForeign l t s args)

259+ inlineWith done env (LForeign l t s args)

260− = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith env e

260+ = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e

261 return (t, e')) args

262− inlineWith env t = return t

262+ inlineWith done env t = return t

263

264− inlineWithAlt env (LConCase i n es rhs)

264+ inlineWithAlt done env (LConCase i n es rhs)

265 = do ns' <- mapM (\n -> do n' <- nextN

266 return (n, n')) es

267 LConCase i n (map snd ns') <$>

268− inlineWith (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs

268+ inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs

269− inlineWithAlt env (LConstCase c e) = LConstCase c <$> inlineWith env e

269+ inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e

270− inlineWithAlt env (LDefaultCase e) = LDefaultCase <$> inlineWith env e

270+ inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e

271

272-- substLExp :: [(Name, LExp)] -> LExp -> LExp

273-- substLExp env (LV (Glob n)) | Just t <- lookup n env = t

src/Idris/Core/Binary.hs+6

@@ -78,6 +78,9 @@ instance Binary SpecialName where

78 CaseN x1 -> do putWord8 4; put x1

79 ElimN x1 -> do putWord8 5; put x1

80 InstanceCtorN x1 -> do putWord8 6; put x1

81+ WithN x1 x2 -> do putWord8 7

82+ put x1

83+ put x2

81 get

84 get

82 = do i <- getWord8

85 = do i <- getWord8

83 case i of

86 case i of

@@ -99,6 +102,9 @@ instance Binary SpecialName where

99 return (ElimN x1)

102 return (ElimN x1)

100 6 -> do x1 <- get

103 6 -> do x1 <- get

101 return (InstanceCtorN x1)

104 return (InstanceCtorN x1)

105+ 7 -> do x1 <- get

106+ x2 <- get

107+ return (WithN x1 x2)

102 _ -> error "Corrupted binary data for SpecialName"

108 _ -> error "Corrupted binary data for SpecialName"

103

109

104

110

src/Idris/Core/DeepSeq.hs+1

@@ -14,6 +14,7 @@ instance NFData Name where

15instance NFData SpecialName where

16 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

17+ rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

17 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

18 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

18 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

19 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

19 rnf (MethodN x1) = rnf x1 `seq` ()

20 rnf (MethodN x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+3

@@ -305,6 +305,7 @@ deriving instance NFData Name

305!-}

306

307data SpecialName = WhereN Int Name Name

308+ | WithN Int Name

308 | InstanceN Name [T.Text]

309 | InstanceN Name [T.Text]

309 | ParentN Name T.Text

310 | ParentN Name T.Text

310 | MethodN Name

311 | MethodN Name

@@ -349,6 +350,7 @@ instance Show Name where

349

350

350instance Show SpecialName where

351instance Show SpecialName where

351 show (WhereN i p c) = show p ++ ", " ++ show c

352 show (WhereN i p c) = show p ++ ", " ++ show c

353+ show (WithN i n) = "with block in " ++ show n

352 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

354 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

353 show (MethodN m) = "method " ++ show m

355 show (MethodN m) = "method " ++ show m

354 show (ParentN p c) = show p ++ "#" ++ T.unpack c

356 show (ParentN p c) = show p ++ "#" ++ T.unpack c

@@ -364,6 +366,7 @@ showCG (MN _ u) | u == txt "underscore" = "_"

364showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

366showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

365showCG (SN s) = showCG' s

367showCG (SN s) = showCG' s

366 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

368 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

369+ showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i

367 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

370 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

368 showCG' (MethodN m) = '!':showCG m

371 showCG' (MethodN m) = '!':showCG m

369 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

372 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

src/Idris/Elab/Clause.hs+1−1

@@ -722,7 +722,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

722 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

723 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

724 logLvl 5 ("New function type " ++ show wtype)

725− let wname = sMN windex (show fname)

725+ let wname = SN (WithN windex fname)

726

727 let imps = getImps wtype -- add to implicits context

728 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

test/reg010/expected+1−1

@@ -1,4 +1,4 @@

1−reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

1+reg010.idr:5:15:When elaborating right hand side of with block in usubst.unsafeSubst:

2Can't unify

3 P x

4with

test/reg018/expected+1−1

@@ -1,5 +1,5 @@

1reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

3reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

4−reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4+reg018c.idr:19:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf

5reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/reg028/expected+2−2

@@ -1,2 +1,2 @@

1−reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad16}

1+reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

2−reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'18}

2+reg028a.idr:11:1:tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/tutorial006/expected+1−1

@@ -10,7 +10,7 @@ When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:

10 [92mplus[0m [95mn[0m [95mn[0m

11 with

12 [92mplus[0m [95mn[0m [95mm[0m

13−tutorial006b.idr:10:10:When elaborating right hand side of Main.parity:

13+tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

14Can't unify

15 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

16with