0 | module Core.AutoSearch

  2 | import Core.Context.Log

  3 | import Core.Env

  4 | import Core.Normalise

  5 | import Core.Unify

  6 | import Core.Value

  8 | import Data.Either

  9 | import Data.Maybe

 11 | import Libraries.Data.NatSet

 12 | import Libraries.Data.List.SizeOf

 13 | import Libraries.Data.WithDefault

 15 | %default covering

 17 | tryUnifyUnambig' : {auto c : Ref Ctxt Defs} ->

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

 19 |                    {default False preferLeftError : Bool} ->

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

 21 | tryUnifyUnambig' left right = handleUnify left $ \case

 22 |   e@(AmbiguousSearch {}) => throw e

 23 |   e                      => if preferLeftError

 24 |                               then tryUnify (right e) (throw e)

 25 |                               else right e

 27 | tryUnifyUnambig : {auto c : Ref Ctxt Defs} ->

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

 29 |                   {default False preferLeftError : Bool} ->

 30 |                   Core a -> Core a -> Core a

 31 | tryUnifyUnambig left right = tryUnifyUnambig' {preferLeftError} left $ const right

 33 | tryNoDefaultsFirst : {auto c : Ref Ctxt Defs} ->

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

 35 |                      (Bool -> Core a) -> Core a

 36 | tryNoDefaultsFirst f = tryUnifyUnambig {preferLeftError=True} (f False) (f True)

 38 | SearchEnv : Scoped

 39 | SearchEnv vars = List (NF vars, Closure vars)

 41 | searchType : {vars : _} ->

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

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

 44 |              FC -> RigCount ->

 45 |              (defaults : Bool) -> (trying : List (Term vars)) ->

 46 |              (depth : Nat) ->

 47 |              (defining : Name) ->

 48 |              (checkDets : Bool) -> (topTy : ClosedTerm) ->

 49 |              Env Term vars -> (target : Term vars) -> Core (Term vars)

 51 | public export

 52 | record ArgInfo (vars : Scope) where

 53 |   constructor MkArgInfo

 54 |   holeID : Int

 55 |   argRig : RigCount

 56 |   plicit : PiInfo (Closure vars)

 57 |   metaApp : Term vars

 58 |   argType : Term vars

 61 | mkArgs : {vars : _} ->

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

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

 64 |          FC -> RigCount ->

 65 |          Env Term vars -> NF vars ->

 66 |          Core (List (ArgInfo vars), NF vars)

 67 | mkArgs fc rigc env (NBind nfc x (Pi fc' c p ty) sc)

 68 |     = do defs <- get Ctxt

 69 |          empty <- clearDefs defs

 70 |          nm <- genName "sa"

 71 |          argTy <- quote empty env ty

 72 |          let argRig = rigMult rigc c

 73 |          (idx, arg) <- newMeta fc' argRig env nm argTy

 74 |                                (Hole (length env) (holeInit False)) False

 75 |          setInvertible fc (Resolved idx)

 76 |          (rest, restTy) <- mkArgs fc rigc env

 77 |                               !(sc defs (toClosure defaultOpts env arg))

 78 |          pure (MkArgInfo idx argRig p arg argTy :: rest, restTy)

 79 | mkArgs fc rigc env ty = pure ([], ty)

 82 | impLast : List (ArgInfo vars) -> List (ArgInfo vars)

 83 | impLast xs = filter (not . impl) xs ++ filter impl xs

 84 |   where

 85 |       impl : ArgInfo vs -> Bool

 86 |       impl inf

 87 |           = case plicit inf of

 88 |                  Explicit => False

 89 |                  _ => True

 91 | searchIfHole : {vars : _} ->

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

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

 94 |                FC ->

 95 |                (defaults : Bool) -> List (Term vars) ->

 96 |                (ispair : Bool) -> (depth : Nat) ->

 97 |                (defining : Name) -> (topTy : ClosedTerm) -> Env Term vars ->

 98 |                (arg : ArgInfo vars) ->

 99 |                Core ()

100 | searchIfHole fc defaults trying ispair Z def top env arg

101 |     = throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing) -- possibly should say depth limit hit?

102 | searchIfHole fc defaults trying ispair (S depth) def top env arg

103 |     = do let hole = holeID arg

104 |          let rig = argRig arg

106 |          defs <- get Ctxt

107 |          Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)

