6f0aff3 · Idris-dev · git.iko.soy

libs/base/Control/Monad/Identity.idr+6−1

compare with master

unifiedsplit

@@ -1,8 +1,13 @@

1module Control.Monad.Identity

2−

2+{-

3public record Identity : Type -> Type where

4 Id : (runIdentity : a) -> Identity a

5+-}

5

6

7+public record Identity (a : Type) where

8+ runIdentity : a

9+ constructor Id

10+

6instance Functor Identity where

11instance Functor Identity where

7 map fn (Id a) = Id (fn a)

12 map fn (Id a) = Id (fn a)

8

13

libs/base/Control/Monad/RWS.idr+5−1

@@ -11,10 +11,14 @@ import Control.Monad.Reader

11class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}

12

13||| The transformer on which the RWS monad is based

14+record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where

15+ runRWST : r -> s -> m (a, s, w)

16+

17+{-

14record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where

18record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where

15 MkRWST : {m : Type -> Type} ->

19 MkRWST : {m : Type -> Type} ->

16 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a

20 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a

17−

21+-}

18instance Monad m => Functor (RWST r w s m) where

22instance Monad m => Functor (RWST r w s m) where

19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

23 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

20 return (f a, s', w)

24 return (f a, s', w)

libs/base/Control/Monad/Reader.idr+6−1

@@ -14,10 +14,15 @@ class Monad m => MonadReader r (m : Type -> Type) where

14 local : (r -> r) -> m a -> m a

15

16||| The transformer on which the Reader monad is based

17+record ReaderT (r : Type) (m : Type -> Type) (a : Type) where

18+ runReaderT : r -> m a

19+ constructor RD

20+

21+{-

17record ReaderT : Type -> (Type -> Type) -> Type -> Type where

22record ReaderT : Type -> (Type -> Type) -> Type -> Type where

18 RD : {m : Type -> Type} ->

23 RD : {m : Type -> Type} ->

19 (runReaderT : r -> m a) -> ReaderT r m a

24 (runReaderT : r -> m a) -> ReaderT r m a

20−

25+-}

21||| Create a ReaderT with an empty context

26||| Create a ReaderT with an empty context

22liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a

27liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a

23liftReaderT m = RD $ const m

28liftReaderT m = RD $ const m

libs/base/Control/Monad/State.idr+5−1

@@ -13,10 +13,14 @@ class Monad m => MonadState s (m : Type -> Type) where

13 put : s -> m ()

14

15||| The transformer on which the State monad is based

16+record StateT (s : Type) (m : Type -> Type) (a : Type) where

17+ runStateT : s -> m (a, s)

18+ constructor ST

19+{-

16record StateT : Type -> (Type -> Type) -> Type -> Type where

20record StateT : Type -> (Type -> Type) -> Type -> Type where

17 ST : {m : Type -> Type} ->

21 ST : {m : Type -> Type} ->

18 (runStateT : s -> m (a, s)) -> StateT s m a

22 (runStateT : s -> m (a, s)) -> StateT s m a

19−

23+-}

20instance Functor f => Functor (StateT s f) where

24instance Functor f => Functor (StateT s f) where

21 map f (ST g) = ST (\st => map (mapFst f) (g st)) where

25 map f (ST g) = ST (\st => map (mapFst f) (g st)) where

22 mapFst : (a -> x) -> (a, s) -> (x, s)

26 mapFst : (a -> x) -> (a, s) -> (x, s)

libs/base/Control/Monad/Writer.idr+6

@@ -16,9 +16,15 @@ class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where

16 pass : m (a, w -> w) -> m a

17

18||| The transformer base of the Writer monad

19+record WriterT (w : Type) (m : Type -> Type) (a : Type) where

20+ runWriterT : m (a, w)

21+ constructor WR

22+

23+{-

19record WriterT : Type -> (Type -> Type) -> Type -> Type where

24record WriterT : Type -> (Type -> Type) -> Type -> Type where

20 WR : {m : Type -> Type} ->

25 WR : {m : Type -> Type} ->

21 (runWriterT : m (a, w)) -> WriterT w m a

26 (runWriterT : m (a, w)) -> WriterT w m a

27+-}

22

28

23instance Functor f => Functor (WriterT w f) where

29instance Functor f => Functor (WriterT w f) where

24 map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g

30 map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g

libs/base/Data/Buffer.idr+5

@@ -27,8 +27,13 @@ import Data.Fin

27

28||| A contiguous chunk of n bytes

29abstract

30+record Buffer (n : Nat) where

31+ offset : Nat

32+ realBufer : prim__UnsafeBuffer

33+{-

30record Buffer : Nat -> Type where

34record Buffer : Nat -> Type where

31 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n

35 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n

36+-}

32

37

33bitsFromNat : Nat -> Bits64

38bitsFromNat : Nat -> Bits64

34bitsFromNat Z = 0

39bitsFromNat Z = 0

libs/base/Network/Cgi.idr+11

@@ -8,6 +8,16 @@ public

8Vars : Type

9Vars = List (String, String)

10

11+record CGIInfo where

12+ GET : Vars

13+ POST : Vars

14+ Cookies : Vars

15+ UserAgent : String

16+ Headers : String

17+ Output : String

18+ constructor CGISt

19+

20+{-

11record CGIInfo : Type where

21record CGIInfo : Type where

12 CGISt : (GET : Vars) ->

22 CGISt : (GET : Vars) ->

13 (POST : Vars) ->

23 (POST : Vars) ->

@@ -15,6 +25,7 @@ record CGIInfo : Type where

15 (UserAgent : String) ->

25 (UserAgent : String) ->

16 (Headers : String) ->

26 (Headers : String) ->

17 (Output : String) -> CGIInfo

27 (Output : String) -> CGIInfo

28+-}

18

29

19add_Headers : String -> CGIInfo -> CGIInfo

30add_Headers : String -> CGIInfo -> CGIInfo

20add_Headers str st = record { Headers = Headers st ++ str } st

31add_Headers str st = record { Headers = Headers st ++ str } st

libs/base/Network/Socket.idr+22−2

@@ -107,6 +107,13 @@ EAGAIN : Int

107EAGAIN = 11

108

109-- TODO: Expand to non-string payloads

110+record UDPRecvData where

111+ remote_addr : SocketAddress

112+ remote_port : Port

113+ recv_data : String

114+ data_len : Int

115+

116+{-

110record UDPRecvData : Type where

117record UDPRecvData : Type where

111 MkUDPRecvData :

118 MkUDPRecvData :

112 (remote_addr : SocketAddress) ->

119 (remote_addr : SocketAddress) ->

@@ -114,13 +121,19 @@ record UDPRecvData : Type where

114 (recv_data : String) ->

121 (recv_data : String) ->

115 (data_len : Int) ->

122 (data_len : Int) ->

116 UDPRecvData

123 UDPRecvData

124+-}

117

125

126+record UDPAddrInfo where

127+ remote_addr : SocketAddress

128+ remote_port : Port

129+

130+{-

118record UDPAddrInfo : Type where

131record UDPAddrInfo : Type where

119 MkUDPAddrInfo :

132 MkUDPAddrInfo :

120 (remote_addr : SocketAddress) ->

133 (remote_addr : SocketAddress) ->

121 (remote_port : Port) ->

134 (remote_port : Port) ->

122 UDPAddrInfo

135 UDPAddrInfo

123−

136+-}

124||| Frees a given pointer

137||| Frees a given pointer

125public

138public

126sock_free : BufPtr -> IO ()

139sock_free : BufPtr -> IO ()

@@ -138,13 +151,20 @@ sock_alloc : ByteLength -> IO BufPtr

138sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl

151sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl

139

152

140||| The metadata about a socket

153||| The metadata about a socket

154+record Socket where

155+ descriptor : SocketDescriptor

156+ family : SocketFamily

157+ socketType : SocketType

158+ protocalNumber : ProtocolNumber

159+

160+{-

141record Socket : Type where

161record Socket : Type where

142 MkSocket : (descriptor : SocketDescriptor) ->

162 MkSocket : (descriptor : SocketDescriptor) ->

143 (family : SocketFamily) ->

163 (family : SocketFamily) ->

144 (socketType : SocketType) ->

164 (socketType : SocketType) ->

145 (protocolNumber : ProtocolNumber) ->

165 (protocolNumber : ProtocolNumber) ->

146 Socket

166 Socket

147−

167+-}

148||| Get the C error number

168||| Get the C error number

149getErrno : IO Int

169getErrno : IO Int

150getErrno = foreign FFI_C "idrnet_errno" (IO Int)

170getErrno = foreign FFI_C "idrnet_errno" (IO Int)

libs/prelude/IO.idr+6−1

@@ -20,9 +20,14 @@ world (TheWorld w) = w

20abstract WorldRes : Type -> Type

21WorldRes x = x

22

23+record FFI where

24+ ffi_types : Type -> Type

25+ ffi_fn : Type

26+ constructor MkFFI

27+{-

23record FFI : Type where

28record FFI : Type where

24 MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI

29 MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI

25−

30+-}

26abstract

31abstract

27data IO' : (lang : FFI) -> Type -> Type where

32data IO' : (lang : FFI) -> Type -> Type where

28 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

33 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a

libs/prelude/Prelude/Nat.idr+19−2

@@ -199,13 +199,30 @@ instance Cast Integer Nat where

199 cast = fromInteger

200

201||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

202−record Multiplicative : Type where

202+data Multiplicative : Type where

203 getMultiplicative : Nat -> Multiplicative

204

205+{-

206+record Multiplicative where

207+ multiplicative_n : Nat

208+ constructor getMultiplicative

209+-}

210+{-

211+record Multiplicative : Type where

212+ getMultiplicative : Nat -> Multiplicative

213+-}

205||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

214||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

215+data Additive : Type where

216+ getAdditive : Nat -> Additive

217+{-

218+record Additive where

219+ additive_n : Nat

220+ constructor getAdditive

221+-}

222+{-

206record Additive : Type where

223record Additive : Type where

207 getAdditive : Nat -> Additive

224 getAdditive : Nat -> Additive

208−

225+-}

209instance Semigroup Multiplicative where

226instance Semigroup Multiplicative where

210 (<+>) left right = getMultiplicative $ left' * right'

227 (<+>) left right = getMultiplicative $ left' * right'

211 where

228 where