0 | module Core.LinearCheck

  2 | import Core.Case.CaseTree

  3 | import Core.Context.Log

  4 | import Core.Env

  5 | import Core.Normalise

  6 | import Core.Options

  7 | import Core.UnifyState

  8 | import Core.Value

 10 | import Libraries.Data.List.SizeOf

 11 | import Libraries.Data.SnocList.SizeOf

 13 | %default covering

 17 | Usage : Scoped

 18 | Usage vars = List (Var vars)

 20 | doneScope : Usage (n :: vars) -> Usage vars

 21 | doneScope = mapMaybe isLater

 23 | count : Nat -> Usage ns -> Nat

 24 | count p [] = 0

 25 | count p (v :: xs)

 26 |     = if p == varIdx v then 1 + count p xs else count p xs

 29 |   updateHoleUsageArgs : {0 vars : _} ->

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

 31 |                         {auto u : Ref UST UState} ->

 32 |                         (useInHole : Bool) ->

 33 |                         Var vars -> List (Var vars) ->

 34 |                         List (Term vars) -> Core Bool

 35 |   updateHoleUsageArgs useInHole var zs [] = pure False

 36 |   updateHoleUsageArgs useInHole var zs (a :: as)

 37 |       = do h <- updateHoleUsage useInHole var zs a

 38 |            h' <- updateHoleUsageArgs useInHole var zs as

 39 |            pure (h || h')

 41 |   -- The assumption here is that hole types are abstracted over the entire

 42 |   -- environment, so that they have the appropriate number of function

 43 |   -- arguments and there are no lets

 44 |   updateHoleType : {0 vars : _} ->

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

 46 |                    {auto u : Ref UST UState} ->

 47 |                    (useInHole : Bool) ->

 48 |                    Var vars -> List (Var vars) ->

 49 |                    Term vs -> List (Term vars) ->

 50 |                    Core (Term vs)

 51 |   updateHoleType useInHole var zs (Bind bfc nm (Pi fc' c e ty) sc) (Local _ r v _ :: as)

 52 |       -- if the argument to the hole type is the variable of interest,

 53 |       -- and the variable should be used in the hole, set it to Rig1,

 54 |       -- otherwise set it to Rig0

 55 |       = if varIdx var == v

 56 |            then do scty <- updateHoleType False var zs sc as

 57 |                    let c' = if useInHole then c else erased

 58 |                    pure (Bind bfc nm (Pi fc' c' e ty) scty)

 59 |            else if elem v (map varIdx zs)

 60 |                 then do scty <- updateHoleType useInHole var zs sc as

 61 |                         pure (Bind bfc nm (Pi fc' erased e ty) scty)

 62 |                 else do scty <- updateHoleType useInHole var zs sc as

 63 |                         pure (Bind bfc nm (Pi fc' c e ty) scty)

 64 |   updateHoleType useInHole var zs (Bind bfc nm (Pi fc' c e ty) sc) (a :: as)

 65 |       = do ignore $ updateHoleUsage False var zs a

 66 |            scty <- updateHoleType useInHole var zs sc as

 67 |            pure (Bind bfc nm (Pi fc' c e ty) scty)

 68 |   updateHoleType useInHole var zs ty as

 69 |       = do ignore $ updateHoleUsageArgs False var zs as

 70 |            pure ty

 72 |   updateHoleUsagePats : {auto c : Ref Ctxt Defs} ->

 73 |                         {auto u : Ref UST UState} ->

 74 |                         (useInHole : Bool) ->

 75 |                         Var vars -> List (Term vars) ->

 76 |                         (vs ** (Env Term vs, Term vs, Term vs)) ->

 77 |                         Core Bool

 78 |   updateHoleUsagePats {vars} useInHole var args (vs ** (env, lhs, rhs))

 79 |       = do -- Find the argument which corresponds to var

 80 |            let argpos = findArg Z args

 81 |            log "quantity.hole" 10 $ "At positions " ++ show argpos

 82 |            -- Find what it's position is in env by looking at the lhs args

 83 |            let vars = mapMaybe (findLocal (getArgs lhs)) argpos

 84 |            hs <- traverse (\vsel => updateHoleUsage useInHole vsel [] rhs)

 85 |                           vars

 86 |            pure (any id hs)

 87 |     where

 88 |       findArg : Nat -> List (Term vars) -> List Nat

 89 |       findArg i [] = []

 90 |       findArg i (Local _ _ idx vel :: els)

 91 |           = if idx == varIdx var

 92 |                then i :: findArg (1 + i) els

 93 |                else findArg (1 + i) els

 94 |       findArg i (_ :: els) = findArg (1 + i) els

 96 |       findLocal : List (Term vs) -> Nat -> Maybe (Var vs)

 97 |       findLocal (Local _ _ _ p :: _) Z = Just (MkVar p)

 98 |       findLocal (As _ _ (Local _ _ _ p) _ :: _) Z = Just (MkVar p)

 99 |       findLocal (As _ _ _ (Local _ _ _ p) :: _) Z = Just (MkVar p)

100 |       findLocal (_ :: els) (S k) = findLocal els k

101 |       findLocal _ _ = Nothing

103 |   updateHoleUsage : {0 vars : _} ->

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

105 |                     {auto u : Ref UST UState} ->

106 |                     (useInHole : Bool) ->

107 |                     Var vars -> List (Var vars) ->

108 |                     Term vars -> Core Bool

109 |   updateHoleUsage useInHole (MkVar var) zs (Bind _ _ (Let _ _ val _) sc)

110 |       = do h <- updateHoleUsage useInHole (MkVar var) zs val

111 |            h' <- updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc

112 |            pure (h || h')

113 |   updateHoleUsage useInHole (MkVar var) zs (Bind _ n b sc)

114 |       = updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc

115 |   updateHoleUsage useInHole var zs (Meta fc n i args)

116 |       = do defs <- get Ctxt

117 |            Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)

118 |                 | Nothing => updateHoleUsageArgs useInHole var zs args

119 |            -- only update for holes with no definition yet

120 |            case definition gdef of

121 |                 Hole {} =>

122 |                    do let ty = type gdef

123 |                       ty' <- updateHoleType useInHole var zs ty args

124 |                       updateTy i ty'

125 |                       logTerm "quantity.hole.update" 5 ("New type of " ++

126 |                                  show (fullname gdef)) ty'

127 |                       logTerm "quantity.hole.update" 5 ("Updated from " ++

128 |                                  show (fullname gdef)) (type gdef)

129 |                       pure True

130 |                 _ => updateHoleUsageArgs useInHole var zs args

131 |   updateHoleUsage useInHole var zs (As _ _ a p)

132 |       = do h <- updateHoleUsage useInHole var zs a

133 |            h' <- updateHoleUsage useInHole var zs a

134 |            pure (h || h')

135 |   updateHoleUsage useInHole var zs (TDelayed _ _ t)

136 |       = updateHoleUsage useInHole var zs t

137 |   updateHoleUsage useInHole var zs (TDelay _ _ _ t)

138 |       = updateHoleUsage useInHole var zs t

139 |   updateHoleUsage useInHole var zs (TForce _ _ t)

140 |       = updateHoleUsage useInHole var zs t

141 |   updateHoleUsage useInHole var zs tm

142 |       = case getFnArgs tm of

143 |              (Ref _ _ fn, args) =>

144 |                   -- no need to look inside 'fn' for holes since we did that

145 |                   -- when working through lcheckDef recursively

146 |                   updateHoleUsageArgs useInHole var zs args

147 |              (f, []) => pure False

148 |              (f, args) => updateHoleUsageArgs useInHole var zs (f :: args)

155 |   lcheck : {vars : _} ->

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

157 |            {auto u : Ref UST UState } ->

158 |            RigCount -> (erase : Bool) -> Env Term vars -> Term vars ->

159 |            Core (Term vars, Glued vars, Usage vars)

160 |   lcheck {vars} rig erase env (Local {name} fc x idx prf)

161 |       = let b = getBinder prf env

162 |             rigb = multiplicity b

163 |             ty = binderType b in

164 |             do log "quantity" 15 "lcheck Local"

165 |                when (not erase) $ rigSafe rigb rig

166 |                pure (Local fc x idx prf, gnf env ty, used rig)

167 |     where

168 |       rigSafe : RigCount -> RigCount -> Core ()

169 |       rigSafe l r = when (l < r)

170 |                          (throw (LinearMisuse fc (nameAt prf) l r))

172 |       -- count the usage if we're in a linear context. If not, the usage doesn't

173 |       -- matter

174 |       used : RigCount -> Usage vars

175 |       used r = if isLinear r then [MkVar prf] else []

177 |   lcheck rig erase env (Ref fc nt fn)

178 |       = do logC "quantity" 15 $ do pure "lcheck Ref \{show (nt)} \{show !(toFullNames fn)}"

179 |            ty <- lcheckDef fc rig erase env fn

180 |            pure (Ref fc nt fn, gnf env (embed ty), [])

182 |   -- If the meta has a definition, and we're not in Rig0, expand it first

183 |   -- and check the result.

184 |   -- Otherwise, don't count variable usage in holes, so as far as linearity

185 |   -- checking is concerned, update the type so that the binders

186 |   -- are in Rig0

187 |   lcheck {vars} rig erase env (Meta fc n idx args)

188 |       = do log "quantity" 15 "lcheck Meta"

189 |            defs <- get Ctxt

190 |            Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)

191 |                 | _ => undefinedName fc n

192 |            let expand = branchZero

193 |                           (case type gdef of

194 |                                 Erased {} => True -- defined elsewhere, need to expand

195 |                                 _ => False)

196 |                           (case definition gdef of

197 |                                 PMDef {} => True

198 |                                 _ => False)

199 |                           rig

200 |            logC "quantity" 10 $ do

201 |              def <- case definition gdef of

202 |                          PMDef _ _ (STerm _ tm) _ _ =>

203 |                               do tm' <- toFullNames tm

204 |                                  pure (show tm')

205 |                          _ => pure ""

206 |              pure (show rig ++ ": " ++ show n ++ " " ++ show fc ++ "\n"

207 |                      ++ show def)

208 |            if expand

209 |               then expandMeta rig erase env n idx (definition gdef) args

210 |               else do let ty : ClosedTerm

211 |                              = case definition gdef of

212 |                                     Hole {} => unusedHoleArgs args (type gdef)

213 |                                     _ => type gdef

214 |                       nty <- nf defs env (embed ty)

215 |                       lcheckMeta rig erase env fc n idx args [] nty

216 |     where

217 |       unusedHoleArgs : List a -> Term vs -> Term vs

218 |       unusedHoleArgs (_ :: args) (Bind bfc n (Pi fc _ e ty) sc)

219 |           = Bind bfc n (Pi fc erased e ty) (unusedHoleArgs args sc)

220 |       unusedHoleArgs args (Bind bfc n (Let fc c e ty) sc)

221 |           = Bind bfc n (Let fc c e ty) (unusedHoleArgs args sc)

222 |       unusedHoleArgs _ ty = ty

224 |   lcheck rig_in erase env (Bind fc nm b sc)

225 |       = do log "quantity" 15 "lcheck Bind"

226 |            (b', bt, usedb) <- handleUnify (lcheckBinder rig erase env b)

227 |                                  (\err =>

228 |                                      case err of

229 |                                           LinearMisuse _ _ r _ =>

230 |                                              lcheckBinder rig erase env

231 |                                                 (setMultiplicity b linear)

232 |                                           _ => throw err)

233 |            -- Anything linear can't be used in the scope of a lambda, if we're

234 |            -- checking in general context

235 |            let env' = if rig_in == top

236 |                          then case b of

237 |                               Lam {} => eraseLinear env

238 |                               _ => env

239 |                          else env

240 |            (sc', sct, usedsc) <- lcheck rig erase (b' :: env') sc

242 |            let used_in = count 0 usedsc

243 |            holeFound <- if not erase && isLinear (multiplicity b)

244 |                            then updateHoleUsage (used_in == 0)

245 |                                          first

246 |                                          (map weaken (getErased env'))

247 |                                          sc'

248 |                            else pure False

250 |            -- if there's a hole, assume it will contain the missing usage

251 |            -- if there is none already

252 |            let used = if isLinear ((multiplicity b) |*| rig) &&

253 |                          holeFound && used_in == 0

254 |                          then 1

255 |                          else used_in

257 |            when (not erase) $

258 |                checkUsageOK used ((multiplicity b) |*| rig)

259 |            defs <- get Ctxt

260 |            discharge defs env fc nm b' bt sc' sct (usedb ++ doneScope usedsc)

261 |     where

262 |       rig : RigCount

263 |       rig = case b of

264 |                  Pi {} =>

265 |                       if isErased rig_in

266 |                          then erased

267 |                          else top -- checking as if an inspectable run-time type

268 |                  Let {} => rig_in

269 |                  _ => if isErased rig_in

270 |                          then erased

271 |                          else linear

273 |       checkUsageOK : Nat -> RigCount -> Core ()

274 |       checkUsageOK used r = when (isLinear r && used /= 1)

275 |                                  (throw (LinearUsed fc used nm))

277 |   lcheck rig erase env (App fc f a)

278 |       = do logC "quantity" 15 $ do pure "lcheck App \{show !(toFullNames f)} \{show !(toFullNames a)}"

279 |            (f', gfty, fused) <- lcheck rig erase env f

280 |            defs <- get Ctxt

281 |            fty <- getNF gfty

282 |            case undot fty of

283 |                 NBind _ _ (Pi _ rigf _ ty) scdone =>

284 |                      -- if the argument is borrowed, it's okay to use it in

285 |                      -- unrestricted context, because we'll be out of the

286 |                      -- application without spending it

287 |                    do let checkRig = rigf |*| rig

288 |                       (a', gaty, aused) <- lcheck checkRig erase env a

289 |                       sc' <- scdone defs (toClosure defaultOpts env a')

290 |                       let aerased = if erase && isErased rigf then Erased fc Placeholder else a'

291 |                       -- Possibly remove this check, or make it a compiler

292 |                       -- flag? It is a useful double check on the result of

293 |                       -- elaboration, but there are pathological cases where

294 |                       -- it makes the check very slow (id id id id ... id id etc

295 |                       -- for example) and there may be similar realistic cases.

296 |                       -- If elaboration is correct, this should never fail!

297 |                       opts <- getSession

298 |                       when (debugElabCheck opts) $ do

299 |                         aty <- getNF gaty

300 |                         when (not !(convert defs env aty !(evalClosure defs ty))) $

301 |                            do ty' <- quote defs env ty

302 |                               aty' <- quote defs env aty

303 |                               throw (CantConvert fc (gamma defs) env ty' aty')

304 |                       pure (App fc f' aerased,

305 |                             glueBack defs env sc',

306 |                             fused ++ aused)

307 |                 NApp _ (NRef _ n) _ =>

308 |                       do Just _ <- lookupCtxtExact n (gamma defs)

309 |                               | _ => undefinedName fc n

310 |                          tfty <- getTerm gfty

311 |                          needFunctionType f' gfty

312 |                 NErased _ Placeholder =>

313 |                   do when (not erase) $ needFunctionType f' gfty

314 |                      -- we don't do any linearity checking when `erase` is set

315 |                      -- so returning an empty usage is fine

316 |                      pure (App fc f a, gErased fc, [])

317 |                 _ =>

318 |                   needFunctionType f' gfty

319 |     where

320 |       needFunctionType : Term vars -> Glued vars -> Core _

321 |       needFunctionType f gfty =

322 |         do tfty <- getTerm gfty

323 |            throw (GenericMsg fc ("Linearity checking failed on " ++ show !(toFullNames f) ++

324 |                  " (" ++ show !(toFullNames tfty) ++ " not a function type)"))

326 |       undot : NF vars -> NF vars

327 |       undot (NErased _ (Dotted tm)) = tm

328 |       undot tm = tm

330 |   lcheck rig erase env (As fc s as pat)

331 |       = do log "quantity" 15 "lcheck As"

332 |            (as', _, _) <- lcheck rig erase env as

333 |            (pat', pty, u) <- lcheck rig erase env pat

334 |            pure (As fc s as' pat', pty, u)

335 |   lcheck rig erase env (TDelayed fc r ty)

336 |       = do log "quantity" 15 "lcheck Delayed"

337 |            (ty', _, u) <- lcheck rig erase env ty

338 |            pure (TDelayed fc r ty', gType fc (MN "top" 0), u)

339 |   lcheck rig erase env (TDelay fc r ty val)

340 |       = do (ty', _, _) <- lcheck erased erase env ty

341 |            (val', gty, u) <- lcheck rig erase env val

342 |            ty <- getTerm gty

343 |            pure (TDelay fc r ty' val', gnf env (TDelayed fc r ty), u)

344 |   lcheck rig erase env (TForce fc r val)

345 |       = do log "quantity" 15 "lcheck Force"

346 |            (val', gty, u) <- lcheck rig erase env val

347 |            tynf <- getNF gty

348 |            case tynf of

349 |                 NDelayed _ r narg

350 |                     => do defs <- get Ctxt

351 |                           pure (TForce fc r val', glueBack defs env narg, u)

352 |                 _ => throw (GenericMsg fc "Not a delayed type")

353 |   lcheck rig erase env (PrimVal fc c)

354 |       = do log "quantity" 15 "lcheck PrimVal"

355 |            pure (PrimVal fc c, gErased fc, [])

356 |   lcheck rig erase env (Erased fc i)

357 |       = do log "quantity" 15 "lcheck Erased"

358 |            pure (Erased fc i, gErased fc, [])

359 |   lcheck rig erase env (TType fc u)

360 |       -- Not universe checking here, just use the top of the hierarchy

361 |       = do log "quantity" 15 "lcheck TType"

362 |            pure (TType fc u, gType fc (MN "top" 0), [])

364 |   lcheckBinder : {vars : _} ->

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

366 |                  {auto u : Ref UST UState} ->

367 |                  RigCount -> (erase : Bool) -> Env Term vars ->

368 |                  Binder (Term vars) ->

369 |                  Core (Binder (Term vars), Glued vars, Usage vars)

370 |   lcheckBinder rig erase env (Lam fc c x ty)

371 |       = do (tyv, tyt, _) <- lcheck erased erase env ty

372 |            pure (Lam fc c x tyv, tyt, [])

373 |   lcheckBinder rig erase env (Let fc rigc val ty)

374 |       = do (tyv, tyt, _) <- lcheck erased erase env ty

375 |            (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val

376 |            pure (Let fc rigc valv tyv, tyt, vs)

377 |   lcheckBinder rig erase env (Pi fc c x ty)

378 |       = do (tyv, tyt, _) <- lcheck (rig |*| c) erase env ty

379 |            pure (Pi fc c x tyv, tyt, [])

380 |   lcheckBinder rig erase env (PVar fc c p ty)

381 |       = do (tyv, tyt, _) <- lcheck erased erase env ty

382 |            pure (PVar fc c p tyv, tyt, [])

383 |   lcheckBinder rig erase env (PLet fc rigc val ty)

384 |       = do (tyv, tyt, _) <- lcheck erased erase env ty

385 |            (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val

386 |            pure (PLet fc rigc valv tyv, tyt, vs)

387 |   lcheckBinder rig erase env (PVTy fc c ty)

388 |       = do (tyv, tyt, _) <- lcheck erased erase env ty

389 |            pure (PVTy fc c tyv, tyt, [])

391 |   discharge : {vars : _} ->

392 |               Defs -> Env Term vars ->

393 |               FC -> (nm : Name) -> Binder (Term vars) -> Glued vars ->

394 |               Term (nm :: vars) -> Glued (nm :: vars) -> Usage vars ->

395 |               Core (Term vars, Glued vars, Usage vars)

396 |   discharge defs env fc nm (Lam fc' c x ty) gbindty scope gscopety used

397 |        = do scty <- getTerm gscopety

398 |             pure (Bind fc nm (Lam fc' c x ty) scope,

399 |                   gnf env (Bind fc nm (Pi fc' c x ty) scty), used)

400 |   discharge defs env fc nm (Let fc' c val ty) gbindty scope gscopety used

401 |        = do scty <- getTerm gscopety

402 |             pure (Bind fc nm (Let fc' c val ty) scope,

403 |                   gnf env (Bind fc nm (Let fc' c val ty) scty), used)

404 |   discharge defs env fc nm (Pi fc' c x ty) gbindty scope gscopety used

405 |        = pure (Bind fc nm (Pi fc' c x ty) scope, gbindty, used)

406 |   discharge defs env fc nm (PVar fc' c p ty) gbindty scope gscopety used

407 |        = do scty <- getTerm gscopety

408 |             pure (Bind fc nm (PVar fc' c p ty) scope,

409 |                   gnf env (Bind fc nm (PVTy fc' c ty) scty), used)

410 |   discharge defs env fc nm (PLet fc' c val ty) gbindty scope gscopety used

411 |        = do scty <- getTerm gscopety

412 |             pure (Bind fc nm (PLet fc' c val ty) scope,

413 |                   gnf env (Bind fc nm (PLet fc' c val ty) scty), used)

414 |   discharge defs env fc nm (PVTy fc' c ty) gbindty scope gscopety used

415 |        = pure (Bind fc nm (PVTy fc' c ty) scope, gbindty, used)

417 |   data ArgUsage

418 |        = UseAny -- RigW so we don't care

419 |        | Use0 -- argument position not used

420 |        | Use1 -- argument position used exactly once

421 |        | UseKeep -- keep as is

422 |        | UseUnknown -- hole, so can't tell

424 |   Show ArgUsage where

425 |     show UseAny = "any"

426 |     show Use0 = "0"

427 |     show Use1 = "1"

428 |     show UseKeep = "keep"

429 |     show UseUnknown = "unknown"

431 |   -- Check argument usage in case blocks. Returns a list of how each argument

432 |   -- in the case block is used, to build the appropriate type for the outer

433 |   -- block.

434 |   getArgUsage : {auto c : Ref Ctxt Defs} ->

435 |                 {auto e : Ref UST UState} ->

436 |                 FC -> RigCount -> ClosedTerm ->

437 |                 List (vs ** (Env Term vs, Term vs, Term vs)) ->

438 |                 Core (List ArgUsage)

439 |   getArgUsage topfc rig ty pats

440 |       = do us <- traverse (getPUsage ty) pats

441 |            pure (map snd !(combine us))

442 |     where

443 |       getCaseUsage : Term ns -> Env Term vs -> List (Term vs) ->

444 |                      Usage vs -> Term vs ->

445 |                      Core (List (Name, ArgUsage))

446 |       getCaseUsage ty env (As _ _ _ p :: args) used rhs

447 |           = getCaseUsage ty env (p :: args) used rhs

448 |       getCaseUsage (Bind _ n (Pi _ rig _ ty) sc) env (arg :: args) used rhs

449 |           = if isLinear rig

450 |                then case arg of

451 |                          (Local _ _ idx p) =>

452 |                            do rest <- getCaseUsage sc env args used rhs

453 |                               let used_in = count idx used

454 |                               holeFound <- updateHoleUsage (used_in == 0) (MkVar p) [] rhs

455 |                               let ause

456 |                                   = if holeFound && used_in == 0

457 |                                             then UseUnknown

458 |                                             else if used_in == 0

459 |                                                     then Use0

460 |                                                     else Use1

461 |                               pure ((n, ause) :: rest)

462 |                          _ => do elseCase

463 |                else elseCase

464 |           where

465 |             elseCase : Core (List (Name, ArgUsage))

466 |             elseCase = do rest <- getCaseUsage sc env args used rhs

467 |                           pure $ if isErased rig

468 |                              then ((n, Use0) :: rest)

469 |                              else ((n, UseKeep) :: rest)

470 |       getCaseUsage tm env args used rhs = pure []

472 |       checkUsageOK : FC -> Nat -> Name -> Bool -> RigCount -> Core ()

473 |       checkUsageOK fc used nm isloc rig

474 |           = when (isLinear rig && ((isloc && used > 1) || (not isloc && used /= 1)))

475 |                  (throw (LinearUsed fc used nm))

477 |       -- Is the variable one of the lhs arguments; i.e. do we treat it as

478 |       -- affine rather than linear

479 |       isLocArg : Var vars -> List (Term vars) -> Bool

480 |       isLocArg p [] = False

481 |       isLocArg p (Local _ _ idx _ :: args)

482 |           = idx == varIdx p || isLocArg p args

483 |       isLocArg p (As _ _ tm pat :: args)

484 |           = isLocArg p (tm :: pat :: args)

485 |       isLocArg p (_ :: args) = isLocArg p args

487 |       -- As checkEnvUsage in general, but it's okay for local variables to

488 |       -- remain unused (since in that case, they must be used outside the

489 |       -- case block)

490 |       checkEnvUsage : {vars : _} ->

491 |                       SizeOf done ->

492 |                       RigCount ->

493 |                       Env Term vars -> Usage (done <>> vars) ->

494 |                       List (Term (done <>> vars)) ->

495 |                       Term (done <>> vars) -> Core ()

496 |       checkEnvUsage s rig [] usage args tm = pure ()

497 |       checkEnvUsage s rig {done} {vars = nm :: xs} (b :: env) usage args tm

498 |           = do let pos = mkVarChiply s

499 |                let used_in = count (varIdx pos) usage

501 |                holeFound <- if isLinear (multiplicity b)

502 |                                then updateHoleUsage (used_in == 0) pos [] tm

503 |                                else pure False

504 |                let used = if isLinear ((multiplicity b) |*| rig) &&

505 |                              holeFound && used_in == 0

506 |                              then 1

507 |                              else used_in

508 |                checkUsageOK (getLoc (binderType b))

509 |                             used nm (isLocArg pos args)

510 |                                     ((multiplicity b) |*| rig)

511 |                checkEnvUsage (s :< nm) rig env usage args tm

513 |       getPUsage : ClosedTerm -> (vs ** (Env Term vs, Term vs, Term vs)) ->

514 |                   Core (List (Name, ArgUsage))

515 |       getPUsage ty (_ ** (penv, lhs, rhs))

516 |           = do logEnv "quantity" 10 "Env" penv

517 |                logTerm "quantity" 10 "LHS" lhs

518 |                logTerm "quantity" 5 "Linear check in case RHS" rhs

519 |                (rhs', _, used) <- lcheck rig False penv rhs

520 |                log "quantity" 10 $ "Used: " ++ show used

521 |                let args = getArgs lhs

522 |                checkEnvUsage [<] rig penv used args rhs'

523 |                ause <- getCaseUsage ty penv args used rhs

524 |                log "quantity" 10 $ "Arg usage: " ++ show ause

525 |                pure ause

527 |       combineUsage : (Name, ArgUsage) -> (Name, ArgUsage) ->

528 |                      Core (Name, ArgUsage)

529 |       combineUsage (n, Use0) (_, Use1)

530 |           = throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))

531 |       combineUsage (n, Use1) (_, Use0)

532 |           = throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))

533 |       combineUsage (n, UseAny) _ = pure (n, UseAny)

534 |       combineUsage _ (n, UseAny) = pure (n, UseAny)

535 |       combineUsage (n, UseKeep) _ = pure (n, UseKeep)

536 |       combineUsage _ (n, UseKeep) = pure (n, UseKeep)

537 |       combineUsage (n, UseUnknown) _ = pure (n, UseUnknown)

538 |       combineUsage _ (n, UseUnknown) = pure (n, UseUnknown)

539 |       combineUsage x y = pure x

541 |       combineUsages : List (Name, ArgUsage) -> List (Name, ArgUsage) ->

542 |                       Core (List (Name, ArgUsage))

543 |       combineUsages [] [] = pure []

544 |       combineUsages (u :: us) (v :: vs)

545 |           = do u' <- combineUsage u v

546 |                us' <- combineUsages us vs

547 |                pure (u' :: us')

548 |       combineUsages _ _ = throw (InternalError "Argument usage lists inconsistent")

550 |       combine : List (List (Name, ArgUsage)) ->

551 |                 Core (List (Name, ArgUsage))

552 |       combine [] = pure []

553 |       combine [x] = pure x

554 |       combine (x :: xs)

555 |           = do xs' <- combine xs

556 |                combineUsages x xs'

558 |   lcheckDef : {auto c : Ref Ctxt Defs} ->

559 |               {auto u : Ref UST UState} ->

560 |               FC -> RigCount -> (erase : Bool) -> Env Term vars -> Name ->

561 |               Core ClosedTerm

562 |   lcheckDef fc rig True env n

563 |       = do defs <- get Ctxt

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

565 |                 | Nothing => undefinedName fc n

566 |            pure (type def)

567 |   lcheckDef fc rig False env n

568 |       = do defs <- get Ctxt

569 |            let Just idx = getNameID n (gamma defs)

570 |                 | Nothing => undefinedName fc n

571 |            Just def <- lookupCtxtExact (Resolved idx) (gamma defs)

572 |                 | Nothing => undefinedName fc n

573 |            rigSafe (multiplicity def) rig

574 |            if linearChecked def

575 |               then pure (type def)

576 |               else case definition def of

577 |                         PMDef _ _ _ _ pats =>

578 |                             do u <- getArgUsage (getLoc (type def))

579 |                                                 rig (type def) pats

580 |                                log "quantity" 5 $ "Overall arg usage " ++ show u

581 |                                let ty' = updateUsage u (type def)

582 |                                updateTy idx ty'

583 |                                setLinearCheck idx True

584 |                                logTerm "quantity" 5 ("New type of " ++

585 |                                           show (fullname def)) ty'

586 |                                logTerm "quantity" 5 ("Updated from " ++

587 |                                           show (fullname def)) (type def)

588 |                                pure ty'

589 |                         _ => pure (type def)

590 |     where

591 |       updateUsage : List ArgUsage -> Term ns -> Term ns

592 |       updateUsage (u :: us) (Bind bfc n (Pi fc c e ty) sc)

593 |           = let sc' = updateUsage us sc

594 |                 c' = case u of

595 |                           Use0 => erased

596 |                           Use1 => linear -- ignore usage elsewhere, we checked here

597 |                           UseUnknown => c -- don't know, assumed unchanged and update hole types

598 |                           UseKeep => c -- matched here, so count usage elsewhere

599 |                           UseAny => c in -- no constraint, so leave alone

600 |                 Bind bfc n (Pi fc c' e ty) sc'

601 |       updateUsage _ ty = ty

603 |       rigSafe : RigCount -> RigCount -> Core ()

604 |       rigSafe a b = when (a < b)

605 |                          (throw (LinearMisuse fc !(getFullName n) a b))

607 |   expandMeta : {vars : _} ->

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

609 |                {auto u : Ref UST UState} ->

610 |                RigCount -> (erase : Bool) -> Env Term vars ->

611 |                Name -> Int -> Def -> List (Term vars) ->

612 |                Core (Term vars, Glued vars, Usage vars)

613 |   expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args

614 |       = do tm <- substMeta (embed fn) args zero Subst.empty

615 |            lcheck rig erase env tm

616 |     where

617 |       substMeta : {drop, vs : _} ->

618 |                   Term (drop ++ vs) -> List (Term vs) ->

619 |                   SizeOf drop -> SubstEnv drop vs ->

620 |                   Core (Term vs)

621 |       substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env

622 |           = substMeta sc as (suc drop) (a :: env)

623 |       substMeta (Bind bfc n (Let _ c val ty) sc) as drop env

624 |           = substMeta (subst val sc) as drop env

625 |       substMeta rhs [] drop env = pure (substs drop env rhs)

626 |       substMeta rhs _ _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show fn))

627 |   expandMeta rig erase env n idx def _

628 |       = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def))

630 |   lcheckMeta : {vars : _} ->

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

632 |                {auto u : Ref UST UState} ->

633 |                RigCount -> Bool -> Env Term vars ->

634 |                FC -> Name -> Int ->

635 |                (args : List (Term vars)) ->

636 |                (checked : List (Term vars)) ->

637 |                NF vars -> Core (Term vars, Glued vars, Usage vars)

638 |   lcheckMeta rig erase env fc n idx

639 |              (arg :: args) chk (NBind _ _ (Pi _ rigf _ ty) sc)

640 |       = do let checkRig = rigf |*| rig

641 |            (arg', gargTy, aused) <- lcheck checkRig erase env arg

642 |            defs <- get Ctxt

643 |            sc' <- sc defs (toClosure defaultOpts env arg')

644 |            let aerased = if erase && isErased rigf

645 |                             then Erased fc Placeholder

646 |                             else arg'

647 |            (tm, gty, u) <- lcheckMeta rig erase env fc n idx args

648 |                                       (aerased :: chk) sc'

649 |            pure (tm, gty, aused ++ u)

650 |   lcheckMeta rig erase env fc n idx (arg :: args) chk nty

651 |       = do defs <- get Ctxt

652 |            empty <- clearDefs defs

653 |            ty <- quote empty env nty

654 |            throw (GenericMsg fc ("Linearity checking failed on metavar "

655 |                       ++ show !(toFullNames n) ++ " (" ++ show !(toFullNames ty)

656 |                       ++ " not a function type)"))

657 |   lcheckMeta rig erase env fc n idx [] chk nty

658 |       = do defs <- get Ctxt

659 |            pure (Meta fc n idx (reverse chk), glueBack defs env nty, [])

662 | checkEnvUsage : {vars : _} ->

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

664 |                 {auto u : Ref UST UState} ->

665 |                 FC -> SizeOf done -> RigCount ->

666 |                 Env Term vars -> Usage (done <>> vars) ->

667 |                 Term (done <>> vars) ->

668 |                 Core ()

669 | checkEnvUsage fc s rig [] usage tm = pure ()

670 | checkEnvUsage fc s rig {vars = nm :: xs} (b :: env) usage tm

671 |     = do let pos = mkVarChiply s

672 |          let used_in = count (varIdx pos) usage

674 |          holeFound <- if isLinear (multiplicity b)

675 |                          then updateHoleUsage (used_in == 0) pos [] tm

676 |                          else pure False

677 |          let used = if isLinear ((multiplicity b) |*| rig) &&

678 |                        holeFound && used_in == 0

679 |                        then 1

680 |                        else used_in

681 |          checkUsageOK used ((multiplicity b) |*| rig)

682 |          checkEnvUsage fc (s :< nm) rig env usage tm

683 |   where

684 |     checkUsageOK : Nat -> RigCount -> Core ()

685 |     checkUsageOK used r = when (isLinear r && used /= 1)

686 |                                (throw (LinearUsed fc used nm))

693 | linearCheck : {vars : _} ->

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

695 |               {auto u : Ref UST UState} ->

696 |               FC -> RigCount -> (erase : Bool) ->

697 |               Env Term vars -> Term vars ->

698 |               Core (Term vars)

699 | linearCheck fc rig erase env tm

700 |     = do logTerm "quantity" 5 "Linearity check on " tm

701 |          logEnv "quantity" 5 "In env" env

702 |          (tm', _, used) <- lcheck rig erase env tm

703 |          log "quantity" 5 $ "Used: " ++ show used

704 |          when (not erase) $ checkEnvUsage fc [<] rig env used tm'

705 |          pure tm'