diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.9.3.1 +Version: 0.9.4 License: BSD3 License-file: LICENSE Author: Edwin Brady @@ -42,6 +42,7 @@ 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 lib/control/monad/*.idr lib/language/*.idr tutorial/examples/*.idr @@ -68,10 +69,12 @@ Idris.Coverage, Idris.IBC, Idris.Unlit, Idris.DataOpts, Idris.Transforms, Idris.DSL, - Util.Pretty, + Util.Pretty, Util.System, + Pkg.Package, Pkg.PParser, IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified, - IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler, + IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner, + IRTS.Compiler, Paths_idris diff --git a/lib/Makefile b/lib/Makefile --- a/lib/Makefile +++ b/lib/Makefile @@ -1,26 +1,14 @@ check: .PHONY - $(IDRIS) --noprelude --verbose --check checkall.idr + $(IDRIS) --build base.ipkg recheck: clean check -install: check - mkdir -p $(TARGET)/prelude - mkdir -p $(TARGET)/network - mkdir -p $(TARGET)/language - mkdir -p $(TARGET)/control/monad - install *.ibc $(TARGET) - install prelude/*.ibc $(TARGET)/prelude - install network/*.ibc $(TARGET)/network - install language/*.ibc $(TARGET)/language - install control/monad/*.ibc $(TARGET)/control/monad +install: + $(IDRIS) --install base.ipkg clean: .PHONY - rm -f *.ibc - rm -f prelude/*.ibc - rm -f network/*.ibc - rm -f language/*.ibc - rm -f control/monad/*.ibc + $(IDRIS) --clean base.ipkg linecount: .PHONY wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr diff --git a/lib/io.idr b/lib/io.idr --- a/lib/io.idr +++ b/lib/io.idr @@ -47,4 +47,7 @@ mkLazyForeign : Foreign x -> x -- mkForeign and mkLazyForeign compiled as primitives +fork : |(thread:IO ()) -> IO Ptr +fork x = io_return prim__vm -- compiled specially + diff --git a/lib/network/sockets.idr b/lib/network/sockets.idr deleted file mode 100644 --- a/lib/network/sockets.idr +++ /dev/null @@ -1,78 +0,0 @@ -%include "network.h" -%lib "network.o" - -f_netTest = mkForeign (FFun "netTest" (Cons FStr (Cons FInt Nil)) FInt); - [%nocg] - -f_clientSocket = mkForeign (FFun "net_UDP_clientSocket" - (Cons FStr (Cons FInt Nil)) FPtr); [%eval] -f_serverSocket = mkForeign (FFun "net_UDP_serverSocket" - (Cons FInt Nil) FPtr); [%eval] -f_send = mkForeign (FFun "net_sendUDP" - (Cons FPtr (Cons FStr (Cons FInt (Cons FStr Nil)))) FInt); [%eval] -f_recv = mkForeign (FFun "net_recvUDP" - (Cons FPtr Nil) FPtr); [%eval] - -f_recvBuf = mkForeign (FFun "get_recvBuf" - (Cons FPtr Nil) FStr); [%eval] -f_recvServer = mkForeign (FFun "get_recvServer" - (Cons FPtr Nil) FStr); [%eval] -f_recvPort = mkForeign (FFun "get_recvPort" - (Cons FPtr Nil) FInt); [%eval] - -f_nullPtr = mkForeign (FFun "nullPtr" (Cons FPtr Nil) FInt); [%eval] - -nullPtr : Ptr -> (IO Bool); -nullPtr ptr = do { p <- f_nullPtr ptr; - return (if_then_else (p==1) True False); -}; - -data Socket = mkCon Ptr; -data Recv = mkRecv String String Int - | noRecv; - -clientSocket : String -> Int -> (IO Socket); -clientSocket server port = do { - sock <- f_clientSocket server port; - return (mkCon sock); }; - -serverSocket : Int -> (IO Socket); -serverSocket port = do { - sock <- f_serverSocket port; - return (mkCon sock); }; - -sendTo : Socket -> String -> Int -> String -> (IO ()); -sendTo (mkCon c) server port dat - = do { v <- f_send c server port dat; - return II; }; - -doMkRecv : Bool -> Ptr -> (IO Recv); -doMkRecv True _ = return noRecv; -doMkRecv False rcv = do { - buf <- f_recvBuf rcv; - server <- f_recvServer rcv; - port <- f_recvPort rcv; --- putStrLn ("Port from connection is " ++ (__toString port)); - return (mkRecv buf server port); -}; - -recvFrom : Socket -> (IO Recv); -recvFrom (mkCon c) = do { - rcv <- f_recv c; - nul <- nullPtr rcv; - doMkRecv nul rcv; -}; - - -recvOK : Recv -> Bool; -recvOK (mkRecv _ _ _) = True; -recvOK noRecv = False; - -recvStr : Recv -> String; -recvStr (mkRecv buf server port) = buf; - -recvServer : Recv -> String; -recvServer (mkRecv buf server port) = server; - -recvPort : Recv -> Int; -recvPort (mkRecv buf server port) = port; diff --git a/lib/prelude/complex.idr b/lib/prelude/complex.idr --- a/lib/prelude/complex.idr +++ b/lib/prelude/complex.idr @@ -6,7 +6,7 @@ module prelude.complex import builtins - +import prelude ------------------------------ Rectangular form diff --git a/lib/prelude/tactics.idr b/lib/prelude/tactics.idr deleted file mode 100644 --- a/lib/prelude/tactics.idr +++ /dev/null @@ -1,4 +0,0 @@ -module prelude.tactics - -data Tactic = Intro (List IdrisName) - | Refine IdrisName diff --git a/lib/system.idr b/lib/system.idr --- a/lib/system.idr +++ b/lib/system.idr @@ -9,10 +9,10 @@ ga' [] 0 n where numArgs : IO Int - numArgs = mkForeign (FFun "epic_numArgs" [] FInt) + numArgs = mkForeign (FFun "idris_numArgs" [FPtr] FInt) prim__vm getArg : Int -> IO String - getArg x = mkForeign (FFun "epic_getArg" [FInt] FString) x + getArg x = mkForeign (FFun "idris_getArg" [FPtr, FInt] (FAny String)) prim__vm x ga' : List String -> Int -> Int -> IO (List String) ga' acc i n = if (i == n) then (return $ reverse acc) else diff --git a/rts/Makefile b/rts/Makefile --- a/rts/Makefile +++ b/rts/Makefile @@ -1,6 +1,6 @@ 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 +CFLAGS = -O2 -Wall -Werror 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 @@ -5,7 +5,7 @@ VAL copy(VM* vm, VAL x) { int i; VAL* argptr; - Closure* cl; + Closure* cl = NULL; if (x==NULL || ISINT(x)) { return x; } @@ -36,6 +36,8 @@ break; case FWD: return x->info.ptr; + default: + break; } x->ty = FWD; x->info.ptr = cl; @@ -62,6 +64,8 @@ argptr++; } break; + default: // Nothing to copy + break; } scan += inc; } @@ -84,6 +88,12 @@ VAL* root; for(root = vm->valstack; root < vm->valstack_top; ++root) { + *root = copy(vm, *root); + } + for(root = vm->inbox_ptr; root < vm->inbox_write; ++root) { + *root = copy(vm, *root); + } + for(root = vm->argv; root < vm->argv + vm->argc; ++root) { *root = copy(vm, *root); } vm->ret = copy(vm, vm->ret); diff --git a/rts/idris_main.c b/rts/idris_main.c --- a/rts/idris_main.c +++ b/rts/idris_main.c @@ -1,8 +1,9 @@ int main(int argc, char* argv[]) { - VM* vm = init_vm(4096000, 2048000); // 1024000); + VM* vm = init_vm(4096000, 2048000, argc, argv); // 1024000); _idris__123_runMain0_125_(vm, NULL); //_idris_main(vm, NULL); #ifdef IDRIS_TRACE gcInfo(vm, 1); #endif + terminate(vm); } diff --git a/rts/idris_rts.c b/rts/idris_rts.c --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -3,37 +3,73 @@ #include #include #include +#include +#include #include "idris_rts.h" #include "idris_gc.h" -VM* init_vm(int stack_size, size_t heap_size) { +VM* init_vm(int stack_size, size_t heap_size, 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)); VM* vm = malloc(sizeof(VM)); - vm -> valstack = valstack; - vm -> valstack_top = valstack; - vm -> valstack_base = valstack; - vm -> intstack = intstack; - vm -> intstack_ptr = intstack; - vm -> floatstack = floatstack; - vm -> floatstack_ptr = floatstack; - vm -> stack_max = valstack + stack_size; - vm -> heap = malloc(heap_size); - vm -> oldheap = NULL; - vm -> heap_next = vm -> heap; - vm -> heap_end = vm -> heap + heap_size; - vm -> heap_size = heap_size; - vm -> collections = 0; - vm -> allocations = 0; - vm -> heap_growth = heap_size; - vm -> ret = NULL; - vm -> reg1 = NULL; + vm->valstack = valstack; + vm->valstack_top = valstack; + vm->valstack_base = valstack; + vm->intstack = intstack; + vm->intstack_ptr = intstack; + vm->floatstack = floatstack; + vm->floatstack_ptr = floatstack; + vm->stack_max = valstack + stack_size; + vm->heap = malloc(heap_size); + vm->oldheap = NULL; + vm->heap_next = vm->heap; + vm->heap_end = vm->heap + heap_size; + vm->heap_size = heap_size; + vm->collections = 0; + vm->allocations = 0; + vm->heap_growth = heap_size; + vm->ret = NULL; + vm->reg1 = NULL; + + vm->inbox = malloc(1024*sizeof(VAL)); + vm->inbox_end = vm->inbox + 1024; + vm->inbox_ptr = vm->inbox; + vm->inbox_write = vm->inbox; + + pthread_mutex_init(&(vm->inbox_lock), NULL); + pthread_mutex_init(&(vm->inbox_block), NULL); + pthread_cond_init(&(vm->inbox_waiting), NULL); + + int i; + + // Assumption: there's enough space for this in the initial heap. + vm->argv = malloc(argc*sizeof(VAL)); + vm->argc = argc; + + for(i = 0; i < argc; ++i) { + vm->argv[i] = MKSTR(vm, argv[i]); + } + return vm; } +void terminate(VM* vm) { + free(vm->inbox); + free(vm->valstack); + free(vm->intstack); + free(vm->floatstack); + free(vm->heap); + free(vm->argv); + if (vm->oldheap != NULL) { free(vm->oldheap); } + pthread_mutex_destroy(&(vm -> inbox_lock)); + pthread_mutex_destroy(&(vm -> inbox_block)); + pthread_cond_destroy(&(vm -> inbox_waiting)); + free(vm); +} + void* allocate(VM* vm, size_t size) { // return malloc(size); if ((size & 7)!=0) { @@ -158,6 +194,9 @@ } printf("] "); break; + case STRING: + printf("STR[%s]", v->info.str); + break; case FWD: printf("FWD "); dumpVal((VAL)(v->info.ptr)); @@ -305,6 +344,145 @@ return cl; } +typedef struct { + VM* vm; + func fn; + VAL arg; +} ThreadData; + +void* runThread(void* arg) { + ThreadData* td = (ThreadData*)arg; + VM* vm = td->vm; + + TOP(0) = td->arg; + BASETOP(0); + ADDTOP(1); + td->fn(vm, NULL); + + free(td); + return NULL; +} + +void* vmThread(VM* callvm, func f, VAL arg) { + VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size, 0, NULL); + pthread_t t; + pthread_attr_t attr; +// size_t stacksize; + + pthread_attr_init(&attr); +// pthread_attr_getstacksize (&attr, &stacksize); +// pthread_attr_setstacksize (&attr, stacksize*64); + + ThreadData *td = malloc(sizeof(ThreadData)); + td->vm = vm; + td->fn = f; + td->arg = copyTo(vm, arg); + + pthread_create(&t, &attr, runThread, td); + usleep(100); + return vm; +} + +// VM is assumed to be a different vm from the one x lives on (so we don't need +// to worry about gc moving things, as the VM x is on will not be allocating) + +VAL copyTo(VM* vm, VAL x) { + int i; + VAL* argptr; + Closure* cl; + if (x==NULL || ISINT(x)) { + return x; + } + switch(x->ty) { + case CON: + cl = allocCon(vm, x->info.c.arity); + cl->info.c.tag = x->info.c.tag; + cl->info.c.arity = x->info.c.arity; + + argptr = (VAL*)(cl->info.c.args); + for(i = 0; i < x->info.c.arity; ++i) { + *argptr = copyTo(vm, *((VAL*)(x->info.c.args)+i)); // recursive version + argptr++; + } + break; + case FLOAT: + cl = MKFLOAT(vm, x->info.f); + break; + case STRING: + cl = MKSTR(vm, x->info.str); + break; + case BIGINT: + cl = MKBIGM(vm, x->info.ptr); + break; + case PTR: + cl = MKPTR(vm, x->info.ptr); + break; + default: + assert(0); // We're in trouble if this happens... + } + return cl; +} + +// Add a message to another VM's message queue +void 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); + + pthread_mutex_lock(&(dest->inbox_lock)); + + *(dest->inbox_write) = dmsg; + + dest->inbox_write++; + if (dest->inbox_write >= dest->inbox_end) { + dest->inbox_write = dest->inbox; + } + + if (dest->inbox_write == dest->inbox_ptr) { + fprintf(stderr, "Inbox full"); // Maybe grow it instead... + exit(-1); + } + + // Wake up the other thread + pthread_cond_signal(&(dest->inbox_waiting)); + + pthread_mutex_unlock(&(dest->inbox_lock)); +} + +// block until there is a message in the queue +VAL recvMessage(VM* vm) { + VAL msg = NULL; + + while (msg == NULL) { + pthread_mutex_lock(&vm->inbox_block); + pthread_cond_wait(&vm->inbox_waiting, &vm->inbox_block); + pthread_mutex_unlock(&vm->inbox_block); + msg = *(vm->inbox_ptr); + } + if (msg != NULL) { + pthread_mutex_lock(&(vm->inbox_lock)); + *(vm->inbox_ptr) = NULL; + vm->inbox_ptr++; + if (vm->inbox_ptr >= vm->inbox_end) { + vm->inbox_ptr = vm->inbox; + } + pthread_mutex_unlock(&(vm->inbox_lock)); + } else { + fprintf(stderr, "No messages waiting"); + exit(-1); + } + + return msg; +} + +int idris_numArgs(VM* vm) { + return vm->argc; +} + +VAL idris_getArg(VM* vm, int i) { + return vm->argv[i]; +} void stackOverflow() { fprintf(stderr, "Stack overflow"); diff --git a/rts/idris_rts.h b/rts/idris_rts.h --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -6,6 +6,7 @@ #include #include #include +#include // Closures @@ -45,6 +46,20 @@ char* heap_next; char* heap_end; VAL* stack_max; + + pthread_mutex_t inbox_lock; + pthread_mutex_t inbox_block; + pthread_cond_t inbox_waiting; + + VAL* inbox; // Block of memory for storing messages + VAL* inbox_end; // End of block of memory + + VAL* inbox_ptr; // Next message to read + VAL* inbox_write; // Location of next message to write + + int argc; + VAL* argv; // command line arguments + size_t heap_size; size_t heap_growth; int allocations; @@ -53,7 +68,10 @@ VAL reg1; } VM; -VM* init_vm(int stack_size, size_t heap_size); +// Create a new VM +VM* init_vm(int stack_size, size_t heap_size, int argc, char* argv[]); +// Clean up a VM once it's no longer needed +void terminate(VM* vm); // Functions all take a pointer to their VM, and previous stack base, // and return nothing. @@ -83,7 +101,7 @@ #define ISINT(x) ((((i_int)x)&1) == 1) #define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1))) -#define FLOATOP(op,x,y) MKFLOAT(((GETFLOAT(x)) op (GETFLOAT(y)))) +#define FLOATOP(op,x,y) MKFLOAT(vm, ((GETFLOAT(x)) op (GETFLOAT(y)))) #define FLOATBOP(op,x,y) MKINT((i_int)(((GETFLOAT(x)) op (GETFLOAT(y))))) #define ADD(x,y) (void*)(((i_int)x)+(((i_int)y)-1)) #define MULT(x,y) (MKINT((((i_int)x)>>1) * (((i_int)y)>>1))) @@ -118,6 +136,16 @@ void* allocate(VM* vm, size_t size); void* allocCon(VM* vm, int arity); +void* vmThread(VM* callvm, func f, VAL arg); + +// Copy a structure to another vm's heap +VAL copyTo(VM* newVM, VAL x); + +// Add a message to another VM's message queue +void sendMessage(VM* sender, VM* dest, VAL msg); +// block until there is a message in the queue +VAL recvMessage(VM* vm); + void dumpVal(VAL r); void dumpStack(VM* vm); @@ -144,6 +172,11 @@ VAL idris_strCons(VM* vm, VAL x, VAL xs); VAL idris_strIndex(VM* vm, VAL str, VAL i); VAL idris_strRev(VM* vm, VAL str); + +// Command line args + +int idris_numArgs(VM* vm); +VAL idris_getArg(VM* vm, int i); // Handle stack overflow. // Just reports an error and exits. 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/rts/libtest.c b/rts/libtest.c new file mode 100644 --- /dev/null +++ b/rts/libtest.c @@ -0,0 +1,1 @@ +int main() {} diff --git a/src/Core/CaseTree.hs b/src/Core/CaseTree.hs --- a/src/Core/CaseTree.hs +++ b/src/Core/CaseTree.hs @@ -31,10 +31,19 @@ type Clause = ([Pat], (Term, Term)) type CS = ([Term], Int) +instance TermSize SC where + termsize (Case n as) = termsize as + termsize (STerm t) = termsize t + termsize _ = 1 + +instance TermSize CaseAlt where + termsize (ConCase _ _ _ s) = termsize s + termsize (ConstCase _ s) = termsize s + termsize (DefaultCase s) = termsize s + -- simple terms can be inlined trivially - good for primitives in particular small :: SC -> Bool --- small (STerm t) = True -small _ = False +small t = termsize t < 150 namesUsed :: SC -> [Name] namesUsed sc = nub $ nu' [] sc where @@ -121,6 +130,7 @@ data Partition = Cons [Clause] | Vars [Clause] + deriving Show isVarPat (PV _ : ps , _) = True isVarPat (PAny : ps , _) = True @@ -145,7 +155,8 @@ = do (ts, v) <- get put (ts ++ (map (fst.snd) xs), v) return $ STerm (snd ret) -- run out of arguments -match vs cs err = do cs <- mixture vs (partition cs) err +match vs cs err = do let ps = partition cs + cs <- mixture vs ps err return cs mixture :: [Name] -> [Partition] -> SC -> State CS SC @@ -188,18 +199,22 @@ argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause]) argsToAlt [] = return ([], []) -argsToAlt rs@((r, m) : _) +argsToAlt rs@((r, m) : rest) = do newArgs <- getNewVars r return (newArgs, addRs rs) where getNewVars [] = return [] - getNewVars ((PV n) : ns) = do nsv <- getNewVars ns - return (n : nsv) + getNewVars ((PV n) : ns) = do v <- getVar + nsv <- getNewVars ns + return (v : nsv) getNewVars (_ : ns) = do v <- getVar nsv <- getNewVars ns return (v : nsv) addRs [] = [] addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs) + + uniq i (UN n) = MN i n + uniq i n = n getVar :: State CS Name getVar = do (t, v) <- get; put (t, v+1); return (MN v "e") diff --git a/src/Core/Constraints.hs b/src/Core/Constraints.hs --- a/src/Core/Constraints.hs +++ b/src/Core/Constraints.hs @@ -11,6 +11,7 @@ import Data.Maybe import qualified Data.Map as M +import Debug.Trace ucheck :: [(UConstraint, FC)] -> TC () ucheck cs = acyclic rels (map fst (M.toList rels)) @@ -23,11 +24,16 @@ mkRels :: [(UConstraint, FC)] -> Relations -> Relations mkRels [] acc = acc mkRels ((c, f) : cs) acc - = case M.lookup (lhs c) acc of - Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc) - Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc) + | not (ignore c) + = case M.lookup (lhs c) acc of + Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc) + Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc) + | otherwise = mkRels cs acc where lhs (ULT l _) = l lhs (ULE l _) = l + ignore (ULE l r) = l == r + ignore _ = False + acyclic :: Relations -> [UExp] -> TC () acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs --- a/src/Core/Elaborate.hs +++ b/src/Core/Elaborate.hs @@ -435,13 +435,21 @@ case runStateT t1 s of OK (v, s') -> do put s' return v - Error e1 -> do put s - case runStateT t2 s of - OK (v, s') -> do put s'; return v - Error e2 -> if score e1 > score e2 - then lift (tfail e1) - else lift (tfail e2) - + Error e1 -> if recoverableErr e1 then + do case runStateT t2 s of + OK (v, s') -> do put s'; return v + Error e2 -> if score e1 > score e2 + then lift (tfail e1) + else lift (tfail e2) + else lift (tfail e1) + where recoverableErr (CantUnify r _ _ _ _ _) = r + recoverableErr _ = True + +tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a +tryWhen True a b = try a b +tryWhen False a b = a + + -- Try a selection of tactics. Exactly one must work, all others must fail tryAll :: [(Elab' aux a, String)] -> Elab' aux a tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs) diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -1,7 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-} -module Core.Evaluate(normalise, normaliseC, normaliseAll, +module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll, simplify, specialise, hnf, convEq, convEq', Def(..), Accessibility(..), Totality(..), PReason(..), Context, initContext, ctxtAlist, uconstraints, next_tvar, @@ -83,22 +83,25 @@ -- Normalise fully type checked terms (so, assume all names/let bindings resolved) normaliseC :: Context -> Env -> TT Name -> TT Name normaliseC ctxt env t - = evalState (do val <- eval ctxt threshold [] env t [] + = evalState (do val <- eval False ctxt threshold [] env t [] quote 0 val) initEval normaliseAll :: Context -> Env -> TT Name -> TT Name normaliseAll ctxt env t - = evalState (do val <- eval ctxt threshold [] env t [AtREPL] + = evalState (do val <- eval False ctxt threshold [] env t [AtREPL] quote 0 val) initEval normalise :: Context -> Env -> TT Name -> TT Name -normalise ctxt env t - = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [] +normalise = normaliseTrace False + +normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name +normaliseTrace tr ctxt env t + = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) [] quote 0 val) initEval specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name specialise ctxt env limits t - = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) [] + = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) [] quote 0 val) (initEval { limited = limits }) -- Like normalise, but we only reduce functions that are marked as okay to @@ -106,13 +109,13 @@ simplify :: Context -> Env -> TT Name -> TT Name simplify ctxt env t - = evalState (do val <- eval ctxt threshold [] + = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0)] (map finalEntry env) (finalise t) [Simplify] quote 0 val) initEval hnf :: Context -> Env -> TT Name -> TT Name hnf ctxt env t - = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF] + = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF] quote 0 val) initEval @@ -130,12 +133,13 @@ unbindEnv [] tm = tm unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc -usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)]) -usable n [] = (True, []) -usable n ns = case lookup n ns of - Just 0 -> (False, ns) - Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns) - _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns) +usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)]) +usable s n [] = (True, []) +usable s n ns = case lookup n ns of + Just 0 -> (False, ns) + Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns) + _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns) + else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns) reduction :: Eval () reduction = do ES ns s <- get @@ -144,8 +148,9 @@ -- Evaluate in a context of locally named things (i.e. not de Bruijn indexed, -- such as we might have during construction of a proof) -eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value -eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where +eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name -> + [EvalOpt] -> Eval Value +eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where spec = Spec `elem` opts simpl = Simplify `elem` opts atRepl = AtREPL `elem` opts @@ -154,7 +159,7 @@ | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred ev ntimes stk top env v ev ntimes_in stk top env (P Ref n ty) - | (True, ntimes) <- usable n ntimes_in + | (True, ntimes) <- usable simpl n ntimes_in = do let val = lookupDefAcc Nothing n atRepl ctxt when (not atRepl) $ step maxred case val of @@ -174,10 +179,17 @@ ev ntimes stk top env (V i) | i < length env = return $ env !! i | otherwise = return $ VV i ev ntimes stk top env (Bind n (Let t v) sc) + | not simpl || vinstances 0 sc < 2 = do v' <- ev ntimes stk top env v --(finalise v) when (not atRepl) $ step maxred sc' <- ev ntimes stk top (v' : env) sc wknV (-1) sc' + | otherwise + = do t' <- ev ntimes stk top env t + v' <- ev ntimes stk top env v --(finalise v) + when (not atRepl) $ step maxred + sc' <- ev ntimes stk top (v' : env) sc + return $ VBind n (Let t' v') (\x -> return sc') ev ntimes stk top env (Bind n (NLet t v) sc) = do t' <- ev ntimes stk top env (finalise t) v' <- ev ntimes stk top env (finalise v) @@ -215,8 +227,8 @@ -- apply ntimes stk False env f args -- | spec = specApply ntimes stk env f args apply ntimes_in stk top env f@(VP Ref n ty) args - | (True, ntimes) <- usable n ntimes_in - = -- trace (show n) $ + | (True, ntimes) <- usable simpl n ntimes_in + = traceWhen traceon (show stk) $ do let val = lookupDefAcc Nothing n atRepl ctxt case val of [(CaseOp inl _ _ ns tree _ _, Public)] -> @@ -629,7 +641,7 @@ ctxtAlist :: Context -> [(Name, Def)] ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt) -veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval +veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt @@ -679,16 +691,13 @@ Type -> Context -> Context addCasedef n alwaysInline tcase covering ps psrt ty uctxt = let ctxt = definitions uctxt - ps' = ps -- simpl ps in - ctxt' = case (simpleCase tcase covering (FC "" 0) ps', + ctxt' = case (simpleCase tcase covering (FC "" 0) ps, simpleCase tcase covering (FC "" 0) psrt) of (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) -> - let inl = alwaysInline in + let inl = alwaysInline || small sc' in addDef n (CaseOp inl ty ps args sc args' sc', Public, Unchecked) ctxt in uctxt { definitions = ctxt' } - where simpl [] = [] - simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context addOperator n ty a op uctxt diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs --- a/src/Core/ProofState.hs +++ b/src/Core/ProofState.hs @@ -425,11 +425,21 @@ _ -> fail "Not an equality type" where -- to make the P for rewrite, replace syntactic occurrences of l in ty with - -- and x, and put \x : lt in front + -- an x, and put \x : lt in front mkP lt l r ty | l == ty = lt mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f a' = if (r /= a) then mkP lt l r a else a in App f' a' + mkP lt l r (Bind n b sc) + = let b' = mkPB b + sc' = if (r /= sc) then mkP lt l r sc else sc in + Bind n b' sc' + where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t + v' = if (r /= v) then mkP lt l r v else v in + Let t' v' + mkPB b = let ty = binderTy b + ty' = if (r /= ty) then mkP lt l r ty else ty in + b { binderTy = ty' } mkP lt l r x = x rname = MN 0 "replaced" diff --git a/src/Core/TT.hs b/src/Core/TT.hs --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -44,8 +44,12 @@ data Err = Msg String | InternalMsg String - | CantUnify Term Term Err [(Name, Type)] Int -- Int is 'score' - how much we did unify + | CantUnify Bool Term Term Err [(Name, Type)] Int + -- Int is 'score' - how much we did unify + -- Bool indicates recoverability, True indicates more info may make + -- unification succeed | NoSuchVariable Name + | NoTypeDecl Name | NotInjective Term Term Term | CantResolve Term | CantResolveAlts [String] @@ -59,8 +63,9 @@ instance Sized Err where size (Msg msg) = length msg size (InternalMsg msg) = length msg - size (CantUnify left right err _ score) = size left + size right + size err + size (CantUnify _ left right err _ score) = size left + size right + size err size (NoSuchVariable name) = size name + size (NoTypeDecl name) = size name size (NotInjective l c r) = size l + size c + size r size (CantResolve trm) = size trm size (CantResolveAlts _) = 1 @@ -71,7 +76,7 @@ size (Inaccessible _) = 1 score :: Err -> Int -score (CantUnify _ _ m _ s) = s + score m +score (CantUnify _ _ _ m _ s) = s + score m score (CantResolve _) = 20 score (NoSuchVariable _) = 1000 score _ = 0 @@ -79,14 +84,14 @@ instance Show Err where show (Msg s) = s show (InternalMsg s) = "Internal error: " ++ show s - show (CantUnify l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " " - ++ show e ++ " in " ++ show sc ++ " " ++ show i + show (CantUnify _ l r e sc i) = "CantUnify " ++ show l ++ " " ++ show r ++ " " + ++ show e ++ " in " ++ show sc ++ " " ++ show i show (Inaccessible n) = show n ++ " is not an accessible pattern variable" show _ = "Error" instance Pretty Err where pretty (Msg m) = text m - pretty (CantUnify l r e _ i) = + pretty (CantUnify _ l r e _ i) = if size l + size r > breakingSize then text "Cannot unify" <+> colon $$ nest nestingSize (pretty l <+> text "and" <+> pretty r) $$ @@ -412,6 +417,20 @@ deriving instance Binary TT !-} +class TermSize a where + termsize :: a -> Int + +instance TermSize a => TermSize [a] where + termsize [] = 0 + termsize (x : xs) = termsize x + termsize xs + +instance TermSize (TT a) where + termsize (P _ _ _) = 1 + termsize (V _) = 1 + termsize (Bind n (Let t v) sc) = termsize v + termsize sc + termsize (App f a) = termsize f + termsize a + termsize _ = 1 + instance Sized a => Sized (TT a) where size (P name n trm) = 1 + size name + size n + size trm size (V v) = 1 @@ -453,6 +472,15 @@ isInjective (Bind _ (Pi _) sc) = True isInjective (App f a) = isInjective f isInjective _ = False + +-- Count the number of instances of a de Bruijn index in a term +vinstances :: Int -> TT n -> Int +vinstances i (V x) | i == x = 1 +vinstances i (App f a) = vinstances i f + vinstances i a +vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc + where instancesB (Let t v) = vinstances i v + instancesB _ = 0 +vinstances i t = 0 instantiate :: TT n -> TT n -> TT n instantiate e = subst 0 where diff --git a/src/Core/Unify.hs b/src/Core/Unify.hs --- a/src/Core/Unify.hs +++ b/src/Core/Unify.hs @@ -28,8 +28,10 @@ = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, []) -- _ -> + -- trace ("Unifying " ++ show (topx, topy)) $ let topxn = normalise ctxt env topx topyn = normalise ctxt env topy in +-- trace ("Unifying " ++ show (topxn, topyn)) $ case runStateT (un' False [] topxn topyn) (UI 0 [] []) of OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails) @@ -60,6 +62,15 @@ un' :: Bool -> [(Name, Name)] -> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)] + un' fn names x y | x == y = return [] -- shortcut + un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _) + | x /= y = unifyFail topx topy + un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _) + | x /= y = unifyFail topx topy + un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _) + = unifyFail topx topy + un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _) + = unifyFail topx topy un' fn bnames (P Bound x _) (P Bound y _) | (x,y) `elem` bnames = do sc 1; return [] un' fn bnames (P Bound x _) tm @@ -77,8 +88,11 @@ un' fn bnames (P Bound x _) (V i) | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return [] - un' fn bnames (App fx ax) (App fy ay) - = do uplus -- do the second one if the first adds any errors + un' fn bnames appx@(App fx ax) appy@(App fy ay) + = do let (headx, _) = unApply fx + let (heady, _) = unApply fy + checkHeads headx heady + uplus -- do the second one if the first adds any errors (do hf <- un' True bnames fx fy let ax' = hnormalise hf ctxt env (substNames hf ax) let ay' = hnormalise hf ctxt env (substNames hf ay) @@ -93,6 +107,16 @@ combine bnames hf ha) where hnormalise [] _ _ t = t hnormalise ns ctxt env t = normalise ctxt env t + checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _) + | x /= y = unifyFail appx appy + checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _) + | x /= y = unifyFail appx appy + checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _) + = unifyFail appx appy + checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _) + = unifyFail appx appy + checkHeads _ _ = return [] + un' fn bnames x (Bind n (Lam t) (App y (P Bound n' _))) | n == n' = un' False bnames x y un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y @@ -104,10 +128,21 @@ un' fn bnames x y | OK True <- convEq' ctxt x y = do sc 1; return [] | otherwise = do UI s i f <- get - let err = CantUnify topx topy (CantUnify x y (Msg "") [] s) (errEnv env) s + let r = recoverable x y + let err = CantUnify r + topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s put (UI s i ((x, y, env, err) : f)) return [] -- lift $ tfail err + -- shortcut failure, if we *know* nothing can fix it + unifyFail x y = do UI s i f <- get + let r = recoverable x y + let err = CantUnify r + topx topy (CantUnify r x y (Msg "") [] s) (errEnv env) s + put (UI s i ((x, y, env, err) : f)) + lift $ tfail err + + uB bnames (Let tx vx) (Let ty vy) = do h1 <- un' False bnames tx ty h2 <- un' False bnames ty vy @@ -123,8 +158,9 @@ uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty uB bnames x y = do UI s i f <- get - let err = CantUnify topx topy - (CantUnify (binderTy x) (binderTy y) (Msg "") [] s) + let r = recoverable (binderTy x) (binderTy y) + let err = CantUnify r topx topy + (CantUnify r (binderTy x) (binderTy y) (Msg "") [] s) (errEnv env) s put (UI s i ((binderTy x, binderTy y, env, err) : f)) return [] -- lift $ tfail err @@ -136,6 +172,22 @@ Just t' -> do un' False bnames t t' sc 1 combine bnames as bs + + -- If there are any clashes of constructors, deem it unrecoverable, otherwise some + -- more work may help. + -- FIXME: Depending on how overloading gets used, this may cause problems. Better + -- rethink overloading properly... + + recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) + | x == y = True + | otherwise = False +-- recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False +-- recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False + recoverable p@(P _ _ _) (App f a) = recoverable p f + recoverable (App f a) p@(P _ _ _) = recoverable f p + recoverable (App f a) (App f' a') + = recoverable f f' && recoverable a a' + recoverable _ _ = True errEnv = map (\(x, b) -> (x, binderTy b)) diff --git a/src/IRTS/Bytecode.hs b/src/IRTS/Bytecode.hs --- a/src/IRTS/Bytecode.hs +++ b/src/IRTS/Bytecode.hs @@ -1,5 +1,8 @@ module IRTS.Bytecode where +-- Bytecode for a stack based VM (e.g. for generating C code with an accurate +-- hand written GC) + import IRTS.Lang import IRTS.Simplified import Core.TT diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs --- a/src/IRTS/CodegenC.hs +++ b/src/IRTS/CodegenC.hs @@ -1,5 +1,3 @@ -{-# LANGUAGE CPP #-} - module IRTS.CodegenC where import IRTS.Bytecode @@ -7,18 +5,19 @@ import IRTS.Simplified import Core.TT import Paths_idris +import Util.System import Data.Char import System.Process import System.Exit import System.IO import System.Directory -import System.Environment import Control.Monad data DbgLevel = NONE | DEBUG | TRACE -codegenC :: [(Name, SDecl)] -> +codegenC :: Maybe FilePath -> -- dump output + [(Name, SDecl)] -> String -> -- output file name Bool -> -- generate executable if True, only .o if False [FilePath] -> -- include files @@ -26,7 +25,7 @@ String -> -- extra compiler flags DbgLevel -> IO () -codegenC defs out exec incs objs libs dbg +codegenC dump defs out exec incs objs libs dbg = do -- print defs let bc = map toBC defs let h = concatMap toDecl (map fst bc) @@ -40,19 +39,21 @@ hFlush tmph hClose tmph let useclang = False - let comp = if useclang then "clang" else "gcc" + comp <- getCC let gcc = comp ++ " -I. " ++ objs ++ " -x c " ++ (if exec then "" else " - c ") ++ gccDbg dbg ++ " " ++ tmpn ++ " `idris --link` `idris --include` " ++ libs ++ - " -lidris_rts -lgmp -o " ++ out - -- putStrLn cout + " -o " ++ out + case dump of + Just co -> do writeFile co cout + Nothing -> return () exit <- system gcc when (exit /= ExitSuccess) $ putStrLn ("FAILURE: " ++ gcc) -headers [] = "#include \n#include \n#include\n" +headers [] = "#include \n#include \n#include \n" headers (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs debug TRACE = "#define IDRIS_TRACE\n\n" @@ -177,7 +178,7 @@ doOp v LGt [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")" doOp v LGe [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")" -doOp v LFPlus [l, r] = v ++ "FLOATOP(+" ++ creg l ++ ", " ++ creg r ++ ")" +doOp v LFPlus [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")" doOp v LFMinus [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")" doOp v LFTimes [l, r] = v ++ "FLOATOP(*" ++ creg l ++ ", " ++ creg r ++ ")" doOp v LFDiv [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")" @@ -239,22 +240,7 @@ doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)" doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)" +doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))" +doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)" doOp v LNoOp [x] = "" doOp _ _ _ = "FAIL" - -tempfile :: IO (FilePath, Handle) -tempfile = do env <- environment "TMPDIR" - let dir = case env of - Nothing -> "/tmp" - (Just d) -> d - openTempFile dir "idris" - -environment :: String -> IO (Maybe String) -environment x = catch (do e <- getEnv x - return (Just e)) -#if MIN_VERSION_base(4,6,0) - (\y-> do return (y::SomeException); return Nothing) -#endif -#if !MIN_VERSION_base(4,6,0) - (\_-> return Nothing) -#endif diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs --- a/src/IRTS/Compiler.hs +++ b/src/IRTS/Compiler.hs @@ -6,6 +6,8 @@ import IRTS.Defunctionalise import IRTS.Simplified import IRTS.CodegenC +import IRTS.CodegenJava +import IRTS.Inliner import Idris.AbsSyntax import Core.TT @@ -21,28 +23,37 @@ import Paths_idris -compileC :: FilePath -> Term -> Idris () -compileC f tm = do checkMVs - let tmnames = namesUsed (STerm tm) - used <- mapM (allNames []) tmnames - defsIn <- mkDecls tm (concat used) - maindef <- irMain tm - objs <- getObjectFiles - libs <- getLibs - hdrs <- getHdrs - let defs = defsIn ++ [(MN 0 "runMain", maindef)] - -- iputStrLn $ showSep "\n" (map show defs) - let (nexttag, tagged) = addTags 0 (liftAll defs) - let ctxtIn = addAlist tagged emptyContext - let defuns = defunctionalise nexttag ctxtIn - -- iputStrLn $ showSep "\n" (map show (toAlist defuns)) - let checked = checkDefs defuns (toAlist defuns) - case checked of - OK c -> do -- iputStrLn $ showSep "\n" (map show c) - liftIO $ codegenC c f True hdrs - (concatMap mkObj objs) - (concatMap mkLib libs) NONE - Error e -> fail $ show e +compile :: Target -> FilePath -> Term -> Idris () +compile target f tm + = do checkMVs + let tmnames = namesUsed (STerm tm) + used <- mapM (allNames []) tmnames + defsIn <- mkDecls tm (concat used) + maindef <- irMain tm + objs <- getObjectFiles + libs <- getLibs + hdrs <- getHdrs + let defs = defsIn ++ [(MN 0 "runMain", maindef)] + -- iputStrLn $ showSep "\n" (map show defs) + let (nexttag, tagged) = addTags 65536 (liftAll defs) + let ctxtIn = addAlist tagged emptyContext + iLOG "Defunctionalising" + let defuns_in = defunctionalise nexttag ctxtIn + logLvl 5 $ show defuns_in + iLOG "Inlining" + let defuns = inline defuns_in + logLvl 5 $ show defuns + + -- iputStrLn $ showSep "\n" (map show (toAlist defuns)) + let checked = checkDefs defuns (toAlist defuns) + dumpC <- getDumpC + case checked of + OK c -> case target of + ViaC -> liftIO $ codegenC dumpC c f True hdrs + (concatMap mkObj objs) + (concatMap mkLib libs) NONE + ViaJava -> liftIO $ codegenJava c f + Error e -> fail $ show e where checkMVs = do i <- get case idris_metavars i \\ primDefs of [] -> return () @@ -97,7 +108,7 @@ return (declArgs [] n e) mkLDecl n (CaseOp _ _ pats _ _ args sc) = do e <- ir (args, sc) return (declArgs [] n e) -mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n (-1) a +mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n))) @@ -105,12 +116,15 @@ ir tm = ir' [] tm where ir' env tm@(App f a) | (P _ (UN "mkForeign") _, args) <- unApply tm - = doForeign args + = doForeign env args | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm = ir' env arg | (P _ (UN "lazy") _, [_, arg]) <- unApply tm = do arg' <- ir' env arg return $ LLazyExp arg' + | (P _ (UN "fork") _, [arg]) <- unApply tm + = do arg' <- ir' env arg + return $ LOp LFork [LLazyExp arg'] | (P _ (UN "prim__IO") _, [v]) <- unApply tm = do v' <- ir' env v return v' @@ -132,10 +146,12 @@ args' <- mapM (ir' env) args return (LApp False f' args') ir' env (P _ n _) = return $ LV (Glob n) - ir' env (V i) = return $ LV (Glob (env!!i)) + ir' env (V i) | i < length env = return $ LV (Glob (env!!i)) + | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm ir' env (Bind n (Lam _) sc) - = do sc' <- ir' (n : env) sc - return $ LLam [n] sc' + = do let n' = uniqueName n env + sc' <- ir' (n' : env) sc + return $ LLam [n'] sc' ir' env (Bind n (Let _ v) sc) = do sc' <- ir' (n : env) sc v' <- ir' env v @@ -157,16 +173,16 @@ buildApp env e xs = do xs' <- mapM (ir' env) xs return $ LApp False e xs' -doForeign :: [TT Name] -> Idris LExp -doForeign (_ : fgn : args) - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn - = let tys = getFTypes fgnArgTys - rty = mkIty' ret in - do args' <- mapM ir args - -- wrap it in a prim__IO - -- return $ con_ 0 @@ impossible @@ - return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args') - | otherwise = fail "Badly formed foreign function call" + doForeign :: [Name] -> [TT Name] -> Idris LExp + doForeign env (_ : fgn : args) + | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn + = let tys = getFTypes fgnArgTys + rty = mkIty' ret in + 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') + | otherwise = fail "Badly formed foreign function call" getFTypes :: TT Name -> [FType] getFTypes tm = case unApply tm of diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs --- a/src/IRTS/Defunctionalise.hs +++ b/src/IRTS/Defunctionalise.hs @@ -1,4 +1,5 @@ -module IRTS.Defunctionalise where +module IRTS.Defunctionalise(module IRTS.Defunctionalise, + module IRTS.Lang) where import IRTS.Lang import Core.TT @@ -7,7 +8,30 @@ import Data.Maybe import Data.List -defunctionalise :: Int -> LDefs -> LDefs +data DExp = DV LVar + | DApp Bool Name [DExp] -- True = tail call + | DLet Name DExp DExp -- name just for pretty printing + | DLam [Name] DExp -- lambda, lifted out before compiling + | DC Int Name [DExp] + | DCase DExp [DAlt] + | DConst Const + | DForeign FLang FType String [(FType, DExp)] + | DOp PrimFn [DExp] + | DError String + deriving Eq + +data DAlt = DConCase Int Name [Name] DExp + | DConstCase Const DExp + | DDefaultCase DExp + deriving (Show, Eq) + +data DDecl = DFun Name [Name] DExp -- name, arg names, definition + | DConstructor Name Int Int -- constructor name, tag, arity + deriving (Show, Eq) + +type DDefs = Ctxt DDecl + +defunctionalise :: Int -> LDefs -> DDefs defunctionalise nexttag defs = let all = toAlist defs -- sort newcons so that EVAL and APPLY cons get sequential tags @@ -36,56 +60,58 @@ -- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY -- 8 Add explicit EVAL to case, primitives, and foreign calls -addApps :: LDefs -> (Name, LDecl) -> (Name, LDecl) -addApps defs o@(n, LConstructor _ _ _) = o -addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e)) +addApps :: LDefs -> (Name, LDecl) -> (Name, DDecl) +addApps defs o@(n, LConstructor _ t a) = (n, DConstructor n t a) +addApps defs (n, LFun _ args e) = (n, DFun n args (aa args e)) where - aa env (LV (Glob n)) | n `elem` env = LV (Glob n) + aa :: [Name] -> LExp -> DExp + aa env (LV (Glob n)) | n `elem` env = DV (Glob n) | otherwise = aa env (LApp False (LV (Glob n)) []) -- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e aa env (LApp tc (LV (Glob n)) args) = let args' = map (aa env) args in case lookupCtxt Nothing n defs of - [LConstructor _ i ar] -> LApp tc (LV (Glob n)) args' + [LConstructor _ i ar] -> DApp tc n args' [LFun _ as _] -> let arity = length as in fixApply tc n args' arity - [] -> chainAPPLY (LV (Glob n)) args' + [] -> chainAPPLY (DV (Glob n)) args' aa env (LLazyApp n args) = let args' = map (aa env) args in case lookupCtxt Nothing n defs of - [LConstructor _ i ar] -> LApp False (LV (Glob n)) args' + [LConstructor _ i ar] -> DApp False n args' [LFun _ as _] -> let arity = length as in fixLazyApply n args' arity - [] -> chainAPPLY (LV (Glob n)) args' + [] -> chainAPPLY (DV (Glob n)) args' aa env (LForce e) = eEVAL (aa env e) - aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc) - aa env (LCon i n args) = LCon i n (map (aa env) args) - aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts) - aa env (LConst c) = LConst c - aa env (LForeign l t n args) = LForeign l t n (map (aaF env) args) - aa env (LOp f args) = LOp f (map (eEVAL . (aa env)) args) - aa env (LError e) = LError e + aa env (LLet n v sc) = DLet n (aa env v) (aa (n : env) sc) + aa env (LCon i n args) = DC i n (map (aa env) args) + aa env (LCase e alts) = DCase (eEVAL (aa env e)) (map (aaAlt env) alts) + aa env (LConst c) = DConst c + aa env (LForeign l t n args) = DForeign l t n (map (aaF env) args) + aa env (LOp LFork args) = DOp LFork (map (aa env) args) + aa env (LOp f args) = DOp f (map (eEVAL . (aa env)) args) + aa env (LError e) = DError e aaF env (t, e) = (t, eEVAL (aa env e)) - aaAlt env (LConCase i n args e) = LConCase i n args (aa (args ++ env) e) - aaAlt env (LConstCase c e) = LConstCase c (aa env e) - aaAlt env (LDefaultCase e) = LDefaultCase (aa env e) + aaAlt env (LConCase i n args e) = DConCase i n args (aa (args ++ env) e) + aaAlt env (LConstCase c e) = DConstCase c (aa env e) + aaAlt env (LDefaultCase e) = DDefaultCase (aa env e) fixApply tc n args ar - | length args == ar = LApp tc (LV (Glob n)) args - | length args < ar = LApp tc (LV (Glob (mkUnderCon n (ar - length args)))) args - | length args > ar = chainAPPLY (LApp tc (LV (Glob n)) (take ar args)) (drop ar args) + | length args == ar = DApp tc n args + | length args < ar = DApp tc (mkUnderCon n (ar - length args)) args + | length args > ar = chainAPPLY (DApp tc n (take ar args)) (drop ar args) fixLazyApply n args ar - | length args == ar = LApp False (LV (Glob (mkFnCon n))) args - | length args < ar = LApp False (LV (Glob (mkUnderCon n (ar - length args)))) args - | length args > ar = chainAPPLY (LApp False (LV (Glob n)) (take ar args)) (drop ar args) + | length args == ar = DApp False (mkFnCon n) args + | length args < ar = DApp False (mkUnderCon n (ar - length args)) args + | length args > ar = chainAPPLY (DApp False n (take ar args)) (drop ar args) chainAPPLY f [] = f - chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as + chainAPPLY f (a : as) = chainAPPLY (DApp False (MN 0 "APPLY") [f, a]) as -eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x] +eEVAL x = DApp False (MN 0 "EVAL") [x] data EvalApply a = EvalCase a | ApplyCase a @@ -94,44 +120,46 @@ -- For a function name, generate a list of -- data constuctors, and whether to handle them in EVAL or APPLY -toCons :: (Name, Int) -> [(Name, Int, EvalApply LAlt)] +toCons :: (Name, Int) -> [(Name, Int, EvalApply DAlt)] toCons (n, i) = (mkFnCon n, i, - EvalCase (LConCase (-1) (mkFnCon n) (take i (genArgs 0)) - (eEVAL (LApp False (LV (Glob n)) (map (LV . Glob) (take i (genArgs 0))))))) + EvalCase (DConCase (-1) (mkFnCon n) (take i (genArgs 0)) + (eEVAL (DApp False n (map (DV . Glob) (take i (genArgs 0))))))) : mkApplyCase n 0 i mkApplyCase fname n ar | n == ar = [] mkApplyCase fname n ar = let nm = mkUnderCon fname (ar - n) in - (nm, n, ApplyCase (LConCase (-1) nm (take n (genArgs 0)) - (LApp False (LV (Glob (mkUnderCon fname (ar - (n + 1))))) - (map (LV . Glob) (take n (genArgs 0) ++ + (nm, n, ApplyCase (DConCase (-1) nm (take n (genArgs 0)) + (DApp False (mkUnderCon fname (ar - (n + 1))) + (map (DV . Glob) (take n (genArgs 0) ++ [MN 0 "arg"]))))) : mkApplyCase fname (n + 1) ar -mkEval :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl) -mkEval xs = (MN 0 "EVAL", LFun (MN 0 "EVAL") [MN 0 "arg"] - (LCase (LV (Glob (MN 0 "arg"))) +mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl) +mkEval xs = (MN 0 "EVAL", DFun (MN 0 "EVAL") [MN 0 "arg"] + (mkBigCase (MN 0 "EVAL") 256 (DV (Glob (MN 0 "arg"))) (mapMaybe evalCase xs ++ - [LDefaultCase (LV (Glob (MN 0 "arg")))]))) + [DDefaultCase (DV (Glob (MN 0 "arg")))]))) where evalCase (n, t, EvalCase x) = Just x evalCase _ = Nothing -mkApply :: [(Name, Int, EvalApply LAlt)] -> (Name, LDecl) -mkApply xs = (MN 0 "APPLY", LFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"] - (LCase (LApp False (LV (Glob (MN 0 "EVAL"))) - [LV (Glob (MN 0 "fn"))]) +mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl) +mkApply xs = (MN 0 "APPLY", DFun (MN 0 "APPLY") [MN 0 "fn", MN 0 "arg"] + (mkBigCase (MN 0 "APPLY") + 256 (DApp False (MN 0 "EVAL") + [DV (Glob (MN 0 "fn"))]) (mapMaybe applyCase xs))) where applyCase (n, t, ApplyCase x) = Just x applyCase _ = Nothing -declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)] + +declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)] declare t xs = dec' t xs [] where dec' t [] acc = reverse acc - dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, LConstructor n t ar) : acc) + dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, DConstructor n t ar) : acc) genArgs i = MN i "P_c" : genArgs (i + 1) @@ -139,4 +167,70 @@ mkFnCon n = MN 0 ("P_" ++ show n) mkUnderCon n 0 = n mkUnderCon n missing = MN missing ("U_" ++ show n) + +instance Show DExp where + show e = show' [] e where + show' env (DV (Loc i)) = env!!i + show' env (DV (Glob n)) = show n + show' env (DApp _ e args) = show e ++ "(" ++ + showSep ", " (map (show' env) args) ++")" + show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++ + show' (env ++ [show n]) e + show' env (DLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " ++ + show' (env ++ (map show args)) e + show' env (DC i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")" + show' env (DCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++ + showSep "\n\t| " (map (showAlt env) alts) + show' env (DConst c) = show c + show' env (DForeign lang ty n args) + = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")" + show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")" + show' env (DError str) = "error " ++ show str + + showAlt env (DConCase _ n args e) + = show n ++ "(" ++ showSep ", " (map show args) ++ ") => " + ++ show' env e + showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e + showAlt env (DDefaultCase e) = "_ => " ++ show' env e + +-- Divide up a large case expression so that each has a maximum of +-- 'max' branches + +mkBigCase cn max arg branches + | length branches <= max = DCase arg branches + | otherwise = -- DCase arg branches -- until I think of something... + -- divide the branches into groups of at most max (by tag), + -- generate a new case and shrink, recursively + let bs = sortBy tagOrd branches + (all, def) = case (last bs) of + DDefaultCase t -> (init all, Just (DDefaultCase t)) + _ -> (all, Nothing) + bss = groupsOf max all + cs = map mkCase bss in + DCase arg branches + + where mkCase bs = DCase arg bs + + tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t' + tagOrd (DConstCase c _) (DConstCase c' _) = compare c c' + tagOrd (DDefaultCase _) (DDefaultCase _) = EQ + tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT + tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT + tagOrd (DConstCase _ _) (DDefaultCase _) = LT + tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT + tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT + tagOrd (DDefaultCase _) (DConstCase _ _) = GT + + +groupsOf :: Int -> [DAlt] -> [[DAlt]] +groupsOf x [] = [] +groupsOf x xs = let (batch, rest) = span (tagLT (x + tagHead xs)) xs in + batch : groupsOf x rest + where tagHead (DConstCase (I i) _ : _) = i + tagHead (DConCase t _ _ _ : _) = t + tagHead (DDefaultCase _ : _) = -1 -- must be the end + + tagLT i (DConstCase (I j) _) = i < j + tagLT i (DConCase j _ _ _) = i < j + tagLT i (DDefaultCase _) = False diff --git a/src/IRTS/Inliner.hs b/src/IRTS/Inliner.hs new file mode 100644 --- /dev/null +++ b/src/IRTS/Inliner.hs @@ -0,0 +1,9 @@ +module IRTS.Inliner where + +import Core.TT + +import IRTS.Defunctionalise + +inline :: DDefs -> DDefs +inline xs = xs + diff --git a/src/IRTS/LParser.hs b/src/IRTS/LParser.hs --- a/src/IRTS/LParser.hs +++ b/src/IRTS/LParser.hs @@ -54,7 +54,7 @@ let checked = checkDefs defuns (toAlist defuns) -- print checked case checked of - OK c -> codegenC c "a.out" True ["math.h"] "" "" TRACE + OK c -> codegenC Nothing c "a.out" True ["math.h"] "" "" TRACE Error e -> fail $ show e parseFOVM :: FilePath -> IO [(Name, LDecl)] diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs --- a/src/IRTS/Lang.hs +++ b/src/IRTS/Lang.hs @@ -36,7 +36,7 @@ | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev | LStdIn | LStdOut | LStdErr - | LNoOp + | LFork | LVMPtr | LNoOp deriving (Show, Eq) -- Supported target languages for foreign calls @@ -52,7 +52,7 @@ | LDefaultCase LExp deriving (Show, Eq) -data LDecl = LFun Name [Name] LExp -- name, arg names, definition +data LDecl = LFun Name [Name] LExp -- name, arg names, definition, inlinable | LConstructor Name Int Int -- constructor name, tag, arity deriving (Show, Eq) @@ -60,8 +60,10 @@ addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)]) addTags i ds = tag i ds [] - where tag i ((n, LConstructor n' t a) : as) acc + where tag i ((n, LConstructor n' (-1) a) : as) acc = tag (i + 1) as ((n, LConstructor n' i a) : acc) + tag i ((n, LConstructor n' t a) : as) acc + = tag i as ((n, LConstructor n' t a) : acc) tag i (x : as) acc = tag i as (x : acc) tag i [] acc = (i, reverse acc) diff --git a/src/IRTS/Simplified.hs b/src/IRTS/Simplified.hs --- a/src/IRTS/Simplified.hs +++ b/src/IRTS/Simplified.hs @@ -1,6 +1,6 @@ module IRTS.Simplified where -import IRTS.Lang +import IRTS.Defunctionalise import Core.TT import Data.Maybe import Control.Monad.State @@ -27,51 +27,50 @@ data SDecl = SFun Name [Name] Int SExp deriving Show -hvar :: State (LDefs, Int) Int +hvar :: State (DDefs, Int) Int hvar = do (l, h) <- get put (l, h + 1) return h -ldefs :: State (LDefs, Int) LDefs +ldefs :: State (DDefs, Int) DDefs ldefs = do (l, h) <- get return l -simplify :: Bool -> LExp -> State (LDefs, Int) SExp -simplify tl (LV (Loc i)) = return (SV (Loc i)) -simplify tl (LV (Glob x)) +simplify :: Bool -> DExp -> State (DDefs, Int) SExp +simplify tl (DV (Loc i)) = return (SV (Loc i)) +simplify tl (DV (Glob x)) = do ctxt <- ldefs case lookupCtxt Nothing x ctxt of - [LConstructor _ t 0] -> return $ SCon t x [] + [DConstructor _ t 0] -> return $ SCon t x [] _ -> return $ SV (Glob x) -simplify tl (LApp tc (LV (Glob n)) args) - = do args' <- mapM sVar args +simplify tl (DApp tc n args) = do args' <- mapM sVar args mkapp (SApp (tl || tc) n) args' -simplify tl (LForeign lang ty fn args) +simplify tl (DForeign lang ty fn args) = do args' <- mapM sVar (map snd args) let fargs = zip (map fst args) args' mkfapp (SForeign lang ty fn) fargs -simplify tl (LLet n v e) = do v' <- simplify False v +simplify tl (DLet n v e) = do v' <- simplify False v e' <- simplify tl e return (SLet (Glob n) v' e') -simplify tl (LCon i n args) = do args' <- mapM sVar args - mkapp (SCon i n) args' -simplify tl (LCase e alts) = do v <- sVar e +simplify tl (DC i n args) = do args' <- mapM sVar args + mkapp (SCon i n) args' +simplify tl (DCase e alts) = do v <- sVar e alts' <- mapM (sAlt tl) alts case v of (x, Nothing) -> return (SCase x alts') (Glob x, Just e) -> return (SLet (Glob x) e (SCase (Glob x) alts')) -simplify tl (LConst c) = return (SConst c) -simplify tl (LOp p args) = do args' <- mapM sVar args +simplify tl (DConst c) = return (SConst c) +simplify tl (DOp p args) = do args' <- mapM sVar args mkapp (SOp p) args' -simplify tl (LError str) = return $ SError str +simplify tl (DError str) = return $ SError str -sVar (LV (Glob x)) +sVar (DV (Glob x)) = do ctxt <- ldefs case lookupCtxt Nothing x ctxt of - [LConstructor _ t 0] -> sVar (LCon t x []) + [DConstructor _ t 0] -> sVar (DC t x []) _ -> return (Glob x, Nothing) -sVar (LV x) = return (x, Nothing) +sVar (DV x) = return (x, Nothing) sVar e = do e' <- simplify False e i <- hvar return (Glob (MN i "R"), Just e') @@ -90,19 +89,19 @@ = do sc <- mkapp' f xs ((ty, x) : args) return (SLet x e sc) -sAlt tl (LConCase i n args e) = do e' <- simplify tl e +sAlt tl (DConCase i n args e) = do e' <- simplify tl e return (SConCase (-1) i n args e') -sAlt tl (LConstCase c e) = do e' <- simplify tl e +sAlt tl (DConstCase c e) = do e' <- simplify tl e return (SConstCase c e') -sAlt tl (LDefaultCase e) = do e' <- simplify tl e +sAlt tl (DDefaultCase e) = do e' <- simplify tl e return (SDefaultCase e') -checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, SDecl)] +checkDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)] checkDefs ctxt [] = return [] -checkDefs ctxt (con@(n, LConstructor _ _ _) : xs) +checkDefs ctxt (con@(n, DConstructor _ _ _) : xs) = do xs' <- checkDefs ctxt xs return xs' -checkDefs ctxt ((n, LFun n' args exp) : xs) +checkDefs ctxt ((n, DFun n' args exp) : xs) = do let sexp = evalState (simplify True exp) (ctxt, 0) (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args) xs' <- checkDefs ctxt xs @@ -111,13 +110,13 @@ lvar v = do i <- get put (max i v) -scopecheck :: LDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp +scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp scopecheck ctxt env tm = sc env tm where sc env (SV (Glob n)) = case lookup n (reverse env) of -- most recent first Just i -> do lvar i; return (SV (Loc i)) Nothing -> case lookupCtxt Nothing n ctxt of - [LConstructor _ i ar] -> + [DConstructor _ i ar] -> if True -- ar == 0 then return (SCon i n []) else fail $ "Codegen error: Constructor " ++ show n ++ @@ -127,7 +126,7 @@ sc env (SApp tc f args) = do args' <- mapM (scVar env) args case lookupCtxt Nothing f ctxt of - [LConstructor n tag ar] -> + [DConstructor n tag ar] -> if True -- (ar == length args) then return $ SCon tag n args' else fail $ "Codegen error: Constructor " ++ show f ++ @@ -141,7 +140,7 @@ sc env (SCon tag f args) = do args' <- mapM (scVar env) args case lookupCtxt Nothing f ctxt of - [LConstructor n tag ar] -> + [DConstructor n tag ar] -> if True -- (ar == length args) then return $ SCon tag n args' else fail $ "Codegen error: Constructor " ++ show f ++ @@ -166,7 +165,7 @@ case lookup n (reverse env) of -- most recent first Just i -> do lvar i; return (Loc i) Nothing -> case lookupCtxt Nothing n ctxt of - [LConstructor _ i ar] -> + [DConstructor _ i ar] -> fail $ "Codegen error : can't pass constructor here" [_] -> return (Glob n) [] -> fail $ "Codegen error: No such variable " ++ show n @@ -175,7 +174,7 @@ scalt env (SConCase _ i n args e) = do let env' = env ++ zip args [length env..] tag <- case lookupCtxt Nothing n ctxt of - [LConstructor _ i ar] -> + [DConstructor _ i ar] -> if True -- (length args == ar) then return i else fail $ "Codegen error: Constructor " ++ show n ++ diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -194,6 +194,18 @@ let opt' = opts { opt_logLevel = l } put (i { idris_options = opt' } ) +setCmdLine :: [Opt] -> Idris () +setCmdLine opts = do i <- get + let iopts = idris_options i + put (i { idris_options = iopts { opt_cmdline = opts } }) + +getDumpC :: Idris (Maybe FilePath) +getDumpC = do i <- get + return $ findC (opt_cmdline (idris_options i)) + where findC [] = Nothing + findC (DumpC x : _) = Just x + findC (_ : xs) = findC xs + logLevel :: Idris Int logLevel = do i <- get return (opt_logLevel (idris_options i)) @@ -257,6 +269,12 @@ valIBCSubDir :: IState -> Idris FilePath valIBCSubDir i = return (opt_ibcsubdir (idris_options i)) +addImportDir :: FilePath -> Idris () +addImportDir fp = do i <- get + let opts = idris_options i + let opt' = opts { opt_importdirs = fp : opt_importdirs opts } + put (i { idris_options = opt' }) + setImportDirs :: [FilePath] -> Idris () setImportDirs fps = do i <- get let opts = idris_options i @@ -264,9 +282,8 @@ put (i { idris_options = opt' }) allImportDirs :: IState -> Idris [FilePath] -allImportDirs i = do datadir <- liftIO $ getDataDir - let optdirs = opt_importdirs (idris_options i) - return ("." : (optdirs ++ [datadir])) +allImportDirs i = do let optdirs = opt_importdirs (idris_options i) + return ("." : optdirs) impShow :: Idris Bool impShow = do i <- get @@ -521,9 +538,12 @@ -- This has become a right mess already. Better redo it some time... implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm -implicit syn n ptm +implicit syn n ptm = implicit' syn [] n ptm + +implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm +implicit' syn ignore n ptm = do i <- get - let (tm', impdata) = implicitise syn i ptm + let (tm', impdata) = implicitise syn ignore i ptm -- let (tm'', spos) = findStatics i tm' put (i { idris_implicits = addDef n impdata (idris_implicits i) }) addIBC (IBCImp n) @@ -532,13 +552,13 @@ -- put (i { idris_statics = addDef n spos (idris_statics i) }) return tm' -implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg]) -implicitise syn ist tm +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) in + ns = ns' \\ (map fst pvars ++ no_imp syn ++ ignore) in if null ns then (tm, reverse declimps) - else implicitise syn ist (pibind uvars ns tm) + else implicitise syn ignore ist (pibind uvars ns tm) where uvars = using syn pvars = syn_params syn diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -31,11 +31,12 @@ opt_repl :: Bool, opt_verbose :: Bool, opt_ibcsubdir :: FilePath, - opt_importdirs :: [FilePath] + opt_importdirs :: [FilePath], + opt_cmdline :: [Opt] -- remember whole command line } deriving (Show, Eq) -defaultOpts = IOption 0 False False True False False True True "" [] +defaultOpts = IOption 0 False False True False False True True "" [] [] -- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e -- without typechecking). @@ -114,6 +115,8 @@ -- Commands in the REPL +data Target = ViaC | ViaJava + data Command = Quit | Help | Eval PTerm @@ -121,7 +124,7 @@ | TotCheck Name | Reload | Edit - | Compile String + | Compile Target String | Execute | ExecVal PTerm | NewCompile String @@ -148,6 +151,7 @@ | Ver | Usage | ShowLibs + | ShowLibdir | ShowIncs | NoPrelude | NoREPL @@ -162,9 +166,15 @@ | Verbose | IBCSubDir String | ImportDir String + | PkgBuild String + | PkgInstall String + | PkgClean String + | WarnOnly + | Pkg String | BCAsm String + | DumpC String | FOVM String - deriving Eq + deriving (Show, Eq) -- Parsed declarations @@ -237,6 +247,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration | PTy SyntaxInfo FC FnOpts Name t -- type declaration | PClauses FC FnOpts Name [PClause' t] -- pattern clause + | PCAF FC Name t -- top level constant | PData SyntaxInfo FC (PData' t) -- data declaration | PParams FC [(Name, t)] [PDecl' t] -- params block | PNamespace String [PDecl' t] -- new namespace diff --git a/src/Idris/Compiler.hs b/src/Idris/Compiler.hs --- a/src/Idris/Compiler.hs +++ b/src/Idris/Compiler.hs @@ -24,8 +24,8 @@ import qualified Epic.Epic as E -} -compile :: FilePath -> Term -> Idris () -compile f t = fail "Epic backend disabled" +compileEpic :: FilePath -> Term -> Idris () +compileEpic f t = fail "Epic backend disabled" {- compile f tm diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -75,7 +75,7 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++ "\nThis is probably a bug, or a missing error message.\n" ++ "Please consider reporting at " ++ bugaddr -pshow i (CantUnify x y e sc s) +pshow i (CantUnify _ x y e sc s) = "Can't unify " ++ show (delab i x) ++ " with " ++ show (delab i y) ++ -- " (" ++ show x ++ " and " ++ show y ++ ") " ++ @@ -94,6 +94,7 @@ show (delab i y) pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c) pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as +pshow i (NoTypeDecl n) = "No type declaration for " ++ show n pshow i (NoSuchVariable n) = "No such variable " ++ show n pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t) pshow i UniverseError = "Universe inconsistency" diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -221,7 +221,16 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris () elabClauses info fc opts n_in cs = let n = liftname info n_in in - do pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs + do ctxt <- getContext + -- Check n actually exists + case lookupTy Nothing n ctxt of + [] -> -- TODO: turn into a CAF if there's no arguments + -- question: CAFs in where blocks? + tclift $ tfail $ (At fc (NoTypeDecl n)) + _ -> return () + pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs + + solveDeferred n let pats = mapMaybe id pats_in logLvl 3 (showSep "\n" (map (\ (l,r) -> @@ -545,15 +554,20 @@ let constraint = PApp fc (PRef fc tn) (map (pexp . PRef fc) (map fst ps)) -- build data declaration - ims <- mapM tdecl (filter tydecl ds) + let mdecls = filter tydecl ds -- method declarations + let mnames = map getMName mdecls + logLvl 2 $ "Building methods " ++ show mnames + ims <- mapM (tdecl mnames) mdecls defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint) (filter clause ds) let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims) let cty = impbind ps $ conbind constraints $ pibind methods constraint let cons = [(cn, cty, fc)] - let ddecl = PData syn fc (PDatadecl tn tty cons) - elabDecl info ddecl + let ddecl = PDatadecl tn tty cons + logLvl 5 $ "Class data " ++ showDImp True ddecl + elabData info (syn { no_imp = no_imp syn ++ mnames }) fc ddecl -- for each constraint, build a top level function to chase it + 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) @@ -574,11 +588,14 @@ conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x) conbind [] x = x - tdecl (PTy syn _ o n t) = do t' <- implicit syn n t - return ( (n, (toExp (map fst ps) Exp t')), - (n, (o, (toExp (map fst ps) Imp t'))), - (n, (syn, o, t) ) ) - tdecl _ = fail "Not allowed in a class declaration" + getMName (PTy _ _ _ n _) = nsroot n + tdecl allmeths (PTy syn _ o n t) + = do t' <- implicit' syn allmeths n t + logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t' + return ( (n, (toExp (map fst ps) Exp t')), + (n, (o, (toExp (map fst ps) Imp t'))), + (n, (syn, o, t) ) ) + tdecl _ _ = fail "Not allowed in a class declaration" -- Create default definitions defdecl mtys c d@(PClauses fc opts n cs) = diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -235,7 +235,7 @@ ctxt <- get_context let guarded = isConName Nothing f ctxt -- when True - try + tryWhen True (do ns <- apply (Var f) (map isph args) let (ns', eargs) = unzip $ diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -857,6 +857,10 @@ PDSL x1 x2 -> do putWord8 9 put x1 put x2 + PCAF x1 x2 x3 -> do putWord8 10 + put x1 + put x2 + put x3 get = do i <- getWord8 case i of @@ -912,6 +916,10 @@ 9 -> do x1 <- get x2 <- get return (PDSL x1 x2) + 10 -> do x1 <- get + x2 <- get + x3 <- get + return (PCAF x1 x2 x3) _ -> error "Corrupted binary data for PDecl'" instance Binary SyntaxInfo where diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -17,11 +17,12 @@ import Core.TT import Core.Evaluate -import Text.ParserCombinators.Parsec -import Text.ParserCombinators.Parsec.Error -import Text.ParserCombinators.Parsec.Expr -import Text.ParserCombinators.Parsec.Language -import qualified Text.ParserCombinators.Parsec.Token as PTok +import Text.Parsec +import Text.Parsec.Error +import Text.Parsec.Expr +import Text.Parsec.Language +import Text.Parsec.String +import qualified Text.Parsec.Token as PTok import Data.List import Control.Monad.State @@ -36,22 +37,22 @@ lexer :: TokenParser IState lexer = PTok.makeTokenParser idrisDef -whiteSpace= PTok.whiteSpace lexer -lexeme = PTok.lexeme lexer -symbol = PTok.symbol lexer -natural = PTok.natural lexer -parens = PTok.parens lexer -semi = PTok.semi lexer -comma = PTok.comma lexer -identifier= PTok.identifier lexer -reserved = PTok.reserved lexer -operator = PTok.operator lexer -reservedOp= PTok.reservedOp lexer -integer = PTok.integer lexer -float = PTok.float lexer -strlit = PTok.stringLiteral lexer -chlit = PTok.charLiteral lexer -lchar = lexeme.char +whiteSpace = PTok.whiteSpace lexer +lexeme = PTok.lexeme lexer +symbol = PTok.symbol lexer +natural = PTok.natural lexer +parens = PTok.parens lexer +semi = PTok.semi lexer +comma = PTok.comma lexer +identifier = PTok.identifier lexer +reserved = PTok.reserved lexer +operator = PTok.operator lexer +reservedOp = PTok.reservedOp lexer +integer = PTok.integer lexer +float = PTok.float lexer +strlit = PTok.stringLiteral lexer +chlit = PTok.charLiteral lexer +lchar = lexeme.char -- Loading modules @@ -61,7 +62,7 @@ ibcsd <- valIBCSubDir i ids <- allImportDirs i fp <- liftIO $ findImport ids ibcsd f - if (f `elem` imported i) + if f `elem` imported i then iLOG $ "Already read " ++ f else do putIState (i { imported = f : imported i }) case fp of @@ -90,7 +91,7 @@ putIState (i { default_access = Hidden }) mapM_ loadModule modules clearIBC -- start a new .ibc file - mapM_ (\m -> addIBC (IBCImport m)) modules + mapM_ (addIBC . IBCImport) modules ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) f rest pos let ds = namespaces mname ds' @@ -107,6 +108,7 @@ iLOG ("Finished " ++ f) ibcsd <- valIBCSubDir i let ibc = ibcPathNoFallback ibcsd f + iLOG "Universe checking" iucheck i <- getIState addHides (hide_list i) @@ -125,10 +127,10 @@ addHides xs = do i <- getIState let defh = default_access i let (hs, as) = partition isNothing xs - if null as then return () - else mapM_ doHide - (map (\ (n, _) -> (n, defh)) hs ++ - map (\ (n, Just a) -> (n, a)) as) + unless (null as) $ + mapM_ doHide + (map (\ (n, _) -> (n, defh)) hs ++ + map (\ (n, Just a) -> (n, a)) as) where isNothing (_, Nothing) = True isNothing _ = False @@ -140,123 +142,121 @@ eof return t) i "(proof)" +iShowError fname err = let ln = sourceLine (errorPos err) + clm = sourceColumn (errorPos err) + msg = map messageString (errorMessages err) in + fname ++ ":" ++ show ln ++ ":parse error" + ++ " at column " ++ show clm -- ++ " with error:\n\t" ++ show msg + parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos) parseImports fname input = do i <- get - case (runParser (do whiteSpace - mname <- pHeader - ps <- many pImport - rest <- getInput - pos <- getPosition - return ((mname, ps, rest, pos), i)) i fname input) of - Left err -> fail (show err) - Right (x, i) -> do put i - return x - where ishow err = let ln = sourceLine (errorPos err) in - fname ++ ":" ++ show ln ++ ":parse error" --- ++ show (map messageString (errorMessages err)) + case runParser (do whiteSpace + mname <- pHeader + ps <- many pImport + rest <- getInput + pos <- getPosition + return ((mname, ps, rest, pos), i)) i fname input of + Left err -> fail (iShowError fname err) + Right (x, i) -> do put i + return x pHeader :: IParser [String] pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';') return (parseName i)) <|> return [] where parseName x = case span (/='.') x of - (x, "") -> [x] - (x, '.':y) -> x : parseName y + (x, "") -> [x] + (x, '.':y) -> x : parseName y -push_indent :: IParser () -push_indent = do pos <- getPosition - ist <- getState - setState (ist { indent_stack = sourceColumn pos : +pushIndent :: IParser () +pushIndent = do pos <- getPosition + ist <- getState + setState (ist { indent_stack = sourceColumn pos : indent_stack ist }) -last_indent :: IParser Int -last_indent = do ist <- getState - case indent_stack ist of - (x : xs) -> return x - _ -> return 1 +lastIndent :: IParser Int +lastIndent = do ist <- getState + case indent_stack ist of + (x : xs) -> return x + _ -> return 1 indent :: IParser Int -indent = do pos <- getPosition - return (sourceColumn pos) +indent = liftM sourceColumn getPosition -pop_indent :: IParser () -pop_indent = do ist <- getState - let (x : xs) = indent_stack ist - setState (ist { indent_stack = xs }) +popIndent :: IParser () +popIndent = do ist <- getState + let (x : xs) = indent_stack ist + setState (ist { indent_stack = xs }) -open_block :: IParser () -open_block = do lchar '{' - ist <- getState - setState (ist { brace_stack = Nothing : brace_stack ist }) +openBlock :: IParser () +openBlock = do lchar '{' + ist <- getState + setState (ist { brace_stack = Nothing : brace_stack ist }) <|> do ist <- getState lvl <- indent setState (ist { brace_stack = Just lvl : brace_stack ist }) -close_block :: IParser () -close_block = do ist <- getState - bs <- case brace_stack ist of - Nothing : xs -> do lchar '}' - return xs - Just lvl : xs -> do i <- indent - inp <- getInput +closeBlock :: IParser () +closeBlock = do ist <- getState + bs <- case brace_stack ist of + Nothing : xs -> do lchar '}' + return xs + Just lvl : xs -> do i <- indent + inp <- getInput -- trace (show (take 10 inp, i, lvl)) $ - if (i >= lvl && take 1 inp /= ")") - then fail "Not end of block" - else return xs - setState (ist { brace_stack = bs }) + if i >= lvl && take 1 inp /= ")" + then fail "Not end of block" + else return xs + setState (ist { brace_stack = bs }) -pTerminator = do lchar ';'; pop_indent - <|> do c <- indent; l <- last_indent - if (c <= l) then pop_indent - else fail "Not a terminator" - <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent - else fail "Not a terminator" +pTerminator = do lchar ';'; popIndent + <|> do c <- indent; l <- lastIndent + if c <= l + then popIndent + else fail "Not a terminator" + <|> do i <- getInput + if "}" `isPrefixOf` i || ")" `isPrefixOf` i + then popIndent + else fail "Not a terminator" <|> lookAhead eof pBarTerminator = do lchar '|'; return () - <|> do c <- indent; l <- last_indent - if (c <= l) then return () - else fail "Not a terminator" + <|> do c <- indent; l <- lastIndent + unless (c <= l) $ fail "Not a terminator" <|> lookAhead eof pKeepTerminator = do lchar ';'; return () - <|> do c <- indent; l <- last_indent - if (c <= l) then return () - else fail "Not a terminator" - <|> do i <- getInput; let h = take 1 i - if (h == "}" || h == ")" || h == "|") then return () - else fail "Not a terminator" + <|> do c <- indent; l <- lastIndent + unless (c <= l) $ fail "Not a terminator" + <|> do i <- getInput + let h = take 1 i + unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator" <|> lookAhead eof -notEndApp = do c <- indent; l <- last_indent +notEndApp = do c <- indent; l <- lastIndent i <- getInput - if (c <= l) then fail "Terminator" - else return () + when (c <= l) $ fail "Terminator" notEndBlock = do ist <- getState case brace_stack ist of - Just lvl : xs -> do i <- indent + Just lvl : xs -> do i <- indent inp <- getInput - if (i < lvl || take 1 inp == ")") - then fail "End of block" - else return () - _ -> return () + when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block" + _ -> return () pfc :: IParser FC pfc = do s <- getPosition let (dir, file) = splitFileName (sourceName s) let f = case dir of - "./" -> file - _ -> sourceName s + "./" -> file + _ -> sourceName s return $ FC f (sourceLine s) pImport :: IParser String -pImport = do reserved "import" - f <- identifier - option ';' (lchar ';') +pImport = do reserved "import"; f <- identifier; option ';' (lchar ';') return (map dot f) where dot '.' = '/' dot c = c @@ -264,19 +264,15 @@ parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl] parseProg syn fname input pos = do i <- get - case (runParser (do setPosition pos - whiteSpace - ps <- many (pDecl syn) - eof - i' <- getState - return (concat ps, i')) i fname input) of - Left err -> fail (ishow err) + case runParser (do setPosition pos + whiteSpace + ps <- many (pDecl syn) + eof + i' <- getState + return (concat ps, i')) i fname input of + Left err -> fail (iShowError fname err) Right (x, i) -> do put i return (collect x) - where ishow err = let ln = sourceLine (errorPos err) in - fname ++ ":" ++ show ln ++ ":parse error" - ++ " at column " ++ show (sourceColumn (errorPos err)) --- show (map messageString (errorMessages err)) -- Collect PClauses with the same function name @@ -322,8 +318,7 @@ <|> pInstance syn <|> do d <- pDSL syn; return [d] <|> pDirective - <|> try (do reserved "import" - fp <- identifier + <|> try (do reserved "import"; fp <- identifier fail "imports must be at the top of file") pFunDecl :: SyntaxInfo -> IParser [PDecl] @@ -365,7 +360,7 @@ pSyntaxRule :: SyntaxInfo -> IParser Syntax pSyntaxRule syn - = do push_indent + = do pushIndent sty <- option AnySyntax (do reserved "term"; return TermSyntax <|> do reserved "pattern"; return PatternSyntax) reserved "syntax" @@ -405,7 +400,7 @@ return (Symbol sym) pFunDecl' :: SyntaxInfo -> IParser PDecl -pFunDecl' syn = try (do push_indent +pFunDecl' syn = try (do pushIndent opts <- pFnOpts acc <- pAccessibility opts' <- pFnOpts @@ -418,25 +413,20 @@ addAcc n acc return (PTy syn fc (opts ++ opts') n ty)) <|> try (pPattern syn) + <|> try (pCAF syn) pUsing :: SyntaxInfo -> IParser [PDecl] pUsing syn = - do reserved "using"; - lchar '(' - ns <- tyDeclList syn - lchar ')' - open_block + do reserved "using"; lchar '('; ns <- tyDeclList syn; lchar ')' + openBlock let uvars = using syn ds <- many1 (pDecl (syn { using = uvars ++ ns })) - close_block + closeBlock return (concat ds) pParams :: SyntaxInfo -> IParser [PDecl] pParams syn = - do reserved "params"; - lchar '(' - ns <- tyDeclList syn - lchar ')' + do reserved "params"; lchar '('; ns <- tyDeclList syn; lchar ')' lchar '{' let pvars = syn_params syn ds <- many1 (pDecl syn { syn_params = pvars ++ ns }) @@ -446,17 +436,16 @@ pNamespace :: SyntaxInfo -> IParser [PDecl] pNamespace syn = - do reserved "namespace"; - n <- identifier - open_block + do reserved "namespace"; n <- identifier; + openBlock ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn }) - close_block + closeBlock return [PNamespace n (concat ds)] --------- Fixity --------- pFixity :: IParser PDecl -pFixity = do push_indent +pFixity = do pushIndent f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',') pTerminator let prec = fromInteger i @@ -478,14 +467,12 @@ pClass :: SyntaxInfo -> IParser [PDecl] pClass syn = do acc <- pAccessibility - reserved "class" - fc <- pfc - cons <- pConstList syn - n_in <- pName; let n = expandNS syn n_in + reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName + let n = expandNS syn n_in cs <- many1 carg - reserved "where"; open_block + reserved "where"; openBlock ds <- many $ pFunDecl syn - close_block + closeBlock let allDs = concat ds accData acc n (concatMap declared allDs) return [PClass syn fc cons n cs allDs] @@ -496,8 +483,7 @@ return (i, PSet) pInstance :: SyntaxInfo -> IParser [PDecl] -pInstance syn = do reserved "instance" - fc <- pfc +pInstance syn = do reserved "instance"; fc <- pfc en <- option Nothing (do lchar '['; n_in <- pfName; lchar ']' let n = expandNS syn n_in @@ -507,9 +493,9 @@ args <- many1 (pSimpleExpr syn) let sc = PApp fc (PRef fc cn) (map pexp args) let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc - reserved "where"; open_block + reserved "where"; openBlock ds <- many $ pFunDecl syn - close_block + closeBlock return [PInstance syn fc cs cn args t en (concat ds)] --------- Expressions --------- @@ -534,7 +520,7 @@ simple (Rule (SimpleExpr x:xs) _ _) = False simple (Rule [Keyword _] _ _) = True simple (Rule [Symbol _] _ _) = True - simple (Rule (_:xs) _ _) = case (last xs) of + simple (Rule (_:xs) _ _) = case last xs of Keyword _ -> True Symbol _ -> True _ -> False @@ -551,7 +537,7 @@ <|> pComprehension syn pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm -pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules)) +pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules)) where valid (Rule _ _ AnySyntax) = True valid (Rule _ _ PatternSyntax) = inPattern syn @@ -648,41 +634,56 @@ addAcc n a = do i <- getState setState (i { hide_list = (n, a) : hide_list i }) +pCaseExpr syn = do + reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of"; + openBlock + pushIndent + opts <- many1 (do notEndBlock + x <- pCaseOpt syn + pKeepTerminator + return x) -- sepBy1 (pCaseOpt syn) (lchar '|') + popIndent + closeBlock + return (PCase fc scr opts) + +pProofExpr syn = do + reserved "proof"; lchar '{' + ts <- endBy (pTactic syn) (lchar ';') + lchar '}' + return (PProof ts) + +pTacticsExpr syn = do + reserved "tactics"; lchar '{' + ts <- endBy (pTactic syn) (lchar ';') + lchar '}' + return (PTactics ts) + pSimpleExpr syn = - try (do symbol "!["; t <- pTerm; lchar ']' - return $ PQuote t) + try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t) <|> do lchar '?'; x <- pName; return (PMetavar x) <|> do reserved "refl"; fc <- pfc; return (PRefl fc) -- <|> do reserved "return"; fc <- pfc; return (PReturn fc) - <|> do reserved "proof"; lchar '{'; - ts <- endBy (pTactic syn) (lchar ';') - lchar '}' - return (PProof ts) - <|> do reserved "tactics"; lchar '{'; - ts <- endBy (pTactic syn) (lchar ';') - lchar '}' - return (PTactics ts) - <|> do reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of"; - open_block - push_indent - opts <- many1 (do notEndBlock - x <- pCaseOpt syn - pKeepTerminator - return x) -- sepBy1 (pCaseOpt syn) (lchar '|') - pop_indent - close_block - return (PCase fc scr opts) - <|> try (do x <- pfName; fc <- pfc; return (PRef fc x)) + <|> pProofExpr syn + <|> pTacticsExpr syn + <|> pCaseExpr syn + <|> try (do x <- pfName + fc <- pfc + return (PRef fc x)) <|> try (pList syn) <|> try (pAlt syn) <|> try (pIdiom syn) - <|> try (do lchar '('; bracketed (noImp syn)) - <|> try (do c <- pConstant; fc <- pfc + <|> try (do lchar '(' + bracketed (noImp syn)) + <|> try (do c <- pConstant + fc <- pfc return (modifyConst syn fc (PConstant c))) <|> do reserved "Set"; return PSet --- <|> do symbol "*"; return PSet - <|> try (do symbol "()"; fc <- pfc; return (PTrue fc)) - <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc)) + <|> try (do symbol "()" + fc <- pfc + return (PTrue fc)) + <|> try (do symbol "_|_" + fc <- pfc + return (PFalse fc)) <|> do lchar '_'; return Placeholder <|> pSimpleExtExpr syn @@ -702,8 +703,7 @@ pexp (PRef fc (MN 0 "x"))])) pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm) -pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; - rhs <- pExpr syn +pCaseOpt syn = do lhs <- pExpr syn; symbol "=>"; rhs <- pExpr syn return (lhs, rhs) modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm @@ -713,8 +713,7 @@ | otherwise = PConstant (I x) modifyConst syn fc x = x -pList syn = do lchar '['; fc <- pfc - xs <- sepBy (pExpr syn) (lchar ','); lchar ']' +pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']' return (mkList fc xs) where mkList fc [] = PRef fc (UN "Nil") @@ -730,10 +729,12 @@ <|> try (do x <- ntuple lchar ')' return x) - <|> do ln <- pName; lchar ':'; lty <- pExpr syn; - reservedOp "**"; + <|> do ln <- pName; lchar ':' + lty <- pExpr syn + reservedOp "**" fc <- pfc - r <- pExpr syn; lchar ')'; + r <- pExpr syn + lchar ')' return (PDPair fc (PRef fc ln) lty r) where restTuple = do lchar ')'; return [] @@ -752,9 +753,7 @@ r <- pExpr syn return (PPair fc l r)) -pAlt syn = do symbol "(|"; - alts <- sepBy1 (pExpr' syn) (lchar ',') - symbol "|)" +pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)" return (PAlternative False alts) pHSimpleExpr syn @@ -781,13 +780,17 @@ <|> do e <- pSimpleExpr syn return (pexp e) -pImplicitArg syn = do lchar '{'; n <- pName +pImplicitArg syn = do lchar '{' + n <- pName fc <- pfc - v <- option (PRef fc n) (do lchar '='; pExpr syn) + v <- option (PRef fc n) (do lchar '=' + pExpr syn) lchar '}' return (pimp n v) -pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}" +pConstraintArg syn = do symbol "@{" + e <- pExpr syn + symbol "}" return (pconst e) pRecordSet syn @@ -796,13 +799,15 @@ fields <- sepBy1 pFieldSet (lchar ',') lchar '}' fc <- pfc - rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e)) + rec <- option Nothing (do e <- pSimpleExpr syn + return (Just e)) case rec of Nothing -> return (PLam (MN 0 "fldx") Placeholder (applyAll fc fields (PRef fc (MN 0 "fldx")))) Just v -> return (applyAll fc fields v) - where pFieldSet = do n <- pfName; lchar '=' + where pFieldSet = do n <- pfName + lchar '=' e <- pExpr syn return (n, e) applyAll fc [] x = x @@ -822,10 +827,10 @@ return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc) pLambda syn = do lchar '\\' - (try (do xt <- tyOptDeclList syn - symbol "=>" - sc <- pExpr syn - return (bindList PLam xt sc)) + try (do xt <- tyOptDeclList syn + symbol "=>" + sc <- pExpr syn + return (bindList PLam xt sc) <|> (do ps <- sepBy (do fc <- pfc e <- pSimpleExpr syn return (fc, e)) (lchar ',') @@ -836,14 +841,15 @@ pmList ((i, (fc, x)) : xs) sc = PLam (MN i "lamp") Placeholder (PCase fc (PRef fc (MN i "lamp")) - [(x, (pmList xs sc))]) + [(x, pmList xs sc)]) pLet syn = try (do reserved "let"; n <- pName; ty <- option Placeholder (do lchar ':'; pExpr' syn) - lchar '='; v <- pExpr syn + lchar '=' + v <- pExpr syn reserved "in"; sc <- pExpr syn return (PLet n ty v sc)) - <|> (do reserved "let"; fc <- pfc; pat <- pExpr' syn + <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } ) symbol "="; v <- pExpr syn reserved "in"; sc <- pExpr syn return (PCase fc v [(pat, sc)])) @@ -855,27 +861,36 @@ symbol "->" sc <- pExpr syn return (bindList (PPi (Exp lazy st)) xt sc)) - <|> try (if implicitAllowed syn then - do lazy <- option False (do lchar '|'; return True) - st <- pStatic - lchar '{'; xt <- tyDeclList syn; lchar '}' - symbol "->" - sc <- pExpr syn - return (bindList (PPi (Imp lazy st)) xt sc) + <|> try (if implicitAllowed syn + then do lazy <- option False (do lchar '|' + return True) + st <- pStatic + lchar '{' + xt <- tyDeclList syn + lchar '}' + symbol "->" + sc <- pExpr syn + return (bindList (PPi (Imp lazy st)) xt sc) else fail "No implicit arguments allowed here") - <|> try (do lchar '{'; reserved "auto" - xt <- tyDeclList syn; lchar '}' + <|> try (do lchar '{' + reserved "auto" + xt <- tyDeclList syn + lchar '}' symbol "->" sc <- pExpr syn return (bindList (PPi (TacImp False Dynamic (PTactics [Trivial]))) xt sc)) - <|> try (do lchar '{'; reserved "default" + <|> try (do lchar '{' + reserved "default" script <- pSimpleExpr syn - xt <- tyDeclList syn; lchar '}' + xt <- tyDeclList syn + lchar '}' symbol "->" sc <- pExpr syn return (bindList (PPi (TacImp False Dynamic script)) xt sc)) <|> do --lazy <- option False (do lchar '|'; return True) - lchar '{'; reserved "static"; lchar '}' + lchar '{' + reserved "static" + lchar '}' t <- pExpr' syn symbol "->" sc <- pExpr syn @@ -892,7 +907,9 @@ return [t]) <|> return [] -tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig (noImp syn); return (x,t)) +tyDeclList syn = try (sepBy1 (do x <- pfName + t <- pTSig (noImp syn) + return (x,t)) (lchar ',')) <|> do ns <- sepBy1 pName (lchar ',') t <- pTSig (noImp syn) @@ -908,8 +925,12 @@ bindList b ((n, t):bs) sc = b n t (bindList b bs sc) pComprehension syn - = do lchar '['; fc <- pfc; pat <- pExpr syn; lchar '|'; - qs <- sepBy1 (pDo syn) (lchar ','); lchar ']'; + = do lchar '[' + fc <- pfc + pat <- pExpr syn + lchar '|' + qs <- sepBy1 (pDo syn) (lchar ',') + lchar ']' return (PDoBlock (map addGuard qs ++ [DoExp fc (PApp fc (PRef fc (UN "return")) [pexp pat])])) @@ -918,34 +939,51 @@ addGuard x = x pDoBlock syn - = do reserved "do"; open_block - push_indent + = do reserved "do" + openBlock + pushIndent ds <- many1 (do notEndBlock - x <- pDo syn; pKeepTerminator; return x) - pop_indent - close_block + x <- pDo syn + pKeepTerminator + return x) + popIndent + closeBlock return (PDoBlock ds) pDo syn - = try (do reserved "let"; i <- pName; - ty <- option Placeholder (do lchar ':'; pExpr' syn) - reservedOp "="; fc <- pfc + = try (do reserved "let" + i <- pName; + ty <- option Placeholder (do lchar ':' + pExpr' syn) + reservedOp "=" + fc <- pfc e <- pExpr syn return (DoLet fc i ty e)) - <|> try (do reserved "let"; i <- pExpr' syn; reservedOp "="; fc <- pfc + <|> try (do reserved "let" + i <- pExpr' syn + reservedOp "=" + fc <- pfc sc <- pExpr syn return (DoLetP fc i sc)) - <|> try (do i <- pName; symbol "<-"; fc <- pfc + <|> try (do i <- pName + symbol "<-" + fc <- pfc e <- pExpr syn; return (DoBind fc i e)) - <|> try (do i <- pExpr' syn; symbol "<-"; fc <- pfc + <|> try (do i <- pExpr' syn + symbol "<-" + fc <- pfc e <- pExpr syn; return (DoBindP fc i e)) - <|> try (do e <- pExpr syn; fc <- pfc + <|> try (do e <- pExpr syn + fc <- pfc return (DoExp fc e)) pIdiom syn - = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]" + = do symbol "[|" + fc <- pfc + e <- pExpr syn + symbol "|]" return (PIdiom fc e) pConstant :: IParser Const @@ -962,7 +1000,9 @@ <|> try (do c <- chlit; return $ Ch c) pStatic :: IParser Static -pStatic = do lchar '['; reserved "static"; lchar ']'; +pStatic = do lchar '[' + reserved "static" + lchar ']'; return Static <|> return Dynamic @@ -971,7 +1011,7 @@ [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]] ++ toTable (reverse fixes) ++ [[backtick], - [binary "=" (\fc x y -> PEq fc x y) AssocLeft], + [binary "=" PEq AssocLeft], [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]] toTable fs = map (map toBin) @@ -984,11 +1024,14 @@ assoc (Infixr _) = AssocRight assoc (InfixN _) = AssocNone -binary name f assoc = Infix (do reservedOp name; fc <- pfc; - return (f fc)) assoc -prefix name f = Prefix (do reservedOp name; fc <- pfc; +binary name f = Infix (do reservedOp name + fc <- pfc; + return (f fc)) +prefix name f = Prefix (do reservedOp name + fc <- pfc; return (f fc)) -backtick = Infix (do lchar '`'; n <- pfName; lchar '`' +backtick = Infix (do lchar '`'; n <- pfName + lchar '`' fc <- pfc return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone @@ -998,20 +1041,23 @@ accData :: Maybe Accessibility -> Name -> [Name] -> IParser () accData (Just Frozen) n ns = do addAcc n (Just Frozen) mapM_ (\n -> addAcc n (Just Hidden)) ns -accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns +accData a n ns = do addAcc n a + mapM_ (`addAcc` a) ns pRecord :: SyntaxInfo -> IParser PDecl pRecord syn = do acc <- pAccessibility - reserved "record"; fc <- pfc - tyn_in <- pfName; ty <- pTSig (impOK syn) + reserved "record" + fc <- pfc + tyn_in <- pfName + ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in reserved "where" - open_block - push_indent + openBlock + pushIndent (cn, cty, _) <- pConstructor syn pKeepTerminator - pop_indent - close_block + popIndent + closeBlock accData acc tyn [cn] let rsyn = syn { syn_namespace = show (nsroot tyn) : syn_namespace syn } @@ -1028,30 +1074,34 @@ pData :: SyntaxInfo -> IParser PDecl pData syn = try (do acc <- pAccessibility - reserved "data"; fc <- pfc - tyn_in <- pfName; ty <- pTSig (impOK syn) + reserved "data" + fc <- pfc + tyn_in <- pfName + ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in reserved "where" - open_block - push_indent + openBlock + pushIndent cons <- many (do notEndBlock c <- pConstructor syn pKeepTerminator return c) -- (lchar '|') - pop_indent - close_block + popIndent + closeBlock accData acc tyn (map (\ (n, _, _) -> n) cons) return $ PData syn fc (PDatadecl tyn ty cons)) - <|> try (do push_indent + <|> try (do pushIndent acc <- pAccessibility - reserved "data"; fc <- pfc - tyn_in <- pfName; args <- many pName + reserved "data" + 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 (\a -> PSet) args) PSet + let ty = bindArgs (map (const PSet) args) PSet cons' <- mapM (\ (x, cargs, cfc) -> do let cty = bindArgs cargs conty return (x, cty, cfc)) cons @@ -1062,8 +1112,7 @@ mkPApp fc t xs = PApp fc t (map pexp xs) bindArgs :: [PTerm] -> PTerm -> PTerm -bindArgs [] t = t -bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t) +bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC) pConstructor syn @@ -1086,13 +1135,15 @@ --------- DSL syntax overloading --------- pDSL :: SyntaxInfo -> IParser PDecl -pDSL syn = do reserved "dsl"; n <- pfName - open_block; push_indent +pDSL syn = do reserved "dsl" + n <- pfName + openBlock + pushIndent bs <- many1 (do notEndBlock b <- pOverload syn pKeepTerminator return b) - pop_indent; close_block + popIndent; closeBlock let dsl = mkDSL bs (dsl_info syn) checkDSL dsl i <- getState @@ -1113,8 +1164,9 @@ checkDSL dsl = return () pOverload :: SyntaxInfo -> IParser (String, PTerm) -pOverload syn = do o <- identifier <|> do reserved "let"; return "let" - if (not (o `elem` overloadable)) +pOverload syn = do o <- identifier <|> do reserved "let" + return "let" + if o `notElem` overloadable then fail $ show o ++ " is not an overloading" else do lchar '=' @@ -1129,21 +1181,35 @@ clause <- pClause syn return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later +pCAF :: SyntaxInfo -> IParser PDecl +pCAF syn = do reserved "let" + n_in <- pfName; let n = expandNS syn n_in + lchar '=' + t <- pExpr syn + pTerminator + fc <- pfc + return (PCAF fc n t) + pArgExpr syn = let syn' = syn { inPattern = True } in try (pHSimpleExpr syn') <|> pSimpleExtExpr syn' pRHS :: SyntaxInfo -> Name -> IParser PTerm pRHS syn n = do lchar '='; pExpr syn <|> do symbol "?="; rhs <- pExpr syn; - return (PLet (UN "value") Placeholder rhs (PMetavar n')) + return (addLet rhs) <|> do reserved "impossible"; return PImpossible where mkN (UN x) = UN (x++"_lemma_1") mkN (NS x n) = NS (mkN x) n n' = mkN n + addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs) + addLet (PCase fc t cs) = PCase fc t (map addLetC cs) + where addLetC (l, r) = (l, addLet r) + addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n')) + pClause :: SyntaxInfo -> IParser PClause pClause syn - = try (do push_indent + = try (do pushIndent n_in <- pfName; let n = expandNS syn n_in cargs <- many (pConstraintArg syn) iargs <- many (pImplicitArg syn) @@ -1155,7 +1221,7 @@ let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn - pop_indent + popIndent return x, do pTerminator return ([], [])] @@ -1164,7 +1230,7 @@ ist <- getState setState (ist { lastParse = Just n }) return $ PClause fc n capp wargs rhs wheres) - <|> try (do push_indent + <|> try (do pushIndent wargs <- many1 (pWExpr syn) ist <- getState n <- case lastParse ist of @@ -1175,13 +1241,13 @@ let ctxt = tt_ctxt ist let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn - pop_indent + popIndent return x, do pTerminator return ([], [])] return $ PClauseR fc wargs rhs wheres) - <|> try (do push_indent + <|> try (do pushIndent n_in <- pfName; let n = expandNS syn n_in cargs <- many (pConstraintArg syn) iargs <- many (pImplicitArg syn) @@ -1190,28 +1256,28 @@ wargs <- many (pWExpr syn) let capp = PApp fc (PRef fc n) (iargs ++ cargs ++ map pexp args) + ist <- getState + setState (ist { lastParse = Just n }) reserved "with" wval <- pSimpleExpr syn - open_block + openBlock ds <- many1 $ pFunDecl syn let withs = map (fillLHSD n capp wargs) $ concat ds - close_block - ist <- getState - setState (ist { lastParse = Just n }) - pop_indent + closeBlock + popIndent return $ PWith fc n capp wargs wval withs) <|> try (do wargs <- many1 (pWExpr syn) fc <- pfc reserved "with" wval <- pSimpleExpr syn - open_block + openBlock ds <- many1 $ pFunDecl syn let withs = concat ds - close_block + closeBlock return $ PWithR fc wargs wval withs) - <|> do push_indent + <|> do pushIndent l <- pArgExpr syn op <- operator let n = expandNS syn (UN op) @@ -1221,7 +1287,7 @@ rhs <- pRHS syn n let wsyn = syn { syn_namespace = [] } (wheres, nmap) <- choice [do x <- pWhereblock n wsyn - pop_indent + popIndent return x, do pTerminator return ([], [])] @@ -1238,9 +1304,9 @@ wargs <- many (pWExpr syn) reserved "with" wval <- pSimpleExpr syn - open_block + openBlock ds <- many1 $ pFunDecl syn - close_block + closeBlock ist <- getState let capp = PApp fc (PRef fc n) [pexp l, pexp r] let withs = map (fillLHSD n capp wargs) $ concat ds @@ -1258,14 +1324,15 @@ fillLHSD n c a x = x pWExpr :: SyntaxInfo -> IParser PTerm -pWExpr syn = do lchar '|'; pExpr' syn +pWExpr syn = do lchar '|' + pExpr' syn pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)]) pWhereblock n syn - = do reserved "where"; open_block + = do reserved "where"; openBlock ds <- many1 $ pFunDecl syn let dns = concatMap (concatMap declared) ds - close_block + closeBlock return (concat ds, map (\x -> (x, decoration syn x)) dns) pDirective :: IParser [PDecl] @@ -1273,7 +1340,7 @@ return [PDirective (do addLib lib addIBC (IBCLib lib))]) <|> try (do lchar '%'; reserved "link"; obj <- strlit; - return [PDirective (do datadir <- liftIO $ getDataDir + return [PDirective (do datadir <- liftIO getDataDir o <- liftIO $ findInPath [".", datadir] obj addIBC (IBCObj o) addObjectFile o)]) diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs --- a/src/Idris/Primitives.hs +++ b/src/Idris/Primitives.hs @@ -163,6 +163,8 @@ (1, LStrRev) total, Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce) (1, LReadStr) partial, + Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce) + (0, LVMPtr) total, -- Streams Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce) (0, LStdIn) partial, diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -12,8 +12,10 @@ import Idris.Compiler import Idris.Prover import Idris.Parser +import Idris.Primitives import Idris.Coverage import Paths_idris +import Util.System import Core.Evaluate import Core.ProofShell @@ -21,6 +23,7 @@ import Core.Constraints import IRTS.Compiler +import IRTS.LParser -- import RTS.SC -- import RTS.Bytecode @@ -29,12 +32,14 @@ import System.Console.Haskeline as H import System.FilePath +import System.Exit import System.Environment import System.Process import System.Directory import System.IO import Control.Monad import Control.Monad.State +import Data.Maybe import Data.List import Data.Char import Data.Version @@ -159,7 +164,7 @@ -- [pexp t]) (tmpn, tmph) <- liftIO tempfile liftIO $ hClose tmph - compileC tmpn tm + compile ViaC tmpn tm liftIO $ system tmpn return () where fc = FC "(input)" 0 @@ -221,7 +226,7 @@ process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext ist <- get - let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm + let tm' = simplify ctxt [] {- (idris_statics ist) -} tm iputStrLn (show (delab ist tm')) process fn (RmProof n') @@ -293,7 +298,7 @@ -- (PRef (FC "main" 0) (NS (UN "main") ["main"])) (tmpn, tmph) <- liftIO tempfile liftIO $ hClose tmph - compileC tmpn m + compile ViaC tmpn m liftIO $ system tmpn return () where fc = FC "main" 0 @@ -301,13 +306,13 @@ = do (m, _) <- elabVal toplevel False (PApp fc (PRef fc (UN "run__IO")) [pexp $ PRef fc (NS (UN "main") ["main"])]) - compile f m + compileEpic f m where fc = FC "main" 0 -process fn (Compile f) +process fn (Compile target f) = do (m, _) <- elabVal toplevel False (PApp fc (PRef fc (UN "run__IO")) [pexp $ PRef fc (NS (UN "main") ["main"])]) - compileC f m + compile target f m where fc = FC "main" 0 process fn (LogLvl i) = setLogLevel i process fn Metavars @@ -351,18 +356,6 @@ [t] -> showTotal t i _ -> "" -tempfile :: IO (FilePath, Handle) -tempfile = do env <- environment "TMPDIR" - let dir = case env of - Nothing -> "/tmp" - (Just d) -> d - openTempFile dir "esc" - -environment :: String -> IO (Maybe String) -environment x = Prelude.catch (do e <- getEnv x - return (Just e)) - (\_ -> return Nothing) - displayHelp = let vstr = showVersion version in "\nIdris version " ++ vstr ++ "\n" ++ "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++ @@ -372,6 +365,36 @@ l ++ take (c1 - length l) (repeat ' ') ++ m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n" +parseArgs :: [String] -> [Opt] +parseArgs [] = [] +parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns) +parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns) +parseArgs ("--check":ns) = NoREPL : (parseArgs ns) +parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns) +parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns) +parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns) +parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns) +parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns) +parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns) +parseArgs ("--help":ns) = Usage : (parseArgs ns) +parseArgs ("--link":ns) = ShowLibs : (parseArgs ns) +parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns) +parseArgs ("--include":ns) = ShowIncs : (parseArgs ns) +parseArgs ("--version":ns) = Ver : (parseArgs ns) +parseArgs ("--verbose":ns) = Verbose : (parseArgs ns) +parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns) +parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns) +parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns) +parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns) +parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns) +parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns) +parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns) +parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns) +parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns) +parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns) +parseArgs ("--dumpc":n:ns) = DumpC n : (parseArgs ns) +parseArgs (n:ns) = Filename n : (parseArgs ns) + help = [ (["Command"], "Arguments", "Purpose"), ([""], "", ""), @@ -394,4 +417,119 @@ ([":unset"], "