diff --git a/.gitignore b/.gitignore
index 444ba6c..a9ebdc6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,6 +6,8 @@
 idris2
 runtests
 
+docs/_build/
+
 libs/**/build
 tests/**/output
 
diff --git a/Makefile b/Makefile
index 1ea0ce5..5f7e72b 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,11 @@ prelude:
 base: prelude
 	make -C libs/base IDRIS2=../../idris2
 
-libs : prelude base
+network: prelude
+	make -C libs/network IDRIS2=../../idris2
+	make -C libs/network test IDRIS2=../../idris2
+
+libs : prelude base network
 
 clean: clean-libs
 	make -C src clean
@@ -37,6 +41,7 @@ clean: clean-libs
 clean-libs:
 	make -C libs/prelude clean
 	make -C libs/base clean
+	make -C libs/network clean
 
 test:
 	idris --build tests.ipkg
@@ -58,3 +63,4 @@ install-exec: idris2
 install-libs: libs
 	make -C libs/prelude install IDRIS2=../../idris2
 	make -C libs/base install IDRIS2=../../idris2
+	make -C libs/network install IDRIS2=../../idris2
diff --git a/Notes/Directives.md b/Notes/Directives.md
index 8f53a29..299d3c9 100644
--- a/Notes/Directives.md
+++ b/Notes/Directives.md
@@ -99,3 +99,49 @@ the elaborator is working on, up to `5` gives you more specific details of
 each stage of the elaboration, and up to `10` gives you full details of
 type checking including progress on unification problems
 
+## Code Generator Directives
+
+### %cg
+
+#### Backend code injection
+
+Syntax:
+* `%cg <backend> <single-line instruction>`
+* `%cg <backend> { <multi-line instructions> }`
+
+The given instructions are passed directly to the code generator, to be
+interpreted in a backend-specific way.
+
+Currently known backends are: `chez`, `chicken` and `racket`.
+
+## Backend Specific Directives
+
+### Chez
+
+#### Dynamic library loading
+
+Syntax: `%cg chez lib<library_name>`
+
+Instructs chez to load given external library at
+runtime, eg. using dynamic library loader. The compiler looks for a
+file called  `library_name` in the following directories and generates
+corresponding file-loading code:
+
+* current directory `.`
+* directories listed in the `IDRIS2_LIBS` environment variable, if
+  set
+* directories `lib/` in each package the code depends on (`base` and
+  `prelude` are automatically added). Loads library as absolute path name of _first matchine file_
+  found.
+* directory `lib/` in the Idris2 installation path (usually
+  `~/.idris2/idris2`).
+
+Note the file is loaded referencing an absolute path of the first
+matching file found, except when it's the current directory in which
+case the file is simply referenced as `./library_name`
+
+### Chicken
+
+The directive should be scheme code which is inserted directly into the generated
+code. This can be used, for example, to import external libraries, e.g.
+`%cg chicken (use posix)`.
diff --git a/docs/conf.py b/docs/conf.py
index 621d128..f982fcf 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -35,13 +35,14 @@ extensions = [
     'sphinx.ext.todo',
 #    'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
     'sphinx.ext.ifconfig',
+    'recommonmark'
 ]
 
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']
 
 # The suffix of source filenames.
-source_suffix = '.rst'
+source_suffix = ['.rst','.md']
 
 # The encoding of source files.
 #source_encoding = 'utf-8-sig'
diff --git a/idris2.ipkg b/idris2.ipkg
index baf8bcc..7e45fe2 100644
--- a/idris2.ipkg
+++ b/idris2.ipkg
@@ -111,6 +111,7 @@ modules =
     TTImp.TTImp,
     TTImp.Unelab,
     TTImp.Utils,
+    TTImp.WithClause,
 
     Utils.Binary,
     Utils.Shunting,
diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index a5df095..99bbb3a 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -85,8 +85,8 @@ export
 strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
 strengthen {n = S k} FZ = Right FZ
 strengthen {n = S k} (FS i) with (strengthen i)
-  strengthen (FS k) | Left x   = Left (FS x)
-  strengthen (FS k) | Right x  = Right (FS x)
+  strengthen (FS i) | Left x   = Left (FS x)
+  strengthen (FS i) | Right x  = Right (FS x)
 strengthen f = Left f
 
 ||| Add some natural number to a Fin, extending the bound accordingly
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index 1d0d135..2f36986 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -40,11 +40,28 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
 public export
 filter : (p : a -> Bool) -> List a -> List a
 filter p [] = []
-filter p (x :: xs) 
+filter p (x :: xs)
    = if p x
         then x :: filter p xs
         else filter p xs
 
+||| Find associated information in a list using a custom comparison.
+public export
+lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
+lookupBy p e []      = Nothing
+lookupBy p e (x::xs) =
+  let (l, r) = x in
+    if p e l then
+      Just r
+    else
+      lookupBy p e xs
+
+||| Find associated information in a list using Boolean equality.
+public export
+lookup : Eq a => a -> List (a, b) -> Maybe b
+lookup = lookupBy (==)
+
+
 public export
 span : (a -> Bool) -> List a -> (List a, List a)
 span p []      = ([], [])
@@ -70,7 +87,7 @@ public export
 splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
 splitAt Z xs = ([], xs)
 splitAt (S k) [] = ([], [])
-splitAt (S k) (x :: xs) 
+splitAt (S k) (x :: xs)
       = let (tk, dr) = splitAt k xs in
             (x :: tk, dr)
 
@@ -115,6 +132,22 @@ export
 toList : Foldable t => t a -> List a
 toList = foldr (::) []
 
+||| Insert some separator between the elements of a list.
+|||
+||| ````idris example
+||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
+||| ````
+|||
+export
+intersperse : a -> List a -> List a
+intersperse sep []      = []
+intersperse sep (x::xs) = x :: intersperse' sep xs
+  where
+    intersperse' : a -> List a -> List a
+    intersperse' sep []      = []
+    intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys
+
+
 --------------------------------------------------------------------------------
 -- Sorting
 --------------------------------------------------------------------------------
@@ -181,17 +214,17 @@ Uninhabited ([] = Prelude.(::) x xs) where
 export
 Uninhabited (Prelude.(::) x xs = []) where
   uninhabited Refl impossible
--- 
+--
 -- ||| (::) is injective
 -- consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
 --                 (x :: xs) = (y :: ys) -> (x = y, xs = ys)
 -- consInjective Refl = (Refl, Refl)
--- 
+--
 -- ||| Two lists are equal, if their heads are equal and their tails are equal.
 -- consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
 --             x = y -> xs = ys -> x :: xs = y :: ys
 -- consCong2 Refl Refl = Refl
--- 
+--
 -- ||| Appending pairwise equal lists gives equal lists
 -- appendCong2 : {x1 : List a} -> {x2 : List a} ->
 --               {y1 : List b} -> {y2 : List b} ->
@@ -203,13 +236,13 @@ Uninhabited (Prelude.(::) x xs = []) where
 --   consCong2
 --     (fst $ consInjective eq1)
 --     (appendCong2 (snd $ consInjective eq1) eq2)
--- 
+--
 -- ||| List.map is distributive over appending.
 -- mapAppendDistributive : (f : a -> b) -> (x : List a) -> (y : List a) ->
 --                         map f (x ++ y) = map f x ++ map f y
 -- mapAppendDistributive _ [] _ = Refl
 -- mapAppendDistributive f (_ :: xs) y = cong $ mapAppendDistributive f xs y
--- 
+--
 ||| The empty list is a right identity for append.
 export
 appendNilRightNeutral : (l : List a) ->
diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr
index 64e0168..583dc39 100644
--- a/libs/base/Data/Strings.idr
+++ b/libs/base/Data/Strings.idr
@@ -72,6 +72,17 @@ public export
 break : (Char -> Bool) -> String -> (String, String)
 break p = span (not . p)
 
+
+||| Splits the string into parts with the predicate
+||| indicating separator characters.
+|||
+||| ```idris example
+||| split (== '.') ".AB.C..D"
+||| ```
+public export
+split : (Char -> Bool) -> String -> List String
+split p xs = map pack (split p (unpack xs))
+
 export
 stringToNatOrZ : String -> Nat
 stringToNatOrZ = fromInteger . prim__cast_StringInteger
diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr
new file mode 100644
index 0000000..775385a
--- /dev/null
+++ b/libs/network/Echo.idr
@@ -0,0 +1,57 @@
+module Main
+
+import System
+import Network.Socket
+import Network.Socket.Data
+import Network.Socket.Raw
+
+%cg chez libidris_net.so
+
+runServer : IO (Either String (Port, ThreadID))
+runServer = do
+  Right sock <- socket AF_INET Stream 0
+        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
+  res <- bind sock (Just (Hostname "localhost")) 0
+  if res /= 0
+    then pure (Left $ "Failed to bind socket with error: " ++ show res)
+    else do
+      port <- getSockPort sock
+      res <- listen sock
+      if res /= 0
+        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
+        else do
+          forked <- fork (serve port sock)
+          pure $ Right (port, forked)
+
+  where
+    serve : Port -> Socket -> IO ()
+    serve port sock = do
+      Right (s, _) <- accept sock
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      Right  (str, _) <- recv s 1024
+        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
+      putStrLn ("Received: " ++ str)
+      Right n <- send s ("echo: " ++ str)
+        | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
+      putStrLn ("Server sent " ++ show n ++ " bytes")
+
+runClient : Port -> IO ()
+runClient serverPort = do
+  Right sock <- socket AF_INET Stream 0
+    | Left fail => putStrLn ("Failed to open socket: " ++ show fail)
+  res <- connect sock (Hostname "localhost") serverPort
+  if res /= 0
+    then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
+    else do
+      Right n <- send sock ("hello world!")
+        | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
+      putStrLn ("Client sent " ++ show n ++ " bytes")
+      Right (str, _) <- recv sock 1024
+        | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
+      putStrLn ("Received: " ++ str)
+
+main : IO ()
+main = do
+  Right (serverPort, tid) <- runServer
+    | Left err => putStrLn $ "[server] " ++ err
+  runClient serverPort
diff --git a/libs/network/Makefile b/libs/network/Makefile
new file mode 100644
index 0000000..b63547e
--- /dev/null
+++ b/libs/network/Makefile
@@ -0,0 +1,61 @@
+RANLIB      ?=ranlib
+AR          ?=ar
+
+MACHINE         := $(shell $(CC) -dumpmachine)
+ifneq (, $(findstring darwin, $(MACHINE)))
+	OS      :=darwin
+else ifneq (, $(findstring cygwin, $(MACHINE)))
+	OS      :=windows
+else ifneq (, $(findstring mingw, $(MACHINE)))
+	OS      :=windows
+else ifneq (, $(findstring windows, $(MACHINE)))
+	OS      :=windows
+else
+	OS      :=unix
+endif
+
+SHLIB_SUFFIX    :=.so
+
+LIBNAME=idris_net
+OBJS = $(LIBNAME).o
+HDRS = $(LIBNAME).h
+CFLAGS := $(CFLAGS)
+IDRIS_SRCS = Network/Socket.idr Network/Socket/Data.idr Network/Socket/Raw.idr
+
+ifneq ($(OS), windows)
+	CFLAGS += -fPIC
+endif
+
+DYLIBTARGET = $(LIBNAME)$(SHLIB_SUFFIX)
+LIBTARGET = $(LIBNAME).a
+TARGET=${HOME}/.idris2
+
+build: $(DYLIBTARGET) $(IDRIS_SRCS)
+	@if ! [ -d build ]; then echo "creating 'build' directory"; mkdir build ; else echo "directory 'build' exists"; fi
+	@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
+	${IDRIS2} --build network.ipkg
+
+$(DYLIBTARGET) : $(OBJS)
+	$(CC) -o $(DYLIBTARGET) $(LIBFLAGS) -shared $(OBJS)
+
+install:
+	@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
+	${IDRIS2} --install network.ipkg
+	@if ! [ -d $(TARGET)/idris2/network/lib ]; then mkdir $(TARGET)/idris2/network/lib; fi
+	install $(DYLIBTARGET) $(HDRS) $(TARGET)/idris2/network/lib
+
+clean :
+	rm -rf $(OBJS) $(LIBTARGET) $(DYLIBTARGET) build
+
+test: build test.c
+	cp $(DYLIBTARGET) lib$(DYLIBTARGET) # to make C linker happy
+	$(CC) -o network-tests -L. -I. test.c -l$(LIBNAME)
+	LD_LIBRARY_PATH=. ./network-tests
+	./lib-tests
+
+$(OBJS): $(HDRS)
+
+all: $(DYLIBTARGET) $(LIBTARGET)
+	${IDRIS2} --build network.ipkg
+
+.PHONY: install clean
diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr
new file mode 100644
index 0000000..e255f58
--- /dev/null
+++ b/libs/network/Network/Socket.idr
@@ -0,0 +1,223 @@
+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
+|||
+||| Original (C) SimonJF, MIT Licensed, 2014
+||| Modified (C) The Idris Community, 2015, 2016, 2019
+module Network.Socket
+
+import public Network.Socket.Data
+import Network.Socket.Raw
+import Data.List
+
+-- ----------------------------------------------------- [ Network Socket API. ]
+
+||| Creates a UNIX socket with the given family, socket type and protocol
+||| number. Returns either a socket or an error.
+socket : (fam  : SocketFamily)
+      -> (ty   : SocketType)
+      -> (pnum : ProtocolNumber)
+      -> IO (Either SocketError Socket)
+socket sf st pn = do
+  socket_res <- cCall Int "idrnet_socket" [toCode sf, toCode st, pn]
+
+  if socket_res == -1
+    then map Left getErrno
+    else pure $ Right (MkSocket socket_res sf st pn)
+
+||| Close a socket
+close : Socket -> IO ()
+close sock = cCall () "close" [descriptor sock]
+
+||| Binds a socket to the given socket address and port.
+||| Returns 0 on success, an error code otherwise.
+bind : (sock : Socket)
+    -> (addr : Maybe SocketAddress)
+    -> (port : Port)
+    -> IO Int
+bind sock addr port = do
+    bind_res <- cCall Int "idrnet_bind"
+                [ descriptor sock, toCode $ family sock
+                , toCode $ socketType sock, saString addr,  port
+                ]
+    if bind_res == (-1)
+      then getErrno
+      else pure 0
+  where
+    saString : Maybe SocketAddress -> String
+    saString (Just sa) = show sa
+    saString Nothing   = ""
+
+||| Connects to a given address and port.
+||| Returns 0 on success, and an error number on error.
+connect : (sock : Socket)
+       -> (addr : SocketAddress)
+       -> (port : Port)
+       -> IO ResultCode
+connect sock addr port = do
+  conn_res <- cCall Int "idrnet_connect"
+              [ descriptor sock, toCode $ family sock, toCode $ socketType sock, show addr, port]
+
+  if conn_res == (-1)
+    then getErrno
+    else pure 0
+
+||| Listens on a bound socket.
+|||
+||| @sock The socket to listen on.
+listen : (sock : Socket) -> IO Int
+listen sock = do
+  listen_res <- cCall Int "listen" [ descriptor sock, BACKLOG ]
+  if listen_res == (-1)
+    then getErrno
+    else pure 0
+
+||| Accept a connection on the provided socket.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success a pairing of:
+||| + `Socket`        :: The socket representing the connection.
+||| + `SocketAddress` :: The
+|||
+||| @sock The socket used to establish connection.
+accept : (sock : Socket)
+      -> IO (Either SocketError (Socket, SocketAddress))
+accept sock = do
+
+  -- We need a pointer to a sockaddr structure. This is then passed into
+  -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
+
+  sockaddr_ptr <- cCall Ptr "idrnet_create_sockaddr" []
+
+  accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ]
+  if accept_res == (-1)
+    then map Left getErrno
+    else do
+      let (MkSocket _ fam ty p_num) = sock
+      sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
+      sockaddr_free (SAPtr sockaddr_ptr)
+      pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
+
+||| Send data on the specified socket.
+|||
+||| Returns on failure a `SocketError`.
+||| Returns on success the `ResultCode`.
+|||
+||| @sock The socket on which to send the message.
+||| @msg  The data to send.
+send : (sock : Socket)
+    -> (msg  : String)
+    -> IO (Either SocketError ResultCode)
+send sock dat = do
+  send_res <- cCall Int "idrnet_send" [ descriptor sock, dat ]
+
+  if send_res == (-1)
+    then map Left getErrno
+    else pure $ Right send_res
+
+||| Receive data on the specified socket.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success a pairing of:
+||| + `String`     :: The payload.
+||| + `ResultCode` :: The result of the underlying function.
+|||
+||| @sock The socket on which to receive the message.
+||| @len  How much of the data to receive.
+recv : (sock : Socket)
+    -> (len : ByteLength)
+    -> IO (Either SocketError (String, ResultCode))
+recv sock len = do
+  -- Firstly make the request, get some kind of recv structure which
+  -- contains the result of the recv and possibly the retrieved payload
+  recv_struct_ptr <- cCall Ptr "idrnet_recv" [ descriptor sock, len]
+  recv_res <- cCall Int "idrnet_get_recv_res"  [ recv_struct_ptr ]
+
+  if recv_res == (-1)
+    then do
+      errno <- getErrno
+      freeRecvStruct (RSPtr recv_struct_ptr)
+      pure $ Left errno
+    else
+      if recv_res == 0
+        then do
+           freeRecvStruct (RSPtr recv_struct_ptr)
+           pure $ Left 0
+        else do
+           payload <- cCall String "idrnet_get_recv_payload" [ recv_struct_ptr ]
+           freeRecvStruct (RSPtr recv_struct_ptr)
+           pure $ Right (payload, recv_res)
+
+||| Receive all the remaining data on the specified socket.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success the payload `String`
+|||
+||| @sock The socket on which to receive the message.
+partial
+recvAll : (sock : Socket) -> IO (Either SocketError String)
+recvAll sock = recvRec sock [] 64
+  where
+    partial
+    recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
+    recvRec sock acc n = do res <- recv sock n
+                            case res of
+                              Left 0 => pure (Right $ concat $ reverse acc)
+                              Left c => pure (Left c)
+                              Right (str, _) => let n' = min (n * 2) 65536 in
+                                                recvRec sock (str :: acc) n'
+
+||| Send a message.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success the `ResultCode`
+|||
+||| @sock The socket on which to send the message.
+||| @addr Address of the recipient.
+||| @port The port on which to send the message.
+||| @msg  The message to send.
+sendTo : (sock : Socket)
+      -> (addr : SocketAddress)
+      -> (port : Port)
+      -> (msg  : String)
+      -> IO (Either SocketError ByteLength)
+sendTo sock addr p dat = do
+  sendto_res <- cCall Int "idrnet_sendto"
+                [ descriptor sock, dat, show addr, p ,toCode $ family sock ]
+
+  if sendto_res == (-1)
+    then map Left getErrno
+    else pure $ Right sendto_res
+
+||| Receive a message.
+|||
+||| Returns on failure a `SocketError`.
+||| Returns on success a triple of
+||| + `UDPAddrInfo` :: The address of the sender.
+||| + `String`      :: The payload.
+||| + `Int`         :: Result value from underlying function.
+|||
+||| @sock The channel on which to receive.
+||| @len  Size of the expected message.
+|||
+recvFrom : (sock : Socket)
+        -> (len  : ByteLength)
+        -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
+recvFrom sock bl = do
+  recv_ptr <- cCall Ptr "idrnet_recvfrom"
+              [ descriptor sock, bl ]
+
+  let recv_ptr' = RFPtr recv_ptr
+  isNull <- (nullPtr recv_ptr)
+  if isNull
+    then map Left getErrno
+    else do
+      result <- cCall Int "idrnet_get_recvfrom_res" [ recv_ptr ]
+      if result == -1
+        then do
+          freeRecvfromStruct recv_ptr'
+          map Left getErrno
+        else do
+          payload <- foreignGetRecvfromPayload recv_ptr'
+          port <- foreignGetRecvfromPort recv_ptr'
+          addr <- foreignGetRecvfromAddr recv_ptr'
+          freeRecvfromStruct recv_ptr'
+          pure $ Right (MkUDPAddrInfo addr port, payload, result)
diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr
new file mode 100644
index 0000000..70c4f1f
--- /dev/null
+++ b/libs/network/Network/Socket/Data.idr
@@ -0,0 +1,214 @@
+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
+||| Types used by Network.Socket.Raw and Network.Socket.
+|||
+||| Original (C) SimonJF, MIT Licensed, 2014
+||| Modified (C) The Idris Community, 2015, 2016, 2019
+module Network.Socket.Data
+
+import Data.List
+import Data.Strings
+
+-- ------------------------------------------------------------ [ Type Aliases ]
+
+-- FIXME should be generic name with OS-dependent suffix
+%cg chez "libidris_net.so"
+
+public export
+ByteLength : Type
+ByteLength = Int
+
+public export
+ResultCode : Type
+ResultCode = Int
+
+||| Protocol Number.
+|||
+||| Generally good enough to just set it to 0.
+public export
+ProtocolNumber : Type
+ProtocolNumber = Int
+
+||| SocketError: Error thrown by a socket operation
+public export
+SocketError : Type
+SocketError = Int
+
+||| SocketDescriptor: Native C Socket Descriptor
+public export
+SocketDescriptor : Type
+SocketDescriptor = Int
+
+public export
+Port : Type
+Port = Int
+
+-- --------------------------------------------------------------- [ Constants ]
+
+||| Backlog used within listen() call -- number of incoming calls
+export
+BACKLOG : Int
+BACKLOG = 20
+
+export
+EAGAIN : Int
+EAGAIN =
+  -- I'm sorry
+  -- maybe
+  unsafePerformIO $ cCall Int "idrnet_geteagain" []
+
+-- ---------------------------------------------------------------- [ Error Code ]
+
+export
+getErrno : IO SocketError
+getErrno = cCall Int "idrnet_errno" []
+
+export
+nullPtr : Ptr -> IO Bool
+nullPtr p = cCall Bool "isNull" [p]
+
+-- -------------------------------------------------------------- [ Interfaces ]
+
+public export
+interface ToCode a where
+  toCode : a -> Int
+
+-- --------------------------------------------------------- [ Socket Families ]
+
+||| Socket Families
+|||
+||| The ones that people might actually use. We're not going to need US
+||| Government proprietary ones.
+public export
+data SocketFamily : Type where
+  ||| Unspecified
+  AF_UNSPEC : SocketFamily
+
+  ||| Unix type sockets
+  AF_UNIX : SocketFamily
+
+  ||| IP / UDP etc. IPv4
+  AF_INET : SocketFamily
+
+  |||  IP / UDP etc. IPv6
+  AF_INET6 : SocketFamily
+
+Show SocketFamily where
+  show AF_UNSPEC = "AF_UNSPEC"
+  show AF_UNIX   = "AF_UNIX"
+  show AF_INET   = "AF_INET"
+  show AF_INET6  = "AF_INET6"
+
+export
+ToCode SocketFamily where
+  -- Don't know how to read a constant value from C code in idris2...
+  -- gotta to hardcode those for now
+  toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
+  toCode AF_UNIX   = 1
+  toCode AF_INET   = 2
+  toCode AF_INET6  = 10
+
+export
+getSocketFamily : Int -> Maybe SocketFamily
+getSocketFamily i =
+    lookup i [ (toCode AF_UNSPEC, AF_UNSPEC)
+             , (toCode AF_UNIX, AF_UNIX)
+             , (toCode AF_INET, AF_INET)
+             , (toCode AF_INET6, AF_INET6)
+             ]
+
+-- ------------------------------------------------------------ [ Socket Types ]
+
+||| Socket Types.
+public export
+data SocketType : Type where
+  ||| Not a socket, used in certain operations
+  NotASocket : SocketType
+
+  ||| TCP
+  Stream : SocketType
+
+  ||| UDP
+  Datagram : SocketType
+
+  ||| Raw sockets
+  RawSocket : SocketType
+
+export
+Show SocketType where
+  show NotASocket = "Not a socket"
+  show Stream     = "Stream"
+  show Datagram   = "Datagram"
+  show RawSocket  = "Raw"
+
+export
+ToCode SocketType where
+  toCode NotASocket = 0
+  toCode Stream     = 1
+  toCode Datagram   = 2
+  toCode RawSocket  = 3
+
+-- --------------------------------------------------------------- [ Addresses ]
+
+||| Network Addresses
+public export
+data SocketAddress : Type where
+  IPv4Addr : Int -> Int -> Int -> Int -> SocketAddress
+
+  ||| Not implemented (yet)
+  IPv6Addr : SocketAddress
+
+  Hostname : String -> SocketAddress
+
+  ||| Used when there's a parse error
+  InvalidAddress : SocketAddress
+
+export
+Show SocketAddress where
+  show (IPv4Addr i1 i2 i3 i4) = concat $ intersperse "." (map show [i1, i2, i3, i4])
+  show IPv6Addr               = "NOT IMPLEMENTED YET"
+  show (Hostname host)        = host
+  show InvalidAddress         = "Invalid"
+
+||| Parses a textual representation of an IPv4 address into a SocketAddress
+export
+parseIPv4 : String -> SocketAddress
+parseIPv4 str =
+    case splitted of
+      (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
+      otherwise                   => InvalidAddress
+  where
+    toInt' : String -> Integer
+    toInt' = cast
+
+    toInt : String -> Int
+    toInt s = fromInteger $ toInt' s
+
+    splitted : List Int
+    splitted = map toInt (split (\c => c == '.') str)
+
+-- --------------------------------------------------------- [ UDP Information ]
+
+-- TODO: Expand to non-string payloads
+public export
+record UDPRecvData where
+  constructor MkUDPRecvData
+  remote_addr : SocketAddress
+  remote_port : Port
+  recv_data   : String
+  data_len    : Int
+
+public export
+record UDPAddrInfo where
+  constructor MkUDPAddrInfo
+  remote_addr : SocketAddress
+  remote_port : Port
+
+-- ----------------------------------------------------------------- [ Sockets ]
+||| The metadata about a socket
+public export
+record Socket where
+  constructor MkSocket
+  descriptor     : SocketDescriptor
+  family         : SocketFamily
+  socketType     : SocketType
+  protocolNumber : ProtocolNumber
diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr
new file mode 100644
index 0000000..41515f3
--- /dev/null
+++ b/libs/network/Network/Socket/Raw.idr
@@ -0,0 +1,190 @@
+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
+||| Type-unsafe parts. Use Network.Socket for a safe variant.
+|||
+||| Original (C) SimonJF, MIT Licensed, 2014
+||| Modified (C) The Idris Community, 2015, 2016
+module Network.Socket.Raw
+
+import public Network.Socket.Data
+
+-- ---------------------------------------------------------------- [ Pointers ]
+
+public export
+data RecvStructPtr     = RSPtr Ptr
+
+public export
+data RecvfromStructPtr = RFPtr Ptr
+
+public export
+data BufPtr = BPtr Ptr
+
+public export
+data SockaddrPtr = SAPtr Ptr
+
+-- ---------------------------------------------------------- [ Socket Utilies ]
+
+||| Frees a given pointer
+sock_free : BufPtr -> IO ()
+sock_free (BPtr ptr) = cCall () "idrnet_free" [ptr]
+
+export
+sockaddr_free : SockaddrPtr -> IO ()
+sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr]
+
+||| Allocates an amount of memory given by the ByteLength parameter.
+|||
+||| Used to allocate a mutable pointer to be given to the Recv functions.
+sock_alloc : ByteLength -> IO BufPtr
+sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl]
+
+||| Retrieves the port the given socket is bound to
+export
+getSockPort : Socket -> IO Port
+getSockPort sock = cCall Int "idrnet_sockaddr_port" [descriptor sock]
+
+
+||| Retrieves a socket address from a sockaddr pointer
+export
+getSockAddr : SockaddrPtr -> IO SocketAddress
+getSockAddr (SAPtr ptr) = do
+  addr_family_int <- cCall Int "idrnet_sockaddr_family"  [ptr]
+
+  -- ASSUMPTION: Foreign call returns a valid int
+  assert_total (case getSocketFamily addr_family_int of
+    Just AF_INET => do
+      ipv4_addr <- cCall String "idrnet_sockaddr_ipv4" [ptr]
+
+      pure $ parseIPv4 ipv4_addr
+    Just AF_INET6 => pure IPv6Addr
+    Just AF_UNSPEC => pure InvalidAddress)
+
+export
+freeRecvStruct : RecvStructPtr -> IO ()
+freeRecvStruct (RSPtr p) = cCall () "idrnet_free_recv_struct" [p]
+
+||| Utility to extract data.
+export
+freeRecvfromStruct : RecvfromStructPtr -> IO ()
+freeRecvfromStruct (RFPtr p) = cCall () "idrnet_free_recvfrom_struct" [p]
+
+||| Sends the data in a given memory location
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success the `ResultCode`
+|||
+||| @sock The socket on which to send the message.
+||| @ptr  The location containing the data to send.
+||| @len  How much of the data to send.
+export
+sendBuf : (sock : Socket)
+       -> (ptr  : BufPtr)
+       -> (len  : ByteLength)
+       -> IO (Either SocketError ResultCode)
+sendBuf sock (BPtr ptr) len = do
+  send_res <- cCall Int "idrnet_send_buf" [ descriptor sock, ptr, len]
+
+  if send_res == (-1)
+   then map Left getErrno
+   else pure $ Right send_res
+
+||| Receive data from a given memory location.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success the `ResultCode`
+|||
+||| @sock The socket on which to receive the message.
+||| @ptr  The location containing the data to receive.
+||| @len  How much of the data to receive.
+export
+recvBuf : (sock : Socket)
+       -> (ptr  : BufPtr)
+       -> (len  : ByteLength)
+       -> IO (Either SocketError ResultCode)
+recvBuf sock (BPtr ptr) len = do
+  recv_res <- cCall Int "idrnet_recv_buf" [ descriptor sock, ptr, len ]
+
+  if (recv_res == (-1))
+    then map Left getErrno
+    else pure $ Right recv_res
+
+||| Send a message stored in some buffer.
+|||
+||| Returns on failure a `SocketError`
+||| Returns on success the `ResultCode`
+|||
+||| @sock The socket on which to send the message.
+||| @addr Address of the recipient.
+||| @port The port on which to send the message.
+||| @ptr  A Pointer to the buffer containing the message.
+||| @len  The size of the message.
+export
+sendToBuf : (sock : Socket)
+         -> (addr : SocketAddress)
+         -> (port : Port)
+         -> (ptr  : BufPtr)
+         -> (len  : ByteLength)
+         -> IO (Either SocketError ResultCode)
+sendToBuf sock addr p (BPtr dat) len = do
+  sendto_res <- cCall Int "idrnet_sendto_buf"
+                [ descriptor sock, dat, len, show addr, p, toCode $ family sock ]
+
+  if sendto_res == (-1)
+    then map Left getErrno
+    else pure $ Right sendto_res
+
+||| Utility function to get the payload of the sent message as a `String`.
+export
+foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
+foreignGetRecvfromPayload (RFPtr p) = cCall String "idrnet_get_recvfrom_payload" [ p ]
+
+||| Utility function to return senders socket address.
+export
+foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
+foreignGetRecvfromAddr (RFPtr p) = do
+  sockaddr_ptr <- map SAPtr $ cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
+  getSockAddr sockaddr_ptr
+
+||| Utility function to return sender's IPV4 port.
+export
+foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
+foreignGetRecvfromPort (RFPtr p) = do
+  sockaddr_ptr <- cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
+  port         <- cCall Int "idrnet_sockaddr_ipv4_port" [sockaddr_ptr]
+  pure port
+
+||| Receive a message placed on a 'known' buffer.
+|||
+||| Returns on failure a `SocketError`.
+||| Returns on success a pair of
+||| + `UDPAddrInfo` :: The address of the sender.
+||| + `Int`         :: Result value from underlying function.
+|||
+||| @sock The channel on which to receive.
+||| @ptr  Pointer to the buffer to place the message.
+||| @len  Size of the expected message.
+|||
+export
+recvFromBuf : (sock : Socket)
+           -> (ptr  : BufPtr)
+           -> (len  : ByteLength)
+           -> IO (Either SocketError (UDPAddrInfo, ResultCode))
+recvFromBuf sock (BPtr ptr) bl = do
+  recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl]
+
+  let recv_ptr' = RFPtr recv_ptr
+
+  isnull <- nullPtr recv_ptr
+
+  if isnull
+    then map Left getErrno
+    else do
+      result <- cCall Int "idrnet_get_recvfrom_res" [recv_ptr]
+      if result == -1
+        then do
+          freeRecvfromStruct recv_ptr'
+          map Left getErrno
+        else do
+          port <- foreignGetRecvfromPort recv_ptr'
+          addr <- foreignGetRecvfromAddr recv_ptr'
+          freeRecvfromStruct recv_ptr'
+          pure $ Right (MkUDPAddrInfo addr port, result + 1)
diff --git a/libs/network/expected b/libs/network/expected
new file mode 100644
index 0000000..bf70af7
--- /dev/null
+++ b/libs/network/expected
@@ -0,0 +1,4 @@
+Client sent 12 bytes
+Received: hello world!
+Server sent 18 bytes
+Received: echo: hello world!
diff --git a/libs/network/idris_net.c b/libs/network/idris_net.c
new file mode 100644
index 0000000..84505f7
--- /dev/null
+++ b/libs/network/idris_net.c
@@ -0,0 +1,383 @@
+// C-Side of the Idris network library
+// (C) Simon Fowler, 2014
+// MIT Licensed. Have fun!
+#include "idris_net.h"
+#include <errno.h>
+#include <stdbool.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+
+#ifndef _WIN32
+#include <netinet/in.h>
+#include <arpa/inet.h>
+#else
+static int socket_inited = 0;
+static WSADATA wsa_data;
+
+static void clean_sockets(void) {
+    WSACleanup();
+}
+
+static int check_init(void) {
+    if (!socket_inited) {
+        int result = WSAStartup(MAKEWORD(2, 2), &wsa_data);
+        if (result == NO_ERROR) {
+            socket_inited = 1;
+            atexit(clean_sockets);
+        }
+    }
+    return socket_inited;
+}
+#endif
+
+
+void buf_htonl(void* buf, int len) {
+    int* buf_i = (int*) buf;
+    int i;
+    for (i = 0; i < (len / sizeof(int)) + 1; i++) {
+        buf_i[i] = htonl(buf_i[i]);
+    }
+}
+
+void buf_ntohl(void* buf, int len) {
+    int* buf_i = (int*) buf;
+    int i;
+    for (i = 0; i < (len / sizeof(int)) + 1; i++) {
+        buf_i[i] = ntohl(buf_i[i]);
+    }
+}
+
+void* idrnet_malloc(int size) {
+    return malloc(size);
+}
+
+void idrnet_free(void* ptr) {
+    free(ptr);
+}
+
+
+int idrnet_socket(int domain, int type, int protocol) {
+#ifdef _WIN32
+    if (!check_init()) {
+        return -1;
+    }
+#endif
+    return socket(domain, type, protocol);
+}
+
+// We call this from quite a few functions. Given a textual host and an int port,
+// populates a struct addrinfo.
+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,
+                       int family, int socket_type) {
+
+    struct addrinfo hints;
+    // Convert port into string
+    char str_port[8];
+    sprintf(str_port, "%d", port);
+
+    // Set up hints structure
+    memset(&hints, 0, sizeof(hints)); // zero out hints
+    hints.ai_family = family;
+    hints.ai_socktype = socket_type;
+
+    // If the length of the hostname is 0 (i.e, it was set to Nothing in Idris)
+    // then we want to instruct the C library to fill in the IP automatically
+    if (strlen(host) == 0) {
+        hints.ai_flags = AI_PASSIVE; // fill in IP automatically
+        return getaddrinfo(NULL, str_port, &hints, address_res);
+    }
+    return getaddrinfo(host, str_port, &hints, address_res);
+
+}
+
+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
+    struct addrinfo *address_res;
+    int addr_res = idrnet_getaddrinfo(&address_res, host, port, family, socket_type);
+    if (addr_res != 0) {
+        //printf("Lib err: bind getaddrinfo\n");
+        return -1;
+    }
+
+    int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
+    if (bind_res == -1) {
+        //freeaddrinfo(address_res);
+        //printf("Lib err: bind\n");
+        return -1;
+    }
+    return 0;
+}
+
+// to retrieve information about a socket bound to port 0
+int idrnet_getsockname(int sockfd, void *address, void *len) {
+  int res = getsockname(sockfd, address, len);
+  if(res != 0) {
+    return -1;
+  }
+
+  return 0;
+}
+
+int idrnet_sockaddr_port(int sockfd) {
+  struct sockaddr address;
+  socklen_t addrlen = sizeof(struct sockaddr);
+  int res = getsockname(sockfd, &address, &addrlen);
+  if(res < 0) {
+    return -1;
+  }
+
+  switch(address.sa_family) {
+  case AF_INET:
+    return ntohs(((struct sockaddr_in*)&address)->sin_port);
+  case AF_INET6:
+    return ntohs(((struct sockaddr_in6*)&address)->sin6_port);
+  default:
+    return -1;
+  }
+}
+
+
+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {
+    struct addrinfo* remote_host;
+    int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, socket_type);
+    if (addr_res != 0) {
+        return -1;
+    }
+
+    int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);
+    if (connect_res == -1) {
+        freeaddrinfo(remote_host);
+        return -1;
+    }
+    freeaddrinfo(remote_host);
+    return 0;
+}
+
+
+int idrnet_sockaddr_family(void* sockaddr) {
+    struct sockaddr* addr = (struct sockaddr*) sockaddr;
+    return (int) addr->sa_family;
+}
+
+char* idrnet_sockaddr_ipv4(void* sockaddr) {
+    struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
+    char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);
+    inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);
+    //printf("Lib: ip_addr: %s\n", ip_addr);
+    return ip_addr;
+}
+
+int idrnet_sockaddr_ipv4_port(void* sockaddr) {
+    struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
+    return ((int) ntohs(addr->sin_port));
+}
+
+void* idrnet_create_sockaddr() {
+    return malloc(sizeof(struct sockaddr_storage));
+}
+
+
+int idrnet_accept(int sockfd, void* sockaddr) {
+    struct sockaddr* addr = (struct sockaddr*) sockaddr;
+    socklen_t addr_size = sizeof(struct sockaddr_storage);
+    return accept(sockfd, addr, &addr_size);
+}
+
+int idrnet_send(int sockfd, char* data) {
+    int len = strlen(data); // For now.
+    return send(sockfd, (void*) data, len, 0);
+}
+
+int idrnet_send_buf(int sockfd, void* data, int len) {
+    void* buf_cpy = malloc(len);
+    memset(buf_cpy, 0, len);
+    memcpy(buf_cpy, data, len);
+    buf_htonl(buf_cpy, len);
+    int res = send(sockfd, buf_cpy, len, 0);
+    free(buf_cpy);
+    return res;
+}
+
+void* idrnet_recv(int sockfd, int len) {
+    idrnet_recv_result* res_struct =
+        (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
+    char* buf = malloc(len + 1);
+    memset(buf, 0, len + 1);
+    int recv_res = recv(sockfd, buf, len, 0);
+    res_struct->result = recv_res;
+
+    if (recv_res > 0) { // Data was received
+        buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
+    }
+    res_struct->payload = buf;
+    return (void*) res_struct;
+}
+
+int idrnet_recv_buf(int sockfd, void* buf, int len) {
+    int recv_res = recv(sockfd, buf, len, 0);
+    if (recv_res != -1) {
+        buf_ntohl(buf, len);
+    }
+    return recv_res;
+}
+
+int idrnet_get_recv_res(void* res_struct) {
+    return (((idrnet_recv_result*) res_struct)->result);
+}
+
+char* idrnet_get_recv_payload(void* res_struct) {
+    return (((idrnet_recv_result*) res_struct)->payload);
+}
+
+void idrnet_free_recv_struct(void* res_struct) {
+    idrnet_recv_result* i_res_struct =
+        (idrnet_recv_result*) res_struct;
+    if (i_res_struct->payload != NULL) {
+        free(i_res_struct->payload);
+    }
+    free(res_struct);
+}
+
+int idrnet_errno() {
+    return errno;
+}
+
+
+int idrnet_sendto(int sockfd, char* data, char* host, int port, int family) {
+
+    struct addrinfo* remote_host;
+    int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
+    if (addr_res != 0) {
+        return -1;
+    }
+
+    int send_res = sendto(sockfd, data, strlen(data), 0,
+                        remote_host->ai_addr, remote_host->ai_addrlen);
+    freeaddrinfo(remote_host);
+    return send_res;
+}
+
+int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family) {
+
+    struct addrinfo* remote_host;
+    int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
+    if (addr_res != 0) {
+        //printf("lib err: sendto getaddrinfo \n");
+        return -1;
+    }
+
+    buf_htonl(buf, buf_len);
+
+    int send_res = sendto(sockfd, buf, buf_len, 0,
+                        remote_host->ai_addr, remote_host->ai_addrlen);
+    if (send_res == -1) {
+        perror("lib err: sendto \n");
+    }
+    //freeaddrinfo(remote_host);
+    return send_res;
+}
+
+
+
+void* idrnet_recvfrom(int sockfd, int len) {
+/*
+ * int recvfrom(int sockfd, void *buf, int len, unsigned int flags,
+             struct sockaddr *from, int *fromlen);
+*/
+    // Allocate the required structures, and nuke them
+    struct sockaddr_storage* remote_addr =
+        (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
+    char* buf = (char*) malloc(len + 1);
+    idrnet_recvfrom_result* ret =
+        (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
+    memset(remote_addr, 0, sizeof(struct sockaddr_storage));
+    memset(buf, 0, len + 1);
+    memset(ret, 0, sizeof(idrnet_recvfrom_result));
+    socklen_t fromlen = sizeof(struct sockaddr_storage);
+
+    int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
+    ret->result = recv_res;
+    // Check for failure...
+    if (recv_res == -1) {
+        free(buf);
+        free(remote_addr);
+    } else {
+        // If data was received, process and populate
+        ret->result = recv_res;
+        ret->remote_addr = remote_addr;
+        // Ensure the last byte is NULL, since in this mode we're sending strings
+        buf[len] = 0x00;
+        ret->payload = (void*) buf;
+    }
+
+    return ret;
+}
+
+void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {
+    // Allocate the required structures, and nuke them
+    struct sockaddr_storage* remote_addr =
+        (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
+    idrnet_recvfrom_result* ret =
+        (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
+    memset(remote_addr, 0, sizeof(struct sockaddr_storage));
+    memset(ret, 0, sizeof(idrnet_recvfrom_result));
+    socklen_t fromlen = 0;
+
+    int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
+    // Check for failure... But don't free the buffer! Not our job.
+    ret->result = recv_res;
+    if (recv_res == -1) {
+        free(remote_addr);
+    }
+    // Payload will be NULL -- since it's been put into the user-specified buffer. We
+    // still need the return struct to get our hands on the remote address, though.
+    if (recv_res > 0) {
+        buf_ntohl(buf, len);
+        ret->payload = NULL;
+        ret->remote_addr = remote_addr;
+    }
+    return ret;
+}
+
+int idrnet_get_recvfrom_res(void* res_struct) {
+    return (((idrnet_recvfrom_result*) res_struct)->result);
+}
+
+char* idrnet_get_recvfrom_payload(void* res_struct) {
+    return (((idrnet_recvfrom_result*) res_struct)->payload);
+}
+
+void* idrnet_get_recvfrom_sockaddr(void* res_struct) {
+    idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
+    return recv_struct->remote_addr;
+}
+
+int idrnet_get_recvfrom_port(void* res_struct) {
+    idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
+    if (recv_struct->remote_addr != NULL) {
+        struct sockaddr_in* remote_addr_in =
+            (struct sockaddr_in*) recv_struct->remote_addr;
+        return ((int) ntohs(remote_addr_in->sin_port));
+    }
+    return -1;
+}
+
+void idrnet_free_recvfrom_struct(void* res_struct) {
+    idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
+    if (recv_struct != NULL) {
+        if (recv_struct->payload != NULL) {
+            free(recv_struct->payload);
+        }
+        if (recv_struct->remote_addr != NULL) {
+            free(recv_struct->remote_addr);
+        }
+    }
+}
+
+int idrnet_geteagain() {
+    return EAGAIN;
+}
+
+int isNull(void* ptr) {
+    return ptr==NULL;
+}
diff --git a/libs/network/idris_net.h b/libs/network/idris_net.h
new file mode 100644
index 0000000..5f4ebe2
--- /dev/null
+++ b/libs/network/idris_net.h
@@ -0,0 +1,98 @@
+#ifndef IDRISNET_H
+#define IDRISNET_H
+
+// Includes used by the idris-file.
+#ifdef _WIN32
+#include <winsock2.h>
+#include <Ws2tcpip.h>
+#else
+#include <netdb.h>
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/socket.h>
+#endif
+
+struct sockaddr_storage;
+struct addrinfo;
+
+typedef struct idrnet_recv_result {
+    int result;
+    void* payload;
+} idrnet_recv_result;
+
+// Same type of thing as idrnet_recv_result, but for UDP, so stores some
+// address information
+typedef struct idrnet_recvfrom_result {
+    int result;
+    void* payload;
+    struct sockaddr_storage* remote_addr;
+} idrnet_recvfrom_result;
+
+// Memory management functions
+void* idrnet_malloc(int size);
+void idrnet_free(void* ptr);
+
+// Gets value of errno
+int idrnet_errno();
+
+int idrnet_socket(int domain, int type, int protocol);
+
+// Bind
+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);
+
+// Retrieve information about socket
+int idrnet_getsockname(int sockfd, void *address, void *len);
+
+// Connect
+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port);
+
+// Accessor functions for struct_sockaddr
+int idrnet_sockaddr_family(void* sockaddr);
+char* idrnet_sockaddr_ipv4(void* sockaddr);
+int idrnet_sockaddr_ipv4_port(void* sockaddr);
+void* idrnet_create_sockaddr();
+
+int idrnet_sockaddr_port(int sockfd);
+
+// Accept
+int idrnet_accept(int sockfd, void* sockaddr);
+
+// Send
+int idrnet_send(int sockfd, char* data);
+int idrnet_send_buf(int sockfd, void* data, int len);
+
+// Receive
+// Creates a result structure containing result and payload
+void* idrnet_recv(int sockfd, int len);
+// Receives directly into a buffer
+int idrnet_recv_buf(int sockfd, void* buf, int len);
+
+// UDP Send
+int idrnet_sendto(int sockfd, char* data, char* host, int port, int family);
+int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family);
+
+
+// UDP Receive
+void* idrnet_recvfrom(int sockfd, int len);
+void* idrnet_recvfrom_buf(int sockfd, void* buf, int len);
+
+// Receive structure accessors
+int idrnet_get_recv_res(void* res_struct);
+char* idrnet_get_recv_payload(void* res_struct);
+void idrnet_free_recv_struct(void* res_struct);
+
+// Recvfrom structure accessors
+int idrnet_get_recvfrom_res(void* res_struct);
+char* idrnet_get_recvfrom_payload(void* res_struct);
+void* idrnet_get_recvfrom_sockaddr(void* res_struct);
+void idrnet_free_recvfrom_struct(void* res_struct);
+
+
+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,
+    int port, int family, int socket_type);
+
+int idrnet_geteagain();
+
+int isNull(void* ptr);
+
+#endif
diff --git a/libs/network/lib-tests b/libs/network/lib-tests
new file mode 100755
index 0000000..67f84a0
--- /dev/null
+++ b/libs/network/lib-tests
@@ -0,0 +1,10 @@
+#!/bin/sh
+
+${IDRIS2} --exec main Echo.idr > build/output
+
+if ! [ -z "$(diff build/output expected)" ]; then
+   echo "TEST FAILURE: unexpected build/output"
+   exit 2
+else
+  echo "TEST SUCCESS"
+fi
diff --git a/libs/network/network.ipkg b/libs/network/network.ipkg
new file mode 100644
index 0000000..968728c
--- /dev/null
+++ b/libs/network/network.ipkg
@@ -0,0 +1,5 @@
+package network
+
+modules = Network.Socket,
+          Network.Socket.Data,
+          Network.Socket.Raw
diff --git a/libs/network/test.c b/libs/network/test.c
new file mode 100644
index 0000000..2504345
--- /dev/null
+++ b/libs/network/test.c
@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdio.h>
+#include <netinet/in.h>
+#include <arpa/inet.h>
+
+#include "idris_net.h"
+
+void test_sockaddr_port_returns_random_port_when_bind_port_is_0() {
+  int sock = idrnet_socket(AF_INET, 1,  0);
+  assert(sock > 0);
+
+  int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 0);
+  assert(res == 0);
+
+  res = idrnet_sockaddr_port(sock);
+  assert(res > 0);
+
+  close(sock);
+}
+
+void test_sockaddr_port_returns_explicitly_assigned_port() {
+  int sock = idrnet_socket(AF_INET, 1,  0);
+  assert(sock > 0);
+
+  int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 34567);
+  assert(res == 0);
+
+  res = idrnet_sockaddr_port(sock);
+  assert(res == 34567);
+
+  close(sock);
+}
+
+
+int main(int argc, char**argv) {
+  test_sockaddr_port_returns_explicitly_assigned_port();
+  test_sockaddr_port_returns_random_port_when_bind_port_is_0();
+
+  printf("network library tests SUCCESS\n");
+  return 0;
+}
diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr
index 7e199a1..bbead0d 100644
--- a/libs/prelude/Prelude.idr
+++ b/libs/prelude/Prelude.idr
@@ -861,7 +861,7 @@ strUncons : String -> Maybe (Char, String)
 strUncons "" = Nothing
 strUncons str = Just (prim__strHead str, prim__strTail str)
 
