7d95bec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make type search work in the prover

This patch does two things: 1. It adds support for a new prover command, :search, with the same syntax and semantics as the REPL command 2. It makes :search work properly with IDESlave, enabling type search from the Emacs prover as well as enabling length-limits in the IRC bot again.

commit7d95beceb6b5f9bf9d7908c40ee74e282cb32bd4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 10 Jul 2014, 20:24 (12 years ago) parent6340534

5 files changed+34−9

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Output.hs+12−1 src/Idris/ParseExpr.hs+5 src/Idris/Prover.hs+5 src/Idris/TypeSearch.hs+11−8

src/Idris/AbsSyntaxTree.hs+1

@@ -762,6 +762,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

762762 | TCheck t

763763 | TEval t

764764 | TDocStr (Either Name Const)

765+ | TSearch t

765766 | Qed | Abandon

766767 deriving (Show, Eq, Functor)

767768{-!

src/Idris/Output.hs+12−1

@@ -78,6 +78,17 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

7878 ppOverload ppo infixes n tm =

7979 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

8080

81+ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()

82+ihRenderOutput h doc =

83+ do i <- getIState

84+ case idris_outputmode i of

85+ RawOutput -> do out <- iRender doc

86+ runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

87+ IdeSlave n ->

88+ do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

89+ let out = [toSExp str, toSExp spans]

90+ runIO . putStrLn $ convSExp "write-decorated" out n

91+

8192ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

8293ihRenderResult h d = do ist <- getIState

8394 case idris_outputmode ist of

@@ -85,7 +96,7 @@ ihRenderResult h d = do ist <- getIState

8596 IdeSlave n -> ideSlaveReturnAnnotated n h d

8697

8798ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

88−ideSlaveReturnWithStatus status n h out = do

99+ideSlaveReturnWithStatus status n h out = do

89100 ist <- getIState

90101 (str, spans) <- fmap displaySpans .

91102 iRender .

src/Idris/ParseExpr.hs+5

@@ -1298,6 +1298,11 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

12981298 n <- (fnName <|> (string "_|_" >> return falseTy))

12991299 eof

13001300 return (TDocStr (Left n)))

1301+ <|> try (do reserved "search"

1302+ whiteSpace

1303+ t <- (indentPropHolds gtProp *> expr syn);

1304+ i <- get

1305+ return $ TSearch (desugar syn i t))

13011306 <?> "prover command")

13021307 <?> "tactic"

13031308 where

src/Idris/Prover.hs+5

@@ -18,6 +18,7 @@ import Idris.DataOpts

1818import Idris.Completion

1919import Idris.IdeSlave

2020import Idris.Output

21+import Idris.TypeSearch (searchByType)

2122

2223import Text.Trifecta.Result(Result(..))

2324

@@ -227,6 +228,7 @@ ploop fn d prompt prf e h

227228 Success (TCheck t) -> checkType t

228229 Success (TEval t) -> evalTerm t e

229230 Success (TDocStr x) -> docStr x

231+ Success (TSearch t) -> search t

230232 Success tac -> do (_, e) <- elabStep e saveState

231233 (_, st) <- elabStep e (runTac autoSolve i fn tac)

232234 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

@@ -318,3 +320,6 @@ ploop fn d prompt prf e h

318320 docStr (Right c) = do ist <- getIState

319321 let h = idris_outh ist

320322 return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))

323+ search t = do ist <- getIState

324+ let h = idris_outh ist

325+ return (False, e, False, prf, Right $ searchByType h t)

src/Idris/TypeSearch.hs+11−8

@@ -20,20 +20,20 @@ import qualified Data.Set as S

2020import qualified Data.Text as T (pack, isPrefixOf)

2121

2222import Idris.AbsSyntax (addUsingConstraints, addImpl, getContext, getIState, putIState, implicit)

23−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

24− IState (idris_classes, idris_docstrings, tt_ctxt),

25− implicitAllowed, prettyDocumentedIst, prettyIst, PTerm, toplevel)

23+import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, Idris,

24+ IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

25+ implicitAllowed, OutputMode(..), prettyDocumentedIst, prettyIst, PTerm, toplevel)

2626import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

2727import Idris.Core.TT hiding (score)

2828import Idris.Core.Unify (match_unify)

2929import Idris.Delaborate (delabTy)

3030import Idris.Docstrings (noDocs, overview)

3131import Idris.ElabDecls (elabType')

32−import Idris.Output (ihRenderResult)

32+import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

3333

3434import System.IO (Handle)

3535

36−import Util.Pretty (text, char, (<>), Doc)

36+import Util.Pretty (text, char, vsep, (<>), Doc)

3737

3838searchByType :: Handle -> PTerm -> Idris ()

3939searchByType h pterm = do

@@ -49,12 +49,15 @@ searchByType h pterm = do

4949 [ let docInfo = (n, delabTy i n, fmap (overview . fst) (lookupCtxtExact n (idris_docstrings i))) in

5050 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

5151 | (n, score) <- names']

52− mapM_ (ihRenderResult h) docs

53− where

52+ case idris_outputmode i of

53+ RawOutput -> do mapM_ (ihRenderOutput h) docs

54+ ihPrintResult h ""

55+ IdeSlave n -> ihRenderResult h (vsep docs)

56+ where

5457 numLimit = 50

5558 syn = defaultSyntax { implicitAllowed = True } -- syntax

5659 n = sMN 0 "searchType" -- name

57−

60+

5861-- | Conduct a type-directed search using a given match predicate

5962searchUsing :: (IState -> Type -> [(Name, Type)] -> [(Name, a)])

6063 -> IState -> Type -> [(Name, a)]