idris 0.9.20 → 0.9.20.1
raw patch · 27 files changed
+320/−198 lines, 27 files
Files
- idris.cabal +9/−1
- rts/Makefile +4/−3
- rts/idris_heap.c +12/−12
- rts/idris_heap.h +2/−2
- rts/idris_net.c +21/−24
- rts/idris_stdfgn.c +16/−6
- rts/windows/idris_net.c +6/−7
- rts/windows/idris_stdfgn.c +0/−82
- src/Idris/CaseSplit.hs +1/−1
- src/Idris/Core/Elaborate.hs +52/−3
- src/Idris/Core/ProofState.hs +10/−0
- src/Idris/DSL.hs +4/−1
- src/Idris/Elab/Clause.hs +0/−23
- src/Idris/Elab/Term.hs +43/−31
- src/Idris/REPL.hs +2/−1
- test/basic002/test006.idr +1/−1
- test/interactive011/expected +3/−0
- test/interactive011/input +2/−0
- test/interactive011/interactive011.idr +11/−0
- test/interactive011/run +3/−0
- test/interactive012/expected +33/−0
- test/interactive012/input +9/−0
- test/interactive012/interactive012.idr +26/−0
- test/interactive012/run +3/−0
- test/reg001/reg001.idr +26/−0
- test/tutorial006/run +1/−0
- test/tutorial006/tutorial006c.idr +20/−0
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.20+Version: 0.9.20.1 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -541,6 +541,14 @@ test/interactive010/expected test/interactive010/input test/interactive010/run+ test/interactive011/expected+ test/interactive011/input+ test/interactive011/run+ test/interactive011/*.idr+ test/interactive012/expected+ test/interactive012/input+ test/interactive012/run+ test/interactive012/*.idr test/io001/run test/io001/*.idr
rts/Makefile view
@@ -1,7 +1,8 @@ include ../config.mk OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \- idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o getline.o+ idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o mini-gmp.o \+ getline.o HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \ idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \ idris_utf8.h getline.h@@ -19,10 +20,10 @@ endif ifeq ($(OS), windows)- OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o+ OBJS += windows/idris_net.o windows/win_utils.o else CFLAGS += -fPIC- OBJS += idris_stdfgn.o idris_net.o+ OBJS += idris_net.o endif LIBTARGET = libidris_rts.a
rts/idris_heap.c view
@@ -7,11 +7,11 @@ /* Used for initializing the heap. */-void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) +void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) {- char * mem = malloc(heap_size); + char * mem = malloc(heap_size); if (mem == NULL) {- fprintf(stderr, + fprintf(stderr, "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n", heap_size); exit(EXIT_FAILURE);@@ -37,8 +37,8 @@ void free_heap(Heap * h) { free(h->heap); - if (h->old != NULL) { - free(h->old); + if (h->old != NULL) {+ free(h->old); } } @@ -47,7 +47,7 @@ /******************** Heap testing ********************************************/ void heap_check_underflow(Heap * heap) { if (!(heap->heap <= heap->next)) {- fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n", + fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n", heap->heap, heap->next); exit(EXIT_FAILURE); }@@ -55,7 +55,7 @@ void heap_check_overflow(Heap * heap) { if (!(heap->next <= heap->end)) {- fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n", + fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n", heap->next, heap->end); exit(EXIT_FAILURE); }@@ -65,13 +65,13 @@ return (v != NULL) && !(ISINT(v)); } -int ref_in_heap(Heap * heap, VAL v) { +int ref_in_heap(Heap * heap, VAL v) { return ((VAL)heap->heap <= v) && (v < (VAL)heap->next); } // Checks three important properties: // 1. Closure.-// Check if all pointers in the _heap_ points only to heap. +// Check if all pointers in the _heap_ points only to heap. // 2. Unidirectionality. (if compact gc) // All references in the heap should be are unidirectional. In other words, // more recently allocated closure can point only to earlier allocated one.@@ -79,7 +79,7 @@ // void heap_check_pointers(Heap * heap) { char* scan = NULL;- + size_t item_size = 0; for(scan = heap->heap; scan < heap->next; scan += item_size) { item_size = *((size_t*)scan);@@ -96,7 +96,7 @@ if (is_valid_ref(ptr)) { // Check for closure. if (!ref_in_heap(heap, ptr)) {- fprintf(stderr, + fprintf(stderr, "RTS ERROR: heap closure broken. "\ "<HEAP %p %p %p> <REF %p>\n", heap->heap, heap->next, heap->end, ptr);@@ -105,7 +105,7 @@ #if 0 // TODO macro // Check for unidirectionality. if (!(ptr < heap_item)) {- fprintf(stderr, + fprintf(stderr, "RTS ERROR: heap unidirectionality broken:" \ "<CON %p> <FIELD %p>\n", heap_item, ptr);
rts/idris_heap.h view
@@ -8,7 +8,7 @@ char* heap; // Point to bottom of heap char* end; // Point to top of heap size_t size; // Size of _next_ heap. Size of current heap is /end - heap/.- size_t growth; // Quantity of heap growth in bytes. + size_t growth; // Quantity of heap growth in bytes. char* old; } Heap;@@ -23,7 +23,7 @@ // Should be used _between_ gc's. #define HEAP_CHECK(vm) heap_check_all(&(vm->heap)); #else-#define HEAP_CHECK(vm) +#define HEAP_CHECK(vm) #endif // IDRIS_DEBUG #endif // _IDRIS_HEAP_H
rts/idris_net.c view
@@ -38,15 +38,15 @@ } // 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, +// 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;@@ -57,7 +57,7 @@ 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); }@@ -75,7 +75,7 @@ //freeaddrinfo(address_res); //printf("Lib err: bind\n"); return -1;- } + } return 0; } @@ -111,7 +111,7 @@ int idrnet_sockaddr_ipv4_port(void* sockaddr) { struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;- return ((int) ntohs(addr->sin_port)); + return ((int) ntohs(addr->sin_port)); } void* idrnet_create_sockaddr() {@@ -141,13 +141,13 @@ } void* idrnet_recv(int sockfd, int len) {- idrnet_recv_result* res_struct = + 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 }@@ -172,7 +172,7 @@ } void idrnet_free_recv_struct(void* res_struct) {- idrnet_recv_result* i_res_struct = + idrnet_recv_result* i_res_struct = (idrnet_recv_result*) res_struct; if (i_res_struct->payload != NULL) { free(i_res_struct->payload);@@ -191,9 +191,9 @@ int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM); if (addr_res == -1) { return -1;- } + } - int send_res = sendto(sockfd, data, strlen(data), 0, + int send_res = sendto(sockfd, data, strlen(data), 0, remote_host->ai_addr, remote_host->ai_addrlen); freeaddrinfo(remote_host); return send_res;@@ -206,11 +206,11 @@ if (addr_res == -1) { //printf("lib err: sendto getaddrinfo \n"); return -1;- } + } buf_htonl(buf, buf_len); - int send_res = sendto(sockfd, buf, buf_len, 0, + 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");@@ -224,13 +224,13 @@ void* idrnet_recvfrom(int sockfd, int len) { /* * int recvfrom(int sockfd, void *buf, int len, unsigned int flags,- struct sockaddr *from, int *fromlen); + struct sockaddr *from, int *fromlen); */ // Allocate the required structures, and nuke them- struct sockaddr_storage* remote_addr = + 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* ret = (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result)); memset(remote_addr, 0, sizeof(struct sockaddr_storage)); memset(buf, 0, len + 1);@@ -240,7 +240,7 @@ int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen); ret->result = recv_res; // Check for failure...- if (recv_res == -1) { + if (recv_res == -1) { free(buf); free(remote_addr); } else {@@ -255,12 +255,11 @@ 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* remote_addr = (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));- idrnet_recvfrom_result* ret = + 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));@@ -269,7 +268,7 @@ 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) { + if (recv_res == -1) { free(remote_addr); } // Payload will be NULL -- since it's been put into the user-specified buffer. We@@ -298,7 +297,7 @@ 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* remote_addr_in = (struct sockaddr_in*) recv_struct->remote_addr; return ((int) ntohs(remote_addr_in->sin_port)); }@@ -316,5 +315,3 @@ } } }--
rts/idris_stdfgn.c view
@@ -2,12 +2,18 @@ #include "idris_rts.h" #include "idris_gmp.h" #include "idris_gc.h"-#include <sys/select.h>+ #include <fcntl.h> #include <errno.h> #include <stdio.h> #include <time.h> +#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+int win_fpoll(void* h);+#else+#include <sys/select.h>+#endif+ extern char** environ; void putStr(char* str) {@@ -25,13 +31,13 @@ } int fileEOF(void* h) {- FILE* f = (FILE*)h;- return feof(f);+ FILE* f = (FILE*)h;+ return feof(f); } int fileError(void* h) {- FILE* f = (FILE*)h;- return ferror(f);+ FILE* f = (FILE*)h;+ return ferror(f); } int idris_writeStr(void* h, char* str) {@@ -45,6 +51,9 @@ int fpoll(void* h) {+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)+ return win_fpoll(h);+#else FILE* f = (FILE*)h; fd_set x; struct timeval timeout;@@ -57,6 +66,7 @@ int r = select(fd+1, &x, 0, 0, &timeout); return r;+#endif } void* do_popen(const char* cmd, const char* mode) {@@ -107,5 +117,5 @@ } void idris_forceGC(void* vm) {- idris_gc((VM*)vm); + idris_gc((VM*)vm); }
rts/windows/idris_net.c view
@@ -12,7 +12,7 @@ #include <Ws2tcpip.h> -// inet_ntop isn't defined in the old mingw delivered with GHC, +// inet_ntop isn't defined in the old mingw delivered with GHC, // so put the prototype here, cribbed from a newer version of it WINSOCK_API_LINKAGE LPCSTR WSAAPI InetNtopA(INT Family, PVOID pAddr, LPSTR pStringBuf, size_t StringBufSize);@@ -50,7 +50,7 @@ // Convert port into string char str_port[8]; sprintf(str_port, "%d", port);- + if (!check_init()) { return -1; }@@ -73,7 +73,7 @@ int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen); if (bind_res == -1) { return -1;- } + } return 0; }@@ -152,13 +152,13 @@ if (!check_init()) { return NULL; }- idrnet_recv_result* res_struct = + 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 }@@ -182,7 +182,7 @@ } void idrnet_free_recv_struct(void* res_struct) {- idrnet_recv_result* i_res_struct = + idrnet_recv_result* i_res_struct = (idrnet_recv_result*) res_struct; if (i_res_struct->payload != NULL) { free(i_res_struct->payload);@@ -193,4 +193,3 @@ int idrnet_errno() { return errno; }-
− rts/windows/idris_stdfgn.c
@@ -1,82 +0,0 @@-#include "../idris_stdfgn.h"-#include "../idris_rts.h"-#include "../idris_gc.h"--#include <fcntl.h>-#include <stdio.h>-#include <time.h>-#include <io.h>--extern char** environ;--int win_fpoll(void* h);--void putStr(char* str) {- printf("%s", str);-}--void* fileOpen(char* name, char* mode) {- FILE* f = fopen(name, mode);- return (void*)f;-}--void fileClose(void* h) {- FILE* f = (FILE*)h;- fclose(f);-}--int fileEOF(void* h) {- FILE* f = (FILE*)h;- return feof(f);-}--int fileError(void* h) {- FILE* f = (FILE*)h;- return ferror(f);-}--int idris_writeStr(void* h, char* str) {- FILE* f = (FILE*)h;- if (fputs(str, f)) {- return 0;- } else {- return -1;- }-}--int fpoll(void* h)-{- return win_fpoll(h);-}--void* do_popen(const char* cmd, const char* mode) {- FILE* f = _popen(cmd, mode);-// int d = fileno(f);-// fcntl(d, F_SETFL, O_NONBLOCK);- return f;-}--int isNull(void* ptr) {- return ptr==NULL;-}--int idris_eqPtr(void* x, void* y) {- return x==y;-}--void* idris_stdin() {- return (void*)stdin;-}--char* getEnvPair(int i) {- return *(environ + i);-}--VAL idris_time() {- time_t t = time(NULL);- return MKBIGI(t);-}--void idris_forceGC(void* vm) {- idris_gc((VM*)vm);-}
src/Idris/CaseSplit.hs view
@@ -362,7 +362,7 @@ -> Idris String getClause l fn un fp = do i <- getIState- case lookupCtxt fn (idris_classes i) of+ case lookupCtxt un (idris_classes i) of [c] -> return (mkClassBodies i (class_methods c)) _ -> do ty_in <- getInternalApp fp l let ty = case ty_in of
src/Idris/Core/Elaborate.hs view
@@ -353,6 +353,9 @@ unifyGoal :: Raw -> Elab' aux () unifyGoal t = processTactic' (UnifyGoal t) +unifyTerms :: Raw -> Raw -> Elab' aux ()+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)+ exact :: Raw -> Elab' aux () exact t = processTactic' (Exact t) @@ -724,7 +727,12 @@ focus f simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()-simple_app infer fun arg str = +simple_app infer fun arg str =+ try (dep_app fun arg str)+ (infer_app infer fun arg str)++infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()+infer_app infer fun arg str = do a <- getNameFrom (sMN 0 "__argTy") b <- getNameFrom (sMN 0 "__retTy") f <- getNameFrom (sMN 0 "f")@@ -755,8 +763,49 @@ when (a `elem` hs) $ do movelast a when (b `elem` hs) $ do movelast b end_unify- where- regretWith err = try regret (lift $ tfail err)++dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()+dep_app fun arg str = + do a <- getNameFrom (sMN 0 "__argTy")+ b <- getNameFrom (sMN 0 "__retTy")+ fty <- getNameFrom (sMN 0 "__fnTy")+ f <- getNameFrom (sMN 0 "f")+ s <- getNameFrom (sMN 0 "s")+ claim a RType+ claim fty RType+ claim f (Var fty)+ tm <- get_term+ g <- goal+ start_unify s+ claim s (Var a)+ + prep_fill f [s]+ focus f; attack; fun+ end_unify+ fty <- goal+ solve+ focus s; attack; + ctxt <- get_context+ env <- get_env+ case normalise ctxt env fty of+ -- if f gives a function type, unify our argument type with+ -- f's expected argument type+ Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)+ -- Can't infer a type for 'f', so fail here (and drop back to+ -- simply typed application where we infer the type for f)+ _ -> fail "Can't make type"+ end_unify+ arg+ solve+ complete_fill++ -- We don't need a and b in the hole queue any more since they were+ -- just for checking f, so move them to the end. If they never end up+ -- getting solved, we'll get an 'Incomplete term' error.+ hs <- get_holes+ when (a `elem` hs) $ do movelast a+ when (b `elem` hs) $ do movelast b+ end_unify -- Abstract over an argument of unknown type, giving a name for the hole -- which we'll fill with the argument type too.
src/Idris/Core/ProofState.hs view
@@ -91,6 +91,7 @@ | MatchProblems Bool | UnifyProblems | UnifyGoal Raw+ | UnifyTerms Raw Raw | ProofState | Undo | QED@@ -477,6 +478,13 @@ return h unifyGoal _ _ _ _ = fail "The focus is not a binder." +unifyTerms :: Raw -> Raw -> RunTactic+unifyTerms tm1 tm2 ctxt env h =+ do (tm1v, _) <- lift $ check ctxt env tm1+ (tm2v, _) <- lift $ check ctxt env tm2+ ns' <- unify' ctxt env (tm1v, Nothing) (tm2v, Nothing)+ return h+ exact :: Raw -> RunTactic exact guess ctxt env (Bind x (Hole ty) sc) = do (val, valty) <- lift $ check ctxt env guess@@ -1113,3 +1121,5 @@ mktac (SetInjective n) = setinj n mktac (MoveLast n) = movelast n mktac (UnifyGoal r) = unifyGoal r+ mktac (UnifyTerms x y) = unifyTerms x y+
src/Idris/DSL.hs view
@@ -108,7 +108,10 @@ block b (DoExp fc tm : rest) = PApp fc b [pexp tm,- pexp (PLam fc (sMN 0 "bindx") NoFC Placeholder (block b rest))]+ pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]+ where mkTy (PCase _ _ _) = PRef fc [] unitTy+ mkTy (PMetavar _ _) = PRef fc [] unitTy+ mkTy _ = Placeholder block b _ = PElabError (Msg "Invalid statement in do block") expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
src/Idris/Elab/Clause.hs view
@@ -669,8 +669,6 @@ (erun fc (build i winfo ERHS opts fname rhs)) errAt "right hand side of " fname (Just clhsty) (erun fc $ psolve lhs_tm)- hs <- get_holes- mapM_ (elabCaseHole is) hs tt <- get_term aux <- getAux let (tm, ds) = runState (collectDeferred (Just fname) @@ -787,27 +785,6 @@ sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in (b : bf, af) sepBlocks' ns [] = ([], [])--- -- if a hole is just an argument/result of a case block, treat it as- -- the unit type. Hack to help elaborate case in do blocks.- elabCaseHole aux h = do- focus h- g <- goal- case g of- TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve- _ -> return ()-- -- Is the name a pattern argument in the declaration- isArg :: Name -> PDecl -> Bool- isArg n (PClauses _ _ _ cs) = any isArg' cs- where- isArg' (PClause _ _ (PApp _ _ args) _ _ _)- = any (\x -> case x of- PRef _ _ n' -> n == n'- _ -> False) (map getTm args)- isArg' _ = False- isArg _ _ = False -- term is not within "with" block isOutsideWith :: PTerm -> Bool
src/Idris/Elab/Term.hs view
@@ -1028,12 +1028,22 @@ solve elab' ina _ c@(PCase fc scr opts) = do attack+ tyn <- getNameFrom (sMN 0 "scty") claim tyn RType valn <- getNameFrom (sMN 0 "scval") scvn <- getNameFrom (sMN 0 "scvar") claim valn (Var tyn) letbind scvn (Var tyn) (Var valn)+ + -- Start filling in the scrutinee type, if we can work one+ -- out from the case options+ let scrTy = getScrType (map fst opts)+ case scrTy of+ Nothing -> return ()+ Just ty -> do focus tyn+ elabE ina (Just fc) ty+ focus valn elabE (ina { e_inarg = True }) (Just fc) scr -- Solve any remaining implicits - we need to solve as many@@ -1084,6 +1094,21 @@ Just xs@(_:_) -> sNS n xs _ -> n + getScrType [] = Nothing+ getScrType (f : os) = maybe (getScrType os) Just (getAppType f)++ getAppType (PRef _ _ n) = + case lookupTyName n (tt_ctxt ist) of+ [(n', ty)] | isDConName n' (tt_ctxt ist) -> + case unApply (getRetTy ty) of+ (P _ tyn _, args) ->+ Just (PApp fc (PRef fc [] tyn)+ (map pexp (map (const Placeholder) args)))+ _ -> Nothing+ _ -> Nothing -- ambiguity is no help to us!+ getAppType (PApp _ t as) = getAppType t+ getAppType _ = Nothing+ inApp (P _ n _) = [n] inApp (App _ f a) = inApp f ++ inApp a inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc@@ -1696,38 +1721,25 @@ collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term-collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =- do ds <- get- t' <- collectDeferred top casenames ctxt t- when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])- collectDeferred top casenames ctxt app- where- -- Evaluate the top level functions in arguments, if possible, and if it's- -- not a name we're immediately going to define in a case block, so that- -- any immediate specialisation of the function applied to constructors - -- can be done- tidyArg env (Bind n b@(Pi im t k) sc) - = Bind n (Pi im (tidy ctxt env t) k)- (tidyArg ((n, b) : env) sc)- tidyArg env t = tidy ctxt env t-- tidy ctxt env t = normalise ctxt env t-- getFn (Bind n (Lam _) t) = getFn t- getFn t | (f, a) <- unApply t = f--collectDeferred top ns ctxt (Bind n b t) - = do b' <- cdb b- t' <- collectDeferred top ns ctxt t- return (Bind n b' t')+collectDeferred top casenames ctxt tm = cd [] tm where- cdb (Let t v) = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)- cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)- cdb b = do ty' <- collectDeferred top ns ctxt (binderTy b)- return (b { binderTy = ty' })-collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f) - (collectDeferred top ns ctxt a)-collectDeferred top ns ctxt t = return t+ cd env (Bind n (GHole i psns t) app) =+ do ds <- get+ t' <- collectDeferred top casenames ctxt t+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])+ cd env app+ cd env (Bind n b t) + = do b' <- cdb b+ t' <- cd ((n, b) : env) t+ return (Bind n b' t')+ where+ cdb (Let t v) = liftM2 Let (cd env t) (cd env v)+ cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)+ cdb b = do ty' <- cd env (binderTy b)+ return (b { binderTy = ty' })+ cd env (App s f a) = liftM2 (App s) (cd env f) + (cd env a)+ cd env t = return t case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD () case_ ind autoSolve ist fn tm = do
src/Idris/REPL.hs view
@@ -943,7 +943,8 @@ where showMetavarInfo ppo ist n i = case lookupTy n (tt_ctxt ist) of- (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))+ (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in+ putTy ppo ist i [] (delab ist (errReverse ist ty')) putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc putTy ppo ist i bnd (PPi _ n _ t sc)
test/basic002/test006.idr view
@@ -23,7 +23,7 @@ ---------- Proofs ---------- Main.parity_lemma_2 = proof {- intro;+ intro j; intro; rewrite sym (plusSuccRightSucc j j); trivial;
+ test/interactive011/expected view
@@ -0,0 +1,3 @@+ show x = ?Show_rhs_1+ showPrec d x = ?Show_rhs_2+append [] _ = ?append_rhs_1
+ test/interactive011/input view
@@ -0,0 +1,2 @@+:ac 5 Show+:ac 7 append
+ test/interactive011/interactive011.idr view
@@ -0,0 +1,11 @@+import Data.Vect++data Foo = Bar | Baz++instance Show Foo where++append : Vect n a -> Vect m a -> Vect (n + m) a+append (x :: xs) ys = ?append_rhs_2+++
+ test/interactive011/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --quiet interactive011.idr < input+rm -f *.ibc
+ test/interactive012/expected view
@@ -0,0 +1,33 @@+ x : Int+--------------------------------------+mkString_rhs_1 : String+ x : String+--------------------------------------+mkString_rhs_2 : String+--------------------------------------+mkThing_rhs_1 : Int+--------------------------------------+mkThing_rhs_2 : String+ str : Bool+ x : IntString str+--------------------------------------+mkString2_rhs : String+ x : ?what+--------------------------------------+mkString3_rhs_1 : String+ x : ?what+--------------------------------------+mkString3_rhs_2 : String+ a : Type+ m : Nat+ ys : Vect m a+--------------------------------------+append_rhs_1 : Vect m a+ a : Type+ x : a+ k : Nat+ xs : Vect k a+ m : Nat+ ys : Vect m a+--------------------------------------+append_rhs_2 : Vect (S (plus k m)) a
+ test/interactive012/input view
@@ -0,0 +1,9 @@+:t mkString_rhs_1+:t mkString_rhs_2+:t mkThing_rhs_1+:t mkThing_rhs_2+:t mkString2_rhs+:t mkString3_rhs_1+:t mkString3_rhs_2+:t append_rhs_1+:t append_rhs_2
+ test/interactive012/interactive012.idr view
@@ -0,0 +1,26 @@+IntString : Bool -> Type+IntString False = Int+IntString True = String++mkString : (str : Bool) -> IntString str -> String+mkString False x = ?mkString_rhs_1+mkString True x = ?mkString_rhs_2++mkThing : (str : Bool) -> IntString str+mkThing False = ?mkThing_rhs_1+mkThing True = ?mkThing_rhs_2++mkString2 : (str : Bool) -> IntString str -> String+mkString2 str x = ?mkString2_rhs++mkString3 : (str : Bool) -> ?what -> String+mkString3 False x = ?mkString3_rhs_1+mkString3 True x = ?mkString3_rhs_2++data Vect : Nat -> Type -> Type where+ Nil : Vect Z a+ (::) : a -> Vect k a -> Vect (S k) a++append : Vect n a -> Vect m a -> Vect (n + m) a+append [] ys = ?append_rhs_1+append (x :: xs) ys = ?append_rhs_2
+ test/interactive012/run view
@@ -0,0 +1,3 @@+#!/usr/bin/env bash+idris --quiet interactive012.idr < input+rm -f *.ibc
test/reg001/reg001.idr view
@@ -182,3 +182,29 @@ vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)] vecfoo = put (S (S Z)) hVectEx1++foom : Monad m => Int -> m Int+foom = pure + +bar : IO ()+bar = case foom 5 of+ Nothing => print 42+ Just n => print n++Max : (Nat -> Type) -> Type+Max p = (Nat , (k : Nat) -> p k -> Nat)+ +maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat+maxEquiv a n1 pr1 = snd a n1 pr1++data Rho = R++rho : Rho -> Rho+rho r = case r of R => r++data Kappa : (r : Rho) -> Type where K : Kappa r++kappa : Kappa (rho r) -> Kappa (rho r)+kappa {r} k = k' where -- k' : Kappa (rho r)+ k' = k+
test/tutorial006/run view
@@ -1,4 +1,5 @@ #!/usr/bin/env bash idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check+idris --nocolour --consolewidth 80 $@ tutorial006c.idr -p effects --check rm -f *.ibc
+ test/tutorial006/tutorial006c.idr view
@@ -0,0 +1,20 @@+import Effects+import Effect.Exception+import Effect.StdIO+import Data.Vect++read_vec : Eff (p ** Vect p Int) [STDIO]+read_vec = do putStr "Number (-1 when done): "+ case run (parseNumber (trim !getStr)) of+ Nothing => do putStrLn "Input error"+ read_vec+ Just v => if (v /= -1)+ then do (_ ** xs) <- read_vec+ pure (_ ** v :: xs)+ else pure (_ ** [])+ where+ parseNumber : String -> Eff Int [EXCEPTION String]+ parseNumber str+ = if all (\x => isDigit x || x == '-') (unpack str)+ then pure (cast str)+ else raise "Not a number"