0 | module Compiler.Inline

  2 | import Compiler.CaseOpts

  3 | import Compiler.CompileExpr

  4 | import Compiler.Opts.ConstantFold

  5 | import Compiler.Opts.Identity

  6 | import Compiler.Opts.InlineHeuristics

  8 | import Core.Context.Log

  9 | import Core.Hash

 10 | import Core.Options

 12 | import Data.List.Quantifiers

 13 | import Data.Vect

 15 | import Libraries.Data.List.LengthMatch

 16 | import Libraries.Data.NameMap

 17 | import Libraries.Data.WithDefault

 18 | import Libraries.Data.List.SizeOf

 20 | %default covering

 22 | EEnv : Scope -> Scope -> Type

 23 | EEnv free = All (\_ => CExp free)

 25 | extend : EEnv free vars -> (args : List (CExp free)) -> (args' : List Name) ->

 26 |          LengthMatch args args' -> EEnv free (Scope.addInner vars args')

 27 | extend env [] [] NilMatch = env

 28 | extend env (a :: xs) (n :: ns) (ConsMatch w)

 29 |     = a :: extend env xs ns w

 31 | Stack : Scoped

 32 | Stack vars = List (CExp vars)

 34 | unload : Stack vars -> CExp vars -> CExp vars

 35 | unload [] e = e

 36 | unload (a :: args) e = unload args (CApp (getFC e) e [a])

 38 | unloadApp : Nat -> Stack vars -> CExp vars -> CExp vars

 39 | unloadApp n args e = unload (drop n args) (CApp (getFC e) e (take n args))

 41 | getArity : CDef -> Nat

 42 | getArity (MkFun args _) = length args

 43 | getArity (MkCon _ arity _) = arity

 44 | getArity (MkForeign _ args _) = length args

 45 | getArity (MkError _) = 0

 47 | takeFromStack : EEnv free vars -> Stack free -> (args : Scope) ->

 48 |                 Maybe (EEnv free (Scope.addInner vars args), Stack free)

 49 | takeFromStack env (e :: es) (a :: as)

 50 |   = do (env', stk') <- takeFromStack env es as

 51 |        pure (e :: env', stk')

 52 | takeFromStack env stk [] = pure (env, stk)

 53 | takeFromStack env [] args = Nothing

 55 | data LVar : Type where

 57 | genName : {auto l : Ref LVar Int} ->

 58 |           String -> Core Name

 59 | genName n

 60 |     = do i <- get LVar

 61 |          put LVar (i + 1)

 62 |          pure (MN n i)

 64 | refToLocal : Name -> (x : Name) -> CExp vars -> CExp (x :: vars)

 65 | refToLocal x new tm = refsToLocals (Add new x None) tm

 67 | largest : Ord a => a -> List a -> a

 68 | largest x [] = x

 69 | largest x (y :: ys)

 70 |     = if y > x

 71 |          then largest y ys

 72 |          else largest x ys

 75 |   used : {free : _} ->

 76 |          {idx : Nat} -> (0 p : IsVar n idx free) -> CExp free -> Int

 77 |   used {idx} n (CLocal _ {idx=pidx} prf) = if idx == pidx then 1 else 0

 78 |   used n (CLam _ _ sc) = used (Later n) sc

 79 |   used n (CLet _ _ NotInline val sc)

 80 |       = let usedl = used n val + used (Later n) sc in

 81 |             if usedl > 0

 82 |                then 1000 -- Don't do any inlining of the name, because if it's

 83 |                          -- used under a non-inlinable let things might go wrong

 84 |                else usedl

 85 |   used n (CLet _ _ YesInline val sc) = used n val + used (Later n) sc

 86 |   used n (CApp _ x args) = foldr (+) (used n x) (map (used n) args)

 87 |   used n (CCon _ _ _ _ args) = foldr (+) 0 (map (used n) args)

 88 |   used n (COp _ _ args) = foldr (+) 0 (map (used n) args)

 89 |   used n (CExtPrim _ _ args) = foldr (+) 0 (map (used n) args)

 90 |   used n (CForce _ _ x) = used n x

 91 |   used n (CDelay _ _ x) = used n x

 92 |   used n (CConCase fc sc alts def)

 93 |      = used n sc +

 94 |           largest (maybe 0 (used n) def) (map (usedCon n) alts)

 95 |   used n (CConstCase fc sc alts def)

 96 |      = used n sc +

 97 |           largest (maybe 0 (used n) def) (map (usedConst n) alts)

 98 |   used _ tm = 0

