Merge pull request #75 from abailly/configurable-ide-mode-socket

Configurable ide-mode-socket REPL

Notes/IDE-mode.md

@@ -40,4 +40,3 @@ Generates a pattern matching definition, if it can find one, for the function
 declared with the given name, on the given line. It will only return the
 first definition it finds, as a list of pattern clauses. This works via a
 combination of case splitting and expression search.
-

src/Idris/CommandLine.idr

@@ -1,5 +1,7 @@
 module Idris.CommandLine
 
+import Data.String
+
 %default total
 
 public export
@@ -48,7 +50,7 @@ data CLOpt
    ||| Whether or not to run in IdeMode (easily parsable for other tools)
   IdeMode |
    ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
-  IdeModeSocket | 
+  IdeModeSocket String |
    ||| Run as a checker for the core language TTImp
   Yaffle String |
   Timing |
@@ -82,9 +84,12 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
 
            MkOpt ["--ide-mode"] [] [IdeMode]
               (Just "Run the REPL with machine-readable syntax"),
-           
-           MkOpt ["--ide-mode-socket"] [] [IdeModeSocket]
-              (Just "Run the ide socket mode"),
+
+           MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"]
+              (Just "Run the ide socket mode on default host and port (localhost:38398"),
+
+           MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
+              (Just "Run the ide socket mode on given host and port"),
 
            MkOpt ["--prefix"] [] [ShowPrefix]
               (Just "Show installation prefix"),
@@ -183,3 +188,18 @@ getCmdOpts = do (_ :: opts) <- getArgs
                     | pure (Left "Invalid command line")
                 pure $ getOpts opts
 
+portPart : String -> Maybe String
+portPart p with (not $ p == "") proof prf
+  portPart p | False  = Nothing
+  portPart p | True = Just $ strTail' p (sym prf)
+
+||| Extract the host and port to bind the IDE socket to
+public export
+ideSocketModeHostPort : List CLOpt -> (String, Int)
+ideSocketModeHostPort []  = ("localhost", 38398)
+ideSocketModeHostPort (IdeModeSocket hp :: _) =
+  let (h, p) = Strings.break (== ':') hp
+      port = fromMaybe 38398 (portPart p >>= parsePositive)
+      host = if h == "" then "localhost" else h
+  in (host, port)
+ideSocketModeHostPort (_ :: rest) = ideSocketModeHostPort rest

src/Idris/IDEMode/Client.idr

