git.iko.soy/Idris-dev
on ad995dc help sign in
Idris-dev/src/Idris/Prover.hs
204 lines 8.2 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
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 [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 (sexp, id) <- case parseMessage l of
141 Left err -> ierror err
142 Right (sexp, id) -> return (sexp, id)
143 putIState $ i { idris_outputmode = (IdeSlave id) }
144 case sexpToCommand sexp of
145 Just (REPLCompletions prefix) ->
146 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
147 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
148 ideslavePutSExp "return" good
149 receiveInput e
150 Just (Interpret cmd) -> return (Just cmd)
151 Nothing -> return Nothing
153ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
154ploop d prompt prf e h
155 = do i <- getIState
156 when d $ dumpState i (proof e)
157 (x, h') <-
158 case idris_outputmode i of
159 RawOutput -> runInputT (proverSettings e) $
160 -- Manually track the history so that we can use the proof state
161 do _ <- case h of
162 Just history -> putHistory history
163 Nothing -> return ()
164 l <- getInputLine (prompt ++ "> ")
165 h' <- getHistory
166 return (l, Just h')
167 IdeSlave n ->
168 do isetPrompt prompt
169 i <- receiveInput e
170 return (i, h)
171 (cmd, step) <- case x of
172 Nothing -> do iPrintError ""; fail "Abandoned"
173 Just input -> do return (parseTactic i input, input)
174 case cmd of
175 Success Abandon -> do iPrintError ""; fail "Abandoned"
176 _ -> return ()
177 (d, st, done, prf') <- idrisCatch
178 (case cmd of
179 Failure err -> do iPrintError (show err)
180 return (False, e, False, prf)
181 Success Undo -> do (_, st) <- elabStep e loadState
182 iPrintResult ""
183 return (True, st, False, init prf)
184 Success ProofState -> do iPrintResult ""
185 return (True, e, False, prf)
186 Success ProofTerm -> do tm <- lifte e get_term
187 iPrintResult $ "TT: " ++ show tm ++ "\n"
188 return (False, e, False, prf)
189 Success Qed -> do hs <- lifte e get_holes
190 when (not (null hs)) $ ifail "Incomplete proof"
191 iPrintResult "Proof completed!"
192 return (False, e, True, prf)
193 Success tac -> do (_, e) <- elabStep e saveState
194 (_, st) <- elabStep e (runTac True i tac)
195-- trace (show (problems (proof st))) $
196 iPrintResult ""
197 return (True, st, False, prf ++ [step]))
198 (\err -> do iPrintError (pshow i err)
199 return (False, e, False, prf))
200 ideslavePutSExp "write-proof-state" (prf', length prf')
201 if done then do (tm, _) <- elabStep st get_term
202 return (tm, prf')
203 else ploop d prompt prf' st h'