0 | module TTImp.Elab.Check

  5 | import Core.Env

  6 | import Core.Metadata

  7 | import Core.Unify

  8 | import Core.Value

 10 | import Idris.REPL.Opts

 11 | import Idris.Syntax

 13 | import TTImp.TTImp

 15 | import Data.Either

 16 | import Libraries.Data.IntMap

 17 | import Libraries.Data.NameMap

 18 | import Libraries.Data.UserNameMap

 19 | import Libraries.Data.WithDefault

 21 | import Libraries.Data.List.SizeOf

 23 | import Libraries.Data.VarSet

 25 | %default covering

 27 | public export

 28 | data ElabMode = InType | InLHS RigCount | InExpr | InTransform

 31 | isLHS : ElabMode -> Maybe RigCount

 32 | isLHS (InLHS w) = Just w

 33 | isLHS _ = Nothing

 36 | Show ElabMode where

 37 |   show InType = "InType"

 38 |   show (InLHS c) = "InLHS " ++ show c

 39 |   show InExpr = "InExpr"

 40 |   show InTransform = "InTransform"

 42 | public export

 43 | data ElabOpt

 44 |   = HolesOkay

 45 |   | InCase

 46 |   | InPartialEval

 47 |   | InTrans

 49 | public export

 50 | Eq ElabOpt where

 51 |   HolesOkay == HolesOkay = True

 52 |   InCase == InCase = True

 53 |   InPartialEval == InPartialEval = True

 54 |   InTrans == InTrans = True

 55 |   _ == _ = False

 59 | public export

 60 | data ImplBinding : Scope -> Type where

 61 |      NameBinding : {vars : _} ->

 62 |                    FC -> RigCount -> PiInfo (Term vars) ->

 63 |                    (elabAs : Term vars) -> (expTy : Term vars) ->

 64 |                    ImplBinding vars

 65 |      AsBinding : {vars : _} ->

 66 |                  RigCount -> PiInfo (Term vars) -> (elabAs : Term vars) -> (expTy : Term vars) ->

 67 |                  (pat : Term vars) ->

 68 |                  ImplBinding vars

 72 | Show (ImplBinding vars) where

 73 |   show (NameBinding _ c p tm ty) = show (tm, ty)

 74 |   show (AsBinding c p tm ty pat) = show (tm, ty) ++ "@" ++ show tm

 77 | bindingMetas : ImplBinding vars -> NameMap Bool

 78 | bindingMetas (NameBinding _ c p tm ty) = getMetas ty

 79 | bindingMetas (AsBinding c p tm ty pat)

 80 |     = insertAll (toList (getMetas ty)) (getMetas pat)

 81 |   where

 82 |     insertAll : List (Name, Bool) -> NameMap Bool -> NameMap Bool

 83 |     insertAll [] ns = ns

 84 |     insertAll ((k, v) :: ks) ns = insert k v (insertAll ks ns)

 88 | bindingType : ImplBinding vars -> Term vars

 89 | bindingType (NameBinding _ _ _ _ ty) = ty

 90 | bindingType (AsBinding _ _ _ ty _) = ty

 95 | bindingTerm : ImplBinding vars -> Term vars

 96 | bindingTerm (NameBinding _ _ _ tm _) = tm

 97 | bindingTerm (AsBinding _ _ tm _ _) = tm

100 | bindingRig : ImplBinding vars -> RigCount

101 | bindingRig (NameBinding _ c _ _ _) = c

102 | bindingRig (AsBinding c _ _ _ _) = c

105 | bindingPiInfo : ImplBinding vars -> PiInfo (Term vars)

106 | bindingPiInfo (NameBinding _ _ p _ _) = p

107 | bindingPiInfo (AsBinding _ p _ _ _) = p

110 | public export

111 | record EState (vars : Scope) where

112 |   constructor MkEState

113 |   {outer : Scope}

114 |   -- The function/constructor name we're currently working on (resolved id)

115 |   defining : Int

116 |   -- The outer environment in which we're running the elaborator. Things here should

117 |   -- be considered parametric as far as case expression elaboration goes, and are

118 |   -- the only things that unbound implicits can depend on

119 |   outerEnv : Env Term outer

120 |   subEnv : Thin outer vars

121 |   boundNames : List (Name, ImplBinding vars)

122 |                   -- implicit pattern/type variable bindings and the

123 |                   -- term/type they elaborated to

