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