100 |   usedCon : {free : _} ->

101 |             {idx : Nat} -> (0 p : IsVar n idx free) -> CConAlt free -> Int

102 |   usedCon n (MkConAlt _ _ _ args sc)

103 |       = let MkVar n' = weakenNs (mkSizeOf args) (MkVar n) in

104 |             used n' sc

106 |   usedConst : {free : _} ->

107 |               {idx : Nat} -> (0 p : IsVar n idx free) -> CConstAlt free -> Int

108 |   usedConst n (MkConstAlt _ sc) = used n sc

111 |   evalLocal : {vars, free : _} ->

112 |               {auto c : Ref Ctxt Defs} ->

113 |               {auto l : Ref LVar Int} ->

114 |               FC -> List Name -> Stack free ->

115 |               EEnv free vars ->

116 |               {idx : Nat} -> (0 p : IsVar x idx (vars ++ free)) ->

117 |               Core (CExp free)

118 |   evalLocal {vars = []} fc rec stk env p

119 |       = pure $ unload stk (CLocal fc p)

120 |   evalLocal {vars = x :: xs} fc rec stk (v :: env) First

121 |       = case stk of

122 |              [] => pure v

123 |              _ => eval rec env stk (weakenNs (mkSizeOf xs) v)

124 |   evalLocal {vars = x :: xs} fc rec stk (_ :: env) (Later p)

125 |       = evalLocal fc rec stk env p

127 |   tryApply : {vars, free : _} ->

128 |              {auto c : Ref Ctxt Defs} ->

129 |              {auto l : Ref LVar Int} ->

130 |              List Name -> Stack free -> EEnv free vars -> CDef ->

131 |              Core (Maybe (CExp free))

132 |   tryApply {free} {vars} rec stk env (MkFun args exp)

133 |       = do let Just (env', stk') = takeFromStack env stk args

134 |                | Nothing => pure Nothing

135 |            res <- eval rec env' stk'

136 |                      (rewrite sym (appendAssociative args vars free) in

137 |                               embed {outer = vars ++ free} exp)

138 |            pure (Just res)

139 |   tryApply rec stk env _ = pure Nothing

141 |   eval : {vars, free : _} ->

142 |          {auto c : Ref Ctxt Defs} ->

143 |          {auto l : Ref LVar Int} ->

144 |          List Name -> -- TODO should be a set

145 |          EEnv free vars -> Stack free -> CExp (vars ++ free) ->

146 |          Core (CExp free)

147 |   eval rec env stk (CLocal fc p) = evalLocal fc rec stk env p

148 |   -- This is hopefully a temporary hack, giving a special case for io_bind.

149 |   -- Currently the elaborator is a bit cautious about inlining case blocks

150 |   -- in case they duplicate work. We should fix that, to decide more accurately

151 |   -- whether they're safe to inline, but until then this gives such a huge

152 |   -- boost by removing unnecessary lambdas that we'll keep the special case.

153 |   eval rec env stk (CRef fc n) = do

154 |         when (n == NS primIONS (UN $ Basic "io_bind")) $

155 |           log "compiler.inline.io_bind" 50 $

156 |             "Attempting to inline io_bind, its stack is: \{show stk}"

157 |         case (n == NS primIONS (UN $ Basic "io_bind"), stk) of

158 |           (True, act :: cont :: world :: stk) =>

159 |                  do xn <- genName "act"

160 |                     sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])

161 |                     pure $ unload stk $

162 |                              CLet fc xn NotInline

163 |                                (CApp fc act [world])

164 |                                (refToLocal xn xn sc)

165 |           (True, [act, cont]) =>

166 |                  do wn <- genName "world"

167 |                     xn <- genName "act"

168 |                     let world : forall vars. CExp vars := CRef fc wn

169 |                     sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world])

170 |                     pure $ CLam fc wn

171 |                          $ refToLocal wn wn

172 |                          $ CLet fc xn NotInline (CApp fc act [world])

173 |                          $ refToLocal xn xn

174 |                          $ sc

175 |           (_,_) =>

176 |              do defs <- get Ctxt

177 |                 Just gdef <- lookupCtxtExact n (gamma defs)

