git.iko.soy/Idris-dev
on master help sign in
Updated standard library to new record syntax.
commit6f0aff3e22274d4418c4c34b25bfabc276a5cbe9 authorSune Alkærsig <sual@itu.dk> dateThu 19 Feb 2015, 11:58 (12 years ago) parent173703d
10 files changed+91−9
compare with master
unifiedsplit
libs/base/Control/Monad/Identity.idr+6−1 libs/base/Control/Monad/RWS.idr+5−1 libs/base/Control/Monad/Reader.idr+6−1 libs/base/Control/Monad/State.idr+5−1 libs/base/Control/Monad/Writer.idr+6 libs/base/Data/Buffer.idr+5 libs/base/Network/Cgi.idr+11 libs/base/Network/Socket.idr+22−2 libs/prelude/IO.idr+6−1 libs/prelude/Prelude/Nat.idr+19−2
libs/base/Control/Monad/Identity.idr+6−1
@@ -1,8 +1,13 @@
11module Control.Monad.Identity
2−
2+{-
33public record Identity : Type -> Type where
44 Id : (runIdentity : a) -> Identity a
5+-}
56
7+public record Identity (a : Type) where
8+ runIdentity : a
9+ constructor Id
10+
611instance Functor Identity where
712 map fn (Id a) = Id (fn a)
813
libs/base/Control/Monad/RWS.idr+5−1
@@ -11,10 +11,14 @@ import Control.Monad.Reader
1111class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
1212
1313||| 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+{-
1418record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
1519 MkRWST : {m : Type -> Type} ->
1620 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
17−
21+-}
1822instance Monad m => Functor (RWST r w s m) where
1923 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
2024 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
1414 local : (r -> r) -> m a -> m a
1515
1616||| 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+{-
1722record ReaderT : Type -> (Type -> Type) -> Type -> Type where
1823 RD : {m : Type -> Type} ->
1924 (runReaderT : r -> m a) -> ReaderT r m a
20−
25+-}
2126||| Create a ReaderT with an empty context
2227liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
2328liftReaderT 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
1313 put : s -> m ()
1414
1515||| 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+{-
1620record StateT : Type -> (Type -> Type) -> Type -> Type where
1721 ST : {m : Type -> Type} ->
1822 (runStateT : s -> m (a, s)) -> StateT s m a
19−
23+-}
2024instance Functor f => Functor (StateT s f) where
2125 map f (ST g) = ST (\st => map (mapFst f) (g st)) where
2226 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
1616 pass : m (a, w -> w) -> m a
1717
1818||| 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+{-
1924record WriterT : Type -> (Type -> Type) -> Type -> Type where
2025 WR : {m : Type -> Type} ->
2126 (runWriterT : m (a, w)) -> WriterT w m a
27+-}
2228
2329instance Functor f => Functor (WriterT w f) where
2430 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
2727
2828||| A contiguous chunk of n bytes
2929abstract
30+record Buffer (n : Nat) where
31+ offset : Nat
32+ realBufer : prim__UnsafeBuffer
33+{-
3034record Buffer : Nat -> Type where
3135 MkBuffer : ( offset : Nat ) -> ( realBuffer : prim__UnsafeBuffer ) -> Buffer n
36+-}
3237
3338bitsFromNat : Nat -> Bits64
3439bitsFromNat Z = 0
libs/base/Network/Cgi.idr+11
@@ -8,6 +8,16 @@ public
88Vars : Type
99Vars = List (String, String)
1010
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+{-
1121record CGIInfo : Type where
1222 CGISt : (GET : Vars) ->
1323 (POST : Vars) ->
@@ -15,6 +25,7 @@ record CGIInfo : Type where
1525 (UserAgent : String) ->
1626 (Headers : String) ->
1727 (Output : String) -> CGIInfo
28+-}
1829
1930add_Headers : String -> CGIInfo -> CGIInfo
2031add_Headers str st = record { Headers = Headers st ++ str } st
libs/base/Network/Socket.idr+22−2
@@ -107,6 +107,13 @@ EAGAIN : Int
107107EAGAIN = 11
108108
109109-- 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+{-
110117record UDPRecvData : Type where
111118 MkUDPRecvData :
112119 (remote_addr : SocketAddress) ->
@@ -114,13 +121,19 @@ record UDPRecvData : Type where
114121 (recv_data : String) ->
115122 (data_len : Int) ->
116123 UDPRecvData
124+-}
117125
126+record UDPAddrInfo where
127+ remote_addr : SocketAddress
128+ remote_port : Port
129+
130+{-
118131record UDPAddrInfo : Type where
119132 MkUDPAddrInfo :
120133 (remote_addr : SocketAddress) ->
121134 (remote_port : Port) ->
122135 UDPAddrInfo
123−
136+-}
124137||| Frees a given pointer
125138public
126139sock_free : BufPtr -> IO ()
@@ -138,13 +151,20 @@ sock_alloc : ByteLength -> IO BufPtr
138151sock_alloc bl = map BPtr $ foreign FFI_C "idrnet_malloc" (Int -> IO Ptr) bl
139152
140153||| The metadata about a socket
154+record Socket where
155+ descriptor : SocketDescriptor
156+ family : SocketFamily
157+ socketType : SocketType
158+ protocalNumber : ProtocolNumber
159+
160+{-
141161record Socket : Type where
142162 MkSocket : (descriptor : SocketDescriptor) ->
143163 (family : SocketFamily) ->
144164 (socketType : SocketType) ->
145165 (protocolNumber : ProtocolNumber) ->
146166 Socket
147−
167+-}
148168||| Get the C error number
149169getErrno : IO Int
150170getErrno = foreign FFI_C "idrnet_errno" (IO Int)
libs/prelude/IO.idr+6−1
@@ -20,9 +20,14 @@ world (TheWorld w) = w
2020abstract WorldRes : Type -> Type
2121WorldRes x = x
2222
23+record FFI where
24+ ffi_types : Type -> Type
25+ ffi_fn : Type
26+ constructor MkFFI
27+{-
2328record FFI : Type where
2429 MkFFI : (ffi_types : Type -> Type) -> (ffi_fn : Type) -> FFI
25−
30+-}
2631abstract
2732data IO' : (lang : FFI) -> Type -> Type where
2833 MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
libs/prelude/Prelude/Nat.idr+19−2
@@ -199,13 +199,30 @@ instance Cast Integer Nat where
199199 cast = fromInteger
200200
201201||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)
202−record Multiplicative : Type where
202+data Multiplicative : Type where
203203 getMultiplicative : Nat -> Multiplicative
204204
205+{-
206+record Multiplicative where
207+ multiplicative_n : Nat
208+ constructor getMultiplicative
209+-}
210+{-
211+record Multiplicative : Type where
212+ getMultiplicative : Nat -> Multiplicative
213+-}
205214||| 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+{-
206223record Additive : Type where
207224 getAdditive : Nat -> Additive
208−
225+-}
209226instance Semigroup Multiplicative where
210227 (<+>) left right = getMultiplicative $ left' * right'
211228 where