@@ -14,6 +14,7 @@ import Idris.Parser
14import Idris.Error
14import Idris.Error
15import Idris.DataOpts
15import Idris.DataOpts
16import Idris.Completion
16import Idris.Completion
18import System.Console.Haskeline
19import System.Console.Haskeline
19import System.Console.Haskeline.History
20import System.Console.Haskeline.History
@@ -41,12 +42,15 @@ showProof lit n ps
41 break = "\n" ++ bird
42 break = "\n" ++ bird
43proverSettings :: ElabState [PDecl] -> Settings Idris
44proverSettings :: ElabState [PDecl] -> Settings Idris
44−proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings
45+proverSettings e = setComplete (proverCompletion (assumptionNames e)) defaultSettings
47+assumptionNames :: ElabState [PDecl] -> [String]
45− where assumptionNames = case envAtFocus (proof e) of
49+ = case envAtFocus (proof e) of
46− OK env -> names env
50+ OK env -> names env
47− names [] = []
51+ where names [] = []
48− names ((MN _ _, _) : bs) = names bs
52+ names ((MN _ _, _) : bs) = names bs
49− names ((n, _) : bs) = show n : names bs
53+ names ((n, _) : bs) = show n : names bs
51prove :: Context -> Bool -> Name -> Type -> Idris ()
55prove :: Context -> Bool -> Name -> Type -> Idris ()
52prove ctxt lit n ty
56prove ctxt lit n ty
@@ -124,6 +128,21 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
124lifte st e = do (v, _) <- elabStep st e
128lifte st e = do (v, _) <- elabStep st e
131+receiveInput :: ElabState [PDecl] -> Idris (Maybe String)
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
143+ Just (Interpret cmd) -> return (Just cmd)
144+ Nothing -> return Nothing
127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
146ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128ploop d prompt prf e h
147ploop d prompt prf e h
129 = do i <- getIState
148 = do i <- getIState
@@ -138,36 +157,38 @@ ploop d prompt prf e h
138 l <- getInputLine (prompt ++ "> ")
157 l <- getInputLine (prompt ++ "> ")
139 h' <- getHistory
158 h' <- getHistory
140 return (l, Just h')
159 return (l, Just h')
141− IdeSlave n -> -- waitforinput
160+ IdeSlave n ->
142 do isetPrompt prompt
161 do isetPrompt prompt
143− return (Just "trivial", h)
163+ return (i, h)
144 (cmd, step) <- case x of
164 (cmd, step) <- case x of
145− Nothing -> fail "Abandoned"
165+ Nothing -> do iFail ""; fail "Abandoned"
146 Just input -> do return (parseTac i input, input)
166 Just input -> do return (parseTac i input, input)
147 case cmd of
167 case cmd of
148− Right Abandon -> fail "Abandoned"
168+ Right Abandon -> do iFail ""; fail "Abandoned"
149 _ -> return ()
169 _ -> return ()
150 (d, st, done, prf') <- idrisCatch
170 (d, st, done, prf') <- idrisCatch
151 (case cmd of
171 (case cmd of
152− Left err -> do iputStrLn (show err)
172+ Left err -> do iFail (show err)
153 return (False, e, False, prf)
173 return (False, e, False, prf)
155− do (_, st) <- elabStep e loadState
174+ Right Undo -> do (_, st) <- elabStep e loadState
156− return (True, st, False, init prf)
176+ return (True, st, False, init prf)
157− Right ProofState ->
177+ Right ProofState -> do iResult ""
158− return (True, e, False, prf)
178+ return (True, e, False, prf)
160− do tm <- lifte e get_term
179+ Right ProofTerm -> do tm <- lifte e get_term
161− iputStrLn $ "TT: " ++ show tm ++ "\n"
180+ iResult $ "TT: " ++ show tm ++ "\n"
162− return (False, e, False, prf)
181+ return (False, e, False, prf)
163 Right Qed -> do hs <- lifte e get_holes
182 Right Qed -> do hs <- lifte e get_holes
164 when (not (null hs)) $ fail "Incomplete proof"
183 when (not (null hs)) $ fail "Incomplete proof"
184+ iResult "Proof completed!"
165 return (False, e, True, prf)
185 return (False, e, True, prf)
166 Right tac -> do (_, e) <- elabStep e saveState
186 Right tac -> do (_, e) <- elabStep e saveState
167 (_, st) <- elabStep e (runTac True i tac)
187 (_, st) <- elabStep e (runTac True i tac)
168−-- trace (show (problems (proof st))) $
188+-- trace (show (problems (proof st))) $
169 return (True, st, False, prf ++ [step]))
190 return (True, st, False, prf ++ [step]))
170− (\err -> do iputStrLn (show err)
191+ (\err -> do iFail (show err)
171 return (False, e, False, prf))
192 return (False, e, False, prf))
172 if done then do (tm, _) <- elabStep st get_term
193 if done then do (tm, _) <- elabStep st get_term
173 return (tm, prf')
194 return (tm, prf')