-export
+public export
 pack : List Char -> String
 pack [] = ""
 pack (x :: xs) = strCons x (pack xs)
@@ -875,7 +875,7 @@ fastPack xs
     toFArgs [] = []
     toFArgs (x :: xs) = x :: toFArgs xs
 
-export
+public export
 unpack : String -> List Char
 unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
   where
diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index 3f70d96..178938b 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -300,10 +300,12 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
              let dn_in = UN ("Default implementation of " ++ show n)
              dn <- inCurrentNS dn_in
 
-             dty <- case lookup n tydecls of
-                         Just (_, _, t) => pure t
-                         Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
-                  
+             (rig, dty) <- 
+                   the (Core (RigCount, RawImp)) $
+                       case lookup n tydecls of
+                          Just (r, (_, t)) => pure (r, t)
+                          Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
+
              let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
 
              -- Substitute the method names with their top level function
@@ -318,7 +320,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
              dty_imp <- bindTypeNames (map fst tydecls ++ vars)
                                       (bindIFace fc ity dty)
              log 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
-             let dtydecl = IClaim fc RigW vis [] (MkImpTy fc dn dty_imp) 
+             let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp) 
              processDecl [] nest env dtydecl
 
              let cs' = map (changeName dn) cs
diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr
index 9814ce0..12e7176 100644
--- a/src/Idris/Main.idr
+++ b/src/Idris/Main.idr
@@ -126,9 +126,11 @@ stMain opts
 
                  u <- newRef UST initUState
                  updateREPLOpts
