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

git.iko.soy/Idris-dev

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

commit4118b79334f39b4b5c0c64f18e8da28c95999f2e authorHannes Mehnert <hannes@mehnert.org> dateTue 7 May 2013, 23:04 (13 years ago) parent3b00d8d

4 files changed+49−37

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+14−1 src/Idris/AbsSyntaxTree.hs+6−3 src/Idris/IdeSlave.hs+16−23 src/Idris/REPL.hs+13−10

src/Idris/AbsSyntax.hs+14−1

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

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

99import Core.Typecheck

1010import Idris.AbsSyntaxTree

11+import Idris.IdeSlave

1112import IRTS.CodegenCommon

1213import Util.DynamicLinker

1314

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

2627import Util.Pretty

2728import Util.System

2829

30+import Text.Printf (printf)

31+

2932getContext :: Idris Context

3033getContext = do i <- getIState; return (tt_ctxt i)

3134

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

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

240243

241244iputStrLn :: String -> Idris ()

242−iputStrLn = liftIO . putStrLn

245+iputStrLn s = do i <- getIState

246+ case idris_outputmode i of

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))

243256

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

245258iWarn 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

4646

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

4848

49+-- | The output mode in use

50+data OutputMode = RawOutput | IdeSlave Integer deriving Show

51+

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

5053-- without typechecking).

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

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

9497 compiled_so :: Maybe String,

9598 idris_dynamic_libs :: [DynamicLib],

9699 idris_language_extensions :: [LanguageExt],

97− ideslave_counter :: Integer

100+ idris_outputmode :: OutputMode

98101 }

99102

100103data SizeChange = Smaller | Same | Bigger | Unknown

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

146149 emptyContext emptyContext emptyContext emptyContext

147150 emptyContext emptyContext emptyContext emptyContext

148151 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

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

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

150153

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

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

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

205208 | Ver

206209 | Usage

207210 | Quiet

208− | IdeSlave

211+ | Ideslave

209212 | ShowLibs

210213 | ShowLibdir

211214 | ShowIncs

src/Idris/IdeSlave.hs+16−23

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

11{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

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

4−

5−import Idris.AbsSyntaxTree

6−import Idris.AbsSyntax

7−

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

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

105import Text.Printf

116import Numeric

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

3429instance SExpable SExp where

3530 toSExp a = a

3631

32+instance SExpable () where

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

34+

3735instance SExpable Bool where

3836 toSExp True = BoolAtom True

3937 toSExp False = BoolAtom False

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

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

9896sexpToCommand _ = Nothing

9997

100−receiveMessage :: Idris (SExp)

101−receiveMessage = do x <- liftIO $ getLine

102− case receiveString x of

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

104− do i <- getIState

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

106− return cmd

107−

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

99+receiveMessage x = case receiveString x of

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

101+ (cmd, id)

108102

109103receiveString :: String -> SExp

110104receiveString x =

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

118112 Right r -> r)

119113 _ -> error "readHex failed"

120114

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

122−sendMessage s =

123− do i <- getIState

124− let msg = case s of

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

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

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

128− where conv id sexp =

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

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

116+sendMessage id s =

117+ let sexp = case s of

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

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

120+ in conv id sexp

121+ where conv id sexp =

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

130123

131124getHexLength :: String -> String

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

src/Idris/REPL.hs+13−10

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

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

8686ideslave orig mods

8787 = do idrisCatch

88− (do sexp <- receiveMessage

88+ (do l <- liftIO $ getLine

89+ let (sexp, id) = receiveMessage l

90+ i <- getIState

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

8992 case sexpToCommand sexp of

9093 Just (Interpret cmd) ->

9194 do i <- getIState

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

9396 (f:_) -> f

9497 _ -> ""

9598 case parseCmd i cmd of

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

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

97100 Right cmd -> do idrisCatch

98101 (do xs <- process fn cmd

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

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

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

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

101104 Just (REPLCompletions str) ->

102105 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))

104107 Just (LoadFile filename) -> do clearErr

105108 mod <- loadModule filename

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

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

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

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

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

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

109112 ideslave orig mods

110113

111114-- | 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

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

499502parseArgs [] = []

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

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

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

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

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

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

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

552555idrisMain opts =

553556 do let inputs = opt getFile opts

554557 let quiet = Quiet `elem` opts

555− let idesl = IdeSlave `elem` opts

558+ let idesl = Ideslave `elem` opts

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

557560 let output = opt getOutput opts

558561 let newoutput = opt getNewOutput opts