108 |               | Nothing => throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing)

109 |          let Hole _ _ = definition gdef

110 |               | _ => pure () -- already solved

111 |          top' <- if ispair

112 |                     then normaliseScope defs Env.empty (type gdef)

113 |                     else pure top

115 |          argdef <- searchType fc rig defaults trying depth def False top' env

116 |                               !(normaliseScope defs env (argType arg))

117 |          logTermNF "auto" 5 "Solved arg" env argdef

118 |          logTermNF "auto" 5 "Arg meta" env (metaApp arg)

119 |          ok <- solveIfUndefined env (metaApp arg) argdef

120 |          if ok

121 |             then pure ()

122 |             else do vs <- unify inTerm fc env (metaApp arg) argdef

123 |                     let [] = constraints vs

124 |                         | _ => throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

125 |                     pure ()

127 | successful : {vars : _} ->

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

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

130 |              List (Core (Term vars)) ->

131 |              Core (List (Either Error (Term vars, Defs, UState)))

132 | successful [] = pure []

133 | successful (elab :: elabs)

134 |     = do ust <- get UST

135 |          defs <- branch

136 |          catch (do -- Run the elaborator

137 |                    res <- elab

138 |                    -- Record post-elaborator state

139 |                    ust' <- get UST

140 |                    defs' <- get Ctxt

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

142 |                    put UST ust

143 |                    put Ctxt defs

144 |                    elabs' <- successful elabs

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

146 |                    pure (Right (res, defs', ust') :: elabs'))

147 |                (\err => do put UST ust

148 |                            put Ctxt defs

149 |                            elabs' <- successful elabs

150 |                            pure (Left err :: elabs'))

152 | anyOne : {auto c : Ref Ctxt Defs} ->

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

154 |          FC -> Env Term vars -> (topTy : ClosedTerm) ->

155 |          List (Core (Term vars)) ->

156 |          Core (Term vars)

157 | anyOne fc env top [] = throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing)

158 | anyOne fc env top [elab]

159 |     = catch elab $

160 |          \case

161 |            err@(CantSolveGoal {})   => throw err

162 |            err@(AmbiguousSearch {}) => throw err

163 |            _ => throw $ CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing

164 | anyOne fc env top (elab :: elabs)

165 |     = tryUnify elab (anyOne fc env top elabs)

167 | exactlyOne : {vars : _} ->

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

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

170 |              FC -> Env Term vars -> (topTy : ClosedTerm) -> (target : NF vars) ->

171 |              List (Core (Term vars)) ->

172 |              Core (Term vars)

173 | exactlyOne fc env top target [elab]

174 |     = catch elab $

175 |          \case

176 |            err@(CantSolveGoal {}) => throw err

177 |            _ => throw $ CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing

178 | exactlyOne {vars} fc env top target all

179 |     = do elabs <- successful all

180 |          case nubBy ((==) `on` fst) $ rights elabs of

181 |               [(res, defs, ust)] =>

182 |                     do put UST ust

183 |                        put Ctxt defs

184 |                        commit

185 |                        pure res

186 |               [] => throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing)

187 |               rs => throw (AmbiguousSearch fc env !(quote !(get Ctxt) env target)

188 |                              !(traverse normRes rs))

189 |   where

190 |     normRes : (Term vars, Defs, UState) -> Core (Term vars)

191 |     normRes (tm, defs, _) = normaliseHoles defs env tm

198 | getUsableEnv : FC -> RigCount ->

199 |                SizeOf done ->

200 |                Env Term vars ->

201 |                -- TODO this will be `vars <>< done` after refactoring

202 |                List (Term (done ++ vars), Term (done ++ vars))

203 | getUsableEnv fc rigc p [] = []

204 | getUsableEnv {vars = v :: vs} {done} fc rigc p (b :: env)

205 |    = let rest = getUsableEnv fc rigc (sucR p) env in

206 |          if (multiplicity b == top || isErased rigc)

207 |             then let 0 var = mkIsVar (hasLength p) in

208 |                      (Local (binderLoc b) Nothing _ var,

209 |                        rewrite appendAssociative done (Scope.single v) vs in

210 |                           weakenNs (sucR p) (binderType b)) ::

211 |                                rewrite appendAssociative done (Scope.single v) vs in rest

212 |             else rewrite appendAssociative done (Scope.single v) vs in rest

215 | usableLocal : {vars : _} ->

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

217 |               FC -> (defaults : Bool) ->

218 |               Env Term vars -> (locTy : NF vars) -> Core Bool

220 | usableLocal loc defaults env (NApp fc (NMeta (PV {}) _ _) args)

221 |     = pure True

222 | usableLocal loc defaults env (NApp fc (NMeta {}) args)

223 |     = pure False

224 | usableLocal {vars} loc defaults env (NTCon _ n _ args)

225 |     = do sd <- getSearchData loc (not defaults) n

226 |          usableLocalArg 0 (detArgs sd) (map snd args)

227 |   -- usable if none of the determining arguments of the local's type are

228 |   -- holes

229 |   where

230 |     usableLocalArg : Nat -> NatSet -> List (Closure vars) -> Core Bool

231 |     usableLocalArg i dets [] = pure True

232 |     usableLocalArg i dets (c :: cs)

233 |         = if i `elem` dets

234 |              then do defs <- get Ctxt

235 |                      u <- usableLocal loc defaults env !(evalClosure defs c)

236 |                      if u

237 |                         then usableLocalArg (1 + i) dets cs

238 |                         else pure False

239 |              else usableLocalArg (1 + i) dets cs

240 | usableLocal loc defaults env (NDCon _ n _ _ args)

241 |     = do defs <- get Ctxt

242 |          us <- traverse (usableLocal loc defaults env)

243 |                         !(traverse (evalClosure defs) $ map snd args)

244 |          pure (all id us)

245 | usableLocal loc defaults env (NApp _ (NLocal {}) args)

246 |     = do defs <- get Ctxt

247 |          us <- traverse (usableLocal loc defaults env)

248 |                         !(traverse (evalClosure defs) $ map snd args)

249 |          pure (all id us)

250 | usableLocal loc defaults env (NBind fc x (Pi {}) sc)

251 |     = do defs <- get Ctxt

252 |          usableLocal loc defaults env

253 |                 !(sc defs (toClosure defaultOpts env (Erased fc Placeholder)))

254 | usableLocal loc defaults env (NErased {}) = pure False

255 | usableLocal loc _ _ _ = pure True

257 | searchLocalWith : {vars : _} ->

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

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

260 |                   FC -> RigCount ->

261 |                   (defaults : Bool) -> List (Term vars) ->

262 |                   (depth : Nat) ->

263 |                   (defining : Name) -> (topTy : ClosedTerm) ->

264 |                   Env Term vars -> (Term vars, Term vars) ->

265 |                   (target : NF vars) -> Core (Term vars)

266 | searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) target

267 |     = do defs <- get Ctxt

268 |          nty <- nf defs env ty

269 |          findPos defs pure nty target

270 |   where

271 |     clearEnvType : {idx : Nat} -> (0 p : IsVar nm idx vs) ->

272 |                    FC -> Env Term vs -> Env Term vs

273 |     clearEnvType First fc (b :: env)

274 |         = Lam (binderLoc b) (multiplicity b) Explicit (Erased fc Placeholder) :: env

275 |     clearEnvType (Later p) fc (b :: env) = b :: clearEnvType p fc env

277 |     clearEnv : Term vars -> Env Term vars -> Env Term vars

278 |     clearEnv (Local fc _ idx p) env

279 |         = clearEnvType p fc env

280 |     clearEnv _ env = env

282 |     findDirect : Defs ->

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

284 |                  NF vars ->  -- local's type

285 |                  (target : NF vars) ->

286 |                  Core (Term vars)

287 |     findDirect defs f ty target

288 |         = do (args, appTy) <- mkArgs fc rigc env ty

289 |              fprf <- f prf

290 |              logTermNF "auto" 10 "Trying" env fprf

291 |              logNF "auto" 10 "Type" env ty

292 |              logNF "auto" 10 "For target" env target

293 |              ures <- unify inTerm fc env target appTy

294 |              let [] = constraints ures

295 |                  | _ => throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

296 |              -- We can only use the local if its type is not an unsolved hole

297 |              if !(usableLocal fc defaults env ty)

298 |                 then do

299 |                    let candidate = apply fc fprf (map metaApp args)

300 |                    logTermNF "auto" 10 "Local var candidate " env candidate

301 |                    -- Clear the local from the environment to avoid getting

302 |                    -- into a loop repeatedly applying it

303 |                    let env' = clearEnv prf env

304 |                    -- Work right to left, because later arguments may solve

305 |                    -- earlier ones by unification

306 |                    traverse_ (searchIfHole fc defaults trying False depth def top env')

307 |                             (impLast args)

308 |                    pure candidate

309 |                 else do logNF "auto" 10 "Can't use " env ty

310 |                         throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

312 |     findPos : Defs ->

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

314 |               NF vars ->  -- local's type

315 |               (target : NF vars) ->

316 |               Core (Term vars)

317 |     findPos defs f nty@(NTCon pfc pn _ [(_, xty), (_, yty)]) target

318 |         = tryUnifyUnambig (findDirect defs f nty target) $

319 |              do fname <- maybe (throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing))

320 |                                pure

321 |                                !fstName

322 |                 sname <- maybe (throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing))