+                 session <- getSession
                  case fname of
                       Nothing => logTime "Loading prelude" $
-                                   readPrelude
+                                   when (not $ noprelude session) $
+                                     readPrelude
                       Just f => logTime "Loading main file" $
                                    loadMainFile f
 
diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr
index 7a4d401..f13d85d 100644
--- a/src/TTImp/Elab/Binders.idr
+++ b/src/TTImp/Elab/Binders.idr
@@ -188,8 +188,9 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty
             inScope fc env' (\e' => 
               check {e=e'} rigc elabinfo nest' env' scope expScope)
          scopet <- getTerm gscopet
-         checkExp rigc elabinfo env fc
-                  (Bind fc n (Let rigb valv tyv) scopev)
-                  (gnf env (Bind fc n (Let rigb valv tyv) scopet))
-                  expty
 
+         -- No need to 'checkExp' here - we've already checked scopet
+         -- against the expected type when checking the scope, so just
+         -- build the term directly
+         pure (Bind fc n (Let rigb valv tyv) scopev,
+               gnf env (Bind fc n (Let rigb valv tyv) scopet))
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index 75f20dc..1d45679 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@@ -20,6 +20,7 @@ import TTImp.Elab.Check
 import TTImp.TTImp
 import TTImp.Unelab
 import TTImp.Utils
+import TTImp.WithClause
 
 import Data.NameMap
 
@@ -202,7 +203,6 @@ combineLinear loc ((n, count) :: cs)
         = do newc <- combine c c'
              combineAll newc cs
 
-export
 checkLHS : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
@@ -210,9 +210,10 @@ checkLHS : {vars : _} ->
            (mult : RigCount) -> (hashit : Bool) ->
            Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
            FC -> RawImp -> 
-           Core (vars' ** (SubVars vars vars',
+           Core (RawImp, -- checked LHS with implicits added
+                 (vars' ** (SubVars vars vars',
                            Env Term vars', NestedNames vars', 
-                           Term vars', Term vars'))
+                           Term vars', Term vars')))
 checkLHS {vars} mult hashit n opts nest env fc lhs_in
     = do defs <- get Ctxt
          lhs_raw <- lhsInCurrentNS nest lhs_in 
