git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/Prover.hs
282 lines 13 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.AbsSyntax
10import Idris.AbsSyntaxTree
11import Idris.Delaborate
12import Idris.ElabDecls
13import Idris.ElabTerm
14import Idris.Parser hiding (params)
15import Idris.Error
16import Idris.DataOpts
17import Idris.Completion
18import Idris.IdeSlave
19import Idris.Output
21import Text.Trifecta.Result(Result(..))
23import System.Console.Haskeline
24import System.Console.Haskeline.History
25import Control.Monad.State.Strict
26import Control.DeepSeq
28import Util.Pretty
29import Debug.Trace
31prover :: Bool -> Name -> Idris ()
32prover lit x =
33 do ctxt <- getContext
34 i <- getIState
35 case lookupTy x ctxt of
36 [t] -> if elem x (map fst (idris_metavars i))
37 then prove (idris_optimisation i) ctxt lit x t
38 else ifail $ show x ++ " is not a metavariable"
39 _ -> fail "No such metavariable"
41showProof :: Bool -> Name -> [String] -> String
42showProof lit n ps
43 = bird ++ show n ++ " = proof" ++ break ++
44 showSep break (map (\x -> " " ++ x) ps) ++
45 break ++ "\n"
46 where bird = if lit then "> " else ""
47 break = "\n" ++ bird
49proverSettings :: ElabState [PDecl] -> Settings Idris
50proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
52assumptionNames :: ElabState [PDecl] -> [String]
53assumptionNames e
54 = case envAtFocus (proof e) of
55 OK env -> names env
56 where names [] = []
57 names ((MN _ _, _) : bs) = names bs
58 names ((n, _) : bs) = show n : names bs
60prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
61prove opt ctxt lit n ty
62 = do let ps = initElaborator n ctxt ty
63 ideslavePutSExp "start-proof-mode" n
64 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
65 iLOG $ "Adding " ++ show tm
66 iputStrLn $ showProof lit n prf
67 i <- getIState
68 ideslavePutSExp "end-proof-mode" n
69 let proofs = proof_list i
70 putIState (i { proof_list = (n, prf) : proofs })
71 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
72 logLvl 3 (show tree)
73 (ptm, pty) <- recheckC (fileFC "proof") [] tm
74 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
75 "Expected type:" ++ show ty)
76 case converts ctxt [] ty pty of
77 OK _ -> return ()
78 Error e -> ierror (CantUnify False ty pty e [] 0)
79 ptm' <- applyOpts ptm
80 updateContext (addCasedef n (CaseInfo True False) False False True False
81 [] [] -- argtys, inaccArgs
82 [Right (P Ref n ty, ptm)]
83 [([], P Ref n ty, ptm)]
84 [([], P Ref n ty, ptm)]
85 [([], P Ref n ty, ptm)]
86 [([], P Ref n ty, ptm')] ty)
87 solveDeferred n
89elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
90elabStep st e = case runStateT eCheck st of
91 OK (a, st') -> return (a, st')
92 Error a -> ierror a
93 where eCheck = do res <- e
94 tm <- get_term
95 ctxt <- get_context
96 lift $ check ctxt [] (forget tm)
97 return res
99dumpState :: IState -> ProofState -> Idris ()
100dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
101 do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."
102 iputGoal rendered
103dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do
104 let OK ty = goalAtFocus ps
105 let OK env = envAtFocus ps
106 let state = prettyOtherGoals hs <> line <>
107 prettyAssumptions env <> line <>
108 prettyGoal (zip (assumptionNames env) (repeat False)) ty
109 rendered <- iRender state
110 iputGoal rendered
112 where
113 showImplicits = opt_showimp (idris_options ist)
115 tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t
117 assumptionNames :: Env -> [Name]
118 assumptionNames = map fst
120 prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
121 prettyPs bnd [] = empty
122 prettyPs bnd ((n@(MN _ r), _) : bs)
123 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
124 prettyPs bnd ((n, Let t v) : bs) =
125 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
126 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
127 prettyPs bnd ((n, b) : bs) =
128 line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
130 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
131 prettyG bnd b = tPretty bnd $ binderTy b
133 prettyGoal bnd ty =
134 text "---------- Goal: ----------" <$$>
135 bindingOf h False <+> colon <+> align (prettyG bnd ty)
137 prettyAssumptions env =
138 if length env == 0 then
139 empty
140 else
141 text "---------- Assumptions: ----------" <>
142 nest nestingSize (prettyPs [] $ reverse env)
144 prettyOtherGoals hs =
145 if length hs == 0 then
146 empty
147 else
148 text "---------- Other goals: ----------" <$$>
149 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
151lifte :: ElabState [PDecl] -> ElabD a -> Idris a
152lifte st e = do (v, _) <- elabStep st e
153 return v
155receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
156receiveInput e =
157 do i <- getIState
158 l <- runIO $ getLine
159 (sexp, id) <- case parseMessage l of
160 Left err -> ierror err
161 Right (sexp, id) -> return (sexp, id)
162 putIState $ i { idris_outputmode = (IdeSlave id) }
163 case sexpToCommand sexp of
164 Just (REPLCompletions prefix) ->
165 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
166 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
167 ideslavePutSExp "return" good
168 receiveInput e
169 Just (Interpret cmd) -> return (Just cmd)
170 Nothing -> return Nothing
172ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
173ploop fn d prompt prf e h
174 = do i <- getIState
175 let autoSolve = opt_autoSolve (idris_options i)
176 when d $ dumpState i (proof e)
177 (x, h') <-
178 case idris_outputmode i of
179 RawOutput -> runInputT (proverSettings e) $
180 -- Manually track the history so that we can use the proof state
181 do _ <- case h of
182 Just history -> putHistory history
183 Nothing -> return ()
184 l <- getInputLine (prompt ++ "> ")
185 h' <- getHistory
186 return (l, Just h')
187 IdeSlave n ->
188 do isetPrompt prompt
189 i <- receiveInput e
190 return (i, h)
191 (cmd, step) <- case x of
192 Nothing -> do iPrintError ""; ifail "Abandoned"
193 Just input -> do return (parseTactic i input, input)
194 case cmd of
195 Success Abandon -> do iPrintError ""; ifail "Abandoned"
196 _ -> return ()
197 (d, st, done, prf') <- idrisCatch
198 (case cmd of
199 Failure err -> do iPrintError (show err)
200 return (False, e, False, prf)
201 Success Undo -> do (_, st) <- elabStep e loadState
202 iPrintResult ""
203 return (True, st, False, init prf)
204 Success ProofState -> do iPrintResult ""
205 return (True, e, False, prf)
206 Success ProofTerm -> do tm <- lifte e get_term
207 iPrintResult $ "TT: " ++ show tm ++ "\n"
208 return (False, e, False, prf)
209 Success Qed -> do hs <- lifte e get_holes
210 when (not (null hs)) $ ifail "Incomplete proof"
211 iPrintResult "Proof completed!"
212 return (False, e, True, prf)
213 Success (TCheck (PRef _ n)) ->
214 do ctxt <- getContext
215 ist <- getIState
216 imp <- impShow
217 idrisCatch (do
218 let h = idris_outh ist
219 OK env = envAtFocus (proof e)
220 ctxt' = envCtxt env ctxt
221 bnd = map (\x -> (fst x, False)) env
222 ist' = ist { tt_ctxt = ctxt' }
223 putIState ist'
224 -- Unlike the REPL, metavars have no special treatment, to
225 -- make it easier to see how to prove with them.
226 case lookupNames n ctxt' of
227 [] -> ihPrintError h $ "No such variable " ++ show n
228 ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
229 putIState ist
230 return (False, e, False, prf))
231 (\err -> do putIState ist ; ierror err)
232 Success (TCheck t) ->
233 do ist <- getIState
234 ctxt <- getContext
235 idrisCatch (do
236 let OK env = envAtFocus (proof e)
237 ctxt' = envCtxt env ctxt
238 putIState ist { tt_ctxt = ctxt' }
239 (tm, ty) <- elabVal toplevel False t
240 let imp = opt_showimp (idris_options ist)
241 ty' = normaliseC ctxt [] ty
242 h = idris_outh ist
243 case tm of
244 TType _ ->
245 ihPrintTermWithType h (prettyImp imp PType) type1Doc
246 _ -> let bnd = map (\x -> (fst x, False)) env in
247 ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))
248 (pprintPTerm imp bnd [] (delab ist ty))
249 putIState ist
250 return (False, e, False, prf))
251 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
252 Success (TEval t) -> withErrorReflection $
253 do ctxt <- getContext
254 ist <- getIState
255 idrisCatch (do
256 let OK env = envAtFocus (proof e)
257 ctxt' = envCtxt env ctxt
258 ist' = ist { tt_ctxt = ctxt' }
259 bnd = map (\x -> (fst x, False)) env
260 putIState ist'
261 (tm, ty) <- elabVal toplevel False t
262 let tm' = force (normaliseAll ctxt' env tm)
263 ty' = force (normaliseAll ctxt' env ty)
264 imp = opt_showimp (idris_options ist')
265 tmDoc = pprintPTerm imp bnd [] (delab ist' tm')
266 tyDoc = pprintPTerm imp bnd [] (delab ist' ty')
267 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
268 putIState ist
269 return (False, e, False, prf))
270 (\err -> do putIState ist ; ierror err)
271 Success tac -> do (_, e) <- elabStep e saveState
272 (_, st) <- elabStep e (runTac autoSolve i fn tac)
273-- trace (show (problems (proof st))) $
274 iPrintResult ""
275 return (True, st, False, prf ++ [step]))
276 (\err -> do iPrintError (pshow i err)
277 return (False, e, False, prf))
278 ideslavePutSExp "write-proof-state" (prf', length prf')
279 if done then do (tm, _) <- elabStep st get_term
280 return (tm, prf')
281 else ploop fn d prompt prf' st h'
282 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env