323 |                                pure

324 |                                !sndName

325 |                 if !(isPairType pn)

326 |                    then do empty <- clearDefs defs

327 |                            xtytm <- quote empty env xty

328 |                            ytytm <- quote empty env yty

329 |                            exactlyOne fc env top target

330 |                             [(do xtynf <- evalClosure defs xty

331 |                                  findPos defs

332 |                                      (\arg => normalise defs env $ apply fc (Ref fc Func fname)

333 |                                                         [xtytm,

334 |                                                          ytytm,

335 |                                                          !(f arg)])

336 |                                      xtynf target),

337 |                              (do ytynf <- evalClosure defs yty

338 |                                  findPos defs

339 |                                      (\arg => normalise defs env $ apply fc (Ref fc Func sname)

340 |                                                         [xtytm,

341 |                                                          ytytm,

342 |                                                          !(f arg)])

343 |                                      ytynf target)]

344 |                    else throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

345 |     findPos defs f nty target

346 |         = findDirect defs f nty target

348 | searchLocalVars : {vars : _} ->

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

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

351 |                   FC -> RigCount ->

352 |                   (defaults : Bool) -> List (Term vars) ->

353 |                   (depth : Nat) ->

354 |                   (defining : Name) -> (topTy : ClosedTerm) ->