178 |                   | Nothing => pure (unload stk (CRef fc n))

179 |                 let Just def = compexpr gdef

180 |                   | Nothing => pure (unload stk (CRef fc n))

181 |                 let arity = getArity def

182 |                 let gdefFlags = flags gdef

183 |                 if (Inline `elem` gdefFlags)

184 |                     && (not (n `elem` rec))

185 |                     && (not (NoInline `elem` gdefFlags))

186 |                    then do ap <- tryApply (n :: rec) stk env def

187 |                            pure $ fromMaybe (unloadApp arity stk (CRef fc n)) ap

188 |                    else pure $ unloadApp arity stk (CRef fc n)

189 |   eval {vars} {free} rec env [] (CLam fc x sc)

190 |       = do xn <- genName "lamv"

191 |            sc' <- eval rec (CRef fc xn :: env) [] sc

192 |            pure $ CLam fc x (refToLocal xn x sc')

193 |   eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc

194 |   eval {vars} {free} rec env stk (CLet fc x NotInline val sc)

195 |       = do xn <- genName "letv"

196 |            sc' <- eval rec (CRef fc xn :: env) [] sc

197 |            val' <- eval rec env [] val

198 |            pure (unload stk $ CLet fc x NotInline val' (refToLocal xn x sc'))

199 |   eval {vars} {free} rec env stk (CLet fc x YesInline val sc)

200 |       = do let u = used First sc

201 |            if u < 1 -- TODO: Can make this <= as long as we know *all* inlinings

202 |                     -- are guaranteed not to duplicate work. (We don't know

203 |                     -- that yet).

204 |               then do val' <- eval rec env [] val

205 |                       eval rec (val' :: env) stk sc

206 |               else do xn <- genName "letv"

207 |                       sc' <- eval rec (CRef fc xn :: env) stk sc

208 |                       val' <- eval rec env [] val

209 |                       pure (CLet fc x YesInline val' (refToLocal xn x sc'))

210 |   eval rec env stk (CApp fc f@(CRef nfc n) args)

211 |       = do -- If we don't know 'n' leave the arity alone, because it's

212 |            -- a name from another module where the job is already done

213 |            defs <- get Ctxt

214 |            Just gdef <- lookupCtxtExact n (gamma defs)

215 |                 | Nothing => do args' <- traverse (eval rec env []) args