@@ -250,7 +251,8 @@ checkLHS {vars} mult hashit n opts nest env fc lhs_in
          logTerm 5 "LHS type" lhsty_lin
          setHoleLHS (bindEnv fc env lhstm_lin)
 
-         extendEnv env SubRefl nest lhstm_lin lhsty_lin
+         ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin
+         pure (lhs, ext)
 
 plicit : Binder (Term vars) -> PiInfo
 plicit (Pi _ p _) = p
@@ -303,110 +305,6 @@ hasEmptyPat defs env (Bind fc x (PVar c p ty) sc)
             || !(hasEmptyPat defs (PVar c p ty :: env) sc)
 hasEmptyPat defs env _ = pure False
     
--- Get the arguments for the rewritten pattern clause of a with by looking
--- up how the argument names matched
-getArgMatch : FC -> Bool -> RawImp -> List (String, RawImp) ->
-              Maybe (PiInfo, Name) -> RawImp
-getArgMatch ploc search warg ms Nothing = warg
-getArgMatch ploc True warg ms (Just (AutoImplicit, UN n))
-    = case lookup n ms of
-           Nothing => ISearch ploc 500
-           Just tm => tm
-getArgMatch ploc True warg ms (Just (AutoImplicit, _))
-    = ISearch ploc 500
-getArgMatch ploc search warg ms (Just (_, UN n))
-    = case lookup n ms of
-           Nothing => Implicit ploc True
-           Just tm => tm
-getArgMatch ploc search warg ms _ = Implicit ploc True
-    
-getNewLHS : {auto c : Ref Ctxt Defs} ->
-            FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo, Name)) ->
-            RawImp -> RawImp -> Core RawImp
-getNewLHS ploc drop wname wargnames lhs_raw patlhs
-    = do (mlhs_raw, wrest) <- dropWithArgs drop patlhs
-         autoimp <- isAutoImplicits
-         autoImplicits True
-         (_, lhs) <- bindNames False lhs_raw
-         (_, mlhs) <- bindNames False mlhs_raw
-         autoImplicits autoimp
-
-         let (warg :: rest) = reverse wrest
-             | _ => throw (GenericMsg ploc "Badly formed 'with' clause")
-         log 10 $ show lhs ++ " against " ++ show mlhs ++
-                 " dropping " ++ show (warg :: rest)
-         ms <- getMatch lhs mlhs
-         log 10 $ "Matches: " ++ show ms
-         let newlhs = apply (IVar ploc wname)
-                            (map (getArgMatch ploc False warg ms) wargnames ++ rest)
-         log 10 $ "New LHS: " ++ show newlhs
-         pure newlhs
-  where
-    dropWithArgs : Nat -> RawImp -> 
-                   Core (RawImp, List RawImp)
-    dropWithArgs Z tm = pure (tm, [])
-    dropWithArgs (S k) (IApp _ f arg)
-        = do (tm, rest) <- dropWithArgs k f
-             pure (tm, arg :: rest)
-    -- Shouldn't happen if parsed correctly, but there's no guarantee that
-    -- inputs come from parsed source so throw an error.
-    dropWithArgs _ _ = throw (GenericMsg ploc "Badly formed 'with' clause")
-        
--- Find a 'with' application on the RHS and update it
-withRHS : {auto c : Ref Ctxt Defs} ->
-          FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo, Name)) ->
-          RawImp -> RawImp -> 
-          Core RawImp
-withRHS fc drop wname wargnames tm toplhs
-    = wrhs tm
-  where
-    withApply : FC -> RawImp -> List RawImp -> RawImp
-    withApply fc f [] = f
-    withApply fc f (a :: as) = withApply fc (IWithApp fc f a) as
-
-    updateWith : FC -> RawImp -> List RawImp -> Core RawImp
-    updateWith fc (IWithApp _ f a) ws = updateWith fc f (a :: ws)
-    updateWith fc tm []
-        = throw (GenericMsg fc "Badly formed 'with' application")
-    updateWith fc tm (arg :: args)
-        = do log 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
-             ms <- getMatch toplhs tm
-             log 10 $ "Result: " ++ show ms
-             let newrhs = apply (IVar fc wname)
-                                (map (getArgMatch fc True arg ms) wargnames)
-             log 10 $ "With args for RHS: " ++ show wargnames
-             log 10 $ "New RHS: " ++ show newrhs
-             pure (withApply fc newrhs args)
-
-    mutual
-      wrhs : RawImp -> Core RawImp
-      wrhs (IPi fc c p n ty sc)
-          = pure $ IPi fc c p n !(wrhs ty) !(wrhs sc)
-      wrhs (ILam fc c p n ty sc)
-          = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)
-      wrhs (ILet fc c n ty val sc)
-          = pure $ ILet fc c n !(wrhs ty) !(wrhs val) !(wrhs sc)
-      wrhs (ICase fc sc ty clauses)
-          = pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
-      wrhs (ILocal fc decls sc)
-          = pure $ ILocal fc decls !(wrhs sc) -- TODO!
-      wrhs (IUpdate fc upds tm)
-          = pure $ IUpdate fc upds !(wrhs tm) -- TODO!
-      wrhs (IApp fc f a)
-          = pure $ IApp fc !(wrhs f) !(wrhs a)
-      wrhs (IImplicitApp fc f n a)
-          = pure $ IImplicitApp fc !(wrhs f) n !(wrhs a)
-      wrhs (IWithApp fc f a) = updateWith fc f [a]
-      wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
-      wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)
-      wrhs (IDelay fc tm) = pure $ IDelay fc !(wrhs tm)
-      wrhs (IForce fc tm) = pure $ IForce fc !(wrhs tm)
-      wrhs tm = pure tm
-
-      wrhsC : ImpClause -> Core ImpClause
-      wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
-      wrhsC c = pure c
-    
 -- For checking with blocks as nested names
 applyEnv : {auto c : Ref Ctxt Defs} ->
            Env Term vars -> Name -> 
