1 | module Core.UnifyState

  3 | import Core.Context.Log

  4 | import Core.Env

  5 | import Core.Normalise

  6 | import Core.Value

  8 | import Libraries.Data.IntMap

  9 | import Libraries.Data.NameMap

 10 | import Libraries.Data.WithDefault

 12 | import Libraries.Data.SnocList.HasLength

 14 | %default covering

 16 | public export

 17 | data Constraint : Type where

 18 |      -- An unsolved constraint, noting two terms which need to be convertible

 19 |      -- in a particular environment

 20 |      MkConstraint : {vars : _} ->

 21 |                     FC ->

 22 |                     (withLazy : Bool) ->

 23 |                     (env : Env Term vars) ->

 24 |                     (x : NF vars) -> (y : NF vars) ->

 25 |                     Constraint

 26 |      -- A resolved constraint

 27 |      Resolved : Constraint

 33 | public export

 34 | data PolyConstraint : Type where

 35 |      MkPolyConstraint : {vars : _} ->

 36 |                         FC -> Env Term vars ->

 37 |                         (arg : Term vars) ->

 38 |                         (expty : NF vars) ->

 39 |                         (argty : NF vars) -> PolyConstraint

 46 | public export

 47 | data DelayReason

 48 |       = CaseBlock

 49 |       | Ambiguity

 50 |       | RecordUpdate

 51 |       | Rewrite

 52 |       | LazyDelay

 54 | public export

 55 | Eq DelayReason where

 56 |   CaseBlock == CaseBlock = True

 57 |   Ambiguity == Ambiguity = True

 58 |   RecordUpdate == RecordUpdate = True

 59 |   Rewrite == Rewrite = True

 60 |   LazyDelay == LazyDelay = True

 61 |   _ == _ = False

 63 | public export

 64 | Ord DelayReason where

 65 |   compare x y = compare (tag x) (tag y)

 66 |     where

 67 |       -- The ordering here is chosen to give the most likely useful error

 68 |       -- messages first. For example, often the real reason for a strange error

 69 |       -- is because there's an ambiguity that can't be resolved.

 70 |       tag : DelayReason -> Int

 71 |       tag CaseBlock = 1 -- we can often proceed even if there's still some

 72 |                         -- ambiguity

 73 |       tag Ambiguity = 2

 74 |       tag LazyDelay = 3

 75 |       tag RecordUpdate = 4

 76 |       tag Rewrite = 5

 78 | public export

 79 | record UState where

 80 |   constructor MkUState

 81 |   holes : IntMap (FC, Name) -- All metavariables with no definition yet.

 82 |                             -- 'Int' is the 'Resolved' name

 83 |   guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved

 84 |                               -- (also includes auto implicit searches)

 85 |   currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session

 86 |   delayedHoles : IntMap (FC, Name) -- Holes left unsolved after an elaboration,

 87 |                                    -- so we need to check again at the end whether

 88 |                                    -- they have been solved later. Doesn't include

 89 |                                    -- user defined hole names, which don't need

 90 |                                    -- to have been solved

 91 |   constraints : IntMap Constraint -- map for finding constraints by ID

 92 |   noSolve : IntMap () -- Names not to solve

 93 |                       -- If we're checking an LHS, then checking an argument can't

 94 |                       -- solve its own type, or we might end up with something

 95 |                       -- less polymorphic than it should be

 96 |   polyConstraints : List PolyConstraint -- constraints which need to be solved

 97 |                       -- successfully to check an LHS is polymorphic enough

 98 |   dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints

 99 |   nextName : Int

100 |   nextConstraint : Int

101 |   delayedElab : List (DelayReason, Int, NameMap (), Core ClosedTerm)

102 |                 -- Elaborators which we need to try again later, because

103 |                 -- we didn't have enough type information to elaborate

104 |                 -- successfully yet.

105 |                 -- The 'Int' is the resolved name.

106 |                 -- NameMap () is the set of local hints at the point of delay

107 |   logging : Bool

110 | initUState : UState

111 | initUState = MkUState

112 |   { holes = empty

113 |   , guesses = empty

114 |   , currentHoles = empty

115 |   , delayedHoles = empty

116 |   , constraints = empty

117 |   , noSolve = empty

118 |   , polyConstraints = []

119 |   , dotConstraints = []

120 |   , nextName = 0

121 |   , nextConstraint = 0

122 |   , delayedElab = []

123 |   , logging = False

124 |   }

127 | data UST : Type where

