267f044 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve case compilation by checking most distinct argument first

267f044Edwin Brady14 years ago

rts/idris_rts.c+1−1

compare with master

unifiedsplit

@@ -87,8 +87,8 @@ void* allocate(VM* vm, size_t size, int outerlock) {

87 if ((size & 7)!=0) {

88 size = 8 + ((size >> 3) << 3);

89 }

90− vm->allocations += size + sizeof(size_t);

91 if (vm -> heap_next + size < vm -> heap_end) {

90 if (vm -> heap_next + size < vm -> heap_end) {

91+ vm->allocations += size + sizeof(size_t);

92 void* ptr = (void*)(vm->heap_next + sizeof(size_t));

93 *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

94 vm -> heap_next += size + sizeof(size_t);

src/Core/CaseTree.hs+31−10

@@ -171,15 +171,16 @@ simpleCase tc cover phase fc []

171simpleCase tc cover phase fc cs

172 = let proj = phase == RunTime

173 pats = map (\ (avs, l, r) ->

174− (avs, rev phase (toPats tc l), (l, r))) cs

174+ (avs, toPats tc l, (l, r))) cs

175 chkPats = mapM chkAccessible pats in

176 case chkPats of

177 OK pats ->

178 let numargs = length (fst (head pats))

179 ns = take numargs args

180+ (ns', ps') = order ns pats

180 (tree, st) = runState

181 (tree, st) = runState

181− (match (rev phase ns) pats (defaultCase cover)) ([], numargs)

182+ (match ns' ps' (defaultCase cover)) ([], numargs)

182− t = CaseDef ns (prune proj (depatt ns tree)) (fst st) in

183+ t = CaseDef ns (prune proj (depatt ns' tree)) (fst st) in

183 if proj then return (stripLambdas t) else return t

184 if proj then return (stripLambdas t) else return t

184 Error err -> Error (At fc err)

185 Error err -> Error (At fc err)

185 where args = map (\i -> MN i "e") [0..]

186 where args = map (\i -> MN i "e") [0..]

@@ -196,11 +197,6 @@ simpleCase tc cover phase fc cs

196 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

197 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

197 acc (_ : xs) n = acc xs n

198 acc (_ : xs) n = acc xs n

198

199

199−-- right to left gives more chance of discriminating on interesting arguments

200−-- rather than indices which are likely to be repeated.

201−-- rev CompileTime = id

202−rev _ = reverse

203−

204data Pat = PCon Name Int [Pat]

200data Pat = PCon Name Int [Pat]

205 | PConst Const

201 | PConst Const

206 | PV Name

202 | PV Name

@@ -264,6 +260,32 @@ partition ms@(m : _)

264 Cons cons : partition rest

260 Cons cons : partition rest

265partition xs = error $ "Partition " ++ show xs

261partition xs = error $ "Partition " ++ show xs

266

262

263+-- reorder the patterns so that the one with most distinct names

264+-- comes next. Take rightmost first, otherwise (i.e. pick value rather

265+-- than dependency)

266+

267+order :: [Name] -> [Clause] -> ([Name], [Clause])

268+order [] cs = ([], cs)

269+order ns [] = (ns, [])

270+order ns cs = let patnames = transpose (map (zip ns) (map fst cs))

271+ pats' = transpose (sortBy moreDistinct (reverse patnames)) in

272+ (getNOrder pats', zipWith rebuild pats' cs)

273+ where

274+ getNOrder [] = error $ "Failed order on " ++ show (ns, cs)

275+ getNOrder (c : _) = map fst c

276+

277+ rebuild patnames clause = (map snd patnames, snd clause)

278+

279+ moreDistinct xs ys = compare (numNames [] (map snd ys))

280+ (numNames [] (map snd xs))

281+

282+ numNames xs (PCon n _ _ : ps)

283+ | not (Left n `elem` xs) = numNames (Left n : xs) ps

284+ numNames xs (PConst c : ps)

285+ | not (Right c `elem` xs) = numNames (Right c : xs) ps

286+ numNames xs (_ : ps) = numNames xs ps

287+ numNames xs [] = length xs

288+

267match :: [Name] -> [Clause] -> SC -- error case

289match :: [Name] -> [Clause] -> SC -- error case

268 -> State CS SC

290 -> State CS SC

269match [] (([], ret) : xs) err

291match [] (([], ret) : xs) err

@@ -273,8 +295,7 @@ match [] (([], ret) : xs) err

273 Impossible -> return ImpossibleCase

295 Impossible -> return ImpossibleCase

274 tm -> return $ STerm tm -- run out of arguments

296 tm -> return $ STerm tm -- run out of arguments

275match vs cs err = do let ps = partition cs

297match vs cs err = do let ps = partition cs

276− cs <- mixture vs ps err

298+ mixture vs ps err

277− return cs

278

299

279mixture :: [Name] -> [Partition] -> SC -> State CS SC

300mixture :: [Name] -> [Partition] -> SC -> State CS SC

280mixture vs [] err = return err

301mixture vs [] err = return err

src/IRTS/Lang.hs+2

@@ -125,6 +125,8 @@ lift env (LApp tc f args) = do f' <- lift env f

125lift env (LLazyApp n args) = do args' <- mapM (lift env) args

126 return (LLazyApp n args')

127lift env (LLazyExp (LConst c)) = return (LConst c)

128+-- lift env (LLazyExp (LApp tc (LV (Glob f)) args))

129+-- = lift env (LLazyApp f args)

128lift env (LLazyExp e) = do e' <- lift env e

130lift env (LLazyExp e) = do e' <- lift env e

129 let usedArgs = nub $ usedIn env e'

131 let usedArgs = nub $ usedIn env e'

130 fn <- getNextName

132 fn <- getNextName