@@ -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,12 +42,15 @@ 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 ()
5256prove ctxt lit n ty
@@ -124,6 +128,21 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
124128lifte st e = do (v, _) <- elabStep st e
125129 return v
126130
131+receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
132+receiveInput e =
133+ do i <- getIState
134+ l <- liftIO $ getLine
135+ let (sexp, id) = parseMessage l
136+ putIState $ i { idris_outputmode = (IdeSlave id) }
137+ case sexpToCommand sexp of
138+ Just (REPLCompletions prefix) ->
139+ do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
140+ let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
141+ liftIO $ putStrLn $ convSExp "return" good id
142+ receiveInput e
143+ Just (Interpret cmd) -> return (Just cmd)
144+ Nothing -> return Nothing
145+
127146ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128147ploop d prompt prf e h
129148 = do i <- getIState
@@ -138,36 +157,38 @@ ploop d prompt prf e h
138157 l <- getInputLine (prompt ++ "> ")
139158 h' <- getHistory
140159 return (l, Just h')
141− IdeSlave n -> -- waitforinput
160+ IdeSlave n ->
142161 do isetPrompt prompt
143− return (Just "trivial", h)
162+ i <- receiveInput e
163+ return (i, h)
144164 (cmd, step) <- case x of
145− Nothing -> fail "Abandoned"
165+ Nothing -> do iFail ""; fail "Abandoned"
146166 Just input -> do return (parseTac i input, input)
147167 case cmd of
148− Right Abandon -> fail "Abandoned"
168+ Right Abandon -> do iFail ""; fail "Abandoned"
149169 _ -> return ()
150170 (d, st, done, prf') <- idrisCatch
151171 (case cmd of
152− Left err -> do iputStrLn (show err)
172+ Left err -> do iFail (show err)
153173 return (False, e, False, prf)
154− Right Undo ->
155− do (_, st) <- elabStep e loadState
156− return (True, st, False, init prf)
157− Right ProofState ->
158− return (True, e, False, prf)
159− Right ProofTerm ->
160− do tm <- lifte e get_term
161− iputStrLn $ "TT: " ++ show tm ++ "\n"
162− return (False, e, False, prf)
174+ Right Undo -> do (_, st) <- elabStep e loadState
175+ iResult ""
176+ return (True, st, False, init prf)
177+ Right ProofState -> do iResult ""
178+ return (True, e, False, prf)
179+ Right ProofTerm -> do tm <- lifte e get_term
180+ iResult $ "TT: " ++ show tm ++ "\n"
181+ return (False, e, False, prf)
163182 Right Qed -> do hs <- lifte e get_holes
164183 when (not (null hs)) $ fail "Incomplete proof"
184+ iResult "Proof completed!"
165185 return (False, e, True, prf)
166186 Right tac -> do (_, e) <- elabStep e saveState
167187 (_, st) <- elabStep e (runTac True i tac)
168−-- trace (show (problems (proof st))) $
188+-- trace (show (problems (proof st))) $
189+ iResult ""
169190 return (True, st, False, prf ++ [step]))
170− (\err -> do iputStrLn (show err)
191+ (\err -> do iFail (show err)
171192 return (False, e, False, prf))
172193 if done then do (tm, _) <- elabStep st get_term
173194 return (tm, prf')