mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Move putChar, getChar etc primitives to C
Back ends can still shortcut these and use their own primitives, but doing things this way gives consistent behaviour between the simple IO primitives and file IO, and allow us to use stdin/stdout consistently (e.g. to flush stdout). This also fixes the behaviour of 'replWith' to be consistent with the Idris 1 version.
This commit is contained in:
parent
a451dcd171
commit
1b36dd99b1
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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]
|
||||
|
@ -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;
|
||||
|
@ -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();
|
||||
|
@ -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
|
||||
|
@ -1,5 +1,5 @@
|
||||
Made it!
|
||||
(40, 30)
|
||||
"Here": (40, 30)
|
||||
Made it!
|
||||
1/1: Building Struct (Struct.idr)
|
||||
Main> Main> Bye for now!
|
||||
|
@ -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'
|
@ -1,4 +0,0 @@
|
||||
foo
|
||||
#(0 bar)
|
||||
1/1: Building Main (Main.idr)
|
||||
Main> Main> Bye for now!
|
@ -1,2 +0,0 @@
|
||||
:exec main
|
||||
:q
|
10
tests/idris2/basic039/Main.idr
Normal file
10
tests/idris2/basic039/Main.idr
Normal file
@ -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
|
18
tests/idris2/basic039/expected
Normal file
18
tests/idris2/basic039/expected
Normal file
@ -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!
|
3
tests/idris2/basic039/input
Normal file
3
tests/idris2/basic039/input
Normal file
@ -0,0 +1,3 @@
|
||||
:di MkFoo
|
||||
:di MkBar
|
||||
:q
|
Loading…
Reference in New Issue
Block a user