{-| Module : Idris.Prover Description : Idris' theorem prover. License : BSD3 Maintainer : The Idris Community. -} {-# LANGUAGE PatternGuards #-} module Idris.Prover (prover, showProof, showRunElab) where -- Hack for GHC 7.10 and earlier compat without CPP or warnings -- This exludes (<$>) as fmap, because wl-pprint uses it for newline import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String, concatMap, elem, error, foldl, foldr, fst, id, init, length, lines, map, not, null, repeat, reverse, tail, zip, ($), (&&), (++), (.), (||)) import Idris.AbsSyntax import Idris.Completion import Idris.Core.CaseTree import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.Evaluate import Idris.Core.TT import Idris.Core.Typecheck import Idris.DataOpts import Idris.Delaborate import Idris.Docs (getDocs, pprintConstDocs, pprintDocs) import Idris.Elab.Term import Idris.Elab.Utils import Idris.Elab.Value import Idris.ElabDecls import Idris.Error import qualified Idris.IdeMode as IdeMode import Idris.Options import Idris.Output import Idris.Parser hiding (params) import Idris.TypeSearch (searchByType) import Util.Pretty import Control.DeepSeq import Control.Monad.State.Strict import System.Console.Haskeline import System.Console.Haskeline.History import System.IO (Handle, hPutStrLn, stdin, stdout) -- | Launch the proof shell prover :: ElabInfo -> Bool -> Bool -> Name -> Idris () prover info mode lit x = do ctxt <- getContext i <- getIState case lookupTy x ctxt of [t] -> if elem x (map fst (idris_metavars i)) then prove mode info (idris_optimisation i) ctxt lit x t else ifail $ show x ++ " is not a hole" _ -> fail "No such hole" showProof :: Bool -> Name -> [String] -> String showProof lit n ps = bird ++ show n ++ " = proof" ++ break ++ showSep break (map (\x -> " " ++ x) ps) ++ break ++ "\n" where bird = if lit then "> " else "" break = "\n" ++ bird showRunElab :: Bool -> Name -> [String] -> String showRunElab lit n ps = birdify (displayS (renderPretty 1.0 80 doc) "") where doc = text (show n) <+> text "=" <+> text "%runElab" <+> enclose lparen rparen (text "do" <+> (align $ vsep (map text ps))) birdify = if lit then concatMap ("> " ++) . lines else id proverSettings :: ElabState EState -> Settings Idris proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings assumptionNames :: ElabState EState -> [String] assumptionNames e = case envAtFocus (proof e) of OK env -> names env where names [] = [] names ((MN _ _, _, _) : bs) = names bs names ((n, _, _) : bs) = show n : names bs prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris () prove mode info opt ctxt lit n ty = do ps <- fmap (\ist -> initElaborator n (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) ty) getIState idemodePutSExp "start-proof-mode" n (tm, prf) <- if mode then elabloop info n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing [] else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++ "in a future release. Please see :elab for a similar feature that "++ "will replace it." ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing logLvl 1 $ "Adding " ++ show tm i <- getIState let shower = if mode then showRunElab else showProof case idris_outputmode i of IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, shower lit n prf) _ -> iputStrLn $ shower lit n prf let proofs = proof_list i putIState (i { proof_list = (n, (mode, prf)) : proofs }) let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)] logLvl 3 (show tree) (ptm, pty) <- recheckC (constraintNS info) (fileFC "proof") id [] tm logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++ "Expected type:" ++ show ty) case converts ctxt [] ty pty of OK _ -> return () Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0) ptm' <- applyOpts ptm ei <- getErasureInfo `fmap` getIState ctxt' <- do ctxt <- getContext tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False [] [] -- argtys, inaccArgs [Right (P Ref n ty, ptm)] [([], P Ref n ty, ptm)] [([], P Ref n ty, ptm')] ty ctxt setContext ctxt' solveDeferred emptyFC n case idris_outputmode i of IdeMode n h -> runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n _ -> return () elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState) elabStep st e = case runStateT eCheck st of OK ((a, ctxt'), ES (ps, est@EState{new_tyDecls = declTodo}) x old) -> do setContext ctxt' processTacticDecls toplevel declTodo return (a, ES (ps, est {new_tyDecls = []}) x old) Error a -> ierror a where eCheck = do res <- e matchProblems True unifyProblems probs' <- get_probs case probs' of [] -> do tm <- get_term ctxt <- get_context lift $ check ctxt [] (forget tm) return (res, ctxt) ((_,_,_,_,e,_,_):_) -> lift $ Error e dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris () dumpState ist inElab menv ps | [] <- holes ps = do let nm = thname ps rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals." iputGoal rendered dumpState ist inElab menv ps | (h : hs) <- holes ps = do let OK ty = goalAtFocus ps OK env = envAtFocus ps state = prettyOtherGoals hs <> line <> prettyAssumptions inElab ty env <> line <> prettyMetaValues (reverse menv) <> prettyGoal (zip (assumptionNames env) (repeat False)) ty rendered <- iRender state iputGoal rendered where (h : _) = holes ps -- apparently the pattern guards don't give us this ppo = ppOptionIst ist tPretty bnd t = annotate (AnnTerm bnd t) . pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t assumptionNames :: Env -> [Name] assumptionNames = map fstEnv prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation prettyPs all g bnd [] = empty prettyPs all g bnd ((n@(MN _ r), _, _) : bs) | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs prettyPs all g bnd ((n@(MN _ _), _, _) : bs) | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs prettyPs all g bnd ((n, _, Let rig t v) : bs) = line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+> align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs prettyPs all g bnd ((n, _, b) : bs) = line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs prettyMetaValues [] = empty prettyMetaValues mvs = text "---------- Meta-values: ----------" <$$> prettyMetaValues' [] mvs <> line <> line prettyMetaValues' _ [] = empty prettyMetaValues' bnd [mv] = ppMv bnd mv prettyMetaValues' bnd ((mv@(n, ty, tm)) : mvs) = ppMv bnd mv <$> prettyMetaValues' ((n, False):bnd) mvs ppMv bnd (n, ty, tm) = kwd "let" <+> bindingOf n False <+> colon <+> tPretty bnd ty <+> text "=" <+> tPretty bnd tm kwd = annotate AnnKeyword . text goalNames (Guess t v) = freeNames t ++ freeNames v goalNames b = freeNames (binderTy b) prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v prettyG bnd b = tPretty bnd $ binderTy b prettyGoal bnd ty = text "---------- Goal: ----------" <$$> bindingOf h False <+> colon <+> align (prettyG bnd ty) prettyAssumptions inElab g env = if null env then empty else text "---------- Assumptions: ----------" <> nest nestingSize (prettyPs inElab g [] $ reverse env) prettyOtherGoals hs = if null hs then empty else text "---------- Other goals: ----------" <$$> nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs) freeEnvNames :: Env -> [Name] freeEnvNames = concatMap (\(n, _, b) -> freeNames (Bind n b Erased)) lifte :: ElabState EState -> ElabD a -> Idris a lifte st e = do (v, _) <- elabStep st e return v receiveInput :: Handle -> ElabState EState -> Idris (Maybe String) receiveInput h e = do i <- getIState let inh = if h == stdout then stdin else h len' <- runIO $ IdeMode.getLen inh len <- case len' of Left err -> ierror err Right n -> return n l <- runIO $ IdeMode.getNChar inh len "" (sexp, id) <- case IdeMode.parseMessage l of Left err -> ierror err Right (sexp, id) -> return (sexp, id) putIState $ i { idris_outputmode = IdeMode id h } case IdeMode.sexpToCommand sexp of Just (IdeMode.REPLCompletions prefix) -> do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "") let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)] idemodePutSExp "return" good receiveInput h e Just (IdeMode.Interpret cmd) -> return (Just cmd) Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str)) Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str)) _ -> return Nothing data ElabShellHistory = ElabStep | LetStep | BothStep undoStep :: [String] -> [(Name, Type, Term)] -> ElabState EState -> ElabShellHistory -> Idris ([String], [(Name, Type, Term)], ElabState EState) undoStep prf env st ElabStep = do (_, st') <- elabStep st loadState return (init prf, env, st') undoStep prf env st LetStep = return (init prf, tail env, st) undoStep prf env st BothStep = do (_, st') <- elabStep st loadState return (init prf, tail env, st') undoElab :: [String] -> [(Name, Type, Term)] -> ElabState EState -> [ElabShellHistory] -> Idris ([String], [(Name, Type, Term)], ElabState EState, [ElabShellHistory]) undoElab prf env st [] = ifail "Nothing to undo" undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h return (prf', env', st', hs) proverfc = fileFC "prover" runWithInterrupt :: ElabState EState -> Idris a -- ^ run with SIGINT handler -> Idris b -- ^ run if mTry finished -> Idris b -- ^ run if mTry was interrupted -> Idris b runWithInterrupt elabState mTry mSuccess mFailure = do ist <- getIState case idris_outputmode ist of RawOutput _ -> do success <- runInputT (proverSettings elabState) $ handleInterrupt (return False) $ withInterrupt (lift mTry >> return True) if success then mSuccess else mFailure IdeMode _ _ -> mTry >> mSuccess elabloop :: ElabInfo -> Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String]) elabloop info fn d prompt prf e prev h env = do ist <- getIState when d $ dumpState ist True env (proof e) (x, h') <- case idris_outputmode ist of RawOutput _ -> runInputT (proverSettings e) $ do case h of Just history -> putHistory history Nothing -> return () l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ") h' <- getHistory return (l, Just h') IdeMode _ handle -> do isetPrompt prompt i <- receiveInput handle e return (i, h) (cmd, step) <- case x of Nothing -> do iPrintError "" ; ifail "Abandoned" Just input -> return (parseElabShellStep ist input, input) -- if we're abandoning, it has to be outside the scope of the catch case cmd of Right (Left EAbandon) -> do iPrintError ""; ifail "Abandoned" _ -> return () (d, prev', st, done, prf', env', res) <- idrisCatch (case cmd of Left err -> do msg <- fmap (Left . Msg . show) (formatMessage err) return (False, prev, e, False, prf, env, msg) Right (Left cmd') -> case cmd' of EQED -> do hs <- lifte e get_holes unless (null hs) $ ifail "Incomplete proof" iputStrLn "Proof completed!" return (False, prev, e, True, prf, env, Right $ iPrintResult "") EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev return (True, prev', st', False, prf', env', Right $ iPrintResult "") EAbandon -> error "the impossible happened - should have been matched on outer scope" EProofState -> return (True, prev, e, False, prf, env, Right $ iPrintResult "") EProofTerm -> do tm <- lifte e get_term return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm)) EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm return (d', prev, st', done, prf', env, go) ECheck (PRef _ _ n) -> do (d', st', done, prf', go) <- checkNameType e prf n return (d', prev, st', done, prf', env, go) ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm return (d', prev, st', done, prf', env, go) ESearch ty -> do (d', st', done, prf', go) <- search e prf ty return (d', prev, st', done, prf', env, go) EDocStr d -> do (d', st', done, prf', go) <- docStr e prf d return (d', prev, st', done, prf', env, go) Right (Right cmd') -> case cmd' of DoLetP {} -> ifail "Pattern-matching let not supported here" DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here" DoBindP {} -> ifail "Pattern-matching <- not supported here" DoLet fc rig i ifc Placeholder expr -> do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr) ctxt <- getContext let tm' = normaliseAll ctxt [] tm ty' = normaliseAll ctxt [] ty return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult "")) DoLet fc rig i ifc ty expr -> do (tm, ty) <- elabVal (recinfo proverfc) ERHS (PApp NoFC (PRef NoFC [] (sUN "the")) [ pexp (inLets ist env ty) , pexp (inLets ist env expr) ]) ctxt <- getContext let tm' = normaliseAll ctxt [] tm ty' = normaliseAll ctxt [] ty return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult "")) DoBind fc i ifc expr -> do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr) (_, e') <- elabStep e saveState -- enable :undo (res, e'') <- elabStep e' $ runElabAction info ist NoFC [] tm ["Shell"] ctxt <- getContext (v, vty) <- tclift $ check ctxt [] (forget res) let v' = normaliseAll ctxt [] v vty' = normaliseAll ctxt [] vty return (True, BothStep:prev, e'', False, prf ++ [step], (i, vty', v') : env, Right (iPrintResult "")) DoExp fc expr -> do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr) -- TODO: call elaborator with Elab () as goal here (_, e') <- elabStep e saveState -- enable :undo (_, e'') <- elabStep e' $ runElabAction info ist NoFC [] tm ["Shell"] return (True, ElabStep:prev, e'', False, prf ++ [step], env, Right (iPrintResult ""))) (\err -> return (False, prev, e, False, prf, env, Left err)) idemodePutSExp "write-proof-state" (prf', length prf') case res of Left err -> do ist <- getIState iRenderError $ pprintErr ist err elabloop info fn d prompt prf' st prev' h' env' Right ok -> if done then do (tm, _) <- elabStep st get_term return (tm, prf') else runWithInterrupt e ok (elabloop info fn d prompt prf' st prev' h' env') (elabloop info fn d prompt prf e prev h' env) where -- A bit of a hack: wrap the value up in a let binding, which will -- normalise away. It would be better to figure out how to call -- the elaborator with a custom environment here to avoid the -- delab step. inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC RigW n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets) ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String]) ploop fn d prompt prf e h = do i <- getIState let autoSolve = opt_autoSolve (idris_options i) when d $ dumpState i False [] (proof e) (x, h') <- case idris_outputmode i of RawOutput _ -> runInputT (proverSettings e) $ -- Manually track the history so that we can use the proof state do case h of Just history -> putHistory history Nothing -> return () l <- handleInterrupt (return $ Just "") $ withInterrupt $ getInputLine (prompt ++ "> ") h' <- getHistory return (l, Just h') IdeMode _ handle -> do isetPrompt prompt i <- receiveInput handle e return (i, h) (cmd, step) <- case x of Nothing -> do iPrintError ""; ifail "Abandoned" Just input -> return (parseTactic i input, input) case cmd of Right Abandon -> do iPrintError ""; ifail "Abandoned" _ -> return () (d, st, done, prf', res) <- idrisCatch (case cmd of Left err -> do msg <- fmap (Left . Msg . show) (formatMessage err) return (False, e, False, prf, msg) Right Undo -> do (_, st) <- elabStep e loadState return (True, st, False, init prf, Right $ iPrintResult "") Right ProofState -> return (True, e, False, prf, Right $ iPrintResult "") Right ProofTerm -> do tm <- lifte e get_term iputStrLn $ "TT: " ++ show tm ++ "\n" return (False, e, False, prf, Right $ iPrintResult "") Right Qed -> do hs <- lifte e get_holes unless (null hs) $ ifail "Incomplete proof" iputStrLn "Proof completed!" return (False, e, True, prf, Right $ iPrintResult "") Right (TCheck (PRef _ _ n)) -> checkNameType e prf n Right (TCheck t) -> checkType e prf t Right (TEval t) -> evalTerm e prf t Right (TDocStr x) -> docStr e prf x Right (TSearch t) -> search e prf t Right tac -> do (_, e) <- elabStep e saveState (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac) return (True, st, False, prf ++ [step], Right $ iPrintResult "")) (\err -> return (False, e, False, prf, Left err)) idemodePutSExp "write-proof-state" (prf', length prf') case res of Left err -> do ist <- getIState iRenderError $ pprintErr ist err ploop fn d prompt prf' st h' Right ok -> if done then do (tm, _) <- elabStep st get_term return (tm, prf') else runWithInterrupt e ok (ploop fn d prompt prf' st h') (ploop fn d prompt prf e h') envCtxt env ctxt = foldl (\c (n, _, b) -> addTyDecl n Bound (binderTy b) c) ctxt env checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ())) checkNameType e prf n = do ctxt <- getContext ist <- getIState imp <- impShow idrisCatch (do let OK env = envAtFocus (proof e) ctxt' = envCtxt env ctxt bnd = map (\x -> (fstEnv x, False)) env ist' = ist { tt_ctxt = ctxt' } putIState ist' -- Unlike the REPL, metavars have no special treatment, to -- make it easier to see how to prove with them. let action = case lookupNames n ctxt' of [] -> iPrintError $ "No such variable " ++ show n ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts) putIState ist return (False, e, False, prf, Right action)) (\err -> do putIState ist ; ierror err) checkType :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ())) checkType e prf t = do ist <- getIState ctxt <- getContext idrisCatch (do let OK env = envAtFocus (proof e) ctxt' = envCtxt env ctxt putIState ist { tt_ctxt = ctxt' } (tm, ty) <- elabVal (recinfo proverfc) ERHS t let ppo = ppOptionIst ist infixes = idris_infixes ist action = case tm of TType _ -> iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc _ -> let bnd = map (\x -> (fstEnv x, False)) env in iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm)) (pprintPTerm ppo bnd [] infixes (delab ist ty)) putIState ist return (False, e, False, prf, Right action)) (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err) proverFC = FC "(prover shell)" (0, 0) (0, 0) evalTerm :: ElabState EState -> [String] -> PTerm -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ())) evalTerm e prf t = withErrorReflection $ do ctxt <- getContext ist <- getIState idrisCatch (do let OK env = envAtFocus (proof e) ctxt' = envCtxt env ctxt ist' = ist { tt_ctxt = ctxt' } bnd = map (\x -> (fstEnv x, False)) env putIState ist' (tm, ty) <- elabVal (recinfo proverfc) ERHS t let tm' = force (normaliseAll ctxt' env tm) ty' = force (normaliseAll ctxt' env ty) ppo = ppOption (idris_options ist') infixes = idris_infixes ist tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm') tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty') action = iPrintTermWithType tmDoc tyDoc putIState ist return (False, e, False, prf, Right action)) (\err -> do putIState ist ; ierror err) docStr :: ElabState EState -> [String] -> Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ())) docStr e prf (Left n) = do ist <- getIState idrisCatch (case lookupCtxtName n (idris_docstrings ist) of [] -> return (False, e, False, prf, Left . Msg $ "No documentation for " ++ show n) ns -> do toShow <- mapM (showDoc ist) ns return (False, e, False, prf, Right $ iRenderResult (vsep toShow))) (\err -> do putIState ist ; ierror err) where showDoc ist (n, d) = do doc <- getDocs n FullDocs return $ pprintDocs ist doc docStr e prf (Right c) = do ist <- getIState return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c)) search e prf t = return (False, e, False, prf, Right $ searchByType [] t)