fb2b17d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add collapsing optimisation and more aggressive erasure

fb2b17dEdwin Brady14 years ago

src/Core/CaseTree.hs+4−2

compare with master

unifiedsplit

@@ -168,8 +168,10 @@ simpleCase tc cover phase fc cs

168 defaultCase True = STerm Erased

169 defaultCase False = UnmatchedCase "Error"

170

171− chkAccessible (avs, l, c) = do mapM_ (acc l) avs

171+ chkAccessible (avs, l, c)

172+ | phase == RunTime = return (l, c)

173+ | otherwise = do mapM_ (acc l) avs

172− return (l, c)

174+ return (l, c)

173

175

174 acc [] n = Error (Inaccessible n)

176 acc [] n = Error (Inaccessible n)

175 acc (PV x : xs) n | x == n = OK ()

177 acc (PV x : xs) n | x == n = OK ()

src/IRTS/Compiler.hs+9−2

@@ -166,11 +166,16 @@ instance ToIR (TT Name) where

166 = irCon env t a n args

167 | (P _ n _, args) <- unApply tm

168 = do i <- get

169+ let collapse = case lookupCtxt Nothing n (idris_optimisation i) of

170+ [oi] -> collapsible oi

171+ _ -> False

169 let unused = case lookupCtxt Nothing n (idris_callgraph i) of

172 let unused = case lookupCtxt Nothing n (idris_callgraph i) of

170 [CGInfo _ _ _ unusedpos] -> unusedpos

173 [CGInfo _ _ _ unusedpos] -> unusedpos

171 _ -> []

174 _ -> []

172 args' <- mapM (ir' env) args

175 args' <- mapM (ir' env) args

176+ if collapse then return LNothing