355 |                   Env Term vars ->

356 |                   (target : NF vars) -> Core (Term vars)

357 | searchLocalVars fc rig defaults trying depth def top env target

358 |     = do let elabs = map (\t => searchLocalWith fc rig defaults trying depth def

359 |                                               top env t target)

360 |                          (getUsableEnv fc rig zero env)

361 |          exactlyOne fc env top target elabs

363 | isPairNF : {auto c : Ref Ctxt Defs} ->

364 |            Env Term vars -> NF vars -> Defs -> Core Bool

365 | isPairNF env (NTCon _ n _ _) defs

366 |     = isPairType n

367 | isPairNF env (NBind fc b (Pi {}) sc) defs

368 |     = isPairNF env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder))) defs

369 | isPairNF _ _ _ = pure False

371 | searchName : {vars : _} ->

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

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

374 |              FC -> RigCount ->

375 |              (defaults : Bool) -> List (Term vars) ->

376 |              (depth : Nat) ->

377 |              (defining : Name) -> (topTy : ClosedTerm) ->

378 |              Env Term vars -> (target : NF vars) ->

379 |              (Name, GlobalDef) ->

380 |              Core (Term vars)

381 | searchName fc rigc defaults trying depth def top env target (n, ndef)

382 |     = do defs <- get Ctxt

383 |          when (not (visibleInAny (!getNS :: !getNestedNS)

384 |                                  (fullname ndef) (collapseDefault $ visibility ndef))) $

385 |             throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

386 |          when (BlockedHint `elem` flags ndef) $

387 |             throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

389 |          let ty = type ndef

390 |          when (isErased ty) $

391 |             throw (CantSolveGoal fc (gamma defs) [] top Nothing)

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

394 |          logNF "auto" 10 ("Searching Name " ++ show n) env nty

395 |          (args, appTy) <- mkArgs fc rigc env nty

396 |          ures <- unify inTerm fc env target appTy

397 |          let [] = constraints ures

398 |              | _ => throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

399 |          ispair <- isPairNF env nty defs

400 |          let candidate = apply fc (Ref fc (getDefNameType ndef) n) (map metaApp args)

401 |          logTermNF "auto" 10 "Candidate " env candidate

402 |          -- Work right to left, because later arguments may solve earlier

