0 | module TTImp.Elab.App

  2 | import Core.Env

  3 | import Core.Metadata

  4 | import Core.Unify

  5 | import Core.Value

  7 | import Idris.REPL.Opts

  8 | import Idris.Syntax

 10 | import TTImp.Elab.Check

 11 | import TTImp.Elab.Dot

 12 | import TTImp.TTImp

 14 | import Data.List

 15 | import Data.Maybe

 17 | import Libraries.Data.List.Extra

 18 | import Libraries.Data.NatSet

 19 | import Libraries.Data.VarSet

 20 | import Libraries.Data.WithDefault

 22 | %default covering

 24 | checkVisibleNS : {auto c : Ref Ctxt Defs} ->

 25 |                  FC -> Name -> Visibility -> Core ()

 26 | checkVisibleNS fc (NS ns x) vis

 27 |     = if !(isVisible ns)

 28 |          then if !isAllPublic

 29 |                        || visibleInAny (!getNS :: !getNestedNS) (NS ns x) vis

 30 |                  then pure ()

 31 |                  else throw $ InvisibleName fc (NS ns x) Nothing

 32 |          else throw $ InvisibleName fc (NS ns x) (Just ns)

 33 | checkVisibleNS _ _ _ = pure ()

 35 | onLHS : ElabMode -> Bool

 36 | onLHS (InLHS _) = True

 37 | onLHS _ = False

 41 | getNameType : {vars : _} ->

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

 43 |               {auto m : Ref MD Metadata} ->

 44 |               {auto e : Ref EST (EState vars)} ->

 45 |               ElabMode ->

 46 |               RigCount -> Env Term vars ->

 47 |               FC -> Name ->

 48 |               Core (Term vars, Glued vars)

 49 | getNameType elabMode rigc env fc x

 50 |     = case defined x env of

 51 |            Just (MkIsDefined rigb lv) =>

 52 |               do rigSafe rigb rigc

 53 |                  let binder = getBinder lv env

 54 |                  let bty = binderType binder

 56 |                  log "metadata.names" 7 $ "getNameType is adding ↓"

 57 |                  addNameType fc x env bty

 59 |                  when (isLinear rigb) $ update EST { linearUsed $= VarSet.insert (MkVar lv) }

 60 |                  log "ide-mode.highlight" 8

 61 |                      $ "getNameType is trying to add Bound: "

 62 |                       ++ show x ++ " (" ++ show fc ++ ")"

 63 |                  when (isSourceName x) $

 64 |                    whenJust (isConcreteFC fc) $ \nfc => do

 65 |                      log "ide-mode.highlight" 7 $ "getNameType is adding Bound: " ++ show x

 66 |                      addSemanticDecorations [(nfc, Bound, Just x)]

 68 |                  pure (Local fc (Just (isLet binder)) _ lv, gnf env bty)

 69 |            Nothing =>

 70 |               do defs <- get Ctxt

 71 |                  [(pname, i, def)] <- lookupCtxtName x (gamma defs)

 72 |                       | ns => ambiguousName fc x (map fst ns)

 73 |                  checkVisibleNS fc (fullname def) (collapseDefault $ visibility def)

 74 |                  when (not $ onLHS elabMode) $

 75 |                    checkDeprecation fc def

 76 |                  rigSafe (multiplicity def) rigc

 77 |                  let nt = getDefNameType def

 79 |                  log "ide-mode.highlight" 8

 80 |                      $ "getNameType is trying to add something for: "

 81 |                       ++ show def.fullname ++ " (" ++ show fc ++ ")"

 83 |                  when (isSourceName def.fullname) $

 84 |                    whenJust (isConcreteFC fc) $ \nfc => do

 85 |                      let decor = ifThenElse (isEscapeHatch def) Postulate (nameDecoration def.fullname nt)

 86 |                      log "ide-mode.highlight" 7

 87 |                        $ "getNameType is adding " ++ show decor ++ ": " ++ show def.fullname

 88 |                      addSemanticDecorations [(nfc, decor, Just def.fullname)]

 90 |                  pure (Ref fc nt (Resolved i), gnf env (embed (type def)))

 91 |   where

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

 93 |     rigSafe lhs rhs = when (lhs < rhs)

 94 |                            (throw (LinearMisuse fc !(getFullName x) lhs rhs))

 96 |     checkDeprecation : FC -> GlobalDef -> Core ()

 97 |     checkDeprecation fc gdef =

 98 |       do when (Deprecate `elem` gdef.flags) $

 99 |            recordWarning $

100 |              Deprecated fc

101 |                "\{show gdef.fullname} is deprecated and will be removed in a future version."

102 |                (Just (fc, gdef.fullname))

105 | getVarType : {vars : _} ->

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

107 |              {auto m : Ref MD Metadata} ->

108 |              {auto e : Ref EST (EState vars)} ->

109 |              ElabMode ->

110 |              RigCount -> NestedNames vars -> Env Term vars ->

111 |              FC -> Name ->

112 |              Core (Term vars, Nat, Glued vars)

113 | getVarType elabMode rigc nest env fc x

114 |     = case lookup x (names nest) of

115 |            Nothing => do (tm, ty) <- getNameType elabMode rigc env fc x

116 |                          pure (tm, 0, ty)

117 |            Just (nestn, argns, tmf) =>

118 |               do defs <- get Ctxt

119 |                  let arglen = length argns

120 |                  let n' = fromMaybe x nestn