@@ -0,0 +1,143 @@
+module Idris.IDEMode.Client
+
+import Data.Primitives.Views
+import System
+import Idris.IDEMode.Commands
+import Idris.IDEMode.Parser
+import Idris.Socket
+import Idris.Syntax
+import Idris.REPL
+import Idris.Socket.Data
+import Idris.IDEMode.REPL
+import Parser.Support
+
+hexDigit : Int -> Char
+hexDigit 0 = '0'
+hexDigit 1 = '1'
+hexDigit 2 = '2'
+hexDigit 3 = '3'
+hexDigit 4 = '4'
+hexDigit 5 = '5'
+hexDigit 6 = '6'
+hexDigit 7 = '7'
+hexDigit 8 = '8'
+hexDigit 9 = '9'
+hexDigit 10 = 'a'
+hexDigit 11 = 'b'
+hexDigit 12 = 'c'
+hexDigit 13 = 'd'
+hexDigit 14 = 'e'
+hexDigit 15 = 'f'
+
+||| Convert a positive integer into a list of (lower case) hexadecimal characters
+asHex : Int -> String
+asHex n = pack $ asHex' n []
+  where
+    asHex' : Int -> List Char -> List Char
+    asHex' 0 hex = hex
+    asHex' n hex with (n `divides` 16)
+      asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex)
+
+connectTo : String -> Int -> IO (Either String Socket)
+connectTo host port = do
+  osock <- socket AF_INET Stream 0
+  case osock of
+    Left fail => do
+      pure $ Left ("Failed to open client socket " ++ show fail)
+    Right sock => do
+      res <- connect sock (Hostname host) port
+      if res /= 0
+      then pure $ Left ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show res)
+      else pure (Right sock)
+
+||| Runs an ide-mode client to execute one command against a given server
+serialize : IDECommand -> Maybe String
+serialize cmd =
+  let scmd = show $ SExpList [ toSExp cmd, toSExp 1 ]
+      hexLen = asHex $ cast $ Strings.length scmd
+      len = case isLTE (length hexLen) 6 of
+                 (Yes _) => Just $ cast (replicate (6 - length hexLen) '0') ++  hexLen
+                 (No  _) => Nothing
+  in (++) <$> len <*> Just scmd
+
+
+readOutput : Socket -> IO (Either String  SExp)
+readOutput sock = do
+  Right (len, _) <- recv sock 6 | Left err => pure (Left $ "failed to read from socket, error: " ++ show err)
+  case toHex 1 (reverse $ cast len) of
+    Nothing => pure $ Left ("expected a length in six-digits hexadecimal, got " ++ len)
+    Just num => do
+      Right (msg, _) <- recv sock num | Left err => pure (Left $ "failed to read from socket, error: " ++ show err)
+      pure $ either (Left . show) Right $ parseSExp msg
+
+data IDEResult : Type where
+  IDEReturn : List SExp -> IDEResult
+  NetworkError : String -> IDEResult
+  InputError : String -> IDEResult
+  OutputError : String -> IDEResult
+
+implementation Show IDEResult where
+  show (IDEReturn exprs) = unlines $ map show exprs
+  show (NetworkError reason) = reason
+  show (InputError reason) = reason
+  show (OutputError reason) = reason
+
+
+readResult: Socket -> List SExp -> IO IDEResult
+readResult sock outputs = do
+  Right output <- readOutput sock | Left err => pure (OutputError err)
+  case output of
+    SExpList (SymbolAtom "return" :: rest) => pure (IDEReturn (SExpList rest :: outputs))
+    res => do
+      readResult sock (res :: outputs)
+
+execute : Socket -> IDECommand -> IO IDEResult
+execute cnx command = do
+      let cmdString = serialize command
+      case cmdString of
+        Just cmd => do
+          Right sent <- send cnx cmd
+            | Left err => pure (NetworkError ("Failed to send command, error: " ++ show err))
+          readResult cnx []
+        Nothing => pure $ InputError "Command is too long"
+
+connect : String -> Int -> IO Socket
+connect host port = do
+  Right sock <- connectTo host port
+    | Left fail => do
+      putStrLn $ "fail to connect to " ++ host ++ ":" ++ show port ++", error: " ++ fail
+      exit 1
+  pure sock
+
+makeIDECommand : REPLCmd -> Either String IDECommand
+makeIDECommand (Eval term)            = Right $ Interpret (show term)
+makeIDECommand (Check term)           = Right $ TypeOf (show term) Nothing
+makeIDECommand (Load file)            = Right $ LoadFile file Nothing
+makeIDECommand (Editing (TypeAt line col name)) = Right $ TypeOf (show name) (Just (cast line, cast col))
+makeIDECommand other                  = Left "Don't know how to interpret command"
+
+parseCommand : String -> Either String IDECommand
+parseCommand = either (Left . show) makeIDECommand . parseRepl
+
+repl : Socket -> IO ()
+repl cnx
+    = do putStr prompt
+         Right input <- map parseCommand getLine
+           | Left err => do
+                  putStrLn err
+                  repl cnx
+         end <- fEOF stdin
+         if end
+            then putStrLn "Bye!"
+            else do
+              result <- execute cnx input
+              putStrLn $ show result
+              repl cnx
+
+  where
+    prompt : String
+    prompt = "λ> "
+
+export
+client : String -> Int -> IO ()
+client host port = connect host port  >>= repl

src/Idris/IDEMode/Commands.idr

@@ -25,7 +25,7 @@ data IDECommand
      | MakeLemma Integer String
      | MakeCase Integer String
      | MakeWith Integer String
-    
+
 readHints : List SExp -> Maybe (List String)
 readHints [] = Just []
 readHints (StringAtom s :: rest)
@@ -46,7 +46,7 @@ getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n])
 getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n,
                          IntegerAtom l, IntegerAtom c])
     = Just $ TypeOf n (Just (l, c))
-getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c, 
+getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c,
                          StringAtom n])
     = Just $ CaseSplit l c n
 getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
@@ -76,6 +76,25 @@ getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
     = Just $ MakeWith l n
 getIDECommand _ = Nothing
 
+export
+putIDECommand : IDECommand -> SExp
+putIDECommand (Interpret cmd)                 = (SExpList [SymbolAtom "interpret", StringAtom cmd])
+putIDECommand (LoadFile fname Nothing)        = (SExpList [SymbolAtom "load-file", StringAtom fname])
+putIDECommand (LoadFile fname (Just line))    = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line])
+putIDECommand (TypeOf cmd Nothing)            = (SExpList [SymbolAtom "type-of", StringAtom cmd])
+putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])
+putIDECommand (CaseSplit line col n)          = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
+putIDECommand (AddClause line n)              = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
+putIDECommand (ExprSearch line n exprs mode)  = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode])
+  where
+  getMode : Bool -> SExp
+  getMode True  = SymbolAtom "all"
+  getMode False = SymbolAtom "other"
+putIDECommand (GenerateDef line n)            = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n])
+putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
+putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
+putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
+
 export
 getMsg : SExp -> Maybe (IDECommand, Integer)
 getMsg (SExpList [cmdexp, IntegerAtom num])