130 | resetNextVar : {auto u : Ref UST UState} ->

131 |                Core ()

132 | resetNextVar = update UST { nextName := 0 }

136 | genName : {auto c : Ref Ctxt Defs} ->

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

138 |           String -> Core Name

139 | genName str

140 |     = do ust <- get UST

141 |          put UST ({ nextName $= (+1) } ust)

142 |          n <- inCurrentNS (MN str (nextName ust))

143 |          pure n

147 | genMVName : {auto c : Ref Ctxt Defs} ->

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

149 |             Name -> Core Name

150 | genMVName (UN str) = genName (displayUserName str)

151 | genMVName (MN str _) = genName str

152 | genMVName n

153 |     = do ust <- get UST

154 |          put UST ({ nextName $= (+1) } ust)

155 |          mn <- inCurrentNS (MN (show n) (nextName ust))

156 |          pure mn

160 | genVarName : {auto c : Ref Ctxt Defs} ->

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

162 |              String -> Core Name

163 | genVarName str

164 |     = do ust <- get UST

165 |          put UST ({ nextName $= (+1) } ust)

166 |          pure (MN str (nextName ust))

170 | genCaseName : {auto c : Ref Ctxt Defs} ->

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

172 |               String -> Core Name

173 | genCaseName root

174 |     = do ust <- get UST

175 |          put UST ({ nextName $= (+1) } ust)

176 |          inCurrentNS (CaseBlock root (nextName ust))

179 | genWithName : {auto c : Ref Ctxt Defs} ->

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

181 |               String -> Core Name

182 | genWithName root

183 |     = do ust <- get UST

184 |          put UST ({ nextName $= (+1) } ust)

185 |          inCurrentNS (WithBlock root (nextName ust))

187 | addHoleName : {auto u : Ref UST UState} ->

188 |               FC -> Name -> Int -> Core ()

189 | addHoleName fc n i = update UST { holes $= insert i (fc, n),

190 |                                   currentHoles $= insert i (fc, n) }

192 | addGuessName : {auto u : Ref UST UState} ->

193 |                FC -> Name -> Int -> Core ()

194 | addGuessName fc n i = update UST { guesses $= insert i (fc, n) }

197 | removeHole : {auto u : Ref UST UState} ->

198 |              Int -> Core ()

199 | removeHole n = update UST { holes $= delete n,

200 |                             currentHoles $= delete n,

201 |                             delayedHoles $= delete n }

204 | removeHoleName : {auto c : Ref Ctxt Defs} ->

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

206 |                  Name -> Core ()

207 | removeHoleName n

208 |     = do defs <- get Ctxt

209 |          whenJust (getNameID n defs.gamma) removeHole

212 | addNoSolve : {auto u : Ref UST UState} ->

213 |              Int -> Core ()

214 | addNoSolve i = update UST { noSolve $= insert i () }

217 | removeNoSolve : {auto u : Ref UST UState} ->

218 |                 Int -> Core ()

219 | removeNoSolve i = update UST { noSolve $= delete i }

222 | saveHoles : {auto u : Ref UST UState} ->

223 |             Core (IntMap (FC, Name))

225 |     = do ust <- get UST

226 |          put UST ({ currentHoles := empty } ust)

227 |          pure (currentHoles ust)

230 | restoreHoles : {auto u : Ref UST UState} ->

231 |                IntMap (FC, Name) -> Core ()

232 | restoreHoles hs = update UST { currentHoles := hs }

235 | removeGuess : {auto u : Ref UST UState} ->

236 |               Int -> Core ()

237 | removeGuess n = update UST { guesses $= delete n }

241 | getHoles : {auto u : Ref UST UState} ->

242 |            Core (IntMap (FC, Name))

243 | getHoles = holes <$> get UST

247 | getGuesses : {auto u : Ref UST UState} ->

248 |            Core (IntMap (FC, Name))

249 | getGuesses = guesses <$> get UST

254 | getCurrentHoles : {auto u : Ref UST UState} ->

255 |                   Core (IntMap (FC, Name))

256 | getCurrentHoles = currentHoles <$> get UST

259 | isHole : {auto u : Ref UST UState} ->

260 |          Int -> Core Bool

261 | isHole i = isJust . lookup i <$> getHoles

264 | isCurrentHole : {auto u : Ref UST UState} ->

265 |                 Int -> Core Bool

266 | isCurrentHole i = isJust . lookup i <$> getCurrentHoles

269 | setConstraint : {auto u : Ref UST UState} ->

270 |                 Int -> Constraint -> Core ()