173− return (LApp False (LV (Glob n)) (mkUnused unused 0 args'))

177+ else return (LApp False (LV (Glob n))

178+ (mkUnused unused 0 args'))

174 | (f, args) <- unApply tm

179 | (f, args) <- unApply tm

175 = do f' <- ir' env f

180 = do f' <- ir' env f

176 args' <- mapM (ir' env) args

181 args' <- mapM (ir' env) args

@@ -194,7 +199,9 @@ instance ToIR (TT Name) where

194 return $ LProj t' i

199 return $ LProj t' i

195 ir' env (Constant c) = return $ LConst c

200 ir' env (Constant c) = return $ LConst c

196 ir' env (Set _) = return $ LNothing

201 ir' env (Set _) = return $ LNothing

202+ ir' env Erased = return $ LNothing

203+ ir' env Impossible = return $ LNothing

197− ir' env _ = return $ LError "Impossible"

204+-- ir' env _ = return $ LError "Impossible"

198

205

199 irCon env t arity n args

206 irCon env t arity n args

200 | length args == arity = buildApp env (LV (Glob n)) args

207 | length args == arity = buildApp env (LV (Glob n)) args

src/Idris/DataOpts.hs+122−9

@@ -15,8 +15,8 @@ import Debug.Trace

15-- optimisations

17forceArgs :: Name -> Type -> Idris ()

18+forceArgs n t = do i <- getIState

18−forceArgs n t = do let fargs = force 0 t

19+ let fargs = force i 0 t

19− i <- getIState

20 copt <- case lookupCtxt Nothing n (idris_optimisation i) of

21 [] -> return $ Optimise False [] []

22 (op:_) -> return op

@@ -26,13 +26,22 @@ forceArgs n t = do let fargs = force 0 t

26 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++

27 show t

28 where

29− force :: Int -> Term -> [Int]

29+ force :: IState -> Int -> Term -> [Int]

30− force i (Bind _ (Pi _) sc)

30+ force ist i (Bind _ (Pi ty) sc)

31+ | collapsibleIn ist ty

32+ = nub $ i : (force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc)

31− = force (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc

33+ | otherwise = force ist (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc

32− force _ sc@(App f a)

34+ force _ _ sc@(App f a)

33 | (_, args) <- unApply sc

35 | (_, args) <- unApply sc

34 = nub $ concatMap guarded args

36 = nub $ concatMap guarded args

35− force _ _ = []

37+ force _ _ _ = []

38+

39+ collapsibleIn i t

40+ | (P _ tn _, _) <- unApply t

41+ = case lookupCtxt Nothing tn (idris_optimisation i) of

42+ [oi] -> collapsible oi

43+ _ -> False

44+ | otherwise = False

37 isF (P _ (MN force "?") _) = Just force

46 isF (P _ (MN force "?") _) = Just force

38 isF _ = Nothing

47 isF _ = Nothing

@@ -49,24 +58,98 @@ forceArgs n t = do let fargs = force 0 t

50collapseCons :: Name -> [(Name, Type)] -> Idris ()

59collapseCons :: Name -> [(Name, Type)] -> Idris ()

51collapseCons ty cons =

60collapseCons ty cons =

52− do i <- getIState

61+ do i <- getIState

53− return ()

62+ let cons' = map (\ (n, t) -> (n, map snd (getArgTys t))) cons

63+ allFR <- mapM (forceRec i) cons'

64+ if and allFR then detaggable (map getRetTy (map snd cons))

65+ else return () -- not collapsible as not detaggable

66+ where

67+ setCollapsible :: Name -> Idris ()

68+ setCollapsible n

69+ = do i <- getIState

70+ iLOG $ show n ++ " collapsible"

71+ case lookupCtxt Nothing n (idris_optimisation i) of

72+ (oi:_) -> do let oi' = oi { collapsible = True }

73+ let opts = addDef n oi' (idris_optimisation i)

74+ putIState (i { idris_optimisation = opts })

75+ [] -> do let oi = Optimise True [] []

76+ let opts = addDef n oi (idris_optimisation i)

77+ putIState (i { idris_optimisation = opts })

78+ addIBC (IBCOpt n)

79+

80+ forceRec :: IState -> (Name, [Type]) -> Idris Bool

81+ forceRec i (n, ts)

82+ = case lookupCtxt Nothing n (idris_optimisation i) of

83+ (oi:_) -> checkFR (forceable oi) 0 ts

84+ _ -> return False

85+ checkFR fs i [] = return True

86+ checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs

87+ checkFR fs i (t : xs)

88+ -- must be recursive or type is not collapsible

89+ = do let rt = getRetTy t

90+ if (ty `elem` freeNames rt)

91+ then checkFR fs (i+1) xs

92+ else return False

93+

94+ detaggable :: [Type] -> Idris ()

95+ detaggable rtys

96+ = do let rtyArgs = map (snd . unApply) rtys

97+ -- if every rtyArgs is disjoint with every other, it's detaggable,

98+ -- therefore also collapsible given forceable/recursive check

99+ if disjoint rtyArgs

100+ then mapM_ setCollapsible (ty : map fst cons)

101+ else return ()

102+

103+ disjoint :: [[Term]] -> Bool

104+ disjoint [] = True

105+ disjoint [x] = True

106+ disjoint (x : xs) = anyDisjoint x xs && disjoint xs

107+

108+ anyDisjoint x [] = True

109+ anyDisjoint x (y : ys) = disjointCons x y

110+

111+ disjointCons [] [] = False

112+ disjointCons [] y = False

113+ disjointCons x [] = False

114+ disjointCons (x : xs) (y : ys)

115+ = disjointCon x y || disjointCons xs ys

116+

117+ disjointCon x y = let (cx, _) = unApply x

118+ (cy, _) = unApply y in

119+ case (cx, cy) of

120+ (P (DCon _ _) nx _, P (DCon _ _) ny _) -> nx /= ny

121+ _ -> False

122

55class Optimisable term where

123class Optimisable term where

56 applyOpts :: term -> Idris term

124 applyOpts :: term -> Idris term

125+ stripCollapsed :: term -> Idris term

126

58instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

127instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

59 applyOpts (x, y) = do x' <- applyOpts x

128 applyOpts (x, y) = do x' <- applyOpts x

60 y' <- applyOpts y

129 y' <- applyOpts y

61 return (x', y')

130 return (x', y')

131+ stripCollapsed (x, y) = do x' <- stripCollapsed x

132+ y' <- stripCollapsed y

133+ return (x', y')

134+

135

63instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where

136instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where

64 applyOpts (v, x, y) = do x' <- applyOpts x

137 applyOpts (v, x, y) = do x' <- applyOpts x

65 y' <- applyOpts y

138 y' <- applyOpts y

66 return (v, x', y')

139 return (v, x', y')

140+ stripCollapsed (v, x, y) = do x' <- stripCollapsed x

141+ y' <- stripCollapsed y

142+ return (v, x', y')

143

68instance Optimisable a => Optimisable [a] where

144instance Optimisable a => Optimisable [a] where

69 applyOpts = mapM applyOpts

145 applyOpts = mapM applyOpts

146+ stripCollapsed = mapM stripCollapsed

147+

148+instance Optimisable a => Optimisable (Either a (a, a)) where

149+ applyOpts (Left t) = do t' <- applyOpts t; return $ Left t'

150+ applyOpts (Right t) = do t' <- applyOpts t; return $ Right t'

151+ stripCollapsed (Left t) = do t' <- stripCollapsed t; return $ Left t'

152+ stripCollapsed (Right t) = do t' <- stripCollapsed t; return $ Right t'

153

71-- Raw is for compile time optimisation (before type checking)

154-- Raw is for compile time optimisation (before type checking)

72-- Term is for run time optimisation (after type checking, collapsing allowed)

155-- Term is for run time optimisation (after type checking, collapsing allowed)

@@ -90,12 +173,19 @@ instance Optimisable Raw where

90 applyOpts (RForce t) = applyOpts t

173 applyOpts (RForce t) = applyOpts t

91 applyOpts t = return t

174 applyOpts t = return t

175

176+ stripCollapsed t = return t

177+

93instance Optimisable t => Optimisable (Binder t) where

178instance Optimisable t => Optimisable (Binder t) where

94 applyOpts (Let t v) = do t' <- applyOpts t

179 applyOpts (Let t v) = do t' <- applyOpts t

95 v' <- applyOpts v

180 v' <- applyOpts v

96 return (Let t' v')

181 return (Let t' v')

97 applyOpts b = do t' <- applyOpts (binderTy b)

182 applyOpts b = do t' <- applyOpts (binderTy b)

98 return (b { binderTy = t' })

183 return (b { binderTy = t' })

184+ stripCollapsed (Let t v) = do t' <- stripCollapsed t

185+ v' <- stripCollapsed v

186+ return (Let t' v')

187+ stripCollapsed b = do t' <- stripCollapsed (binderTy b)

188+ return (b { binderTy = t' })

189

100

190

101applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

191applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

@@ -110,6 +200,11 @@ applyDataOpt oi n args

110-- Run-time: do everything

200-- Run-time: do everything

111

201

112instance Optimisable (TT Name) where

202instance Optimisable (TT Name) where

203+ applyOpts c@(P (DCon t arity) n _)

204+ = do i <- getIState

205+ case lookupCtxt Nothing n (idris_optimisation i) of

206+ (oi:_) -> return $ applyDataOptRT oi n t arity []

207+ _ -> return c

113 applyOpts t@(App f a)

208 applyOpts t@(App f a)

114 | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

209 | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

115 = do args' <- mapM applyOpts args

210 = do args' <- mapM applyOpts args

@@ -123,8 +218,25 @@ instance Optimisable (TT Name) where

123 applyOpts (Bind n b t) = do b' <- applyOpts b

218 applyOpts (Bind n b t) = do b' <- applyOpts b

124 t' <- applyOpts t

219 t' <- applyOpts t

125 return (Bind n b' t')

220 return (Bind n b' t')

221+ applyOpts (Proj t i) = do t' <- applyOpts t

222+ return (Proj t' i)

126 applyOpts t = return t

223 applyOpts t = return t

127

224

225+ stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x

226+ = do i <- getIState

227+ case lookupCtxt Nothing ty (idris_optimisation i) of

228+ [oi] -> if collapsible oi

229+ then do t' <- stripCollapsed t

230+ return (Bind n (PVar x) (instantiate Erased t'))

231+ else do t' <- stripCollapsed t

232+ return (Bind n (PVar x) t')

233+ _ -> do t' <- stripCollapsed t

234+ return (Bind n (PVar x) t')

235+ stripCollapsed (Bind n (PVar x) t)

236+ = do t' <- stripCollapsed t

237+ return (Bind n (PVar x) t')

238+ stripCollapsed t = return t

239+

128-- Need to saturate arguments first to ensure that erasure happens uniformly

240-- Need to saturate arguments first to ensure that erasure happens uniformly

129

241

130applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term

242applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term

@@ -148,3 +260,4 @@ applyDataOptRT oi n tag arity args

148

260

149 keep (forced, _) = not forced

261 keep (forced, _) = not forced

150

262

263+

src/Idris/ElabDecls.hs+38−6

@@ -233,23 +233,55 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

233elabClauses info fc opts n_in cs = let n = liftname info n_in in

234 do ctxt <- getContext

235 -- Check n actually exists

236− case lookupTy Nothing n ctxt of

236+ fty <- case lookupTy Nothing n ctxt of

237 [] -> -- TODO: turn into a CAF if there's no arguments

238 -- question: CAFs in where blocks?

239 tclift $ tfail $ (At fc (NoTypeDecl n))

240− _ -> return ()

240+ [ty] -> return ty

241 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

242−

242+ -- if the return type of 'ty' is collapsible, the optimised version should

243+ -- just do nothing

244+ ist <- get

245+ let (ap, _) = unApply (getRetTy fty)

246+ logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

247+ -- FIXME: Really ought to only do this for total functions!

248+ let doNothing = case ap of

249+ P _ tn _ -> case lookupCtxt Nothing tn

250+ (idris_optimisation ist) of

251+ [oi] -> collapsible oi

252+ _ -> False

253+ _ -> False

243 solveDeferred n

254 solveDeferred n

255+ ist <- get

256+ when doNothing $

257+ case lookupCtxt Nothing n (idris_optimisation ist) of

258+ [oi] -> do let opts = addDef n (oi { collapsible = True })

259+ (idris_optimisation ist)

260+ put (ist { idris_optimisation = opts })

261+ _ -> do let opts = addDef n (Optimise True [] [])

262+ (idris_optimisation ist)

263+ put (ist { idris_optimisation = opts })

264+ addIBC (IBCOpt n)

265+ ist <- get

244 let pats = pats_in

266 let pats = pats_in

245-- logLvl 3 (showSep "\n" (map (\ (l,r) ->

267-- logLvl 3 (showSep "\n" (map (\ (l,r) ->

246-- show l ++ " = " ++

268-- show l ++ " = " ++

247-- show r) pats))

269-- show r) pats))

248− ist <- get

249 let tcase = opt_typecase (idris_options ist)

270 let tcase = opt_typecase (idris_options ist)

250 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats

271 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats

272+

273+ numArgs <- tclift $ sameLength pdef

274+

275+ optpats <- if doNothing

276+ then return $ [Right (mkApp (P Bound n Erased)

277+ (take numArgs (repeat Erased)), Erased)]

278+ else stripCollapsed pats

279+

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

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

282+

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

251 tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

284 tree@(CaseDef scargs sc _) <- tclift $ simpleCase tcase False CompileTime fc pdef

252− tclift $ sameLength pdef

253 cov <- coverage

285 cov <- coverage

254 pmissing <-

286 pmissing <-

255 if cov

287 if cov

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

263 return missing'

295 return missing'

264 else return []

296 else return []

265 let pcover = null pmissing

297 let pcover = null pmissing

266− pdef' <- applyOpts pdef

298+ pdef' <- applyOpts optpdef

267 ist <- get

299 ist <- get

268-- let wf = wellFounded ist n sc

300-- let wf = wellFounded ist n sc

269 let tot = if pcover || AssertTotal `elem` opts

301 let tot = if pcover || AssertTotal `elem` opts

src/Idris/UnusedArgs.hs+5−3

@@ -37,18 +37,20 @@ used :: [(Name, Int)] -> Name -> Int -> Idris Bool

37used path g j

38 | (g, j) `elem` path = return False -- cycle, never used on the way

39 | otherwise

40+ = do logLvl 5 $ (show ((g, j) : path))

40− = do i <- get

41+ i <- get

41 case lookupCtxt Nothing g (idris_callgraph i) of

42 case lookupCtxt Nothing g (idris_callgraph i) of

42 [CGInfo args calls usedns unused] ->

43 [CGInfo args calls usedns unused] ->

43 if (j >= length args)

44 if (j >= length args)

44 then -- overapplied, assume used

45 then -- overapplied, assume used

45 return True

46 return True

47+ else do let directuse = args!!j `elem` usedns

46− else do let garg = getFargpos calls (args!!j, j)

48+ let garg = getFargpos calls (args!!j, j)

47 logLvl 5 $ show (g, j, garg)

49 logLvl 5 $ show (g, j, garg)

48 recused <- mapM (\ (argn, j, (g', j')) ->

50 recused <- mapM (\ (argn, j, (g', j')) ->

49 used ((g,j):path) g' j') garg

51 used ((g,j):path) g' j') garg

50 -- used on any route from here, or not used recursively

52 -- used on any route from here, or not used recursively

51− return (null recused || or recused)

53+ return (directuse || null recused || or recused)

52 _ -> return True -- no definition, assume used

54 _ -> return True -- no definition, assume used

54getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

56getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

test/test001/test001.idr+5−3

@@ -7,7 +7,7 @@ interpTy TyInt = Int

7interpTy TyBool = Bool

8interpTy (TyFun s t) = interpTy s -> interpTy t

10−using (G : Vect Ty n) {

10+using (G : Vect Ty n)

12 data Env : Vect Ty n -> Set where

13 Nil : Env Nil

@@ -20,6 +20,7 @@ using (G : Vect Ty n) {

20 lookup : HasType i G t -> Env G -> interpTy t

21 lookup stop (x :: xs) = x

22 lookup (pop k) (x :: xs) = lookup k xs

23+ lookup stop [] impossible

24 data Expr : Vect Ty n -> Ty -> Set where

25 data Expr : Vect Ty n -> Ty -> Set where

25 Var : HasType i G t -> Expr G t

26 Var : HasType i G t -> Expr G t

@@ -78,14 +79,15 @@ using (G : Vect Ty n) {

78 (\y => Bind (App eDouble (Val x))

79 (\y => Bind (App eDouble (Val x))

79 (\z => App (App eAdd (Val y)) (Val z))))))

80 (\z => App (App eAdd (Val y)) (Val z))))))

81−}

82−

83test : Int

82test : Int

84test = interp [] eProg 2 2

83test = interp [] eProg 2 2

86testFac : Int

85testFac : Int

87testFac = interp [] eFac 4

86testFac = interp [] eFac 4

88+testEnv : Int -> Env [TyInt,TyInt]

89+testEnv x = [x,x]

90+

89main : IO ()

91main : IO ()

90main = do { print testFac

92main = do { print testFac

91 print test }

93 print test }

test/test015/test015.idr+2−2

@@ -4,8 +4,8 @@ import parity

4import system

6data Bit : Nat -> Set where

7− b0 : Bit 0

7+ b0 : Bit O

8− b1 : Bit 1

8+ b1 : Bit (S O)

10instance Show (Bit n) where

11 show = show' where