121 |                  case !(lookupCtxtExact n' (gamma defs)) of

122 |                       Nothing => undefinedName fc n'

123 |                       Just ndef =>

124 |                          let nt = getDefNameType ndef

125 |                              tm = tmf fc nt

126 |                              tyenv = useVars (getArgs tm)

127 |                                              (embed (type ndef)) in

128 |                              do checkVisibleNS fc (fullname ndef) (collapseDefault $ visibility ndef)

129 |                                 logTerm "elab" 5 ("Type of " ++ show n') tyenv

130 |                                 logTerm "elab" 5 ("Expands to") tm

131 |                                 log "elab" 5 $ "Arg length " ++ show arglen

133 |                                 -- Add the type to the metadata

134 |                                 log "metadata.names" 7 $ "getVarType is adding ↓"

135 |                                 addNameType fc x env tyenv

137 |                                 when (isSourceName ndef.fullname) $

138 |                                   whenJust (isConcreteFC fc) $ \nfc => do

139 |                                     let decor = nameDecoration ndef.fullname nt

140 |                                     log "ide-mode.highlight" 7

141 |                                        $ "getNameType is adding "++ show decor ++": "

142 |                                                                  ++ show ndef.fullname

143 |                                     addSemanticDecorations [(nfc, decor, Just ndef.fullname)]

145 |                                 pure (tm, arglen, gnf env tyenv)

146 |     where

147 |       useVars : {vars : _} ->

148 |                 List (Term vars) -> Term vars -> Term vars

149 |       useVars [] sc = sc

150 |       useVars (a :: as) (Bind bfc n (Pi fc c _ ty) sc)

151 |            = Bind bfc n (Let fc c a ty) (useVars (map weaken as) sc)

152 |       useVars as (Bind bfc n (Let fc c v ty) sc)

153 |            = Bind bfc n (Let fc c v ty) (useVars (map weaken as) sc)

154 |       useVars _ sc = sc -- Can't happen?

156 | isHole : NF vars -> Bool

157 | isHole (NApp _ (NMeta {}) _) = True

158 | isHole _ = False

161 |   makeImplicit : {vars : _} ->

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

163 |                  {auto m : Ref MD Metadata} ->

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

165 |                  {auto e : Ref EST (EState vars)} ->

166 |                  {auto s : Ref Syn SyntaxInfo} ->

167 |                  {auto o : Ref ROpts REPLOpts} ->

168 |                  RigCount -> RigCount -> ElabInfo ->

169 |                  NestedNames vars -> Env Term vars ->

170 |                  FC -> (fntm : Term vars) ->

171 |                  Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->

172 |                  (argdata : (Maybe Name, Nat)) ->

173 |                  (expargs : List RawImp) ->

174 |                  (autoargs : List RawImp) ->

175 |                  (namedargs : List (Name, RawImp)) ->

176 |                  (knownret : Bool) ->

177 |                  (expected : Maybe (Glued vars)) ->

178 |                  Core (Term vars, Glued vars)

179 |   makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty

180 |       = do defs <- get Ctxt

181 |            nm <- genMVName x

182 |            empty <- clearDefs defs

183 |            metaty <- quote empty env aty

184 |            metaval <- metaVar fc argRig env nm metaty

185 |            let fntm = App fc tm metaval

186 |            fnty <- sc defs (toClosure defaultOpts env metaval)

187 |            when (bindingVars elabinfo) $ update EST $

188 |              addBindIfUnsolved nm (getLoc (getFn tm)) argRig Implicit env metaval metaty

189 |            checkAppWith rig elabinfo nest env fc

190 |                         fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

192 |   makeAutoImplicit : {vars : _} ->

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

194 |                      {auto m : Ref MD Metadata} ->

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

196 |                      {auto e : Ref EST (EState vars)} ->

197 |                      {auto s : Ref Syn SyntaxInfo} ->

198 |                      {auto o : Ref ROpts REPLOpts} ->

199 |                      RigCount -> RigCount -> ElabInfo ->

200 |                      NestedNames vars -> Env Term vars ->

201 |                      FC -> (fntm : Term vars) ->

202 |                      Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->

203 |                      (argpos : (Maybe Name, Nat)) ->

204 |                      (expargs : List RawImp) ->

205 |                      (autoargs : List RawImp) ->

206 |                      (namedargs : List (Name, RawImp)) ->

207 |                      (knownret : Bool) ->

208 |                      (expected : Maybe (Glued vars)) ->

209 |                      Core (Term vars, Glued vars)

210 |   makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty

211 |   -- on the LHS, just treat it as an implicit pattern variable.

212 |   -- on the RHS, add a searchable hole

213 |       = if metavarImp (elabMode elabinfo)

214 |            then do defs <- get Ctxt

215 |                    nm <- genMVName x

216 |                    empty <- clearDefs defs

217 |                    metaty <- quote empty env aty

218 |                    metaval <- metaVar fc argRig env nm metaty

219 |                    let fntm = App fc tm metaval

220 |                    fnty <- sc defs (toClosure defaultOpts env metaval)

221 |                    update EST $ addBindIfUnsolved nm (getLoc (getFn tm)) argRig AutoImplicit env metaval metaty

222 |                    checkAppWith rig elabinfo nest env fc

223 |                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

224 |            else do defs <- get Ctxt

225 |                    nm <- genMVName x

226 |                    empty <- clearDefs defs

227 |                    -- Normalise fully, but only if it's cheap enough.

228 |                    -- We have to get the normal form eventually anyway, but

229 |                    -- it might be too early to do it now if something is

230 |                    -- blocking it and we're not yet ready to search.

231 |                    metaty <- catch (quoteOpts (MkQuoteOpts False False (Just 10))

232 |                                               defs env aty)

233 |                                    (\err => quote empty env aty)

234 |                    est <- get EST

235 |                    lim <- getAutoImplicitLimit

236 |                    metaval <- searchVar fc argRig lim (Resolved (defining est))

237 |                                         env nest nm metaty

238 |                    let fntm = App fc tm metaval

239 |                    fnty <- sc defs (toClosure defaultOpts env metaval)

240 |                    checkAppWith rig elabinfo nest env fc

241 |                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

242 |     where

243 |       metavarImp : ElabMode -> Bool

244 |       metavarImp (InLHS _) = True

245 |       metavarImp InTransform = True

246 |       metavarImp _ = False

248 |   makeDefImplicit : {vars : _} ->

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

250 |                     {auto m : Ref MD Metadata} ->

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

252 |                     {auto e : Ref EST (EState vars)} ->

253 |                     {auto s : Ref Syn SyntaxInfo} ->

254 |                     {auto o : Ref ROpts REPLOpts} ->

255 |                     RigCount -> RigCount -> ElabInfo ->

256 |                     NestedNames vars -> Env Term vars ->

257 |                     FC -> (fntm : Term vars) ->

258 |                     Name -> Closure vars -> Closure vars ->

259 |                     (Defs -> Closure vars -> Core (NF vars)) ->

260 |                     (argpos : (Maybe Name, Nat)) ->

261 |                     (expargs : List RawImp) ->

262 |                     (autoargs : List RawImp) ->

263 |                     (namedargs : List (Name, RawImp)) ->

264 |                     (knownret : Bool) ->

265 |                     (expected : Maybe (Glued vars)) ->

266 |                     Core (Term vars, Glued vars)

267 |   makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs autoargs namedargs kr expty

268 |   -- on the LHS, just treat it as an implicit pattern variable.

269 |   -- on the RHS, use the default

270 |       = if metavarImp (elabMode elabinfo)

271 |            then do defs <- get Ctxt

272 |                    nm <- genMVName x

273 |                    empty <- clearDefs defs

274 |                    metaty <- quote empty env aty

275 |                    metaval <- metaVar fc argRig env nm metaty

276 |                    let fntm = App fc tm metaval

277 |                    fnty <- sc defs (toClosure defaultOpts env metaval)

278 |                    update EST $ addBindIfUnsolved nm (getLoc (getFn tm)) argRig AutoImplicit env metaval metaty

279 |                    checkAppWith rig elabinfo nest env fc

280 |                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

281 |            else do defs <- get Ctxt

282 |                    empty <- clearDefs defs

283 |                    aval <- quote empty env arg

284 |                    let fntm = App fc tm aval

285 |                    fnty <- sc defs (toClosure defaultOpts env aval)

286 |                    checkAppWith rig elabinfo nest env fc

287 |                                 fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

288 |     where

289 |       metavarImp : ElabMode -> Bool

290 |       metavarImp (InLHS _) = True

291 |       metavarImp InTransform = True

292 |       metavarImp _ = False

294 |   -- Defer elaborating anything which will be easier given a known target

295 |   -- type (ambiguity, cases, etc)

296 |   needsDelayExpr : {auto c : Ref Ctxt Defs} ->

297 |                    (knownRet : Bool) -> RawImp ->

298 |                    Core Bool

299 |   needsDelayExpr False _ = pure False

300 |   needsDelayExpr True (IVar fc n)

301 |       = do defs <- get Ctxt

302 |            pure $ case !(lookupCtxtName n (gamma defs)) of

303 |                        (_ :: _ :: _) => True

304 |                        _ => False

305 |   needsDelayExpr True (IApp _ f _) = needsDelayExpr True f

306 |   needsDelayExpr True (IAutoApp _ f _) = needsDelayExpr True f

307 |   needsDelayExpr True (INamedApp _ f _ _) = needsDelayExpr True f

308 |   needsDelayExpr True (ILam {}) = pure True

309 |   needsDelayExpr True (ICase {}) = pure True

310 |   needsDelayExpr True (ILocal {}) = pure True

311 |   needsDelayExpr True (IUpdate {}) = pure True

312 |   needsDelayExpr True (IAlternative {}) = pure True

313 |   needsDelayExpr True (ISearch {}) = pure True

314 |   needsDelayExpr True (IRewrite {}) = pure True

315 |   needsDelayExpr True _ = pure False

317 |   -- On the LHS, for any concrete thing, we need to make sure we know

318 |   -- its type before we proceed so that we can reject it if the type turns

319 |   -- out to be polymorphic

320 |   needsDelayLHS : {auto c : Ref Ctxt Defs} ->

321 |                   RawImp -> Core Bool

322 |   needsDelayLHS (IVar fc n) = pure True

323 |   needsDelayLHS (IApp _ f _) = needsDelayLHS f

324 |   needsDelayLHS (IAutoApp _ f _) = needsDelayLHS f

325 |   needsDelayLHS (INamedApp _ f _ _) = needsDelayLHS f

326 |   needsDelayLHS (IAlternative {}) = pure True

327 |   needsDelayLHS (IAs _ _ _ _ t) = needsDelayLHS t

328 |   needsDelayLHS (ISearch {}) = pure True

329 |   needsDelayLHS (IPrimVal {}) = pure True

330 |   needsDelayLHS (IType _) = pure True

331 |   needsDelayLHS (IWithUnambigNames _ _ t) = needsDelayLHS t

332 |   needsDelayLHS _ = pure False

334 |   needsDelay : {auto c : Ref Ctxt Defs} ->

335 |                ElabMode ->

336 |                (knownRet : Bool) -> RawImp ->

337 |                Core Bool

338 |   needsDelay (InLHS _) _ tm = needsDelayLHS tm

339 |   needsDelay _ kr tm = needsDelayExpr kr tm

341 |   checkValidPattern :

342 |     {vars : _} ->

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

344 |     {auto m : Ref MD Metadata} ->

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

346 |     {auto e : Ref EST (EState vars)} ->

347 |     RigCount -> Env Term vars -> FC ->

348 |     Term vars -> Glued vars ->

349 |     Core (Term vars, Glued vars)

350 |   checkValidPattern rig env fc tm ty

351 |     = do log "elab.app.lhs" 50 $ "Checking that " ++ show tm ++ " is a valid pattern"

352 |          case tm of

353 |            Bind _ _ (Lam {}) _ => registerDot rig env fc NotConstructor tm ty

354 |            _ => pure (tm, ty)

356 |   dotErased : {vars : _} ->

357 |               {auto c : Ref Ctxt Defs} -> (argty : Closure vars) ->

358 |               Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp

359 |   dotErased argty mn argpos (InLHS lrig ) rig tm

360 |       = if not (isErased lrig) && isErased rig

361 |           then do

362 |             -- if the argument type aty has a single constructor, there's no need

363 |             -- to dot it

364 |             defs <- get Ctxt

365 |             nfargty <- evalClosure defs argty

366 |             mconsCount <- countConstructors nfargty

367 |             logNF "elab.app.dot" 50

368 |               "Found \{show mconsCount} constructors for type"

369 |               (mkEnv emptyFC vars)

370 |               nfargty

371 |             if mconsCount == Just 1 || mconsCount == Just 0

372 |               then pure tm

373 |               else

374 |                 -- if argpos is an erased position of 'n', leave it, otherwise dot if

375 |                 -- necessary

376 |                 do Just gdef <- maybe (pure Nothing) (\n => lookupCtxtExact n (gamma defs)) mn

377 |                         | Nothing => pure (dotTerm tm)

378 |                    if argpos `elem` safeErase gdef

379 |                       then pure tm

380 |                       else pure $ dotTerm tm

381 |           else pure tm

382 |     where

383 |       -- TODO: this seems too conservative. If we get back an expression stuck on a

384 |       -- meta, shouldn't we delay the check instead of declaring the tm dotted?

385 |       ||| Count the constructors of a fully applied concrete datatype

386 |       countConstructors : NF vars -> Core (Maybe Nat)

387 |       countConstructors (NTCon _ tycName n args) =

388 |         if length args == n

389 |         then do defs <- get Ctxt

390 |                 Just gdef <- lookupCtxtExact tycName (gamma defs)

391 |                 | Nothing => pure Nothing

392 |                 let (TCon _ _ _ _ _ datacons _) = gdef.definition

393 |                 | _ => pure Nothing

394 |                 pure (length <$> datacons)

395 |         else pure Nothing

396 |       countConstructors _ = pure Nothing

398 |       dotTerm : RawImp -> RawImp

399 |       dotTerm tm

400 |           = case tm of

401 |                  IMustUnify {} => tm

402 |                  IBindVar {} => tm

403 |                  Implicit {} => tm

404 |                  IAs _ _ _ _ (IBindVar {}) => tm

405 |                  IAs _ _ _ _ (Implicit {}) => tm

406 |                  IAs fc nameFC p t arg => IAs fc nameFC p t (IMustUnify fc ErasedArg tm)

407 |                  _ => IMustUnify (getFC tm) ErasedArg tm

408 |   dotErased _ _ _ _ _ tm = pure tm

410 |   -- Check the rest of an application given the argument type and the

411 |   -- raw argument. We choose elaboration order depending on whether we know

412 |   -- the return type now. If we know it, elaborate the rest of the

413 |   -- application first and come back to it, because that might infer types

414 |   -- for implicit arguments, which might in turn help with type-directed

415 |   -- disambiguation when elaborating the argument.

416 |   checkRestApp : {vars : _} ->

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

418 |                  {auto m : Ref MD Metadata} ->

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

420 |                  {auto e : Ref EST (EState vars)} ->

421 |                  {auto s : Ref Syn SyntaxInfo} ->

422 |                  {auto o : Ref ROpts REPLOpts} ->

423 |                  RigCount -> RigCount -> ElabInfo ->

424 |                  NestedNames vars -> Env Term vars ->

425 |                  FC -> (fntm : Term vars) -> Name ->

426 |                  (aty : Closure vars) -> (sc : Defs -> Closure vars -> Core (NF vars)) ->

427 |                  (argdata : (Maybe Name, Nat)) ->

428 |                  (arg : RawImp) ->

429 |                  (expargs : List RawImp) ->

430 |                  (autoargs : List RawImp) ->

431 |                  (namedargs : List (Name, RawImp)) ->

432 |                  (knownret : Bool) ->

433 |                  (expected : Maybe (Glued vars)) ->

434 |                  Core (Term vars, Glued vars)

435 |   checkRestApp rig argRig elabinfo nest env fc tm x aty sc

436 |                (n, argpos) arg_in expargs autoargs namedargs knownret expty

437 |      = do defs <- get Ctxt

438 |           arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in

439 |           kr <- if knownret

440 |                    then pure True

441 |                    else do sc' <- sc defs (toClosure defaultOpts env (Erased fc Placeholder))

442 |                            concrete defs env sc'

443 |           -- In theory we can check the arguments in any order. But it turns

444 |           -- out that it's sometimes better to do the rightmost arguments

445 |           -- first to give ambiguity resolution more to work with. So

446 |           -- we do that if the target type is unknown, or if we see that

447 |           -- the raw term is otherwise worth delaying.

448 |           if (isHole !(evalClosure defs aty) && kr) || !(needsDelay (elabMode elabinfo) kr arg_in)

449 |              then handle (checkRtoL kr arg)

450 |                   -- if the type isn't resolved, we might encounter an

451 |                   -- implicit that we can't use yet because we don't know

452 |                   -- about it. In that case, revert to LtoR

453 |                     (\err => if invalidArg err

454 |                                 then checkLtoR kr arg

455 |                                 else throw err)

456 |              else checkLtoR kr arg

457 |     where

458 |       invalidArg : Error -> Bool

459 |       invalidArg (InvalidArgs {}) = True

460 |       invalidArg _ = False

462 |       checkRtoL : Bool -> -- return type is known

463 |                   RawImp -> -- argument currently being checked

464 |                   Core (Term vars, Glued vars)

465 |       checkRtoL kr arg

466 |         = do defs <- get Ctxt

467 |              nm <- genMVName x

468 |              empty <- clearDefs defs

469 |              metaty <- quote empty env aty

470 |              (idx, metaval) <- argVar (getFC arg) argRig env nm metaty

471 |              let fntm = App fc tm metaval

472 |              logTerm "elab" 10 "...as" metaval

473 |              fnty <- sc defs (toClosure defaultOpts env metaval)

474 |              (tm, gty) <- checkAppWith rig elabinfo nest env fc

475 |                                        fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

476 |              defs <- get Ctxt

477 |              aty' <- nf defs env metaty

478 |              logNF "elab" 10 ("Now trying " ++ show nm ++ " " ++ show arg) env aty'

480 |              -- On the LHS, checking an argument can't resolve its own type,

481 |              -- it must be resolved from elsewhere. Otherwise we might match

482 |              -- on things which are too specific for their polymorphic type.

483 |              when (onLHS (elabMode elabinfo)) $

484 |                 case aty' of

485 |                      NApp _ (NMeta _ i _) _ =>

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

487 |                                   | Nothing => pure ()

488 |                              when (isErased (multiplicity gdef)) $ addNoSolve i

489 |                      _ => pure ()

490 |              res <- check argRig ({ topLevel := False } elabinfo) nest env arg (Just $ glueBack defs env aty')

491 |              when (onLHS (elabMode elabinfo)) $

492 |                 case aty' of

493 |                      NApp _ (NMeta _ i _) _ => removeNoSolve i

494 |                      _ => pure ()

496 |              (argv, argt) <-

497 |                if not (onLHS (elabMode elabinfo))

498 |                  then pure res

499 |                  else do let (argv, argt) = res

500 |                          checkValidPattern rig env fc argv argt

502 |              defs <- get Ctxt

503 |              -- If we're on the LHS, reinstantiate it with 'argv' because it

504 |              -- *may* have as patterns in it and we need to retain them.

505 |              -- (As patterns are a bit of a hack but I don't yet see a

506 |              -- better way that leads to good code...)

507 |              logTerm "elab" 10 ("Solving " ++ show metaval ++ " with") argv

508 |              ok <- solveIfUndefined env metaval argv

509 |              -- If there's a constraint, make a constant, but otherwise

510 |              -- just return the term as expected

511 |              tm <- if not ok

512 |                       then do res <- convert fc elabinfo env

513 |                                                  (gnf env metaval)

514 |                                                  (gnf env argv)

515 |                               let [] = constraints res

516 |                                   | cs => do tmty <- getTerm gty

517 |                                              newConstant fc rig env tm tmty cs

518 |                               ignore $ updateSolution env metaval argv

519 |                               pure tm

520 |                       else pure tm

521 |              when (onLHS $ elabMode elabinfo) $

522 |                  -- reset hole and redo it with the unexpanded definition

523 |                  do updateDef (Resolved idx) (const (Just (Hole 0 (holeInit False))))

524 |                     ignore $ solveIfUndefined env metaval argv

525 |              -- Mark for reduction when we finish elaborating

526 |              updateDef (Resolved idx)

527 |                   (\def => case def of

528 |                         (PMDef pminfo args treeCT treeRT pats) =>

529 |                            Just (PMDef ({alwaysReduce := True} pminfo) args treeCT treeRT pats)

530 |                         _ => Nothing

531 |                         )

532 |              removeHole idx

533 |              pure (tm, gty)

535 |       checkLtoR : Bool -> -- return type is known

536 |                   RawImp -> -- argument currently being checked

537 |                   Core (Term vars, Glued vars)

538 |       checkLtoR kr arg

539 |         = do defs <- get Ctxt

540 |              logNF "elab" 10 ("Full function type") env

541 |                       (NBind fc x (Pi fc argRig Explicit aty) sc)

542 |              logC "elab" 10

543 |                      (do ety <- maybe (pure Nothing)

544 |                                      (\t => pure (Just !(toFullNames!(getTerm t))))

545 |                                      expty

546 |                          pure ("Overall expected type: " ++ show ety))

547 |              res <- check argRig ({ topLevel := False } elabinfo)

548 |                                    nest env arg (Just (glueClosure defs env aty))

549 |              (argv, argt) <-

550 |                if not (onLHS (elabMode elabinfo))

551 |                  then pure res

552 |                  else do let (argv, argt) = res

553 |                          checkValidPattern rig env fc argv argt

555 |              logGlueNF "elab" 10 "Got arg type" env argt

556 |              defs <- get Ctxt

557 |              let fntm = App fc tm argv

558 |              fnty <- sc defs (toClosure defaultOpts env argv)

559 |              checkAppWith rig elabinfo nest env fc

560 |                           fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

562 |   export

563 |   findNamed : Name -> List (Name, a) -> Maybe ((Name, a), List (Name, a))

564 |   findNamed n = findAndDeleteBy $ (== n) . fst

566 |   export

567 |   findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp

568 |   findBindAllExpPattern = lookup (UN Underscore)

570 |   isImplicitAs : RawImp -> Bool

571 |   isImplicitAs (IAs _ _ UseLeft _ (Implicit {})) = True

572 |   isImplicitAs _ = False

574 |   isBindAllExpPattern : Name -> Bool

575 |   isBindAllExpPattern (UN Underscore) = True

576 |   isBindAllExpPattern _ = False

578 |   -- Check an application of 'fntm', with type 'fnty' to the given list

579 |   -- of explicit and implicit arguments.

580 |   -- Returns the checked term and its (weakly) normalised type

581 |   checkAppWith' : {vars : _} ->

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

583 |                  {auto m : Ref MD Metadata} ->

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

585 |                  {auto e : Ref EST (EState vars)} ->

586 |                  {auto s : Ref Syn SyntaxInfo} ->

587 |                  {auto o : Ref ROpts REPLOpts} ->

588 |                  RigCount -> ElabInfo ->

589 |                  NestedNames vars -> Env Term vars ->

590 |                  FC -> (fntm : Term vars) -> (fnty : NF vars) ->

591 |                  (argdata : (Maybe Name, Nat)) ->

592 |                       -- function we're applying, and argument position, for

593 |                       -- checking if it's okay to erase against 'safeErase'

594 |                  (expargs : List RawImp) ->

595 |                  (autoargs : List RawImp) ->

596 |                  (namedargs : List (Name, RawImp)) ->

597 |                  (knownret : Bool) -> -- Do we know what the return type is yet?

598 |                               -- if we do, we might be able to use it to work

599 |                               -- out the types of arguments before elaborating them

600 |                  (expected : Maybe (Glued vars)) ->

601 |                  Core (Term vars, Glued vars)

602 |    -- Explicit Pi, we use provided unnamed explicit argument

603 |   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)

604 |                argdata (arg :: expargs') autoargs namedargs kr expty

605 |      = do let argRig = rig |*| rigb

606 |           checkRestApp rig argRig elabinfo nest env fc

607 |                        tm x aty sc argdata arg expargs' autoargs namedargs kr expty

608 |   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)

609 |                argdata [] autoargs namedargs kr expty with (findNamed x namedargs)

610 |    -- We found a compatible named argument

611 |    checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)

612 |                 argdata [] autoargs namedargs kr expty | Just ((_, arg), namedargs')

613 |     = do let argRig = rig |*| rigb

614 |          checkRestApp rig argRig elabinfo nest env fc

615 |                       tm x aty sc argdata arg [] autoargs namedargs' kr expty

616 |    checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)

617 |                 argdata [] autoargs namedargs kr expty | Nothing

618 |     = case findBindAllExpPattern namedargs of

619 |            Just arg => -- Bind-all-explicit pattern is present - implicitly bind

620 |              do let argRig = rig |*| rigb

621 |                 checkRestApp rig argRig elabinfo nest env fc

622 |                              tm x aty sc argdata arg [] autoargs namedargs kr expty

623 |            _ =>

624 |              do defs <- get Ctxt

625 |                 if all isImplicitAs (autoargs

626 |                                       ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))

