git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Prover.hs
343 lines 15 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Prover where
4import Idris.Core.Elaborate hiding (Tactic(..))
5import Idris.Core.TT
6import Idris.Core.Evaluate
7import Idris.Core.CaseTree
8import Idris.Core.Typecheck
10import Idris.Elab.Utils
11import Idris.Elab.Value
13import Idris.AbsSyntax
14import Idris.AbsSyntaxTree
15import Idris.Delaborate
16import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
17import Idris.ElabDecls
18import Idris.ElabTerm
19import Idris.Parser hiding (params)
20import Idris.Error
21import Idris.DataOpts
22import Idris.Completion
23import qualified Idris.IdeMode as IdeMode
24import Idris.Output
25import Idris.TypeSearch (searchByType)
27import Text.Trifecta.Result(Result(..))
29import System.IO (Handle, stdin, stdout, hPutStrLn)
30import System.Console.Haskeline
31import System.Console.Haskeline.History
32import Control.Monad.State.Strict
33import Control.DeepSeq
35import Util.Pretty
36import Debug.Trace
38prover :: Bool -> Name -> Idris ()
39prover lit x =
40 do ctxt <- getContext
41 i <- getIState
42 case lookupTy x ctxt of
43 [t] -> if elem x (map fst (idris_metavars i))
44 then prove (idris_optimisation i) ctxt lit x t
45 else ifail $ show x ++ " is not a metavariable"
46 _ -> fail "No such metavariable"
48showProof :: Bool -> Name -> [String] -> String
49showProof lit n ps
50 = bird ++ show n ++ " = proof" ++ break ++
51 showSep break (map (\x -> " " ++ x) ps) ++
52 break ++ "\n"
53 where bird = if lit then "> " else ""
54 break = "\n" ++ bird
56proverSettings :: ElabState EState -> Settings Idris
57proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
59assumptionNames :: ElabState EState -> [String]
60assumptionNames e
61 = case envAtFocus (proof e) of
62 OK env -> names env
63 where names [] = []
64 names ((MN _ _, _) : bs) = names bs
65 names ((n, _) : bs) = show n : names bs
67prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
68prove opt ctxt lit n ty
69 = do let ps = initElaborator n ctxt ty
70 idemodePutSExp "start-proof-mode" n
71 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
72 iLOG $ "Adding " ++ show tm
73 i <- getIState
74 case idris_outputmode i of
75 IdeMode _ _ -> idemodePutSExp "end-proof-mode" (n, showProof lit n prf)
76 _ -> iputStrLn $ showProof lit n prf
77 let proofs = proof_list i
78 putIState (i { proof_list = (n, prf) : proofs })
79 let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
80 logLvl 3 (show tree)
81 (ptm, pty) <- recheckC (fileFC "proof") id [] tm
82 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
83 "Expected type:" ++ show ty)
84 case converts ctxt [] ty pty of
85 OK _ -> return ()
86 Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)
87 ptm' <- applyOpts ptm
88 ei <- getErasureInfo `fmap` getIState
89 updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False
90 [] [] -- argtys, inaccArgs
91 [Right (P Ref n ty, ptm)]
92 [([], P Ref n ty, ptm)]
93 [([], P Ref n ty, ptm)]
94 [([], P Ref n ty, ptm)]
95 [([], P Ref n ty, ptm')] ty)
96 solveDeferred n
97 case idris_outputmode i of
98 IdeMode n h ->
99 runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n
100 _ -> return ()
102elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)
103elabStep st e = case runStateT eCheck st of
104 OK (a, st') -> return (a, st')
105 Error a -> ierror a
106 where eCheck = do res <- e
107 matchProblems True
108 unifyProblems
109 probs' <- get_probs
110 case probs' of
111 [] -> do tm <- get_term
112 ctxt <- get_context
113 lift $ check ctxt [] (forget tm)
114 return res
115 ((_,_,_,_,e,_,_):_) -> lift $ Error e
117dumpState :: IState -> ProofState -> Idris ()
118dumpState ist ps | [] <- holes ps =
119 do let nm = thname ps
120 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
121 iputGoal rendered
122dumpState ist ps | (h : hs) <- holes ps = do
123 let OK ty = goalAtFocus ps
124 let OK env = envAtFocus ps
125 let state = prettyOtherGoals hs <> line <>
126 prettyAssumptions env <> line <>
127 prettyGoal (zip (assumptionNames env) (repeat False)) ty
128 rendered <- iRender state
129 iputGoal rendered
131 where
132 (h : hs) = holes ps -- apparently the pattern guards don't give us this
134 ppo = ppOptionIst ist
136 tPretty bnd t = annotate (AnnTerm bnd t) .
137 pprintPTerm ppo bnd [] (idris_infixes ist) $
138 delab ist t
140 assumptionNames :: Env -> [Name]
141 assumptionNames = map fst
143 prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
144 prettyPs bnd [] = empty
145 prettyPs bnd ((n@(MN _ r), _) : bs)
146 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
147 prettyPs bnd ((n@(MN _ _), _) : bs)
148 | not (n `elem` freeEnvNames bs) = prettyPs bnd bs
149 prettyPs bnd ((n, Let t v) : bs) =
150 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
151 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
152 prettyPs bnd ((n, b) : bs) =
153 line <> bindingOf n False <+> colon <+>
154 align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
156 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
157 prettyG bnd b = tPretty bnd $ binderTy b
159 prettyGoal bnd ty =
160 text "---------- Goal: ----------" <$$>
161 bindingOf h False <+> colon <+> align (prettyG bnd ty)
163 prettyAssumptions env =
164 if length env == 0 then
165 empty
166 else
167 text "---------- Assumptions: ----------" <>
168 nest nestingSize (prettyPs [] $ reverse env)
170 prettyOtherGoals hs =
171 if length hs == 0 then
172 empty
173 else
174 text "---------- Other goals: ----------" <$$>
175 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
177 freeEnvNames :: Env -> [Name]
178 freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))
180lifte :: ElabState EState -> ElabD a -> Idris a
181lifte st e = do (v, _) <- elabStep st e
182 return v
184receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)
185receiveInput h e =
186 do i <- getIState
187 let inh = if h == stdout then stdin else h
188 len' <- runIO $ IdeMode.getLen inh
189 len <- case len' of
190 Left err -> ierror err
191 Right n -> return n
192 l <- runIO $ IdeMode.getNChar inh len ""
193 (sexp, id) <- case IdeMode.parseMessage l of
194 Left err -> ierror err
195 Right (sexp, id) -> return (sexp, id)
196 putIState $ i { idris_outputmode = (IdeMode id h) }
197 case IdeMode.sexpToCommand sexp of
198 Just (IdeMode.REPLCompletions prefix) ->
199 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
200 let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]
201 idemodePutSExp "return" good
202 receiveInput h e
203 Just (IdeMode.Interpret cmd) -> return (Just cmd)
204 Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))
205 Just (IdeMode.DocsFor str _) -> return (Just (":doc " ++ str))
206 _ -> return Nothing
208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])
209ploop fn d prompt prf e h
210 = do i <- getIState
211 let autoSolve = opt_autoSolve (idris_options i)
212 when d $ dumpState i (proof e)
213 (x, h') <-
214 case idris_outputmode i of
215 RawOutput _ ->
216 runInputT (proverSettings e) $
217 -- Manually track the history so that we can use the proof state
218 do case h of
219 Just history -> putHistory history
220 Nothing -> return ()
221 l <- getInputLine (prompt ++ "> ")
222 h' <- getHistory
223 return (l, Just h')
224 IdeMode _ handle ->
225 do isetPrompt prompt
226 i <- receiveInput handle e
227 return (i, h)
228 (cmd, step) <- case x of
229 Nothing -> do iPrintError ""; ifail "Abandoned"
230 Just input -> do return (parseTactic i input, input)
231 case cmd of
232 Success Abandon -> do iPrintError ""; ifail "Abandoned"
233 _ -> return ()
234 (d, st, done, prf', res) <- idrisCatch
235 (case cmd of
236 Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
237 Success Undo -> do (_, st) <- elabStep e loadState
238 return (True, st, False, init prf, Right $ iPrintResult "")
239 Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
240 Success ProofTerm -> do tm <- lifte e get_term
241 iputStrLn $ "TT: " ++ show tm ++ "\n"
242 return (False, e, False, prf, Right $ iPrintResult "")
243 Success Qed -> do hs <- lifte e get_holes
244 when (not (null hs)) $ ifail "Incomplete proof"
245 iputStrLn "Proof completed!"
246 return (False, e, True, prf, Right $ iPrintResult "")
247 Success (TCheck (PRef _ n)) -> checkNameType n
248 Success (TCheck t) -> checkType t
249 Success (TEval t) -> evalTerm t e
250 Success (TDocStr x) -> docStr x
251 Success (TSearch t) -> search t
252 Success tac ->
253 do (_, e) <- elabStep e saveState
254 (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
255 return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
256 (\err -> return (False, e, False, prf, Left err))
257 idemodePutSExp "write-proof-state" (prf', length prf')
258 case res of
259 Left err -> do ist <- getIState
260 iRenderError $ pprintErr ist err
261 ploop fn d prompt prf' st h'
262 Right ok ->
263 if done then do (tm, _) <- elabStep st get_term
264 return (tm, prf')
265 else do ok
266 ploop fn d prompt prf' st h'
267 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
268 checkNameType n = do
269 ctxt <- getContext
270 ist <- getIState
271 imp <- impShow
272 idrisCatch (do
273 let OK env = envAtFocus (proof e)
274 ctxt' = envCtxt env ctxt
275 bnd = map (\x -> (fst x, False)) env
276 ist' = ist { tt_ctxt = ctxt' }
277 putIState ist'
278 -- Unlike the REPL, metavars have no special treatment, to
279 -- make it easier to see how to prove with them.
280 let action = case lookupNames n ctxt' of
281 [] -> iPrintError $ "No such variable " ++ show n
282 ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
283 putIState ist
284 return (False, e, False, prf, Right action))
285 (\err -> do putIState ist ; ierror err)
287 checkType t = do
288 ist <- getIState
289 ctxt <- getContext
290 idrisCatch (do
291 let OK env = envAtFocus (proof e)
292 ctxt' = envCtxt env ctxt
293 putIState ist { tt_ctxt = ctxt' }
294 (tm, ty) <- elabVal recinfo ERHS t
295 let ppo = ppOptionIst ist
296 ty' = normaliseC ctxt [] ty
297 infixes = idris_infixes ist
298 action = case tm of
299 TType _ ->
300 iPrintTermWithType (prettyImp ppo PType) type1Doc
301 _ -> let bnd = map (\x -> (fst x, False)) env in
302 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))
303 (pprintPTerm ppo bnd [] infixes (delab ist ty))
304 putIState ist
305 return (False, e, False, prf, Right action))
306 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
308 proverFC = FC "(prover shell)" (0, 0) (0, 0)
310 evalTerm t e = withErrorReflection $
311 do ctxt <- getContext
312 ist <- getIState
313 idrisCatch (do
314 let OK env = envAtFocus (proof e)
315 ctxt' = envCtxt env ctxt
316 ist' = ist { tt_ctxt = ctxt' }
317 bnd = map (\x -> (fst x, False)) env
318 putIState ist'
319 (tm, ty) <- elabVal recinfo ERHS t
320 let tm' = force (normaliseAll ctxt' env tm)
321 ty' = force (normaliseAll ctxt' env ty)
322 ppo = ppOption (idris_options ist')
323 infixes = idris_infixes ist
324 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
325 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
326 action = iPrintTermWithType tmDoc tyDoc
327 putIState ist
328 return (False, e, False, prf, Right action))
329 (\err -> do putIState ist ; ierror err)
330 docStr :: Either Name Const -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))
331 docStr (Left n) = do ist <- getIState
332 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of
333 [] -> return (False, e, False, prf,
334 Left . Msg $ "No documentation for " ++ show n)
335 ns -> do toShow <- mapM (showDoc ist) ns
336 return (False, e, False, prf,
337 Right $ iRenderResult (vsep toShow)))
338 (\err -> do putIState ist ; ierror err)
339 where showDoc ist (n, d) = do doc <- getDocs n FullDocs
340 return $ pprintDocs ist doc
341 docStr (Right c) = do ist <- getIState
342 return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))
343 search t = return (False, e, False, prf, Right $ searchByType [] t)