@@ -103,6 +122,10 @@ public export
 interface SExpable a where
   toSExp : a -> SExp
 
+export
+SExpable IDECommand where
+  toSExp = putIDECommand
+
 export
 SExpable SExp where
   toSExp = id
@@ -129,7 +152,7 @@ SExpable Name where
 
 export
 (SExpable a, SExpable b) => SExpable (a, b) where
-  toSExp (x, y) 
+  toSExp (x, y)
       = case toSExp y of
              SExpList xs => SExpList (toSExp x :: xs)
              y' => SExpList [toSExp x, y']
@@ -151,7 +174,7 @@ hex : File -> Int -> IO ()
 hex (FHandle h) num = foreign FFI_C "fprintf" (Ptr -> String -> Int -> IO ()) h "%06x" num
 
 sendLine : File -> String -> IO ()
-sendLine (FHandle h) st = 
+sendLine (FHandle h) st =
   map (const ()) (prim_fwrite h st)
 
 export

src/Idris/IDEMode/REPL.idr

@@ -43,10 +43,10 @@ socketToFile (MkSocket f _ _ _) = do
   if !(ferror file) then do
     pure (Left "Failed to fdopen socket file descriptor")
   else pure (Right file)
-  
+
 export
-initIDESocketFile : Int -> IO (Either String File)
-initIDESocketFile p = do
+initIDESocketFile : String -> Int -> IO (Either String File)
+initIDESocketFile h p = do
   osock <- socket AF_INET Stream 0
   case osock of
     Left fail => do
@@ -54,9 +54,9 @@ initIDESocketFile p = do
       putStrLn "Failed to open socket"
       exit 1
     Right sock => do
-      res <- bind sock (Just (Hostname "localhost")) p
-      if res /= 0 
-      then 
+      res <- bind sock (Just (Hostname h)) p
+      if res /= 0
+      then
         pure (Left ("Failed to bind socket with error: " ++ show res))
       else do
         res <- listen sock
@@ -66,11 +66,11 @@ initIDESocketFile p = do
         else do
           putStrLn (show p)
           res <- accept sock
-          case res of 
-            Left err => 
+          case res of
+            Left err =>
                pure (Left ("Failed to accept on socket with error: " ++ show err))
-            Right (s, _) => 
-               socketToFile s             
+            Right (s, _) =>
+               socketToFile s
 
 getChar : File -> IO Char
 getChar (FHandle h) = do
@@ -83,7 +83,7 @@ getChar (FHandle h) = do
       putStrLn "Failed to read a character"
       exit 1
     else pure chr
-  
+
 getFLine : File -> IO String
 getFLine (FHandle h) = do
   str <- prim_fread h
@@ -95,7 +95,7 @@ getFLine (FHandle h) = do
 getNChars : File -> Nat -> IO (List Char)
 getNChars i Z = pure []
 getNChars i (S k)
-    = do x <- getChar i 
+    = do x <- getChar i
          xs <- getNChars i k
          pure (x :: xs)
 
@@ -117,12 +117,14 @@ hex 'd' = Just 13
 hex 'e' = Just 14
 hex 'f' = Just 15
 hex _ = Nothing
-    
+
+export
 toHex : Int -> List Char -> Maybe Int
 toHex _ [] = Just 0
-toHex m (d :: ds) 
+toHex m (d :: ds)
     = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
 
+
 -- Read 6 characters. If they're a hex number, read that many characters.
 -- Otherwise, just read to newline
 getInput : File -> IO String
@@ -145,7 +147,7 @@ process : {auto c : Ref Ctxt Defs} ->
 process (Interpret cmd)
     = do interpret cmd
          printResult "Done"
-process (LoadFile fname toline) 
+process (LoadFile fname toline)
     = do opts <- get ROpts
          put ROpts (record { mainfile = Just fname } opts)
          resetContext
@@ -157,7 +159,7 @@ process (LoadFile fname toline)
          case errs of
               [] => printResult $ "Loaded " ++ fname
               _ => printError $ "Failed to load " ++ fname
-process (TypeOf n Nothing) 
+process (TypeOf n Nothing)
     = do Idris.REPL.process (Check (PRef replFC (UN n)))
          pure ()
 process (TypeOf n (Just (l, c)))
@@ -170,7 +172,7 @@ process (AddClause l n)
     = do Idris.REPL.process (Editing (AddClause (fromInteger l) (UN n)))
          pure ()
 process (ExprSearch l n hs all)
