@@ -14,6 +14,7 @@ import Idris.Parser
1414import Idris.Error
1515import Idris.DataOpts
1616import Idris.Completion
17+import Idris.IdeSlave
1718
1819import System.Console.Haskeline
1920import System.Console.Haskeline.History
@@ -41,26 +42,31 @@ showProof lit n ps
4142 break = "\n" ++ bird
4243
4344proverSettings :: ElabState [PDecl] -> Settings Idris
44−proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings
45− where assumptionNames = case envAtFocus (proof e) of
46− OK env -> names env
47− names [] = []
48− names ((MN _ _, _) : bs) = names bs
49− names ((n, _) : bs) = show n : names bs
45+proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
46+
47+assumptionNames :: ElabState [PDecl] -> [String]
48+assumptionNames 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
5054
5155prove :: Context -> Bool -> Name -> Type -> Idris ()
52−prove ctxt lit n ty
56+prove ctxt lit n ty
5357 = do let ps = initElaborator n ctxt ty
58+ ideslavePutSExp "start-proof-mode" n
5459 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
5560 iLOG $ "Adding " ++ show tm
5661 iputStrLn $ showProof lit n prf
5762 i <- getIState
63+ ideslavePutSExp "end-proof-mode" n
5864 let proofs = proof_list i
5965 putIState (i { proof_list = (n, prf) : proofs })
6066 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
6167 logLvl 3 (show tree)
6268 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
63− logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
69+ logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
6470 "Expected type:" ++ show ty)
6571 case converts ctxt [] ty pty of
6672 OK _ -> return ()
@@ -68,7 +74,7 @@ prove ctxt lit n ty
6874 ptm' <- applyOpts ptm
6975 updateContext (addCasedef n True False True False
7076 [Right (P Ref n ty, ptm)]
71− [([], P Ref n ty, ptm)]
77+ [([], P Ref n ty, ptm)]
7278 [([], P Ref n ty, ptm')] ty)
7379 solveDeferred n
7480elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
@@ -77,13 +83,13 @@ elabStep st e = do case runStateT e st of
7783 Error a -> do i <- getIState
7884 fail (pshow i a)
7985
80−dumpState :: IState -> ProofState -> IO ()
86+dumpState :: IState -> ProofState -> Idris ()
8187dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
82− putStrLn . render $ pretty nm <> colon <+> text "No more goals."
88+ iputGoal . render $ pretty nm <> colon <+> text "No more goals."
8389dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
8490 let OK ty = goalAtFocus ps
8591 let OK env = envAtFocus ps
86− putStrLn . render $
92+ iputGoal . render $
8793 prettyOtherGoals hs $$
8894 prettyAssumptions env $$
8995 prettyGoal ty
@@ -124,46 +130,69 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
124130lifte st e = do (v, _) <- elabStep st e
125131 return v
126132
133+receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
134+receiveInput e =
135+ do i <- getIState
136+ l <- liftIO $ getLine
137+ let (sexp, id) = parseMessage l
138+ putIState $ i { idris_outputmode = (IdeSlave id) }
139+ case sexpToCommand sexp of
140+ Just (REPLCompletions prefix) ->
141+ do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
142+ let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
143+ ideslavePutSExp "return" good
144+ receiveInput e
145+ Just (Interpret cmd) -> return (Just cmd)
146+ Nothing -> return Nothing
147+
127148ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128149ploop d prompt prf e h
129150 = do i <- getIState
130− when d $ liftIO $ dumpState i (proof e)
131− (x, h') <- runInputT (proverSettings e) $
132− -- Manually track the history so that we can use the proof state
133− do _ <- case h of
134− Just history -> putHistory history
135− Nothing -> return ()
136− l <- getInputLine (prompt ++ "> ")
137− h' <- getHistory
138− return (l, Just h')
151+ when d $ dumpState i (proof e)
152+ (x, h') <-
153+ case idris_outputmode i of
154+ RawOutput -> runInputT (proverSettings e) $
155+ -- Manually track the history so that we can use the proof state
156+ do _ <- case h of
157+ Just history -> putHistory history
158+ Nothing -> return ()
159+ l <- getInputLine (prompt ++ "> ")
160+ h' <- getHistory
161+ return (l, Just h')
162+ IdeSlave n ->
163+ do isetPrompt prompt
164+ i <- receiveInput e
165+ return (i, h)
139166 (cmd, step) <- case x of
140− Nothing -> fail "Abandoned"
167+ Nothing -> do iFail ""; fail "Abandoned"
141168 Just input -> do return (parseTac i input, input)
142169 case cmd of
143− Right Abandon -> fail "Abandoned"
170+ Right Abandon -> do iFail ""; fail "Abandoned"
144171 _ -> return ()
145172 (d, st, done, prf') <- idrisCatch
146173 (case cmd of
147− Left err -> do iputStrLn (show err)
174+ Left err -> do iFail (show err)
148175 return (False, e, False, prf)
149− Right Undo ->
150− do (_, st) <- elabStep e loadState
151− return (True, st, False, init prf)
152− Right ProofState ->
153− return (True, e, False, prf)
154− Right ProofTerm ->
155− do tm <- lifte e get_term
156− iputStrLn $ "TT: " ++ show tm ++ "\n"
157− return (False, e, False, prf)
176+ Right Undo -> do (_, st) <- elabStep e loadState
177+ iResult ""
178+ return (True, st, False, init prf)
179+ Right ProofState -> do iResult ""
180+ return (True, e, False, prf)
181+ Right ProofTerm -> do tm <- lifte e get_term
182+ iResult $ "TT: " ++ show tm ++ "\n"
183+ return (False, e, False, prf)
158184 Right Qed -> do hs <- lifte e get_holes
159185 when (not (null hs)) $ fail "Incomplete proof"
186+ iResult "Proof completed!"
160187 return (False, e, True, prf)
161188 Right tac -> do (_, e) <- elabStep e saveState
162189 (_, st) <- elabStep e (runTac True i tac)
163−-- trace (show (problems (proof st))) $
190+-- trace (show (problems (proof st))) $
191+ iResult ""
164192 return (True, st, False, prf ++ [step]))
165− (\err -> do iputStrLn (show err)
193+ (\err -> do iFail (show err)
166194 return (False, e, False, prf))
195+ ideslavePutSExp "write-proof-state" (prf', length prf')
167196 if done then do (tm, _) <- elabStep st get_term
168197 return (tm, prf')
169198 else ploop d prompt prf' st h'