edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-10 06:05:31 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/edwinb/Idris2

Browse Source
This commit is contained in:
Arnaud Bailly 2019-08-02 07:08:34 +02:00
commit b682accc0b
No known key found for this signature in database
GPG Key ID: 389CC2BC5448321E
37 changed files with 1758 additions and 199 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -6,6 +6,8 @@
idris2
runtests
docs/_build/
libs/**/build
tests/**/output

8
Makefile
View File

@ -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

46
Notes/Directives.md
View File

@ -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)`.

3
docs/conf.py
View File

@ -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'

1
idris2.ipkg
View File

@ -111,6 +111,7 @@ modules =
TTImp.TTImp,
TTImp.Unelab,
TTImp.Utils,
TTImp.WithClause,
Utils.Binary,
Utils.Shunting,

4
libs/base/Data/Fin.idr
View File

@ -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

47
libs/base/Data/List.idr
View File

@ -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) ->

11
libs/base/Data/Strings.idr
View File

@ -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

57
libs/network/Echo.idr Normal file
View File

@ -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

61
libs/network/Makefile Normal file
View File

@ -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

223
libs/network/Network/Socket.idr Normal file
View File

@ -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)

214
libs/network/Network/Socket/Data.idr Normal file
View File

@ -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

190
libs/network/Network/Socket/Raw.idr Normal file
View File

@ -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)

4
libs/network/expected Normal file
View File

@ -0,0 +1,4 @@
Client sent 12 bytes
Received: hello world!
Server sent 18 bytes
Received: echo: hello world!

383
libs/network/idris_net.c Normal file
View File

@ -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;
}

98
libs/network/idris_net.h Normal file
View File

@ -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

10
libs/network/lib-tests Executable file
View File

@ -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

5
libs/network/network.ipkg Normal file
View File

@ -0,0 +1,5 @@
package network
modules = Network.Socket,
Network.Socket.Data,
Network.Socket.Raw

41
libs/network/test.c Normal file
View File

@ -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;
}

4
libs/prelude/Prelude.idr
View File

@ -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

12
src/Idris/Elab/Interface.idr
View File

@ -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

4
src/Idris/Main.idr
View File

@ -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

9
src/TTImp/Elab/Binders.idr
View File

@ -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))

126
src/TTImp/ProcessDef.idr
View File

@ -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)

59
src/TTImp/Utils.idr
View File

@ -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

189
src/TTImp/WithClause.idr Normal file
View File

@ -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

7
tests/Main.idr
View File

@ -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

49
tests/idris2/basic028/Do.idr Normal file
View File

@ -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

7
tests/idris2/basic028/expected Normal file
View File

@ -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!

6
tests/idris2/basic028/input Normal file
View File

@ -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

5
tests/idris2/basic028/run Executable file
View File

@ -0,0 +1,5 @@
unset IDRIS2_PATH
$1 --no-prelude < input
rm -rf build

35
tests/idris2/perf002/Big.idr Normal file
View File

@ -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 ()

1
tests/idris2/perf002/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Big (Big.idr)

3
tests/idris2/perf002/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check Big.idr
rm -rf build

29
tests/idris2/with001/Temp.idr Normal file
View File

@ -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

1
tests/idris2/with001/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Temp (Temp.idr)

3
tests/idris2/with001/run Executable file
View File

@ -0,0 +1,3 @@
$1 --check Temp.idr
rm -rf build