Merge pull request #1375 from david-christiansen/type-search-in-prover

Make type search work in the prover

src/Idris/AbsSyntaxTree.hs

@@ -762,6 +762,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
                 | TCheck t
                 | TEval t
                 | TDocStr (Either Name Const)
+                | TSearch t
                 | Qed | Abandon
     deriving (Show, Eq, Functor)
 {-!

src/Idris/Output.hs

@@ -78,6 +78,17 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState
         ppOverload ppo infixes n tm =
           fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
 
+ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()
+ihRenderOutput h doc =
+  do i <- getIState
+     case idris_outputmode i of
+       RawOutput -> do out <- iRender doc
+                       runIO $ putStrLn (displayDecorated (consoleDecorate i) out)
+       IdeSlave n ->
+        do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc
+           let out = [toSExp str, toSExp spans]
+           runIO . putStrLn $ convSExp "write-decorated" out n
+
 ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
 ihRenderResult h d = do ist <- getIState
                         case idris_outputmode ist of
@@ -85,7 +96,7 @@ ihRenderResult h d = do ist <- getIState
                           IdeSlave n -> ideSlaveReturnAnnotated n h d
 
 ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
-ideSlaveReturnWithStatus status n h out = do 
+ideSlaveReturnWithStatus status n h out = do
   ist <- getIState
   (str, spans) <- fmap displaySpans .
                   iRender .

src/Idris/ParseExpr.hs

@@ -1298,6 +1298,11 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
                               n <- (fnName <|> (string "_|_" >> return falseTy))
                               eof
                               return (TDocStr (Left n)))
+                  <|> try (do reserved "search"
+                              whiteSpace
+                              t <- (indentPropHolds gtProp *> expr syn);
+                              i <- get
+                              return $ TSearch (desugar syn i t))
                   <?> "prover command")
           <?> "tactic"
   where

src/Idris/Prover.hs

@@ -18,6 +18,7 @@ import Idris.DataOpts
 import Idris.Completion
 import Idris.IdeSlave
 import Idris.Output
+import Idris.TypeSearch (searchByType)
 
 import Text.Trifecta.Result(Result(..))
 
@@ -227,6 +228,7 @@ ploop fn d prompt prf e h
               Success (TCheck t) -> checkType t
               Success (TEval t)  -> evalTerm t e
               Success (TDocStr x) -> docStr x
+              Success (TSearch t) -> search t
               Success tac -> do (_, e) <- elabStep e saveState
                                 (_, st) <- elabStep e (runTac autoSolve i fn tac)
                                 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
@@ -318,3 +320,6 @@ ploop fn d prompt prf e h
         docStr (Right c) = do ist <- getIState
                               let h = idris_outh ist
                               return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))
+        search t = do ist <- getIState
+                      let h = idris_outh ist
+                      return (False, e, False, prf, Right $ searchByType h t)

src/Idris/TypeSearch.hs

@@ -20,20 +20,20 @@ import qualified Data.Set as S
 import qualified Data.Text as T (pack, isPrefixOf)
 
 import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)
-import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris, 
-  IState (idris_classes, idris_docstrings, tt_ctxt),
-  implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)
+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,
+  IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),
+  implicitAllowed, OutputMode(..), prettyDocumentedIst, prettyIst, PTerm, toplevel)
 import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)
 import Idris.Core.TT hiding (score)
 import Idris.Core.Unify (match_unify)
 import Idris.Delaborate (delabTy)
 import Idris.Docstrings (noDocs, overview)
 import Idris.ElabDecls (elabType')
-import Idris.Output (ihRenderResult)
+import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)
 
 import System.IO (Handle)
 
-import Util.Pretty (text, char, (<>), Doc)
+import Util.Pretty (text, char, vsep, (<>), Doc)
 
 searchByType :: Handle -> PTerm -> Idris ()
 searchByType h pterm = do
@@ -49,12 +49,15 @@ searchByType h pterm = do
        [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in
          displayScore score <> char ' ' <> prettyDocumentedIst i docInfo
                 | (n, score) <- names']
-  mapM_ (ihRenderResult h) docs
-  where 
+  case idris_outputmode i of
+    RawOutput -> do mapM_ (ihRenderOutput h) docs
+                    ihPrintResult h ""
+    IdeSlave n -> ihRenderResult h (vsep docs)
+  where
     numLimit = 50
     syn = defaultSyntax { implicitAllowed = True } -- syntax
     n = sMN 0 "searchType" -- name
-  
+
 -- | Conduct a type-directed search using a given match predicate
 searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)]) 
   -> IState -> Type -> [(Name, a)]