0 | module TTImp.Interactive.ExprSearch

 12 | import Core.AutoSearch

 13 | import Core.Case.CaseTree

 14 | import Core.Env

 15 | import Core.LinearCheck

 16 | import Core.Metadata

 17 | import Core.Unify

 18 | import Core.Value

 20 | import Idris.REPL.Opts

 21 | import Idris.Syntax

 23 | import TTImp.Elab.Check

 24 | import TTImp.TTImp

 25 | import TTImp.TTImp.Functor

 26 | import TTImp.Unelab

 27 | import TTImp.Utils

 29 | import Libraries.Data.List.SizeOf

 30 | import Libraries.Data.Tap

 31 | import Libraries.Data.WithDefault

 33 | %default covering

 37 | record RecData where

 38 |   constructor MkRecData

 39 |   {localVars : Scope}

 40 |   recname : Name -- resolved name

 41 |   lhsapp : Term localVars

 44 | ExprDefs : Type

 45 | ExprDefs = List ImpDecl

 48 | one : a -> Core (Search a)

 49 | one res = pure $ res :: pure []

 52 | noResult : Core (Search a)

 53 | noResult = pure []

 56 | searchN : {auto c : Ref Ctxt Defs} ->

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

 58 |           Nat -> Core (Search a) -> Core (List a, Core (Search a))

 59 | searchN max s

 60 |     = do startTimer (searchTimeout !getSession) "expression search"

 61 |          tryUnify

 62 |            (do res <- s

 63 |                xs <- count max res

 64 |                clearTimer

 65 |                pure xs)

 66 |            (do clearTimer

 67 |                pure ([], pure []))

 68 |   where

 69 |     count : Nat -> Search a -> Core (List a, Core (Search a))

 70 |     count k [] = pure ([], pure [])

 71 |     count Z _ = pure ([], pure [])

 72 |     count (S Z) (a :: next) = pure ([a], next)

 73 |     count (S k) (a :: next)

 74 |         = do (rest, cont) <- count k !next

 75 |              pure $ (a :: rest, cont)

 80 | searchSort : {auto c : Ref Ctxt Defs} ->

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

 82 |              Nat -> Core (Search a) ->

 83 |              (a -> a -> Ordering) ->

 84 |              Core (Search a)

 85 | searchSort max s ord

 86 |     = do (batch, next) <- searchN max s

 87 |          if isNil batch

 88 |             then pure []

 89 |             else returnBatch (sortBy ord batch) next

 90 |   where

 91 |     returnBatch : List a -> Core (Search a) -> Core (Search a)

 92 |     returnBatch [] res = searchSort max res ord

 93 |     returnBatch (res :: xs) x

 94 |         = pure (res :: returnBatch xs x)

 97 | nextResult : {auto c : Ref Ctxt Defs} ->

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

 99 |              Core (Search a) -> Core (Maybe (a, Core (Search a)))

100 | nextResult s

101 |     = tryUnify

102 |          (do res <- s

103 |              case res of

104 |                   [] => pure Nothing

105 |                   r :: next => pure (Just (r, next)))

106 |          (pure Nothing)

108 | public export

109 | record SearchOpts where

110 |   constructor MkSearchOpts

111 |   holesOK : Bool -- add a hole on getting stuck, rather than an error

112 |   getRecData : Bool -- update the LHS data

113 |   recData : Maybe RecData -- LHS, to help build recursive calls

114 |   depth : Nat -- maximum search depth

115 |   inArg : Bool -- in an argument (not top level). Here, try recursive calls

116 |                -- before constructors, otherwise try recursive calls last

117 |   inUnwrap : Bool

118 |   ltor : Bool -- case split left to right

119 |               -- (right to left is good for auxiliary definitions, because

120 |               -- then we split on the new pattern first)

121 |   mustSplit : Bool -- must begin with a case split (in a case helper)

122 |   doneSplit : Bool -- definitely under a case split

123 |   genExpr : Maybe (SearchOpts -> Name -> Nat -> ClosedTerm ->

124 |                    Core (Search (FC, List ImpClause)))

127 | initSearchOpts : (rec : Bool) -> (maxDepth : Nat) -> SearchOpts

128 | initSearchOpts rec depth

129 |     = MkSearchOpts False rec Nothing depth

130 |                    False False True False False

131 |                    Nothing

133 | search : {auto c : Ref Ctxt Defs} ->

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

135 |          FC -> RigCount ->

136 |          SearchOpts -> List Name -> ClosedTerm ->

137 |          Name -> Core (Search (ClosedTerm, ExprDefs))

139 | getAllEnv : {vars : _} -> FC ->

140 |             SizeOf done ->

141 |             Env Term vars ->

142 |             -- TODO should be `vars <>< done`

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

144 | getAllEnv fc done [] = []

145 | getAllEnv {vars = v :: vs} {done} fc p (b :: env)

146 |    = let rest = getAllEnv fc (sucR p) env

147 |          0 var = mkIsVar (hasLength p)