271 | setConstraint cid c = update UST { constraints $= insert cid c }

274 | deleteConstraint : {auto u : Ref UST UState} ->

275 |                 Int -> Core ()

276 | deleteConstraint cid = update UST { constraints $= delete cid }

279 | addConstraint : {auto u : Ref UST UState} ->

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

281 |                 Constraint -> Core Int

282 | addConstraint constr

283 |     = do ust <- get UST

284 |          let cid = nextConstraint ust

285 |          put UST ({ constraints $= insert cid constr,

286 |                     nextConstraint := cid+1 } ust)

287 |          pure cid

290 | addDot : {vars : _} ->

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

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

293 |          FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->

294 |          Core ()

295 | addDot fc env dotarg x reason y

296 |     = do defs <- get Ctxt

297 |          xnf <- nf defs env x

298 |          ynf <- nf defs env y

299 |          update UST { dotConstraints $= ((dotarg, reason, MkConstraint fc False env xnf ynf) ::) }

302 | addPolyConstraint : {vars : _} ->

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

304 |                     FC -> Env Term vars -> Term vars -> NF vars -> NF vars ->

305 |                     Core ()

306 | addPolyConstraint fc env arg x@(NApp _ (NMeta {}) _) y

307 |     = update UST { polyConstraints $= ((MkPolyConstraint fc env arg x y) ::) }

308 | addPolyConstraint fc env arg x y

309 |     = pure ()

311 | mkLocal : {wkns : SnocList Name} -> FC -> Binder (Term vars) -> Term (wkns <>> x :: (vars ++ done))

312 | mkLocal fc b = Local fc (Just (isLet b)) _ (mkIsVarChiply (mkHasLength wkns))

314 | mkConstantAppArgs : {vars : _} ->

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

316 |                     (wkns : SnocList Name) ->

317 |                     List (Term (wkns <>> (vars ++ done)))

318 | mkConstantAppArgs lets fc [] wkns = []

319 | mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns

320 |     = let rec = mkConstantAppArgs {done} lets fc env (wkns :< x) in

321 |           if lets || not (isLet b)

322 |              then mkLocal fc b :: rec

323 |              else rec

325 | mkConstantAppArgsSub : {vars : _} ->

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

327 |                        Thin smaller vars ->

328 |                        (wkns : SnocList Name) ->

329 |                        List (Term (wkns <>> (vars ++ done)))

330 | mkConstantAppArgsSub lets fc [] p wkns = []

331 | mkConstantAppArgsSub {done} {vars = x :: xs}

332 |                         lets fc (b :: env) Refl wkns

333 |     = mkConstantAppArgs lets fc env (wkns :< x)

334 | mkConstantAppArgsSub {done} {vars = x :: xs}

335 |                         lets fc (b :: env) (Drop p) wkns

336 |     = mkConstantAppArgsSub lets fc env p (wkns :< x)

337 | mkConstantAppArgsSub {done} {vars = x :: xs}

338 |                         lets fc (b :: env) (Keep p) wkns

339 |     = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns :< x) in

340 |           if lets || not (isLet b)

341 |              then mkLocal fc b :: rec

342 |              else rec

344 | mkConstantAppArgsOthers : {vars : _} ->

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

346 |                           Thin smaller vars ->

347 |                           (wkns : SnocList Name) ->

348 |                           List (Term (wkns <>> (vars ++ done)))

349 | mkConstantAppArgsOthers lets fc [] p wkns = []

350 | mkConstantAppArgsOthers {done} {vars = x :: xs}

351 |                         lets fc (b :: env) Refl wkns

352 |     = mkConstantAppArgsOthers lets fc env Refl (wkns :< x)

353 | mkConstantAppArgsOthers {done} {vars = x :: xs}

354 |                         lets fc (b :: env) (Keep p) wkns

355 |     = mkConstantAppArgsOthers lets fc env p (wkns :< x)

356 | mkConstantAppArgsOthers {done} {vars = x :: xs}

357 |                         lets fc (b :: env) (Drop p) wkns

358 |     = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns :< x) in

359 |           if lets || not (isLet b)

360 |              then mkLocal fc b :: rec

361 |              else rec

364 | applyTo : {vars : _} ->

365 |           FC -> Term vars -> Env Term vars -> Term vars

366 | applyTo fc tm env

367 |   = let args = reverse (mkConstantAppArgs {done = Scope.empty} False fc env [<]) in

368 |         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

371 | applyToFull : {vars : _} ->

