git.iko.soy/Idris-dev
on master help sign in
Changed libs to new record syntax.
7e43af7Sune Alkærsig
libs/base/Control/Monad/Identity.idr+2−6
compare with master
unifiedsplit
@@ -1,13 +1,9 @@
1module Control.Monad.Identity
1module Control.Monad.Identity
2−{-
3−public record Identity : Type -> Type where
4− Id : (runIdentity : a) -> Identity a
5−-}
6
2
7public record Identity (a : Type) where
3public record Identity (a : Type) where
8− runIdentity : a
9 constructor Id
4 constructor Id
10−
5+ runIdentity : a
6+
11instance Functor Identity where
7instance Functor Identity where
12 map fn (Id a) = Id (fn a)
8 map fn (Id a) = Id (fn a)
13
9
libs/base/Control/Monad/RWS.idr+2−6
@@ -12,13 +12,9 @@ class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r
12
12
13||| The transformer on which the RWS monad is based
13||| The transformer on which the RWS monad is based
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
15+ constructor MkRWST
15 runRWST : r -> s -> m (a, s, w)
16 runRWST : r -> s -> m (a, s, w)
16−
17+
17−{-
18−record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
19− MkRWST : {m : Type -> Type} ->
20− (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
21−-}
22instance Monad m => Functor (RWST r w s m) where
18instance Monad m => Functor (RWST r w s m) where
23 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
24 return (f a, s', w)
20 return (f a, s', w)
libs/base/Control/Monad/Reader.idr+1−6
@@ -15,14 +15,9 @@ class Monad m => MonadReader r (m : Type -> Type) where
15
15
16||| The transformer on which the Reader monad is based
16||| The transformer on which the Reader monad is based
17record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
17record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
18− runReaderT : r -> m a
19 constructor RD
18 constructor RD
19+ runReaderT : r -> m a
20
20
21−{-
22−record ReaderT : Type -> (Type -> Type) -> Type -> Type where
23− RD : {m : Type -> Type} ->
24− (runReaderT : r -> m a) -> ReaderT r m a
25−-}
26||| Create a ReaderT with an empty context
21||| Create a ReaderT with an empty context
27liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
22liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
28liftReaderT m = RD $ const m
23liftReaderT m = RD $ const m
libs/base/Control/Monad/State.idr+2−6
@@ -14,13 +14,9 @@ class Monad m => MonadState s (m : Type -> Type) where
14
14
15||| The transformer on which the State monad is based
15||| The transformer on which the State monad is based
16record StateT (s : Type) (m : Type -> Type) (a : Type) where
16record StateT (s : Type) (m : Type -> Type) (a : Type) where
17− runStateT : s -> m (a, s)
18 constructor ST
17 constructor ST
19−{-
20−record StateT : Type -> (Type -> Type) -> Type -> Type where
21− ST : {m : Type -> Type} ->
22− (runStateT : s -> m (a, s)) -> StateT s m a
18+ runStateT : s -> m (a, s)
23−-}
19+
24instance Functor f => Functor (StateT s f) where
20instance Functor f => Functor (StateT s f) where
25 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
21 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
26 mapFst : (a -> x) -> (a, s) -> (x, s)
22 mapFst : (a -> x) -> (a, s) -> (x, s)
libs/base/Control/Monad/Writer.idr+1−2
@@ -17,9 +17,8 @@ class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
17
17
18||| The transformer base of the Writer monad
18||| The transformer base of the Writer monad
19record WriterT (w : Type) (m : Type -> Type) (a : Type) where
19record WriterT (w : Type) (m : Type -> Type) (a : Type) where
20− runWriterT : m (a, w)
21 constructor WR
20 constructor WR
22−
21+ runWriterT : m (a, w)
23{-
22{-
24record WriterT : Type -> (Type -> Type) -> Type -> Type where
23record WriterT : Type -> (Type -> Type) -> Type -> Type where
25 WR : {m : Type -> Type} ->
24 WR : {m : Type -> Type} ->
libs/base/Data/Buffer.idr+6−4
@@ -28,8 +28,10 @@ import Data.Fin
28||| A contiguous chunk of n bytes
28||| A contiguous chunk of n bytes
29abstract
29abstract
30record Buffer (n : Nat) where
30record Buffer (n : Nat) where
31+ constructor MkBuffer
31 offset : Nat
32 offset : Nat
32− realBufer : prim__UnsafeBuffer
33+ realBuffer : prim__UnsafeBuffer
34+
33{-
35{-
34record Buffer : Nat -> Type where
36record Buffer : Nat -> Type where
35 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
37 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
@@ -48,13 +50,13 @@ bitsFromFin (FS k) = 1 + bitsFromFin k
48||| approximate ultimate size of the Buffer is known. Users can assume
50||| approximate ultimate size of the Buffer is known. Users can assume
49||| the new Buffer is word-aligned.
51||| the new Buffer is word-aligned.
50public
52public
51−allocate : ( hint : Nat ) -> Buffer Z
53+allocate : ( hint : Nat) -> Buffer Z
52−allocate = MkBuffer Z . prim__allocate . bitsFromNat
54+allocate = MkBuffer Z . prim__allocate . bitsFromNat
53
55
54||| Append count repetitions of a Buffer to another Buffer
56||| Append count repetitions of a Buffer to another Buffer
55%assert_total
57%assert_total
56public
58public
57−appendBuffer : Buffer n ->
59+appendBuffer : {n : Nat} -> {m : Nat} -> Buffer n ->
58 ( count : Nat ) ->
60 ( count : Nat ) ->
59 Buffer m ->
61 Buffer m ->
60 Buffer ( n + count * m )
62 Buffer ( n + count * m )
libs/base/Network/Cgi.idr+1−11
@@ -9,23 +9,13 @@ Vars : Type
9Vars = List (String, String)
9Vars = List (String, String)
10
10
11record CGIInfo where
11record CGIInfo where
12+ constructor CGISt
12 GET : Vars
13 GET : Vars
13 POST : Vars
14 POST : Vars
14 Cookies : Vars
15 Cookies : Vars
15 UserAgent : String
16 UserAgent : String
16 Headers : String
17 Headers : String
17 Output : String
18 Output : String
18− constructor CGISt
19−
20−{-
21−record CGIInfo : Type where
22− CGISt : (GET : Vars) ->
23− (POST : Vars) ->
24− (Cookies : Vars) ->
25− (UserAgent : String) ->
26− (Headers : String) ->
27− (Output : String) -> CGIInfo
28−-}
29
19
30add_Headers : String -> CGIInfo -> CGIInfo
20add_Headers : String -> CGIInfo -> CGIInfo
31add_Headers str st = record { Headers = Headers st ++ str } st
21add_Headers str st = record { Headers = Headers st ++ str } st
libs/base/Network/Socket.idr+4−26
@@ -108,32 +108,17 @@ EAGAIN = 11
108
108
109-- TODO: Expand to non-string payloads
109-- TODO: Expand to non-string payloads
110record UDPRecvData where
110record UDPRecvData where
111+ constructor MkUDPRecvData
111 remote_addr : SocketAddress
112 remote_addr : SocketAddress
112 remote_port : Port
113 remote_port : Port
113 recv_data : String
114 recv_data : String
114 data_len : Int
115 data_len : Int
115−
116−{-
117−record UDPRecvData : Type where
118− MkUDPRecvData :
119− (remote_addr : SocketAddress) ->
120− (remote_port : Port) ->
121− (recv_data : String) ->
122− (data_len : Int) ->
123− UDPRecvData
124−-}
125
116
126record UDPAddrInfo where
117record UDPAddrInfo where
118+ constructor MkUDPAddrInfo
127 remote_addr : SocketAddress
119 remote_addr : SocketAddress
128 remote_port : Port
120 remote_port : Port
129
121
130−{-
131−record UDPAddrInfo : Type where
132− MkUDPAddrInfo :
133− (remote_addr : SocketAddress) ->
134− (remote_port : Port) ->
135− UDPAddrInfo
136−-}
137||| Frees a given pointer
122||| Frees a given pointer
138public
123public
139sock_free : BufPtr -> IO ()
124sock_free : BufPtr -> IO ()
@@ -152,19 +137,12 @@ sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
152
137
153||| The metadata about a socket
138||| The metadata about a socket
154record Socket where
139record Socket where
140+ constructor MkSocket
155 descriptor : SocketDescriptor
141 descriptor : SocketDescriptor
156 family : SocketFamily
142 family : SocketFamily
157 socketType : SocketType
143 socketType : SocketType
158 protocalNumber : ProtocolNumber
144 protocalNumber : ProtocolNumber
159−
145+
160−{-
161−record Socket : Type where
162− MkSocket : (descriptor : SocketDescriptor) ->
163− (family : SocketFamily) ->
164− (socketType : SocketType) ->
165− (protocolNumber : ProtocolNumber) ->
166− Socket
167−-}
168||| Get the C error number
146||| Get the C error number
169getErrno : IO Int
147getErrno : IO Int
170getErrno = foreign FFI_C "idrnet_errno" (IO Int)
148getErrno = foreign FFI_C "idrnet_errno" (IO Int)
libs/prelude/IO.idr+1−9
@@ -21,18 +21,10 @@ abstract WorldRes : Type -> Type
21WorldRes x = x
21WorldRes x = x
22
22
23record FFI where
23record FFI where
24+ constructor MkFFI
24 ffi_types : Type -> Type
25 ffi_types : Type -> Type
25 ffi_fn : Type
26 ffi_fn : Type
26 ffi_data : Type
27 ffi_data : Type
27− constructor MkFFI
28−
29−{-
30−record FFI : Type where
31− MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI
32− MkFFI : (ffi_types : Type -> Type) ->
33− (ffi_fn : Type) ->
34− (ffi_data : Type) -> FFI
35−-}
36
28
37abstract
29abstract
38data IO' : (lang : FFI) -> Type -> Type where
30data IO' : (lang : FFI) -> Type -> Type where