627 |                                                                     -- Only non-user implicit `as` bindings added by

628 |                                                                     -- the compiler are allowed here

629 |                    then -- We are done

630 |                         checkExp rig elabinfo env fc tm (glueBack defs env ty) expty

631 |                    else -- Some user defined binding is present while we are out of explicit arguments, that's an error

632 |                         throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)

633 |   -- Function type is delayed:

634 |   --   RHS: force the term

635 |   --   LHS: strip off delay but only for explicit functions and disallow any further patterns

636 |   checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ i _) sc)) argdata expargs autoargs namedargs kr expty

637 |       = if onLHS (elabMode elabinfo)

638 |            then do when (isImplicit i) $ throw (LazyImplicitFunction fc)

639 |                    let ([], [], []) = (expargs, autoargs, namedargs)

640 |                        | _ => throw (LazyPatternVar fc)

641 |                    (tm, gfty) <- checkAppWith' rig elabinfo nest env fc tm ty argdata expargs autoargs namedargs kr expty

642 |                    fty <- getTerm gfty

643 |                    pure (tm, gnf env (TDelayed dfc r fty))

644 |            else checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty

645 |   -- If there's no more arguments given, and the plicities of the type and

646 |   -- the expected type line up, stop

647 |   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)

648 |                argdata [] [] [] kr (Just expty_in)