-    = do Idris.REPL.process (Editing (ExprSearch (fromInteger l) (UN n) 
+    = do Idris.REPL.process (Editing (ExprSearch (fromInteger l) (UN n)
                                                  (map UN hs) all))
          pure ()
 process (GenerateDef l n)
@@ -205,7 +207,7 @@ processCatch cmd
                            put ROpts o'
                            emitError err
                            printError "Command failed")
-                                                      
+
 loop : {auto c : Ref Ctxt Defs} ->
        {auto u : Ref UST UState} ->
        {auto s : Ref Syn SyntaxInfo} ->
@@ -213,7 +215,7 @@ loop : {auto c : Ref Ctxt Defs} ->
        {auto o : Ref ROpts REPLOpts} ->
        Core ()
 loop
-    = do res <- getOutput 
+    = do res <- getOutput
          case res of
               REPL _ => printError "Running idemode but output isn't"
               IDEMode _ inf outf => do
@@ -226,11 +228,11 @@ loop
                        loop
                   Right sexp =>
                     case getMsg sexp of
-                      Just (cmd, i) => 
+                      Just (cmd, i) =>
                         do updateOutput i
                            processCatch cmd
-                           loop 
-                      Nothing => 
+                           loop
+                      Nothing =>
                         do printError ("Unrecognised command: " ++ show sexp)
                            loop
   where
@@ -254,4 +256,3 @@ replIDE
               IDEMode _ inf outf => do
                 send outf (version 2 0)
                 loop
-

src/Idris/Main.idr

@@ -144,7 +144,8 @@ stMain opts
                        setOutput (IDEMode 0 stdin stdout)
                        replIDE {c} {u} {m}
                      else do
-                       f <- coreLift $ initIDESocketFile 38398
+                       let (host, port) = ideSocketModeHostPort opts
+                       f <- coreLift $ initIDESocketFile host port
                        case f of
                          Left err => do
                            coreLift $ putStrLn err

src/Idris/SetOptions.idr

@@ -18,7 +18,7 @@ addPkgDir : {auto c : Ref Ctxt Defs} ->
             String -> Core ()
 addPkgDir p
     = do defs <- get Ctxt
-         addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++ 
+         addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
                              "idris2" ++ dirSep ++ p)
 
 -- Options to be processed before type checking
@@ -37,7 +37,7 @@ preOptions (SetCG e :: opts)
     = case getCG e of
            Just cg => do setCG cg
                          preOptions opts
-           Nothing => 
+           Nothing =>
               do coreLift $ putStrLn "No such code generator"
                  coreLift $ putStrLn $ "Code generators available: " ++
                                  showSep ", " (map fst availableCGs)
@@ -63,11 +63,11 @@ postOptions (OutputFile outfile :: rest)
     = do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile
          postOptions rest
          pure False
-postOptions (ExecFn str :: rest) 
+postOptions (ExecFn str :: rest)
     = do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
          postOptions rest
          pure False
-postOptions (CheckOnly :: rest) 
+postOptions (CheckOnly :: rest)
     = do postOptions rest
          pure False
 postOptions (_ :: rest) = postOptions rest
@@ -81,6 +81,5 @@ ideMode (_ :: xs) = ideMode xs
 export
 ideModeSocket : List CLOpt -> Bool
 ideModeSocket [] = False
-ideModeSocket (IdeModeSocket :: _) = True
+ideModeSocket (IdeModeSocket _ :: _) = True
 ideModeSocket (_ :: xs) = ideModeSocket xs
-

tests/Main.idr

@@ -64,6 +64,10 @@ chezTests
    = ["chez001", "chez002", "chez003", "chez004",
       "chez005", "chez006", "chez007"]
 
+ideModeTests : List String
+ideModeTests
+  =  [ "ideMode001" ]
+
 chdir : String -> IO Bool
 chdir dir
     = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
@@ -136,7 +140,8 @@ main
          let filteredNonCGTests =
               filterTests $ concat [testPaths "ttimp" ttimpTests,
                                     testPaths "idris2" idrisTests,
-                                    testPaths "typedd-book" typeddTests]
+                                    testPaths "typedd-book" typeddTests,
+                                    testPaths "ideMode" ideModeTests]
          let filteredChezTests = filterTests (testPaths "chez" chezTests)
          nonCGTestRes <- traverse (runTest idris2) filteredNonCGTests
          chezTestRes <- if length filteredChezTests > 0

tests/ideMode/ideMode001/LocType.idr

@@ -0,0 +1,7 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys

tests/ideMode/ideMode001/expected

@@ -0,0 +1,4 @@
+000018(:protocol-version 2 0)
+000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
+00002a(:return (:ok "Loaded LocType.idr" ()) 1)
+Alas the file is done, aborting

tests/ideMode/ideMode001/input

@@ -0,0 +1 @@
+00001e((:load-file "LocType.idr") 1)

tests/ideMode/ideMode001/run

@@ -0,0 +1,3 @@
+$1 --ide-mode < input
+
+rm -rf build