148 |          usable = usableName v in

149 |          if usable

150 |             then (Local fc Nothing _ var,

151 |                      rewrite appendAssociative done [v] vs in

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

153 |                              rewrite appendAssociative done [v] vs in rest

154 |             else rewrite appendAssociative done [v] vs in rest

155 |   where

156 |     usableName : Name -> Bool

157 |     usableName (UN _) = True

158 |     usableName _ = False

161 | searchIfHole : {vars : _} ->

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

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

164 |                FC -> SearchOpts -> List Name -> ClosedTerm ->

165 |                Env Term vars -> ArgInfo vars ->

166 |                Core (Search (Term vars, ExprDefs))

167 | searchIfHole fc opts hints topty env arg

168 |     = case depth opts of

169 |            Z => noResult

170 |            S k =>

171 |               do let hole = holeID arg

172 |                  let rig = argRig arg

173 |                  defs <- get Ctxt

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

175 |                       | Nothing => noResult

176 |                  let Hole _ _ = definition gdef

177 |                       | _ => one (!(normaliseHoles defs env (metaApp arg)), [])

178 |                                 -- already solved

179 |                  res <- search fc rig ({ depth := k,

180 |                                          inArg := True } opts) hints

181 |                                topty (Resolved hole)

182 |                  -- When we solve an argument, we're also building a lambda

183 |                  -- expression for its environment, so we need to apply it to

184 |                  -- the current environment to use it as an argument.

185 |                  traverse (\(tm, ds) =>

186 |                     pure (!(normaliseHoles defs env

187 |                              (applyTo fc (embed tm) env)), ds)) res

189 | explicit : ArgInfo vars -> Bool

190 | explicit ai

191 |     = case plicit ai of

192 |            Explicit => True

193 |            _ => False

195 | firstSuccess : {auto c : Ref Ctxt Defs} ->

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

197 |                List (Core (Search a)) ->

198 |                Core (Search a)

199 | firstSuccess [] = noResult

200 | firstSuccess (elab :: elabs)

201 |     = do ust <- get UST

202 |          defs <- get Ctxt

203 |          catch (do res :: more <- elab

204 |                       | [] => continue ust defs elabs

205 |                    pure (res :: continue ust defs (more :: elabs)))

206 |                (\err =>

207 |                     case err of

208 |                          -- Give up on timeout, or we'll keep trying all the

209 |                          -- other branches.

210 |                          Timeout _ => noResult

211 |                          _ => continue ust defs elabs)

212 |   where

213 |     continue : UState -> Defs -> List (Core (Search a)) ->

214 |                Core (Search a)

215 |     continue ust defs elabs

216 |         = do put UST ust

217 |              put Ctxt defs

218 |              firstSuccess elabs

222 | trySearch : {auto c : Ref Ctxt Defs} ->

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

224 |             Core (Search a) ->

225 |             Core (Search a) ->

226 |             Core (Search a)

227 | trySearch s1 s2 = firstSuccess [s1, s2]

230 | combine : {auto c : Ref Ctxt Defs} ->

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

232 |           (a -> b -> t) -> Search a -> Search b -> Core (Search t)

233 | combine f [] y = pure []

234 | combine f (x :: next) [] = pure []

235 | combine f (x :: nextx) (y :: nexty)

236 |     = pure $ (::) (f x y) $

237 |                      (do nexty' <- nexty

238 |                          combine f !(one x) nexty')

239 |                          `trySearch`

240 |                      ((do nextx' <- nextx

241 |                           combine f nextx' !(one y))

242 |                           `trySearch`

243 |                       (do nextx' <- nextx

244 |                           nexty' <- nexty

245 |                           combine f nextx' nexty'))

247 | mkCandidates : {vars : _} ->

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

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

250 |                FC -> Term vars -> ExprDefs ->

251 |                List (Search (Term vars, ExprDefs)) ->

252 |                Core (Search (Term vars, ExprDefs))

254 | mkCandidates fc f ds [] = one (f, ds)

256 | mkCandidates fc f ds ([] :: argss) = noResult

258 | mkCandidates fc f ds (((arg, ds') :: next) :: argss)

259 |     = firstSuccess

260 |            [mkCandidates fc (App fc f arg) (ds ++ ds') argss,

261 |             do next' <- next

262 |                mkCandidates fc f ds (next' :: argss)]

267 | searchName : {vars : _} ->

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

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

270 |              FC -> RigCount -> SearchOpts -> List Name ->

271 |              Env Term vars -> NF vars -> ClosedTerm ->

272 |              (Name, GlobalDef) ->

273 |              Core (Search (Term vars, ExprDefs))

274 | searchName fc rigc opts hints env target topty (n, ndef)

275 |     = do defs <- get Ctxt

276 |          checkTimer

277 |          let True = visibleInAny (!getNS :: !getNestedNS)

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

279 |              | _ => noResult

280 |          let ty = type ndef

281 |          let True = usableName (fullname ndef)

282 |              | _ => noResult

283 |          log "interaction.search" 5 $ "Trying " ++ show (fullname ndef)

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

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

286 |          logNF "interaction.search" 5 "Target" env target

287 |          logNF "interaction.search" 10 "App type" env appTy

288 |          ures <- unify inSearch fc env target appTy

289 |          let [] = constraints ures

290 |              | _ => noResult

291 |          -- Search the explicit arguments first, they may resolve other holes

292 |          traverse_ (searchIfHole fc opts hints topty env)

293 |                    (filter explicit args)

294 |          args' <- traverse (searchIfHole fc opts hints topty env)

295 |                            args

296 |          mkCandidates fc (Ref fc (getDefNameType ndef) n) [] args'

297 |   where

298 |     -- we can only use the name in a search result if it's a user writable

299 |     -- name (so, no recursive with blocks or case blocks, for example)

300 |     usableName : Name -> Bool

301 |     usableName (UN _) = True

302 |     usableName (NS _ n) = usableName n

303 |     usableName (Nested _ n) = usableName n

304 |     usableName _ = False

306 | getSuccessful : {vars : _} ->

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

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

309 |                 FC -> RigCount -> SearchOpts -> Bool ->

310 |                 Env Term vars -> Term vars -> ClosedTerm ->

311 |                 List (Core (Search (Term vars, ExprDefs))) ->

312 |                 Core (Search (Term vars, ExprDefs))

313 | getSuccessful {vars} fc rig opts mkHole env ty topty all

314 |     = do res <- firstSuccess all

315 |          case res of

316 |               [] => -- If no successful search, make a hole

317 |                 if mkHole && holesOK opts

318 |                    then do defs <- get Ctxt

319 |                            let base = maybe "arg"

320 |                                             (\r => nameRoot (recname r) ++ "_rhs")

321 |                                             (recData opts)

322 |                            hn <- uniqueBasicName defs (toList $ map nameRoot vars) base

323 |                            (idx, tm) <- newMeta fc rig env (UN $ Basic hn) ty

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

325 |                                                 False

326 |                            one (tm, [])

327 |                    else noResult

328 |               r => pure r

330 | searchNames : {vars : _} ->

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

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

333 |               FC -> RigCount -> SearchOpts -> List Name -> Env Term vars ->

334 |               Term vars -> ClosedTerm ->

335 |               List Name -> Core (Search (Term vars, ExprDefs))

336 | searchNames fc rig opts hints env ty topty []

337 |     = noResult

338 | searchNames fc rig opts hints env ty topty (n :: ns)

339 |     = do defs <- get Ctxt

340 |          checkTimer

341 |          vis <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)

342 |          let visns = mapMaybe id vis

343 |          nfty <- nf defs env ty

344 |          logTerm "interaction.search" 10 ("Searching " ++ show (map fst visns) ++ " for ") ty

345 |          getSuccessful fc rig opts False env ty topty

346 |             (map (searchName fc rig opts hints env nfty topty) visns)

347 |   where

348 |     visible : Context -> List Namespace -> Name ->

349 |               Core (Maybe (Name, GlobalDef))

350 |     visible gam nspace n

351 |         = do Just def <- lookupCtxtExact n gam

352 |                   | Nothing => pure Nothing

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

354 |                 then pure (Just (n, def))

355 |                 else pure Nothing

357 | tryRecursive : {vars : _} ->

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

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

360 |                FC -> RigCount -> SearchOpts -> List Name ->

361 |                Env Term vars -> Term vars -> ClosedTerm ->

362 |                RecData -> Core (Search (Term vars, ExprDefs))

363 | tryRecursive fc rig opts hints env ty topty rdata

364 |     = do defs <- get Ctxt

365 |          case !(lookupCtxtExact (recname rdata) (gamma defs)) of

366 |               Nothing => noResult

367 |               Just def =>

368 |                 do res <- searchName fc rig ({ recData := Nothing } opts) hints

369 |                                      env !(nf defs env ty)

370 |                                      topty (recname rdata, def)

371 |                    res' <- traverse (\ (t, ds) => pure (!(toFullNames t), ds)) res

372 |                    filter (structDiffTm (lhsapp rdata)) res'

373 |   where

374 |     mutual

375 |       -- A fairly simple superficialy syntactic check to make sure that

376 |       -- the recursive call is structurally different from the lhs

377 |       -- (Essentially, meaning that there's a constructor application in

378 |       -- one where there's a local in another, or that constructor applications

379 |       -- differ somewhere)

380 |       argDiff : Term vs -> Term vs' -> Bool

381 |       argDiff (Local {}) _ = False

382 |       argDiff (Ref _ _ fn) (Ref _ _ fn') = fn /= fn'

383 |       argDiff (Bind {}) _ = False

384 |       argDiff _ (Bind {}) = False

385 |       argDiff (App _ f a) (App _ f' a')

386 |          = structDiff f f' || structDiff a a'

387 |       argDiff (PrimVal _ c) (PrimVal _ c') = c /= c'

388 |       argDiff (Erased {}) _ = False

389 |       argDiff _ (Erased {}) = False

390 |       argDiff (TType {}) (TType {}) = False

391 |       argDiff (As _ _ _ x) y = argDiff x y

392 |       argDiff x (As _ _ _ y) = argDiff x y

393 |       argDiff _ _ = True

395 |       appsDiff : Term vs -> Term vs' -> List (Term vs) -> List (Term vs') ->

396 |                  Bool

397 |       appsDiff (Ref _ (DataCon {}) f) (Ref _ (DataCon {}) f') args args'

398 |          = f /= f' || any (uncurry argDiff) (zip args args')

399 |       appsDiff (Ref _ (TyCon _) f) (Ref _ (TyCon _) f') args args'

400 |          = f /= f' || any (uncurry argDiff) (zip args args')

401 |       appsDiff (Ref _ _ f) (Ref _ _ f') args args'

402 |          = f == f'

403 |            && length args == length args'

404 |            && any (uncurry argDiff) (zip args args')

405 |       appsDiff (Ref _ (DataCon {}) f) (Local {}) _ _ = True

406 |       appsDiff (Local {}) (Ref _ (DataCon {}) f) _ _ = True

407 |       appsDiff f f' [] [] = argDiff f f'

408 |       appsDiff _ _ _ _ = False -- can't be sure...

410 |       -- Reject if the recursive call is the same in structure as the lhs

411 |       structDiff : Term vs -> Term vs' -> Bool

412 |       structDiff tm tm'

413 |          = let (f, args) = getFnArgs tm

414 |                (f', args') = getFnArgs tm' in

415 |                appsDiff f f' args args'

417 |       structDiffTm : Term vs -> (Term vs', ExprDefs) -> Bool

418 |       structDiffTm tm (tm', _) = structDiff tm tm'

421 | usableLocal : FC -> Env Term vars -> NF vars -> Bool

422 | usableLocal loc env (NApp _ (NMeta {}) args) = False

423 | usableLocal loc _ _ = True

425 | searchLocalWith : {vars : _} ->

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

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

428 |                   FC -> Bool ->

429 |                   RigCount -> SearchOpts -> List Name -> Env Term vars ->

430 |                   List (Term vars, Term vars) ->

431 |                   Term vars -> ClosedTerm ->

432 |                   Core (Search (Term vars, ExprDefs))

433 | searchLocalWith fc nofn rig opts hints env [] ty topty

434 |     = noResult

435 | searchLocalWith {vars} fc nofn rig opts hints env ((p, pty) :: rest) ty topty

436 |     = do defs <- get Ctxt

437 |          checkTimer

438 |          nty <- nf defs env ty

439 |          getSuccessful fc rig opts False env ty topty

440 |                        [findPos defs p id !(nf defs env pty) nty,

441 |                         searchLocalWith fc nofn rig opts hints env rest ty

442 |                                         topty]

443 |   where

444 |     findDirect : Defs -> Term vars ->

445 |                  (Term vars -> Term vars) ->

446 |                  NF vars -> -- local variable's type

447 |                  NF vars -> -- type we're looking for

448 |                  Core (Search (Term vars, ExprDefs))

449 |     findDirect defs prf f nty ty

450 |         = do (args, appTy) <- mkArgs fc rig env nty

451 |              -- We can only use a local variable if it's not an unsolved

452 |              -- hole

453 |              if usableLocal fc env nty

454 |                 then

455 |                   tryUnify -- try with no arguments first

456 |                     (do when (not (isNil args) && nofn) $

457 |                              throw (InternalError "Must apply function")

458 |                         ures <- unify inTerm fc env ty nty

459 |                         let [] = constraints ures

460 |                             | _ => throw (InternalError "Can't use directly")

461 |                         mkCandidates fc (f prf) [] [])

462 |                     (do ures <- unify inTerm fc env ty appTy

463 |                         let [] = constraints ures

464 |                             | _ => noResult

465 |                         args' <- traverse (searchIfHole fc opts hints topty env)

466 |                                           args

467 |                         mkCandidates fc (f prf) [] args')

468 |                 else noResult

470 |     findPos : Defs -> Term vars ->

471 |               (Term vars -> Term vars) ->

472 |               NF vars -> NF vars -> Core (Search (Term vars, ExprDefs))

473 |     findPos defs prf f x@(NTCon pfc pn _ [(fc1, xty), (fc2, yty)]) target

474 |         = getSuccessful fc rig opts False env ty topty

475 |               [findDirect defs prf f x target,

476 |                  (do fname <- maybe (throw (InternalError "No fst"))

477 |                                     pure

478 |                                     !fstName

479 |                      sname <- maybe (throw (InternalError "No snd"))

480 |                                     pure

481 |                                     !sndName

482 |                      if !(isPairType pn)

483 |                         then do empty <- clearDefs defs

484 |                                 xtytm <- quote empty env xty

485 |                                 ytytm <- quote empty env yty

486 |                                 getSuccessful fc rig opts False env ty topty

487 |                                   [(do xtynf <- evalClosure defs xty

488 |                                        findPos defs prf

489 |                                          (\arg => applyStackWithFC (Ref fc Func fname)

490 |                                                           [(fc1, xtytm),

491 |                                                            (fc2, ytytm),

492 |                                                            (fc, f arg)])

493 |                                          xtynf target),

494 |                                    (do ytynf <- evalClosure defs yty

495 |                                        findPos defs prf

496 |                                            (\arg => applyStackWithFC (Ref fc Func sname)

497 |                                                           [(fc1, xtytm),

498 |                                                            (fc2, ytytm),

499 |                                                            (fc, f arg)])

500 |                                            ytynf target)]

501 |                          else noResult)]

502 |     findPos defs prf f nty target = findDirect defs prf f nty target

504 | searchLocal : {vars : _} ->

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

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

507 |               FC -> RigCount -> SearchOpts -> List Name ->

508 |               Env Term vars -> Term vars -> ClosedTerm ->

509 |               Core (Search (Term vars, ExprDefs))

510 | searchLocal fc rig opts hints env ty topty

511 |     = -- Reverse the environment so we try the patterns left to right.

512 |       -- This heuristic is just so arguments appear the same order in

513 |       -- recursive calls

514 |       searchLocalWith fc False rig opts hints env (reverse (getAllEnv fc zero env))

515 |                       ty topty

517 | makeHelper : {vars : _} ->

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

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

520 |              FC -> RigCount -> SearchOpts ->

521 |              Env Term vars ->

522 |              Term vars -> Term vars -> Search (Term vars, ExprDefs) ->

523 |              Core (Search (Term vars, ExprDefs))

524 | makeHelper fc rig opts env letty targetty []

525 |     = pure []

526 | makeHelper fc rig opts env letty targetty ((locapp, ds) :: next)

527 |     = do let S depth' = depth opts

528 |              | Z => noResult

529 |          logTerm "interaction.search" 10 "Local app" locapp

530 |          let Just gendef = genExpr opts

531 |              | Nothing => noResult

532 |          intn <- genVarName "cval"

533 |          helpern_in <- genCaseName "search"

534 |          helpern <- inCurrentNS helpern_in

535 |          let env' = Lam fc top Explicit letty :: env

536 |          scopeMeta <- metaVar fc top env' helpern

537 |                              (weaken targetty)

538 |          let scope = toApp scopeMeta

539 |          updateDef helpern (const (Just None))

540 |          -- Apply the intermediate result to the helper function we're

541 |          -- about to generate.

542 |          let def = App fc (Bind fc intn (Lam fc top Explicit letty) scope)

543 |                           locapp

545 |          logTermNF "interaction.search" 10 "Binding def" env def

546 |          defs <- get Ctxt

547 |          Just ty <- lookupTyExact helpern (gamma defs)

548 |              | Nothing => throw (InternalError "Can't happen")

549 |          logTermNF "interaction.search" 10 "Type of scope name" Env.empty ty

551 |          -- Generate a definition for the helper, but with more restrictions.

552 |          -- Always take the first result, to avoid blowing up search space.

553 |          -- Go right to left on variable split, to get the variable we just

554 |          -- added first.

555 |          -- There must be at least one case split.

556 |          ((helper :: _), nextdef) <-

557 |                     searchN 1 $ gendef ({ getRecData := False,

558 |                                           inUnwrap := True,

559 |                                           depth := depth',

560 |                                           ltor := False,

561 |                                           mustSplit := True } opts)

562 |                                        helpern 0 ty

563 |               | _ => do log "interaction.search" 10 "No results"

564 |                         noResult

566 |          let helperdef = IDef fc helpern (snd helper)

567 |          log "interaction.search" 10 $ "Def: " ++ show helperdef

568 |          pure ((::) (def, helperdef :: ds) -- plus helper

569 |                       (do next' <- next

570 |                           makeHelper fc rig opts env letty targetty next'))

571 |   where

572 |     -- convert a metavar application (as created by 'metaVar') to a normal

573 |     -- application (as required by a case block)

574 |     toApp : forall vars . Term vars -> Term vars

575 |     toApp (Meta fc n i args) = apply fc (Ref fc Func (Resolved i)) args

576 |     toApp tm = tm

579 | tryIntermediateWith : {vars : _} ->

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

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

582 |                       FC -> RigCount -> SearchOpts -> List Name ->

583 |                       Env Term vars -> List (Term vars, Term vars) ->

584 |                       Term vars -> ClosedTerm ->

585 |                       Core (Search (Term vars, ExprDefs))

586 | tryIntermediateWith fc rig opts hints env [] ty topty = noResult

587 | tryIntermediateWith fc rig opts hints env ((p, pty) :: rest) ty topty

588 |     = do defs <- get Ctxt

589 |          getSuccessful fc rig opts False env ty topty

590 |                        [applyLocal defs p !(nf defs env pty) ty,

591 |                         tryIntermediateWith fc rig opts hints env rest ty

592 |                                             topty]

593 |   where

594 |     matchable : Defs -> NF vars -> Core Bool

595 |     matchable defs (NBind fc x (Pi {}) sc)

596 |         = matchable defs !(sc defs (toClosure defaultOpts env

597 |                                               (Erased fc Placeholder)))

598 |     matchable defs (NTCon {}) = pure True

599 |     matchable _ _ = pure False

601 |     applyLocal : Defs -> Term vars ->

602 |                  NF vars -> Term vars -> Core (Search (Term vars, ExprDefs))

603 |     applyLocal defs tm locty@(NBind _ x (Pi fc' _ _ _) sc) targetty

604 |         = -- If the local has a function type, and the return type is

605 |           -- something we can pattern match on (so, NTCon) then apply it,

606 |           -- let bind the result, and try to generate a definition for

607 |           -- the scope of the let binding

608 |           do True <- matchable defs

609 |                            !(sc defs (toClosure defaultOpts env

610 |                                                 (Erased fc Placeholder)))

611 |                  | False => noResult

612 |              intnty <- genVarName "cty"

613 |              u <- uniVar fc

614 |              letty <- metaVar fc' erased env intnty (TType fc u)

615 |              let opts' = { inUnwrap := True } opts

616 |              locsearch <- searchLocalWith fc True rig opts' hints env [(p, pty)]

617 |                                           letty topty

618 |              makeHelper fc rig opts env letty targetty locsearch

619 |     applyLocal defs tm _ _ = noResult

624 | tryIntermediate : {vars : _} ->

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

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

627 |                   FC -> RigCount -> SearchOpts -> List Name ->

628 |                   Env Term vars -> Term vars -> ClosedTerm ->

629 |                   Core (Search (Term vars, ExprDefs))

630 | tryIntermediate fc rig opts hints env ty topty

631 |     = tryIntermediateWith fc rig opts hints env (reverse (getAllEnv fc zero env))

632 |                           ty topty

638 | tryIntermediateRec : {vars : _} ->

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

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

641 |                      FC -> RigCount -> SearchOpts -> List Name ->

642 |                      Env Term vars ->

643 |                      Term vars -> ClosedTerm ->

644 |                      Maybe RecData -> Core (Search (Term vars, ExprDefs))

645 | tryIntermediateRec fc rig opts hints env ty topty Nothing = noResult

646 | tryIntermediateRec fc rig opts hints env ty topty (Just rd)

647 |     = do defs <- get Ctxt

648 |          Just rty <- lookupTyExact (recname rd) (gamma defs)

649 |               | Nothing => noResult

650 |          True <- isSingleCon defs !(nf defs Env.empty rty)

651 |               | _ => noResult

652 |          intnty <- genVarName "cty"

653 |          u <- uniVar fc

654 |          letty <- metaVar fc erased env intnty (TType fc u)

655 |          let opts' = { inUnwrap := True,

656 |                        recData := Nothing } opts

657 |          logTerm "interaction.search" 10 "Trying recursive search for" ty

658 |          logC "interaction.search" 10 $ show <$> toFullNames (recname rd)

659 |          logTerm "interaction.search" 10 "LHS" !(toFullNames (lhsapp rd))

660 |          recsearch <- tryRecursive fc rig opts' hints env letty topty rd

661 |          makeHelper fc rig opts' env letty ty recsearch

662 |   where

663 |     isSingleCon : Defs -> ClosedNF -> Core Bool

664 |     isSingleCon defs (NBind fc x (Pi {}) sc)

665 |         = isSingleCon defs !(sc defs (toClosure defaultOpts Env.empty

666 |                                               (Erased fc Placeholder)))

667 |     isSingleCon defs (NTCon _ n _ _)

668 |         = do Just (TCon _ _ _ _ _ (Just [con]) _) <- lookupDefExact n (gamma defs)

669 |                   | _ => pure False

670 |              pure True

671 |     isSingleCon _ _ = pure False

673 | searchType : {vars : _} ->

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

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

676 |              FC -> RigCount -> SearchOpts -> List Name -> Env Term vars ->

677 |              ClosedTerm ->

678 |              Nat -> Term vars -> Core (Search (Term vars, ExprDefs))

679 | searchType fc rig opts hints env topty (S k) (Bind bfc n b@(Pi fc' c info ty) sc)

680 |     = do let env' : Env Term (n :: _) = b :: env

681 |          log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc

682 |          scVal <- searchType fc rig opts hints env' topty k sc

683 |          pure (map (\ (sc, ds) => (Bind bfc n (Lam fc' c info ty) sc, ds)) scVal)

684 | searchType {vars} fc rig opts hints env topty Z (Bind bfc n b@(Pi fc' c info ty) sc)

685 |     = -- try a local before creating a lambda...

686 |       getSuccessful fc rig opts False env ty topty

687 |            [searchLocal fc rig opts hints env (Bind bfc n b sc) topty,

688 |             (do defs <- get Ctxt

689 |                 let n' = UN $ Basic !(getArgName defs n [] (toList vars) !(nf defs env ty))

690 |                 let env' : Env Term (n' :: _) = b :: env

691 |                 let sc' = compat sc

692 |                 log "interaction.search" 10 $ "Introduced lambda, search for " ++ show sc'

693 |                 scVal <- searchType fc rig opts hints env' topty Z sc'

694 |                 pure (map (\ (sc, ds) =>

695 |                              (Bind bfc n' (Lam fc' c info ty) sc, ds)) scVal))]

696 | searchType fc rig opts hints env topty _ ty

697 |     = case getFnArgs ty of

698 |            (Ref rfc (TyCon ar) n, args) =>

699 |                 do defs <- get Ctxt

700 |                    if length args == ar

701 |                      then do sd <- getSearchData fc False n

702 |                              let allHints = concat (map snd (hintGroups sd)) ++ hints

703 |                              -- Solutions is either:

704 |                              -- First try the locals,

705 |                              -- Then try the hints in order

706 |                              -- Then try a recursive call

707 |                              log "interaction.search" 10 $ "Hints found for " ++ show n ++ " "

708 |                                          ++ show allHints

709 |                              let tries =

710 |                                    [searchLocal fc rig opts hints env ty topty,

711 |                                     searchNames fc rig opts hints env ty topty allHints]

712 |                              let tryRec =

713 |                                    case recData opts of

714 |                                         Nothing => []

715 |                                         Just rd => [tryRecursive fc rig opts hints env ty topty rd]

716 |                              let tryIntRec =

717 |                                    if doneSplit opts

718 |                                       then [tryIntermediateRec fc rig opts hints env ty topty (recData opts)]

719 |                                       else []

720 |                              let tryInt = if not (inUnwrap opts)

721 |                                              then [tryIntermediate fc rig opts hints env ty topty]

722 |                                              else []

723 |                              -- if we're in an argument, try the recursive call

724 |                              -- first. We're more likely to want that than nested

725 |                              -- constructors.

726 |                              let allns : List _

727 |                                      = if inArg opts

728 |                                           then tryRec ++ tryInt ++ tries

729 |                                           else tryInt ++ tries ++ tryRec ++ tryIntRec

730 |                              getSuccessful fc rig opts True env ty topty allns

731 |                      else noResult

732 |            _ => do logTerm "interaction.search" 10 "Searching locals only at" ty

733 |                    let tryInt = if not (inUnwrap opts)

734 |                                    then [tryIntermediate fc rig opts hints env ty topty]

735 |                                    else []

736 |                    let tryIntRec = if inArg opts || not (doneSplit opts)

737 |                                       then []

738 |                                       else [tryIntermediateRec fc rig opts hints env ty topty (recData opts)]

739 |                    getSuccessful fc rig opts True env ty topty

740 |                            (tryInt ++ [searchLocal fc rig opts hints env ty topty]

741 |                              ++ case recData opts of

742 |                                      Nothing => []

743 |                                      Just rd => [tryRecursive fc rig opts hints env ty topty rd]

744 |                              ++ tryIntRec)

746 | searchHole : {auto c : Ref Ctxt Defs} ->

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

748 |              FC -> RigCount -> SearchOpts -> List Name -> Name ->

749 |              Nat -> ClosedTerm ->

750 |              Defs -> GlobalDef -> Core (Search (ClosedTerm, ExprDefs))

751 | searchHole fc rig opts hints n locs topty defs glob

752 |     = do searchty <- normalise defs Env.empty (type glob)

753 |          logTerm "interaction.search" 10 "Normalised type" searchty

754 |          checkTimer

755 |          searchType fc rig opts hints Env.empty topty locs searchty

758 | search fc rig opts hints topty n_in

759 |     = do defs <- get Ctxt

760 |          case !(lookupHoleName n_in (gamma defs)) of

761 |               Just (n, i, gdef) =>

762 |                    -- The definition should be 'BySearch' at this stage,

763 |                    -- if it's arising from an auto implicit

764 |                    case definition gdef of

765 |                         Hole locs _ => searchHole fc rig opts hints n locs topty defs gdef

766 |                         BySearch {} => searchHole fc rig opts hints n

767 |                                                    !(getArity defs Env.empty (type gdef))

768 |                                                    topty defs gdef

769 |                         _ => do log "interaction.search" 10 $ show n_in ++ " not a hole"

770 |                                 throw (InternalError $ "Not a hole: " ++ show n ++ " in " ++

771 |                                         show (map recname (recData opts)))

772 |               _ => do log "interaction.search" 10 $ show n_in ++ " not found"

773 |                       undefinedName fc n_in

774 |   where

775 |     lookupHoleName : Name -> Context ->

776 |                      Core (Maybe (Name, Int, GlobalDef))

777 |     lookupHoleName n defs

778 |         = case !(lookupCtxtExactI n defs) of

779 |                Just (i, res) => pure $ Just (n, i, res)

780 |                Nothing => case !(lookupCtxtName n defs) of

781 |                                [res] => pure $ Just res

782 |                                _ => pure Nothing

784 | getLHSData : {auto c : Ref Ctxt Defs} ->

785 |              Defs -> Maybe ClosedTerm -> Core (Maybe RecData)

786 | getLHSData defs Nothing = pure Nothing

787 | getLHSData defs (Just tm)

788 |     = pure $ getLHS !(toFullNames !(normaliseHoles defs Env.empty tm))

789 |   where

790 |     getLHS : {vars : _} -> Term vars -> Maybe RecData

791 |     getLHS (Bind _ _ (PVar {}) sc) = getLHS sc

792 |     getLHS (Bind _ _ (PLet {}) sc) = getLHS sc

793 |     getLHS sc

794 |         = case getFn sc of

795 |                Ref _ _ n => Just (MkRecData n sc)

796 |                _ => Nothing

798 | firstLinearOK : {auto c : Ref Ctxt Defs} ->

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

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

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

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

803 |                 FC -> Search (ClosedTerm, ExprDefs) ->

804 |                 Core (Search RawImp)

805 | firstLinearOK fc [] = noResult

806 | firstLinearOK fc ((t, ds) :: next)

807 |     = handleUnify

808 |             (do unless (isNil ds) $

809 |                    traverse_ (processDecl [InCase] (MkNested []) Env.empty) ds

810 |                 ignore $ linearCheck fc linear False Env.empty t

811 |                 defs <- get Ctxt

812 |                 nft <- normaliseHoles defs Env.empty t

813 |                 raw <- unelab Env.empty !(toFullNames nft)

814 |                 pure (map rawName raw :: firstLinearOK fc !next))

815 |             (\err =>

816 |                 do next' <- next

817 |                    firstLinearOK fc next')

820 | exprSearchOpts : {auto c : Ref Ctxt Defs} ->

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

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

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

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

825 |                  SearchOpts -> FC -> Name -> List Name ->

826 |                  Core (Search RawImp)

827 | exprSearchOpts opts fc n_in hints

828 |     = do defs <- get Ctxt

829 |          Just (n, idx, gdef) <- lookupHoleName n_in defs

830 |              | Nothing => undefinedName fc n_in

831 |          -- the REPL does this step, but doing it here too because

832 |          -- expression search might be invoked some other way

833 |          let Hole _ _ = definition gdef

834 |              | PMDef pi [] (STerm _ tm) _ _

835 |                  => do raw <- unelab Env.empty !(toFullNames !(normaliseHoles defs Env.empty tm))

836 |                        one (map rawName raw)

837 |              | _ => throw (GenericMsg fc "Name is already defined")

838 |          lhs <- findHoleLHS !(getFullName (Resolved idx))

839 |          log "interaction.search" 10 $ "LHS hole data " ++ show (n, lhs)

840 |          opts' <- if getRecData opts

841 |                      then do d <- getLHSData defs lhs

842 |                              pure ({ recData := d } opts)

843 |                      else pure opts

844 |          validHints <- concat <$> for hints (\hint => do

845 |            defs <- get Ctxt

846 |            entries <- lookupCtxtName hint (gamma defs)

847 |            pure $ map (Resolved . fst . snd) entries)

848 |          res <- search fc (multiplicity gdef) opts' validHints (type gdef) n

849 |          firstLinearOK fc res

850 |   where

851 |     lookupHoleName : Name -> Defs -> Core (Maybe (Name, Int, GlobalDef))

852 |     lookupHoleName n defs

853 |         = case !(lookupCtxtExactI n (gamma defs)) of

854 |                Just (idx, res) => pure $ Just (n, idx, res)

855 |                Nothing => case !(lookupCtxtName n (gamma defs)) of

856 |                                [res] => pure $ Just res

857 |                                _ => pure Nothing

859 | exprSearch' : {auto c : Ref Ctxt Defs} ->

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

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

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

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

864 |               FC -> Name -> List Name ->

865 |               Core (Search RawImp)

866 | exprSearch' = exprSearchOpts (initSearchOpts True 5)

869 | exprSearch : {auto c : Ref Ctxt Defs} ->

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

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

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

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

874 |              FC -> Name -> List Name ->

875 |              Core (Search RawImp)

876 | exprSearch fc n hints

877 |     = do startTimer (searchTimeout !getSession) "expression search"

878 |          res <- exprSearch' fc n hints

879 |          clearTimer

880 |          pure res

883 | exprSearchN : {auto c : Ref Ctxt Defs} ->

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

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

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

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

888 |               FC -> Nat -> Name -> List Name ->

889 |               Core (List RawImp)

890 | exprSearchN fc max n hints

891 |     = do (res, _) <- searchN max (exprSearch fc n hints)

892 |          pure res