649 |       = do let argRig = rig |*| rigb

650 |            expty <- getNF expty_in

651 |            defs <- get Ctxt

652 |            case expty of

653 |                 NBind tfc' x' (Pi _ rigb' Implicit aty') sc'

654 |                    => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)

655 |                 _ => if not (preciseInf elabinfo)

656 |                         then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)

657 |                         -- in 'preciseInf' mode blunder on anyway, and hope

658 |                         -- that we can resolve the implicits

659 |                         else handle (checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in))

660 |                                (\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in))

661 |   -- Same for auto

662 |   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb AutoImplicit aty) sc)

663 |                argdata [] [] [] kr (Just expty_in)

664 |       = do let argRig = rig |*| rigb

665 |            expty <- getNF expty_in

666 |            defs <- get Ctxt

667 |            case expty of

668 |                 NBind tfc' x' (Pi _ rigb' AutoImplicit aty') sc'

669 |                    => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)

670 |                 _ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)

671 |   -- Same for default

672 |   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb (DefImplicit aval) aty) sc)

673 |                argdata [] [] [] kr (Just expty_in)

674 |       = do let argRig = rigMult rig rigb

675 |            expty <- getNF expty_in

676 |            defs <- get Ctxt

677 |            case expty of

678 |                 NBind tfc' x' (Pi _ rigb' (DefImplicit aval') aty') sc'

