4118b79 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

implement outputmode in IState, which either prints it raw or sexpressions (for ideslave support)

4118b79Hannes Mehnert13 years ago

src/Idris/AbsSyntax.hs+14−1

compare with master

unifiedsplit

@@ -8,6 +8,7 @@ import Core.Evaluate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11+import Idris.IdeSlave

11import IRTS.CodegenCommon

12import IRTS.CodegenCommon

12import Util.DynamicLinker

13import Util.DynamicLinker

@@ -26,6 +27,8 @@ import Debug.Trace

26import Util.Pretty

27import Util.Pretty

27import Util.System

28import Util.System

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)

@@ -239,7 +242,17 @@ solveDeferred n = do i <- getIState

239 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

242 putIState $ i { idris_metavars = idris_metavars i \\ [n] }

240

243

241iputStrLn :: String -> Idris ()

244iputStrLn :: String -> Idris ()

245+iputStrLn s = do i <- getIState

246+ case idris_outputmode i of

242−iputStrLn = liftIO . putStrLn

247+ RawOutput -> liftIO $ putStrLn s

248+ IdeSlave n -> liftIO $ putStrLn (conv n (toSExp s))

249+ where conv id sexp

250+ = let sex = List [SymbolAtom "write-string", sexp, IntegerAtom id] in

251+ let str = sExpToString sex in

252+ (getHexLength str) ++ str

253+

254+getHexLength :: String -> String

255+getHexLength s = printf "%06x" (1 + (length s))

243

256

244iWarn :: FC -> String -> Idris ()

257iWarn :: FC -> String -> Idris ()

245iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)

258iWarn fc err = liftIO $ putStrLn (show fc ++ ":" ++ err)

src/Idris/AbsSyntaxTree.hs+6−3

@@ -46,6 +46,9 @@ defaultOpts = IOption 0 False False True False False True True False False ViaC

47data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)

49+-- | The output mode in use

50+data OutputMode = RawOutput | IdeSlave Integer deriving Show

51+

49-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

52-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

50-- without typechecking).

53-- without typechecking).

51-- This will include all the functions and data declarations, plus fixity declarations

54-- This will include all the functions and data declarations, plus fixity declarations

@@ -94,7 +97,7 @@ data IState = IState {

94 compiled_so :: Maybe String,

97 compiled_so :: Maybe String,

95 idris_dynamic_libs :: [DynamicLib],

98 idris_dynamic_libs :: [DynamicLib],

96 idris_language_extensions :: [LanguageExt],

99 idris_language_extensions :: [LanguageExt],

97− ideslave_counter :: Integer

100+ idris_outputmode :: OutputMode

98 }

101 }

102

100data SizeChange = Smaller | Same | Bigger | Unknown

103data SizeChange = Smaller | Same | Bigger | Unknown

@@ -146,7 +149,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

146 emptyContext emptyContext emptyContext emptyContext

149 emptyContext emptyContext emptyContext emptyContext

147 emptyContext emptyContext emptyContext emptyContext

150 emptyContext emptyContext emptyContext emptyContext

148 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

151 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

149− [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] 0

