9150698 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Primitive type for world state

This means we can make primitives for reading/writing file handles which are given the world state, so can be written more safely. Also, a minimal back end can implement these rather than implementing an entire FFI. Updated primitive LReadStr (which can now reasonably be total, like any foreign function, because it has a world state) and added primitive LWriteStr.

commit91506984286deccac4bd4758e9bade271c1ae9c3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 18 Jan 2015, 00:14 (12 years ago) parentd5377be

15 files changed+70−31

compare with master

unifiedsplit

libs/prelude/IO.idr+13−6 libs/prelude/Prelude.idr+7−8 rts/idris_stdfgn.c+6−2 rts/idris_stdfgn.h+2−1 src/IRTS/CodegenC.hs+4−3 src/IRTS/Compiler.hs+1 src/IRTS/Lang.hs+1−1 src/Idris/Core/Binary.hs+4 src/Idris/Core/DeepSeq.hs+2 src/Idris/Core/Execute.hs+14−4 src/Idris/Core/TT.hs+6 src/Idris/Core/Typecheck.hs+1 src/Idris/ParseExpr.hs+2 src/Idris/Primitives.hs+7−5 test/ffi004/test026.idr−1

libs/prelude/IO.idr+13−6

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

1111 prim__IO : a -> PrimIO a

1212

1313||| 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

1519

1620abstract WorldRes : Type -> Type

1721WorldRes x = x

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

8690liftPrimIO = MkIO

8791

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

89−run__IO (MkIO f) = f TheWorld

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

9094

9195unsafePerformIO : IO' ffi a -> a

9296unsafePerformIO (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))

9498

9599--------- The C FFI

96100

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

126130IO = IO' FFI_C

127131

128132run__provider : IO a -> PrimIO a

129−run__provider (MkIO f) = f TheWorld

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

130134

131135prim_fork : PrimIO () -> PrimIO Ptr

132136prim_fork x = prim_io_return prim__vm -- compiled specially

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

137141 (\ x => prim_io_return x)))

138142 (\x => prim_io_return x))

139143

140−partial

141144prim_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))

143150

144151forceGC : IO ()

145152forceGC = 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

434434---- some basic io

435435

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

437−partial

438437putStr : String -> IO ()

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

438+putStr x = do prim_fwrite prim__stdout x

439+ return ()

440440

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

442−partial

443442putStrLn : String -> IO ()

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

445444

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

470469data File = FHandle Ptr

471470

472471||| Standard input

473−partial stdin : File

472+stdin : File

474473stdin = FHandle prim__stdin

475474

476475||| Standard output

477−partial stdout : File

476+stdout : File

478477stdout = FHandle prim__stdout

479478

480479||| Standard output

481−partial stderr : File

480+stderr : File

482481stderr = FHandle prim__stderr

483482

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

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

553552

554553partial

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

556−do_fwrite h s

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

555+do_fwrite h s = do prim_fwrite h s

556+ return ()

558557

559558partial

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

rts/idris_stdfgn.c+6−2

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

3232 return ferror(f);

3333}

3434

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

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

3636 FILE* f = (FILE*)h;

37− fputs(str, f);

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

38+ return 0;

39+ } else {

40+ return -1;

41+ }

3842}

3943

4044int fpoll(void* h)

rts/idris_stdfgn.h+2−1

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

1010void fileClose(void* h);

1111int fileEOF(void* h);

1212int fileError(void* h);

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

13+// return 0 on success

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

1415

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

1617int fpoll(void* h);

src/IRTS/CodegenC.hs+4−3

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

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

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

433433

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

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

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

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

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

436+ ++ "),GETSTR("

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

437438

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

439440doOp 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