679 |                    => if !(convert defs env aval aval')

680 |                          then checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)

681 |                          else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)

682 |                 _ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)

684 |   -- Check next unnamed auto implicit argument

685 |   checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)

686 |                argdata expargs (arg :: autoargs') namedargs kr expty

687 |       = checkRestApp rig (rig |*| rigb) elabinfo nest env fc

688 |                          tm x aty sc argdata arg expargs autoargs' namedargs kr expty

689 |   -- Check next named auto implicit argument

690 |   checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)

691 |                argdata expargs [] namedargs kr expty

692 |       = let argRig = rig |*| rigb in

693 |             case findNamed x namedargs of

694 |                  Just ((_, arg), namedargs') =>

695 |                     checkRestApp rig argRig elabinfo nest env fc

696 |                                  tm x aty sc argdata arg expargs [] namedargs' kr expty

697 |                  Nothing =>

698 |                          makeAutoImplicit rig argRig elabinfo nest env fc tm

699 |                                               x aty sc argdata expargs [] namedargs kr expty

700 |   -- Check next implicit argument

701 |   checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Implicit aty) sc)

702 |                argdata expargs autoargs namedargs kr expty

703 |       = let argRig = rig |*| rigb in

704 |             case findNamed x namedargs of

705 |                Nothing => makeImplicit rig argRig elabinfo nest env fc tm