@@ -453,7 +351,7 @@ checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
                             then pure Nothing
                             else throw (ValidCase fc env (Right err)))
 checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
-    = do (vars'  ** (sub', env', nest', lhstm', lhsty')) <- 
+    = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <- 
              checkLHS mult hashit n opts nest env fc lhs_in
          let rhsMode = case mult of
                             Rig0 => InType
@@ -478,7 +376,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
          pure (Just (MkClause env' lhstm' rhstm))
 -- TODO: (to decide) With is complicated. Move this into its own module?
 checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
-    = do (vars'  ** (sub', env', nest', lhspat, reqty)) <- 
+    = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <- 
              checkLHS mult hashit n opts nest env fc lhs_in
          let wmode
                = case mult of
@@ -549,7 +447,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
                           (gnf env' reqty)
 
          -- Generate new clauses by rewriting the matched arguments
-         cs' <- traverse (mkClauseWith 1 wname wargNames lhs_in) cs
+         cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs
          log 3 $ "With clauses: " ++ show cs'
 
          -- Elaborate the new definition here
@@ -588,16 +486,16 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
                    RawImp -> ImpClause -> 
                    Core ImpClause
     mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)
-        = do newlhs <- getNewLHS ploc drop wname wargnames lhs patlhs
+        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              newrhs <- withRHS ploc drop wname wargnames rhs lhs
              pure (PatClause ploc newlhs newrhs)
     mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs ws)