152+ [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

150

153

151-- | The monad for the main REPL - reading and processing files and updating

154-- | The monad for the main REPL - reading and processing files and updating

152-- global state (hence the IO inner monad).

155-- global state (hence the IO inner monad).

@@ -205,7 +208,7 @@ data Opt = Filename String

205 | Ver

208 | Ver

206 | Usage

209 | Usage

207 | Quiet

210 | Quiet

208− | IdeSlave

211+ | Ideslave

209 | ShowLibs

212 | ShowLibs

210 | ShowLibdir

213 | ShowLibdir

211 | ShowIncs

214 | ShowIncs

src/Idris/IdeSlave.hs+16−23

@@ -1,11 +1,6 @@

1{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

3−module Idris.IdeSlave(receiveMessage, sendMessage, IdeSlaveCommand(..), sexpToCommand, SExp(..)) where

3+module Idris.IdeSlave(receiveMessage, sendMessage, IdeSlaveCommand(..), sexpToCommand, toSExp, sExpToString, SExp(..)) where

4−

5−import Idris.AbsSyntaxTree

6−import Idris.AbsSyntax

7−

8−import Control.Monad.Trans ( liftIO, lift )

10import Text.Printf

5import Text.Printf

11import Numeric

6import Numeric

@@ -34,6 +29,9 @@ class SExpable a where

34instance SExpable SExp where

29instance SExpable SExp where

35 toSExp a = a

30 toSExp a = a

32+instance SExpable () where

33+ toSExp a = List [ StringAtom "Unit" ]

34+

37instance SExpable Bool where

35instance SExpable Bool where

38 toSExp True = BoolAtom True

36 toSExp True = BoolAtom True

39 toSExp False = BoolAtom False

37 toSExp False = BoolAtom False

@@ -97,14 +95,10 @@ sexpToCommand (List [SymbolAtom "repl-completions", StringAtom prefix]) = Just (

97sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

95sexpToCommand (List [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

98sexpToCommand _ = Nothing

96sexpToCommand _ = Nothing

100−receiveMessage :: Idris (SExp)

98+receiveMessage :: String -> (SExp, Integer)

101−receiveMessage = do x <- liftIO $ getLine

102− case receiveString x of

99+receiveMessage x = case receiveString x of

103− (List [cmd, (IntegerAtom id)]) ->

100+ (List [cmd, (IntegerAtom id)]) ->

104− do i <- getIState

101+ (cmd, id)

105− putIState $ (i { ideslave_counter = id } )

106− return cmd

107−

108

102

109receiveString :: String -> SExp

103receiveString :: String -> SExp

110receiveString x =

104receiveString x =

@@ -118,15 +112,14 @@ receiveString x =

118 Right r -> r)

112 Right r -> r)

119 _ -> error "readHex failed"

113 _ -> error "readHex failed"

120

114

121−sendMessage :: SExpable a => Either a a -> Idris ()

115+sendMessage :: SExpable a => Integer -> Either a a -> String

122−sendMessage s =

116+sendMessage id s =

123− do i <- getIState

124− let msg = case s of

117+ let sexp = case s of

125− Left err -> List [SymbolAtom "error", toSExp err]

118+ Left err -> List [SymbolAtom "error", toSExp err]

126− Right succ -> List [SymbolAtom "ok", toSExp succ]

119+ Right succ -> List [SymbolAtom "ok", toSExp succ]

127− liftIO $ putStrLn (conv (ideslave_counter i) msg)

120+ in conv id sexp

128− where conv id sexp =

121+ where conv id sexp =

129− let str = sExpToString (List [SymbolAtom "return", sexp, IntegerAtom id]) in (getHexLength str) ++ str

122+ let str = sExpToString (List [SymbolAtom "return", sexp, IntegerAtom id]) in (getHexLength str) ++ str

130

123

131getHexLength :: String -> String

124getHexLength :: String -> String

132getHexLength s = printf "%06x" (1 + (length s))

125getHexLength s = printf "%06x" (1 + (length s))

src/Idris/REPL.hs+13−10

@@ -85,7 +85,10 @@ repl orig mods

85ideslave :: IState -> [FilePath] -> Idris ()

86ideslave orig mods

87 = do idrisCatch

88+ (do l <- liftIO $ getLine

88− (do sexp <- receiveMessage

89+ let (sexp, id) = receiveMessage l

90+ i <- getIState

91+ putIState $ i { idris_outputmode = (IdeSlave id) }

89 case sexpToCommand sexp of

92 case sexpToCommand sexp of

90 Just (Interpret cmd) ->

93 Just (Interpret cmd) ->

91 do i <- getIState

94 do i <- getIState

@@ -93,19 +96,19 @@ ideslave orig mods

93 (f:_) -> f

96 (f:_) -> f

94 _ -> ""

97 _ -> ""

95 case parseCmd i cmd of

98 case parseCmd i cmd of

96− Left err -> do sendMessage (Left (show err))

99+ Left err -> do liftIO $ putStrLn $ sendMessage id (Left (show err))

97 Right cmd -> do idrisCatch

100 Right cmd -> do idrisCatch

98 (do xs <- process fn cmd

101 (do xs <- process fn cmd

99− sendMessage (Right (xs, "no output")))

102+ liftIO $ putStrLn $ sendMessage id (Right (xs, "no output")))

100− (\e -> do sendMessage (Left (show e)))

103+ (\e -> do liftIO $ putStrLn $ sendMessage id (Left (show e)))

101 Just (REPLCompletions str) ->

104 Just (REPLCompletions str) ->

102 do (unused, compls) <- replCompletion (reverse str, "")

105 do (unused, compls) <- replCompletion (reverse str, "")

103− sendMessage (Right (map replacement compls, reverse unused))

106+ liftIO $ putStrLn $ sendMessage id (Right (map replacement compls, reverse unused))

104 Just (LoadFile filename) -> do clearErr

107 Just (LoadFile filename) -> do clearErr

105 mod <- loadModule filename

108 mod <- loadModule filename

106− sendMessage (Right (SymbolAtom "good"))

109+ liftIO $ putStrLn $ sendMessage id (Right (SymbolAtom "good"))

107− Nothing -> do sendMessage (Left "did not understand"))

110+ Nothing -> do liftIO $ putStrLn $ sendMessage id (Left "did not understand"))

108− (\e -> do sendMessage (Left (show e)))

111+ (\e -> do liftIO $ putStrLn $ sendMessage 0 (Left (show e)))

109 ideslave orig mods

112 ideslave orig mods

110

113

111-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

114-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

@@ -498,7 +501,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function

498parseArgs :: [String] -> [Opt]

501parseArgs :: [String] -> [Opt]

499parseArgs [] = []

502parseArgs [] = []

500parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

503parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

501−parseArgs ("--ideslave":ns) = IdeSlave : (parseArgs ns)

504+parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)

502parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

505parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

503parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

506parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

504parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

507parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

@@ -552,7 +555,7 @@ idrisMain :: [Opt] -> Idris ()

552idrisMain opts =

555idrisMain opts =

553 do let inputs = opt getFile opts

556 do let inputs = opt getFile opts

554 let quiet = Quiet `elem` opts

557 let quiet = Quiet `elem` opts

555− let idesl = IdeSlave `elem` opts

558+ let idesl = Ideslave `elem` opts

556 let runrepl = not (NoREPL `elem` opts)

559 let runrepl = not (NoREPL `elem` opts)

557 let output = opt getOutput opts

560 let output = opt getOutput opts

558 let newoutput = opt getNewOutput opts

561 let newoutput = opt getNewOutput opts