Merge branch 'master' into fix_win

.gitignore

@@ -7,19 +7,13 @@
 *.a
 *.dll
 
-*.dSYM
-
 /build
 
-/dist/idris2.c
-
-/docs/build/
-
 /libs/**/build
 
-/src/IdrisPaths.idr
-
 /tests/**/output
 /tests/**/*.so
 /tests/**/*.dylib
 /tests/**/*.dll
+
+/src/IdrisPaths.idr

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
 

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

bootstrap/idris2sh_app/idris2sh.ss

@@ -266,6 +266,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)))

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)

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"
 

libs/base/Makefile

@@ -5,4 +5,4 @@ install:
 	${IDRIS2} --install base.ipkg
 
 clean:
-	rm -rf build
+	$(RM) -r build

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)

libs/contrib/Makefile

@@ -5,4 +5,4 @@ install:
 	${IDRIS2} --install contrib.ipkg
 
 clean:
-	rm -rf build
+	$(RM) -r build

libs/network/.gitignore

@@ -3,6 +3,8 @@
 *.d
 *.o
 *.obj
+*.a
+*.lib
 *.so
 *.dylib
 *.dll

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

libs/prelude/Makefile

@@ -5,4 +5,4 @@ install:
 	${IDRIS2} --install prelude.ipkg
 
 clean:
-	rm -rf build
+	$(RM) -r build

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

support/c/.gitignore

@@ -0,0 +1,8 @@
+*.d
+*.o
+*.obj
+*.a
+*.lib
+*.so
+*.dylib
+*.dll

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

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