372 |               FC -> Term vars -> Env Term vars -> Term vars

373 | applyToFull fc tm env

374 |   = let args = reverse (mkConstantAppArgs {done = Scope.empty} True fc env [<]) in

375 |         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

378 | applyToSub : {vars : _} ->

379 |              FC -> Term vars -> Env Term vars ->

380 |              Thin smaller vars -> Term vars

381 | applyToSub fc tm env sub

382 |   = let args = reverse (mkConstantAppArgsSub {done = Scope.empty} True fc env sub [<]) in

383 |         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

386 | applyToOthers : {vars : _} ->

387 |                 FC -> Term vars -> Env Term vars ->

388 |                 Thin smaller vars -> Term vars

389 | applyToOthers fc tm env sub

390 |   = let args = reverse (mkConstantAppArgsOthers {done = Scope.empty} True fc env sub [<]) in

391 |         apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

399 | newMetaLets : {vars : _} ->

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

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

402 |               FC -> RigCount ->

403 |               Env Term vars -> Name -> Term vars -> Def ->

404 |               Bool -> Bool ->

405 |               Core (Int, Term vars)

406 | newMetaLets {vars} fc rig env n ty def nocyc lets

407 |     = do let hty = if lets then abstractFullEnvType fc env ty

408 |                            else abstractEnvType fc env ty

409 |          let hole = { noCycles := nocyc }

410 |                            (newDef fc n rig Scope.empty hty (specified Public) def)

411 |          log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig)

412 |          logTerm "unify.meta" 10 ("New meta type " ++ show n) hty

413 |          idx <- addDef n hole

414 |          addHoleName fc n idx

415 |          pure (idx, Meta fc n idx envArgs)

416 |   where

417 |     envArgs : List (Term vars)

418 |     envArgs = let args = reverse (mkConstantAppArgs {done = Scope.empty} lets fc env [<]) in

419 |                   rewrite sym (appendNilRightNeutral vars) in args

422 | newMeta : {vars : _} ->

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

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

425 |           FC -> RigCount ->

426 |           Env Term vars -> Name -> Term vars -> Def ->

427 |           Bool ->

428 |           Core (Int, Term vars)

429 | newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False

431 | mkConstant : {vars : _} ->

432 |              FC -> Env Term vars -> Term vars -> ClosedTerm

433 | mkConstant fc [] tm = tm

436 | mkConstant {vars = x :: _} fc (b :: env) tm

437 |     = let ty = binderType b in

438 |           mkConstant fc env (Bind fc x (Lam fc (multiplicity b) Explicit ty) tm)

444 | newConstant : {vars : _} ->

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

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

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

448 |               (tm : Term vars) -> (ty : Term vars) ->

449 |               (constrs : List Int) ->

450 |               Core (Term vars)

451 | newConstant {vars} fc rig env tm ty constrs

452 |     = do let def = mkConstant fc env tm

453 |          let defty = abstractFullEnvType fc env ty

454 |          cn <- genName "postpone"

455 |          let guess = newDef fc cn rig Scope.empty defty (specified Public)

456 |                             (Guess def (length env) constrs)

457 |          log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig)

458 |          logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty

459 |          idx <- addDef cn guess

460 |          addGuessName fc cn idx

461 |          pure (Meta fc cn idx envArgs)

462 |   where

463 |     envArgs : List (Term vars)

464 |     envArgs = let args = reverse (mkConstantAppArgs {done = Scope.empty} True fc env [<]) in

465 |                   rewrite sym (appendNilRightNeutral vars) in args

471 | newSearch : {vars : _} ->

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

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

474 |             FC -> RigCount -> Nat -> Name ->

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

476 | newSearch {vars} fc rig depth def env n ty

477 |     = do let hty = abstractEnvType fc env ty

478 |          let hole = newDef fc n rig Scope.empty hty (specified Public) (BySearch rig depth def)

479 |          log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n

480 |          logTermNF "unify.search" 10 "New search type" Env.empty hty

481 |          idx <- addDef n hole

482 |          addGuessName fc n idx

483 |          pure (idx, Meta fc n idx envArgs)

484 |   where

485 |     envArgs : List (Term vars)

486 |     envArgs = let args = reverse (mkConstantAppArgs {done = Scope.empty} False fc env [<]) in

487 |                   rewrite sym (appendNilRightNeutral vars) in args

491 | newDelayed : {vars : _} ->

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

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

494 |              FC -> RigCount ->

495 |              Env Term vars -> Name ->

