idris 0.9.5 → 0.9.5.1

raw patch · 27 files changed

+314/−100 lines, 27 files

Files

• config.mk +3/−0
• idris.cabal +5/−2
• lib/Builtins.idr +3/−0
• lib/Control/Arrow.idr +21/−0
• lib/Control/Category.idr +15/−0
• lib/Prelude/Monad.idr +1/−1
• lib/System/Concurrency/Raw.idr +25/−0
• lib/base.ipkg +4/−2
• rts/Makefile +5/−0
• rts/idris_gc.c +3/−3
• rts/idris_gmp.c +7/−7
• rts/idris_main.c +1/−1
• rts/idris_rts.c +50/−22
• rts/idris_rts.h +20/−3
• rts/libidris_rts.a binary
• src/Core/CoreParser.hs +11/−9
• src/Core/Evaluate.hs +2/−1
• src/Core/TT.hs +4/−0
• src/IRTS/CodegenC.hs +1/−0
• src/IRTS/Compiler.hs +5/−1
• src/IRTS/Lang.hs +9/−1
• src/Idris/AbsSyntax.hs +13/−2
• src/Idris/AbsSyntaxTree.hs +2/−0
• src/Idris/ElabDecls.hs +42/−14
• src/Idris/IBC.hs +25/−8
• src/Idris/Parser.hs +36/−22
• src/Idris/Primitives.hs +1/−1

@@ -0,0 +1,3 @@+GMP_INCLUDE_DIR :=+CC              :=gcc+CABAL           :=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

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

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

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

@@ -1,4 +1,4 @@-module prelude.monad+module Prelude.Monad  -- Monads and Functors 

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

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

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

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

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

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

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

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

binary file changed (27120 → 26024 bytes)

@@ -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 ":!#$%&*+./<=>?@\\^|-~"

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

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

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

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

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

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

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

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

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

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

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