git.iko.soy/Idris-dev
on master help sign in
Changed libs to new record syntax.
commit7e43af7bb7535e9785d96f111013eccd6fbfe401 authorSune Alkærsig <sual@itu.dk> dateThu 19 Mar 2015, 18:48 (12 years ago) parentf36a8f7
9 files changed+20−76
compare with master
unifiedsplit
libs/base/Control/Monad/Identity.idr+2−6 libs/base/Control/Monad/RWS.idr+2−6 libs/base/Control/Monad/Reader.idr+1−6 libs/base/Control/Monad/State.idr+2−6 libs/base/Control/Monad/Writer.idr+1−2 libs/base/Data/Buffer.idr+6−4 libs/base/Network/Cgi.idr+1−11 libs/base/Network/Socket.idr+4−26 libs/prelude/IO.idr+1−9
libs/base/Control/Monad/Identity.idr+2−6
@@ -1,13 +1,9 @@
11module Control.Monad.Identity
2−{-
3−public record Identity : Type -> Type where
4− Id : (runIdentity : a) -> Identity a
5−-}
62
73public record Identity (a : Type) where
8− runIdentity : a
94 constructor Id
10−
5+ runIdentity : a
6+
117instance Functor Identity where
128 map fn (Id a) = Id (fn a)
139
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
1212
1313||| The transformer on which the RWS monad is based
1414record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
15+ constructor MkRWST
1516 runRWST : r -> s -> m (a, s, w)
16−
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−-}
17+
2218instance Monad m => Functor (RWST r w s m) where
2319 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
2420 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
1515
1616||| The transformer on which the Reader monad is based
1717record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
18− runReaderT : r -> m a
1918 constructor RD
19+ runReaderT : r -> m a
2020
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−-}
2621||| Create a ReaderT with an empty context
2722liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
2823liftReaderT 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
1414
1515||| The transformer on which the State monad is based
1616record StateT (s : Type) (m : Type -> Type) (a : Type) where
17− runStateT : s -> m (a, s)
1817 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
23−-}
18+ runStateT : s -> m (a, s)
19+
2420instance Functor f => Functor (StateT s f) where
2521 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
2622 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
1717
1818||| The transformer base of the Writer monad
1919record WriterT (w : Type) (m : Type -> Type) (a : Type) where
20− runWriterT : m (a, w)
2120 constructor WR
22−
21+ runWriterT : m (a, w)
2322{-
2423record WriterT : Type -> (Type -> Type) -> Type -> Type where
2524 WR : {m : Type -> Type} ->
libs/base/Data/Buffer.idr+6−4
@@ -28,8 +28,10 @@ import Data.Fin
2828||| A contiguous chunk of n bytes
2929abstract
3030record Buffer (n : Nat) where
31+ constructor MkBuffer
3132 offset : Nat
32− realBufer : prim__UnsafeBuffer
33+ realBuffer : prim__UnsafeBuffer
34+
3335{-
3436record Buffer : Nat -> Type where
3537 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
@@ -48,13 +50,13 @@ bitsFromFin (FS k) = 1 + bitsFromFin k
4850||| approximate ultimate size of the Buffer is known. Users can assume
4951||| the new Buffer is word-aligned.
5052public
51−allocate : ( hint : Nat ) -> Buffer Z
52−allocate = MkBuffer Z . prim__allocate . bitsFromNat
53+allocate : ( hint : Nat) -> Buffer Z
54+allocate = MkBuffer Z . prim__allocate . bitsFromNat
5355
5456||| Append count repetitions of a Buffer to another Buffer
5557%assert_total
5658public
57−appendBuffer : Buffer n ->
59+appendBuffer : {n : Nat} -> {m : Nat} -> Buffer n ->
5860 ( count : Nat ) ->
5961 Buffer m ->
6062 Buffer ( n + count * m )
libs/base/Network/Cgi.idr+1−11
@@ -9,23 +9,13 @@ Vars : Type
99Vars = List (String, String)
1010
1111record CGIInfo where
12+ constructor CGISt
1213 GET : Vars
1314 POST : Vars
1415 Cookies : Vars
1516 UserAgent : String
1617 Headers : String
1718 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−-}
2919
3020add_Headers : String -> CGIInfo -> CGIInfo
3121add_Headers str st = record { Headers = Headers st ++ str } st
libs/base/Network/Socket.idr+4−26
@@ -108,32 +108,17 @@ EAGAIN = 11
108108
109109-- TODO: Expand to non-string payloads
110110record UDPRecvData where
111+ constructor MkUDPRecvData
111112 remote_addr : SocketAddress
112113 remote_port : Port
113114 recv_data : String
114115 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−-}
125116
126117record UDPAddrInfo where
118+ constructor MkUDPAddrInfo
127119 remote_addr : SocketAddress
128120 remote_port : Port
129121
130−{-
131−record UDPAddrInfo : Type where
132− MkUDPAddrInfo :
133− (remote_addr : SocketAddress) ->
134− (remote_port : Port) ->
135− UDPAddrInfo
136−-}
137122||| Frees a given pointer
138123public
139124sock_free : BufPtr -> IO ()
@@ -152,19 +137,12 @@ sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
152137
153138||| The metadata about a socket
154139record Socket where
140+ constructor MkSocket
155141 descriptor : SocketDescriptor
156142 family : SocketFamily
157143 socketType : SocketType
158144 protocalNumber : ProtocolNumber
159−
160−{-
161−record Socket : Type where
162− MkSocket : (descriptor : SocketDescriptor) ->
163− (family : SocketFamily) ->
164− (socketType : SocketType) ->
165− (protocolNumber : ProtocolNumber) ->
166− Socket
167−-}
145+
168146||| Get the C error number
169147getErrno : IO Int
170148getErrno = foreign FFI_C "idrnet_errno" (IO Int)
libs/prelude/IO.idr+1−9
@@ -21,18 +21,10 @@ abstract WorldRes : Type -> Type
2121WorldRes x = x
2222
2323record FFI where
24+ constructor MkFFI
2425 ffi_types : Type -> Type
2526 ffi_fn : Type
2627 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−-}
3628
3729abstract
3830data IO' : (lang : FFI) -> Type -> Type where