496 |              (ty : Term vars) -> Core (Int, Term vars)

497 | newDelayed {vars} fc rig env n ty

498 |     = do let hty = abstractEnvType fc env ty

499 |          let hole = newDef fc n rig Scope.empty hty (specified Public) Delayed

500 |          idx <- addDef n hole

501 |          log "unify.delay" 10 $ "Added delayed elaborator " ++ show (n, idx)

502 |          addHoleName fc n idx

503 |          pure (idx, Meta fc n idx envArgs)

504 |   where

505 |     envArgs : List (Term vars)

506 |     envArgs = let args = reverse (mkConstantAppArgs {done = Scope.empty} False fc env [<]) in

507 |                   rewrite sym (appendNilRightNeutral vars) in args

510 | tryErrorUnify : {auto c : Ref Ctxt Defs} ->

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

512 |                 {default False unResolve : Bool} ->

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

514 | tryErrorUnify elab

515 |     = do ust <- get UST

516 |          defs <- branch

517 |          catch (do res <- elab

518 |                    commit

519 |                    pure (Right res))

520 |                (\err => do put UST ust

521 |                            err <- ifThenElse unResolve toFullNames pure err

522 |                            defs' <- get Ctxt

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

524 |                            pure (Left err))

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

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

529 |            Core a -> Core a -> Core a

530 | tryUnify elab1 elab2

531 |     = do Right ok <- tryErrorUnify elab1

532 |                | Left err => elab2

533 |          pure ok

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

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

538 |               {default False unResolve : Bool} ->

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

540 | handleUnify elab1 elab2

541 |     = do Right ok <- tryErrorUnify {unResolve} elab1

542 |                | Left err => elab2 err

543 |          pure ok

548 | addDelayedHoleName : {auto u : Ref UST UState} ->

549 |                      (Int, (FC, Name)) -> Core ()

550 | addDelayedHoleName (idx, h) = update UST { delayedHoles $= insert idx h }

553 | checkDelayedHoles : {auto u : Ref UST UState} ->

554 |                     Core (Maybe Error)

556 |     = do ust <- get UST

557 |          let hs = toList (delayedHoles ust)

558 |          if (not (isNil hs))

559 |             then do pure (Just (UnsolvedHoles (map snd hs)))

560 |             else pure Nothing

566 | checkValidHole : {auto c : Ref Ctxt Defs} ->

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

568 |                  Int -> (Int, (FC, Name)) -> Core ()

569 | checkValidHole base (idx, (fc, n))

570 |   = when (idx >= base) $

571 |       do defs <- get Ctxt

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

573 |               | Nothing => pure ()

574 |          case definition gdef of

575 |               BySearch {} =>

576 |                   do defs <- get Ctxt

577 |                      Just ty <- lookupTyExact n (gamma defs)

578 |                           | Nothing => pure ()

579 |                      throw (CantSolveGoal fc (gamma defs) Env.empty ty Nothing)

580 |               Guess tm envb (con :: _) =>

581 |                   do ust <- get UST

582 |                      let Just c = lookup con (constraints ust)

583 |                           | Nothing => pure ()

584 |                      case c of

585 |                           MkConstraint fc l env x y =>

586 |                              do put UST ({ guesses := empty } ust)

587 |                                 empty <- clearDefs defs

588 |                                 xnf <- quote empty env x

589 |                                 ynf <- quote empty env y

590 |                                 throw (CantSolveEq fc (gamma defs) env xnf ynf)

591 |                           _ => pure ()

592 |               _ => traverse_ checkRef !(traverse getFullName

593 |                                         ((keys (getRefs (Resolved (-1)) (type gdef)))))

594 |   where

595 |     checkRef : Name -> Core ()

596 |     checkRef (PV n f)

597 |         = throw (GenericMsg fc

598 |                    ("Hole cannot depend on an unbound implicit " ++ show n))

599 |     checkRef _ = pure ()

607 | checkUserHolesAfter : {auto u : Ref UST UState} ->

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

609 |                       Int -> Bool -> Core ()

610 | checkUserHolesAfter base now

611 |     = do gs_map <- getGuesses

612 |          let gs = toList gs_map

613 |          log "unify.unsolved" 10 $ "Unsolved guesses " ++ show gs

614 |          List.traverse_ (checkValidHole base) gs

615 |          hs_map <- getCurrentHoles

616 |          let hs = toList hs_map

617 |          let hs' = if any isUserName (map (snd . snd) hs)

618 |                       then [] else hs

