9150698 · Idris-dev · git.iko.soy

libs/prelude/IO.idr+13−6

compare with master

unifiedsplit

@@ -11,7 +11,11 @@ data PrimIO : Type -> Type where

11 prim__IO : a -> PrimIO a

12

13||| A token representing the world, for use in `IO`

14−abstract data World = TheWorld

14+abstract data World = TheWorld prim__WorldType

15+

16+private

17+world : World -> prim__WorldType

18+world (TheWorld w) = w

15

19

16abstract WorldRes : Type -> Type

20abstract WorldRes : Type -> Type

17WorldRes x = x

21WorldRes x = x

@@ -86,11 +90,11 @@ liftPrimIO : (World -> PrimIO a) -> IO' l a

86liftPrimIO = MkIO

90liftPrimIO = MkIO

87

91

88run__IO : IO' l () -> PrimIO ()

92run__IO : IO' l () -> PrimIO ()

89−run__IO (MkIO f) = f TheWorld

93+run__IO (MkIO f) = f (TheWorld prim__TheWorld)

90

94

91unsafePerformIO : IO' ffi a -> a

95unsafePerformIO : IO' ffi a -> a

92unsafePerformIO (MkIO f) = unsafePerformPrimIO

96unsafePerformIO (MkIO f) = unsafePerformPrimIO

93− (prim_io_bind (f TheWorld) (\ b => prim_io_return b))

97+ (prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))

94

98

95--------- The C FFI

99--------- The C FFI

96

100

@@ -126,7 +130,7 @@ IO : Type -> Type

126IO = IO' FFI_C

130IO = IO' FFI_C

127

131

128run__provider : IO a -> PrimIO a

132run__provider : IO a -> PrimIO a

129−run__provider (MkIO f) = f TheWorld

133+run__provider (MkIO f) = f (TheWorld prim__TheWorld)

130

134

131prim_fork : PrimIO () -> PrimIO Ptr

135prim_fork : PrimIO () -> PrimIO Ptr

132prim_fork x = prim_io_return prim__vm -- compiled specially

136prim_fork x = prim_io_return prim__vm -- compiled specially

@@ -137,9 +141,12 @@ fork (MkIO f) = MkIO (\w => prim_io_bind

137 (\ x => prim_io_return x)))

141 (\ x => prim_io_return x)))

138 (\x => prim_io_return x))

142 (\x => prim_io_return x))

139

143

140−partial

141prim_fread : Ptr -> IO String

144prim_fread : Ptr -> IO String

142−prim_fread h = MkIO (\w => prim_io_return (prim__readString h))

145+prim_fread h = MkIO (\w => prim_io_return (prim__readString (world w) h))

146+

147+prim_fwrite : Ptr -> String -> IO Int

148+prim_fwrite h s

149+ = MkIO (\w => prim_io_return (prim__writeString (world w) h s))

143

150

144forceGC : IO ()

151forceGC : IO ()

145forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

152forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

libs/prelude/Prelude.idr+7−8

@@ -434,12 +434,11 @@ uniformB64x2 x = prim__mkB64x2 x x

434---- some basic io

435

436||| Output a string to stdout without a trailing newline

437−partial

438putStr : String -> IO ()

437putStr : String -> IO ()

439−putStr x = foreign FFI_C "putStr" (String -> IO ()) x

438+putStr x = do prim_fwrite prim__stdout x

439+ return ()

440

441||| Output a string to stdout with a trailing newline

442−partial

443putStrLn : String -> IO ()

442putStrLn : String -> IO ()

444putStrLn x = putStr (x ++ "\n")

443putStrLn x = putStr (x ++ "\n")

445

444

@@ -470,15 +469,15 @@ abstract

470data File = FHandle Ptr

469data File = FHandle Ptr

471

470

472||| Standard input

471||| Standard input

473−partial stdin : File

472+stdin : File

474stdin = FHandle prim__stdin

473stdin = FHandle prim__stdin

475

474

476||| Standard output

475||| Standard output

477−partial stdout : File

476+stdout : File

478stdout = FHandle prim__stdout

477stdout = FHandle prim__stdout

479

478

480||| Standard output

479||| Standard output

481−partial stderr : File

480+stderr : File

482stderr = FHandle prim__stderr

481stderr = FHandle prim__stderr