706 |                                        x aty sc argdata expargs autoargs namedargs kr expty

707 |                Just ((_, arg), namedargs') =>

708 |                      checkRestApp rig argRig elabinfo nest env fc

709 |                                   tm x aty sc argdata arg expargs autoargs namedargs' kr expty

710 |   -- Check next default argument

711 |   checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb (DefImplicit arg) aty) sc)

712 |                argdata expargs autoargs namedargs kr expty

713 |       = let argRig = rigMult rig rigb in

714 |             case findNamed x namedargs of

715 |                Nothing => makeDefImplicit rig argRig elabinfo nest env fc tm

716 |                                           x arg aty sc argdata expargs autoargs namedargs kr expty

717 |                Just ((_, arg), namedargs') =>

718 |                      checkRestApp rig argRig elabinfo nest env fc

719 |                                   tm x aty sc argdata arg expargs autoargs namedargs' kr expty

720 |   -- Invent a function type if we have extra explicit arguments but type is further unknown

721 |   checkAppWith' {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) autoargs namedargs kr expty

722 |       = -- Invent a function type,  and hope that we'll know enough to solve it

723 |         -- later when we unify with expty

724 |         do logNF "elab.with" 10 "Function type" env ty

725 |            logTerm "elab.with" 10 "Function " tm

726 |            argn <- genName "argTy"

727 |            retn <- genName "retTy"

728 |            u <- uniVar fc

729 |            argTy <- metaVar fc erased env argn (TType fc u)

730 |            let argTyG = gnf env argTy

731 |            retTy <- metaVar -- {vars = argn :: vars}

732 |                             fc erased env -- (Pi RigW Explicit argTy :: env)

733 |                             retn (TType fc u)

734 |            (argv, argt) <- check rig elabinfo

735 |                                  nest env arg (Just argTyG)

736 |            let fntm = App fc tm argv

737 |            defs <- get Ctxt

738 |            fnty <- nf defs env retTy -- (Bind fc argn (Let RigW argv argTy) retTy)

739 |            let expfnty = gnf env (Bind fc argn (Pi fc top Explicit argTy) (weaken retTy))

740 |            logGlue "elab.with" 10 "Expected function type" expfnty

741 |            whenJust expty (logGlue "elab.with" 10 "Expected result type")

742 |            res <- checkAppWith' rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

743 |            cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty

744 |            let [] = constraints cres

745 |               | cs => do cty <- getTerm expfnty

746 |                          ctm <- newConstant fc rig env (fst res) cty cs

747 |                          pure (ctm, gnf env retTy)

748 |            pure res

749 |   -- Only non-user implicit `as` bindings are allowed to be present as arguments at this stage

750 |   checkAppWith' rig elabinfo nest env fc tm ty argdata [] autoargs namedargs kr expty

751 |       = do defs <- get Ctxt

752 |            if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))

