37b3f6c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add instance ctor application analysis.

37b3f6cMatus Tejiscak13 years ago

src/IRTS/Compiler.hs+2−2

compare with master

unifiedsplit

@@ -407,8 +407,8 @@ instance ToIR SC where

407 -- and we need to do that everywhere.

408 --

409 -- 2. Unused-case elimination:

410− -- case {e0} of

410+ -- case {e0} of ==> P

411− -- C(x,y) -> P[... x,y not used ...] ==> P

411+ -- C(x,y) -> P[... x,y not used ...]

412 --

413 -- This is important for runtime because sometimes we case on irrelevant data:

414 --

src/Idris/Erasure.hs+33−7

@@ -347,9 +347,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

347 -- applications may add items to Cond

348 getDepsTerm vs bs cd app@(App _ _)

349 | (fun, args) <- unApply app = case fun of

350+ -- instance constructors -> create metamethod deps

351+ P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _

352+ -> conditionalDeps ctorName args -- regular data ctor stuff

353+ `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

354+

350− -- constructors

355+ -- ordinary constructors

351 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

356 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

352− P (DCon _ _) n _ -> node n args -- depends on whether (n,#) is used

357+ P (DCon _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

353

358

354 -- mkForeign* calls must be special-cased because they are variadic

359 -- mkForeign* calls must be special-cased because they are variadic

355 -- All arguments must be marked as used, except for the first one,

360 -- All arguments must be marked as used, except for the first one,

@@ -365,7 +370,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

365 -- local name that refers to a method

370 -- local name that refers to a method

366 | Just var <- M.lookup n vs

371 | Just var <- M.lookup n vs

367 , Just meth <- viMethod var

372 , Just meth <- viMethod var

368− -> node meth args -- use the method instead

373+ -> viDeps var `ins` conditionalDeps meth args -- use the method instead

369

374

370 -- local name

375 -- local name

371 | Just var <- M.lookup n vs

376 | Just var <- M.lookup n vs

@@ -375,7 +380,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

375 -- global name

380 -- global name

376 | otherwise

381 | otherwise

377 -- depends on whether the referred thing uses its argument

382 -- depends on whether the referred thing uses its argument

378− -> node n args

383+ -> conditionalDeps n args

379

384

380 -- TODO: could we somehow infer how bound variables use their arguments?

385 -- TODO: could we somehow infer how bound variables use their arguments?

381 V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)

386 V i -> M.unionWith (M.unionWith S.union) ((bs !! i) cd) (unconditionalDeps args)

@@ -395,15 +400,31 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

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

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

396 where

401 where

397 ins = M.insertWith (M.unionWith S.union) cd

402 ins = M.insertWith (M.unionWith S.union) cd

398− unconditionalDeps args = unionMap (getDepsTerm vs bs cd) args

399

403

404+ unconditionalDeps :: [Term] -> Deps

405+ unconditionalDeps = unionMap (getDepsTerm vs bs cd)

406+

400− node :: Name -> [Term] -> Deps

407+ conditionalDeps :: Name -> [Term] -> Deps

408+ conditionalDeps n

401− node n = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices

409+ = ins (M.singleton (n, Result) S.empty) . unionMap (getDepsArgs n) . zip indices

402 where

410 where

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

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

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

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

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

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

406

414

415+ methodDeps :: Name -> (Int, Term) -> Deps

416+ methodDeps ctorName (methNo, t) = getDepsTerm vars bruijns cond t

417+ where

418+ vars = M.fromList [(v, VI

419+ { viDeps = M.singleton (metameth, Arg i) S.empty

420+ , viFunArg = Just i

421+ , viMethod = Nothing

422+ }) | (v, i) <- zip args [0..]]

423+ bruijns = reverse [\cd -> M.singleton cd (M.singleton (metameth, Arg i) S.empty) | i <- [0..length args-1]]

424+ cond = S.singleton (metameth, Result)

425+ metameth = mkField ctorName methNo

426+ (args, body) = unfoldLams t

427+

407 -- projections

428 -- projections

408 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n

429 getDepsTerm vs bs cd (Proj t (-1)) = getDepsTerm vs bs cd t -- naturals, (S n) -> n

409 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t

430 getDepsTerm vs bs cd (Proj t i) = error $ "cannot[1] analyse projection !" ++ show i ++ " of " ++ show t

@@ -444,6 +465,11 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

444 lamToLet (x:xs) t = App (lamToLet xs t) x

465 lamToLet (x:xs) t = App (lamToLet xs t) x

445 lamToLet [] t = t

466 lamToLet [] t = t

446

467

468+ -- split "\x_i -> T(x_i)" into [x_i] and T

469+ unfoldLams :: Term -> ([Name], Term)

470+ unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')

471+ unfoldLams t = ([], t)

472+

447 mkField :: Name -> Int -> Name

473 mkField :: Name -> Int -> Name

448 mkField ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

474 mkField ctorName fieldNo = SN (WhereN fieldNo ctorName $ sMN fieldNo "field")

449

475