-        = do newlhs <- getNewLHS ploc drop wname wargnames lhs patlhs
+        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              newrhs <- withRHS ploc drop wname wargnames rhs lhs
              ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws
              pure (WithClause ploc newlhs newrhs ws')
     mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)
-        = do newlhs <- getNewLHS ploc drop wname wargnames lhs patlhs
+        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              pure (ImpossibleClause ploc newlhs)
 
 
diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr
index 2ffe505..588fffb 100644
--- a/src/TTImp/Utils.idr
+++ b/src/TTImp/Utils.idr
@@ -252,62 +252,3 @@ uniqueName defs used n
     next str 
         = let (n, i) = nameNum str in
               n ++ "_" ++ show (i + 1)
-
-matchFail : FC -> Core a
-matchFail loc = throw (GenericMsg loc "Clauses do not match")
-
-mutual
-  export
-  getMatch : RawImp -> RawImp ->
-             Core (List (String, RawImp))
-  getMatch (IBindVar _ n) tm = pure [(n, tm)]
-  getMatch (Implicit _ _) tm = pure []
-
-  getMatch (IVar _ n) (IVar loc n') 
-      = if n == n' then pure [] else matchFail loc
-  getMatch (IPi _ c p n arg ret) (IPi loc c' p' n' arg' ret')
-      = if c == c' && p == p' && n == n'
-           then matchAll [(arg, arg'), (ret, ret')]
-           else matchFail loc
-  -- TODO: Lam, Let, Case, Local, Update
-  getMatch (IApp _ f a) (IApp loc f' a')
-      = matchAll [(f, f'), (a, a')]
-  getMatch (IImplicitApp _ f n a) (IImplicitApp loc f' n' a')
-      = if n == n' 
-           then matchAll [(f, f'), (a, a')]
-           else matchFail loc
-  getMatch (IWithApp _ f a) (IWithApp loc f' a')
-      = matchAll [(f, f'), (a, a')]
-  -- It's okay to skip implicits
-  getMatch (IImplicitApp fc f n a) f' 
-      = getMatch f f;
-  getMatch f (IImplicitApp fc f' n a)
-      = getMatch f f;
-  -- Alternatives are okay as long as all corresponding alternatives are okay
-  getMatch (IAlternative _ _ as) (IAlternative _ _ as')
-      = matchAll (zip as as')
-  getMatch (IAs _ _ _ p) p' = getMatch p p'
-  getMatch p (IAs _ _ _ p') = getMatch p p'
-  getMatch (IType _) (IType _) = pure []
-  getMatch pat spec = matchFail (getFC pat)
-
-  matchAll : List (RawImp, RawImp) ->
-             Core (List (String, RawImp))
-  matchAll [] = pure []
-  matchAll ((x, y) :: ms)
-      = do matches <- matchAll ms
-           mxy <- getMatch x y
-           mergeMatches (mxy ++ matches)
-
-  mergeMatches : List (String, RawImp) ->
-                 Core (List (String, RawImp))
-  mergeMatches [] = pure []
-  mergeMatches ((n, tm) :: rest)
-      = do rest' <- mergeMatches rest
-           case lookup n rest' of
-                Nothing => pure ((n, tm) :: rest')
-                Just tm' =>
-                   do getMatch tm tm' -- just need to know it succeeds
-                      mergeMatches rest
-
-
diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr
new file mode 100644
index 0000000..9cc1444
--- /dev/null
+++ b/src/TTImp/WithClause.idr
@@ -0,0 +1,189 @@
+module TTImp.WithClause
+
+import Core.Context
+import Core.TT
+import TTImp.BindImplicits
+import TTImp.TTImp
+
+matchFail : FC -> Core a
+matchFail loc = throw (GenericMsg loc "With clause does not match parent")
+
+mutual
+  export
+  getMatch : (lhs : Bool) -> RawImp -> RawImp ->
+             Core (List (String, RawImp))
+  getMatch lhs (IBindVar _ n) tm = pure [(n, tm)]
+  getMatch lhs (Implicit _ _) tm = pure []
+
+  getMatch lhs (IVar _ (NS ns n)) (IVar loc (NS ns' n'))
+      = if n == n' && isSuffixOf ns' ns then pure [] else matchFail loc
+  getMatch lhs (IVar _ (NS ns n)) (IVar loc n')
+      = if n == n' then pure [] else matchFail loc
+  getMatch lhs (IVar _ n) (IVar loc n') 
+      = if n == n' then pure [] else matchFail loc
+  getMatch lhs (IPi _ c p n arg ret) (IPi loc c' p' n' arg' ret')
+      = if c == c' && p == p' && n == n'
+           then matchAll lhs [(arg, arg'), (ret, ret')]
+           else matchFail loc
+  -- TODO: Lam, Let, Case, Local, Update
+  getMatch lhs (IApp _ f a) (IApp loc f' a')
+      = matchAll lhs [(f, f'), (a, a')]
+  getMatch lhs (IImplicitApp _ f n a) (IImplicitApp loc f' n' a')
+      = if n == n' 
+           then matchAll lhs [(f, f'), (a, a')]
+           else matchFail loc
+  getMatch lhs (IWithApp _ f a) (IWithApp loc f' a')
+      = matchAll lhs [(f, f'), (a, a')]
+  -- On LHS: If there's an implicit in the parent, but not the clause, add the
+  -- implicit to the clause. This will propagate the implicit through to the
+  -- body
+  getMatch True (IImplicitApp fc f n a) f'
+      = matchAll True [(f, f'), (a, a)]
+  -- On RHS: Rely on unification to fill in the implicit
+  getMatch False (IImplicitApp fc f n a) f'
+      = getMatch False f f
+  -- Can't have an implicit in the clause if there wasn't a matching
+  -- implicit in the parent
+  getMatch lhs f (IImplicitApp fc f' n a)
+      = matchFail fc
+  -- Alternatives are okay as long as all corresponding alternatives are okay
+  getMatch lhs (IAlternative _ _ as) (IAlternative _ _ as')
+      = matchAll lhs (zip as as')
+  getMatch lhs (IAs _ _ (UN n) p) (IAs fc _ (UN n') p')
+      = do ms <- getMatch lhs p p'
+           mergeMatches lhs ((n, IBindVar fc n') :: ms)
+  getMatch lhs (IAs _ _ (UN n) p) p' 
+      = do ms <- getMatch lhs p p'
+           mergeMatches lhs ((n, p') :: ms)
+  getMatch lhs (IAs _ _ _ p) p' = getMatch lhs p p'
+  getMatch lhs p (IAs _ _ _ p') = getMatch lhs p p'
+  getMatch lhs (IType _) (IType _) = pure []
+  getMatch lhs pat spec = matchFail (getFC pat)
+
+  matchAll : (lhs : Bool) -> List (RawImp, RawImp) ->
+             Core (List (String, RawImp))
+  matchAll lhs [] = pure []
+  matchAll lhs ((x, y) :: ms)
+      = do matches <- matchAll lhs ms
+           mxy <- getMatch lhs x y
+           mergeMatches lhs (mxy ++ matches)
+
+  mergeMatches : (lhs : Bool) -> List (String, RawImp) ->
+                 Core (List (String, RawImp))
+  mergeMatches lhs [] = pure []
+  mergeMatches lhs ((n, tm) :: rest)
+      = do rest' <- mergeMatches lhs rest
+           case lookup n rest' of
+                Nothing => pure ((n, tm) :: rest')
+                Just tm' =>
+                   do getMatch lhs tm tm' -- just need to know it succeeds
+                      mergeMatches lhs rest
+
+-- Get the arguments for the rewritten pattern clause of a with by looking
+-- up how the argument names matched
+getArgMatch : FC -> Bool -> RawImp -> List (String, RawImp) ->
+              Maybe (PiInfo, Name) -> RawImp
+getArgMatch ploc search warg ms Nothing = warg
+getArgMatch ploc True warg ms (Just (AutoImplicit, UN n))
+    = case lookup n ms of
+           Nothing => ISearch ploc 500
+           Just tm => tm
+getArgMatch ploc True warg ms (Just (AutoImplicit, _))
+    = ISearch ploc 500
+getArgMatch ploc search warg ms (Just (_, UN n))
+    = case lookup n ms of
+           Nothing => Implicit ploc True
+           Just tm => tm
+getArgMatch ploc search warg ms _ = Implicit ploc True
+    
+export
+getNewLHS : {auto c : Ref Ctxt Defs} ->
+            FC -> (drop : Nat) -> NestedNames vars ->
+            Name -> List (Maybe (PiInfo, Name)) ->
+            RawImp -> RawImp -> Core RawImp
+getNewLHS ploc drop nest wname wargnames lhs_raw patlhs
+    = do (mlhs_raw, wrest) <- dropWithArgs drop patlhs
+         autoimp <- isAutoImplicits
+         autoImplicits True
+         (_, lhs) <- bindNames False lhs_raw
+         (_, mlhs) <- bindNames False mlhs_raw
+         autoImplicits autoimp
+
+         let (warg :: rest) = reverse wrest
+             | _ => throw (GenericMsg ploc "Badly formed 'with' clause")
+         log 5 $ show lhs ++ " against " ++ show mlhs ++
+                 " dropping " ++ show (warg :: rest)
+         ms <- getMatch True lhs mlhs
+         log 5 $ "Matches: " ++ show ms
+         let newlhs = apply (IVar ploc wname)
+                            (map (getArgMatch ploc False warg ms) wargnames ++ rest)
+         log 5 $ "New LHS: " ++ show newlhs
+         pure newlhs
+  where
+    dropWithArgs : Nat -> RawImp -> 
+                   Core (RawImp, List RawImp)
+    dropWithArgs Z tm = pure (tm, [])
+    dropWithArgs (S k) (IApp _ f arg)
+        = do (tm, rest) <- dropWithArgs k f
+             pure (tm, arg :: rest)
+    -- Shouldn't happen if parsed correctly, but there's no guarantee that
+    -- inputs come from parsed source so throw an error.
+    dropWithArgs _ _ = throw (GenericMsg ploc "Badly formed 'with' clause")
+        
+-- Find a 'with' application on the RHS and update it
+export
+withRHS : {auto c : Ref Ctxt Defs} ->
+          FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo, Name)) ->
+          RawImp -> RawImp -> 
+          Core RawImp
+withRHS fc drop wname wargnames tm toplhs
+    = wrhs tm
+  where
+    withApply : FC -> RawImp -> List RawImp -> RawImp
+    withApply fc f [] = f
+    withApply fc f (a :: as) = withApply fc (IWithApp fc f a) as
+
+    updateWith : FC -> RawImp -> List RawImp -> Core RawImp
+    updateWith fc (IWithApp _ f a) ws = updateWith fc f (a :: ws)
+    updateWith fc tm []
+        = throw (GenericMsg fc "Badly formed 'with' application")
+    updateWith fc tm (arg :: args)
+        = do log 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
+             ms <- getMatch False toplhs tm
+             log 10 $ "Result: " ++ show ms
+             let newrhs = apply (IVar fc wname)
+                                (map (getArgMatch fc True arg ms) wargnames)
+             log 10 $ "With args for RHS: " ++ show wargnames
+             log 10 $ "New RHS: " ++ show newrhs
+             pure (withApply fc newrhs args)
+
+    mutual
+      wrhs : RawImp -> Core RawImp
+      wrhs (IPi fc c p n ty sc)
+          = pure $ IPi fc c p n !(wrhs ty) !(wrhs sc)
+      wrhs (ILam fc c p n ty sc)
+          = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)
+      wrhs (ILet fc c n ty val sc)
+          = pure $ ILet fc c n !(wrhs ty) !(wrhs val) !(wrhs sc)
+      wrhs (ICase fc sc ty clauses)
+          = pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
+      wrhs (ILocal fc decls sc)
+          = pure $ ILocal fc decls !(wrhs sc) -- TODO!
+      wrhs (IUpdate fc upds tm)
+          = pure $ IUpdate fc upds !(wrhs tm) -- TODO!
+      wrhs (IApp fc f a)
+          = pure $ IApp fc !(wrhs f) !(wrhs a)
+      wrhs (IImplicitApp fc f n a)
+          = pure $ IImplicitApp fc !(wrhs f) n !(wrhs a)
+      wrhs (IWithApp fc f a) = updateWith fc f [a]
+      wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
+      wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)
+      wrhs (IDelay fc tm) = pure $ IDelay fc !(wrhs tm)
+      wrhs (IForce fc tm) = pure $ IForce fc !(wrhs tm)
+      wrhs tm = pure tm
+
+      wrhsC : ImpClause -> Core ImpClause
+      wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
+      wrhsC c = pure c
+    
+
diff --git a/tests/Main.idr b/tests/Main.idr
index 452844b..4ed51ba 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -28,7 +28,7 @@ idrisTests
        "basic011", "basic012", "basic013", "basic014", "basic015",
        "basic016", "basic017", "basic018", "basic019", "basic020",
        "basic021", "basic022", "basic023", "basic024", "basic025",
-       "basic026", "basic027",
+       "basic026", "basic027", "basic028",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
@@ -43,12 +43,13 @@ idrisTests
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",
-       "perf001",
+       "perf001", "perf002",
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
        "record001", "record002",
        "total001", "total002", "total003", "total004", "total005",
-       "total006"]
+       "total006",
+       "with001"]
 
 typeddTests : List String
 typeddTests
diff --git a/tests/idris2/basic028/Do.idr b/tests/idris2/basic028/Do.idr
new file mode 100644
index 0000000..156f27c
--- /dev/null
+++ b/tests/idris2/basic028/Do.idr
@@ -0,0 +1,49 @@
+data Maybe a = Nothing 
+             | Just a
+
+infixl 1 >>=
+
+(>>=) : Maybe a -> (a -> Maybe b) -> Maybe b
+(>>=) Nothing k = Nothing
+(>>=) (Just x) k = k x
+
+data Nat : Type where
+   Z : Nat
+   S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z     y = y
+plus (S k) y = S (plus k y)
+
+maybeAdd' : Maybe Nat -> Maybe Nat -> Maybe Nat
+maybeAdd' x y
+    = x >>= \x' =>
+      y >>= \y' =>
+      Just (plus x' y')
+
+maybeAdd : Maybe Nat -> Maybe Nat -> Maybe Nat
+maybeAdd x y
+    = do x' <- x
+         y' <- y
+         Just (plus x' y')
+
+data Either : Type -> Type -> Type where
+     Left : a -> Either a b
+     Right : b -> Either a b
+
+mEmbed : Maybe a -> Maybe (Either String a)
+mEmbed Nothing = Just (Left "FAIL")
+mEmbed (Just x) = Just (Right x)
+
+mPatBind : Maybe Nat -> Maybe Nat -> Maybe Nat
+mPatBind x y
+    = do Right res <- mEmbed (maybeAdd x y)
+            | Left err => Just Z
+         Just res
+
+mLetBind : Maybe Nat -> Maybe Nat -> Maybe Nat
+mLetBind x y
+    = do let Just res = maybeAdd x y
+                  | Nothing => Just Z
+         Just res
+
diff --git a/tests/idris2/basic028/expected b/tests/idris2/basic028/expected
new file mode 100644
index 0000000..c76d47c
--- /dev/null
+++ b/tests/idris2/basic028/expected
@@ -0,0 +1,7 @@
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> 1/1: Building Do (Do.idr)
+Main> Just (S (S (S Z)))
+Main> Just Z
+Main> Just (S (S (S Z)))
+Main> Just Z
+Main> Bye for now!
diff --git a/tests/idris2/basic028/input b/tests/idris2/basic028/input
new file mode 100644
index 0000000..9630947
--- /dev/null
+++ b/tests/idris2/basic028/input
@@ -0,0 +1,6 @@
+:l Do.idr
+mPatBind (Just (S Z)) (Just (S (S Z)))
+mPatBind (Just (S Z)) Nothing
+mLetBind (Just (S Z)) (Just (S (S Z)))
+mLetBind (Just (S Z)) Nothing
+:q
diff --git a/tests/idris2/basic028/run b/tests/idris2/basic028/run
new file mode 100755
index 0000000..1caedf8
--- /dev/null
+++ b/tests/idris2/basic028/run
@@ -0,0 +1,5 @@
+unset IDRIS2_PATH
+
+$1 --no-prelude < input
+
+rm -rf build
diff --git a/tests/idris2/perf002/Big.idr b/tests/idris2/perf002/Big.idr
new file mode 100644
index 0000000..3c8bf15
--- /dev/null
+++ b/tests/idris2/perf002/Big.idr
@@ -0,0 +1,35 @@
+import Data.Vect
+
+test : Vect 2 () -> IO ()
+test b =
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  let i = index 1 b in
+  pure ()
+
+main : IO ()
+main = do
+  pure ()
diff --git a/tests/idris2/perf002/expected b/tests/idris2/perf002/expected
new file mode 100644
index 0000000..57c29d0
--- /dev/null
+++ b/tests/idris2/perf002/expected
@@ -0,0 +1 @@
+1/1: Building Big (Big.idr)
diff --git a/tests/idris2/perf002/run b/tests/idris2/perf002/run
new file mode 100755
index 0000000..1402531
--- /dev/null
+++ b/tests/idris2/perf002/run
@@ -0,0 +1,3 @@
+$1 --check Big.idr
+
+rm -rf build
diff --git a/tests/idris2/with001/Temp.idr b/tests/idris2/with001/Temp.idr
new file mode 100644
index 0000000..c4a60b2
--- /dev/null
+++ b/tests/idris2/with001/Temp.idr
@@ -0,0 +1,29 @@
+module Temp
+
+import Data.List
+
+safeStrHead : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
+safeStrHead s with (unpack s)
+  safeStrHead s | [] = absurd pr
+  safeStrHead s | (c::_) = c
+
+safeStrHead1 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
+safeStrHead1 s with (unpack s)
+  safeStrHead1 {pr} s | [] = absurd pr
+  safeStrHead1 s | (c::_) = c
+
+safeStrHead2 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
+safeStrHead2 s with (unpack s)
+  safeStrHead2 {pr=foo} s | [] = absurd foo
+  safeStrHead2 s | (c::_) = c
+
+safeStrHead3 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
+safeStrHead3 {pr=foo} s with (unpack s)
+  safeStrHead3 s | [] = absurd foo
+  safeStrHead3 s | (c::_) = c
+
+safeStrHead4 : (s : String) -> {pr : NonEmpty (unpack s)} -> Char
+safeStrHead4 {pr=foo} s with (unpack s)
+  safeStrHead4 {pr=bar} s | [] = absurd bar
+  safeStrHead4 s | (c::_) = c
+
diff --git a/tests/idris2/with001/expected b/tests/idris2/with001/expected
new file mode 100644
index 0000000..dc6007d
--- /dev/null
+++ b/tests/idris2/with001/expected
@@ -0,0 +1 @@
+1/1: Building Temp (Temp.idr)
diff --git a/tests/idris2/with001/run b/tests/idris2/with001/run
new file mode 100755
index 0000000..2f53866
--- /dev/null
+++ b/tests/idris2/with001/run
@@ -0,0 +1,3 @@
+$1 --check Temp.idr
+
+rm -rf build