Merge branch 'master' into fix-makefiles

libs/base/System/File.idr

@@ -32,6 +32,8 @@ prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
 prim__writeLine : FilePtr -> String -> PrimIO Int
 %foreign support "idris2_eof"
 prim__eof : FilePtr -> PrimIO Int
+%foreign "C:fflush,libc"
+prim__flush : FilePtr -> PrimIO Int
 
 %foreign support "idris2_fileRemove"
 prim__fileRemove : String -> PrimIO Int
@@ -155,6 +157,12 @@ fEOF (FHandle f)
     = do res <- primIO (prim__eof f)
          pure (res /= 0)
 
+export
+fflush : (h : File) -> IO ()
+fflush (FHandle f)
+    = do primIO (prim__flush f)
+         pure ()
+
 export
 fileAccessTime : (h : File) -> IO (Either FileError Int)
 fileAccessTime (FHandle f)

libs/base/System/REPL.idr

@@ -11,11 +11,12 @@ export
 replWith : (state : a) -> (prompt : String) ->
            (onInput : a -> String -> Maybe (String, a)) -> IO ()
 replWith acc prompt fn
-   = do putStr prompt
-        eof <- fEOF stdin
+   = do eof <- fEOF stdin
         if eof
           then pure ()
-          else do x <- getLine
+          else do putStr prompt
+                  fflush stdout
+                  x <- getLine
                   case fn acc x of
                        Just (out, acc') =>
                            do putStr out

libs/prelude/PrimIO.idr

@@ -41,9 +41,9 @@ io_bind (MkIO fn) k
                       MkIO res = k x' in
                       res w')
 
-%extern prim__putStr : String -> (1 x : %World) -> IORes ()
-%extern prim__getStr : (1 x : %World) -> IORes String
-%extern prim__putChar : Char -> (1 x : %World) -> IORes ()
+%foreign "C:putchar,libc"
+prim__putChar : Char -> (1 x : %World) -> IORes ()
+%foreign "C:getchar,libc"
 %extern prim__getChar : (1 x : %World) -> IORes Char
 
 -- A pointer representing a given parameter type
@@ -85,6 +85,26 @@ export %inline
 cCall : (ret : Type) -> String -> FArgList -> IO ret
 cCall ret fn args = primIO (prim__cCall ret fn args)
 
+%foreign "C:idris2_isNull, libidris2_support"
+export
+prim__nullAnyPtr : AnyPtr -> Int
+
+prim__forgetPtr : Ptr t -> AnyPtr
+prim__forgetPtr = believe_me
+
+export %inline
+prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
+prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)
+
+%foreign "C:idris2_getString, libidris2_support"
+export
+prim__getString : Ptr String -> String
+
+%foreign "C:idris2_getStr,libidris2_support"
+prim__getStr : PrimIO String
+%foreign "C:idris2_putStr,libidris2_support"
+prim__putStr : String -> PrimIO ()
+
 ||| Output a string to stdout without a trailing newline.
 export
 putStr : String -> IO ()
@@ -123,21 +143,6 @@ export
 prim_fork : (1 prog : PrimIO ()) -> PrimIO ThreadID
 prim_fork act w = prim__schemeCall ThreadID "blodwen-thread" [act] w
 
-%foreign "C:idris2_isNull, libidris2_support"
-export
-prim__nullAnyPtr : AnyPtr -> Int
-
-prim__forgetPtr : Ptr t -> AnyPtr
-prim__forgetPtr = believe_me
-
-export %inline
-prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
-prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)
-
-%foreign "C:idris2_getString, libidris2_support"
-export
-prim__getString : Ptr String -> String
-
 %foreign "C:idris2_readString, libidris2_support"
 export
 prim__getErrno : Int

src/Compiler/Scheme/Common.idr

@@ -160,7 +160,6 @@ schOp BelieveMe [_,_,x] = x
 ||| Extended primitives for the scheme backend, outside the standard set of primFn
 public export
 data ExtPrim = CCall | SchemeCall
-             | PutStr | GetStr | PutChar | GetChar
              | NewIORef | ReadIORef | WriteIORef
              | NewArray | ArrayGet | ArraySet
              | GetField | SetField
@@ -172,10 +171,6 @@ export
 Show ExtPrim where
   show CCall = "CCall"
   show SchemeCall = "SchemeCall"
-  show PutStr = "PutStr"
-  show GetStr = "GetStr"
-  show PutChar = "PutChar"
-  show GetChar = "GetChar"
   show NewIORef = "NewIORef"
   show ReadIORef = "ReadIORef"
   show WriteIORef = "WriteIORef"
