idris 0.9.11.1 → 0.9.11.2
raw patch · 25 files changed
+936/−139 lines, 25 files
Files
- idris.cabal +2/−1
- libs/base/Network/Socket.idr +246/−0
- libs/base/base.ipkg +1/−1
- libs/neweffects/Effects.idr +9/−8
- libs/prelude/Prelude/Strings.idr +13/−0
- rts/Makefile +2/−2
- rts/idris_net.c +143/−0
- rts/idris_net.h +53/−0
- src/IRTS/CodegenJavaScript.hs +217/−61
- src/Idris/AbsSyntax.hs +82/−4
- src/Idris/AbsSyntaxTree.hs +12/−2
- src/Idris/Core/Elaborate.hs +0/−2
- src/Idris/Core/Unify.hs +18/−9
- src/Idris/Delaborate.hs +1/−1
- src/Idris/ElabDecls.hs +42/−14
- src/Idris/ElabTerm.hs +15/−3
- src/Idris/IBC.hs +8/−1
- src/Idris/ParseExpr.hs +10/−4
- src/Idris/ParseHelpers.hs +2/−1
- src/Idris/ParseOps.hs +1/−1
- src/Idris/ProofSearch.hs +14/−1
- src/Idris/REPL.hs +5/−3
- src/Util/DynamicLinker.hs +38/−18
- test/dsl002/run +1/−1
- test/proof003/run +1/−1
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.11.1+Version: 0.9.11.2 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -55,6 +55,7 @@ rts/idris_gmp.h rts/idris_main.c rts/idris_rts.h+ rts/idris_net.h rts/idris_stdfgn.h rts/libtest.c
+ libs/base/Network/Socket.idr view
@@ -0,0 +1,246 @@+-- Time to do this properly.+-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.+-- (C) SimonJF, MIT Licensed, 2014+module Network.Socket++%include C "idris_net.h"+%include C "sys/types.h" -- Pushing my luck, might need to re-export everything+%include C "sys/socket.h" +%include C "netdb.h"++%access public++ByteLength : Type+ByteLength = Int++class ToCode a where+ toCode : a -> Int++-- Socket Families.+-- The ones that people might actually use. We're not going to need US Government+-- proprietary ones...+data SocketFamily = AF_UNSPEC -- Unspecified+ | AF_INET -- IP / UDP etc. IPv4+ | AF_INET6 -- IP / UDP etc. IPv6++instance Show SocketFamily where+ show AF_UNSPEC = "AF_UNSPEC"+ show AF_INET = "AF_INET"+ show AF_INET6 = "AF_INET4"++instance ToCode SocketFamily where+ toCode AF_UNSPEC = 0+ toCode AF_INET = 2+ toCode AF_INET6 = 10++getSocketFamily : Int -> Maybe SocketFamily+getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]++-- Socket Types.+data SocketType = NotASocket -- Not a socket, used in certain operations+ | Stream -- TCP+ | Datagram -- UDP+ | RawSocket -- Raw sockets. A guy can dream.++instance Show SocketType where+ show NotASocket = "Not a socket"+ show Stream = "Stream"+ show Datagram = "Datagram"+ show Raw = "Raw"++instance ToCode SocketType where+ toCode NotASocket = 0+ toCode Stream = 1+ toCode Datagram = 2+ toCode Raw = 3++-- Protocol Number. Generally good enough to just set it to 0.+ProtocolNumber : Type+ProtocolNumber = Int++-- SocketError: Error thrown by a socket operation+SocketError : Type+SocketError = Int++-- SocketDescriptor: Native C Socket Descriptor+SocketDescriptor : Type+SocketDescriptor = Int++data SocketAddress = IPv4Addr Int Int Int Int+ | IPv6Addr -- Not implemented (yet)+ | Hostname String+ | InvalidAddress -- Used when there's a parse error++instance Show SocketAddress where+ show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])+ show IPv6Addr = "NOT IMPLEMENTED YET"+ show (Hostname host) = host+ show InvalidAddress = "Invalid"++Port : Type+Port = Int++-- Backlog used within listen() call -- number of incoming calls+BACKLOG : Int+BACKLOG = 20++-- FIXME: This *must* be pulled in from C+EAGAIN : Int +EAGAIN = 11++-- Allocates an amount of memory given by the ByteLength parameter.+-- Used to allocate a mutable pointer to be given to the Recv functions.+private+alloc : ByteLength -> IO Ptr+alloc bl = mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl++-- Frees a given pointer+private+free : Ptr -> IO ()+free ptr = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr++record Socket : Type where+ MkSocket : (descriptor : SocketDescriptor) ->+ (family : SocketFamily) ->+ (socketType : SocketType) ->+ (protocolNumber : ProtocolNumber) ->+ Socket++getErrno : IO Int+getErrno = mkForeign (FFun "idrnet_errno" [] FInt)++-- Creates a UNIX socket with the given family, socket type and protocol number.+-- Returns either a socket or an error.+socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)+socket sf st pn = do+ socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn+ if socket_res == -1 then -- error+ map Left getErrno+ else + return $ Right (MkSocket socket_res sf st pn)+++close : Socket -> IO ()+close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)++-- Binds a socket to the given socket address and port.+-- Returns 0 on success, an error code otherwise.+bind : Socket -> SocketAddress -> Port -> IO Int+bind sock addr port = do+ bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt) + (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)+ if bind_res == (-1) then -- error+ getErrno+ else return 0 -- Success++-- Connects to a given address and port.+-- Returns 0 on success, and an error number on error.+connect : Socket -> SocketAddress -> Port -> IO Int+connect sock addr port = do+ conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)+ (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)+ if conn_res == (-1) then+ getErrno+ else return 0++-- Listens on a bound socket.+listen : Socket -> IO Int+listen sock = do+ listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG+ if listen_res == (-1) then+ getErrno+ else return 0++-- Parses a textual representation of an IPv4 address into a SocketAddress+private+parseIPv4 : String -> SocketAddress+parseIPv4 str = case splitted of+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4+ _ => InvalidAddress+ where toInt' : String -> Integer+ toInt' = cast+ toInt : String -> Int+ toInt s = fromInteger $ toInt' s+ splitted : List Int+ splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)+++-- Retrieves a socket address from a sockaddr pointer+private+getSockAddr : Ptr -> IO SocketAddress+getSockAddr ptr = do+ addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr+ -- FIXME: Is this really a safe assertion? Depends where the Ptr came+ -- from!+ assert_total $ case getSocketFamily addr_family_int of+ Just AF_INET => do+ ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr+ return $ parseIPv4 ipv4_addr+ Just AF_INET6 => return IPv6Addr+ Just AF_UNSPEC => return IPv6Addr -- FIXME: Horrible hack++-- Accepts a connection from a listening socket.+accept : 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 <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr) + accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr+ if accept_res == (-1) then+ map Left getErrno+ else do+ let (MkSocket _ fam ty p_num) = sock+ sockaddr <- getSockAddr sockaddr_ptr+ free sockaddr_ptr+ return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)++send : Socket -> String -> IO (Either SocketError ByteLength)+send sock dat = do+ send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat+ if send_res == (-1) then+ map Left getErrno+ else+ return $ Right send_res++private+freeRecvStruct : Ptr -> IO ()+freeRecvStruct p = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p+++recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))+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 <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len+ recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr+ if recv_res == (-1) then do+ errno <- getErrno+ freeRecvStruct recv_struct_ptr+ return $ Left errno+ else + if recv_res == 0 then do+ freeRecvStruct recv_struct_ptr+ return $ Left 0+ else do+ payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr+ freeRecvStruct recv_struct_ptr+ return $ Right (payload, recv_res)+++-- Sends the data in a given memory location+sendBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)+sendBuf sock ptr len = do+ send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len+ if send_res == (-1) then+ map Left getErrno+ else + return $ Right send_res++recvBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)+recvBuf sock ptr len = do+ recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len+ if (recv_res == (-1)) then+ map Left getErrno+ else+ return $ Right recv_res+
libs/base/base.ipkg view
@@ -3,7 +3,7 @@ opts = "--nobasepkgs --total -i ../prelude" modules = System, - Network.Cgi,+ Network.Cgi, Network.Socket, Debug.Trace, System.Concurrency.Raw, System.Concurrency.Process,
libs/neweffects/Effects.idr view
@@ -22,10 +22,10 @@ -- A bit of syntactic sugar ('syntax' is not very flexible so we only go -- up to a small number of parameters...) +syntax "{" [inst] "}" [eff] = eff inst (\result => inst) syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff] = eff inst (\b => outst) syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)-syntax "{" [inst] "}" [eff] = eff inst (\result => inst) ---- Properties and proof construction @@ -252,13 +252,14 @@ -- yuck :) Haven't got type class instances working nicely in tactic -- proofs yet, so just brute force it.-syntax MkDefaultEnv = (| [], [default], [default, default],- [default, default, default],- [default, default, default, default],- [default, default, default, default, default],- [default, default, default, default, default, default],- [default, default, default, default, default, default, default],- [default, default, default, default, default, default, default, default] |)+syntax MkDefaultEnv = with Env+ (| [], [default], [default, default],+ [default, default, default],+ [default, default, default, default],+ [default, default, default, default, default],+ [default, default, default, default, default, default],+ [default, default, default, default, default, default, default],+ [default, default, default, default, default, default, default, default] |) run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a run {env} prog = eff env prog (\r, env => pure r)
libs/prelude/Prelude/Strings.idr view
@@ -145,3 +145,16 @@ length : String -> Nat length = fromInteger . prim__zextInt_BigInt . prim_lenString++toLower : String -> String+toLower x with (strM x)+ strToLower "" | StrNil = ""+ strToLower (strCons c cs) | (StrCons c cs) =+ strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))++toUpper : String -> String+toUpper x with (strM x)+ strToLower "" | StrNil = ""+ strToLower (strCons c cs) | (StrCons c cs) =+ strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))+
rts/Makefile view
@@ -1,9 +1,9 @@ include ../config.mk OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o \- idris_bitstring.o idris_opts.o idris_stats.o mini-gmp.o+ idris_bitstring.o idris_net.o idris_opts.o idris_stats.o mini-gmp.o HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h \- idris_bitstring.h idris_opts.h idris_stats.h mini-gmp.h+ idris_bitstring.h idris_net.h idris_opts.h idris_stats.h mini-gmp.h CFLAGS:=-fPIC $(CFLAGS) CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)
+ rts/idris_net.c view
@@ -0,0 +1,143 @@+// C-Side of the Idris network library+// (C) Simon Fowler, 2014+// MIT Licensed. Have fun!+#include "idris_net.h"+#include <arpa/inet.h>++void* idrnet_malloc(int size) {+ return malloc(size);+}++void idrnet_free(void* ptr) {+ free(ptr);+}++int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {+ struct addrinfo hints;+ struct addrinfo* address_res;+ // 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+ }++ int addr_res = getaddrinfo(host, str_port, &hints, &address_res);+ if (addr_res == -1) {+ return -1;+ }++ int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);+ if (bind_res == -1) {+ return -1;+ } ++ return 0;+}++int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {+ char str_port[8];+ sprintf(str_port, "%d", port);+ struct addrinfo hints;+ struct addrinfo* remote_host;++ // Set up hints structure for getaddrinfo+ memset(&hints, 0, sizeof(hints));+ hints.ai_family = family;+ hints.ai_socktype = socket_type;++ // Get info about the remote host (DNS lookup etc)+ int addr_res = getaddrinfo(host, str_port, &hints, &remote_host);+ if (addr_res == -1) {+ return -1;+ }++ int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);+ if (connect_res == -1) {+ return -1;+ }++ 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*) addr;+ char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);+ inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);+ return ip_addr;+}++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 = 0;+ 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) {+ return send(sockfd, data, len, 0);+}++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);+ 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 = (void*) buf;+ return (void*) res_struct;+}++int idrnet_recv_buf(int sockfd, void* buf, int len) {+ return recv(sockfd, buf, len, 0);+}++int idrnet_get_recv_res(void* res_struct) {+ return (((idrnet_recv_result*) res_struct)->result);+}++void* 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;+}+
+ rts/idris_net.h view
@@ -0,0 +1,53 @@+#ifndef IDRISNET_H+#define IDRISNET_H++#include <errno.h>+#include <netdb.h>+#include <stdbool.h>+#include <stdlib.h>+#include <stdio.h>+#include <string.h>+#include <sys/types.h>+#include <sys/socket.h>++typedef struct idrnet_recv_result {+ int result;+ void* payload;+} idrnet_recv_result;++// Memory management functions+void* idrnet_malloc(int size);+void idrnet_free(void* ptr);++// Gets value of errno+int idrnet_errno(); ++// Bind+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);++// 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);+void* idrnet_create_sockaddr();++// 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);++// Receive structure accessors+int idrnet_get_recv_res(void* res_struct);+void* idrnet_get_recv_payload(void* res_struct);+void idrnet_free_recv_struct(void* res_struct);+#endif
src/IRTS/CodegenJavaScript.hs view
@@ -20,9 +20,10 @@ import System.Directory idrNamespace :: String-idrNamespace = "__IDR__"-idrRTNamespace = "__IDRRT__"-idrLTNamespace = "__IDRLT__"+idrNamespace = "__IDR__"+idrRTNamespace = "__IDRRT__"+idrLTNamespace = "__IDRLT__"+idrCTRNamespace = "__IDRCTR__" data JSTarget = Node | JavaScript deriving Eq@@ -408,16 +409,33 @@ isJSConstant :: JS -> Bool isJSConstant js- | JSString _ <- js = True- | JSChar _ <- js = True- | JSNum _ <- js = True- | JSType _ <- js = True- | JSNull <- js = True+ | JSString _ <- js = True+ | JSChar _ <- js = True+ | JSNum _ <- js = True+ | JSType _ <- js = True+ | JSNull <- js = True+ | JSArray vals <- js = all isJSConstant vals | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True+ | otherwise = False +isJSConstantConstructor :: [String] -> JS -> Bool+isJSConstantConstructor constants js+ | isJSConstant js =+ True+ | JSArray vals <- js =+ all (isJSConstantConstructor constants) vals+ | JSNew "__IDRRT__Con" args <- js =+ all (isJSConstantConstructor constants) args+ | JSIndex (JSProj (JSIdent _) "vars") (JSNum _) <- js =+ True+ | JSIdent name <- js+ , name `elem` constants =+ True+ | otherwise = False + inlineJS :: JS -> JS inlineJS (JSReturn (JSApp (JSFunction [] err@(JSError _)) [])) = err inlineJS (JSReturn (JSApp (JSFunction ["cse"] body) [val@(JSVar _)])) =@@ -564,14 +582,14 @@ where replaceHelper :: [Int] -> JS -> JS replaceHelper tags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray []])- | tag `elem` tags = JSIdent ("__IDRCTR__" ++ show tag)+ | tag `elem` tags = JSIdent (idrCTRNamespace ++ show tag) replaceHelper tags js = transformJS (replaceHelper tags) js createConstant :: Int -> JS createConstant tag =- JSAlloc ("__IDRCTR__" ++ show tag) (Just (+ JSAlloc (idrCTRNamespace ++ show tag) (Just ( JSNew (idrRTNamespace ++ "Con") [JSNum (JSInt tag), JSArray []] )) @@ -632,33 +650,11 @@ inlineAble :: Int -> String -> [String] -> JS -> Maybe JS- inlineAble 1 fun args body+ inlineAble 1 fun args (JSReturn body) | nonRecur fun body =- inlineAble' body- where- inlineAble' :: JS -> Maybe JS- inlineAble' (- JSReturn js@(JSNew "__IDRRT__Con" [JSNum _, JSArray vals])- )- | and $ map (\x -> isJSIdent x || isJSConstant x) vals = Just js-- inlineAble' (- JSReturn js@(JSNew "__IDRRT__Cont" [JSFunction [] (- JSReturn (JSApp (JSIdent _) args)- )])- )- | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js-- inlineAble' (- JSReturn js@(JSIndex (JSProj (JSApp (JSIdent _) args) "vars") _)- )- | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js-- inlineAble' _ = Nothing-- isJSIdent js- | JSIdent _ <- js = True- | otherwise = False+ if all (<= 1) (map ($ body) (map countIDOccurences args))+ then Just body+ else Nothing inlineAble _ _ _ _ = Nothing @@ -694,6 +690,16 @@ countAll name js = sum $ map (countInvokations name) js + countIDOccurences :: String -> JS -> Int+ countIDOccurences name = foldJS match (+) 0+ where+ match :: JS -> Int+ match js+ | JSIdent ident <- js+ , name == ident = 1+ | otherwise = 0++ countInvokations :: String -> JS -> Int countInvokations name = foldJS match (+) 0 where@@ -785,10 +791,10 @@ JSSeq [ JSAlloc "ret" $ Just ( JSTernary ( (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`- (hasProp "__IDRLT__mEVAL0" "arg0")+ (hasProp "__IDRLT__EVAL" "arg0") ) (JSApp (JSIndex- (JSIdent "__IDRLT__mEVAL0")+ (JSIdent "__IDRLT__EVAL") (JSProj (JSIdent "arg0") "tag") ) [JSIdent "arg0"]@@ -811,10 +817,10 @@ , JSAlloc "ret" $ Just ( JSTernary ( (JSIdent "ev" `jsInstanceOf` jsCon) `jsAnd`- (hasProp "__IDRLT__mAPPLY0" "ev")+ (hasProp "__IDRLT__APPLY" "ev") ) (JSApp (JSIndex- (JSIdent "__IDRLT__mAPPLY0")+ (JSIdent "__IDRLT__APPLY") (JSProj (JSIdent "ev") "tag") ) [JSIdent "fn0", JSIdent "arg0", JSIdent "ev"]@@ -837,8 +843,8 @@ unfoldLookupTable :: [JS] -> [JS] unfoldLookupTable input =- let (evals, evalunfold) = unfoldLT "__IDRLT__mEVAL0" input- (applys, applyunfold) = unfoldLT "__IDRLT__mAPPLY0" evalunfold+ let (evals, evalunfold) = unfoldLT "__IDRLT__EVAL" input+ (applys, applyunfold) = unfoldLT "__IDRLT__APPLY" evalunfold js = applyunfold in adaptRuntime $ expandCons evals applys js where@@ -848,12 +854,12 @@ adaptApply var = map (jsSubst (- JSIndex (JSIdent "__IDRLT__mAPPLY0") (JSProj (JSIdent var) "tag")+ JSIndex (JSIdent "__IDRLT__APPLY") (JSProj (JSIdent var) "tag") ) (JSProj (JSIdent var) "app")) adaptEval = map (jsSubst (- JSIndex (JSIdent "__IDRLT__mEVAL0") (JSProj (JSIdent "arg0") "tag")+ JSIndex (JSIdent "__IDRLT__EVAL") (JSProj (JSIdent "arg0") "tag") ) (JSProj (JSIdent "arg0") "eval")) @@ -893,8 +899,8 @@ where expandCons' :: JS -> JS expandCons' (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray args])- | evalid <- getId "__IDRLT__mEVAL0" tag evals- , applyid <- getId "__IDRLT__mAPPLY0" tag applys =+ | evalid <- getId "__IDRLT__EVAL" tag evals+ , applyid <- getId "__IDRLT__APPLY" tag applys = JSNew "__IDRRT__Con" [ JSNum (JSInt tag) , maybe JSNull JSIdent evalid , maybe JSNull JSIdent applyid@@ -911,8 +917,8 @@ ltIdentifier :: String -> Int -> String- ltIdentifier "__IDRLT__mEVAL0" id = idrLTNamespace ++ "EVAL" ++ show id- ltIdentifier "__IDRLT__mAPPLY0" id = idrLTNamespace ++ "APPLY" ++ show id+ ltIdentifier "__IDRLT__EVAL" id = idrLTNamespace ++ "EVAL" ++ show id+ ltIdentifier "__IDRLT__APPLY" id = idrLTNamespace ++ "APPLY" ++ show id extractLT :: String -> [JS] -> (JS, [JS])@@ -1011,6 +1017,158 @@ | otherwise = js +extractLocalConstructors :: [JS] -> [JS]+extractLocalConstructors js =+ concatMap extractLocalConstructors' js+ where+ globalCons :: [String]+ globalCons = concatMap (getGlobalCons) js+++ extractLocalConstructors' :: JS -> [JS]+ extractLocalConstructors' js@(JSAlloc fun (Just (JSFunction args body))) =+ map allocCon cons ++ [foldr (uncurry jsSubst) js (reverse cons)]+ where+ cons :: [(JS, JS)]+ cons = zipWith genName (foldJS match (++) [] body) [1..]+ where+ genName :: JS -> Int -> (JS, JS)+ genName js id =+ (js, JSIdent $ idrCTRNamespace ++ fun ++ "_" ++ show id)++ match :: JS -> [JS]+ match js+ | JSNew "__IDRRT__Con" args <- js+ , all isConstant args = [js]+ | otherwise = []+++ allocCon :: (JS, JS) -> JS+ allocCon (js, JSIdent name) =+ JSAlloc name (Just js)+++ isConstant :: JS -> Bool+ isConstant js+ | JSNew "__IDRRT__Con" args <- js+ , all isConstant args =+ True+ | otherwise =+ isJSConstantConstructor globalCons js++ extractLocalConstructors' js = [js]+++ getGlobalCons :: JS -> [String]+ getGlobalCons js = foldJS match (++) [] js+ where+ match :: JS -> [String]+ match js+ | (JSAlloc name (Just (JSNew "__IDRRT__Con" _))) <- js =+ [name]+ | otherwise =+ []+++evalCons :: [JS] -> [JS]+evalCons js =+ map (collapseCont . collapseTC . expandProj . evalCons') js+ where+ cons :: [(String, JS)]+ cons = concatMap getGlobalCons js++ evalCons' :: JS -> JS+ evalCons' js = transformJS match js+ where+ match :: JS -> JS+ match (JSApp (JSIdent "__IDRRT__EVALTC") [arg])+ | JSIdent name <- arg+ , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =+ arg++ match (JSApp (JSIdent "__IDR__mEVAL0") [arg])+ | JSIdent name <- arg+ , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =+ arg++ match js = transformJS match js+++ lookupConstructor :: String -> [(String, JS)] -> Maybe JS+ lookupConstructor ctr cons+ | Just (JSIdent name) <- lookup ctr cons = lookupConstructor name cons+ | Just con@(JSNew _ _) <- lookup ctr cons = Just con+ | otherwise = Nothing+++ expandProj :: JS -> JS+ expandProj js = transformJS match js+ where+ match :: JS -> JS+ match (+ JSIndex (+ JSProj (JSIdent name) "vars"+ ) (+ JSNum (JSInt idx)+ )+ )+ | Just (JSNew _ [_, _, _, JSArray args]) <- lookup name cons =+ args !! idx++ match js = transformJS match js+++ collapseTC :: JS -> JS+ collapseTC js = transformJS match js+ where+ match :: JS -> JS+ match (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (+ JSReturn (JSIdent name)+ )])+ | Just _ <- lookup name cons = (JSIdent name)++ match js = transformJS match js+++ collapseCont :: JS -> JS+ collapseCont js = transformJS match js+ where+ match :: JS -> JS+ match (JSNew "__IDRRT__Cont" [JSFunction [] (+ JSReturn ret@(JSNew "__IDRRT__Cont" [JSFunction [] _])+ )]) = collapseCont ret+++ match (JSNew "__IDRRT__Cont" [JSFunction [] (+ JSReturn (JSIdent name)+ )]) = JSIdent name++ match (JSNew "__IDRRT__Cont" [JSFunction [] (+ JSReturn ret@(JSNew "__IDRRT__Con" [_, _, _, JSArray args])+ )])+ | all collapsable args = ret+ where+ collapsable :: JS -> Bool+ collapsable (JSIdent _) = True+ collapsable js = isJSConstantConstructor (map fst cons) js+++ match js = transformJS match js+++getGlobalCons :: JS -> [(String, JS)]+getGlobalCons js = foldJS match (++) [] js+ where+ match :: JS -> [(String, JS)]+ match js+ | (JSAlloc name (Just con@(JSNew "__IDRRT__Con" _))) <- js =+ [(name, con)]+ | (JSAlloc name (Just con@(JSIdent _))) <- js =+ [(name, con)]+ | otherwise =+ []++ codegenJavaScript :: JSTarget -> [(Name, SDecl)]@@ -1067,7 +1225,9 @@ , map removeInstanceChecks , inlineFunctions , map reduceContinuations+ , extractLocalConstructors , unfoldLookupTable+ , evalCons ] prelude :: [JS]@@ -1227,7 +1387,7 @@ lookup t = (JSApp (JSIndex (JSIdent t) (JSProj (JSIdent lvar) "tag")) [JSIdent "fn0", JSIdent "arg0", JSIdent lvar]) in- [ lookupTable [(var, "chk")] var cases+ [ lookupTable "APPLY" [(var, "chk")] var cases , jsDecl $ JSFunction ["fn0", "arg0"] ( JSSeq [ JSAlloc "__var_0" (Just $ JSIdent "fn0") , JSAlloc (translateVariableName var) (@@ -1235,8 +1395,8 @@ ) , JSReturn $ (JSTernary ( (JSVar var `jsInstanceOf` jsCon) `jsAnd`- (hasProp lookupTableName (translateVariableName var))- ) (lookup lookupTableName) JSNull)+ (hasProp (idrLTNamespace ++ "APPLY") (translateVariableName var))+ ) (lookup (idrLTNamespace ++ "APPLY")) JSNull) ] ) ]@@ -1244,13 +1404,13 @@ | (MN _ ev) <- name , (SChkCase var cases) <- body , ev == txt "EVAL" =- [ lookupTable [] var cases+ [ lookupTable "EVAL" [] var cases , jsDecl $ JSFunction ["arg0"] (JSReturn $ JSTernary ( (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`- (hasProp lookupTableName "arg0")+ (hasProp (idrLTNamespace ++ "EVAL") "arg0") ) (JSApp- (JSIndex (JSIdent lookupTableName) (JSProj (JSIdent "arg0") "tag"))+ (JSIndex (JSIdent (idrLTNamespace ++ "EVAL")) (JSProj (JSIdent "arg0") "tag")) [JSIdent "arg0"] ) (JSIdent "arg0") )@@ -1276,13 +1436,9 @@ getTag _ = Nothing - lookupTableName :: String- lookupTableName = idrLTNamespace ++ translateName name--- lookupTable :: [(LVar, String)] -> LVar -> [SAlt] -> JS- lookupTable aux var cases =- JSAlloc lookupTableName $ Just (+ lookupTable :: String -> [(LVar, String)] -> LVar -> [SAlt] -> JS+ lookupTable table aux var cases =+ JSAlloc (idrLTNamespace ++ table) $ Just ( JSApp (JSFunction [] ( JSSeq $ [ JSAlloc "t" $ Just (JSArray [])
src/Idris/AbsSyntax.hs view
@@ -66,10 +66,13 @@ addDyLib :: [String] -> Idris (Either DynamicLib String) addDyLib libs = do i <- getIState let ls = idris_dynamic_libs i+ let importdirs = opt_importdirs (idris_options i) case mapMaybe (findDyLib ls) libs of x:_ -> return (Left x) [] -> do- handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs+ handle <- lift . lift .+ mapM (\l -> catchIO (tryLoadLib importdirs l)+ (\_ -> return Nothing)) $ libs case msum handle of Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++ concat (intersperse "," libs) ++ "\"")@@ -155,7 +158,77 @@ = do i <- getIState putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) } --- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.+addTyInferred :: Name -> Idris ()+addTyInferred n + = do i <- getIState+ putIState $ i { idris_tyinfodata =+ addDef n TIPartial (idris_tyinfodata i) }++addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()+addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts+ mapM_ addConstraint ts+ return ()+ where addConstraint (x, y) = findMVApps x y++ findMVApps x y+ = do let (fx, argsx) = unApply x+ let (fy, argsy) = unApply y+ if (not (fx == fy)) + then do+ tryAddMV fx y+ tryAddMV fy x+ else mapM_ addConstraint (zip argsx argsy)++ tryAddMV (P _ mv _) y =+ do ist <- get+ case lookup mv (idris_metavars ist) of+ Just _ -> addConstraintRule mv y+ _ -> return ()+ tryAddMV _ _ = return ()++ addConstraintRule :: Name -> Term -> Idris ()+ addConstraintRule n t + = do ist <- get+ logLvl 1 $ "TI constraint: " ++ show (n, t)+ case lookupCtxt n (idris_tyinfodata ist) of+ [TISolution ts] -> + do mapM_ (checkConsistent t) ts+ let ti' = addDef n (TISolution (t : ts)) + (idris_tyinfodata ist)+ put $ ist { idris_tyinfodata = ti' }+ _ -> + do let ti' = addDef n (TISolution [t]) + (idris_tyinfodata ist)+ put $ ist { idris_tyinfodata = ti' }++ -- Check a solution is consistent with previous solutions+ -- Meaning: If heads are both data types, they had better be the+ -- same.+ checkConsistent :: Term -> Term -> Idris ()+ checkConsistent x y =+ do let (fx, _) = unApply x+ let (fy, _) = unApply y+ case (fx, fy) of+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n) + (P (TCon _ _) n _, Constant _) -> errWhen True+ (Constant _, P (TCon _ _) n' _) -> errWhen True+ (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n) + _ -> return ()++ where errWhen True + = throwError (At fc + (CantUnify False x y (Msg "") [] 0))+ errWhen False = return ()++isTyInferred :: Name -> Idris Bool+isTyInferred n+ = do i <- getIState+ case lookupCtxt n (idris_tyinfodata i) of+ [TIPartial] -> return True+ _ -> return False++-- | Adds error handlers for a particular function and argument. If names are+-- ambiguous, all matching handlers are updated. addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris () addFunctionErrorHandlers f arg hs = do i <- getIState@@ -425,14 +498,19 @@ iRender :: Doc a -> Idris (SimpleDoc a) iRender d = do w <- getWidth+ ist <- getIState+ let ideSlave = case idris_outputmode ist of+ IdeSlave _ -> True+ _ -> False case w of InfinitelyWide -> return $ renderPretty 1.0 1000000000 d ColsWide n -> return $ if n < 1 then renderPretty 1.0 1000000000 d else renderPretty 0.8 n d- AutomaticWidth -> do width <- runIO getScreenWidth- return $ renderPretty 0.8 width d+ AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d+ | otherwise -> do width <- runIO getScreenWidth+ return $ renderPretty 0.8 width d ihPrintResult :: Handle -> String -> Idris () ihPrintResult h s = do i <- getIState
src/Idris/AbsSyntaxTree.hs view
@@ -112,6 +112,7 @@ idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos idris_calledgraph :: Ctxt [Name], idris_docstrings :: Ctxt String,+ idris_tyinfodata :: Ctxt TIData, idris_totcheck :: [(FC, Name)], -- names to check totality on idris_defertotcheck :: [(FC, Name)], -- names to check at the end idris_options :: IOption,@@ -216,7 +217,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext emptyContext- emptyContext+ emptyContext emptyContext [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty@@ -811,6 +812,12 @@ deriving instance NFData ClassInfo !-} +-- Type inference data++data TIData = TIPartial -- ^ a function with a partially defined type+ | TISolution [Term] -- ^ possible solutions to a metavariable in a type + deriving Show+ -- An argument is conditionally forceable iff its forceability -- depends on the collapsibility of the whole type. data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)@@ -952,7 +959,10 @@ getInferTerm (App (App _ _) tm) = tm getInferTerm tm = tm -- error ("getInferTerm " ++ show tm) -getInferType (Bind n b sc) = Bind n b $ getInferType sc+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc+ where toTy (Lam t) = Pi t+ toTy (PVar t) = PVTy t+ toTy b = b getInferType (App (App _ ty) _) = ty
src/Idris/Core/Elaborate.hs view
@@ -466,8 +466,6 @@ do args <- prepare_apply fn (map fst imps) -- _Don't_ solve the arguments we're specifying by hand. -- (remove from unified list before calling end_unify)- -- HMMM: Actually, if we get it wrong, the typechecker will complain!- -- so do nothing hs <- get_holes ES (p, a) s prev <- get let dont = head hs : dontunify p ++
src/Idris/Core/Unify.hs view
@@ -257,7 +257,7 @@ then unifyTmpFail xtm tm else do sc 1 checkCycle bnames (x, tm)- | not (injective xtm) && injective tm = unifyFail xtm tm+ | not (injective xtm) && injective tm = unifyTmpFail xtm tm un' fn bnames tm ytm@(P _ y _) | holeIn env y || y `elem` holes = do UI s f <- get@@ -268,7 +268,7 @@ then unifyTmpFail tm ytm else do sc 1 checkCycle bnames (y, tm)- | not (injective ytm) && injective tm = unifyFail ytm tm+ | not (injective ytm) && injective tm = unifyTmpFail tm ytm un' fn bnames (V i) (P _ x _) | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return [] un' fn bnames (P _ x _) (V i)@@ -379,9 +379,10 @@ unArgs vs xs ys metavarApp tm = let (f, args) = unApply tm in- metavar f &&- all (\x -> metavarApp x) args- && nub args == args+ (metavar f &&+ all (\x -> metavarApp x) args+ && nub args == args) ||+ globmetavar tm metavarArgs tm = let (f, args) = unApply tm in all (\x -> metavar x || inenv x) args && nub args == args@@ -413,14 +414,22 @@ rigid (P (DCon _ _) _ _) = True rigid (P (TCon _ _) _ _) = True- rigid t@(P Ref _ _) = inenv t+ rigid t@(P Ref _ _) = inenv t || globmetavar t rigid (Constant _) = True rigid (App f a) = rigid f && rigid a- rigid t = not (metavar t)+ rigid t = not (metavar t) || globmetavar t + globmetavar t = case unApply t of+ (P _ x _, _) ->+ case lookupDef x ctxt of+ [TyDecl _ _] -> True+ _ -> False+ _ -> False+ metavar t = case t of- P _ x _ -> (x `elem` holes || holeIn env x) &&- not (x `elem` dont)+ P _ x _ -> ((x `elem` holes || holeIn env x) &&+ not (x `elem` dont))+ || globmetavar t _ -> False pat t = case t of P _ x _ -> x `elem` holes || patIn env x
src/Idris/Delaborate.hs view
@@ -151,7 +151,7 @@ _ -> line <> line <> text "Specifically:" <> indented (pprintErr' i e) <> if (opt_errContext (idris_options i)) then text $ showSc i sc else empty-pprintErr' i (CantConvert x y env) =+pprintErr' i (CantConvert x y env) = trace (show (x,y)) $ text "Can't convert" <> indented (pprintTerm i (delab i x)) <$> text "with" <> indented (pprintTerm i (delab i y)) <> if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
src/Idris/ElabDecls.hs view
@@ -49,10 +49,19 @@ addConstraints fc cs return (tm, ty) -checkDef fc ns = do ctxt <- getContext- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t- return (n, (i, top, t'))) ns +checkDef fc ns = checkAddDef False True fc ns++checkAddDef add toplvl fc [] = return []+checkAddDef add toplvl fc ((n, (i, top, t)) : ns) + = do ctxt <- getContext+ (t', _) <- recheckC fc [] t+ when add $ addDeferred [(n, (i, top, t, toplvl))]+ ns' <- checkAddDef add toplvl fc ns+ return ((n, (i, top, t')) : ns')+-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t+-- return (n, (i, top, t'))) ns+ -- | Elaborate a top-level type declaration - for example, "foo : Int -> Int". elabType :: ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris Type@@ -76,9 +85,12 @@ ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) [] (errAt "type of " n (erun fc (build i info False [] n ty)))- ds <- checkDef fc defer- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds- addDeferred ds'+ ds <- checkAddDef True False fc defer+ -- if the type is not complete, note that we'll need to infer+ -- things later (for solving metavariables)+ when (not (null ds)) $ addTyInferred n+-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds+-- addDeferred ds' mapM_ (elabCaseBlock info opts) is ctxt <- getContext logLvl 5 $ "Rechecking"@@ -630,7 +642,7 @@ -- Elaborate the provider term to TT and check that the type matches (e, et) <- elabVal toplevel False tm- unless (isProviderOf ty' et) $+ unless (isProviderOf (normalise ctxt [] ty') et) $ ifail $ "Expected provider type IO (Provider (" ++ show ty' ++ "))" ++ ", got " ++ show et ++ " instead." @@ -1262,6 +1274,7 @@ -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- getIState+ inf <- isTyInferred fname -- get the parameters first, to pass through to any where block let fn_ty = case lookupTy fname (tt_ctxt i) of [t] -> t@@ -1275,16 +1288,25 @@ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs) logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is)) - ((lhs', dlhs, []), _) <-+ (((lhs', dlhs, []), probs), _) <- tclift $ elaborate ctxt (sMN 0 "patLHS") infP []- (errAt "left hand side of " fname- (erun fc (buildTC i info True opts fname (infTerm lhs))))+ (do res <- errAt "left hand side of " fname+ (erun fc (buildTC i info True opts fname (infTerm lhs)))+ probs <- get_probs+ return (res, probs))++ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)+ let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' logLvl 3 ("Elaborated: " ++ show lhs_tm) logLvl 3 ("Elaborated type: " ++ show lhs_ty) - (clhs_c, clhsty) <- recheckC fc [] lhs_tm+ -- If we're inferring metavariables in the type, don't recheck,+ -- because we're only doing this to try to work out those metavariables+ (clhs_c, clhsty) <- if not inf+ then recheckC fc [] lhs_tm+ else return (lhs_tm, lhs_ty) let clhs = normalise ctxt [] clhs_c logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))@@ -1319,7 +1341,7 @@ logLvl 2 $ "RHS: " ++ showTmImpls rhs ctxt <- getContext -- new context with where block added logLvl 5 "STARTING CHECK"- ((rhs', defer, is), _) <-+ ((rhs', defer, is, probs), _) <- tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty [] (do pbinds lhs_tm setNextName @@ -1332,7 +1354,11 @@ mapM_ (elabCaseHole aux) hs tt <- get_term let (tm, ds) = runState (collectDeferred (Just fname) tt) []- return (tm, ds, is))+ probs <- get_probs+ return (tm, ds, is, probs))++ when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)+ logLvl 5 "DONE CHECK" logLvl 2 $ "---> " ++ show rhs' when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)@@ -1352,7 +1378,9 @@ ctxt <- getContext logLvl 5 $ "Rechecking" logLvl 6 $ " ==> " ++ show (forget rhs')- (crhs, crhsty) <- recheckC fc [] rhs'+ (crhs, crhsty) <- if not inf + then recheckC fc [] rhs'+ else return (rhs', clhsty) logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty case converts ctxt [] clhsty crhsty of OK _ -> return ()
src/Idris/ElabTerm.hs view
@@ -11,6 +11,7 @@ import Idris.Core.Elaborate hiding (Tactic(..)) import Idris.Core.TT import Idris.Core.Evaluate+import Idris.Core.Unify import Idris.Core.Typecheck (check) import Control.Applicative ((<$>))@@ -46,6 +47,10 @@ ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl]) build ist info pattern opts fn tm = do elab ist info pattern opts fn tm+ let tmIn = tm+ let inf = case lookupCtxt fn (idris_tyinfodata ist) of+ [TIPartial] -> True+ _ -> False ivs <- get_instances hs <- get_holes ptm <- get_term@@ -70,7 +75,8 @@ probs <- get_probs case probs of [] -> return ()- ((_,_,_,e):es) -> lift (Error e)+ ((_,_,_,e):es) -> if inf then return ()+ else lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred (Just fn) tt) []@@ -87,13 +93,18 @@ buildTC ist info pattern opts fn tm = do -- set name supply to begin after highest index in tm let ns = allNamesIn tm+ let tmIn = tm+ let inf = case lookupCtxt fn (idris_tyinfodata ist) of+ [TIPartial] -> True+ _ -> False initNextNameFrom ns elab ist info pattern opts fn tm probs <- get_probs tm <- get_term case probs of [] -> return ()- ((_,_,_,e):es) -> lift (Error e)+ ((_,_,_,e):es) -> if inf then return ()+ else lift (Error e) is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred (Just fn) tt) []@@ -841,7 +852,8 @@ Term -> State [(Name, (Int, Maybe Name, Type))] Term collectDeferred top (Bind n (GHole i t) app) = do ds <- get- when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)+ t' <- collectDeferred top t+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))]) collectDeferred top app collectDeferred top (Bind n b t) = do b' <- cdb b t' <- collectDeferred top t
src/Idris/IBC.hs view
@@ -26,7 +26,7 @@ ibcVersion :: Word8-ibcVersion = 58+ibcVersion = 59 data IBCFile = IBCFile { ver :: Word8,@@ -1650,6 +1650,10 @@ put x1 PNoImplicits x1 -> do putWord8 36 put x1+ PDisamb x1 x2 -> do putWord8 37+ put x1+ put x2+ get = do i <- getWord8 case i of@@ -1759,6 +1763,9 @@ return (PUnifyLog x1) 36 -> do x1 <- get return (PNoImplicits x1)+ 37 -> do x1 <- get+ x2 <- get+ return (PDisamb x1 x2) _ -> error "Corrupted binary data for PTerm" instance (Binary t) => Binary (PTactic' t) where
src/Idris/ParseExpr.hs view
@@ -70,8 +70,14 @@ | InternalExpr; @ -}-expr' :: SyntaxInfo -> IdrisParser PTerm-expr' syn = try (externalExpr syn)+expr' syn = doexpr' syn+-- = do l <- restOfLine+-- f <- getFC+-- e <- trace (show (f, l)) $ doexpr' syn+-- return e++doexpr' :: SyntaxInfo -> IdrisParser PTerm+doexpr' syn = try (externalExpr syn) <|> internalExpr syn <?> "expression" @@ -181,6 +187,7 @@ | Let | RewriteTerm | Pi+ | CaseExpr | DoBlock ; @@@ -199,6 +206,7 @@ <|> rewriteTerm syn <|> try(pi syn) <|> doBlock syn+ <|> caseExpr syn <|> simpleExpr syn <?> "expression" @@ -263,7 +271,6 @@ | 'refl' ('{' Expr '}')? | ProofExpr | TacticsExpr- | CaseExpr | FnName | List | Comprehension@@ -290,7 +297,6 @@ <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t)) <|> proofExpr syn <|> tacticsExpr syn- <|> caseExpr syn <|> do reserved "Type"; return PType <|> try (do c <- constant fc <- getFC
src/Idris/ParseHelpers.hs view
@@ -260,7 +260,8 @@ -- | Parses an operator operator :: MonadicParsing m => m String operator = do op <- token . some $ operatorLetter- when (op == ":") $ fail "(:) is not a valid operator"+ when (op `elem` [":", "=>", "->", "<-", "=", "?="]) $ + fail $ op ++ " is not a valid operator" return op {- * Position helpers -}
src/Idris/ParseOps.hs view
@@ -39,7 +39,7 @@ [[backtick], [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight], [binary "=" PEq AssocLeft],- [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]+ [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]] -- | Calculates table for fixtiy declarations toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
src/Idris/ProofSearch.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE PatternGuards #-}+ module Idris.ProofSearch(trivial, proofSearch) where import Idris.Core.Elaborate hiding (Tactic(..))@@ -36,9 +38,20 @@ proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] -> IState -> ElabD ()-proofSearch elab fn nroot hints ist = psRec maxDepth+proofSearch elab fn nroot hints ist + = case lookupCtxt nroot (idris_tyinfodata ist) of+ [TISolution ts] -> findInferredTy ts+ _ -> psRec maxDepth where maxDepth = 6++ findInferredTy (t : _) = elab (delab ist (toUN t)) ++ toUN t@(P nt (MN i n) ty) + | ('_':xs) <- str n = t+ | otherwise = P nt (UN n) ty+ toUN (App f a) = App (toUN f) (toUN a)+ toUN t = t psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached" psRec d = try' (trivial elab ist)
src/Idris/REPL.hs view
@@ -8,6 +8,7 @@ import Idris.ElabDecls import Idris.ElabTerm import Idris.Error+import Idris.ErrReverse import Idris.Delaborate import Idris.Prover import Idris.Parser@@ -486,7 +487,7 @@ where showMetavarInfo imp ist n i = case lookupTy n (tt_ctxt ist) of- (ty:_) -> putTy imp ist i [] (delab ist ty)+ (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty)) putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation putTy imp ist 0 bnd sc = putGoal imp ist bnd sc putTy imp ist i bnd (PPi _ n t sc)@@ -894,8 +895,9 @@ _ -> iPrintError $ "Ambiguous name" process h fn (DynamicLink l) = do i <- getIState- let lib = trim l- handle <- lift . lift $ tryLoadLib lib+ let importdirs = opt_importdirs (idris_options i)+ lib = trim l+ handle <- lift . lift $ tryLoadLib importdirs lib case handle of Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\"" Just x -> do let libs = idris_dynamic_libs i
src/Util/DynamicLinker.hs view
@@ -1,7 +1,7 @@ -- | Platform-specific dynamic linking support. Add new platforms to this file -- through conditional compilation. {-# LANGUAGE ExistentialQuantification, CPP #-}-module Util.DynamicLinker where+module Util.DynamicLinker (ForeignFun(..), DynamicLib(..), tryLoadLib, tryLoadFn) where #ifdef IDRIS_FFI import Foreign.LibFFI@@ -9,11 +9,13 @@ import System.Directory #ifndef WINDOWS import System.Posix.DynamicLinker+import System.FilePath.Posix ((</>)) #else import qualified Control.Exception as Exception (catch, IOException) import System.Win32.DLL import System.Win32.Types type DL = HMODULE+import System.FilePath.Windows ((</>)) #endif hostDynamicLibExt :: String@@ -45,14 +47,27 @@ instance Eq DynamicLib where (Lib a _) == (Lib b _) = a == b +firstExisting :: [FilePath] -> IO (Maybe FilePath)+firstExisting [] = return Nothing+firstExisting (f:fs) = do exists <- doesFileExist f+ if exists+ then return (Just f)+ else firstExisting fs++libFileName :: [FilePath] -> String -> IO String+libFileName dirs lib = do let names = [lib, lib ++ "." ++ hostDynamicLibExt]+ cwd <- getCurrentDirectory+ found <- firstExisting $+ map ("."</>) names ++ [d </> f | d <- cwd:dirs, f <- names]+ return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found+ #ifndef WINDOWS-tryLoadLib :: String -> IO (Maybe DynamicLib)-tryLoadLib lib = do exactName <- doesFileExist lib- let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt- handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]- if undl handle == nullPtr- then return Nothing- else return . Just $ Lib lib handle+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)+tryLoadLib dirs lib = do filename <- libFileName dirs lib+ handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]+ if undl handle == nullPtr+ then return Nothing+ else return . Just $ Lib lib handle tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)@@ -61,13 +76,12 @@ then return Nothing else return . Just $ Fun fn cFn #else-tryLoadLib :: String -> IO (Maybe DynamicLib)-tryLoadLib lib = do exactName <- doesFileExist lib- let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt- handle <- Exception.catch (loadLibrary filename) nullPtrOnException- if handle == nullPtr- then return Nothing- else return . Just $ Lib lib handle+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)+tryLoadLib dirs lib = do filename <- libFileName dirs lib+ handle <- Exception.catch (loadLibrary filename) nullPtrOnException+ if handle == nullPtr+ then return Nothing+ else return . Just $ Lib lib handle where nullPtrOnException :: Exception.IOException -> IO DL nullPtrOnException e = return nullPtr -- `show e` will however give broken error message@@ -86,11 +100,17 @@ } deriving Eq -tryLoadLib :: String -> IO (Maybe DynamicLib)-tryLoadLib lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."- return Nothing+data ForeignFun = forall a. Fun { fun_name :: String+ , fun_handle :: ()+ } +tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)+tryLoadLib fps lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."+ return Nothing +tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)+tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."+ return Nothing #endif
test/dsl002/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash idris $@ test014.idr -o test014 ./test014-rm -f test014 resimp.ibc test014.ibc+rm -f test014 Resimp.ibc test014.ibc
test/proof003/run view
@@ -1,4 +1,4 @@ #!/usr/bin/env bash idris $@ test015.idr -o test015 ./test015-rm -f test015 parity.ibc test015.ibc+rm -f test015 Parity.ibc test015.ibc