@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2−module Idris.Prover where
2+module Idris.Prover (prover, showProof, showRunElab) where
33
44import Idris.Core.Elaborate hiding (Tactic(..))
55import Idris.Core.TT
@@ -35,13 +35,14 @@ import Control.DeepSeq
3535import Util.Pretty
3636import Debug.Trace
3737
38−prover :: Bool -> Name -> Idris ()
39−prover lit x =
38+-- | Launch the proof shell
39+prover :: Bool -> Bool -> Name -> Idris ()
40+prover mode lit x =
4041 do ctxt <- getContext
4142 i <- getIState
4243 case lookupTy x ctxt of
4344 [t] -> if elem x (map fst (idris_metavars i))
44− then prove (idris_optimisation i) ctxt lit x t
45+ then prove mode (idris_optimisation i) ctxt lit x t
4546 else ifail $ show x ++ " is not a metavariable"
4647 _ -> fail "No such metavariable"
4748
@@ -53,6 +54,15 @@ showProof lit n ps
5354 where bird = if lit then "> " else ""
5455 break = "\n" ++ bird
5556
57+showRunElab :: Bool -> Name -> [String] -> String
58+showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "")
59+ where doc = text (show n) <+> text "=" <+> text "%runElab" <+>
60+ enclose lparen rparen
61+ (text "do" <+> (align $ vsep (map text ps)))
62+ birdify = if lit
63+ then concatMap ("> " ++) . lines
64+ else id
65+
5666proverSettings :: ElabState EState -> Settings Idris
5767proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
5868
@@ -64,18 +74,24 @@ assumptionNames e
6474 names ((MN _ _, _) : bs) = names bs
6575 names ((n, _) : bs) = show n : names bs
6676
67−prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
68−prove opt ctxt lit n ty
77+prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
78+prove mode opt ctxt lit n ty
6979 = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState
7080 idemodePutSExp "start-proof-mode" n
71− (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
81+ (tm, prf) <-
82+ if mode
83+ then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
84+ else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
7285 iLOG $ "Adding " ++ show tm
7386 i <- getIState
87+ let shower = if mode
88+ then showRunElab
89+ else showProof
7490 case idris_outputmode i of
75− IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, showProof lit n prf)
76− _ -> iputStrLn $ showProof lit n prf
91+ IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf)
92+ _ -> iputStrLn $ shower lit n prf
7793 let proofs = proof_list i
78− putIState (i { proof_list = (n, prf) : proofs })
94+ putIState (i { proof_list = (n, (mode, prf)) : proofs })
7995 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
8096 logLvl 3 (show tree)
8197 (ptm, pty) <- recheckC (fileFC "proof") id [] tm
@@ -117,16 +133,17 @@ elabStep st e = case runStateT eCheck st of
117133 return res
118134 ((_,_,_,_,e,_,_):_) -> lift $ Error e
119135
120−dumpState :: IState -> ProofState -> Idris ()
121−dumpState ist ps | [] <- holes ps =
136+dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
137+dumpState ist menv ps | [] <- holes ps =
122138 do let nm = thname ps
123139 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
124140 iputGoal rendered
125−dumpState ist ps | (h : hs) <- holes ps = do
141+dumpState ist menv ps | (h : hs) <- holes ps = do
126142 let OK ty = goalAtFocus ps
127143 let OK env = envAtFocus ps
128144 let state = prettyOtherGoals hs <> line <>
129145 prettyAssumptions env <> line <>
146+ prettyMetaValues (reverse menv) <>
130147 prettyGoal (zip (assumptionNames env) (repeat False)) ty
131148 rendered <- iRender state
132149 iputGoal rendered
@@ -156,6 +173,21 @@ dumpState ist ps | (h : hs) <- holes ps = do
156173 line <> bindingOf n False <+> colon <+>
157174 align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
158175
176+ prettyMetaValues [] = empty
177+ prettyMetaValues mvs =
178+ text "---------- Meta-values: ----------" <$$>
179+ prettyMetaValues' [] mvs <> line <> line
180+ prettyMetaValues' _ [] = empty
181+ prettyMetaValues' bnd [mv] = ppMv bnd mv
182+ prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) =
183+ ppMv bnd mv <$>
184+ prettyMetaValues' ((n, False):bnd) mvs
185+
186+ ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+>
187+ tPretty bnd ty <+> text "=" <+> tPretty bnd tm
188+
189+ kwd = annotate AnnKeyword . text
190+
159191 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
160192 prettyG bnd b = tPretty bnd $ binderTy b
161193
@@ -208,11 +240,141 @@ receiveInput h e =
208240 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
209241 _ -> return Nothing
210242
243+data ElabShellHistory = ElabStep | LetStep | BothStep
244+
245+undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState)
246+undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState
247+ return (init prf, env, st')
248+undoStep prf env st LetStep = return (init prf, tail env, st)
249+undoStep prf env st BothStep = do (_, st') <- elabStep st loadState
250+ return (init prf, tail env, st')
251+
252+undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory])
253+undoElab prf env st [] = ifail "Nothing to undo"
254+undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
255+ return (prf', env', st', hs)
256+
257+elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
258+elabloop fn d prompt prf e prev h env
259+ = do ist <- getIState
260+ when d $ dumpState ist env (proof e)
261+ (x, h') <-
262+ case idris_outputmode ist of
263+ RawOutput _ ->
264+ runInputT (proverSettings e) $
265+ do case h of
266+ Just history -> putHistory history
267+ Nothing -> return ()
268+ l <- getInputLine (prompt ++ "> ")
269+ h' <- getHistory
270+ return (l, Just h')
271+ IdeMode _ handle ->
272+ do isetPrompt prompt
273+ i <- receiveInput handle e
274+ return (i, h)
275+ (cmd, step) <- case x of
276+ Nothing -> do iPrintError "" ; ifail "Abandoned"
277+ Just input -> return (parseElabShellStep ist input, input)
278+
279+ -- if we're abandoning, it has to be outside the scope of the catch
280+ case cmd of
281+ Success (Left EAbandon) -> do iPrintError ""; ifail "Abandoned"
282+ _ -> return ()
283+
284+ (d, prev', st, done, prf', env', res) <-
285+ idrisCatch
286+ (case cmd of
287+ Failure err ->
288+ return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
289+ Success (Left cmd') ->
290+ case cmd' of
291+ EQED -> do hs <- lifte e get_holes
292+ when (not (null hs)) $ ifail "Incomplete proof"
293+ iputStrLn "Proof completed!"
294+ return (False, prev, e, True, prf, env, Right $ iPrintResult "")
295+ EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev
296+ return (True, prev', st', False, prf', env', Right $ iPrintResult "")
297+ EAbandon ->
298+ error "the impossible happened - should have been matched on outer scope"
299+ EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "")
300+ EProofTerm ->
301+ do tm <- lifte e get_term
302+ return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))
303+ EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm
304+ return (d', prev, st', done, prf', env, go)
305+ ECheck (PRef _ n) ->
306+ do (d', st', done, prf', go) <- checkNameType e prf n
307+ return (d', prev, st', done, prf', env, go)
308+ ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm
309+ return (d', prev, st', done, prf', env, go)
310+ ESearch ty -> do (d', st', done, prf', go) <- search e prf ty
311+ return (d', prev, st', done, prf', env, go)
312+ EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d
313+ return (d', prev, st', done, prf', env, go)
314+ Success (Right cmd') ->
315+ case cmd' of
316+ DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"
317+ DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"
318+ DoLet fc i ifc Placeholder expr ->
319+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
320+ ctxt <- getContext
321+ let tm' = normaliseAll ctxt [] tm
322+ ty' = normaliseAll ctxt [] ty
323+ return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
324+ DoLet fc i ifc ty expr ->
325+ do (tm, ty) <- elabVal recinfo ERHS
326+ (PApp NoFC (PRef NoFC (sUN "the"))
327+ [ pexp (inLets ist env ty)
328+ , pexp (inLets ist env expr)
329+ ])
330+ ctxt <- getContext
331+ let tm' = normaliseAll ctxt [] tm
332+ ty' = normaliseAll ctxt [] ty
333+ return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))
334+ DoBind fc i ifc expr ->
335+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
336+ (_, e') <- elabStep e saveState -- enable :undo
337+ (res, e'') <- elabStep e' $
338+ runTactical ist NoFC [] tm ["Shell"]
339+ ctxt <- getContext
340+ (v, vty) <- tclift $ check ctxt [] (forget res)
341+ let v' = normaliseAll ctxt [] v
342+ vty' = normaliseAll ctxt [] vty
343+ return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult ""))
344+ DoExp fc expr ->
345+ do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)
346+ -- TODO: call elaborator with Elab () as goal here
347+ (_, e') <- elabStep e saveState -- enable :undo
348+ (_, e'') <- elabStep e' $
349+ runTactical ist NoFC [] tm ["Shell"]
350+ return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult "")))
351+ (\err -> return (False, prev, e, False, prf, env, Left err))
352+ idemodePutSExp "write-proof-state" (prf', length prf')
353+ case res of
354+ Left err -> do ist <- getIState
355+ iRenderError $ pprintErr ist err
356+ elabloop fn d prompt prf' st prev' h' env'
357+ Right ok ->
358+ if done then do (tm, _) <- elabStep st get_term
359+ return (tm, prf')
360+ else do ok
361+ elabloop fn d prompt prf' st prev' h' env'
362+
363+ where
364+ -- A bit of a hack: wrap the value up in a let binding, which will
365+ -- normalise away. It would be better to figure out how to call
366+ -- the elaborator with a custom environment here to avoid the
367+ -- delab step.
368+ inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm
369+ inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)
370+
371+
372+
211373ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
212374ploop fn d prompt prf e h
213375 = do i <- getIState
214376 let autoSolve = opt_autoSolve (idris_options i)
215− when d $ dumpState i (proof e)
377+ when d $ dumpState i [] (proof e)
216378 (x, h') <-
217379 case idris_outputmode i of
218380 RawOutput _ ->
@@ -247,11 +409,11 @@ ploop fn d prompt prf e h
247409 when (not (null hs)) $ ifail "Incomplete proof"
248410 iputStrLn "Proof completed!"
249411 return (False, e, True, prf, Right $ iPrintResult "")
250− Success (TCheck (PRef _ n)) -> checkNameType n
251− Success (TCheck t) -> checkType t
252− Success (TEval t) -> evalTerm t e
253− Success (TDocStr x) -> docStr x
254− Success (TSearch t) -> search t
412+ Success (TCheck (PRef _ n)) -> checkNameType e prf n
413+ Success (TCheck t) -> checkType e prf t
414+ Success (TEval t) -> evalTerm e prf t
415+ Success (TDocStr x) -> docStr e prf x
416+ Success (TSearch t) -> search e prf t
255417 Success tac ->
256418 do (_, e) <- elabStep e saveState
257419 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
@@ -267,80 +429,87 @@ ploop fn d prompt prf e h
267429 return (tm, prf')
268430 else do ok
269431 ploop fn d prompt prf' st h'
270− where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
271− checkNameType n = do
272− ctxt <- getContext
273− ist <- getIState
274− imp <- impShow
275− idrisCatch (do
276− let OK env = envAtFocus (proof e)
277− ctxt' = envCtxt env ctxt
278− bnd = map (\x -> (fst x, False)) env
279− ist' = ist { tt_ctxt = ctxt' }
280− putIState ist'
281− -- Unlike the REPL, metavars have no special treatment, to
282− -- make it easier to see how to prove with them.
283− let action = case lookupNames n ctxt' of
284− [] -> iPrintError $ "No such variable " ++ show n
285− ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
286− putIState ist
287− return (False, e, False, prf, Right action))
288− (\err -> do putIState ist ; ierror err)
289−
290− checkType t = do
291− ist <- getIState
292− ctxt <- getContext
293− idrisCatch (do
294− let OK env = envAtFocus (proof e)
295− ctxt' = envCtxt env ctxt
296− putIState ist { tt_ctxt = ctxt' }
297− (tm, ty) <- elabVal recinfo ERHS t
298− let ppo = ppOptionIst ist
299− ty' = normaliseC ctxt [] ty
300− infixes = idris_infixes ist
301− action = case tm of
302− TType _ ->
303− iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
304− _ -> let bnd = map (\x -> (fst x, False)) env in
305− iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
306− (pprintPTerm ppo bnd [] infixes (delab ist ty))
307− putIState ist
308− return (False, e, False, prf, Right action))
309− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
310−
311− proverFC = FC "(prover shell)" (0, 0) (0, 0)
312−
313− evalTerm t e = withErrorReflection $
314− do ctxt <- getContext
315− ist <- getIState
316− idrisCatch (do
317− let OK env = envAtFocus (proof e)
318− ctxt' = envCtxt env ctxt
319− ist' = ist { tt_ctxt = ctxt' }
320− bnd = map (\x -> (fst x, False)) env
321− putIState ist'
322− (tm, ty) <- elabVal recinfo ERHS t
323− let tm' = force (normaliseAll ctxt' env tm)
324− ty' = force (normaliseAll ctxt' env ty)
325− ppo = ppOption (idris_options ist')
326− infixes = idris_infixes ist
327− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
328− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
329− action = iPrintTermWithType tmDoc tyDoc
330− putIState ist
331− return (False, e, False, prf, Right action))
332− (\err -> do putIState ist ; ierror err)
333− docStr :: Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
334− docStr (Left n) = do ist <- getIState
335− idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
336− [] -> return (False, e, False, prf,
337− Left . Msg $ "No documentation for " ++ show n)
338− ns -> do toShow <- mapM (showDoc ist) ns
339− return (False, e, False, prf,
340− Right $ iRenderResult (vsep toShow)))
341− (\err -> do putIState ist ; ierror err)
342− where showDoc ist (n, d) = do doc <- getDocs n FullDocs
343− return $ pprintDocs ist doc
344− docStr (Right c) = do ist <- getIState
345− return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
346− search t = return (False, e, False, prf, Right $ searchByType [] t)
432+
433+
434+envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
435+
436+checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
437+checkNameType e prf n = do
438+ ctxt <- getContext
439+ ist <- getIState
440+ imp <- impShow
441+ idrisCatch (do
442+ let OK env = envAtFocus (proof e)
443+ ctxt' = envCtxt env ctxt
444+ bnd = map (\x -> (fst x, False)) env
445+ ist' = ist { tt_ctxt = ctxt' }
446+ putIState ist'
447+ -- Unlike the REPL, metavars have no special treatment, to
448+ -- make it easier to see how to prove with them.
449+ let action = case lookupNames n ctxt' of
450+ [] -> iPrintError $ "No such variable " ++ show n
451+ ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
452+ putIState ist
453+ return (False, e, False, prf, Right action))
454+ (\err -> do putIState ist ; ierror err)
455+
456+checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
457+checkType e prf t = do
458+ ist <- getIState
459+ ctxt <- getContext
460+ idrisCatch (do
461+ let OK env = envAtFocus (proof e)
462+ ctxt' = envCtxt env ctxt
463+ putIState ist { tt_ctxt = ctxt' }
464+ (tm, ty) <- elabVal recinfo ERHS t
465+ let ppo = ppOptionIst ist
466+ ty' = normaliseC ctxt [] ty
467+ infixes = idris_infixes ist
468+ action = case tm of
469+ TType _ ->
470+ iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc
471+ _ -> let bnd = map (\x -> (fst x, False)) env in
472+ iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
473+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
474+ putIState ist
475+ return (False, e, False, prf, Right action))
476+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
477+
478+proverFC = FC "(prover shell)" (0, 0) (0, 0)
479+
480+evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
481+evalTerm e prf t = withErrorReflection $
482+ do ctxt <- getContext
483+ ist <- getIState
484+ idrisCatch (do
485+ let OK env = envAtFocus (proof e)
486+ ctxt' = envCtxt env ctxt
487+ ist' = ist { tt_ctxt = ctxt' }
488+ bnd = map (\x -> (fst x, False)) env
489+ putIState ist'
490+ (tm, ty) <- elabVal recinfo ERHS t
491+ let tm' = force (normaliseAll ctxt' env tm)
492+ ty' = force (normaliseAll ctxt' env ty)
493+ ppo = ppOption (idris_options ist')
494+ infixes = idris_infixes ist
495+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
496+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
497+ action = iPrintTermWithType tmDoc tyDoc
498+ putIState ist
499+ return (False, e, False, prf, Right action))
500+ (\err -> do putIState ist ; ierror err)
501+
502+docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
503+docStr e prf (Left n) = do ist <- getIState
504+ idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
505+ [] -> return (False, e, False, prf,
506+ Left . Msg $ "No documentation for " ++ show n)
507+ ns -> do toShow <- mapM (showDoc ist) ns
508+ return (False, e, False, prf,
509+ Right $ iRenderResult (vsep toShow)))
510+ (\err -> do putIState ist ; ierror err)
511+ where showDoc ist (n, d) = do doc <- getDocs n FullDocs
512+ return $ pprintDocs ist doc
513+docStr e prf (Right c) = do ist <- getIState
514+ return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
515+search e prf t = return (False, e, False, prf, Right $ searchByType [] t)