git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Prover.hs
523 lines 25 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Prover (prover, showProof, showRunElab) where
4-- Hack for GHC 7.10 and earlier compat without CPP or warnings
5-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
6import Prelude (Eq(..), Show(..),
7 Bool(..), Either(..), Maybe(..), String,
8 (.), ($), (++),
9 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
10 length, lines, map, not, null, repeat, reverse, tail, zip)
12import Idris.Core.Elaborate hiding (Tactic(..))
13import Idris.Core.TT
14import Idris.Core.Evaluate
15import Idris.Core.CaseTree
16import Idris.Core.Typecheck
18import Idris.Elab.Utils
19import Idris.Elab.Value
20import Idris.Elab.Term
22import Idris.AbsSyntax
23import Idris.AbsSyntaxTree
24import Idris.Delaborate
25import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
26import Idris.ElabDecls
27import Idris.Parser hiding (params)
28import Idris.Error
29import Idris.DataOpts
30import Idris.Completion
31import qualified Idris.IdeMode as IdeMode
32import Idris.Output
33import Idris.TypeSearch (searchByType)
35import Text.Trifecta.Result(Result(..))
37import System.IO (Handle, stdin, stdout, hPutStrLn)
38import System.Console.Haskeline
39import System.Console.Haskeline.History
40import Control.Monad.State.Strict
41import Control.DeepSeq
43import Util.Pretty
44import Debug.Trace
46-- | Launch the proof shell
47prover :: Bool -> Bool -> Name -> Idris ()
48prover mode lit x =
49 do ctxt <- getContext
50 i <- getIState
51 case lookupTy x ctxt of
52 [t] -> if elem x (map fst (idris_metavars i))
53 then prove mode (idris_optimisation i) ctxt lit x t
54 else ifail $ show x ++ " is not a hole"
55 _ -> fail "No such hole"
57showProof :: Bool -> Name -> [String] -> String
58showProof lit n ps
59 = bird ++ show n ++ " = proof" ++ break ++
60 showSep break (map (\x -> " " ++ x) ps) ++
61 break ++ "\n"
62 where bird = if lit then "> " else ""
63 break = "\n" ++ bird
65showRunElab :: Bool -> Name -> [String] -> String
66showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "")
67 where doc = text (show n) <+> text "=" <+> text "%runElab" <+>
68 enclose lparen rparen
69 (text "do" <+> (align $ vsep (map text ps)))
70 birdify = if lit
71 then concatMap ("> " ++) . lines
72 else id
74proverSettings :: ElabState EState -> Settings Idris
75proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
77assumptionNames :: ElabState EState -> [String]
78assumptionNames e
79 = case envAtFocus (proof e) of
80 OK env -> names env
81 where names [] = []
82 names ((MN _ _, _) : bs) = names bs
83 names ((n, _) : bs) = show n : names bs
85prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
86prove mode opt ctxt lit n ty
87 = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState
88 idemodePutSExp "start-proof-mode" n
89 (tm, prf) <-
90 if mode
91 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
92 else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
93 logLvl 1 $ "Adding " ++ show tm
94 i <- getIState
95 let shower = if mode
96 then showRunElab
97 else showProof
98 case idris_outputmode i of
99 IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf)
100 _ -> iputStrLn $ shower lit n prf
101 let proofs = proof_list i
102 putIState (i { proof_list = (n, (mode, prf)) : proofs })
103 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
104 logLvl 3 (show tree)
105 (ptm, pty) <- recheckC (fileFC "proof") id [] tm
106 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
107 "Expected type:" ++ show ty)
108 case converts ctxt [] ty pty of
109 OK _ -> return ()
110 Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)
111 ptm' <- applyOpts ptm
112 ei <- getErasureInfo `fmap` getIState
113 ctxt' <- do ctxt <- getContext
114 tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
115 [] [] -- argtys, inaccArgs
116 [Right (P Ref n ty, ptm)]
117 [([], P Ref n ty, ptm)]
118 [([], P Ref n ty, ptm)]
119 [([], P Ref n ty, ptm)]
120 [([], P Ref n ty, ptm')] ty
121 ctxt
122 setContext ctxt'
123 solveDeferred n
124 case idris_outputmode i of
125 IdeMode n h ->
126 runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
127 _ -> return ()
129elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
130elabStep st e = case runStateT eCheck st of
131 OK (a, st') -> return (a, st')
132 Error a -> ierror a
133 where eCheck = do res <- e
134 matchProblems True
135 unifyProblems
136 probs' <- get_probs
137 case probs' of
138 [] -> do tm <- get_term
139 ctxt <- get_context
140 lift $ check ctxt [] (forget tm)
141 return res
142 ((_,_,_,_,e,_,_):_) -> lift $ Error e
144dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
145dumpState ist menv ps | [] <- holes ps =
146 do let nm = thname ps
147 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
148 iputGoal rendered
149dumpState ist menv ps | (h : hs) <- holes ps = do
150 let OK ty = goalAtFocus ps
151 let OK env = envAtFocus ps
152 let state = prettyOtherGoals hs <> line <>
153 prettyAssumptions env <> line <>
154 prettyMetaValues (reverse menv) <>
155 prettyGoal (zip (assumptionNames env) (repeat False)) ty
156 rendered <- iRender state
157 iputGoal rendered
159 where
160 (h : hs) = holes ps -- apparently the pattern guards don't give us this
162 ppo = ppOptionIst ist
164 tPretty bnd t = annotate (AnnTerm bnd t) .
165 pprintPTerm ppo bnd [] (idris_infixes ist) $
166 delab ist t
168 assumptionNames :: Env -> [Name]
169 assumptionNames = map fst
171 prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
172 prettyPs bnd [] = empty
173 prettyPs bnd ((n@(MN _ r), _) : bs)
174 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
175 prettyPs bnd ((n@(MN _ _), _) : bs)
176 | not (n `elem` freeEnvNames bs) = prettyPs bnd bs
177 prettyPs bnd ((n, Let t v) : bs) =
178 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
179 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
180 prettyPs bnd ((n, b) : bs) =
181 line <> bindingOf n False <+> colon <+>
182 align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
184 prettyMetaValues [] = empty
185 prettyMetaValues mvs =
186 text "---------- Meta-values: ----------" <$$>
187 prettyMetaValues' [] mvs <> line <> line
188 prettyMetaValues' _ [] = empty
189 prettyMetaValues' bnd [mv] = ppMv bnd mv
190 prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =
191 ppMv bnd mv <$>
192 prettyMetaValues' ((n, False):bnd) mvs
194 ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+>
195 tPretty bnd ty <+> text "=" <+> tPretty bnd tm
197 kwd = annotate AnnKeyword . text
199 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
200 prettyG bnd b = tPretty bnd $ binderTy b
202 prettyGoal bnd ty =
203 text "---------- Goal: ----------" <$$>
204 bindingOf h False <+> colon <+> align (prettyG bnd ty)
206 prettyAssumptions env =
207 if length env == 0 then
208 empty
209 else
210 text "---------- Assumptions: ----------" <>
211 nest nestingSize (prettyPs [] $ reverse env)
213 prettyOtherGoals hs =
214 if length hs == 0 then
215 empty
216 else
217 text "---------- Other goals: ----------" <$$>
218 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
220 freeEnvNames :: Env -> [Name]
221 freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))
223lifte :: ElabState EState -> ElabD a -> Idris a
224lifte st e = do (v, _) <- elabStep st e
225 return v
227receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
228receiveInput h e =
229 do i <- getIState
230 let inh = if h == stdout then stdin else h
231 len' <- runIO $ IdeMode.getLen inh
232 len <- case len' of
233 Left err -> ierror err
234 Right n -> return n
235 l <- runIO $ IdeMode.getNChar inh len ""
236 (sexp, id) <- case IdeMode.parseMessage l of
237 Left err -> ierror err
238 Right (sexp, id) -> return (sexp, id)
239 putIState $ i { idris_outputmode = (IdeMode id h) }
240 case IdeMode.sexpToCommand sexp of
241 Just (IdeMode.REPLCompletions prefix) ->
242 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
243 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
244 idemodePutSExp "return" good
245 receiveInput h e
246 Just (IdeMode.Interpret cmd) -> return (Just cmd)
247 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
248 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
249 _ -> return Nothing
251data ElabShellHistory = ElabStep | LetStep | BothStep
253undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
254undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
255 return (init prf, env, st')
256undoStep prf env st LetStep = return (init prf, tail env, st)
257undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
258 return (init prf, tail env, st')
260undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
261undoElab prf env st [] = ifail "Nothing to undo"
262undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
263 return (prf', env', st', hs)
265elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
266elabloop fn d prompt prf e prev h env
267 = do ist <- getIState
268 when d $ dumpState ist env (proof e)
269 (x, h') <-
270 case idris_outputmode ist of
271 RawOutput _ ->
272 runInputT (proverSettings e) $
273 do case h of
274 Just history -> putHistory history
275 Nothing -> return ()
276 l <- getInputLine (prompt ++ "> ")
277 h' <- getHistory
278 return (l, Just h')
279 IdeMode _ handle ->
280 do isetPrompt prompt
281 i <- receiveInput handle e
282 return (i, h)
283 (cmd, step) <- case x of
284 Nothing -> do iPrintError "" ; ifail "Abandoned"
285 Just input -> return (parseElabShellStep ist input, input)
287 -- if we're abandoning, it has to be outside the scope of the catch
288 case cmd of
289 Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
290 _ -> return ()
292 (d, prev', st, done, prf', env', res) <-
293 idrisCatch
294 (case cmd of
295 Failure err ->
296 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
297 Success (Left cmd') ->
298 case cmd' of
299 EQED -> do hs <- lifte e get_holes
300 when (not (null hs)) $ ifail "Incomplete proof"
301 iputStrLn "Proof completed!"
302 return (False, prev, e, True, prf, env, Right $ iPrintResult "")
303 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
304 return (True, prev', st', False, prf', env', Right $ iPrintResult "")
305 EAbandon ->
306 error "the impossible happened - should have been matched on outer scope"
307 EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
308 EProofTerm ->
309 do tm <- lifte e get_term
310 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
311 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
312 return (d', prev, st', done, prf', env, go)
313 ECheck (PRef _ _ n) ->
314 do (d', st', done, prf', go) <- checkNameType e prf n
315 return (d', prev, st', done, prf', env, go)
316 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
317 return (d', prev, st', done, prf', env, go)
318 ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
319 return (d', prev, st', done, prf', env, go)
320 EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
321 return (d', prev, st', done, prf', env, go)
322 Success (Right cmd') ->
323 case cmd' of
324 DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"
325 DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"
326 DoLet fc i ifc Placeholder expr ->
327 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
328 ctxt <- getContext
329 let tm' = normaliseAll ctxt [] tm
330 ty' = normaliseAll ctxt [] ty
331 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
332 DoLet fc i ifc ty expr ->
333 do (tm, ty) <- elabVal recinfo ERHS
334 (PApp NoFC (PRef NoFC [] (sUN "the"))
335 [ pexp (inLets ist env ty)
336 , pexp (inLets ist env expr)
337 ])
338 ctxt <- getContext
339 let tm' = normaliseAll ctxt [] tm
340 ty' = normaliseAll ctxt [] ty
341 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
342 DoBind fc i ifc expr ->
343 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
344 (_, e') <- elabStep e saveState -- enable :undo
345 (res, e'') <- elabStep e' $
346 runElabAction ist NoFC [] tm ["Shell"]
347 ctxt <- getContext
348 (v, vty) <- tclift $ check ctxt [] (forget res)
349 let v' = normaliseAll ctxt [] v
350 vty' = normaliseAll ctxt [] vty
351 return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
352 DoExp fc expr ->
353 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
354 -- TODO: call elaborator with Elab () as goal here
355 (_, e') <- elabStep e saveState -- enable :undo
356 (_, e'') <- elabStep e' $
357 runElabAction ist NoFC [] tm ["Shell"]
358 return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
359 (\err -> return (False, prev, e, False, prf, env, Left err))
360 idemodePutSExp "write-proof-state" (prf', length prf')
361 case res of
362 Left err -> do ist <- getIState
363 iRenderError $ pprintErr ist err
364 elabloop fn d prompt prf' st prev' h' env'
365 Right ok ->
366 if done then do (tm, _) <- elabStep st get_term
367 return (tm, prf')
368 else do ok
369 elabloop fn d prompt prf' st prev' h' env'
371 where
372 -- A bit of a hack: wrap the value up in a let binding, which will
373 -- normalise away. It would be better to figure out how to call
374 -- the elaborator with a custom environment here to avoid the
375 -- delab step.
376 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
377 inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
381ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
382ploop fn d prompt prf e h
383 = do i <- getIState
384 let autoSolve = opt_autoSolve (idris_options i)
385 when d $ dumpState i [] (proof e)
386 (x, h') <-
387 case idris_outputmode i of
388 RawOutput _ ->
389 runInputT (proverSettings e) $
390 -- Manually track the history so that we can use the proof state
391 do case h of
392 Just history -> putHistory history
393 Nothing -> return ()
394 l <- getInputLine (prompt ++ "> ")
395 h' <- getHistory
396 return (l, Just h')
397 IdeMode _ handle ->
398 do isetPrompt prompt
399 i <- receiveInput handle e
400 return (i, h)
401 (cmd, step) <- case x of
402 Nothing -> do iPrintError ""; ifail "Abandoned"
403 Just input -> do return (parseTactic i input, input)
404 case cmd of
405 Success Abandon -> do iPrintError ""; ifail "Abandoned"
406 _ -> return ()
407 (d, st, done, prf', res) <- idrisCatch
408 (case cmd of
409 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
410 Success Undo -> do (_, st) <- elabStep e loadState
411 return (True, st, False, init prf, Right $ iPrintResult "")
412 Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
413 Success ProofTerm -> do tm <- lifte e get_term
414 iputStrLn $ "TT: " ++ show tm ++ "\n"
415 return (False, e, False, prf, Right $ iPrintResult "")
416 Success Qed -> do hs <- lifte e get_holes
417 when (not (null hs)) $ ifail "Incomplete proof"
418 iputStrLn "Proof completed!"
419 return (False, e, True, prf, Right $ iPrintResult "")
420 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n
421 Success (TCheck t) -> checkType e prf t
422 Success (TEval t) -> evalTerm e prf t
423 Success (TDocStr x) -> docStr e prf x
424 Success (TSearch t) -> search e prf t
425 Success tac ->
426 do (_, e) <- elabStep e saveState
427 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
428 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
429 (\err -> return (False, e, False, prf, Left err))
430 idemodePutSExp "write-proof-state" (prf', length prf')
431 case res of
432 Left err -> do ist <- getIState
433 iRenderError $ pprintErr ist err
434 ploop fn d prompt prf' st h'
435 Right ok ->
436 if done then do (tm, _) <- elabStep st get_term
437 return (tm, prf')
438 else do ok
439 ploop fn d prompt prf' st h'
442envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
444checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
445checkNameType e prf n = do
446 ctxt <- getContext
447 ist <- getIState
448 imp <- impShow
449 idrisCatch (do
450 let OK env = envAtFocus (proof e)
451 ctxt' = envCtxt env ctxt
452 bnd = map (\x -> (fst x, False)) env
453 ist' = ist { tt_ctxt = ctxt' }
454 putIState ist'
455 -- Unlike the REPL, metavars have no special treatment, to
456 -- make it easier to see how to prove with them.
457 let action = case lookupNames n ctxt' of
458 [] -> iPrintError $ "No such variable " ++ show n
459 ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
460 putIState ist
461 return (False, e, False, prf, Right action))
462 (\err -> do putIState ist ; ierror err)
464checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
465checkType e prf t = do
466 ist <- getIState
467 ctxt <- getContext
468 idrisCatch (do
469 let OK env = envAtFocus (proof e)
470 ctxt' = envCtxt env ctxt
471 putIState ist { tt_ctxt = ctxt' }
472 (tm, ty) <- elabVal recinfo ERHS t
473 let ppo = ppOptionIst ist
474 ty' = normaliseC ctxt [] ty
475 infixes = idris_infixes ist
476 action = case tm of
477 TType _ ->
478 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
479 _ -> let bnd = map (\x -> (fst x, False)) env in
480 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
481 (pprintPTerm ppo bnd [] infixes (delab ist ty))
482 putIState ist
483 return (False, e, False, prf, Right action))
484 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
486proverFC = FC "(prover shell)" (0, 0) (0, 0)
488evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
489evalTerm e prf t = withErrorReflection $
490 do ctxt <- getContext
491 ist <- getIState
492 idrisCatch (do
493 let OK env = envAtFocus (proof e)
494 ctxt' = envCtxt env ctxt
495 ist' = ist { tt_ctxt = ctxt' }
496 bnd = map (\x -> (fst x, False)) env
497 putIState ist'
498 (tm, ty) <- elabVal recinfo ERHS t
499 let tm' = force (normaliseAll ctxt' env tm)
500 ty' = force (normaliseAll ctxt' env ty)
501 ppo = ppOption (idris_options ist')
502 infixes = idris_infixes ist
503 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
504 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
505 action = iPrintTermWithType tmDoc tyDoc
506 putIState ist
507 return (False, e, False, prf, Right action))
508 (\err -> do putIState ist ; ierror err)
510docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
511docStr e prf (Left n) = do ist <- getIState
512 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
513 [] -> return (False, e, False, prf,
514 Left . Msg $ "No documentation for " ++ show n)
515 ns -> do toShow <- mapM (showDoc ist) ns
516 return (False, e, False, prf,
517 Right $ iRenderResult (vsep toShow)))
518 (\err -> do putIState ist ; ierror err)
519 where showDoc ist (n, d) = do doc <- getDocs n FullDocs
520 return $ pprintDocs ist doc
521docStr e prf (Right c) = do ist <- getIState
522 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
523search e prf t = return (False, e, False, prf, Right $ searchByType [] t)