4e1d50e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use method info to erase stuff in Compiler.hs.

4e1d50eMatus Tejiscak13 years ago

src/IRTS/Compiler.hs+8−1

compare with master

unifiedsplit

@@ -266,6 +266,8 @@ irTerm vs env tm@(App f a) = case unApply tm of

266 -- otherwise, just apply the name

267 _ -> applyName n ist args

268

269+ (V i, args) -> irTerm vs env (P Bound (env !! i) Erased)

270+

269 (f, args)

271 (f, args)

270 -> LApp False

272 -> LApp False

271 <$> irTerm vs env f

273 <$> irTerm vs env f

@@ -288,7 +290,12 @@ irTerm vs env tm@(App f a) = case unApply tm of

288 [] -> 0 -- no definition, probably local name => can't erase anything

290 [] -> 0 -- no definition, probably local name => can't erase anything

289 def -> error $ "unknown arity: " ++ show (n, def)

291 def -> error $ "unknown arity: " ++ show (n, def)

290

292

293+ -- name for purposes of usage info lookup

294+ uName

295+ | Just n' <- viMethod =<< M.lookup n vs = n'

296+ | otherwise = n

297+

291− used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)

298+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

292 fst4 (x,_,_,_) = x

299 fst4 (x,_,_,_) = x

293

300

294irTerm vs env (P _ n _) = return $ LV (Glob n)

301irTerm vs env (P _ n _) = return $ LV (Glob n)

src/Idris/Erasure.hs+1

@@ -480,5 +480,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

480 unionMap :: (a -> Deps) -> [a] -> Deps

481 unionMap f = M.unionsWith (M.unionWith S.union) . map f

482

483+-- Make a field name out of a data constructor name and field number.

483mkFieldName :: Name -> Int -> Name

484mkFieldName :: Name -> Int -> Name

484mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

485mkFieldName ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")