619 |          when (now && not (isNil hs')) $

620 |               throw (UnsolvedHoles (map snd (nubBy nameEq hs)))

621 |          -- Note the hole names, to ensure they are resolved

622 |          -- by the end of elaborating the current source file

623 |          traverse_ addDelayedHoleName hs'

624 |   where

625 |     nameEq : (a, b, Name) -> (a, b, Name) -> Bool

626 |     nameEq (_, _, x) (_, _, y) = x == y

629 | checkUserHoles : {auto u : Ref UST UState} ->

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

631 |                  Bool -> Core ()

632 | checkUserHoles = checkUserHolesAfter 0

635 | checkNoGuards : {auto u : Ref UST UState} ->

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

637 |                 Core ()

638 | checkNoGuards = checkUserHoles False

641 | dumpHole : {auto u : Ref UST UState} ->

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

643 |            LogTopic -> Nat -> (hole : Int) -> Core ()

644 | dumpHole s n hole

645 |     = do ust <- get UST

646 |          defs <- get Ctxt

647 |          case !(lookupCtxtExact (Resolved hole) (gamma defs)) of

648 |           Nothing => pure ()

649 |           Just gdef => case (definition gdef, type gdef) of

650 |              (Guess tm envb constraints, ty) =>

651 |                   do logString s.topic n $

652 |                        "!" ++ show !(getFullName (Resolved hole)) ++ " : "

653 |                            ++ show !(toFullNames !(normaliseHoles defs Env.empty ty))

654 |                        ++ "\n\t  = "

655 |                            ++ show !(normaliseHoles defs Env.empty tm)

656 |                            ++ "\n\twhen"

657 |                      traverse_ dumpConstraint constraints

658 |              (Hole _ p, ty) =>

659 |                   logString s.topic n $

660 |                     "?" ++ show (fullname gdef) ++ " : "

661 |                         ++ show !(normaliseHoles defs Env.empty ty)

662 |                         ++ if implbind p then " (ImplBind)" else ""

663 |                         ++ if invertible gdef then " (Invertible)" else ""

664 |              (BySearch _ _ _, ty) =>

665 |                   logString s.topic n $

666 |                      "Search " ++ show hole ++ " : " ++

667 |                      show !(toFullNames !(normaliseHoles defs Env.empty ty))

668 |              (PMDef _ args t _ _, ty) =>

669 |                   log s 4 $

670 |                      "Solved: " ++ show hole ++ " : " ++

671 |                      show !(normalise defs Env.empty ty) ++

672 |                      " = " ++ show !(normalise defs Env.empty (Ref emptyFC Func (Resolved hole)))

673 |              (ImpBind, ty) =>

674 |                   log s 4 $

675 |                       "Bound: " ++ show hole ++ " : " ++

676 |                       show !(normalise defs Env.empty ty)

677 |              (Delayed, ty) =>

678 |                   log s 4 $

679 |                      "Delayed elaborator : " ++

680 |                      show !(normalise defs Env.empty ty)

681 |              _ => pure ()

682 |   where

683 |     dumpConstraint : Int -> Core ()

684 |     dumpConstraint cid

685 |         = do ust <- get UST

686 |              defs <- get Ctxt

687 |              case lookup cid (constraints ust) of

688 |                   Nothing => pure ()

689 |                   Just Resolved => logString s.topic n "\tResolved"

690 |                   Just (MkConstraint _ lazy env x y) =>

691 |                     do logString s.topic n $

692 |                          "\t  " ++ show !(toFullNames !(quote defs env x))

693 |                                 ++ " =?= " ++ show !(toFullNames !(quote defs env y))

694 |                        empty <- clearDefs defs

695 |                        log s 5 $

696 |                          "\t    from " ++ show !(toFullNames !(quote empty env x))

697 |                             ++ " =?= " ++ show !(toFullNames !(quote empty env y))

698 |                             ++ if lazy then "\n\t(lazy allowed)" else ""

701 | dumpConstraints : {auto u : Ref UST UState} ->

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

703 |                   LogTopic -> (verbosity : Nat) -> (all : Bool) -> Core ()

704 | dumpConstraints s n all

705 |     = do ust <- get UST

706 |          defs <- get Ctxt

707 |          when !(logging s n) $ do

708 |            let hs = toList (guesses ust) ++

709 |                     toList (if all then holes ust else currentHoles ust)

710 |            unless (isNil hs) $

711 |              do logString s.topic n "--- CONSTRAINTS AND HOLES ---"

712 |                 traverse_ (dumpHole s n) (map fst hs)