403 |          -- dependencies by unification

404 |          traverse_ (searchIfHole fc defaults trying ispair depth def top env)

405 |                   (impLast args)

406 |          pure candidate

408 | searchNames : {vars : _} ->

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

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

411 |               FC -> RigCount ->

412 |               (defaults : Bool) -> List (Term vars) ->

413 |               (depth : Nat) ->

414 |               (defining : Name) -> (topTy : ClosedTerm) ->

415 |               Env Term vars -> Bool -> List Name ->

416 |               (target : NF vars) -> Core (Term vars)

417 | searchNames fc rigc defaults trying depth defining topty env ambig [] target

418 |     = throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty topty Nothing)

419 | searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) target

420 |     = do defs <- get Ctxt

421 |          visnsm <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)

422 |          let visns = mapMaybe id visnsm

423 |          let elabs = map (searchName fc rigc defaults trying depth defining topty env target) visns

424 |          if ambig

425 |             then anyOne fc env topty elabs

426 |             else exactlyOne fc env topty target elabs

427 |   where

428 |     visible : Context ->

429 |               List Namespace -> Name -> Core (Maybe (Name, GlobalDef))

430 |     visible gam nspace n

431 |         = do Just def <- lookupCtxtExact n gam

432 |                   | Nothing => pure Nothing

433 |              if visibleInAny nspace n (collapseDefault $ visibility def)

434 |                 then pure $ Just (n, def)

435 |                 else pure $ Nothing

437 | concreteDets : {vars : _} ->

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

439 |                FC -> Bool ->

440 |                Env Term vars -> (top : ClosedTerm) ->

441 |                (pos : Nat) -> (dets : NatSet) ->

442 |                (args : List (Closure vars)) ->

443 |                Core ()

444 | concreteDets fc defaults env top pos dets [] = pure ()

445 | concreteDets {vars} fc defaults env top pos dets (arg :: args)

446 |     = do when (pos `elem` dets) $ do

447 |            defs <- get Ctxt

448 |            argnf <- evalClosure defs arg

449 |            logNF "auto.determining" 10

450 |              "Checking that the following argument is concrete"

451 |              env argnf

452 |            concrete defs argnf True

453 |          concreteDets fc defaults env top (1 + pos) dets args

454 |   where

455 |     concrete : Defs -> NF vars -> (atTop : Bool) -> Core ()

456 |     concrete defs (NBind nfc x b sc) atTop

457 |         = do scnf <- sc defs (toClosure defaultOpts env (Erased nfc Placeholder))

458 |              concrete defs scnf False

459 |     concrete defs (NTCon nfc n a args) atTop

460 |         = do sd <- getSearchData nfc False n

461 |              let args' = NatSet.take (detArgs sd) args

