diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index b024254..1c71d6a 100644 --- a/libs/base/System/File.idr +++ b/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) diff --git a/libs/base/System/REPL.idr b/libs/base/System/REPL.idr index 844bf43..26e8a9b 100644 --- a/libs/base/System/REPL.idr +++ b/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 diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 15e8db8..3772841 100644 --- a/libs/prelude/PrimIO.idr +++ b/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 diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 79cb84a..45910be 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/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] diff --git a/support/c/idris_support.c b/support/c/idris_support.c index d25ca59..5898593 100644 --- a/support/c/idris_support.c +++ b/support/c/idris_support.c @@ -1,6 +1,9 @@ #include "idris_support.h" -#include +#include "idris_file.h" + #include +#include +#include #include 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; diff --git a/support/c/idris_support.h b/support/c/idris_support.h index d8d7307..1e510a6 100644 --- a/support/c/idris_support.h +++ b/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(); diff --git a/tests/Main.idr b/tests/Main.idr index 6415cbf..995c753 100644 --- a/tests/Main.idr +++ b/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 diff --git a/tests/chez/chez013/expected b/tests/chez/chez013/expected index d087ee1..2d04a64 100644 --- a/tests/chez/chez013/expected +++ b/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! diff --git a/tests/chez/chez017/Main.idr b/tests/chez/chez017/Main.idr deleted file mode 100644 index 6ee5aac..0000000 --- a/tests/chez/chez017/Main.idr +++ /dev/null @@ -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' diff --git a/tests/chez/chez017/expected b/tests/chez/chez017/expected deleted file mode 100644 index 66fb782..0000000 --- a/tests/chez/chez017/expected +++ /dev/null @@ -1,4 +0,0 @@ -foo -#(0 bar) -1/1: Building Main (Main.idr) -Main> Main> Bye for now! diff --git a/tests/chez/chez017/input b/tests/chez/chez017/input deleted file mode 100644 index fc5992c..0000000 --- a/tests/chez/chez017/input +++ /dev/null @@ -1,2 +0,0 @@ -:exec main -:q diff --git a/tests/idris2/basic039/Main.idr b/tests/idris2/basic039/Main.idr new file mode 100644 index 0000000..6d45d43 --- /dev/null +++ b/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 diff --git a/tests/idris2/basic039/expected b/tests/idris2/basic039/expected new file mode 100644 index 0000000..06b06db --- /dev/null +++ b/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! diff --git a/tests/idris2/basic039/input b/tests/idris2/basic039/input new file mode 100644 index 0000000..996da9c --- /dev/null +++ b/tests/idris2/basic039/input @@ -0,0 +1,3 @@ +:di MkFoo +:di MkBar +:q diff --git a/tests/chez/chez017/run b/tests/idris2/basic039/run similarity index 100% rename from tests/chez/chez017/run rename to tests/idris2/basic039/run