git.iko.soy/Idris-dev
on bba09bd help sign in
Idris-dev/src/Idris/Prover.hs
202 lines 8.0 kB history raw
1module Idris.Prover where
3import Core.Elaborate hiding (Tactic(..))
4import Core.TT
5import Core.Evaluate
6import Core.CaseTree
7import 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
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 (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 [Right (P Ref n ty, ptm)]
79 [([], P Ref n ty, ptm)]
80 [([], P Ref n ty, ptm)]
81 [([], P Ref n ty, ptm)]
82 [([], P Ref n ty, ptm')] ty)
83 solveDeferred n
84elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
85elabStep st e = do case runStateT e st of
86 OK (a, st') -> return (a, st')
87 Error a -> ierror a
89dumpState :: IState -> ProofState -> Idris ()
90dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
91 iputGoal . render $ pretty nm <> colon <+> text "No more goals."
92dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
93 let OK ty = goalAtFocus ps
94 let OK env = envAtFocus ps
95 iputGoal . render $
96 prettyOtherGoals hs $$
97 prettyAssumptions env $$
98 prettyGoal ty
99 where
100 -- XXX
101 tPretty t = pretty $ delab ist t
103 prettyPs [] = empty
104 prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
105 prettyPs ((n, Let t v) : bs) =
106 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
107 tPretty t $$ prettyPs bs)
108 prettyPs ((n, b) : bs) =
109 pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
111 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
112 prettyG b = tPretty $ binderTy b
114 prettyGoal ty =
115 text "---------- Goal: ----------" $$
116 pretty h <> colon $$ nest nestingSize (prettyG ty)
118 prettyAssumptions env =
119 if length env == 0 then
120 empty
121 else
122 text "---------- Assumptions: ----------" $$
123 nest nestingSize (prettyPs $ reverse env)
125 prettyOtherGoals hs =
126 if length hs == 0 then
127 empty
128 else
129 text "---------- Other goals: ----------" $$
130 pretty hs
132lifte :: ElabState [PDecl] -> ElabD a -> Idris a
133lifte st e = do (v, _) <- elabStep st e
134 return v
136receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
137receiveInput e =
138 do i <- getIState
139 l <- runIO $ getLine
140 let (sexp, id) = parseMessage l
141 putIState $ i { idris_outputmode = (IdeSlave id) }
142 case sexpToCommand sexp of
143 Just (REPLCompletions prefix) ->
144 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
145 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
146 ideslavePutSExp "return" good
147 receiveInput e
148 Just (Interpret cmd) -> return (Just cmd)
149 Nothing -> return Nothing
151ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
152ploop d prompt prf e h
153 = do i <- getIState
154 when d $ dumpState i (proof e)
155 (x, h') <-
156 case idris_outputmode i of
157 RawOutput -> runInputT (proverSettings e) $
158 -- Manually track the history so that we can use the proof state
159 do _ <- case h of
160 Just history -> putHistory history
161 Nothing -> return ()
162 l <- getInputLine (prompt ++ "> ")
163 h' <- getHistory
164 return (l, Just h')
165 IdeSlave n ->
166 do isetPrompt prompt
167 i <- receiveInput e
168 return (i, h)
169 (cmd, step) <- case x of
170 Nothing -> do iPrintError ""; fail "Abandoned"
171 Just input -> do return (parseTactic i input, input)
172 case cmd of
173 Success Abandon -> do iPrintError ""; fail "Abandoned"
174 _ -> return ()
175 (d, st, done, prf') <- idrisCatch
176 (case cmd of
177 Failure err -> do iPrintError (show err)
178 return (False, e, False, prf)
179 Success Undo -> do (_, st) <- elabStep e loadState
180 iPrintResult ""
181 return (True, st, False, init prf)
182 Success ProofState -> do iPrintResult ""
183 return (True, e, False, prf)
184 Success ProofTerm -> do tm <- lifte e get_term
185 iPrintResult $ "TT: " ++ show tm ++ "\n"
186 return (False, e, False, prf)
187 Success Qed -> do hs <- lifte e get_holes
188 when (not (null hs)) $ ifail "Incomplete proof"
189 iPrintResult "Proof completed!"
190 return (False, e, True, prf)
191 Success tac -> do (_, e) <- elabStep e saveState
192 (_, st) <- elabStep e (runTac True i tac)
193-- trace (show (problems (proof st))) $
194 iPrintResult ""
195 return (True, st, False, prf ++ [step]))
196 (\err -> do iPrintError (show err)
197 return (False, e, False, prf))
198 ideslavePutSExp "write-proof-state" (prf', length prf')
199 if done then do (tm, _) <- elabStep st get_term
200 return (tm, prf')
201 else ploop d prompt prf' st h'