216 |                                 pure (unload stk

217 |                                           (CApp fc (CRef nfc n) args'))

218 |            eval rec env (!(traverse (eval rec env []) args) ++ stk) f

219 |   eval rec env stk (CApp fc f args)

220 |       = eval rec env (!(traverse (eval rec env []) args) ++ stk) f

221 |   eval rec env stk (CCon fc n ci t args)

222 |       = pure $ unload stk $ CCon fc n ci t !(traverse (eval rec env []) args)

223 |   eval rec env stk (COp fc p args)

224 |       = pure $ unload stk $ COp fc p !(traverseVect (eval rec env []) args)

225 |   eval rec env stk (CExtPrim fc p args)

226 |       = pure $ unload stk $ CExtPrim fc p !(traverse (eval rec env []) args)

227 |   eval rec env stk (CForce fc lr e)

228 |       = case !(eval rec env [] e) of

229 |              CDelay _ _ e' => eval rec [] stk e'

230 |              res => pure $ unload stk (CForce fc lr res) -- change this to preserve laziness semantics

231 |   eval rec env stk (CDelay fc lr e)

232 |       = pure $ unload stk (CDelay fc lr !(eval rec env [] e))

233 |   eval rec env stk (CConCase fc sc alts def)

234 |       = do sc' <- eval rec env [] sc

235 |            let env' = update sc env sc'

236 |            Nothing <- pickAlt rec env' stk sc' alts def | Just val => pure val

237 |            def' <- traverseOpt (eval rec env' stk) def

238 |            pure $ caseOfCase $ CConCase fc sc'

239 |                      !(traverse (evalAlt fc rec env' stk) alts)

240 |                      def'

241 |     where

242 |       updateLoc : {idx, vs : _} ->

243 |                   (0 p : IsVar x idx (vs ++ free)) ->

244 |                   EEnv free vs -> CExp free -> EEnv free vs

245 |       updateLoc {vs = []} p env val = env

246 |       updateLoc {vs = (x::xs)} First (e :: env) val = val :: env

247 |       updateLoc {vs = (y::xs)} (Later p) (e :: env) val = e :: updateLoc p env val

249 |       update : {vs : _} ->

250 |                CExp (vs ++ free) -> EEnv free vs -> CExp free -> EEnv free vs

251 |       update (CLocal _ p) env sc = updateLoc p env sc

252 |       update _ env _ = env

254 |   eval rec env stk (CConstCase fc sc alts def)

255 |       = do sc' <- eval rec env [] sc

256 |            Nothing <- pickConstAlt rec env stk sc' alts def | Just val => pure val

257 |            def' <- traverseOpt (eval rec env stk) def

258 |            pure $ caseOfCase $ CConstCase fc sc'

259 |                          !(traverse (evalConstAlt rec env stk) alts)

260 |                          def'

261 |   eval rec env stk (CPrimVal fc c) = pure $ unload stk $ CPrimVal fc c

262 |   eval rec env stk (CErased fc) = pure $ unload stk $ CErased fc

263 |   eval rec env stk (CCrash fc str) = pure $ unload stk $ CCrash fc str

265 |   extendLoc : {auto l : Ref LVar Int} ->

266 |               FC -> EEnv free vars -> (args' : List Name) ->

267 |               Core (Bounds args', EEnv free (args' ++ vars))

268 |   extendLoc fc env [] = pure (None, env)

269 |   extendLoc fc env (n :: ns)

270 |       = do xn <- genName "cv"

271 |            (bs', env') <- extendLoc fc env ns

272 |            pure (Add n xn bs', CRef fc xn :: env')

274 |   evalAlt : {vars, free : _} ->

275 |             {auto c : Ref Ctxt Defs} ->

276 |             {auto l : Ref LVar Int} ->

277 |             FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (vars ++ free) ->

278 |             Core (CConAlt free)

279 |   evalAlt {free} {vars} fc rec env stk (MkConAlt n ci t args sc)

280 |       = do (bs, env') <- extendLoc fc env args

281 |            scEval <- eval rec env' stk

282 |                           (rewrite sym (appendAssociative args vars free) in sc)

283 |            pure $ MkConAlt n ci t args (refsToLocals bs scEval)

285 |   evalConstAlt : {vars, free : _} ->

286 |                  {auto c : Ref Ctxt Defs} ->

287 |                  {auto l : Ref LVar Int} ->

288 |                  List Name -> EEnv free vars -> Stack free -> CConstAlt (vars ++ free) ->

289 |                  Core (CConstAlt free)

290 |   evalConstAlt rec env stk (MkConstAlt c sc)

291 |       = MkConstAlt c <$> eval rec env stk sc

293 |   pickAlt : {vars, free : _} ->

294 |             {auto c : Ref Ctxt Defs} ->

295 |             {auto l : Ref LVar Int} ->

296 |             List Name -> EEnv free vars -> Stack free ->

297 |             CExp free -> List (CConAlt (vars ++ free)) ->

298 |             Maybe (CExp (vars ++ free)) ->

299 |             Core (Maybe (CExp free))

300 |   pickAlt rec env stk (CCon fc n ci t args) [] def

301 |       = traverseOpt (eval rec env stk) def

302 |   pickAlt {vars} {free} rec env stk con@(CCon fc n ci t args) (MkConAlt n' _ t' args' sc :: alts) def

303 |       = if matches n t n' t'

304 |            then case checkLengthMatch args args' of

305 |                      Nothing => pure Nothing

306 |                      Just m =>

307 |                          do let env' : EEnv free (args' ++ vars)

308 |                                    = extend env args args' m

309 |                             pure $ Just !(eval rec env' stk

310 |                                     (rewrite sym (appendAssociative args' vars free) in

311 |                                              sc))

312 |            else pickAlt rec env stk con alts def

313 |     where

314 |       matches : Name -> Maybe Int -> Name -> Maybe Int -> Bool

315 |       matches _ (Just t) _ (Just t') = t == t'

316 |       matches n Nothing n' Nothing = n == n'

317 |       matches _ _ _ _ = False

318 |   pickAlt rec env stk _ _ _ = pure Nothing

320 |   pickConstAlt : {vars, free : _} ->

321 |                  {auto c : Ref Ctxt Defs} ->

322 |                  {auto l : Ref LVar Int} ->

323 |                  List Name -> EEnv free vars -> Stack free ->

324 |                  CExp free -> List (CConstAlt (vars ++ free)) ->

325 |                  Maybe (CExp (vars ++ free)) ->

326 |                  Core (Maybe (CExp free))

327 |   pickConstAlt rec env stk (CPrimVal fc c) [] def

328 |       = traverseOpt (eval rec env stk) def

329 |   pickConstAlt {vars} {free} rec env stk (CPrimVal fc c) (MkConstAlt c' sc :: alts) def

330 |       = if c == c'

331 |            then Just <$> eval rec env stk sc

332 |            else pickConstAlt rec env stk (CPrimVal fc c) alts def

333 |   pickConstAlt rec env stk _ _ _ = pure Nothing

339 | fixArityTm : {auto c : Ref Ctxt Defs} ->

340 |              CExp vars -> List (CExp vars) -> Core (CExp vars)

341 | fixArityTm (CRef fc n) args

342 |     = do defs <- get Ctxt

343 |          Just gdef <- lookupCtxtExact n (gamma defs)

344 |               | Nothing => pure (unload args (CRef fc n))

345 |          let arity = case compexpr gdef of

346 |                           Just def => getArity def

347 |                           _ => 0

348 |          pure $ expandToArity arity (CApp fc (CRef fc n) []) args

349 | fixArityTm (CLam fc x sc) args

350 |     = pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args

351 | fixArityTm (CLet fc x inl val sc) args

352 |     = pure $ expandToArity Z

353 |                  (CLet fc x inl !(fixArityTm val []) !(fixArityTm sc [])) args

354 | fixArityTm outf@(CApp fc f@(CRef _ n) fargs) args

355 |     = do defs <- get Ctxt

356 |          -- If we don't know 'n' leave the arity alone, because it's

357 |          -- a name from another module where the job is already done

358 |          Just gdef <- lookupCtxtExact n (gamma defs)

359 |               | Nothing => pure (unload args outf)

360 |          fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)

361 | fixArityTm (CApp fc f fargs) args

362 |     = fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)

363 | fixArityTm (CCon fc n ci t args) []

364 |     = pure $ CCon fc n ci t !(traverse (\tm => fixArityTm tm []) args)

365 | fixArityTm (COp fc op args) []

366 |     = pure $ COp fc op !(traverseArgs args)

367 |   where

368 |     traverseArgs : Vect n (CExp vs) -> Core (Vect n (CExp vs))

369 |     traverseArgs [] = pure []

370 |     traverseArgs (a :: as) = pure $ !(fixArityTm a []) :: !(traverseArgs as)

371 | fixArityTm (CExtPrim fc p args) []

372 |     = pure $ CExtPrim fc p !(traverse (\tm => fixArityTm tm []) args)

373 | fixArityTm (CForce fc lr tm) args

374 |     = pure $ expandToArity Z (CForce fc lr !(fixArityTm tm [])) args

375 | fixArityTm (CDelay fc lr tm) args

376 |     = pure $ expandToArity Z (CDelay fc lr !(fixArityTm tm [])) args

377 | fixArityTm (CConCase fc sc alts def) args

378 |     = pure $ expandToArity Z

379 |               (CConCase fc !(fixArityTm sc [])

380 |                            !(traverse fixArityAlt alts)

381 |                            !(traverseOpt (\tm => fixArityTm tm []) def)) args

382 |   where

383 |     fixArityAlt : CConAlt vars -> Core (CConAlt vars)

384 |     fixArityAlt (MkConAlt n ci t a sc)

385 |         = pure $ MkConAlt n ci t a !(fixArityTm sc [])

386 | fixArityTm (CConstCase fc sc alts def) args

387 |     = pure $ expandToArity Z

388 |               (CConstCase fc !(fixArityTm sc [])

389 |                              !(traverse fixArityConstAlt alts)

390 |                              !(traverseOpt (\tm => fixArityTm tm []) def)) args

391 |   where

392 |     fixArityConstAlt : CConstAlt vars -> Core (CConstAlt vars)

393 |     fixArityConstAlt (MkConstAlt c sc)

394 |         = pure $ MkConstAlt c !(fixArityTm sc [])

395 | fixArityTm t [] = pure t

396 | fixArityTm t args = pure $ expandToArity Z t args

399 | fixArityExp : {auto c : Ref Ctxt Defs} ->

400 |               CExp vars -> Core (CExp vars)

401 | fixArityExp tm = fixArityTm tm []

403 | fixArity : {auto c : Ref Ctxt Defs} ->

404 |            CDef -> Core CDef

405 | fixArity (MkFun args exp) = pure $ MkFun args !(fixArityTm exp [])

406 | fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])

407 | fixArity d = pure d

410 | getLams : {done : _} -> SizeOf done ->

411 |           Int -> SubstCEnv done args -> CExp (done ++ args) ->

412 |           (args' ** (SizeOf args', SubstCEnv args' args, CExp (args' ++ args)))

413 | getLams {done} d i env (CLam fc x sc)

414 |     = getLams {done = x :: done} (suc d) (i + 1) (CRef fc (MN "ext" i) :: env) sc

415 | getLams {done} d i env sc = (done ** (d, env, sc))

417 | mkBounds : (xs : _) -> Bounds xs

418 | mkBounds [] = None

419 | mkBounds (x :: xs) = Add x x (mkBounds xs)

422 | getNewArgs : {done : _} ->

423 |              SubstCEnv done args -> Scope

424 | getNewArgs [] = []

425 | getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs

426 | getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub

432 | mergeLambdas : (args : Scope) -> CExp args -> (args' ** CExp args')

433 | mergeLambdas args (CLam fc x sc)

434 |     = let (args' ** (s, env, exp')) = getLams zero 0 Subst.empty (CLam fc x sc)