462 |              traverse_ (\ parg => do argnf <- evalClosure defs parg

463 |                                      concrete defs argnf False) (map snd args')

464 |     concrete defs (NDCon nfc n t a args) atTop

465 |         = do traverse_ (\ parg => do argnf <- evalClosure defs parg

466 |                                      concrete defs argnf False) (map snd args)

467 |     concrete defs (NApp _ (NMeta n i _) _) True

468 |         = do Just (Hole _ b) <- lookupDefExact n (gamma defs)

469 |                   | _ => throw (DeterminingArg fc n i Env.empty top)

470 |              unless (implbind b) $

471 |                   throw (DeterminingArg fc n i Env.empty top)

472 |     concrete defs (NApp _ (NMeta n i _) _) False

473 |         = do Just (Hole _ b) <- lookupDefExact n (gamma defs)

474 |                   | def => throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

475 |              unless (implbind b) $

476 |                   throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

477 |     concrete defs tm atTop = pure ()

479 | checkConcreteDets : {vars : _} ->

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

481 |                     FC -> Bool ->

482 |                     Env Term vars -> (top : ClosedTerm) ->

483 |                     NF vars ->

484 |                     Core ()

485 | checkConcreteDets fc defaults env top (NTCon tfc tyn a args)

486 |     = do defs <- get Ctxt

487 |          if !(isPairType tyn)

488 |             then case args of

489 |                       [(_, aty), (_, bty)] =>

490 |                           do anf <- evalClosure defs aty

491 |                              bnf <- evalClosure defs bty

492 |                              checkConcreteDets fc defaults env top anf

493 |                              checkConcreteDets fc defaults env top bnf

494 |                       _ => do sd <- getSearchData fc defaults tyn

495 |                               concreteDets fc defaults env top 0 (detArgs sd) (map snd args)

496 |             else

497 |               do sd <- getSearchData fc defaults tyn

498 |                  log "auto.determining" 10 $

499 |                    "Determining arguments for " ++ show !(toFullNames tyn)

500 |                    ++ " " ++ show (detArgs sd)

501 |                  concreteDets fc defaults env top 0 (detArgs sd) (map snd args)

502 | checkConcreteDets fc defaults env top _

503 |     = pure ()

505 | abandonIfCycle : {vars : _} ->

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

507 |                  Env Term vars -> Term vars -> List (Term vars) ->

508 |                  Core ()

509 | abandonIfCycle env tm [] = pure ()

510 | abandonIfCycle env tm (ty :: tys)

511 |     = do defs <- get Ctxt

512 |          if !(convert defs env tm ty)

513 |             then throw (InternalError "Cycle in search")

514 |             else abandonIfCycle env tm tys

517 | searchType fc rigc defaults trying depth def checkdets top env (Bind nfc x b@(Pi fc' c p ty) sc)

518 |     = pure (Bind nfc x (Lam fc' c p ty)

519 |              !(searchType fc rigc defaults [] depth def checkdets top

520 |                           (b :: env) sc))

521 | searchType fc rigc defaults trying depth def checkdets top env (Bind nfc x b@(Let fc' c val ty) sc)

522 |     = pure (Bind nfc x b

523 |              !(searchType fc rigc defaults [] depth def checkdets top

524 |                           (b :: env) sc))

525 | searchType {vars} fc rigc defaults trying depth def checkdets top env target

526 |     = do defs <- get Ctxt

527 |          abandonIfCycle env target trying

528 |          let trying' = target :: trying

529 |          nty <- nf defs env target

530 |          case nty of

531 |               NTCon tfc tyn a args =>

532 |                   if a == length args

533 |                      then do logNF "auto" 10 "Next target" env nty

534 |                              sd <- getSearchData fc defaults tyn

535 |                              -- Check determining arguments are okay for 'args'

536 |                              when checkdets $

537 |                                  checkConcreteDets fc defaults env top

538 |                                                    (NTCon tfc tyn a args)

539 |                              if defaults && checkdets

540 |                                 then tryGroups Nothing nty (hintGroups sd)

541 |                                 else tryUnifyUnambig

542 |                                        (searchLocalVars fc rigc defaults trying' depth def top env nty)

543 |                                        (tryGroups Nothing nty (hintGroups sd))

544 |                      else throw (CantSolveGoal fc (gamma defs) Env.empty top Nothing)

545 |               _ => do logNF "auto" 10 "Next target: " env nty

546 |                       searchLocalVars fc rigc defaults trying' depth def top env nty

547 |   where

548 |     -- Take the earliest error message (that's when we look inside pairs,

549 |     -- typically, and it's best to be more precise)

550 |     tryGroups : Maybe Error ->

551 |                 NF vars -> List (Bool, List Name) -> Core (Term vars)

552 |     tryGroups (Just err) nty [] = throw err

553 |     tryGroups Nothing nty [] = throw (CantSolveGoal fc (gamma !(get Ctxt)) Env.empty top Nothing)

554 |     tryGroups merr nty ((ambigok, g) :: gs)

555 |         = tryUnifyUnambig'

556 |              (do logC "auto" 5

557 |                         (do gn <- traverse getFullName g

558 |                             pure ("Search: Trying " ++ show (length gn) ++

559 |                                            " names " ++ show gn))

560 |                  logNF "auto" 5 "For target" env nty

561 |                  tryNoDefaultsFirst $ \d =>

562 |                    searchNames fc rigc d (target :: trying) depth def top env ambigok g nty)

563 |              (\err => tryGroups (Just $ fromMaybe err merr) nty gs)

573 | Core.Unify.search fc rigc defaults depth def top env

574 |     = do logTermNF "auto" 3 "Initial target: " env top

575 |          log "auto" 3 $ "Running search with defaults " ++ show defaults

576 |          tm <- searchType fc rigc defaults [] depth def

577 |                           True (abstractEnvType fc env top) env

578 |                           top

579 |          logTermNF "auto" 3 "Result" env tm

580 |          pure tm