just putzing around still but I managed to get some looking up to work just by filtering the list of all global defs.

src/Core/Context/Log.idr

@@ -31,6 +31,8 @@ log' lvl msg
             then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
             else pure ()
 
+||| Log a message with the given log level. Use increasingly
+||| high log level numbers for more granular logging.
 export
 log : {auto c : Ref Ctxt Defs} ->
       String -> Nat -> Lazy String -> Core ()

src/Idris/REPL.idr

@@ -607,7 +607,6 @@ loadMainFile f
            [] => pure (FileLoaded f)
            _ => pure (ErrorsBuildingFile f errs)
 
-
 ||| Process a single `REPLCmd`
 |||
 ||| Returns `REPLResult` for display by the higher level shell which
@@ -714,35 +713,84 @@ process (Exec ctm)
     = execExp ctm
 process Help
     = pure RequestedHelp
-process (ProofSearch (PType fc))
-    = do let ty = gType fc
-         logGlue "repl.ps" 2 "tst" [] ty
-         pure Done
-process (ProofSearch pterm)
-    = do ttimp <- desugar AnyExpr [] pterm 
-         logRaw "repl.ps" 2 "tst" ttimp
-         log "repl.ps" 2 (show (getFn ttimp))
-         let ty = gType (getFC ttimp)
-         logGlue "repl.ps" 2 "gType" [] ty
+process (ProofSearch searchTerm@(PPi fc rc piInfo _ argTy retTy))
+    = do log "repl.ps" 2 $ "piInfo " ++ (show piInfo) ++ "  argTy " ++ (show argTy) ++ "  retTy " ++ (show retTy)
+         defs <- get Ctxt
+         let context = gamma defs
+         allDefs <- map catMaybes $ traverse (flip lookupCtxtExact context) $ !(allNames context)
+         log "repl.ps" 2 $ "Defs: " ++ (show $ length allDefs)
+
+         ttimpSearchTerm <- desugar AnyExpr [] searchTerm
+
          let n = (UN "[input]")
          inidx <- resolveName n 
-         -- (tm1, gl1) <- check top (initElabInfo InType) (MkNested []) [] ttimp Nothing
-         -- logTermNF "repl.ps" 2 "tst" [] tm1
+         (tm, _) <- elabTerm inidx InType [] (MkNested [])
+                                  [] ttimpSearchTerm Nothing
+         logTermNF "repl.ps" 2 "tm" [] tm
+
+         let filteredDefs = (flip filter) allDefs (\def => def.type == tm)
+         log "repl.ps" 2 $ "filtered count: " ++ (show $ length filteredDefs)
+
+         doc <- traverse (getDocsFor replFC) $ (.fullname) <$> filteredDefs
+         pure $ Printed $ vsep $ pretty <$> (intersperse "\n" $ join doc)
+process (ProofSearch pterm)
+    = do log "repl.ps" 2 (show pterm)
+         ttimp <- desugar AnyExpr [] pterm 
+         logRaw "repl.ps" 2 "ttimp from desugar" ttimp
+         log "repl.ps" 2 (show (getFn ttimp))
+         -- let ty = gType (getFC ttimp)
+         -- logGlue "repl.ps" 2 "gType" [] ty
+         let n = (UN "[input]")
+         inidx <- resolveName n 
+         newRef EST (initEState 0 [])
+         (tm1, gl1) <- checkImp top (initElabInfo InType) (MkNested []) [] ttimp Nothing
+         logTermNF "repl.ps" 2 "checkImp generated type" [] tm1
          -- logGlue "repl.ps" 2 "tst" [] gl1
          (tm, gl) <- elabTerm inidx InType [] (MkNested [])
                                   [] ttimp Nothing
-         logTermNF "repl.ps" 2 "tst" [] tm
-         logGlue "repl.ps" 2 "tst" [] gl
+         logTermNF "repl.ps" 2 "tm" [] tm
+         -- logGlue "repl.ps" 2 "glue term" [] gl
 
-         addNameType replFC n [] tm
-         searchResults <- exprSearchN replFC 3 n []
-         pure $ log $ show searchResults
+         -- addNameType replFC n [] tm
+         -- searchResults <- exprSearchN replFC 3 n []
+         -- pure $ log $ show searchResults
 
-         tm' <- search replFC top False 1000 n tm []
+         ty <- checkTerm inidx InType [] (MkNested []) []
+                             (IBindHere replFC (PI erased) ttimp)
+                             (gType replFC)
+         logTerm "repl.ps" 2 "check term result" ty
+         logTermNF "repl.ps" 2 ("Type of " ++ show n) [] (abstractFullEnvType replFC [] ty)
+
+
+         log "repl.pl" 2 ""
+         log "repl.ps" 2 "--- AutoSearch ------"
+
+         tm' <- search replFC top False 1000 n ty [] -- ty or tm?
          defs <- get Ctxt
          fnms <- toFullNames !(normaliseAll defs [] tm')
          itm <- resugar [] fnms
-         logTermNF "repl.ps" 2 "tst" [] fnms
+         logTermNF "repl.ps" 2 "full names from tm'" [] fnms
+
+         log "repl.pl" 2 ""
+         log "repl.ps" 2 "--- Editing Search ------"
+
+         searchty <- normalise defs [] ty -- ty or tm?
+         logTerm "repl.ps" 2 "Normalised type" searchty
+         arity <- getArity defs [] ty -- ty or tm?
+         log "repl.ps" 2 $ "arity : " ++ (show arity)
+         let results = searchType replFC top (initSearchOpts True 1000) [] ty 0 searchty -- replaced arity with 0 -- ty or tm?
+         Just ((resTm, exprDefs), results2) <- nextResult results
+           | Nothing => pure Done
+         logTerm "repl.ps" 2 "1st search result" resTm
+
+         Just ((resTm2, exprDefs2), results3) <- nextResult results2
+           | Nothing => pure Done
+         logTerm "repl.ps" 2 "2nd search result" resTm2
+
+         Just ((resTm3, exprDefs3), results4) <- nextResult results3
+           | Nothing => pure Done
+         logTerm "repl.ps" 2 "3rd search result" resTm3
+
          pure $ ProofFound $ itm
 
 process (Missing n)

src/TTImp/Interactive/ExprSearch.idr

@@ -710,6 +710,7 @@ tryIntermediateRec fc rig opts env ty topty (Just rd)
              pure True
     isSingleCon _ _ = pure False
 
+export
 searchType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->