753 |               then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty

754 |               else throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)

756 |   ||| Entrypoint for checkAppWith: run the elaboration first and, if we're

759 |   checkAppWith : {vars : _} ->

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

761 |                  {auto m : Ref MD Metadata} ->

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

763 |                  {auto e : Ref EST (EState vars)} ->

764 |                  {auto s : Ref Syn SyntaxInfo} ->

765 |                  {auto o : Ref ROpts REPLOpts} ->

766 |                  RigCount -> ElabInfo ->

767 |                  NestedNames vars -> Env Term vars ->

768 |                  FC -> (fntm : Term vars) -> (fnty : NF vars) ->

769 |                  (argdata : (Maybe Name, Nat)) ->

770 |                       -- function we're applying, and argument position, for

771 |                       -- checking if it's okay to erase against 'safeErase'

772 |                  (expargs : List RawImp) ->

773 |                  (autoargs : List RawImp) ->

774 |                  (namedargs : List (Name, RawImp)) ->

775 |                  (knownret : Bool) -> -- Do we know what the return type is yet?

776 |                               -- if we do, we might be able to use it to work

777 |                               -- out the types of arguments before elaborating them

778 |                  (expected : Maybe (Glued vars)) ->

779 |                  Core (Term vars, Glued vars)

780 |   checkAppWith rig info nest env fc tm ty