124 |   toBind : List (Name, ImplBinding vars)

125 |                   -- implicit pattern/type variables which haven't been

126 |                   -- bound yet. Record how they're bound (auto-implicit bound

127 |                   -- pattern vars need to be dealt with in with-application on

128 |                   -- the RHS)

129 |   bindIfUnsolved : List (Name, FC, RigCount,

130 |                           (vars' ** (Env Term vars', PiInfo (Term vars'),

131 |                                      Term vars', Term vars', Thin outer vars')))

132 |                   -- names to add as unbound implicits if they are still holes

133 |                   -- when unbound implicits are added

134 |   lhsPatVars : List Name

135 |                   -- names which we've bound in elab mode InLHS (i.e. not

136 |                   -- in a dot pattern). We keep track of this because every

137 |                   -- occurrence other than the first needs to be dotted

138 |   allPatVars : List Name

139 |                   -- Holes standing for pattern variables, which we'll delete

140 |                   -- once we're done elaborating

141 |   polyMetavars : List (FC, Env Term vars, Term vars, Term vars)

142 |                   -- Metavars which need to be a polymorphic type at the end

143 |                   -- of elaboration. If they aren't, it means we're trying to

144 |                   -- pattern match on a type that we don't have available.

145 |   delayDepth : Nat -- if it gets too deep, it gets slow, so fail quicker

146 |   linearUsed : VarSet vars

147 |   saveHoles : NameMap () -- things we'll need to save to TTC, even if solved

149 |   unambiguousNames : UserNameMap (Name, Int, GlobalDef)

150 |                   -- Mapping from userNameRoot to fully resolved names.

151 |                   -- For names in this mapping, we don't run disambiguation.

152 |                   -- Used in with-expressions.

155 | data EST : Type where

158 | initEStateSub : {outer : _} ->

159 |                 Int -> Env Term outer -> Thin outer vars -> EState vars

160 | initEStateSub n env sub = MkEState

161 |     { defining = n

162 |     , outerEnv = env

163 |     , subEnv = sub

164 |     , boundNames = []

165 |     , toBind = []

166 |     , bindIfUnsolved = []

167 |     , lhsPatVars = []

168 |     , allPatVars = []

169 |     , polyMetavars = []

170 |     , delayDepth = Z

171 |     , linearUsed = VarSet.empty

172 |     , saveHoles = empty

173 |     , unambiguousNames = empty

174 |     }

177 | initEState : {vars : _} ->

178 |              Int -> Env Term vars -> EState vars

179 | initEState n env = initEStateSub n env Refl

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

183 |            Name -> Core ()

184 | saveHole n = update EST { saveHoles $= insert n () }

186 | weakenedEState : {n, vars : _} ->

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

188 |                  Core (Ref EST (EState (n :: vars)))

189 | weakenedEState {e}

190 |     = do est <- get EST

191 |          eref <- newRef EST $

192 |                    { subEnv $= Drop

193 |                    , boundNames $= map wknTms

194 |                    , toBind $= map wknTms

195 |                    , linearUsed $= weaken {tm = VarSet}

196 |                    , polyMetavars := [] -- no binders on LHS

197 |                    } est

198 |          pure eref

199 |   where

200 |     wknTms : (Name, ImplBinding vs) ->

201 |              (Name, ImplBinding (n :: vs))

202 |     wknTms (f, NameBinding fc c p x y)

203 |         = (f, NameBinding fc c (map weaken p) (weaken x) (weaken y))

204 |     wknTms (f, AsBinding c p x y z)

205 |         = (f, AsBinding c (map weaken p) (weaken x) (weaken y) (weaken z))

207 | strengthenedEState : {n, vars : _} ->

208 |                      Ref Ctxt Defs ->

209 |                      Ref EST (EState (n :: vars)) ->

210 |                      FC -> Env Term (n :: vars) ->

211 |                      Core (EState vars)

212 | strengthenedEState {n} {vars} c e fc env

213 |     = do est <- get EST

214 |          defs <- get Ctxt

215 |          svs <- dropSub (subEnv est)

216 |          bns <- traverse (strTms defs) (boundNames est)

217 |          todo <- traverse (strTms defs) (toBind est)

218 |          pure $ { subEnv := svs

219 |                 , boundNames := bns

220 |                 , toBind := todo

221 |                 , linearUsed $= VarSet.dropFirst

222 |                 , polyMetavars := [] -- no binders on LHS

223 |                 } est

225 |   where

226 |     dropSub : Thin xs (y :: ys) -> Core (Thin xs ys)

227 |     dropSub (Drop sub) = pure sub

228 |     dropSub _ = throw (InternalError "Badly formed weakened environment")

230 |     -- Remove any instance of the top level local variable from an

231 |     -- application. Fail if it turns out to be necessary.

232 |     -- NOTE: While this isn't strictly correct given the type of the hole

233 |     -- which stands for the unbound implicits, it's harmless because we

234 |     -- never actualy *use* that hole - this process is only to ensure that the

235 |     -- unbound implicit doesn't depend on any variables it doesn't have

236 |     -- in scope.

237 |     removeArgVars : List (Term (n :: vs)) -> Maybe (List (Term vs))

238 |     removeArgVars [] = pure []

239 |     removeArgVars (Local fc r (S k) p :: args)

240 |         = do args' <- removeArgVars args

241 |              pure (Local fc r _ (dropLater p) :: args')

242 |     removeArgVars (Local fc r Z p :: args)

243 |         = removeArgVars args

244 |     removeArgVars (a :: args)

245 |         = do a' <- shrink a (Drop Refl)

246 |              args' <- removeArgVars args

247 |              pure (a' :: args')

249 |     removeArg : Term (n :: vs) -> Maybe (Term vs)

250 |     removeArg tm

251 |         = case getFnArgs tm of

252 |                (f, args) =>

253 |                    do args' <- removeArgVars args

254 |                       f' <- shrink f (Drop Refl)

255 |                       pure (apply (getLoc f) f' args')

257 |     strTms : Defs -> (Name, ImplBinding (n :: vars)) ->

258 |              Core (Name, ImplBinding vars)

259 |     strTms defs (f, NameBinding fc c p x y)

260 |         = do xnf <- normaliseHoles defs env x

261 |              ynf <- normaliseHoles defs env y

262 |              case (shrinkPi p (Drop Refl),

263 |                    removeArg xnf,

264 |                    shrink ynf (Drop Refl)) of

265 |                (Just p', Just x', Just y') =>

266 |                     pure (f, NameBinding fc c p' x' y')

267 |                _ => throw (BadUnboundImplicit fc env f y)

268 |     strTms defs (f, AsBinding c p x y z)

269 |         = do xnf <- normaliseHoles defs env x

270 |              ynf <- normaliseHoles defs env y

271 |              znf <- normaliseHoles defs env z

272 |              case (shrinkPi p (Drop Refl),

273 |                    shrink xnf (Drop Refl),

274 |                    shrink ynf (Drop Refl),

275 |                    shrink znf (Drop Refl)) of

276 |                (Just p', Just x', Just y', Just z') =>

277 |                     pure (f, AsBinding c p' x' y' z')

278 |                _ => throw (BadUnboundImplicit fc env f y)

281 | inScope : {n, vars : _} ->

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

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

284 |           FC -> Env Term (n :: vars) ->

285 |           (Ref EST (EState (n :: vars)) -> Core a) ->

286 |           Core a

287 | inScope {c} {e} fc env elab

288 |     = do e' <- weakenedEState

289 |          res <- elab e'

290 |          st' <- strengthenedEState c e' fc env

291 |          put {ref=e} EST st'

292 |          pure res

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

296 |              FC -> Env Term vars ->

297 |              Term vars -> Term vars -> Core ()

298 | mustBePoly fc env tm ty = update EST { polyMetavars $= ((fc, env, tm, ty) :: ) }

304 | concrete : Defs -> Env Term vars -> NF vars -> Core Bool

305 | concrete defs env (NBind fc _ (Pi {}) sc)

306 |     = do sc' <- sc defs (toClosure defaultOpts env (Erased fc Placeholder))

307 |          concrete defs env sc'

308 | concrete defs env (NDCon {}) = pure True

309 | concrete defs env (NTCon {}) = pure True

310 | concrete defs env (NPrimVal {}) = pure True

311 | concrete defs env (NType {}) = pure True

312 | concrete defs env _ = pure False

315 | updateEnv : {new : _} ->

316 |             Env Term new -> Thin new vars ->

317 |             List (Name, FC, RigCount,

318 |                    (vars' ** (Env Term vars', PiInfo (Term vars'),

319 |                               Term vars', Term vars', Thin new vars'))) ->

320 |             EState vars -> EState vars

321 | updateEnv env sub bif st

322 |     = { outerEnv := env

323 |       , subEnv := sub

324 |       , bindIfUnsolved := bif

325 |       } st

328 | addBindIfUnsolved : {vars : _} ->

329 |                     Name -> FC -> RigCount -> PiInfo (Term vars) ->

330 |                     Env Term vars -> Term vars -> Term vars ->

331 |                     EState vars -> EState vars

332 | addBindIfUnsolved hn fc r p env tm ty st

333 |     = { bindIfUnsolved $=

334 |          ((hn, fc, r, (_ ** (env, p, tm, ty, subEnv st))) ::)} st

336 | clearBindIfUnsolved : EState vars -> EState vars

337 | clearBindIfUnsolved = { bindIfUnsolved := [] }

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

342 |               (excepts : List Name) -> Core ()

343 | clearToBind excepts =

344 |   update EST $ { toBind $= filter (\x => fst x `elem` excepts) } . clearBindIfUnsolved

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

348 |                 ElabMode -> Name -> Core ()

349 | noteLHSPatVar (InLHS _) n = update EST { lhsPatVars $= (n ::) }

350 | noteLHSPatVar _         _ = pure ()

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

354 |              Name -> Core ()

355 | notePatVar n = update EST { allPatVars $= (n ::) }

358 | metaVar : {vars : _} ->

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

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

361 |           FC -> RigCount ->

362 |           Env Term vars -> Name -> Term vars -> Core (Term vars)

363 | metaVar fc rig env n ty

364 |     = do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit False)) True

365 |          pure tm

368 | implBindVar : {vars : _} ->

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

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

371 |               FC -> RigCount ->

372 |               Env Term vars -> Name -> Term vars -> Core (Term vars)

373 | implBindVar fc rig env n ty

374 |     = do (_, tm) <- newMeta fc rig env n ty (Hole (length env) (holeInit True)) True

375 |          pure tm

378 | metaVarI : {vars : _} ->

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

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

381 |            FC -> RigCount ->

382 |            Env Term vars -> Name -> Term vars -> Core (Int, Term vars)

383 | metaVarI fc rig env n ty

384 |     = do defs <- get Ctxt

385 |          tynf <- nf defs env ty

386 |          let hinf = case tynf of

387 |                          NApp _ (NMeta {}) _ =>

388 |                               { precisetype := True } (holeInit False)

389 |                          _ => holeInit False

390 |          newMeta fc rig env n ty (Hole (length env) hinf) True

393 | argVar : {vars : _} ->

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

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

396 |          FC -> RigCount ->

397 |          Env Term vars -> Name -> Term vars -> Core (Int, Term vars)

398 | argVar fc rig env n ty

399 |     = newMetaLets fc rig env n ty (Hole (length env) (holeInit False)) False True

402 | uniVar : {auto c : Ref Ctxt Defs} ->

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

404 |          FC -> Core Name

405 | uniVar fc

406 |     = do n <- genName "u"

407 |          idx <- addDef n (newDef fc n erased Scope.empty (Erased fc Placeholder) (specified Public) None)

408 |          pure (Resolved idx)

411 | searchVar : {vars : _} ->

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

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

414 |             FC -> RigCount -> Nat -> Name ->

415 |             Env Term vars -> NestedNames vars -> Name -> Term vars -> Core (Term vars)

416 | searchVar fc rig depth def env nest n ty

417 |     = do defs <- get Ctxt

418 |          (vars' ** (bind, env')) <- envHints (keys (localHints defs)) env

419 |          -- Initial the search with an environment which binds the applied

420 |          -- local hints

421 |          (_, tm) <- newSearch fc rig depth def env' n

422 |                               (weakenNs (mkSizeOf vars') ty)

423 |          pure (bind tm)

424 |   where

425 |     useVars : {vars : _} ->

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

427 |     useVars [] sc = sc

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

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

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

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

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

434 |     find : Name -> List (Name, (Maybe Name, b)) -> Maybe (Maybe Name, b)

435 |     find x [] = Nothing

436 |     find x ((n, t) :: xs)

437 |        = if x == n

438 |             then Just t

439 |             else case t of

440 |                       (Nothing, _) => find x xs

441 |                       (Just n', _) => if x == n'

442 |                                          then Just t

443 |                                          else find x xs

445 |     envHints : List Name -> Env Term vars ->

446 |                Core (vars' ** (Term (vars' ++ vars) -> Term vars, Env Term (vars' ++ vars)))

447 |     envHints [] env = pure (Scope.empty ** (id, env))

448 |     envHints (n :: ns) env

449 |         = do (vs ** (f, env')) <- envHints ns env

450 |              let Just (nestn, argns, tmf) = find !(toFullNames n) (names nest)

451 |                  | Nothing => pure (vs ** (f, env'))

452 |              let n' = maybe n id nestn

453 |              defs <- get Ctxt

454 |              Just ndef <- lookupCtxtExact n' (gamma defs)

455 |                  | Nothing => pure (vs ** (f, env'))

456 |              let nt = getDefNameType ndef

457 |              let app = tmf fc nt

458 |              let tyenv = useVars (getArgs app) (embed (type ndef))

459 |              let binder = Let fc top (weakenNs (mkSizeOf vs) app)

460 |                                      (weakenNs (mkSizeOf vs) tyenv)

461 |              varn <- toFullNames n'

462 |              pure ((varn :: vs) **

463 |                     (\t => f (Bind fc varn binder t),

464 |                        binder :: env'))

467 | public export

468 | record ElabInfo where

469 |   constructor MkElabInfo

470 |   elabMode : ElabMode

471 |   implicitMode : BindMode

472 |   topLevel : Bool

473 |   bindingVars : Bool

474 |   preciseInf : Bool -- are types inferred precisely (True) or do we generalise

475 |                     -- pi bindings to RigW (False, default)

476 |   ambigTries : List Name

479 | initElabInfo : ElabMode -> ElabInfo

480 | initElabInfo m = MkElabInfo m NONE False True False []

483 | tryError : {vars : _} ->

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

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

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

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

488 |            Core a -> Core (Either Error a)

489 | tryError elab

490 |     = do ust <- get UST

491 |          est <- get EST

492 |          md <- get MD

493 |          defs <- branch

494 |          catch (do res <- elab

495 |                    commit

496 |                    pure (Right res))

497 |                (\err => do put UST ust

498 |                            put EST est

499 |                            put MD md

500 |                            defs' <- get Ctxt

501 |                            put Ctxt ({ timings := timings defs' } defs)

502 |                            pure (Left err))

505 | try : {vars : _} ->

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

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

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

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

510 |       Core a -> Core a -> Core a

511 | try elab1 elab2

512 |     = do Right ok <- tryError elab1

513 |                | Left err => elab2

514 |          pure ok

517 | handle : {vars : _} ->

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

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

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

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

522 |          Core a -> (Error -> Core a) -> Core a

523 | handle elab1 elab2

524 |     = do Right ok <- tryError elab1

525 |                | Left err => elab2 err

526 |          pure ok

528 | successful : {vars : _} ->

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

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

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

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

533 |              Bool -> -- constraints allowed

534 |              List (Maybe Name, Core a) ->

535 |              Core (List (Either (Maybe Name, Error)

536 |                                 (Nat, a, Defs, UState, EState vars, Metadata)))

537 | successful allowCons [] = pure []

538 | successful allowCons ((tm, elab) :: elabs)

539 |     = do ust <- get UST

540 |          let ncons = if allowCons

541 |                         then 0

542 |                         else length (toList (guesses ust))

543 |          est <- get EST

544 |          md <- get MD

545 |          defs <- branch

546 |          catch (do -- Run the elaborator

547 |                    logC "elab" 5 $

548 |                             do tm' <- maybe (pure (UN $ Basic "__"))

549 |                                              toFullNames tm

550 |                                pure ("Running " ++ show tm')

551 |                    res <- elab

552 |                    -- Record post-elaborator state

553 |                    ust' <- get UST

554 |                    let ncons' = if allowCons

555 |                                    then 0

556 |                                    else length (toList (guesses ust'))

558 |                    est' <- get EST

559 |                    md' <- get MD

560 |                    defs' <- get Ctxt

562 |                    -- Reset to previous state and try the rest

563 |                    put UST ust

564 |                    put EST est

565 |                    put MD md

566 |                    put Ctxt defs

567 |                    logC "elab" 5 $

568 |                             do tm' <- maybe (pure (UN $ Basic "__"))

569 |                                             toFullNames tm

570 |                                pure ("Success " ++ show tm' ++

571 |                                      " (" ++ show ncons' ++ " - "

572 |                                           ++ show ncons ++ ")")

573 |                    elabs' <- successful allowCons elabs

574 |                    -- Record success, and the state we ended at

575 |                    pure (Right (minus ncons' ncons,

576 |                                 res, defs', ust', est', md') :: elabs'))

577 |                (\err => do put UST ust

578 |                            put EST est

579 |                            put MD md

580 |                            put Ctxt defs

581 |                            when (abandon err) $ throw err

582 |                            elabs' <- successful allowCons elabs

583 |                            pure (Left (tm, err) :: elabs'))

584 |   where

585 |     -- Some errors, it's not worth trying all the possibilities because

586 |     -- something serious has gone wrong, so just give up immediately.

587 |     abandon : Error -> Bool

588 |     abandon (UndefinedName {}) = True

589 |     abandon (InType _ _ err) = abandon err

590 |     abandon (InCon _ err) = abandon err

591 |     abandon (InLHS _ _ err) = abandon err

592 |     abandon (InRHS _ _ err) = abandon err

593 |     abandon (AllFailed errs) = any (abandon . snd) errs

594 |     abandon _ = False

597 | exactlyOne' : {vars : _} ->

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

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

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

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

602 |               Bool -> FC -> Env Term vars ->

603 |               List (Maybe Name, Core (Term vars, Glued vars)) ->

604 |               Core (Term vars, Glued vars)

605 | exactlyOne' allowCons fc env [(tm, elab)] = elab

606 | exactlyOne' {vars} allowCons fc env all

607 |     = do elabs <- successful allowCons all

608 |          case getRight elabs of

609 |               Right (res, defs, ust, est, md) =>

610 |                     do put UST ust

611 |                        put EST est

612 |                        put MD  md

613 |                        put Ctxt defs

614 |                        commit

615 |                        pure res

616 |               Left rs => throw (altError (lefts elabs) rs)

617 |   where

618 |     getRight : List (Either err (Nat, res)) -> Either (List res) res

619 |     getRight es

620 |         = case rights es of

621 |                [(_, res)] => Right res

622 |                rs => case filter (\x => fst x == Z) rs of

623 |                           [(_, res)] => Right res

624 |                           _ => Left (map snd rs)

626 |     getRes : ((Term vars, Glued vars), Defs, st) -> (Context, Term vars)

627 |     getRes ((tm, _), defs, thisst) = (gamma defs, tm)

629 |     getDepthError : Error -> Maybe Error

630 |     getDepthError e@(AmbiguityTooDeep {}) = Just e

631 |     getDepthError _ = Nothing

633 |     depthError : List (Maybe Name, Error) -> Maybe Error

634 |     depthError [] = Nothing

635 |     depthError ((_, e) :: es)

636 |         = maybe (depthError es) Just (getDepthError e)

638 |     -- If they've all failed, collect all the errors

639 |     -- If more than one succeeded, report the ambiguity

640 |     altError : List (Maybe Name, Error) ->

641 |                List ((Term vars, Glued vars), Defs, st) ->

642 |                Error

643 |     altError ls []

644 |         = case depthError ls of

645 |                Nothing => AllFailed ls

646 |                Just err => err

647 |     altError ls rs = AmbiguousElab fc env (map getRes rs)

650 | exactlyOne : {vars : _} ->

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

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

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

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

655 |              FC -> Env Term vars ->

656 |              List (Maybe Name, Core (Term vars, Glued vars)) ->

657 |              Core (Term vars, Glued vars)

658 | exactlyOne = exactlyOne' True

661 | anyOne : {vars : _} ->

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

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

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

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

666 |          FC -> List (Maybe Name, Core (Term vars, Glued vars)) ->

667 |          Core (Term vars, Glued vars)

668 | anyOne fc es = anyOneErrs es [<] where

669 |   anyOneErrs : List (Maybe Name, Core a) -> SnocList (Maybe Name, Error) -> Core a

670 |   anyOneErrs [] [<]        = throw $ GenericMsg fc "No elaborators provided"

671 |   anyOneErrs [] [<(tm, e)] = throw e

672 |   anyOneErrs [] errs       = throw $ AllFailed $ errs <>> []

673 |   anyOneErrs ((tm, elab) :: es) errs = case !(tryError elab) of

674 |     Right res => pure res

675 |     Left err  => anyOneErrs es $ errs :< (tm, err)

680 | check : {vars : _} ->

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

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

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

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

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

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

687 |         RigCount -> ElabInfo ->

688 |         NestedNames vars -> Env Term vars -> RawImp ->

689 |         Maybe (Glued vars) ->

690 |         Core (Term vars, Glued vars)

694 | checkImp : {vars : _} ->

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

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

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

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

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

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

701 |            RigCount -> ElabInfo ->

702 |            NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) ->

703 |            Core (Term vars, Glued vars)

707 | processDecl : {vars : _} ->

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

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

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

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

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

713 |               List ElabOpt -> NestedNames vars ->

714 |               Env Term vars -> ImpDecl -> Core ()

721 |         : {vars : _} ->

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

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

724 |           (withLazy : Bool) ->

725 |           FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->

726 |           Core UnifyResult

727 | convertWithLazy withLazy fc elabinfo env x y

728 |     = let umode : UnifyInfo

729 |                 = case elabMode elabinfo of

730 |                        InLHS _ => inLHS

731 |                        _ => inTerm in

732 |           catch

733 |             (do let lazy = !isLazyActive && withLazy

734 |                 logGlueNF "elab.unify" 5 ("Unifying " ++ show withLazy ++ " "

735 |                              ++ show (elabMode elabinfo)) env x

736 |                 logGlueNF "elab.unify" 5 "....with" env y

737 |                 vs <- if isFromTerm x && isFromTerm y

738 |                          then do xtm <- getTerm x

739 |                                  ytm <- getTerm y

740 |                                  if lazy

741 |                                     then unifyWithLazy umode fc env xtm ytm

742 |                                     else unify umode fc env xtm ytm

743 |                          else do xnf <- getNF x

744 |                                  ynf <- getNF y

745 |                                  if lazy

746 |                                     then unifyWithLazy umode fc env xnf ynf

747 |                                     else unify umode fc env xnf ynf

748 |                 when (holesSolved vs) $

749 |                     solveConstraints umode Normal

750 |                 pure vs)

751 |             (\err =>

752 |                do xtm <- getTerm x

753 |                   ytm <- getTerm y

754 |                   -- See if we can improve the error message by

755 |                   -- resolving any more constraints

756 |                   catch (solveConstraints umode Normal)

757 |                         (\err => pure ())

758 |                   -- We need to normalise the known holes before

759 |                   -- throwing because they may no longer be known

760 |                   -- by the time we look at the error

761 |                   defs <- get Ctxt

762 |                   throw (WhenUnifying fc (gamma defs) env xtm ytm err))

765 | convert : {vars : _} ->

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

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

768 |           FC -> ElabInfo -> Env Term vars -> Glued vars -> Glued vars ->

769 |           Core UnifyResult

770 | convert = convertWithLazy False

778 | checkExp : {vars : _} ->

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

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

781 |            RigCount -> ElabInfo -> Env Term vars -> FC ->

782 |            (term : Term vars) ->

783 |            (got : Glued vars) -> (expected : Maybe (Glued vars)) ->

784 |            Core (Term vars, Glued vars)

785 | checkExp rig elabinfo env fc tm got (Just exp)

786 |     = do vs <- convertWithLazy True fc elabinfo env got exp

787 |          case (constraints vs) of

788 |               [] => case addLazy vs of

789 |                          NoLazy => do logTerm "elab" 5 "Solved" tm

790 |                                       pure (tm, got)

791 |                          AddForce r => do logTerm "elab" 5 "Force" tm

792 |                                           logGlue "elab" 5 "Got" got

793 |                                           logGlue "elab" 5 "Exp" exp

794 |                                           pure (TForce fc r tm, exp)

795 |                          AddDelay r => do ty <- getTerm got

796 |                                           logTerm "elab" 5 "Delay" tm

797 |                                           pure (TDelay fc r ty tm, exp)

798 |               cs => do logTerm "elab" 5 "Not solved" tm

799 |                        defs <- get Ctxt

800 |                        empty <- clearDefs defs

801 |                        cty <- getTerm exp

802 |                        ctm <- newConstant fc rig env tm cty cs

803 |                        dumpConstraints "elab" 5 False

804 |                        case addLazy vs of

805 |                             NoLazy => pure (ctm, got)

806 |                             AddForce r => pure (TForce fc r tm, exp)

807 |                             AddDelay r => do ty <- getTerm got

808 |                                              pure (TDelay fc r ty tm, exp)

809 | checkExp rig elabinfo env fc tm got Nothing = pure (tm, got)