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

git.iko.soy/Idris-dev

Handle overapplied functions correctly.

commit44ee6d34dd362cf7230d1447cd4341414f125dff authorMatus Tejiscak <ziman@functor.sk> dateMon 10 Feb 2014, 15:46 (13 years ago) parentd67bc67

3 files changed+50−28

compare with master

unifiedsplit

src/IRTS/Compiler.hs+33−24 src/Idris/Core/Evaluate.hs+1−1 src/Idris/Erasure.hs+16−3

src/IRTS/Compiler.hs+33−24

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

2929

3030import Control.Applicative

3131import Control.Monad.State

32+import Data.Maybe

3233import Data.List

3334import Data.IntSet (IntSet)

3435import qualified Data.IntMap as IM

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

267268 = irCon env t a n args

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

269270 = return LNothing

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

271− = do i <- getIState

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

273− case getPrim i n args' of

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

284− if collapse

285− then return LNothing

286− else do

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

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

289− (mkUsed used 0 args'))

271+

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

273+ ist <- getIState

274+ case lookup n (idris_scprims ist) of

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

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

277+

278+ Nothing

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

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

281+ -> return LNothing

282+

283+ -- otherwise, compile normally

284+ | otherwise -> applyName n ist args

285+

290286 | (f, args) <- unApply tm

291287 = do f' <- ir' env f

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

293289 return (LApp False f' args')

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

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

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

297− mkUsed Nothing _ xs = xs

290+

291+ where

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

293+ applyName n ist args =

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+

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

299308-- = return $ LConst (BI 0)

300309 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,

1111 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,

1212 mapDefCtxt,

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

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

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

1515

1616import Debug.Trace

1717import 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

212212 -- assumed to be a global reference

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

214214 where

215− specialMNs = words "{__Unit0}"

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

216216

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

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

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

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

280280 where

281281 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

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

285283

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+

286291 -- projections (= methods)

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

288293

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

294299

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

296301

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+

297310 -- convert applications of lambdas to lets

298311 -- Note that this transformation preserves de bruijn numbering

299312 lamToLet :: [Term] -> Term -> Term