44ee6d3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Handle overapplied functions correctly.

44ee6d3Matus Tejiscak13 years ago

src/IRTS/Compiler.hs+33−24

compare with master

unifiedsplit

@@ -29,6 +29,7 @@ import Idris.Core.CaseTree

30import Control.Applicative

31import Control.Monad.State

32+import Data.Maybe

32import Data.List

33import Data.List

33import Data.IntSet (IntSet)

34import Data.IntSet (IntSet)

34import qualified Data.IntMap as IM

35import qualified Data.IntMap as IM

@@ -267,34 +268,42 @@ instance ToIR (TT Name) where

267 = irCon env t a n args

268 = irCon env t a n args

268 | (P (TCon t a) n _, args) <- unApply tm

269 | (P (TCon t a) n _, args) <- unApply tm

269 = return LNothing

270 = return LNothing

271+

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

272+ | (P _ n _, args) <- unApply tm = do

271− = do i <- getIState

273+ ist <- getIState

274+ case lookup n (idris_scprims ist) of

275+ -- if it's a primitive, compile to the corresponding code

272− args' <- mapM (ir' env) args

276+ Just _ -> fromJust . getPrim ist n <$> mapM (ir' env) args

273− case getPrim i n args' of

277+

274− Just tm -> return tm

275− _ -> do

276− let collapse

277− = case lookupCtxtExact n (idris_optimisation i) of

278− Just oi -> collapsible oi

279− _ -> False

280− let used

281− = case lookupCtxtExact n (idris_callgraph i) of

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

283− _ -> Nothing

278+ Nothing

284− if collapse

279+ -- if it's collapsible, compile to LNothing

285− then return LNothing

280+ | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True

286− else do

281+ -> return LNothing

287− iLOG $ "ERASE:\n " ++ show tm ++ "\n ==>\n " ++ show (LApp False (LV (Glob n)) (mkUsed used 0 args'))

282+

288− return (LApp False (LV (Glob n))

283+ -- otherwise, compile normally

289− (mkUsed used 0 args'))

284+ | otherwise -> applyName n ist args

285+

290 | (f, args) <- unApply tm

286 | (f, args) <- unApply tm

291 = do f' <- ir' env f

287 = do f' <- ir' env f

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

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

293 return (LApp False f' args')

289 return (LApp False f' args')

290+

294− where mkUsed (Just u) i [] = []

291+ where

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

292+ applyName :: Name -> IState -> [Term] -> Idris LExp

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

293+ applyName n ist args =

297− mkUsed Nothing _ xs = xs

294+ LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)

295+ where

296+ erase (i, x)

297+ | i >= arity || i `elem` used = x

298+ | otherwise = Erased

299+

300+ arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of

301+ [CaseOp ci ty tys def tot cdefs] -> length tys

302+ _ -> 0

303+

304+ used = fromMaybe [] (usedpos <$> lookupCtxtExact n (idris_callgraph ist))

305+ fst4 (x,_,_,_) = x

306+

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

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

299-- = return $ LConst (BI 0)

308-- = return $ LConst (BI 0)

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

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

src/Idris/Core/Evaluate.hs+1−1

@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where

16import Debug.Trace

17import Control.Monad.State -- not Strict!

src/Idris/Erasure.hs+16−3

@@ -212,7 +212,7 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

212 -- assumed to be a global reference

213 | otherwise = M.singleton cd (S.singleton (n, Result))

214 where

215− specialMNs = words "{__Unit0}"

215+ specialMNs = words "{__Unit0} {__False0} {__True0}"

216

217 -- dependencies of de bruijn variables are described in `bs'

218 getDepsTerm vs bs cd (V i) = (bs !! i) cd

@@ -279,10 +279,15 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

279 _ -> error $ "cannot analyse application of " ++ show fun ++ " to " ++ show args

280 where

281 ins = M.insertWith S.union cd

282− node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip [0..]

283− getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t

284 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

282 unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

285

283

284+ node :: Name -> [Term] -> Deps

285+ node n = ins (S.singleton (n, Result)) . unionMap (getDepsArgs n) . zip indices

286+ where

287+ indices = map Just [0 .. getArity n - 1] ++ repeat Nothing

288+ getDepsArgs n (Just i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t -- conditional

289+ getDepsArgs n (Nothing, t) = getDepsTerm vs bs cd t -- unconditional

290+

286 -- projections (= methods)

291 -- projections (= methods)

287 getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t -- TODO?

292 getDepsTerm vs bs cd (Proj t i) = getDepsTerm vs bs cd t -- TODO?

288

293

@@ -294,6 +299,14 @@ buildDepMap ci ctx ns = addPostulates $ dfs S.empty M.empty ns

294

299

295 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t

300 getDepsTerm vs bs cd t = error $ "cannot get deps of: " ++ show t

296

301

302+ -- Get the number of arguments that might be considered for erasure.

303+ -- If the symbol is unknown, we assume that it uses all its arguments.

304+ getArity :: Name -> Int

305+ getArity n = case lookupDef n ctx of

306+ [CaseOp ci ty tys def tot cdefs]

307+ -> length tys

308+ _ -> 0

309+

297 -- convert applications of lambdas to lets

310 -- convert applications of lambdas to lets

298 -- Note that this transformation preserves de bruijn numbering

311 -- Note that this transformation preserves de bruijn numbering

299 lamToLet :: [Term] -> Term -> Term

312 lamToLet :: [Term] -> Term -> Term