git.iko.soy/Idris-dev
on master help sign in
Merge pull request #312 from hannesm/ideslave
f608369Edwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -90,7 +90,7 @@ Executable idris
90 Core.CaseTree, Core.Constraints,
90 Core.CaseTree, Core.Constraints,
91
91
92 Idris.AbsSyntax, Idris.AbsSyntaxTree,
92 Idris.AbsSyntax, Idris.AbsSyntaxTree,
93− Idris.Parser, Idris.Help, Idris.REPL,
93+ Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,
94 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
94 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
95 Idris.Delaborate, Idris.Primitives, Idris.Imports,
95 Idris.Delaborate, Idris.Primitives, Idris.Imports,
96 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
96 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
src/Idris/AbsSyntax.hs+42−2
@@ -8,6 +8,7 @@ import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
9import Core.Typecheck
10import Idris.AbsSyntaxTree
10import Idris.AbsSyntaxTree
11+import Idris.IdeSlave
11import IRTS.CodegenCommon
12import IRTS.CodegenCommon
12import Util.DynamicLinker
13import Util.DynamicLinker
13
14
@@ -26,6 +27,8 @@ import Debug.Trace
26import Util.Pretty
27import Util.Pretty
27import Util.System
28import Util.System
28
29
30+import Text.Printf (printf)
31+
29getContext :: Idris Context
32getContext :: Idris Context
30getContext = do i <- getIState; return (tt_ctxt i)
33getContext = do i <- getIState; return (tt_ctxt i)
31
34
@@ -242,11 +245,43 @@ solveDeferred :: Name -> Idris ()
242solveDeferred n = do i <- getIState
245solveDeferred n = do i <- getIState
243 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
246 putIState $ i { idris_metavars = idris_metavars i \\ [n] }
244
247
248+iResult :: String -> Idris ()
249+iResult s = do i <- getIState
250+ case idris_outputmode i of
251+ RawOutput -> case s of
252+ "" -> return ()
253+ s -> liftIO $ putStrLn s
254+ IdeSlave n ->
255+ let good = List [SymbolAtom "ok", toSExp s] in
256+ liftIO $ putStrLn $ convSExp "return" good n
257+
258+iFail :: String -> Idris ()
259+iFail s = do i <- getIState
260+ case idris_outputmode i of
261+ RawOutput -> case s of
262+ "" -> return ()
263+ s -> liftIO $ putStrLn s
264+ IdeSlave n ->
265+ let good = List [SymbolAtom "error", toSExp s] in
266+ liftIO $ putStrLn $ convSExp "return" good n
267+
245iputStrLn :: String -> Idris ()
268iputStrLn :: String -> Idris ()
269+iputStrLn s = do i <- getIState
270+ case idris_outputmode i of
271+ RawOutput -> liftIO $ putStrLn s
272+ IdeSlave n ->
273+ case span (/=':') s of
274+ (fn, ':':rest) -> case span isDigit rest of
275+ ([], ':':msg) -> iWarn (FC fn 0) msg
276+ ([], msg) -> iWarn (FC fn 0) msg
277+ (num, ':':msg) -> iWarn (FC fn (read num)) msg
246−iputStrLn = liftIO . putStrLn
278+ _ -> liftIO $ putStrLn $ convSExp "write-string" s n
247
279
248iWarn :: FC -> String -> Idris ()
280iWarn :: FC -> String -> Idris ()
281+iWarn fc err = do i <- getIState
282+ case idris_outputmode i of
249−iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)
283+ RawOutput -> liftIO $ putStrLn (show fc ++ ":" ++ err)
284+ IdeSlave n -> liftIO $ putStrLn $ convSExp "warning" (fc_fname fc, fc_line fc, err) n
250
285
251setLogLevel :: Int -> Idris ()
286setLogLevel :: Int -> Idris ()
252setLogLevel l = do i <- getIState
287setLogLevel l = do i <- getIState
@@ -323,6 +358,11 @@ outputTy :: Idris OutputType
323outputTy = do i <- getIState
358outputTy = do i <- getIState
324 return $ opt_outputTy $ idris_options i
359 return $ opt_outputTy $ idris_options i
325
360
361+setIdeSlave :: Bool -> Idris ()
362+setIdeSlave True = do i <- getIState
363+ putIState $ i { idris_outputmode = (IdeSlave 0) }
364+setIdeSlave False = return ()
365+
326verbose :: Idris Bool
366verbose :: Idris Bool
327verbose = do i <- getIState
367verbose = do i <- getIState
328 return (opt_verbose (idris_options i))
368 return (opt_verbose (idris_options i))
src/Idris/AbsSyntaxTree.hs+8−2
@@ -45,6 +45,9 @@ defaultOpts = IOption 0 False False True False False True True False ViaC Execut
45
45
46data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)
46data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)
47
47
48+-- | The output mode in use
49+data OutputMode = RawOutput | IdeSlave Integer deriving Show
50+
48-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
51-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
49-- without typechecking).
52-- without typechecking).
50-- This will include all the functions and data declarations, plus fixity declarations
53-- This will include all the functions and data declarations, plus fixity declarations
@@ -92,7 +95,8 @@ data IState = IState {
92 ibc_write :: [IBCWrite],
95 ibc_write :: [IBCWrite],
93 compiled_so :: Maybe String,
96 compiled_so :: Maybe String,
94 idris_dynamic_libs :: [DynamicLib],
97 idris_dynamic_libs :: [DynamicLib],
95− idris_language_extensions :: [LanguageExt]
98+ idris_language_extensions :: [LanguageExt],
99+ idris_outputmode :: OutputMode
96 }
100 }
97
101
98data SizeChange = Smaller | Same | Bigger | Unknown
102data SizeChange = Smaller | Same | Bigger | Unknown
@@ -144,10 +148,11 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
144 emptyContext emptyContext emptyContext emptyContext
148 emptyContext emptyContext emptyContext emptyContext
145 emptyContext emptyContext emptyContext emptyContext
149 emptyContext emptyContext emptyContext emptyContext
146 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
150 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
147− [] Nothing Nothing [] [] [] Hidden False [] Nothing [] []
151+ [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
148
152
149-- | The monad for the main REPL - reading and processing files and updating
153-- | The monad for the main REPL - reading and processing files and updating
150-- global state (hence the IO inner monad).
154-- global state (hence the IO inner monad).
155+--type Idris = WriterT [Either String (IO ())] (State IState a))
151type Idris = StateT IState IO
156type Idris = StateT IState IO
152
157
153-- Commands in the REPL
158-- Commands in the REPL
@@ -202,6 +207,7 @@ data Opt = Filename String
202 | Ver
207 | Ver
203 | Usage
208 | Usage
204 | Quiet
209 | Quiet
210+ | Ideslave
205 | ShowLibs
211 | ShowLibs
206 | ShowLibdir
212 | ShowLibdir
207 | ShowIncs
213 | ShowIncs
src/Idris/IdeSlave.hsnew file+126
@@ -0,0 +1,126 @@
1+{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}
2+
3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..)) where
4+
5+import Text.Printf
6+import Numeric
7+import Data.List
8+-- import qualified Data.Text as T
9+import Text.Parsec
10+
11+data SExp = List [SExp]
12+ | StringAtom String
13+ | BoolAtom Bool
14+ | IntegerAtom Integer
15+ | SymbolAtom String
16+ deriving ( Eq, Show )
17+
18+sExpToString :: SExp -> String
19+sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""
20+sExpToString (BoolAtom True) = ":True"
21+sExpToString (BoolAtom False) = ":False"
22+sExpToString (IntegerAtom i) = printf "%d" i
23+sExpToString (SymbolAtom s) = ":" ++ s
24+sExpToString (List l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"
25+
26+class SExpable a where
27+ toSExp :: a -> SExp
28+
29+instance SExpable SExp where
30+ toSExp a = a
31+
32+instance SExpable () where
33+ toSExp a = List [ StringAtom "Unit" ]
34+
35+instance SExpable Bool where
36+ toSExp True = BoolAtom True
37+ toSExp False = BoolAtom False
38+
39+instance SExpable String where
40+ toSExp s = StringAtom s
41+
42+instance SExpable Integer where
43+ toSExp n = IntegerAtom n
44+
45+instance SExpable Int where
46+ toSExp n = IntegerAtom (toInteger n)
47+
48+instance (SExpable a) => SExpable (Maybe a) where
49+ toSExp Nothing = List [SymbolAtom "Nothing"]
50+ toSExp (Just a) = List [SymbolAtom "Just", toSExp a]
51+
52+instance (SExpable a) => SExpable [a] where
53+ toSExp l = List (map toSExp l)
54+
55+instance (SExpable a, SExpable b) => SExpable (a, b) where
56+ toSExp (l, r) = List [toSExp l, toSExp r]
57+
58+instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
59+ toSExp (l, m, n) = List [toSExp l, toSExp m, toSExp n]
60+
61+escape :: String -> String
62+escape = concatMap escapeChar
63+ where
64+ escapeChar '\\' = "\\\\"
65+ escapeChar '"' = "\\\""
66+ escapeChar c = [c]
67+
68+pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
69+ return (List xs)
70+ <|> atom
71+
72+atom = do char ':'; x <- atomC; return x
73+ <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
74+ <|> do ints <- many1 digit
75+ case readDec ints of
76+ ((num, ""):_) -> return (IntegerAtom (toInteger num))
77+ _ -> return (StringAtom ints)
78+
79+atomC = do string "True"; return (BoolAtom True)
80+ <|> do string "False"; return (BoolAtom False)
81+ <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
82+
83+quotedChar = try (string "\\\\" >> return '\\')
84+ <|> try (string "\\\"" >> return '"')
85+ <|> noneOf "\""
86+
87+parseSExp :: String -> Either ParseError SExp
88+parseSExp = parse pSExp "(unknown)"
89+
90+data IdeSlaveCommand = REPLCompletions String
91+ | Interpret String
92+ | LoadFile String
93+ deriving Show
94+
95+sexpToCommand :: SExp -> Maybe IdeSlaveCommand
96+sexpToCommand (List (x:[])) = sexpToCommand x
97+sexpToCommand (List [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
98+sexpToCommand (List [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
99+sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
100+sexpToCommand _ = Nothing
101+
102+parseMessage :: String -> (SExp, Integer)
103+parseMessage x = case receiveString x of
104+ (List [cmd, (IntegerAtom id)]) ->
105+ (cmd, id)
106+
107+receiveString :: String -> SExp
108+receiveString x =
109+ case readHex (take 6 x) of
110+ ((num, ""):_) ->
111+ let msg = drop 6 x in
112+ if (length msg) /= (num - 1)
113+ then error "bad input length"
114+ else (case parseSExp msg of
115+ Left _ -> error "parse failure"
116+ Right r -> r)
117+ _ -> error "readHex failed"
118+
119+convSExp :: SExpable a => String -> a -> Integer -> String
120+convSExp pre s id =
121+ let sex = List [SymbolAtom pre, toSExp s, IntegerAtom id] in
122+ let str = sExpToString sex in
123+ (getHexLength str) ++ str
124+
125+getHexLength :: String -> String
126+getHexLength s = printf "%06x" (1 + (length s))
src/Idris/REPL.hs+159−54
@@ -18,6 +18,7 @@ import Idris.UnusedArgs
18import Idris.Docs
18import Idris.Docs
19import Idris.Help
19import Idris.Help
20import Idris.Completion
20import Idris.Completion
21+import Idris.IdeSlave
21
22
22import Paths_idris
23import Paths_idris
23import Util.System
24import Util.System
@@ -80,6 +81,104 @@ repl orig mods
80 ctrlC e = do lift $ iputStrLn (show e)
81 ctrlC e = do lift $ iputStrLn (show e)
81 repl orig mods
82 repl orig mods
82
83
84+-- | Run the IdeSlave
85+ideslaveStart :: IState -> [FilePath] -> Idris ()
86+ideslaveStart orig mods
87+ = do i <- getIState
88+ case idris_outputmode i of
89+ IdeSlave n ->
90+ when (mods /= []) (do liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt mods) n)
91+ ideslave orig mods
92+
93+
94+ideslave :: IState -> [FilePath] -> Idris ()
95+ideslave orig mods
96+ = do idrisCatch
97+ (do l <- liftIO $ getLine
98+ let (sexp, id) = parseMessage l
99+ i <- getIState
100+ putIState $ i { idris_outputmode = (IdeSlave id) }
101+ case sexpToCommand sexp of
102+ Just (Interpret cmd) ->
103+ do let fn = case mods of
104+ (f:_) -> f
105+ _ -> ""
106+ case parseCmd i cmd of
107+ Left err -> iFail $ show err
108+ Right cmd -> idrisCatch
109+ (do ideslaveProcess fn cmd)
110+ (\e -> do iFail $ show e)
111+ Just (REPLCompletions str) ->
112+ do (unused, compls) <- replCompletion (reverse str, "")
113+ let good = List [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
114+ liftIO $ putStrLn $ convSExp "return" good id
115+ Just (LoadFile filename) ->
116+ do clearErr
117+ putIState (orig { idris_options = idris_options i,
118+ idris_outputmode = (IdeSlave id) })
119+ loadModule filename
120+ iucheck
121+ liftIO $ putStrLn $ convSExp "set-prompt" (mkPrompt [filename]) id
122+ -- report success! or failure!
123+ ideslave orig [filename]
124+ Nothing -> do iFail "did not understand")
125+ (\e -> do iFail $ show e)
126+ ideslave orig mods
127+
128+ideslaveProcess :: FilePath -> Command -> Idris ()
129+ideslaveProcess fn Help = process fn Help
130+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)
131+ iResult "changed directory to"
132+ideslaveProcess fn (Eval t) = process fn (Eval t)
133+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)
134+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))
135+ideslaveProcess fn (Check t) = process fn (Check t)
136+ideslaveProcess fn (DocStr n) = process fn (DocStr n)
137+ideslaveProcess fn Universes = process fn Universes
138+ideslaveProcess fn (Defn n) = do process fn (Defn n)
139+ iResult ""
140+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)
141+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)
142+ iResult ""
143+ideslaveProcess fn (Info n) = process fn (Info n)
144+ideslaveProcess fn (Search t) = process fn (Search t)
145+ideslaveProcess fn (Spec t) = process fn (Spec t)
146+-- RmProof and AddProof not supported!
147+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
148+ideslaveProcess fn (Prove n') = process fn (Prove n')
149+ideslaveProcess fn (HNF t) = process fn (HNF t)
150+--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
151+
152+--that most likely does not work, since we need to wrap
153+--input/output of the executed binary...
154+ideslaveProcess fn Execute = do process fn Execute
155+ iResult ""
156+ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)
157+ iResult ""
158+ideslaveProcess fn (Compile target f) = do process fn (Compile target f)
159+ iResult ""
160+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)
161+ iResult ""
162+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)
163+ideslaveProcess fn (Missing n) = process fn (Missing n)
164+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)
165+ iResult ""
166+ideslaveProcess fn ListDynamic = do process fn ListDynamic
167+ iResult ""
168+ideslaveProcess fn Metavars = process fn Metavars
169+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)
170+ iResult ""
171+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)
172+ iResult ""
173+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)
174+ iResult ""
175+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)
176+ iResult ""
177+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)
178+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)
179+ideslaveProcess fn _ = iFail "command not recognized or not supported"
180+
181+
83-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
182-- | The prompt consists of the currently loaded modules, or "Idris" if there are none
84mkPrompt [] = "Idris"
183mkPrompt [] = "Idris"
85mkPrompt [x] = "*" ++ dropExtension x
184mkPrompt [x] = "*" ++ dropExtension x
@@ -173,25 +272,25 @@ proofs orig
173
272
174insertScript :: String -> [String] -> [String]
273insertScript :: String -> [String] -> [String]
175insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
274insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf]
176−insertScript prf (p@"---------- Proofs ----------" : "" : xs)
275+insertScript prf (p@"---------- Proofs ----------" : "" : xs)
177 = p : "" : prf : xs
276 = p : "" : prf : xs
178insertScript prf (x : xs) = x : insertScript prf xs
277insertScript prf (x : xs) = x : insertScript prf xs
179
278
180process :: FilePath -> Command -> Idris ()
279process :: FilePath -> Command -> Idris ()
181−process fn Help = iputStrLn displayHelp
280+process fn Help = iResult displayHelp
182process fn (ChangeDirectory f)
281process fn (ChangeDirectory f)
183 = do liftIO $ setCurrentDirectory f
282 = do liftIO $ setCurrentDirectory f
184 return ()
283 return ()
185−process fn (Eval t)
284+process fn (Eval t)
186 = do (tm, ty) <- elabVal toplevel False t
285 = do (tm, ty) <- elabVal toplevel False t
187 ctxt <- getContext
286 ctxt <- getContext
188− ist <- getIState
287+ ist <- getIState
189 let tm' = normaliseAll ctxt [] tm
288 let tm' = normaliseAll ctxt [] tm
190 let ty' = normaliseAll ctxt [] ty
289 let ty' = normaliseAll ctxt [] ty
191 logLvl 3 $ "Raw: " ++ show (tm', ty')
290 logLvl 3 $ "Raw: " ++ show (tm', ty')
192 imp <- impShow
291 imp <- impShow
193− iputStrLn (showImp imp (delab ist tm') ++ " : " ++
292+ iResult (showImp imp (delab ist tm') ++ " : " ++
194− showImp imp (delab ist ty'))
293+ showImp imp (delab ist ty'))
195process fn (ExecVal t)
294process fn (ExecVal t)
196 = do ctxt <- getContext
295 = do ctxt <- getContext
197 ist <- getIState
296 ist <- getIState
@@ -200,30 +299,31 @@ process fn (ExecVal t)
200 let ty' = normaliseAll ctxt [] ty
299 let ty' = normaliseAll ctxt [] ty
201 res <- execute tm
300 res <- execute tm
202 imp <- impShow
301 imp <- impShow
203− iputStrLn (showImp imp (delab ist res) ++ " : " ++
302+ iResult (showImp imp (delab ist res) ++ " : " ++
204− showImp imp (delab ist ty'))
303+ showImp imp (delab ist ty'))
205− return ()
206process fn (Check (PRef _ n))
304process fn (Check (PRef _ n))
207 = do ctxt <- getContext
305 = do ctxt <- getContext
208 ist <- getIState
306 ist <- getIState
209 imp <- impShow
307 imp <- impShow
210 case lookupNames n ctxt of
308 case lookupNames n ctxt of
211− ts@(_:_) -> mapM_ (\n -> iputStrLn $ show n ++ " : " ++
309+ ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++
212− showImp imp (delabTy ist n)) ts
310+ showImp imp (delabTy ist n)) ts
311+ iResult ""
213− [] -> iputStrLn $ "No such variable " ++ show n
312+ [] -> iFail $ "No such variable " ++ show n
214process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
313process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
215 ctxt <- getContext
314 ctxt <- getContext
216− ist <- getIState
315+ ist <- getIState
217 imp <- impShow
316 imp <- impShow
218 let ty' = normaliseC ctxt [] ty
317 let ty' = normaliseC ctxt [] ty
219− iputStrLn (showImp imp (delab ist tm) ++ " : " ++
318+ iResult (showImp imp (delab ist tm) ++ " : " ++
220− showImp imp (delab ist ty))
319+ showImp imp (delab ist ty))
221
320
222process fn (DocStr n) = do i <- getIState
321process fn (DocStr n) = do i <- getIState
223 case lookupCtxtName n (idris_docstrings i) of
322 case lookupCtxtName n (idris_docstrings i) of
224− [] -> iputStrLn $ "No documentation for " ++ show n
323+ [] -> iFail $ "No documentation for " ++ show n
225− ns -> mapM_ showDoc ns
324+ ns -> do mapM_ showDoc ns
325+ iResult ""
226− where showDoc (n, d)
326+ where showDoc (n, d)
227 = do doc <- getDocs n
327 = do doc <- getDocs n
228 iputStrLn $ show doc
328 iputStrLn $ show doc
229process fn Universes = do i <- getIState
329process fn Universes = do i <- getIState
@@ -233,8 +333,8 @@ process fn Universes = do i <- getIState
233 let n = length cs
333 let n = length cs
234 iputStrLn $ "(" ++ show n ++ " constraints)"
334 iputStrLn $ "(" ++ show n ++ " constraints)"
235 case ucheck cs of
335 case ucheck cs of
236− Error e -> iputStrLn $ pshow i e
336+ Error e -> iFail $ pshow i e
237− OK _ -> iputStrLn "Universes OK"
337+ OK _ -> iResult "Universes OK"
238process fn (Defn n) = do i <- getIState
338process fn (Defn n) = do i <- getIState
239 iputStrLn "Compiled patterns:\n"
339 iputStrLn "Compiled patterns:\n"
240 liftIO $ print (lookupDef n (tt_ctxt i))
340 liftIO $ print (lookupDef n (tt_ctxt i))
@@ -245,15 +345,15 @@ process fn (Defn n) = do i <- getIState
245 case lookupTotal n (tt_ctxt i) of
345 case lookupTotal n (tt_ctxt i) of
246 [t] -> iputStrLn (showTotal t i)
346 [t] -> iputStrLn (showTotal t i)
247 _ -> return ()
347 _ -> return ()
248− where printCase i (_, lhs, rhs)
348+ where printCase i (_, lhs, rhs)
249− = do liftIO $ putStr $ showImp True (delab i lhs)
349+ = do iputStrLn (showImp True (delab i lhs) ++ " = " ++
250− liftIO $ putStr " = "
251− liftIO $ putStrLn $ showImp True (delab i rhs)
350+ showImp True (delab i rhs))
252process fn (TotCheck n) = do i <- getIState
351process fn (TotCheck n) = do i <- getIState
253 case lookupTotal n (tt_ctxt i) of
352 case lookupTotal n (tt_ctxt i) of
254− [t] -> iputStrLn (showTotal t i)
353+ [t] -> iResult (showTotal t i)
354+ _ -> do iFail ""
255− _ -> return ()
355+ return ()
256−process fn (DebugInfo n)
356+process fn (DebugInfo n)
257 = do i <- getIState
357 = do i <- getIState
258 let oi = lookupCtxtName n (idris_optimisation i)
358 let oi = lookupCtxtName n (idris_optimisation i)
259 when (not (null oi)) $ iputStrLn (show oi)
359 when (not (null oi)) $ iputStrLn (show oi)
@@ -275,13 +375,13 @@ process fn (DebugInfo n)
275process fn (Info n) = do i <- getIState
375process fn (Info n) = do i <- getIState
276 case lookupCtxt n (idris_classes i) of
376 case lookupCtxt n (idris_classes i) of
277 [c] -> classInfo c
377 [c] -> classInfo c
278− _ -> iputStrLn "Not a class"
378+ _ -> iFail "Not a class"
279−process fn (Search t) = iputStrLn "Not implemented"
379+process fn (Search t) = iFail "Not implemented"
280process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
380process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
281 ctxt <- getContext
381 ctxt <- getContext
282 ist <- getIState
382 ist <- getIState
283 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
383 let tm' = simplify ctxt True [] {- (idris_statics ist) -} tm
284− iputStrLn (show (delab ist tm'))
384+ iResult (show (delab ist tm'))
285
385
286process fn (RmProof n')
386process fn (RmProof n')
287 = do i <- getIState
387 = do i <- getIState
@@ -333,8 +433,8 @@ process fn (ShowProof n')
333 n <- resolveProof n'
433 n <- resolveProof n'
334 let proofs = proof_list i
434 let proofs = proof_list i
335 case lookup n proofs of
435 case lookup n proofs of
336− Nothing -> iputStrLn "No proof to show"
436+ Nothing -> iFail "No proof to show"
337− Just p -> iputStrLn $ showProof False n p
437+ Just p -> iResult $ showProof False n p
338
438
339process fn (Prove n')
439process fn (Prove n')
340 = do ctxt <- getContext
440 = do ctxt <- getContext
@@ -354,13 +454,13 @@ process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t
354 ctxt <- getContext
454 ctxt <- getContext
355 ist <- getIState
455 ist <- getIState
356 let tm' = hnf ctxt [] tm
456 let tm' = hnf ctxt [] tm
357− iputStrLn (show (delab ist tm'))
457+ iResult (show (delab ist tm'))
358process fn TTShell = do ist <- getIState
458process fn TTShell = do ist <- getIState
359 let shst = initState (tt_ctxt ist)
459 let shst = initState (tt_ctxt ist)
360 runShell shst
460 runShell shst
361 return ()
461 return ()
362−process fn Execute = do (m, _) <- elabVal toplevel False
462+process fn Execute = do (m, _) <- elabVal toplevel False
363− (PApp fc
463+ (PApp fc
364 (PRef fc (UN "run__IO"))
464 (PRef fc (UN "run__IO"))
365 [pexp $ PRef fc (NS (UN "main") ["Main"])])
465 [pexp $ PRef fc (NS (UN "main") ["Main"])])
366-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
466-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))
@@ -370,37 +470,37 @@ process fn Execute = do (m, _) <- elabVal toplevel False
370 compile t tmpn m
470 compile t tmpn m
371 liftIO $ system tmpn
471 liftIO $ system tmpn
372 return ()
472 return ()
373− where fc = FC "main" 0
473+ where fc = FC "main" 0
374−process fn (NewCompile f)
474+process fn (NewCompile f)
375 = do (m, _) <- elabVal toplevel False
475 = do (m, _) <- elabVal toplevel False
376 (PApp fc (PRef fc (UN "run__IO"))
476 (PApp fc (PRef fc (UN "run__IO"))
377 [pexp $ PRef fc (NS (UN "main") ["Main"])])
477 [pexp $ PRef fc (NS (UN "main") ["Main"])])
378 compileEpic f m
478 compileEpic f m
379− where fc = FC "main" 0
479+ where fc = FC "main" 0
380−process fn (Compile target f)
480+process fn (Compile target f)
381 = do (m, _) <- elabVal toplevel False
481 = do (m, _) <- elabVal toplevel False
382 (PApp fc (PRef fc (UN "run__IO"))
482 (PApp fc (PRef fc (UN "run__IO"))
383 [pexp $ PRef fc (NS (UN "main") ["Main"])])
483 [pexp $ PRef fc (NS (UN "main") ["Main"])])
384 compile target f m
484 compile target f m
385− where fc = FC "main" 0
485+ where fc = FC "main" 0
386−process fn (LogLvl i) = setLogLevel i
486+process fn (LogLvl i) = setLogLevel i
387-- Elaborate as if LHS of a pattern (debug command)
487-- Elaborate as if LHS of a pattern (debug command)
388−process fn (Pattelab t)
488+process fn (Pattelab t)
389 = do (tm, ty) <- elabVal toplevel True t
489 = do (tm, ty) <- elabVal toplevel True t
390− iputStrLn $ show tm ++ "\n\n : " ++ show ty
490+ iResult $ show tm ++ "\n\n : " ++ show ty
391
491
392−process fn (Missing n)
492+process fn (Missing n)
393 = do i <- getIState
493 = do i <- getIState
394 case lookupCtxt n (idris_patdefs i) of
494 case lookupCtxt n (idris_patdefs i) of
395 [] -> return ()
495 [] -> return ()
396− [(_, tms)] ->
496+ [(_, tms)] ->
397− iputStrLn (showSep "\n" (map (showImp True) tms))
497+ iResult (showSep "\n" (map (showImp True) tms))
398− _ -> iputStrLn $ "Ambiguous name"
498+ _ -> iFail $ "Ambiguous name"
399process fn (DynamicLink l) = do i <- getIState
499process fn (DynamicLink l) = do i <- getIState
400 let lib = trim l
500 let lib = trim l
401 handle <- lift $ tryLoadLib lib
501 handle <- lift $ tryLoadLib lib
402 case handle of
502 case handle of
403− Nothing -> iputStrLn $ "Could not load dynamic lib \"" ++ l ++ "\""
503+ Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""
404 Just x -> do let libs = idris_dynamic_libs i
504 Just x -> do let libs = idris_dynamic_libs i
405 putIState $ i { idris_dynamic_libs = x:libs }
505 putIState $ i { idris_dynamic_libs = x:libs }
406 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
506 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
@@ -413,8 +513,8 @@ process fn Metavars
413 = do ist <- getIState
513 = do ist <- getIState
414 let mvs = idris_metavars ist \\ primDefs
514 let mvs = idris_metavars ist \\ primDefs
415 case mvs of
515 case mvs of
416− [] -> iputStrLn "No global metavariables to solve"
516+ [] -> iFail "No global metavariables to solve"
417− _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
517+ _ -> iResult $ "Global metavariables:\n\t" ++ show mvs
418process fn NOP = return ()
518process fn NOP = return ()
419
519
420process fn (SetOpt ErrContext) = setErrContext True
520process fn (SetOpt ErrContext) = setErrContext True
@@ -422,8 +522,8 @@ process fn (UnsetOpt ErrContext) = setErrContext False
422process fn (SetOpt ShowImpl) = setImpShow True
522process fn (SetOpt ShowImpl) = setImpShow True
423process fn (UnsetOpt ShowImpl) = setImpShow False
523process fn (UnsetOpt ShowImpl) = setImpShow False
424
524
425−process fn (SetOpt _) = iputStrLn "Not a valid option"
525+process fn (SetOpt _) = iFail "Not a valid option"
426−process fn (UnsetOpt _) = iputStrLn "Not a valid option"
526+process fn (UnsetOpt _) = iFail "Not a valid option"
427
527
428
528
429classInfo :: ClassInfo -> Idris ()
529classInfo :: ClassInfo -> Idris ()
@@ -432,6 +532,7 @@ classInfo ci = do iputStrLn "Methods:\n"
432 iputStrLn ""
532 iputStrLn ""
433 iputStrLn "Instances:\n"
533 iputStrLn "Instances:\n"
434 mapM_ dumpInstance (class_instances ci)
534 mapM_ dumpInstance (class_instances ci)
535+ iResult ""
435
536
436dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
537dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()
437dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
538dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t
@@ -471,6 +572,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function
471parseArgs :: [String] -> [Opt]
572parseArgs :: [String] -> [Opt]
472parseArgs [] = []
573parseArgs [] = []
473parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
574parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)
575+parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
474parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
576parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
475parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
577parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
476parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
578parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
@@ -524,6 +626,7 @@ idrisMain :: [Opt] -> Idris ()
524idrisMain opts =
626idrisMain opts =
525 do let inputs = opt getFile opts
627 do let inputs = opt getFile opts
526 let quiet = Quiet `elem` opts
628 let quiet = Quiet `elem` opts
629+ let idesl = Ideslave `elem` opts
527 let runrepl = not (NoREPL `elem` opts)
630 let runrepl = not (NoREPL `elem` opts)
528 let output = opt getOutput opts
631 let output = opt getOutput opts
529 let newoutput = opt getNewOutput opts
632 let newoutput = opt getNewOutput opts
@@ -543,6 +646,7 @@ idrisMain opts =
543 mapM_ addLangExt (opt getLanguageExt opts)
646 mapM_ addLangExt (opt getLanguageExt opts)
544 setREPL runrepl
647 setREPL runrepl
545 setQuiet quiet
648 setQuiet quiet
649+ setIdeSlave idesl
546 setVerbose runrepl
650 setVerbose runrepl
547 setCmdLine opts
651 setCmdLine opts
548 setOutputTy outty
652 setOutputTy outty
@@ -567,7 +671,7 @@ idrisMain opts =
567 elabPrims
671 elabPrims
568 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
672 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"
569 return ()
673 return ()
570− when (runrepl && not quiet) $ iputStrLn banner
674+ when (runrepl && not quiet && not idesl) $ iputStrLn banner
571 ist <- getIState
675 ist <- getIState
572 mods <- mapM loadModule inputs
676 mods <- mapM loadModule inputs
573 ok <- noErrors
677 ok <- noErrors
@@ -577,7 +681,8 @@ idrisMain opts =
577 when ok $ case newoutput of
681 when ok $ case newoutput of
578 [] -> return ()
682 [] -> return ()
579 (o:_) -> process "" (NewCompile o)
683 (o:_) -> process "" (NewCompile o)
580− when runrepl $ runInputT replSettings $ repl ist inputs
684+ when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs
685+ when (idesl) $ ideslaveStart ist inputs
581 ok <- noErrors
686 ok <- noErrors
582 when (not ok) $ liftIO (exitWith (ExitFailure 1))
687 when (not ok) $ liftIO (exitWith (ExitFailure 1))
583 where
688 where