483

482

484||| Call the RTS's file opening function

483||| Call the RTS's file opening function

@@ -553,8 +552,8 @@ fread (FHandle h) = do_fread h

553

552

554partial

553partial

555do_fwrite : Ptr -> String -> IO ()

554do_fwrite : Ptr -> String -> IO ()

556−do_fwrite h s

555+do_fwrite h s = do prim_fwrite h s

557− = foreign FFI_C "fputStr" (Ptr -> String -> IO ()) h s

556+ return ()

558

557

559partial

558partial

560fwrite : File -> String -> IO ()

559fwrite : File -> String -> IO ()

rts/idris_stdfgn.c+6−2

@@ -32,9 +32,13 @@ int fileError(void* h) {

32 return ferror(f);

33}

34

35−void fputStr(void* h, char* str) {

35+int idris_writeStr(void* h, char* str) {

36 FILE* f = (FILE*)h;

37− fputs(str, f);

37+ if (fputs(str, f)) {

38+ return 0;

39+ } else {

40+ return -1;

41+ }

38}

42}

39

43

40int fpoll(void* h)

44int fpoll(void* h)

rts/idris_stdfgn.h+2−1

@@ -10,7 +10,8 @@ void* fileOpen(char* f, char* mode);

10void fileClose(void* h);

11int fileEOF(void* h);

12int fileError(void* h);

13+// return 0 on success

13−void fputStr(void*h, char* str);

14+int idris_writeStr(void*h, char* str);

14

15

15void* do_popen(const char* cmd, const char* mode);

16void* do_popen(const char* cmd, const char* mode);

16int fpoll(void* h);

17int fpoll(void* h);

src/IRTS/CodegenC.hs+4−3

@@ -431,9 +431,10 @@ doOp v (LIntStr (ITFixed _)) [x] = v ++ "idris_castBitsStr(vm, " ++ creg x ++ ")

431doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"

432doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"

433

434−doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