435 |           expNs = substs s env exp'

436 |           newArgs = reverse $ getNewArgs env

437 |           expLocs = mkLocals (mkSizeOf args) {vars = []} (mkBounds newArgs)

438 |                              (rewrite appendNilRightNeutral args in expNs) in

439 |           (_ ** expLocs)

440 | mergeLambdas args exp = (args ** exp)

445 | doEval : {args : _} ->

446 |          {auto c : Ref Ctxt Defs} ->

447 |          (n : Name) -> (exp : CExp args) -> Core (CExp args)

448 | doEval n exp

449 |     = do l <- newRef LVar (the Int 0)

450 |          log "compiler.inline.eval" 10 (show n ++ ": " ++ show exp)

451 |          exp' <- eval [] [] [] exp

452 |          log "compiler.inline.eval" 10 ("Inlined: " ++ show exp')

453 |          pure exp'

455 | inline : {auto c : Ref Ctxt Defs} ->

456 |          Name -> CDef -> Core CDef

457 | inline n (MkFun args def)

458 |     = pure $ MkFun args !(doEval n def)

459 | inline n d = pure d

462 | mergeLam : {auto c : Ref Ctxt Defs} ->

463 |            CDef -> Core CDef

464 | mergeLam (MkFun args def)

465 |     = do let (args' ** exp') = mergeLambdas args def

466 |          pure $ MkFun args' exp'

467 | mergeLam d = pure d

470 |   addRefs : NameMap Bool -> CExp vars -> NameMap Bool

471 |   addRefs ds (CRef _ n) = insert n False ds

472 |   addRefs ds (CLam _ _ sc) = addRefs ds sc

473 |   addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc

474 |   addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args

475 |   addRefs ds (CCon _ n _ _ args) = addRefsArgs (insert n False ds) args

476 |   addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)

