a1fb7a3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Inline with blocks

commita1fb7a31446a47ad3041ac53931865edf8377e5f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 19 Aug 2014, 16:21 (12 years ago) parent5695e4c

10 files changed+50−39

compare with master

unifiedsplit

src/IRTS/Compiler.hs+1 src/IRTS/Lang.hs+33−33 src/Idris/Core/Binary.hs+6 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+3 src/Idris/Elab/Clause.hs+1−1 test/reg010/expected+1−1 test/reg018/expected+1−1 test/reg028/expected+2−2 test/tutorial006/expected+1−1

src/IRTS/Compiler.hs+1

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

204204

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

206206 caseName (SN (CaseN _)) = True

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

207208 caseName (NS n _) = caseName n

208209 caseName _ = False

209210

src/IRTS/Lang.hs+33−33

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

1414data LVar = Loc Int | Glob Name

1515 deriving (Show, Eq)

1616

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

1718data LExp = LV LVar

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

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

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

217218doInline :: LDefs -> LDecl -> LDecl

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

219220doInline 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

221222 LFun opts topn args res

222223 where

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

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

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

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

226+ = case lookup n env of

225227 Just t -> return t

226228 Nothing -> return var

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

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

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

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

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

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

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

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

232− inlineWith env (LLet n val sc)

234+ inlineWith done env (LLet n val sc)

233235 = do n' <- nextN

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

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

236− inlineWith env (LLam args sc)

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

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

238+ inlineWith done env (LLam args sc)

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

238240 return (n, n')) args

239241 LLam (map snd ns') <$>

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

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

242− inlineWith env (LCon loc i n es)

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

244− inlineWith env (LCase ty e alts)

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

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

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

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

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

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

246+ inlineWith done env (LCase ty e alts)

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

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

247249 -- the interesting case!

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

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

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

251+ | n `notElem` done,

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

250253 Inline `elem` opts,

251254 length es == length args

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

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

254−-- inlineWith

255−-- -- inlineWith env

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

257− inlineWith env (LApp t f es)

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

259− inlineWith env (LForeign l t s args)

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

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

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

257+ inlineWith done env (LApp t f es)

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

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

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

261261 return (t, e')) args

262− inlineWith env t = return t

262+ inlineWith done env t = return t

263263

264− inlineWithAlt env (LConCase i n es rhs)

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

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

266266 return (n, n')) es

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

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

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

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

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

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

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

271271

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

273273-- 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

7878 CaseN x1 -> do putWord8 4; put x1

7979 ElimN x1 -> do putWord8 5; put x1

8080 InstanceCtorN x1 -> do putWord8 6; put x1

81+ WithN x1 x2 -> do putWord8 7

82+ put x1

83+ put x2

8184 get

8285 = do i <- getWord8

8386 case i of

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

99102 return (ElimN x1)

100103 6 -> do x1 <- get

101104 return (InstanceCtorN x1)

105+ 7 -> do x1 <- get

106+ x2 <- get

107+ return (WithN x1 x2)

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

103109

104110

src/Idris/Core/DeepSeq.hs+1

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

1414

1515instance NFData SpecialName where

1616 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` ()

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

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

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

src/Idris/Core/TT.hs+3

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

305305!-}

306306

307307data SpecialName = WhereN Int Name Name

308+ | WithN Int Name

308309 | InstanceN Name [T.Text]

309310 | ParentN Name T.Text

310311 | MethodN Name

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

349350

350351instance Show SpecialName where

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

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

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

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

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

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

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

365367showCG (SN s) = showCG' s

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

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

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

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

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

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

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

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

725− let wname = sMN windex (show fname)

725+ let wname = SN (WithN windex fname)

726726

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

728728 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:

22Can't unify

33 P x

44with

test/reg018/expected+1−1

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

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

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

33reg018b.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

55reg018d.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}

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

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: with block in tbad.qsort'

test/tutorial006/expected+1−1

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

1010 [92mplus[0m [95mn[0m [95mn[0m

1111 with

1212 [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:

1414Can't unify

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

1616with