434+doOp v LReadStr [_,x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

435−doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

435+doOp v LWriteStr [_,x,s] = v ++ "MKINT((i_int)(idris_writeStr(GETPTR(" ++ creg x

436−doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"

436+ ++ "),GETSTR("

437+ ++ creg s ++ "))))"

437

438

438doOp v (LSLt (ATInt (ITFixed ty))) [x, y] = bitOp v "SLt" ty [x, y]

439doOp v (LSLt (ATInt (ITFixed ty))) [x, y] = bitOp v "SLt" ty [x, y]

439doOp v (LSLe (ATInt (ITFixed ty))) [x, y] = bitOp v "SLte" ty [x, y]

440doOp v (LSLe (ATInt (ITFixed ty))) [x, y] = bitOp v "SLte" ty [x, y]

src/IRTS/Compiler.hs+1

@@ -429,6 +429,7 @@ irTerm vs env (Proj t (-1)) = do

429 [t', LConst (BI 1)]

430

431irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i

432+irTerm vs env (Constant TheWorld) = return $ LNothing

432irTerm vs env (Constant c) = return $ LConst c

433irTerm vs env (Constant c) = return $ LConst c

433irTerm vs env (TType _) = return $ LNothing

434irTerm vs env (TType _) = return $ LNothing

434irTerm vs env Erased = return $ LNothing

435irTerm vs env Erased = return $ LNothing

src/IRTS/Lang.hs+1−1

@@ -55,7 +55,7 @@ data PrimFn = LPlus ArithTy | LMinus ArithTy | LTimes ArithTy

55 | LStrConcat | LStrLt | LStrEq | LStrLen

56 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

57 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

58− | LPrintNum | LPrintStr | LReadStr

58+ | LReadStr | LWriteStr

59 | LBitCast ArithTy ArithTy -- Only for values of equal width

60

src/Idris/Core/Binary.hs+4

@@ -317,6 +317,8 @@ instance Binary Const where

317 BufferType -> putWord8 25

318 ManagedPtrType -> putWord8 26

319 VoidType -> putWord8 27

320+ WorldType -> putWord8 28

321+ TheWorld -> putWord8 29

320 get

322 get

321 = do i <- getWord8

323 = do i <- getWord8

322 case i of

324 case i of

@@ -360,6 +362,8 @@ instance Binary Const where

360 25 -> return BufferType

362 25 -> return BufferType

361 26 -> return ManagedPtrType

363 26 -> return ManagedPtrType

362 27 -> return VoidType

364 27 -> return VoidType

365+ 28 -> return WorldType

366+ 29 -> return TheWorld

363 _ -> error "Corrupted binary data for Const"

367 _ -> error "Corrupted binary data for Const"

364

368

365

369

src/Idris/Core/DeepSeq.hs+2

@@ -145,6 +145,8 @@ instance NFData Const where

145 rnf (B32V x1) = rnf x1 `seq` ()

146 rnf (B64V x1) = rnf x1 `seq` ()

147 rnf (AType x1) = rnf x1 `seq` ()

148+ rnf WorldType = ()

149+ rnf TheWorld = ()

148 rnf StrType = ()

150 rnf StrType = ()

149 rnf PtrType = ()

151 rnf PtrType = ()

150 rnf ManagedPtrType = ()

152 rnf ManagedPtrType = ()

src/Idris/Core/Execute.hs+14−4

@@ -403,8 +403,10 @@ deNS (NS n _) = n

403deNS n = n

404

405prs = sUN "prim__readString"

406+pws = sUN "prim__writeString"

406pbm = sUN "prim__believe_me"

407pbm = sUN "prim__believe_me"

407−pstd = sUN "prim__stdin"

408+pstdin = sUN "prim__stdin"

409+pstdout = sUN "prim__stdout"

408mkfprim = sUN "mkForeignPrim"

410mkfprim = sUN "mkForeignPrim"

409pioret = sUN "prim_io_return"

411pioret = sUN "prim_io_return"

410piobind = sUN "prim_io_bind"

412piobind = sUN "prim_io_bind"

@@ -415,11 +417,19 @@ force = sUN "Force"

415-- | Look up primitive operations in the global table and transform them into ExecVal functions

417-- | Look up primitive operations in the global table and transform them into ExecVal functions

416getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

418getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

417getOp fn [_, _, x] | fn == pbm = Just (return x)

419getOp fn [_, _, x] | fn == pbm = Just (return x)

420+getOp fn [_, EP _ fn' _, EConstant (Str n)]

421+ | fn == pws && fn' == pstdout =

422+ Just $ do execIO $ putStr n

423+ return (EConstant (I 0))

418−getOp fn [EP _ fn' _]

424+getOp fn [_, EP _ fn' _]

419− | fn == prs && fn' == pstd =

425+ | fn == prs && fn' == pstdin =

420 Just $ do line <- execIO getLine

426 Just $ do line <- execIO getLine

421 return (EConstant (Str line))

427 return (EConstant (Str line))

428+getOp fn [_, EHandle h, EConstant (Str n)]

429+ | fn == prs =

430+ Just $ do execIO $ hPutStr h n

431+ return (EConstant (I 0))

422−getOp fn [EHandle h]

432+getOp fn [_, EHandle h]

423 | fn == prs =

433 | fn == prs =

424 Just $ do contents <- execIO $ hGetLine h

434 Just $ do contents <- execIO $ hGetLine h

425 return (EConstant (Str (contents ++ "\n")))

435 return (EConstant (Str (contents ++ "\n")))

src/Idris/Core/TT.hs+6

@@ -550,6 +550,7 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

550 | B8V (Vector Word8) | B16V (Vector Word16)

551 | B32V (Vector Word32) | B64V (Vector Word64)

552 | AType ArithTy | StrType

553+ | WorldType | TheWorld

554 deriving (Eq, Ord, Data, Typeable)

555 deriving (Eq, Ord, Data, Typeable)

555{-!

556{-!

@@ -562,6 +563,7 @@ isTypeConst (AType _) = True

562isTypeConst StrType = True

563isTypeConst StrType = True

563isTypeConst ManagedPtrType = True

564isTypeConst ManagedPtrType = True

564isTypeConst BufferType = True

565isTypeConst BufferType = True

566+isTypeConst WorldType = True

565isTypeConst PtrType = True

567isTypeConst PtrType = True

566isTypeConst VoidType = True

568isTypeConst VoidType = True

567isTypeConst _ = False

569isTypeConst _ = False

@@ -577,6 +579,8 @@ instance Pretty Const OutputAnnotation where

577 pretty (Str s) = text s

579 pretty (Str s) = text s

578 pretty (AType a) = pretty a

580 pretty (AType a) = pretty a

579 pretty StrType = text "String"

581 pretty StrType = text "String"

582+ pretty TheWorld = text "%theWorld"

583+ pretty WorldType = text "prim__World"

580 pretty BufferType = text "prim__UnsafeBuffer"

584 pretty BufferType = text "prim__UnsafeBuffer"

581 pretty PtrType = text "Ptr"

585 pretty PtrType = text "Ptr"

582 pretty ManagedPtrType = text "Ptr"

586 pretty ManagedPtrType = text "Ptr"

@@ -1266,6 +1270,8 @@ instance Show Const where

1266 show (AType (ATInt ITChar)) = "Char"

1270 show (AType (ATInt ITChar)) = "Char"

1267 show (AType (ATInt (ITFixed it))) = itBitsName it

1271 show (AType (ATInt (ITFixed it))) = itBitsName it

1268 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

1272 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

1273+ show TheWorld = "prim__TheWorld"

1274+ show WorldType = "prim__WorldType"

1269 show StrType = "String"

1275 show StrType = "String"

1270 show BufferType = "prim__UnsafeBuffer"

1276 show BufferType = "prim__UnsafeBuffer"

1271 show PtrType = "Ptr"

1277 show PtrType = "Ptr"

src/Idris/Core/Typecheck.hs+1

@@ -129,6 +129,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

129 constType (B16V a) = Constant (AType (ATInt (ITVec IT16 (V.length a))))

130 constType (B32V a) = Constant (AType (ATInt (ITVec IT32 (V.length a))))

131 constType (B64V a) = Constant (AType (ATInt (ITVec IT64 (V.length a))))

132+ constType TheWorld = Constant WorldType

132 constType Forgot = Erased

133 constType Forgot = Erased

133 constType _ = TType (UVal 0)

134 constType _ = TType (UVal 0)

134 chk u env (RForce t) = do (_, ty) <- chk u env t

135 chk u env (RForce t) = do (_, ty) <- chk u env t

src/Idris/ParseExpr.hs+2

@@ -1150,6 +1150,8 @@ constants =

1150 , ("String", StrType)

1151 , ("Ptr", PtrType)

1152 , ("ManagedPtr", ManagedPtrType)

1153+ , ("prim__WorldType", WorldType)

1154+ , ("prim__TheWorld", TheWorld)

1153 , ("prim__UnsafeBuffer", BufferType)

1155 , ("prim__UnsafeBuffer", BufferType)

1154 , ("Bits8", AType (ATInt (ITFixed IT8)))

1156 , ("Bits8", AType (ATInt (ITFixed IT8)))

1155 , ("Bits16", AType (ATInt (ITFixed IT16)))

1157 , ("Bits16", AType (ATInt (ITFixed IT16)))

src/Idris/Primitives.hs+7−5

@@ -166,17 +166,19 @@ primitives =

166 (2, LStrIndex) partial,

167 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

168 (1, LStrRev) total,

169− Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

169+ Prim (sUN "prim__readString") (ty [WorldType,PtrType] StrType) 2 (p_cantreduce)

170− (1, LReadStr) iopartial,

170+ (2, LReadStr) total, -- total is okay, because we have 'WorldType'

171+ Prim (sUN "prim__writeString") (ty [WorldType,PtrType,StrType] (AType (ATInt ITNative))) 3 (p_cantreduce)

172+ (3, LWriteStr) total,

171 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

173 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

172 (0, LVMPtr) total,

174 (0, LVMPtr) total,

173 -- Streams

175 -- Streams

174 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

176 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

175− (0, LStdIn) iopartial,

177+ (0, LStdIn) total,

176 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

178 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

177− (0, LStdOut) iopartial,

179+ (0, LStdOut) total,

178 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

180 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

179− (0, LStdErr) iopartial,

181+ (0, LStdErr) total,

180 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

182 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

181 (0, LNullPtr) total,

183 (0, LNullPtr) total,

182 -- Managed pointer registration

184 -- Managed pointer registration

test/ffi004/test026.idr−1

@@ -29,4 +29,3 @@ testFoo = foo

29

30testBar : Nat

31testBar = bar

32−