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