@@ -194,10 +189,6 @@ toPrim : Name -> ExtPrim
 toPrim pn@(NS _ n)
     = cond [(n == UN "prim__schemeCall", SchemeCall),
             (n == UN "prim__cCall", CCall),
-            (n == UN "prim__putStr", PutStr),
-            (n == UN "prim__getStr", GetStr),
-            (n == UN "prim__putChar", PutChar),
-            (n == UN "prim__getChar", GetChar),
             (n == UN "prim__newIORef", NewIORef),
             (n == UN "prim__readIORef", ReadIORef),
             (n == UN "prim__writeIORef", WriteIORef),
@@ -405,14 +396,6 @@ parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
   schExtCommon i SchemeCall [ret, fn, args, world]
        = pure $ mkWorld ("(apply (eval (string->symbol " ++ !(schExp i fn) ++")) "
                     ++ !(readArgs i args) ++ ")")
-  schExtCommon i PutStr [arg, world]
-      = pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit
-  schExtCommon i GetStr [world]
-      = pure $ mkWorld "(blodwen-get-line (current-input-port))"
-  schExtCommon i PutChar [arg, world]
-      = pure $ "(begin (display " ++ !(schExp i arg) ++ ") " ++ mkWorld (schConstructor 0 []) ++ ")" -- code for MkUnit
-  schExtCommon i GetChar [world]
-      = pure $ mkWorld "(blodwen-get-char (current-input-port))"
   schExtCommon i NewIORef [_, val, world]
       = pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")"
   schExtCommon i ReadIORef [_, ref, world]

support/c/idris_support.c

@@ -1,6 +1,9 @@
 #include "idris_support.h"
-#include <string.h>
+#include "idris_file.h"
+
 #include <errno.h>
+#include <stdio.h>
+#include <string.h>
 #include <time.h>
 
 int idris2_isNull(void* ptr) {
@@ -15,6 +18,22 @@ int idris2_getErrno() {
     return errno;
 }
 
+char* idris2_getStr() {
+    char *inp = idris2_readLine(stdin);
+    // Remove trailing newline; easier to do this than in PrimIO which
+    // doesn't have the relevant functions available yet
+    for(char *c = inp; *c != '\0'; ++c) {
+        if (*c == '\n' || *c == '\r') {
+            *c = '\0';
+        }
+    }
+    return inp;
+}
+
+void idris2_putStr(char* f) {
+    idris2_writeLine(stdout, f);
+}
+
 void idris2_sleep(int sec) {
     struct timespec t;
     t.tv_sec = sec;

support/c/idris_support.h

@@ -8,6 +8,9 @@ int idris2_isNull(void*);
 char* idris2_getString(void *p);
 int idris2_getErrno();
 
+char* idris2_getStr();
+void idris2_putStr(char* f);
+
 void idris2_sleep(int sec);
 void idris2_usleep(int usec);
 int idris2_time();

tests/Main.idr

@@ -34,7 +34,7 @@ idrisTests
        "basic021", "basic022", "basic023", "basic024", "basic025",
        "basic026", "basic027", "basic028", "basic029", "basic030",
        "basic031", "basic032", "basic033", "basic034", "basic035",
-       "basic036", "basic037", "basic038",
+       "basic036", "basic037", "basic038", "basic039",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006",
@@ -98,7 +98,7 @@ chezTests : List String
 chezTests
    = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
-      "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
+      "chez013", "chez014", "chez015", "chez016",            "chez018",
       "reg001"]
 
 ideModeTests : List String

tests/chez/chez013/expected

@@ -1,5 +1,5 @@
+Made it!
 (40, 30)
 "Here": (40, 30)
-Made it!
 1/1: Building Struct (Struct.idr)
 Main> Main> Bye for now!

tests/chez/chez017/Main.idr

@@ -1,19 +0,0 @@
-module Main
-
-data Foo : Type where
-  MkFoo : String -> Foo
-
-data Bar : Type where
-  [noNewtype]
-  MkBar : String -> Bar
-
-
--- This code rely on the fact that `putStr` calls the Chez function `display`,
--- which allows any value to be printed. This will expose the internal
--- structure of each data type.
-main : IO ()
-main = do
-  putStr (believe_me (MkFoo "foo"))
-  putChar '\n'
-  putStr (believe_me (MkBar "bar"))
-  putChar '\n'

tests/chez/chez017/expected

@@ -1,4 +0,0 @@
-foo
-#(0 bar)
-1/1: Building Main (Main.idr)
-Main> Main> Bye for now!

tests/chez/chez017/input

@@ -1,2 +0,0 @@
-:exec main
-:q

tests/idris2/basic039/Main.idr

@@ -0,0 +1,10 @@
+module Main
+
+-- Using :di we can see the internal structure. MkFoo should be a newtype,
+-- MkBar not
+data Foo : Type where
+  MkFoo : String -> Foo
+
+data Bar : Type where
+  [noNewtype]
+  MkBar : String -> Bar

tests/idris2/basic039/expected

@@ -0,0 +1,18 @@
+1/1: Building Main (Main.idr)
+Main> Main.MkFoo ==> DataCon 0 1 (newtype by (False, 0))
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Refers to: []
+Refers to (runtime): []
+Main> Main.MkBar ==> DataCon 0 1
+RigW
+Erasable args: []
+Detaggable arg types: []
+Specialise args: []
+Inferrable args: []
+Refers to: []
+Refers to (runtime): []
+Main> Bye for now!

tests/idris2/basic039/input

@@ -0,0 +1,3 @@
+:di MkFoo
+:di MkBar
+:q