781 |     argdata expargs autoargs namedargs knownret expected

782 |     = do res <- checkAppWith' rig info nest env fc tm ty

783 |                    argdata expargs autoargs namedargs knownret expected

784 |          let Just _ = isLHS (elabMode info)

785 |                | Nothing => pure res

786 |          let (Ref _ t _, args) = getFnArgs (fst res)

787 |                | _ => pure res

788 |          let Just a = isCon t

789 |                | _ => pure res

790 |          if a == length args

791 |            then pure res

792 |            else registerDot rig env fc UnderAppliedCon (fst res) (snd res)

795 | checkApp : {vars : _} ->

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

797 |            {auto m : Ref MD Metadata} ->

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

799 |            {auto e : Ref EST (EState vars)} ->

800 |            {auto s : Ref Syn SyntaxInfo} ->

801 |            {auto o : Ref ROpts REPLOpts} ->

802 |            RigCount -> ElabInfo ->

803 |            NestedNames vars -> Env Term vars ->

804 |            FC -> (fn : RawImp) ->

805 |            (expargs : List RawImp) ->

806 |            (autoargs : List RawImp) ->

807 |            (namedargs : List (Name, RawImp)) ->

808 |            Maybe (Glued vars) ->

809 |            Core (Term vars, Glued vars)

810 | checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs autoargs namedargs exp

811 |    = checkApp rig elabinfo nest env fc' fn (arg :: expargs) autoargs namedargs exp

812 | checkApp rig elabinfo nest env fc (IAutoApp fc' fn arg) expargs autoargs namedargs exp

813 |    = checkApp rig elabinfo nest env fc' fn expargs (arg :: autoargs) namedargs exp

814 | checkApp rig elabinfo nest env fc (INamedApp fc' fn nm arg) expargs autoargs namedargs exp

815 |    = checkApp rig elabinfo nest env fc' fn expargs autoargs ((nm, arg) :: namedargs) exp

816 | checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp

817 |    = do (ntm, arglen, nty_in) <- getVarType elabinfo.elabMode rig nest env fc' n

818 |         nty <- getNF nty_in

819 |         prims <- getPrimitiveNames

820 |         elabinfo <- updateElabInfo prims elabinfo.elabMode n expargs elabinfo

822 |         addNameLoc fc' n

824 |         logC "elab" 10

825 |                 (do defs <- get Ctxt

826 |                     fnty <- quote defs env nty

827 |                     exptyt <- maybe (pure Nothing)

828 |                                        (\t => do ety <- getTerm t

829 |                                                  etynf <- normaliseHoles defs env ety

830 |                                                  pure (Just !(toFullNames etynf)))

831 |                                        exp

832 |                     pure ("Checking application of " ++ show !(getFullName n) ++

833 |                           " (" ++ show n ++ ")" ++

834 |                           " to " ++ show expargs ++ "\n\tFunction type " ++

835 |                           (show !(toFullNames fnty)) ++ "\n\tExpected app type "

836 |                                 ++ show exptyt))

837 |         let fn = mapNestedName nest n

838 |         normalisePrims prims env

839 |            !(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs autoargs namedargs False exp)

840 |   where

842 |     -- If the term is an application of a primitive conversion (fromInteger etc)

843 |     -- and it's applied to a constant, fully normalise the term.

844 |     normalisePrims : {vs : _} ->

845 |                      List Name -> Env Term vs ->

846 |                      (Term vs, Glued vs) ->

847 |                      Core (Term vs, Glued vs)

848 |     normalisePrims prims env res

849 |         = do tm <- Normalise.normalisePrims (`boundSafe` elabMode elabinfo)

850 |                                             isIPrimVal

851 |                                             (onLHS (elabMode elabinfo))

852 |                                             prims n expargs (fst res) env

853 |              pure (fromMaybe (fst res) tm, snd res)

855 |       where

857 |         boundSafe : Constant -> ElabMode -> Bool

858 |         boundSafe _ (InLHS _) = True -- always need to expand on LHS

859 |         -- only do this for relatively small bounds.

860 |         -- Once it gets too big, we might be making the term

861 |         -- bigger than it would have been without evaluating!

862 |         boundSafe (BI x) _ = abs x < 100

863 |         boundSafe (Str str) _ = length str < 10

864 |         boundSafe _ _ = True

866 |     updateElabInfo : List Name -> ElabMode -> Name ->

867 |                      List RawImp -> ElabInfo -> Core ElabInfo

868 |     -- If it's a primitive function applied to a constant on the LHS, treat it

869 |     -- as an expression because we'll normalise the function away and match on

870 |     -- the result

871 |     updateElabInfo prims (InLHS _) n [IPrimVal fc c] elabinfo =

872 |         do if isPrimName prims !(getFullName n)

873 |               then pure ({ elabMode := InExpr } elabinfo)

874 |               else pure elabinfo

875 |     updateElabInfo _ _ _ _ info = pure info

877 | checkApp rig elabinfo nest env fc fn expargs autoargs namedargs exp

878 |    = do (fntm, fnty_in) <- checkImp rig elabinfo nest env fn Nothing

879 |         fnty <- getNF fnty_in

880 |         checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs autoargs namedargs False exp