diff --git a/Notes/IDE-mode.md b/Notes/IDE-mode.md index 056ad5b..02a2947 100644 --- a/Notes/IDE-mode.md +++ b/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. - diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index ea6157a..cab2803 100644 --- a/src/Idris/CommandLine.idr +++ b/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 diff --git a/src/Idris/IDEMode/Client.idr b/src/Idris/IDEMode/Client.idr new file mode 100644 index 0000000..5cdc218 --- /dev/null +++ b/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 diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index ac56125..9b4cba3 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/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 diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 124bd6d..4ad2abc 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/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 - diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index f46f906..12e7176 100644 --- a/src/Idris/Main.idr +++ b/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 diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 6698ace..e732fe2 100644 --- a/src/Idris/SetOptions.idr +++ b/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 - diff --git a/tests/Main.idr b/tests/Main.idr index 862ce54..d46511d 100644 --- a/tests/Main.idr +++ b/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 diff --git a/tests/ideMode/ideMode001/LocType.idr b/tests/ideMode/ideMode001/LocType.idr new file mode 100644 index 0000000..dd8a348 --- /dev/null +++ b/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 diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected new file mode 100644 index 0000000..22d62d3 --- /dev/null +++ b/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 diff --git a/tests/ideMode/ideMode001/input b/tests/ideMode/ideMode001/input new file mode 100644 index 0000000..f079ba3 --- /dev/null +++ b/tests/ideMode/ideMode001/input @@ -0,0 +1 @@ +00001e((:load-file "LocType.idr") 1) diff --git a/tests/ideMode/ideMode001/run b/tests/ideMode/ideMode001/run new file mode 100755 index 0000000..86bdf71 --- /dev/null +++ b/tests/ideMode/ideMode001/run @@ -0,0 +1,3 @@ +$1 --ide-mode < input + +rm -rf build