git.iko.soy/Idris-dev
on de72eb9 help sign in
Idris-dev/src/Idris/Prover.hs
211 lines 8.8 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 . renderPretty 0.7 breakingSize $
93 prettyName False [] nm <> colon <+> text "No more goals."
94dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
95 let OK ty = goalAtFocus ps
96 let OK env = envAtFocus ps
97 iputGoal . renderPretty 0.7 breakingSize $
98 prettyOtherGoals hs <> line <>
99 prettyAssumptions env <> line <>
100 prettyGoal (zip (assumptionNames env) (repeat False)) ty
101 where
102 -- XXX
103 tPretty bnd t = pprintPTerm True bnd $ delab ist t
105 assumptionNames :: Env -> [Name]
106 assumptionNames = map fst
108 prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
109 prettyPs bnd [] = empty
110 prettyPs bnd ((n@(MN _ r), _) : bs)
111 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
112 prettyPs bnd ((n, Let t v) : bs) =
113 nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
114 tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
115 prettyPs bnd ((n, b) : bs) =
116 line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs
118 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
119 prettyG bnd b = tPretty bnd $ binderTy b
121 prettyGoal bnd ty =
122 text "---------- Goal: ----------" <$$>
123 bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)
125 prettyAssumptions env =
126 if length env == 0 then
127 empty
128 else
129 text "---------- Assumptions: ----------" <>
130 nest nestingSize (prettyPs [] $ reverse env)
132 prettyOtherGoals hs =
133 if length hs == 0 then
134 empty
135 else
136 text "---------- Other goals: ----------" <$$>
137 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
139lifte :: ElabState [PDecl] -> ElabD a -> Idris a
140lifte st e = do (v, _) <- elabStep st e
141 return v
143receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
144receiveInput e =
145 do i <- getIState
146 l <- runIO $ getLine
147 (sexp, id) <- case parseMessage l of
148 Left err -> ierror err
149 Right (sexp, id) -> return (sexp, id)
150 putIState $ i { idris_outputmode = (IdeSlave id) }
151 case sexpToCommand sexp of
152 Just (REPLCompletions prefix) ->
153 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
154 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
155 ideslavePutSExp "return" good
156 receiveInput e
157 Just (Interpret cmd) -> return (Just cmd)
158 Nothing -> return Nothing
160ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
161ploop d prompt prf e h
162 = do i <- getIState
163 when d $ dumpState i (proof e)
164 (x, h') <-
165 case idris_outputmode i of
166 RawOutput -> runInputT (proverSettings e) $
167 -- Manually track the history so that we can use the proof state
168 do _ <- case h of
169 Just history -> putHistory history
170 Nothing -> return ()
171 l <- getInputLine (prompt ++ "> ")
172 h' <- getHistory
173 return (l, Just h')
174 IdeSlave n ->
175 do isetPrompt prompt
176 i <- receiveInput e
177 return (i, h)
178 (cmd, step) <- case x of
179 Nothing -> do iPrintError ""; fail "Abandoned"
180 Just input -> do return (parseTactic i input, input)
181 case cmd of
182 Success Abandon -> do iPrintError ""; fail "Abandoned"
183 _ -> return ()
184 (d, st, done, prf') <- idrisCatch
185 (case cmd of
186 Failure err -> do iPrintError (show err)
187 return (False, e, False, prf)
188 Success Undo -> do (_, st) <- elabStep e loadState
189 iPrintResult ""
190 return (True, st, False, init prf)
191 Success ProofState -> do iPrintResult ""
192 return (True, e, False, prf)
193 Success ProofTerm -> do tm <- lifte e get_term
194 iPrintResult $ "TT: " ++ show tm ++ "\n"
195 return (False, e, False, prf)
196 Success Qed -> do hs <- lifte e get_holes
197 when (not (null hs)) $ ifail "Incomplete proof"
198 iPrintResult "Proof completed!"
199 return (False, e, True, prf)
200 Success tac -> do (_, e) <- elabStep e saveState
201 (_, st) <- elabStep e (runTac True i tac)
202-- trace (show (problems (proof st))) $
203 iPrintResult ""
204 return (True, st, False, prf ++ [step]))
205 (\err -> do iPrintError (pshow i err)
206 return (False, e, False, prf))
207 ideslavePutSExp "write-proof-state" (prf', length prf')
208 if done then do (tm, _) <- elabStep st get_term
209 return (tm, prf')
210 else ploop d prompt prf' st h'