git.iko.soy/Idris-dev
on dd09721 help sign in
Idris-dev/src/Idris/Prover.hs
276 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
88elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
89elabStep st e = do case runStateT e st of
90 OK (a, st') -> return (a, st')
91 Error a -> ierror a
93dumpState :: IState -> ProofState -> Idris ()
94dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
95 do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."
96 iputGoal rendered
97dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do
98 let OK ty = goalAtFocus ps
99 let OK env = envAtFocus ps
100 let state = prettyOtherGoals hs <> line <>
101 prettyAssumptions env <> line <>
102 prettyGoal (zip (assumptionNames env) (repeat False)) ty
103 rendered <- iRender state
104 iputGoal rendered
106 where
107 showImplicits = opt_showimp (idris_options ist)
109 tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t
111 assumptionNames :: Env -> [Name]
112 assumptionNames = map fst
114 prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
115 prettyPs bnd [] = empty
116 prettyPs bnd ((n@(MN _ r), _) : bs)
117 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
118 prettyPs bnd ((n, Let t v) : bs) =
119 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
120 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
121 prettyPs bnd ((n, b) : bs) =
122 line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
124 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
125 prettyG bnd b = tPretty bnd $ binderTy b
127 prettyGoal bnd ty =
128 text "---------- Goal: ----------" <$$>
129 bindingOf h False <+> colon <+> align (prettyG bnd ty)
131 prettyAssumptions env =
132 if length env == 0 then
133 empty
134 else
135 text "---------- Assumptions: ----------" <>
136 nest nestingSize (prettyPs [] $ reverse env)
138 prettyOtherGoals hs =
139 if length hs == 0 then
140 empty
141 else
142 text "---------- Other goals: ----------" <$$>
143 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
145lifte :: ElabState [PDecl] -> ElabD a -> Idris a
146lifte st e = do (v, _) <- elabStep st e
147 return v
149receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
150receiveInput e =
151 do i <- getIState
152 l <- runIO $ getLine
153 (sexp, id) <- case parseMessage l of
154 Left err -> ierror err
155 Right (sexp, id) -> return (sexp, id)
156 putIState $ i { idris_outputmode = (IdeSlave id) }
157 case sexpToCommand sexp of
158 Just (REPLCompletions prefix) ->
159 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
160 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
161 ideslavePutSExp "return" good
162 receiveInput e
163 Just (Interpret cmd) -> return (Just cmd)
164 Nothing -> return Nothing
166ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
167ploop fn d prompt prf e h
168 = do i <- getIState
169 let autoSolve = opt_autoSolve (idris_options i)
170 when d $ dumpState i (proof e)
171 (x, h') <-
172 case idris_outputmode i of
173 RawOutput -> runInputT (proverSettings e) $
174 -- Manually track the history so that we can use the proof state
175 do _ <- case h of
176 Just history -> putHistory history
177 Nothing -> return ()
178 l <- getInputLine (prompt ++ "> ")
179 h' <- getHistory
180 return (l, Just h')
181 IdeSlave n ->
182 do isetPrompt prompt
183 i <- receiveInput e
184 return (i, h)
185 (cmd, step) <- case x of
186 Nothing -> do iPrintError ""; ifail "Abandoned"
187 Just input -> do return (parseTactic i input, input)
188 case cmd of
189 Success Abandon -> do iPrintError ""; ifail "Abandoned"
190 _ -> return ()
191 (d, st, done, prf') <- idrisCatch
192 (case cmd of
193 Failure err -> do iPrintError (show err)
194 return (False, e, False, prf)
195 Success Undo -> do (_, st) <- elabStep e loadState
196 iPrintResult ""
197 return (True, st, False, init prf)
198 Success ProofState -> do iPrintResult ""
199 return (True, e, False, prf)
200 Success ProofTerm -> do tm <- lifte e get_term
201 iPrintResult $ "TT: " ++ show tm ++ "\n"
202 return (False, e, False, prf)
203 Success Qed -> do hs <- lifte e get_holes
204 when (not (null hs)) $ ifail "Incomplete proof"
205 iPrintResult "Proof completed!"
206 return (False, e, True, prf)
207 Success (TCheck (PRef _ n)) ->
208 do ctxt <- getContext
209 ist <- getIState
210 imp <- impShow
211 idrisCatch (do
212 let h = idris_outh ist
213 OK env = envAtFocus (proof e)
214 ctxt' = envCtxt env ctxt
215 bnd = map (\x -> (fst x, False)) env
216 ist' = ist { tt_ctxt = ctxt' }
217 putIState ist'
218 -- Unlike the REPL, metavars have no special treatment, to
219 -- make it easier to see how to prove with them.
220 case lookupNames n ctxt' of
221 [] -> ihPrintError h $ "No such variable " ++ show n
222 ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
223 putIState ist
224 return (False, e, False, prf))
225 (\err -> do putIState ist ; ierror err)
226 Success (TCheck t) ->
227 do ist <- getIState
228 ctxt <- getContext
229 idrisCatch (do
230 let OK env = envAtFocus (proof e)
231 ctxt' = envCtxt env ctxt
232 putIState ist { tt_ctxt = ctxt' }
233 (tm, ty) <- elabVal toplevel False t
234 let imp = opt_showimp (idris_options ist)
235 ty' = normaliseC ctxt [] ty
236 h = idris_outh ist
237 case tm of
238 TType _ ->
239 ihPrintTermWithType h (prettyImp imp PType) type1Doc
240 _ -> let bnd = map (\x -> (fst x, False)) env in
241 ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))
242 (pprintPTerm imp bnd [] (delab ist ty))
243 putIState ist
244 return (False, e, False, prf))
245 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
246 Success (TEval t) -> withErrorReflection $
247 do ctxt <- getContext
248 ist <- getIState
249 idrisCatch (do
250 let OK env = envAtFocus (proof e)
251 ctxt' = envCtxt env ctxt
252 ist' = ist { tt_ctxt = ctxt' }
253 bnd = map (\x -> (fst x, False)) env
254 putIState ist'
255 (tm, ty) <- elabVal toplevel False t
256 let tm' = force (normaliseAll ctxt' env tm)
257 ty' = force (normaliseAll ctxt' env ty)
258 imp = opt_showimp (idris_options ist')
259 tmDoc = pprintPTerm imp bnd [] (delab ist' tm')
260 tyDoc = pprintPTerm imp bnd [] (delab ist' ty')
261 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
262 putIState ist
263 return (False, e, False, prf))
264 (\err -> do putIState ist ; ierror err)
265 Success tac -> do (_, e) <- elabStep e saveState
266 (_, st) <- elabStep e (runTac autoSolve i fn tac)
267-- trace (show (problems (proof st))) $
268 iPrintResult ""
269 return (True, st, False, prf ++ [step]))
270 (\err -> do iPrintError (pshow i err)
271 return (False, e, False, prf))
272 ideslavePutSExp "write-proof-state" (prf', length prf')
273 if done then do (tm, _) <- elabStep st get_term
274 return (tm, prf')
275 else ploop fn d prompt prf' st h'
276 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env