477 |   addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args

478 |   addRefs ds (CForce _ _ e) = addRefs ds e

479 |   addRefs ds (CDelay _ _ e) = addRefs ds e

480 |   addRefs ds (CConCase _ sc alts def)

481 |       = let ds' = maybe ds (addRefs ds) def in

482 |             addRefsConAlts (addRefs ds' sc) alts

483 |   addRefs ds (CConstCase _ sc alts def)

484 |       = let ds' = maybe ds (addRefs ds) def in

485 |             addRefsConstAlts (addRefs ds' sc) alts

486 |   addRefs ds tm = ds

488 |   addRefsArgs : NameMap Bool -> List (CExp vars) -> NameMap Bool

489 |   addRefsArgs ds [] = ds

490 |   addRefsArgs ds (a :: as) = addRefsArgs (addRefs ds a) as

492 |   addRefsConAlts : NameMap Bool -> List (CConAlt vars) -> NameMap Bool

493 |   addRefsConAlts ds [] = ds

494 |   addRefsConAlts ds (MkConAlt n _ _ _ sc :: rest)

495 |       = addRefsConAlts (addRefs (insert n False ds) sc) rest

497 |   addRefsConstAlts : NameMap Bool -> List (CConstAlt vars) -> NameMap Bool

498 |   addRefsConstAlts ds [] = ds

499 |   addRefsConstAlts ds (MkConstAlt _ sc :: rest)

500 |       = addRefsConstAlts (addRefs ds sc) rest

502 | getRefs : CDef -> NameMap Bool

503 | getRefs (MkFun args exp) = addRefs empty exp

504 | getRefs _ = empty

507 | inlineDef : {auto c : Ref Ctxt Defs} ->

508 |             Name -> Core ()

509 | inlineDef n

510 |     = do defs <- get Ctxt

511 |          Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()

512 |          let Just cexpr = compexpr def              | Nothing => pure ()

513 |          setCompiled n !(inline n cexpr)

517 | updateCallGraph : {auto c : Ref Ctxt Defs} ->

518 |                   Name -> Core ()

519 | updateCallGraph n

520 |     = do defs <- get Ctxt

521 |          Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()

522 |          let Just cexpr =  compexpr def             | Nothing => pure ()

523 |          let refs = getRefs cexpr

524 |          ignore $ addDef n ({ refersToRuntimeM := Just refs } def)

527 | fixArityDef : {auto c : Ref Ctxt Defs} ->

528 |               Name -> Core ()

529 | fixArityDef n

530 |     = do defs <- get Ctxt

531 |          Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()

532 |          let Just cexpr =  compexpr def             | Nothing => pure ()

533 |          setCompiled n !(fixArity cexpr)

536 | mergeLamDef : {auto c : Ref Ctxt Defs} ->

537 |               Name -> Core ()

538 | mergeLamDef n

539 |     = do defs <- get Ctxt

540 |          Just def <- lookupCtxtExact n (gamma defs)

541 |               | Nothing => pure ()

542 |          let PMDef pi _ _ _ _ = definition def

543 |               | _ => pure ()

544 |          if not (isNil (incrementalCGs !getSession)) &&

545 |                 externalDecl pi -- better keep it at arity 0

546 |             then pure ()

547 |             else do let Just cexpr =  compexpr def

548 |                              | Nothing => pure ()

549 |                     setCompiled n !(mergeLam cexpr)

552 | addArityHash : {auto c : Ref Ctxt Defs} ->

553 |                Name -> Core ()

554 | addArityHash n

555 |     = do defs <- get Ctxt

556 |          Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()

557 |          let Just cexpr =  compexpr def             | Nothing => pure ()

558 |          let MkFun args _ = cexpr                   | _ => pure ()

559 |          case collapseDefault $ visibility def of

560 |               Private => pure ()

561 |               _ => addHash (n, length args)

564 | compileAndInlineAll : {auto c : Ref Ctxt Defs} ->

565 |                       Core ()

567 |     = do defs <- get Ctxt

568 |          let ns = keys (toIR defs)

569 |          cns <- filterM nonErased ns

571 |          traverse_ compileDef cns

572 |          traverse_ rewriteIdentityFlag cns

573 |          transform 3 cns -- number of rounds to run transformations.

574 |                          -- This seems to be the point where not much useful

575 |                          -- happens any more.

576 |          traverse_ updateCallGraph cns

577 |          -- in incremental mode, add the arity of the definitions to the hash,

578 |          -- because if these change we need to recompile dependencies

579 |          -- accordingly

580 |          unless (isNil (incrementalCGs !getSession)) $

581 |            traverse_ addArityHash cns

582 |   where

583 |     transform : Nat -> List Name -> Core ()

584 |     transform Z cns = pure ()

585 |     transform (S k) cns

586 |         = do traverse_ inlineDef cns

587 |              traverse_ mergeLamDef cns

588 |              traverse_ caseLamDef cns

589 |              traverse_ fixArityDef cns

590 |              traverse_ inlineHeuristics cns

591 |              traverse_ constantFold cns

592 |              traverse_ setIdentity cns

593 |              transform k cns

595 |     nonErased : Name -> Core Bool

596 |     nonErased n

597 |         = do defs <- get Ctxt

598 |              Just gdef <- lookupCtxtExact n (gamma defs)

599 |                   | Nothing => pure False

600 |              pure (multiplicity gdef /= erased)