e0783ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

initial ideslave

e0783efHannes Mehnert14 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -90,7 +90,7 @@ Executable idris

90 Core.CaseTree, Core.Constraints,

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,

95 Idris.Delaborate, Idris.Primitives, Idris.Imports,

96 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

src/Idris/AbsSyntax.hs+6

@@ -299,6 +299,12 @@ setQuiet q = do i <- getIState

299 let opt' = opts { opt_quiet = q }

300 putIState $ i { idris_options = opt' }

301

302+setIdeSlave :: Bool -> Idris ()

303+setIdeSlave s = do i <- getIState

304+ let opts = idris_options i

305+ let opt' = opts { opt_ideslave = s }

306+ putIState $ i { idris_options = opt' }

307+

302setTarget :: Target -> Idris ()

308setTarget :: Target -> Idris ()

303setTarget t = do i <- getIState

309setTarget t = do i <- getIState

304 let opts = idris_options i

310 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+3−1

@@ -33,6 +33,7 @@ data IOption = IOption { opt_logLevel :: Int,

33 opt_repl :: Bool,

34 opt_verbose :: Bool,

35 opt_quiet :: Bool,

36+ opt_ideslave :: Bool,

36 opt_target :: Target,

37 opt_target :: Target,

37 opt_outputTy :: OutputType,

38 opt_outputTy :: OutputType,

38 opt_ibcsubdir :: FilePath,

39 opt_ibcsubdir :: FilePath,

@@ -41,7 +42,7 @@ data IOption = IOption { opt_logLevel :: Int,

41 }

42 }

42 deriving (Show, Eq)

43 deriving (Show, Eq)

44−defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []

45+defaultOpts = IOption 0 False False True False False True True False False ViaC Executable "" [] []

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

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

@@ -202,6 +203,7 @@ data Opt = Filename String

202 | Ver

203 | Ver

203 | Usage

204 | Usage

204 | Quiet

205 | Quiet

206+ | IdeSlave

205 | ShowLibs

207 | ShowLibs

206 | ShowLibdir

208 | ShowLibdir

207 | ShowIncs

209 | ShowIncs

src/Idris/IdeSlave.hsnew file+119

@@ -0,0 +1,119 @@

1+{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

3+module Idris.IdeSlave(receiveMessage, sendMessage) where

5+import Text.Printf

6+import Numeric

7+import Data.List

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 Bool where

30+ toSExp True = BoolAtom True

31+ toSExp False = BoolAtom False

32+

33+instance SExpable String where

34+ toSExp s = StringAtom s

35+

36+instance SExpable Integer where

37+ toSExp n = IntegerAtom n

38+

39+instance SExpable Int where

40+ toSExp n = IntegerAtom (toInteger n)

41+

42+instance (SExpable a) => SExpable (Maybe a) where

43+ toSExp Nothing = List [SymbolAtom "Nothing"]

44+ toSExp (Just a) = List ((SymbolAtom "Just") : [toSExp a])

45+

46+instance (SExpable a) => SExpable [a] where

47+ toSExp l = List (map toSExp l)

48+

49+escape :: String -> String

50+escape = concatMap escapeChar

51+ where

52+ escapeChar '\\' = "\\\\"

53+ escapeChar '"' = "\\\""

54+ escapeChar c = [c]

55+

56+pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))

57+ return (List xs)

58+ <|> atom

59+

60+atom = do char ':'; x <- atomC; return x

61+ <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

62+ <|> do ints <- many1 digit

63+ case readDec ints of

64+ ((num, ""):_) -> return (IntegerAtom (toInteger num))

65+ _ -> return (StringAtom ints)

66+

67+atomC = do string "True"; return (BoolAtom True)

68+ <|> do string "False"; return (BoolAtom False)

69+ <|> do xs <- many (noneOf " \n\"()"); return (SymbolAtom xs)

70+

71+quotedChar = noneOf "\""

72+ <|> try (string "\\\"" >> return '"')

73+

74+parseSExp :: String -> Either ParseError SExp

75+parseSExp input = parse pSExp "(unknown)" input

76+

77+data Command = Version

78+ deriving Show

79+

80+sexpToCommand :: SExp -> Maybe Command

81+sexpToCommand (List (x:[])) = sexpToCommand x

82+sexpToCommand (SymbolAtom "version") = Just Version

83+sexpToCommand _ = Nothing

84+

85+receiveMessage :: IO (Maybe Command)

86+receiveMessage

87+ = do x <- getLine

88+ return (receiveString x)

89+

90+receiveString :: String -> Maybe Command

91+receiveString x =

92+ case readHex (take 6 x) of

93+ ((num, ""):_) ->

94+ let msg = drop 6 x in

95+ if (length msg) /= (num - 1)

96+ then error "bad input"

97+ else parseSExpToCommand msg

98+ _ -> error "blah"

99+

100+parseSExpToCommand :: String -> Maybe Command

101+parseSExpToCommand msg =

102+ case parseSExp msg of

103+ Left _ -> Nothing

104+ Right r -> sexpToCommand r

105+

106+sendMessage :: SExpable a => a -> IO ()

107+sendMessage s =

108+ do let str = convertToSExpString s

109+ putStrLn $ (getHexLength str) ++ str

110+

111+convertToSExpString :: SExpable a => a -> String

112+convertToSExpString s =

113+ let str = sExpToString (toSExp s) in

114+ if (str !! 0) == '('

115+ then str

116+ else "(" ++ str ++ ")"

117+

118+getHexLength :: String -> String

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

src/Idris/REPL.hs+17−2

@@ -18,6 +18,7 @@ import Idris.UnusedArgs

18import Idris.Docs

19import Idris.Help

20import Idris.Completion

21+import Idris.IdeSlave

22import Paths_idris

23import Paths_idris

23import Util.System

24import Util.System

@@ -80,6 +81,16 @@ 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

84+-- | Run the IdeSlave

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

86+ideslave orig mods

87+ = do x <- liftIO $ receiveMessage

88+ case x of

89+ Nothing -> do liftIO $ sendMessage (Just "did not understand")

90+ Just y -> do liftIO $ sendMessage (Just "understood you!")

91+ liftIO $ sendMessage (Just "Hello world")

92+ ideslave orig mods

93+

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

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

84mkPrompt [] = "Idris"

95mkPrompt [] = "Idris"

85mkPrompt [x] = "*" ++ dropExtension x

96mkPrompt [x] = "*" ++ dropExtension x

@@ -471,6 +482,7 @@ parseTarget _ = error "unknown target" -- FIXME: partial function

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

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

472parseArgs [] = []

483parseArgs [] = []

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

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

485+parseArgs ("--ideslave":ns) = IdeSlave : (parseArgs ns)

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

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

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

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

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

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

@@ -524,6 +536,7 @@ idrisMain :: [Opt] -> Idris ()

524idrisMain opts =

536idrisMain opts =

525 do let inputs = opt getFile opts

537 do let inputs = opt getFile opts

526 let quiet = Quiet `elem` opts

538 let quiet = Quiet `elem` opts

539+ let idesl = IdeSlave `elem` opts

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

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

528 let output = opt getOutput opts

541 let output = opt getOutput opts

529 let newoutput = opt getNewOutput opts

542 let newoutput = opt getNewOutput opts

@@ -543,6 +556,7 @@ idrisMain opts =

543 mapM_ addLangExt (opt getLanguageExt opts)

556 mapM_ addLangExt (opt getLanguageExt opts)

544 setREPL runrepl

557 setREPL runrepl

545 setQuiet quiet

558 setQuiet quiet

559+ setIdeSlave idesl

546 setVerbose runrepl

560 setVerbose runrepl

547 setCmdLine opts

561 setCmdLine opts

548 setOutputTy outty

562 setOutputTy outty

@@ -567,7 +581,7 @@ idrisMain opts =

567 elabPrims

581 elabPrims

568 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

582 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

569 return ()

583 return ()

570− when (runrepl && not quiet) $ iputStrLn banner

584+ when (runrepl && not quiet && not idesl) $ iputStrLn banner

571 ist <- getIState

585 ist <- getIState

572 mods <- mapM loadModule inputs

586 mods <- mapM loadModule inputs

573 ok <- noErrors

587 ok <- noErrors

@@ -577,7 +591,8 @@ idrisMain opts =

577 when ok $ case newoutput of

591 when ok $ case newoutput of

578 [] -> return ()

592 [] -> return ()

579 (o:_) -> process "" (NewCompile o)

593 (o:_) -> process "" (NewCompile o)

580− when runrepl $ runInputT replSettings $ repl ist inputs

594+ when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs

595+ when (idesl) $ runInputT replSettings $ ideslave ist inputs

581 ok <- noErrors

596 ok <- noErrors

582 when (not ok) $ liftIO (exitWith (ExitFailure 1))

597 when (not ok) $ liftIO (exitWith (ExitFailure 1))

583 where

598 where