git.iko.soy/Idris-dev
on e63fcef help sign in
Idris-dev/src/Idris/Prover.hs
206 lines 8.3 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.Delaborate
11import Idris.ElabDecls
12import Idris.ElabTerm
13import Idris.Parser
14import Idris.Error
15import Idris.DataOpts
16import Idris.Completion
17import Idris.IdeSlave
19import Text.Trifecta.Result(Result(..))
21import System.Console.Haskeline
22import System.Console.Haskeline.History
23import Control.Monad.State.Strict
25import Util.Pretty
26import Debug.Trace
28prover :: Bool -> Name -> Idris ()
29prover lit x =
30 do ctxt <- getContext
31 i <- getIState
32 case lookupTy x ctxt of
33 [t] -> if elem x (map fst (idris_metavars i))
34 then prove ctxt lit x t
35 else ifail $ show x ++ " is not a metavariable"
36 _ -> fail "No such metavariable"
38showProof :: Bool -> Name -> [String] -> String
39showProof lit n ps
40 = bird ++ show n ++ " = proof" ++ break ++
41 showSep break (map (\x -> " " ++ x) ps) ++
42 break ++ "\n"
43 where bird = if lit then "> " else ""
44 break = "\n" ++ bird
46proverSettings :: ElabState [PDecl] -> Settings Idris
47proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
49assumptionNames :: ElabState [PDecl] -> [String]
50assumptionNames e
51 = case envAtFocus (proof e) of
52 OK env -> names env
53 where names [] = []
54 names ((MN _ _, _) : bs) = names bs
55 names ((n, _) : bs) = show n : names bs
57prove :: Context -> Bool -> Name -> Type -> Idris ()
58prove ctxt lit n ty
59 = do let ps = initElaborator n ctxt ty
60 ideslavePutSExp "start-proof-mode" n
61 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
62 iLOG $ "Adding " ++ show tm
63 iputStrLn $ showProof lit n prf
64 i <- getIState
65 ideslavePutSExp "end-proof-mode" n
66 let proofs = proof_list i
67 putIState (i { proof_list = (n, prf) : proofs })
68 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [([], P Ref n ty, tm)]
69 logLvl 3 (show tree)
70 (ptm, pty) <- recheckC (fileFC "proof") [] tm
71 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
72 "Expected type:" ++ show ty)
73 case converts ctxt [] ty pty of
74 OK _ -> return ()
75 Error e -> ierror (CantUnify False ty pty e [] 0)
76 ptm' <- applyOpts ptm
77 updateContext (addCasedef n (CaseInfo True False) False False True False
78 []
79 [Right (P Ref n ty, ptm)]
80 [([], P Ref n ty, ptm)]
81 [([], P Ref n ty, ptm)]
82 [([], P Ref n ty, ptm)]
83 [([], P Ref n ty, ptm')] ty)
84 solveDeferred n
85elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
86elabStep st e = do case runStateT e st of
87 OK (a, st') -> return (a, st')
88 Error a -> ierror a
90dumpState :: IState -> ProofState -> Idris ()
91dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
92 iputGoal . render $ pretty nm <> colon <+> text "No more goals."
93dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
94 let OK ty = goalAtFocus ps
95 let OK env = envAtFocus ps
96 iputGoal . render $
97 prettyOtherGoals hs $$
98 prettyAssumptions env $$
99 prettyGoal ty
100 where
101 -- XXX
102 tPretty t = pretty $ delab ist t
104 prettyPs [] = empty
105 prettyPs ((MN _ r, _) : bs)
106 | r == txt "rewrite_rule" = prettyPs bs
107 prettyPs ((n, Let t v) : bs) =
108 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
109 tPretty t $$ prettyPs bs)
110 prettyPs ((n, b) : bs) =
111 pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
113 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
114 prettyG b = tPretty $ binderTy b
116 prettyGoal ty =
117 text "---------- Goal: ----------" $$
118 pretty h <> colon $$ nest nestingSize (prettyG ty)
120 prettyAssumptions env =
121 if length env == 0 then
122 empty
123 else
124 text "---------- Assumptions: ----------" $$
125 nest nestingSize (prettyPs $ reverse env)
127 prettyOtherGoals hs =
128 if length hs == 0 then
129 empty
130 else
131 text "---------- Other goals: ----------" $$
132 pretty hs
134lifte :: ElabState [PDecl] -> ElabD a -> Idris a
135lifte st e = do (v, _) <- elabStep st e
136 return v
138receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
139receiveInput e =
140 do i <- getIState
141 l <- runIO $ getLine
142 (sexp, id) <- case parseMessage l of
143 Left err -> ierror err
144 Right (sexp, id) -> return (sexp, id)
145 putIState $ i { idris_outputmode = (IdeSlave id) }
146 case sexpToCommand sexp of
147 Just (REPLCompletions prefix) ->
148 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
149 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
150 ideslavePutSExp "return" good
151 receiveInput e
152 Just (Interpret cmd) -> return (Just cmd)
153 Nothing -> return Nothing
155ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
156ploop d prompt prf e h
157 = do i <- getIState
158 when d $ dumpState i (proof e)
159 (x, h') <-
160 case idris_outputmode i of
161 RawOutput -> runInputT (proverSettings e) $
162 -- Manually track the history so that we can use the proof state
163 do _ <- case h of
164 Just history -> putHistory history
165 Nothing -> return ()
166 l <- getInputLine (prompt ++ "> ")
167 h' <- getHistory
168 return (l, Just h')
169 IdeSlave n ->
170 do isetPrompt prompt
171 i <- receiveInput e
172 return (i, h)
173 (cmd, step) <- case x of
174 Nothing -> do iPrintError ""; fail "Abandoned"
175 Just input -> do return (parseTactic i input, input)
176 case cmd of
177 Success Abandon -> do iPrintError ""; fail "Abandoned"
178 _ -> return ()
179 (d, st, done, prf') <- idrisCatch
180 (case cmd of
181 Failure err -> do iPrintError (show err)
182 return (False, e, False, prf)
183 Success Undo -> do (_, st) <- elabStep e loadState
184 iPrintResult ""
185 return (True, st, False, init prf)
186 Success ProofState -> do iPrintResult ""
187 return (True, e, False, prf)
188 Success ProofTerm -> do tm <- lifte e get_term
189 iPrintResult $ "TT: " ++ show tm ++ "\n"
190 return (False, e, False, prf)
191 Success Qed -> do hs <- lifte e get_holes
192 when (not (null hs)) $ ifail "Incomplete proof"
193 iPrintResult "Proof completed!"
194 return (False, e, True, prf)
195 Success tac -> do (_, e) <- elabStep e saveState
196 (_, st) <- elabStep e (runTac True i tac)
197-- trace (show (problems (proof st))) $
198 iPrintResult ""
199 return (True, st, False, prf ++ [step]))
200 (\err -> do iPrintError (pshow i err)
201 return (False, e, False, prf))
202 ideslavePutSExp "write-proof-state" (prf', length prf')
203 if done then do (tm, _) <- elabStep st get_term
204 return (tm, prf')
205 else ploop d prompt prf' st h'