diff --git a/config.mk b/config.mk new file mode 100644 --- /dev/null +++ b/config.mk @@ -0,0 +1,3 @@ +GMP_INCLUDE_DIR := +CC :=gcc +CABAL :=cabal diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.9.5 +Version: 0.9.5.1 License: BSD3 License-file: LICENSE Author: Edwin Brady @@ -47,9 +47,12 @@ Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h rts/libtest.c -Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr lib/Network/*.idr +Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr + lib/Network/*.idr lib/Control/*.idr lib/Control/Monad/*.idr lib/Language/*.idr + lib/System/Concurrency/*.idr tutorial/examples/*.idr lib/base.ipkg + config.mk rts/*.c rts/*.h rts/Makefile source-repository head diff --git a/lib/Builtins.idr b/lib/Builtins.idr --- a/lib/Builtins.idr +++ b/lib/Builtins.idr @@ -22,6 +22,9 @@ lazy : a -> a lazy x = x -- compiled specially +par : |(thunk:a) -> a +par x = x -- compiled specially + malloc : Int -> a -> a malloc size x = x -- compiled specially diff --git a/lib/Control/Arrow.idr b/lib/Control/Arrow.idr new file mode 100644 --- /dev/null +++ b/lib/Control/Arrow.idr @@ -0,0 +1,21 @@ +module Category.Arrow + +import Prelude.Morphisms +import Control.Category + +infixr 3 *** +infixr 3 &&& + +class Category arr => Arrow (arr : Set -> Set -> Set) where + arrow : (a -> b) -> arr a b + first : arr a b -> arr (a, c) (b, c) + second : arr a b -> arr (c, a) (c, b) + (***) : arr a b -> arr a' b' -> arr (a, a') (b, b') + (&&&) : arr a b -> arr a b' -> arr a (b, b') + +instance Arrow Morphism where + arrow f = Homo f + first (Homo f) = Homo $ \(a, b) => (f a, b) + second (Homo f) = Homo $ \(a, b) => (a, f b) + (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b) + (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a) diff --git a/lib/Control/Category.idr b/lib/Control/Category.idr new file mode 100644 --- /dev/null +++ b/lib/Control/Category.idr @@ -0,0 +1,15 @@ +module Control.Category + +import Prelude.Morphisms + +class Category (cat : Set -> Set -> Set) where + id : cat a a + (.) : cat b c -> cat a b -> cat a c + +instance Category Morphism where + id = Homo Builtins.id + (Homo f) . (Homo g) = Homo $ Builtins.(.) f g + +infixr 1 >>> +(>>>) : Category cat => cat a b -> cat b c -> cat a c +f >>> g = g . f diff --git a/lib/Prelude/Monad.idr b/lib/Prelude/Monad.idr --- a/lib/Prelude/Monad.idr +++ b/lib/Prelude/Monad.idr @@ -1,4 +1,4 @@ -module prelude.monad +module Prelude.Monad -- Monads and Functors diff --git a/lib/System/Concurrency/Raw.idr b/lib/System/Concurrency/Raw.idr new file mode 100644 --- /dev/null +++ b/lib/System/Concurrency/Raw.idr @@ -0,0 +1,25 @@ +module System.Concurrency.Raw + +-- Raw (i.e. not type safe) message passing + +import System + +-- Send a message of any type to the thread with the given thread id + +sendToThread : (thread_id : Ptr) -> a -> IO () +sendToThread {a} dest val + = mkForeign (FFun "idris_sendMessage" + [FPtr, FPtr, FAny a] FUnit) prim__vm dest val + +checkMsgs : IO Bool +checkMsgs = do msgs <- mkForeign (FFun "idris_checkMessage" + [FPtr] FInt) prim__vm + return (intToBool msgs) + +-- Check inbox for messages. If there are none, blocks until a message +-- arrives. + +getMsg : IO a +getMsg {a} = mkForeign (FFun "idris_recvMessage" + [FPtr] (FAny a)) prim__vm + diff --git a/lib/base.ipkg b/lib/base.ipkg --- a/lib/base.ipkg +++ b/lib/base.ipkg @@ -5,10 +5,12 @@ Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin, Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative, - Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Heap, - Prelude.Complex, Prelude.Morphisms, + Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars, + Prelude.Heap, Prelude.Complex, Prelude.Morphisms, Network.Cgi, + + System.Concurrency.Raw, Language.Reflection, diff --git a/rts/Makefile b/rts/Makefile --- a/rts/Makefile +++ b/rts/Makefile @@ -1,6 +1,11 @@ +include ../config.mk + OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h CFLAGS = -O2 -Wall -Werror +ifneq ($(GMP_INCLUDE_DIR),) + CFLAGS += -isystem $(GMP_INCLUDE_DIR) +endif LIBTARGET = libidris_rts.a diff --git a/rts/idris_gc.c b/rts/idris_gc.c --- a/rts/idris_gc.c +++ b/rts/idris_gc.c @@ -9,7 +9,7 @@ if (x==NULL || ISINT(x)) { return x; } - switch(x->ty) { + switch(GETTY(x)) { case CON: cl = allocCon(vm, x->info.c.arity); cl->info.c.tag = x->info.c.tag; @@ -39,7 +39,7 @@ default: break; } - x->ty = FWD; + SETTY(x, FWD); x->info.ptr = cl; return cl; } @@ -53,7 +53,7 @@ size_t inc = *((size_t*)scan); VAL heap_item = (VAL)(scan+sizeof(size_t)); // If it's a CON, copy its arguments - switch(heap_item->ty) { + switch(GETTY(heap_item)) { case CON: argptr = (VAL*)(heap_item->info.c.args); for(i = 0; i < heap_item->info.c.arity; ++i) { diff --git a/rts/idris_gmp.c b/rts/idris_gmp.c --- a/rts/idris_gmp.c +++ b/rts/idris_gmp.c @@ -15,7 +15,7 @@ mpz_init(*bigint); mpz_set_str(*bigint, val, 10); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; @@ -29,7 +29,7 @@ mpz_init(*bigint); mpz_set(*bigint, *((mpz_t*)big)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; @@ -44,7 +44,7 @@ mpz_init(*bigint); mpz_set_si(*bigint, GETINT(x)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; @@ -58,7 +58,7 @@ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*)); bigint = allocate(vm, sizeof(mpz_t)); mpz_add(*bigint, GETMPZ(x), GETMPZ(y)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; } @@ -68,7 +68,7 @@ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*)); bigint = allocate(vm, sizeof(mpz_t)); mpz_sub(*bigint, GETMPZ(x), GETMPZ(y)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; } @@ -78,7 +78,7 @@ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*)); bigint = allocate(vm, sizeof(mpz_t)); mpz_mul(*bigint, GETMPZ(x), GETMPZ(y)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; } @@ -88,7 +88,7 @@ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*)); bigint = allocate(vm, sizeof(mpz_t)); mpz_div(*bigint, GETMPZ(x), GETMPZ(y)); - cl -> ty = BIGINT; + SETTY(cl, BIGINT); cl -> info.ptr = (void*)bigint; return cl; } diff --git a/rts/idris_main.c b/rts/idris_main.c --- a/rts/idris_main.c +++ b/rts/idris_main.c @@ -1,5 +1,5 @@ int main(int argc, char* argv[]) { - VM* vm = init_vm(4096000, 2048000, argc, argv); // 1024000); + VM* vm = init_vm(4096000, 2048000, 1, argc, argv); // 1024000); _idris__123_runMain0_125_(vm, NULL); //_idris_main(vm, NULL); #ifdef IDRIS_TRACE diff --git a/rts/idris_rts.c b/rts/idris_rts.c --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -9,7 +9,9 @@ #include "idris_rts.h" #include "idris_gc.h" -VM* init_vm(int stack_size, size_t heap_size, int argc, char* argv[]) { +VM* init_vm(int stack_size, size_t heap_size, + int max_threads, // not implemented yet + int argc, char* argv[]) { VAL* valstack = malloc(stack_size*sizeof(VAL)); int* intstack = malloc(stack_size*sizeof(int)); double* floatstack = malloc(stack_size*sizeof(double)); @@ -43,8 +45,9 @@ pthread_mutex_init(&(vm->inbox_block), NULL); pthread_cond_init(&(vm->inbox_waiting), NULL); + vm->max_threads = max_threads; + int i; - // Assumption: there's enough space for this in the initial heap. vm->argv = malloc(argc*sizeof(VAL)); vm->argc = argc; @@ -90,7 +93,7 @@ void* allocCon(VM* vm, int arity) { Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity); - cl -> ty = CON; + SETTY(cl, CON); if (arity == 0) { cl -> info.c.args = NULL; } else { @@ -104,7 +107,7 @@ VAL MKFLOAT(VM* vm, double val) { Closure* cl = allocate(vm, sizeof(Closure)); - cl -> ty = FLOAT; + SETTY(cl, FLOAT); cl -> info.f = val; return cl; } @@ -112,7 +115,7 @@ VAL MKSTR(VM* vm, char* str) { Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) + sizeof(char)*strlen(str)+1); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); strcpy(cl -> info.str, str); @@ -121,7 +124,7 @@ VAL MKPTR(VM* vm, void* ptr) { Closure* cl = allocate(vm, sizeof(Closure)); - cl -> ty = PTR; + SETTY(cl, PTR); cl -> info.ptr = ptr; return cl; } @@ -185,7 +188,7 @@ printf("%d ", (int)(GETINT(v))); return; } - switch(v->ty) { + switch(GETTY(v)) { case CON: printf("%d[", v->info.c.tag); for(i = 0; i < v->info.c.arity; ++i) { @@ -209,7 +212,7 @@ VAL idris_castIntStr(VM* vm, VAL i) { Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); sprintf(cl -> info.str, "%d", (int)(GETINT(i))); return cl; @@ -226,7 +229,7 @@ VAL idris_castFloatStr(VM* vm, VAL i) { Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); sprintf(cl -> info.str, "%g", GETFLOAT(i)); return cl; @@ -242,7 +245,7 @@ // dumpVal(l); // printf("\n"); Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); strcpy(cl -> info.str, ls); strcat(cl -> info.str, rs); @@ -317,7 +320,7 @@ char *xstr = GETSTR(xs); Closure* cl = allocate(vm, sizeof(Closure) + strlen(xstr) + 2); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); cl -> info.str[0] = (char)(GETINT(x)); strcpy(cl -> info.str+1, xstr); @@ -332,7 +335,7 @@ char *xstr = GETSTR(str); Closure* cl = allocate(vm, sizeof(Closure) + strlen(xstr) + 1); - cl -> ty = STRING; + SETTY(cl, STRING); cl -> info.str = (char*)cl + sizeof(Closure); int y = 0; int x = strlen(xstr); @@ -364,7 +367,9 @@ } void* vmThread(VM* callvm, func f, VAL arg) { - VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size, 0, NULL); + VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size, + callvm->max_threads, + 0, NULL); pthread_t t; pthread_attr_t attr; // size_t stacksize; @@ -379,7 +384,7 @@ td->arg = copyTo(vm, arg); pthread_create(&t, &attr, runThread, td); - usleep(100); +// usleep(100); return vm; } @@ -393,7 +398,7 @@ if (x==NULL || ISINT(x)) { return x; } - switch(x->ty) { + switch(GETTY(x)) { case CON: cl = allocCon(vm, x->info.c.arity); cl->info.c.tag = x->info.c.tag; @@ -424,12 +429,14 @@ } // Add a message to another VM's message queue -void sendMessage(VM* sender, VM* dest, VAL msg) { +void idris_sendMessage(VM* sender, VM* dest, VAL msg) { // FIXME: If GC kicks in in the middle of the copy, we're in trouble. // Probably best check there is enough room in advance. (How?) VAL dmsg = copyTo(dest, msg); + +// printf("Sending [lock]...\n"); pthread_mutex_lock(&(dest->inbox_lock)); *(dest->inbox_write) = dmsg; @@ -445,21 +452,42 @@ } // Wake up the other thread - pthread_cond_signal(&(dest->inbox_waiting)); + pthread_mutex_lock(&dest->inbox_block); + pthread_cond_signal(&dest->inbox_waiting); + pthread_mutex_unlock(&dest->inbox_block); +// printf("Sending [signalled]...\n"); + pthread_mutex_unlock(&(dest->inbox_lock)); +// printf("Sending [unlock]...\n"); } +int idris_checkMessages(VM* vm) { + VAL msg = *(vm->inbox_ptr); + return (msg != NULL); +} + // block until there is a message in the queue -VAL recvMessage(VM* vm) { - VAL msg = NULL; +VAL idris_recvMessage(VM* vm) { + VAL msg; + struct timespec timeout; + int status; + pthread_mutex_lock(&vm->inbox_block); + msg = *(vm->inbox_ptr); while (msg == NULL) { - pthread_mutex_lock(&vm->inbox_block); - pthread_cond_wait(&vm->inbox_waiting, &vm->inbox_block); - pthread_mutex_unlock(&vm->inbox_block); +// printf("No message yet\n"); +// printf("Waiting [lock]...\n"); + timeout.tv_sec = time (NULL) + 3; + timeout.tv_nsec = 0; + status = pthread_cond_timedwait(&vm->inbox_waiting, &vm->inbox_block, + &timeout); + (void)(status); //don't emit 'unused' warning +// printf("Waiting [unlock]... %d\n", status); msg = *(vm->inbox_ptr); } + pthread_mutex_unlock(&vm->inbox_block); + if (msg != NULL) { pthread_mutex_lock(&(vm->inbox_lock)); *(vm->inbox_ptr) = NULL; diff --git a/rts/idris_rts.h b/rts/idris_rts.h --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -21,6 +21,8 @@ } con; typedef struct { +// Use top 16 bits of ty for saying which heap value is in +// Bottom 16 bits for closure type ClosureType ty; union { con c; @@ -57,6 +59,8 @@ VAL* inbox_ptr; // Next message to read VAL* inbox_write; // Location of next message to write + int max_threads; // maximum number of threads to run in parallel + int argc; VAL* argv; // command line arguments @@ -69,7 +73,9 @@ } VM; // Create a new VM -VM* init_vm(int stack_size, size_t heap_size, int argc, char* argv[]); +VM* init_vm(int stack_size, size_t heap_size, + int max_threads, + int argc, char* argv[]); // Clean up a VM once it's no longer needed void terminate(VM* vm); @@ -92,6 +98,15 @@ #define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag : (-1)) ) +// Use top 16 bits for saying which heap value is in +// Bottom 16 bits for closure type + +#define GETTY(x) ((x)->ty & 0x0000ffff) +#define SETTY(x,t) (x)->ty = (((x)->ty & 0xffff0000) | (t)) + +#define GETHEAP(x) ((x)->ty >> 16) +#define SETHEAP(x,y) (x)->ty = (((x)->ty & 0x0000ffff) | ((t) << 16)) + // Integers, floats and operators typedef intptr_t i_int; @@ -143,9 +158,11 @@ VAL copyTo(VM* newVM, VAL x); // Add a message to another VM's message queue -void sendMessage(VM* sender, VM* dest, VAL msg); +void idris_sendMessage(VM* sender, VM* dest, VAL msg); +// Check whether there are any messages in the queue +int idris_checkMessages(VM* vm); // block until there is a message in the queue -VAL recvMessage(VM* vm); +VAL idris_recvMessage(VM* vm); void dumpVal(VAL r); void dumpStack(VM* vm); diff --git a/rts/libidris_rts.a b/rts/libidris_rts.a Binary files a/rts/libidris_rts.a and b/rts/libidris_rts.a differ diff --git a/src/Core/CoreParser.hs b/src/Core/CoreParser.hs --- a/src/Core/CoreParser.hs +++ b/src/Core/CoreParser.hs @@ -19,15 +19,17 @@ opStart = iOpStart, opLetter = iOpLetter, identLetter = identLetter haskellDef <|> lchar '.', - reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"], - reservedNames = ["let", "in", "data", "codata", "record", "Set", - "do", "dsl", "import", "impossible", - "case", "of", "total", "partial", - "infix", "infixl", "infixr", - "where", "with", "syntax", "proof", "postulate", - "using", "namespace", "class", "instance", - "public", "private", "abstract", - "Int", "Integer", "Float", "Char", "String", "Ptr"] + reservedOpNames + = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"], + reservedNames + = ["let", "in", "data", "codata", "record", "Set", + "do", "dsl", "import", "impossible", + "case", "of", "total", "partial", "mutual", + "infix", "infixl", "infixr", + "where", "with", "syntax", "proof", "postulate", + "using", "namespace", "class", "instance", + "public", "private", "abstract", + "Int", "Integer", "Float", "Char", "String", "Ptr"] } iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~" diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -109,7 +109,8 @@ simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t - = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0)] + = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0), + (UN "par", 0)] (map finalEntry env) (finalise t) [Simplify] quote 0 val) initEval diff --git a/src/Core/TT.hs b/src/Core/TT.hs --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -199,6 +199,10 @@ tcname (NS n _) = tcname n tcname _ = False +implicitable (NS n _) = implicitable n +implicitable (UN (x:xs)) = isLower x +implicitable _ = False + nsroot (NS n _) = n nsroot n = n diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs --- a/src/IRTS/CodegenC.hs +++ b/src/IRTS/CodegenC.hs @@ -245,6 +245,7 @@ doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)" doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))" +doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))" doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)" doOp v LNoOp args = "" doOp _ _ _ = "FAIL" diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -145,6 +145,9 @@ | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = do arg' <- ir' env arg return $ LLazyExp arg' + | (P _ (UN "par") _, [_, arg]) <- unApply tm + = do arg' <- ir' env arg + return $ LOp LPar [LLazyExp arg'] | (P _ (UN "fork") _, [arg]) <- unApply tm = do arg' <- ir' env arg return $ LOp LFork [LLazyExp arg'] @@ -224,7 +227,8 @@ do args' <- mapM (ir' env) args -- wrap it in a prim__IO -- return $ con_ 0 @@ impossible @@ - return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args') + return $ LLazyExp $ + LForeign LANG_C rty fgnName (zip tys args') | otherwise = fail "Badly formed foreign function call" getFTypes :: TT Name -> [FType] diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs --- a/src/IRTS/Lang.hs +++ b/src/IRTS/Lang.hs @@ -25,6 +25,9 @@ | LError String deriving Eq +-- Primitive operators. Backends are not *required* to implement all +-- of these, but should report an error if they are unable + data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq | LLt | LLe | LGt | LGe | LFPlus | LFMinus | LFTimes | LFDiv | LFEq | LFLt | LFLe | LFGt | LFGe | LBPlus | LBMinus | LBTimes | LBDiv | LBEq | LBLt | LBLe | LBGt | LBGe @@ -38,7 +41,12 @@ | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev | LStdIn | LStdOut | LStdErr - | LFork | LVMPtr | LNoOp + + | LFork + | LPar -- evaluate argument anywhere, possibly on another + -- core or another machine. 'id' is a valid implementation + | LVMPtr + | LNoOp deriving (Show, Eq) -- Supported target languages for foreign calls diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -160,6 +160,13 @@ show n ++ " already defined" _ -> return () +isUndefined :: FC -> Name -> Idris Bool +isUndefined fc n + = do i <- getContext + case lookupTy Nothing n i of + (_:_) -> return False + _ -> return True + setContext :: Context -> Idris () setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } ) @@ -614,7 +621,8 @@ implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg]) implicitise syn ignore ist tm = let (declimps, ns') = execState (imps True [] tm) ([], []) - ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in + ns = filter (\n -> implicitable n || elem n (map fst uvars)) $ + ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in if null ns then (tm, reverse declimps) else implicitise syn ignore ist (pibind uvars ns tm) @@ -693,7 +701,10 @@ pibind using (n:ns) sc = case lookup n using of Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc) - Nothing -> PPi (Imp False Dynamic) n Placeholder (pibind using ns sc) + Nothing -> if (implicitable n) + then PPi (Imp False Dynamic) n Placeholder + (pibind using ns sc) + else pibind using ns sc -- Add implicit arguments in function calls addImplPat :: IState -> PTerm -> PTerm diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -296,6 +296,7 @@ [PDecl' t] | PDSL Name (DSL' t) | PSyntax FC Syntax + | PMutual FC [PDecl' t] | PDirective (Idris ()) deriving Functor {-! @@ -314,6 +315,7 @@ data PData' t = PDatadecl { d_name :: Name, d_tcon :: t, d_cons :: [(Name, t, FC)] } + | PLaterdecl { d_name :: Name, d_tcon :: t } deriving Functor {-! deriving instance Binary PData' diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -76,7 +76,7 @@ addIBC (IBCAccess n Frozen) elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris () -elabData info syn fc codata (PDatadecl n t_in dcons) +elabData info syn fc codata (PLaterdecl n t_in) = do iLOG (show fc) checkUndefined fc n ctxt <- getContext @@ -91,6 +91,23 @@ (cty, _) <- recheckC fc [] t' logLvl 2 $ "---> " ++ show cty updateContext (addTyDecl n cty) -- temporary, to check cons + +elabData info syn fc codata (PDatadecl n t_in dcons) + = do iLOG (show fc) + undef <- isUndefined fc n + ctxt <- getContext + i <- get + t_in <- implicit syn n t_in + let t = addImpl i t_in + ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) [] + (erun fc (build i info False n t)) + def' <- checkDef fc defer + addDeferred def' + mapM_ (elabCaseBlock info) is + (cty, _) <- recheckC fc [] t' + logLvl 2 $ "---> " ++ show cty + -- temporary, to check cons + when undef $ updateContext (addTyDecl n cty) cons <- mapM (elabCon info syn n codata) dcons ttag <- getName i <- get @@ -123,7 +140,7 @@ let nonImp = mapMaybe isNonImp (zip cimp ptys_u) let implBinds = getImplB id cty' update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..]) - mapM_ (elabDecl info) (concat proj_decls) + mapM_ (elabDecl EAll info) (concat proj_decls) mapM_ (tryElabDecl info) (update_decls) where -- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in } @@ -542,7 +559,7 @@ -- ==> fname' ps wpat [rest], match pats against toplevel for ps wb <- mapM (mkAuxC wname lhs (map fst bargs)) withblock logLvl 5 ("with block " ++ show wb) - mapM_ (elabDecl info) wb + mapM_ (elabDecl EAll info) wb -- rhs becomes: fname' ps wval let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++ @@ -628,12 +645,12 @@ logLvl 5 $ "Building functions" let usyn = syn { using = ps ++ using syn } fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints - mapM_ (elabDecl info) (concat fns) + mapM_ (elabDecl EAll info) (concat fns) -- for each method, build a top level function fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods - mapM_ (elabDecl info) (concat fns) + mapM_ (elabDecl EAll info) (concat fns) -- add the default definitions - mapM_ (elabDecl info) (concat (map (snd.snd) defs)) + mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs)) i <- get let defaults = map (\ (x, (y, z)) -> (x,y)) defs addClass tn (CI cn imethods defaults (map fst ps) []) @@ -795,7 +812,7 @@ let idecls = [PClauses fc [Inlinable, TCGen] iname [PClause fc iname lhs [] rhs wb]] iLOG (show idecls) - mapM (elabDecl info) idecls + mapM (elabDecl EAll info) idecls addIBC (IBCInstance intInst n iname) where intInst = case ps of @@ -915,12 +932,17 @@ data ElabWhat = ETypes | EDefns | EAll deriving (Show, Eq) -elabDecl :: ElabInfo -> PDecl -> Idris () -elabDecl info d = idrisCatch (elabDecl' EAll info d) - (\e -> do let msg = show e - setErrLine (getErrLine msg) - iputStrLn msg) +elabDecls :: ElabInfo -> [PDecl] -> Idris () +elabDecls info ds = do mapM_ (elabDecl EAll info) ds +-- mapM_ (elabDecl EDefns info) ds +elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris () +elabDecl what info d + = idrisCatch (elabDecl' what info d) + (\e -> do let msg = show e + setErrLine (getErrLine msg) + iputStrLn msg) + elabDecl' _ info (PFix _ _ _) = return () -- nothing to elaborate elabDecl' _ info (PSyntax _ p) @@ -930,9 +952,12 @@ = do iLOG $ "Elaborating type decl " ++ show n ++ show o elabType info s f o n ty elabDecl' what info (PData s f co d) - | what /= EDefns + | what /= ETypes = do iLOG $ "Elaborating " ++ show (d_name d) elabData info s f co d + | otherwise + = do iLOG $ "Elaborating [type of] " ++ show (d_name d) + elabData info s f co (PLaterdecl (d_name d) (d_tcon d)) elabDecl' what info d@(PClauses f o n ps) | what /= ETypes = do iLOG $ "Elaborating clause " ++ show n @@ -941,6 +966,9 @@ [fs] -> fs [] -> [] elabClauses info f (o ++ o') n ps +elabDecl' what info (PMutual f ps) + = do mapM_ (elabDecl ETypes info) ps + mapM_ (elabDecl EDefns info) ps elabDecl' what info (PParams f ns ps) = do i <- get iLOG $ "Expanding params block with " ++ show (concatMap declared ps) @@ -965,7 +993,7 @@ = do iLOG $ "Elaborating class " ++ show n elabClass info s f cs n ps ds elabDecl' what info (PInstance s f cs n ps t expn ds) - | what /= EDefns + | what /= ETypes = do iLOG $ "Elaborating instance " ++ show n elabInstance info s f cs n ps t expn ds elabDecl' what info (PRecord s f tyn ty cn cty) diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -920,6 +920,9 @@ put x1 put x2 put x3 + PMutual x1 x2 -> do putWord8 11 + put x1 + put x2 get = do i <- getWord8 case i of @@ -980,6 +983,9 @@ x2 <- get x3 <- get return (PCAF x1 x2 x3) + 11 -> do x1 <- get + x2 <- get + return (PMutual x1 x2) _ -> error "Corrupted binary data for PDecl'" instance Binary SyntaxInfo where @@ -1060,15 +1066,26 @@ _ -> error "Corrupted binary data for PClause'" instance (Binary t) => Binary (PData' t) where - put (PDatadecl x1 x2 x3) - = do put x1 - put x2 - put x3 + put x + = case x of + PDatadecl x1 x2 x3 -> do putWord8 0 + put x1 + put x2 + put x3 + PLaterdecl x1 x2 -> do putWord8 1 + put x1 + put x2 get - = do x1 <- get - x2 <- get - x3 <- get - return (PDatadecl x1 x2 x3) + = do i <- getWord8 + case i of + 0 -> do x1 <- get + x2 <- get + x3 <- get + return (PDatadecl x1 x2 x3) + 1 -> do x1 <- get + x2 <- get + return (PLaterdecl x1 x2) + _ -> error "Corrupted binary data for PData'" instance Binary PTerm where put x diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -104,7 +104,7 @@ -- Now add all the declarations to the context v <- verbose when v $ iputStrLn $ "Type checking " ++ f - mapM_ (elabDecl toplevel) ds + elabDecls toplevel ds i <- get -- simplify every definition do give the totality checker -- a better chance @@ -306,6 +306,7 @@ getfc (PClauses fc _ _ _) = fc collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds +collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds' collect (PInstance f s cs n ps t en ds : ds') @@ -329,6 +330,7 @@ return [d'] <|> pUsing syn <|> pParams syn + <|> pMutual syn <|> pNamespace syn <|> pClass syn <|> pInstance syn @@ -454,6 +456,16 @@ fc <- pfc return [PParams fc ns (concat ds)] +pMutual :: SyntaxInfo -> IParser [PDecl] +pMutual syn = + do reserved "mutual" + openBlock + let pvars = syn_params syn + ds <- many1 (pDecl syn) + closeBlock + fc <- pfc + return [PMutual fc (concat ds)] + pNamespace :: SyntaxInfo -> IParser [PDecl] pNamespace syn = do reserved "namespace"; n <- identifier; @@ -1111,34 +1123,36 @@ tyn_in <- pfName ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in - reserved "where" - openBlock - pushIndent - cons <- many (do notEndBlock - c <- pConstructor syn - pKeepTerminator - return c) -- (lchar '|') - popIndent - closeBlock - accData acc tyn (map (\ (n, _, _) -> n) cons) - return $ PData syn fc co (PDatadecl tyn ty cons)) + option (PData syn fc co (PLaterdecl tyn ty)) (do + reserved "where" + openBlock + pushIndent + cons <- many (do notEndBlock + c <- pConstructor syn + pKeepTerminator + return c) -- (lchar '|') + popIndent + closeBlock + accData acc tyn (map (\ (n, _, _) -> n) cons) + return $ PData syn fc co (PDatadecl tyn ty cons))) <|> try (do pushIndent acc <- pAccessibility co <- pDataI fc <- pfc tyn_in <- pfName args <- many pName - let tyn = expandNS syn tyn_in - lchar '=' - cons <- sepBy1 (pSimpleCon syn) (lchar '|') - pTerminator - let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args) let ty = bindArgs (map (const PSet) args) PSet - cons' <- mapM (\ (x, cargs, cfc) -> - do let cty = bindArgs cargs conty - return (x, cty, cfc)) cons - accData acc tyn (map (\ (n, _, _) -> n) cons') - return $ PData syn fc co (PDatadecl tyn ty cons')) + let tyn = expandNS syn tyn_in + option (PData syn fc co (PLaterdecl tyn ty)) (do + lchar '=' + cons <- sepBy1 (pSimpleCon syn) (lchar '|') + pTerminator + let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args) + cons' <- mapM (\ (x, cargs, cfc) -> + do let cty = bindArgs cargs conty + return (x, cty, cfc)) cons + accData acc tyn (map (\ (n, _, _) -> n) cons') + return $ PData syn fc co (PDatadecl tyn ty cons'))) where mkPApp fc t [] = t mkPApp fc t xs = PApp fc t (map pexp xs) diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs --- a/src/Idris/Primitives.hs +++ b/src/Idris/Primitives.hs @@ -280,7 +280,7 @@ putIState i { idris_scprims = (n, sc) : idris_scprims i } elabPrims :: Idris () -elabPrims = do mapM_ (elabDecl toplevel) +elabPrims = do mapM_ (elabDecl EAll toplevel) (map (PData defaultSyntax (FC "builtin" 0) False) [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]) mapM_ elabPrim primitives