e866fa6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't erase from unknown names.

e866fa6Matus Tejiscak13 years ago

src/IRTS/Compiler.hs+9−11

compare with master

unifiedsplit

@@ -60,7 +60,7 @@ compile codegen f tm

60 let (residDeps, (reachableNames', minUse)) = minimalUsage depMap

61 reachableNames = sUN "prim__subBigInt" : sUN "prim__addBigInt" : S.toList reachableNames'

62 iLOG $ "RESIDUAL DEPS:\n" ++ unlines (map printItem . M.toList $ residDeps)

63− iLOG $ "REACHABLE NAMES: " ++ show reachableNames

63+ iLOG $ "REACHABLE NAMES:\n" ++ unlines (map show reachableNames)

65 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList

66 iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse

@@ -276,16 +276,13 @@ instance ToIR (TT Name) where

276 Just tm -> return tm

277 _ -> do

278 let collapse

279− = case lookupCtxtExact n

280− (idris_optimisation i) of

279+ = case lookupCtxtExact n (idris_optimisation i) of

281 Just oi -> collapsible oi

280 Just oi -> collapsible oi

282 _ -> False

281 _ -> False

283 let used

282 let used

284− = case lookupCtxtExact n

283+ = case lookupCtxtExact n (idris_callgraph i) of

285− (idris_callgraph i) of

286− Just (CGInfo _ _ _ _ usedpos) ->

284+ Just (CGInfo _ _ _ _ usedpos) -> Just usedpos

287− usedpos

285+ _ -> Nothing

288− _ -> [] -- TODO: is this correct?

289 if collapse

286 if collapse

290 then return LNothing

287 then return LNothing

291 else do

288 else do

@@ -296,9 +293,10 @@ instance ToIR (TT Name) where

296 = do f' <- ir' env f

293 = do f' <- ir' env f

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

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

298 return (LApp False f' args')

295 return (LApp False f' args')

299− where mkUsed u i [] = []

296+ where mkUsed (Just u) i [] = []

300− mkUsed u i (x : xs) | i `elem` u = x : mkUsed u (i + 1) xs

297+ mkUsed (Just u) i (x : xs) | i `elem` u = x : mkUsed (Just u) (i + 1) xs

301− | otherwise = LNothing : mkUsed u (i + 1) xs

298+ | otherwise = LNothing : mkUsed (Just u) (i + 1) xs

299+ mkUsed Nothing _ xs = xs

302-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)

300-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)

303-- = return $ LConst (BI 0)

301-- = return $ LConst (BI 0)

304 ir' env (P _ n _) = return $ LV (Glob n)

302 ir' env (P _ n _) = return $ LV (Glob n)

src/IRTS/Simplified.hs−1

@@ -123,7 +123,6 @@ checkDefs ctxt [] = return []

123checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)

124 = do xs' <- checkDefs ctxt xs

125 return xs'

126−checkDefs ctxt ((n, DFun n' args exp) : xs) | ("CHECK DEF", n, n', args, exp) `traceShow` False = undefined

127checkDefs ctxt ((n, DFun n' args exp) : xs)

126checkDefs ctxt ((n, DFun n' args exp) : xs)

128 = do let sexp = evalState (simplify True exp) (ctxt, 0)

127 = do let sexp = evalState (simplify True exp) (ctxt, 0)

129 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

128 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

src/Idris/Erasure.hs+5

@@ -100,11 +100,16 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

100 , it "mkForeign" [1]

101 , it "prim__toStrBigInt" [0]

102 , it "prim__addBigInt" [0,1]

103+ , it "prim__subBigInt" [0,1]

103 , it "prim__sextInt_BigInt" [0]

104 , it "prim__sextInt_BigInt" [0]

104 , it "prim__zextInt_BigInt" [0]

105 , it "prim__zextInt_BigInt" [0]

105 , it "prim__eqString" [0,1]

106 , it "prim__eqString" [0,1]

106 , it "prim__eqChar" [0,1]

107 , it "prim__eqChar" [0,1]

107 , it "prim__eqBigInt" [0,1]

108 , it "prim__eqBigInt" [0,1]

109+ , it "prim__charToInt" [0]

110+ , it "prim__sltBigInt" [0,1]

111+ , it "prim__sltChar" [0,1]

112+ , it "prim__toStrInt" [0,1]

108 , mn "__MkPair" [0,1]

113 , mn "__MkPair" [0,1]

109 ]

114 ]

110 ]

115 ]