330eaa5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

330eaa5David Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

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

762 | TCheck t

763 | TEval t

764 | TDocStr (Either Name Const)

765+ | TSearch t

765 | Qed | Abandon

766 | Qed | Abandon

766 deriving (Show, Eq, Functor)

767 deriving (Show, Eq, Functor)

767{-!

768{-!

src/Idris/Output.hs+12−1

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

78 ppOverload ppo infixes n tm =

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

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+

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

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

82ihRenderResult h d = do ist <- getIState

93ihRenderResult h d = do ist <- getIState

83 case idris_outputmode ist of

94 case idris_outputmode ist of

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

85 IdeSlave n -> ideSlaveReturnAnnotated n h d

96 IdeSlave n -> ideSlaveReturnAnnotated n h d

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

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

88−ideSlaveReturnWithStatus status n h out = do

99+ideSlaveReturnWithStatus status n h out = do

89 ist <- getIState

100 ist <- getIState

90 (str, spans) <- fmap displaySpans .

101 (str, spans) <- fmap displaySpans .

91 iRender .

102 iRender .

src/Idris/ParseExpr.hs+5

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

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

1299 eof

1300 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))

1301 <?> "prover command")

1306 <?> "prover command")

1302 <?> "tactic"

1307 <?> "tactic"

1303 where

1308 where

src/Idris/Prover.hs+5

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

18import Idris.Completion

19import Idris.IdeSlave

20import Idris.Output

21+import Idris.TypeSearch (searchByType)

22import Text.Trifecta.Result(Result(..))

23import Text.Trifecta.Result(Result(..))

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

227 Success (TCheck t) -> checkType t

228 Success (TCheck t) -> checkType t

228 Success (TEval t) -> evalTerm t e

229 Success (TEval t) -> evalTerm t e

229 Success (TDocStr x) -> docStr x

230 Success (TDocStr x) -> docStr x

231+ Success (TSearch t) -> search t

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

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

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

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

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

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

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

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

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

319 let h = idris_outh ist

321 let h = idris_outh ist

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

322 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

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

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

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

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

24− IState (idris_classes, idris_docstrings, tt_ctxt),

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

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

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

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

27import Idris.Core.TT hiding (score)

28import Idris.Core.Unify (match_unify)

29import Idris.Delaborate (delabTy)

30import Idris.Docstrings (noDocs, overview)

31import Idris.ElabDecls (elabType')

32−import Idris.Output (ihRenderResult)

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

34import System.IO (Handle)

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

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

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

39searchByType h pterm = do

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

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

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

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

52+ case idris_outputmode i of

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

54+ ihPrintResult h ""

52− mapM_ (ihRenderResult h) docs

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

53− where

56+ where

54 numLimit = 50

57 numLimit = 50

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

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

56 n = sMN 0 "searchType" -- name

59 n = sMN 0 "searchType" -- name

57−

60+

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

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

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

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

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

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