429429 [t', LConst (BI 1)]

430430

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

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

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

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

434435irTerm vs env Erased = return $ LNothing

src/IRTS/Lang.hs+1−1

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

5555 | LStrConcat | LStrLt | LStrEq | LStrLen

5656 | LIntFloat IntTy | LFloatInt IntTy | LIntStr IntTy | LStrInt IntTy

5757 | LFloatStr | LStrFloat | LChInt IntTy | LIntCh IntTy

58− | LPrintNum | LPrintStr | LReadStr

58+ | LReadStr | LWriteStr

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

6060

src/Idris/Core/Binary.hs+4

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

317317 BufferType -> putWord8 25

318318 ManagedPtrType -> putWord8 26

319319 VoidType -> putWord8 27

320+ WorldType -> putWord8 28

321+ TheWorld -> putWord8 29

320322 get

321323 = do i <- getWord8

322324 case i of

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

360362 25 -> return BufferType

361363 26 -> return ManagedPtrType

362364 27 -> return VoidType

365+ 28 -> return WorldType

366+ 29 -> return TheWorld

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

364368

365369

src/Idris/Core/DeepSeq.hs+2

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

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

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

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

148+ rnf WorldType = ()

149+ rnf TheWorld = ()

148150 rnf StrType = ()

149151 rnf PtrType = ()

150152 rnf ManagedPtrType = ()

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

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

403403deNS n = n

404404

405405prs = sUN "prim__readString"

406+pws = sUN "prim__writeString"

406407pbm = sUN "prim__believe_me"

407−pstd = sUN "prim__stdin"

408+pstdin = sUN "prim__stdin"

409+pstdout = sUN "prim__stdout"

408410mkfprim = sUN "mkForeignPrim"

409411pioret = sUN "prim_io_return"

410412piobind = sUN "prim_io_bind"

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

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

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

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

418−getOp fn [EP _ fn' _]

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

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

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

422+ Just $ do execIO $ putStr n

423+ return (EConstant (I 0))

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

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

420426 Just $ do line <- execIO getLine

421427 return (EConstant (Str line))

422−getOp fn [EHandle h]

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

429+ | fn == prs =

430+ Just $ do execIO $ hPutStr h n

431+ return (EConstant (I 0))

432+getOp fn [_, EHandle h]

423433 | fn == prs =

424434 Just $ do contents <- execIO $ hGetLine h

425435 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

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

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

552552 | AType ArithTy | StrType

553+ | WorldType | TheWorld

554555 deriving (Eq, Ord, Data, Typeable)

555556{-!

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

562563isTypeConst StrType = True

563564isTypeConst ManagedPtrType = True

564565isTypeConst BufferType = True

566+isTypeConst WorldType = True

565567isTypeConst PtrType = True

566568isTypeConst VoidType = True

567569isTypeConst _ = False

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

577579 pretty (Str s) = text s

578580 pretty (AType a) = pretty a

579581 pretty StrType = text "String"

582+ pretty TheWorld = text "%theWorld"

583+ pretty WorldType = text "prim__World"

580584 pretty BufferType = text "prim__UnsafeBuffer"

581585 pretty PtrType = text "Ptr"

582586 pretty ManagedPtrType = text "Ptr"

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

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

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

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

1273+ show TheWorld = "prim__TheWorld"

1274+ show WorldType = "prim__WorldType"

12691275 show StrType = "String"

12701276 show BufferType = "prim__UnsafeBuffer"

12711277 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

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

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

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

132+ constType TheWorld = Constant WorldType

132133 constType Forgot = Erased

133134 constType _ = TType (UVal 0)

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

src/Idris/ParseExpr.hs+2

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

11501150 , ("String", StrType)

11511151 , ("Ptr", PtrType)

11521152 , ("ManagedPtr", ManagedPtrType)

1153+ , ("prim__WorldType", WorldType)

1154+ , ("prim__TheWorld", TheWorld)

11531155 , ("prim__UnsafeBuffer", BufferType)

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

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

src/Idris/Primitives.hs+7−5

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

166166 (2, LStrIndex) partial,

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

168168 (1, LStrRev) total,

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

170− (1, LReadStr) iopartial,

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

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,

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

172174 (0, LVMPtr) total,

173175 -- Streams

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

175− (0, LStdIn) iopartial,

177+ (0, LStdIn) total,

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

177− (0, LStdOut) iopartial,

179+ (0, LStdOut) total,

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

179− (0, LStdErr) iopartial,

181+ (0, LStdErr) total,

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

181183 (0, LNullPtr) total,

182184 -- Managed pointer registration

test/ffi004/test026.idr−1

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

2929

3030testBar : Nat

3131testBar = bar

32−