From 3321dc6be308a53669ddb3bf6e67aa4c6ecf00ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Mon, 18 May 2020 18:28:33 +0100 Subject: [PATCH 1/4] Add rmDir to System.Directory --- bootstrap/idris2sh_app/idris2sh.ss | 1 + libs/base/System/Directory.idr | 7 +++++++ support/c/idris_directory.c | 4 ++++ 3 files changed, 12 insertions(+) diff --git a/bootstrap/idris2sh_app/idris2sh.ss b/bootstrap/idris2sh_app/idris2sh.ss index c67aaa1b4..d0d0c9e7e 100755 --- a/bootstrap/idris2sh_app/idris2sh.ss +++ b/bootstrap/idris2sh_app/idris2sh.ss @@ -259,6 +259,7 @@ (define Directory-System-prim_createDir (lambda (farg-0 farg-1) ((foreign-procedure #f "idris2_createDir" (string) int) farg-0))) (define Directory-System-prim_closeDir (lambda (farg-0 farg-1) ((foreign-procedure #f "idris2_dirClose" (void*) void) farg-0) (vector 0 ))) (define Directory-System-prim_changeDir (lambda (farg-0 farg-1) ((foreign-procedure #f "idris2_changeDir" (string) int) farg-0))) +(define Directory-System-prim_rmDir (lambda (farg-0 farg-1) ((foreign-procedure #f "idris2_rmDir" (string) int) farg-0))) (define Buffer-Data-stringByteLength (lambda (farg-0) ((foreign-procedure #f "strlen" (string) int) farg-0))) (define Buffer-Data-prim__writeBuffer (lambda (farg-0 farg-1 farg-2 farg-3) (blodwen-write-bytevec farg-0 farg-1 farg-2))) (define Buffer-Data-prim__setString (lambda (farg-0 farg-1 farg-2 farg-3) (blodwen-buffer-setstring farg-0 farg-1 farg-2))) diff --git a/libs/base/System/Directory.idr b/libs/base/System/Directory.idr index a722e6538..7fa519d51 100644 --- a/libs/base/System/Directory.idr +++ b/libs/base/System/Directory.idr @@ -41,6 +41,9 @@ prim_openDir : String -> PrimIO DirPtr %foreign support "idris2_dirClose" prim_closeDir : DirPtr -> PrimIO () +%foreign support "idris2_rmDir" +prim_rmDir : String -> PrimIO () + %foreign support "idris2_nextDirEntry" prim_dirEntry : DirPtr -> PrimIO (Ptr String) @@ -82,6 +85,10 @@ export dirClose : Directory -> IO () dirClose (MkDir d) = primIO (prim_closeDir d) +export +rmDir : String -> IO () +rmDir dirName = primIO (prim_rmDir dirName) + export dirEntry : Directory -> IO (Either FileError String) dirEntry (MkDir d) diff --git a/support/c/idris_directory.c b/support/c/idris_directory.c index a6c583d90..778d9ac70 100644 --- a/support/c/idris_directory.c +++ b/support/c/idris_directory.c @@ -49,6 +49,10 @@ void idris2_dirClose(void* d) { free(di); } +int idris2_rmDir(char* path) { + return rmdir(path); +} + char* idris2_nextDirEntry(void* d) { DirInfo* di = (DirInfo*)d; struct dirent* de = readdir(di->dirptr); From 47e943cc7d6deb823b356dcc89f8a1f81ee4e6ac Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Tue, 19 May 2020 17:49:21 +0600 Subject: [PATCH 2/4] Update .gitignore files --- .gitignore | 9 +++------ libs/network/.gitignore | 2 ++ support/c/.gitignore | 8 ++++++++ 3 files changed, 13 insertions(+), 6 deletions(-) create mode 100644 support/c/.gitignore diff --git a/.gitignore b/.gitignore index f5ab3c0f2..eb8d6d3f0 100644 --- a/.gitignore +++ b/.gitignore @@ -3,16 +3,13 @@ *.ttc *.ttm -*.dSYM - /build -/dist/idris2.c - -/docs/build/ - /libs/**/build + /tests/**/output /tests/**/*.so /tests/**/*.dylib /tests/**/*.dll + +/src/IdrisPaths.idr diff --git a/libs/network/.gitignore b/libs/network/.gitignore index d4d0722cc..16cb2adfc 100644 --- a/libs/network/.gitignore +++ b/libs/network/.gitignore @@ -3,6 +3,8 @@ *.d *.o *.obj +*.a +*.lib *.so *.dylib *.dll diff --git a/support/c/.gitignore b/support/c/.gitignore new file mode 100644 index 000000000..4077c8d7f --- /dev/null +++ b/support/c/.gitignore @@ -0,0 +1,8 @@ +*.d +*.o +*.obj +*.a +*.lib +*.so +*.dylib +*.dll From b801b97fcc5c0b23acfc88b8a6e081e2a479dc6b Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Tue, 19 May 2020 18:50:47 +0600 Subject: [PATCH 3/4] Refactor makefiles --- Makefile | 7 +++---- config.mk | 2 +- libs/base/Makefile | 2 +- libs/contrib/Makefile | 2 +- libs/network/Makefile | 10 +++++----- libs/prelude/Makefile | 2 +- support/c/Makefile | 6 +++--- 7 files changed, 15 insertions(+), 16 deletions(-) diff --git a/Makefile b/Makefile index b693c6287..06c741278 100644 --- a/Makefile +++ b/Makefile @@ -28,8 +28,7 @@ export IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH} IDRIS2_VERSION_TAG := ${IDRIS2_VERSION}${VER_TAG} export SCHEME -export IDRIS2_CURDIR = $(CURDIR) -export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc:${IDRIS2_CURDIR}/libs/network/build/ttc +export IDRIS2_BOOT_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc:${CURDIR}/libs/network/build/ttc .PHONY: all support clean support-clean bootstrap init-bootstrap idris2-exec ${TARGET} @@ -73,8 +72,8 @@ clean-libs: ${MAKE} -C libs/contrib clean clean: clean-libs support-clean - ${IDRIS2_BOOT} --clean idris2.ipkg - rm -rf ${TARGETDIR} + -${IDRIS2_BOOT} --clean idris2.ipkg + $(RM) -r build install: install-idris2 install-support install-libs diff --git a/config.mk b/config.mk index 8f03a86b2..86d182f53 100644 --- a/config.mk +++ b/config.mk @@ -10,7 +10,7 @@ CC := clang RANLIB ?= ranlib AR ?= ar -CFLAGS := -Wall $(CFLAGS) $(OPT) +CFLAGS := -Wall $(CFLAGS) LDFLAGS := $(LDFLAGS) MACHINE := $(shell $(CC) -dumpmachine) diff --git a/libs/base/Makefile b/libs/base/Makefile index dc53bc6a6..0a609e3e4 100644 --- a/libs/base/Makefile +++ b/libs/base/Makefile @@ -5,4 +5,4 @@ install: ${IDRIS2} --install base.ipkg clean: - rm -rf build + $(RM) -r build diff --git a/libs/contrib/Makefile b/libs/contrib/Makefile index 6059f2a19..a5ea667b1 100644 --- a/libs/contrib/Makefile +++ b/libs/contrib/Makefile @@ -5,4 +5,4 @@ install: ${IDRIS2} --install contrib.ipkg clean: - rm -rf build + $(RM) -r build diff --git a/libs/network/Makefile b/libs/network/Makefile index 39a213086..5415f945d 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -1,4 +1,4 @@ -include $(IDRIS2_CURDIR)/config.mk +include ../../config.mk INSTALLDIR = `${IDRIS2} --libdir`/network/lib @@ -36,11 +36,11 @@ $(TARGET)$(SHLIB_SUFFIX): $(OBJS) .PHONY: clean clean : - rm -f $(OBJS) $(TARGET)$(SHLIB_SUFFIX) - rm -rf build + $(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX) + $(RM) -r build cleandep: clean - rm -f $(DEPS) + $(RM) $(DEPS) .PHONY: install @@ -55,4 +55,4 @@ install: test: build test.c $(CC) -o network-tests -L. -I. test.c $(TARGET)$(SHLIB_SUFFIX) LD_LIBRARY_PATH=. ./network-tests - @rm -f ./network-tests test.o + @$(RM) ./network-tests test.o diff --git a/libs/prelude/Makefile b/libs/prelude/Makefile index 9df12386a..63480597f 100644 --- a/libs/prelude/Makefile +++ b/libs/prelude/Makefile @@ -5,4 +5,4 @@ install: ${IDRIS2} --install prelude.ipkg clean: - rm -rf build + $(RM) -r build diff --git a/support/c/Makefile b/support/c/Makefile index b16a4321e..d82fcb048 100644 --- a/support/c/Makefile +++ b/support/c/Makefile @@ -1,4 +1,4 @@ -include $(IDRIS2_CURDIR)/config.mk +include ../../config.mk TARGET = libidris2_support @@ -38,10 +38,10 @@ $(DYLIBTARGET): $(OBJS) .PHONY: clean clean: - rm -f $(OBJS) $(DYLIBTARGET) $(LIBTARGET) + $(RM) $(OBJS) $(DYLIBTARGET) $(LIBTARGET) cleandep: clean - rm -f $(DEPS) + $(RM) $(DEPS) .PHONY: install From 8994e54402001a54d3e28010926d64167569b94b Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 19 May 2020 15:13:58 +0100 Subject: [PATCH 4/4] IDE mode ported I've tested this in Atom, and the vim mode also works (in both cases, just by changing the executable to point to the right place) --- README.md | 3 - idris2.ipkg | 5 +- src/Idris/IDEMode/REPL.idr | 126 +++++++++++++++++++------------------ 3 files changed, 65 insertions(+), 69 deletions(-) diff --git a/README.md b/README.md index a868d9fd8..6f110a3d7 100644 --- a/README.md +++ b/README.md @@ -9,7 +9,4 @@ There are no guarantees: This repository might move or be renamed or deleted or anything at no notice. It will eventually turn into the real Idris 2 repository, one way or another. -There's still a couple of bits and pieces that don't work (IDE mode related) -but I will get to them shortly. - Good luck :) diff --git a/idris2.ipkg b/idris2.ipkg index 0fd73e109..5af5dbb57 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -79,9 +79,6 @@ modules = Idris.REPLOpts, Idris.Resugar, Idris.SetOptions, --- Idris.Socket, --- Idris.Socket.Data, --- Idris.Socket.Raw, Idris.Syntax, Idris.Version, @@ -146,7 +143,7 @@ modules = Yaffle.Main, Yaffle.REPL -depends = contrib +depends = contrib, network sourcedir = "src" diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index fc29ba7d7..c7567f70d 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -35,19 +35,22 @@ import TTImp.ProcessDecls import Utils.Hex +import Data.List import System --- import Idris.Socket --- import Idris.Socket.Data +import Network.Socket +import Network.Socket.Data + +%foreign "C:fdopen,libc 6" +prim__fdopen : Int -> String -> PrimIO AnyPtr -{- export socketToFile : Socket -> IO (Either String File) socketToFile (MkSocket f _ _ _) = do - file <- map FHandle $ foreign FFI_C "fdopen" (Int -> String -> IO Ptr) f "r+" - if !(ferror file) then do - pure (Left "Failed to fdopen socket file descriptor") - else pure (Right file) + file <- FHandle <$> primIO (prim__fdopen f "r+") + if !(fileError file) + then pure (Left "Failed to fdopen socket file descriptor") + else pure (Right file) export initIDESocketFile : String -> Int -> IO (Either String File) @@ -57,45 +60,44 @@ initIDESocketFile h p = do Left fail => do putStrLn (show fail) putStrLn "Failed to open socket" - exit 1 + exitWith (ExitFailure 1) Right sock => do 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 - if res /= 0 - then - pure (Left ("Failed to listen on socket with error: " ++ show res)) - else do - putStrLn (show p) - res <- accept sock - case res of - Left err => - pure (Left ("Failed to accept on socket with error: " ++ show err)) - Right (s, _) => - socketToFile s + then pure (Left ("Failed to bind socket with error: " ++ show res)) + else + do res <- listen sock + if res /= 0 + then + pure (Left ("Failed to listen on socket with error: " ++ show res)) + else + do putStrLn (show p) + res <- accept sock + case res of + Left err => + pure (Left ("Failed to accept on socket with error: " ++ show err)) + Right (s, _) => + socketToFile s getChar : File -> IO Char -getChar (FHandle h) = do - if !(fEOF (FHandle h)) then do - putStrLn "Alas the file is done, aborting" - exit 1 - else do - chr <- map cast $ foreign FFI_C "fgetc" (Ptr -> IO Int) h - if !(ferror (FHandle h)) then do - putStrLn "Failed to read a character" - exit 1 - else pure chr +getChar h = do + if !(fEOF h) + then do + putStrLn "Alas the file is done, aborting" + exitWith (ExitFailure 1) + else do + Right chr <- fGetChar h + | Left err => do putStrLn "Failed to read a character" + exitWith (ExitFailure 1) + pure chr getFLine : File -> IO String -getFLine (FHandle h) = do - str <- prim_fread h - if !(ferror (FHandle h)) then do - putStrLn "Failed to read a line" - exit 1 - else pure str +getFLine h + = do Right str <- fGetLine h + | Left err => + do putStrLn "Failed to read a line" + exitWith (ExitFailure 1) + pure str getNChars : File -> Nat -> IO (List Char) getNChars i Z = pure [] @@ -114,7 +116,7 @@ getInput f do rest <- getFLine f pure (pack x ++ rest) Just num => - do inp <- getNChars f (cast num) + do inp <- getNChars f (integerToNat (cast num)) pure (pack inp) @@ -286,28 +288,28 @@ loop IDEMode idx inf outf => do inp <- coreLift $ getInput inf end <- coreLift $ fEOF inf - if end then pure () - else case parseSExp inp of - Left err => - do printIDEError outf idx ("Parse error: " ++ show err) - loop - Right sexp => - case getMsg sexp of - Just (cmd, i) => - do updateOutput i - res <- processCatch cmd - handleIDEResult outf i res - loop - Nothing => - do printIDEError outf idx ("Unrecognised command: " ++ show sexp) + if end + then pure () + else case parseSExp inp of + Left err => + do printIDEError outf idx ("Parse error: " ++ show err) loop + Right sexp => + case getMsg sexp of + Just (cmd, i) => + do updateOutput i + res <- processCatch cmd + handleIDEResult outf i res + loop + Nothing => + do printIDEError outf idx ("Unrecognised command: " ++ show sexp) + loop where updateOutput : Integer -> Core () updateOutput idx = do IDEMode _ i o <- getOutput | _ => pure () setOutput (IDEMode idx i o) - -} export replIDE : {auto c : Ref Ctxt Defs} -> @@ -316,10 +318,10 @@ replIDE : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> Core () -replIDE = throw (InternalError "Not implemented yet") --- = do res <- getOutput --- case res of --- REPL _ => printError "Running idemode but output isn't" --- IDEMode _ inf outf => do --- send outf (version 2 0) --- loop +replIDE + = do res <- getOutput + case res of + REPL _ => printError "Running idemode but output isn't" + IDEMode _ inf outf => do + send outf (version 2 0) + loop