idris 0.9.3.1 → 0.9.4
raw patch · 44 files changed
+1569/−754 lines, 44 files
Files
- idris.cabal +6/−3
- lib/Makefile +4/−16
- lib/io.idr +3/−0
- lib/network/sockets.idr +0/−78
- lib/prelude/complex.idr +1/−1
- lib/prelude/tactics.idr +0/−4
- lib/system.idr +2/−2
- rts/Makefile +1/−1
- rts/idris_gc.c +11/−1
- rts/idris_main.c +2/−1
- rts/idris_rts.c +197/−19
- rts/idris_rts.h +35/−2
- rts/libidris_rts.a binary
- rts/libtest.c +1/−0
- src/Core/CaseTree.hs +21/−6
- src/Core/Constraints.hs +9/−3
- src/Core/Elaborate.hs +15/−7
- src/Core/Evaluate.hs +34/−25
- src/Core/ProofState.hs +11/−1
- src/Core/TT.hs +34/−6
- src/Core/Unify.hs +57/−5
- src/IRTS/Bytecode.hs +3/−0
- src/IRTS/CodegenC.hs +13/−27
- src/IRTS/Compiler.hs +53/−37
- src/IRTS/Defunctionalise.hs +138/−44
- src/IRTS/Inliner.hs +9/−0
- src/IRTS/LParser.hs +1/−1
- src/IRTS/Lang.hs +5/−3
- src/IRTS/Simplified.hs +31/−32
- src/Idris/AbsSyntax.hs +29/−9
- src/Idris/AbsSyntaxTree.hs +15/−4
- src/Idris/Compiler.hs +2/−2
- src/Idris/Delaborate.hs +2/−1
- src/Idris/ElabDecls.hs +26/−9
- src/Idris/ElabTerm.hs +1/−1
- src/Idris/IBC.hs +8/−0
- src/Idris/Parser.hs +335/−268
- src/Idris/Primitives.hs +2/−0
- src/Idris/REPL.hs +156/−18
- src/Idris/REPLParser.hs +2/−1
- src/Main.hs +20/−116
- src/Pkg/PParser.hs +102/−0
- src/Pkg/Package.hs +137/−0
- src/Util/System.hs +35/−0
idris.cabal view
@@ -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
lib/Makefile view
@@ -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
lib/io.idr view
@@ -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+
− lib/network/sockets.idr
@@ -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;
lib/prelude/complex.idr view
@@ -6,7 +6,7 @@ module prelude.complex import builtins-+import prelude ------------------------------ Rectangular form
− lib/prelude/tactics.idr
@@ -1,4 +0,0 @@-module prelude.tactics--data Tactic = Intro (List IdrisName)- | Refine IdrisName
lib/system.idr view
@@ -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
rts/Makefile view
@@ -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
rts/idris_gc.c view
@@ -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);
rts/idris_main.c view
@@ -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); }
rts/idris_rts.c view
@@ -3,37 +3,73 @@ #include <string.h> #include <unistd.h> #include <stdarg.h>+#include <assert.h>+#include <pthread.h> #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");
rts/idris_rts.h view
@@ -6,6 +6,7 @@ #include <string.h> #include <unistd.h> #include <stdarg.h>+#include <pthread.h> // 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.
rts/libidris_rts.a view
binary file changed (21048 → 27208 bytes)
+ rts/libtest.c view
@@ -0,0 +1,1 @@+int main() {}
src/Core/CaseTree.hs view
@@ -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")
src/Core/Constraints.hs view
@@ -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
src/Core/Elaborate.hs view
@@ -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)
src/Core/Evaluate.hs view
@@ -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
src/Core/ProofState.hs view
@@ -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"
src/Core/TT.hs view
@@ -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
src/Core/Unify.hs view
@@ -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))
src/IRTS/Bytecode.hs view
@@ -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
src/IRTS/CodegenC.hs view
@@ -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 <idris_rts.h>\n#include <idris_stdfgn.h>\n#include<assert.h>\n"+headers [] = "#include <idris_rts.h>\n#include <idris_stdfgn.h>\n#include <assert.h>\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
src/IRTS/Compiler.hs view
@@ -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
src/IRTS/Defunctionalise.hs view
@@ -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
+ src/IRTS/Inliner.hs view
@@ -0,0 +1,9 @@+module IRTS.Inliner where++import Core.TT++import IRTS.Defunctionalise++inline :: DDefs -> DDefs +inline xs = xs+
src/IRTS/LParser.hs view
@@ -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)]
src/IRTS/Lang.hs view
@@ -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)
src/IRTS/Simplified.hs view
@@ -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 ++
src/Idris/AbsSyntax.hs view
@@ -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
src/Idris/AbsSyntaxTree.hs view
@@ -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
src/Idris/Compiler.hs view
@@ -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
src/Idris/Delaborate.hs view
@@ -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"
src/Idris/ElabDecls.hs view
@@ -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) =
src/Idris/ElabTerm.hs view
@@ -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 $
src/Idris/IBC.hs view
@@ -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
src/Idris/Parser.hs view
@@ -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)])
src/Idris/Primitives.hs view
@@ -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,
src/Idris/REPL.hs view
@@ -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"], "<option>", "Unset an option"), ([":q",":quit"], "", "Exit the Idris system") ]++-- invoke as if from command line+idris :: [Opt] -> IO IState+idris opts = runInputT defaultSettings $ execStateT (idrisMain opts) idrisInit++idrisMain :: [Opt] -> Idris ()+idrisMain opts = + do let inputs = opt getFile opts+ let runrepl = not (NoREPL `elem` opts)+ let output = opt getOutput opts+ let newoutput = opt getNewOutput opts+ let ibcsubdir = opt getIBCSubDir opts+ let importdirs = opt getImportDir opts+ let bcs = opt getBC opts+ let vm = opt getFOVM opts+ let pkgdirs = opt getPkgDir opts+ setREPL runrepl+ setVerbose runrepl+ setCmdLine opts+ when (Verbose `elem` opts) $ setVerbose True+ mapM_ makeOption opts+ -- if we have the --fovm flag, drop into the first order VM testing+ case vm of+ [] -> return ()+ xs -> liftIO $ mapM_ fovm xs + -- if we have the --bytecode flag, drop into the bytecode assembler+ case bcs of+ [] -> return ()+ xs -> return () -- liftIO $ mapM_ bcAsm xs + case ibcsubdir of+ [] -> setIBCSubDir ""+ (d:_) -> setIBCSubDir d+ setImportDirs importdirs+ addPkgDir "base"+ mapM_ addPkgDir pkgdirs+ elabPrims+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"+ return ()+ when runrepl $ iputStrLn banner + ist <- get+ mods <- mapM loadModule inputs+ ok <- noErrors+ when ok $ case output of+ [] -> return ()+ (o:_) -> process "" (Compile ViaC o) + when ok $ case newoutput of+ [] -> return ()+ (o:_) -> process "" (NewCompile o) + when runrepl $ repl ist inputs+ ok <- noErrors+ when (not ok) $ liftIO (exitWith (ExitFailure 1))+ where+ makeOption (OLogging i) = setLogLevel i+ makeOption TypeCase = setTypeCase True+ makeOption TypeInType = setTypeInType True+ makeOption NoCoverage = setCoverage False+ makeOption ErrContext = setErrContext True+ makeOption _ = return ()++ addPkgDir :: String -> Idris ()+ addPkgDir p = do ddir <- liftIO $ getDataDir + addImportDir (ddir ++ "/" ++ p)++getFile :: Opt -> Maybe String+getFile (Filename str) = Just str+getFile _ = Nothing++getBC :: Opt -> Maybe String+getBC (BCAsm str) = Just str+getBC _ = Nothing++getFOVM :: Opt -> Maybe String+getFOVM (FOVM str) = Just str+getFOVM _ = Nothing++getOutput :: Opt -> Maybe String+getOutput (Output str) = Just str+getOutput _ = Nothing++getNewOutput :: Opt -> Maybe String+getNewOutput (NewOutput str) = Just str+getNewOutput _ = Nothing++getIBCSubDir :: Opt -> Maybe String+getIBCSubDir (IBCSubDir str) = Just str+getIBCSubDir _ = Nothing++getImportDir :: Opt -> Maybe String+getImportDir (ImportDir str) = Just str+getImportDir _ = Nothing++getPkgDir :: Opt -> Maybe String+getPkgDir (Pkg str) = Just str+getPkgDir _ = Nothing++getPkg :: Opt -> Maybe (Bool, String)+getPkg (PkgBuild str) = Just (False, str)+getPkg (PkgInstall str) = Just (True, str)+getPkg _ = Nothing++getPkgClean :: Opt -> Maybe String+getPkgClean (PkgClean str) = Just str+getPkgClean _ = Nothing++opt :: (Opt -> Maybe a) -> [Opt] -> [a]+opt = mapMaybe ++ver = showVersion version++banner = " ____ __ _ \n" ++ + " / _/___/ /____(_)____ \n" +++ " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" +++ " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" +++ " /___/\\__,_/_/ /_/____/ Type :? for help \n" +
src/Idris/REPLParser.hs view
@@ -26,7 +26,8 @@ <|> try (do cmd ["e", "edit"]; eof; return Edit) <|> try (do cmd ["exec", "execute"]; eof; return Execute) <|> try (do cmd ["ttshell"]; eof; return TTShell)- <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))+ <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))+ <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f)) <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f)) <|> try (do cmd ["m", "metavars"]; eof; return Metavars) <|> try (do cmd ["proofs"]; eof; return Proofs)
src/Main.hs view
@@ -25,8 +25,7 @@ import Idris.Imports import Idris.Error -import IRTS.Lang-import IRTS.LParser+import Pkg.Package import Paths_idris @@ -34,94 +33,23 @@ -- on with the REPL. main = do xs <- getArgs- opts <- parseArgs xs+ let opts = parseArgs xs runInputT defaultSettings $ execStateT (runIdris opts) idrisInit runIdris :: [Opt] -> Idris ()-runIdris opts = - do let inputs = opt getFile opts- let runrepl = not (NoREPL `elem` opts)- let output = opt getOutput opts- let newoutput = opt getNewOutput opts- let ibcsubdir = opt getIBCSubDir opts- let importdirs = opt getImportDir opts- let bcs = opt getBC opts- let vm = opt getFOVM opts-+runIdris opts = do when (Ver `elem` opts) $ liftIO showver when (Usage `elem` opts) $ liftIO usage when (ShowIncs `elem` opts) $ liftIO showIncs when (ShowLibs `elem` opts) $ liftIO showLibs- setREPL runrepl- setVerbose runrepl- when (Verbose `elem` opts) $ setVerbose True- mapM_ makeOption opts- -- if we have the --fovm flag, drop into the first order VM testing- case vm of- [] -> return ()- xs -> liftIO $ mapM_ fovm xs - -- if we have the --bytecode flag, drop into the bytecode assembler- case bcs of- [] -> return ()- xs -> return () -- liftIO $ mapM_ bcAsm xs - case ibcsubdir of- [] -> setIBCSubDir ""- (d:_) -> setIBCSubDir d- setImportDirs importdirs- elabPrims- when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"- return ()- when runrepl $ iputStrLn banner - ist <- get- mods <- mapM loadModule inputs- ok <- noErrors- when ok $ case output of- [] -> return ()- (o:_) -> process "" (Compile o) - when ok $ case newoutput of- [] -> return ()- (o:_) -> process "" (NewCompile o) - when runrepl $ repl ist inputs- ok <- noErrors- when (not ok) $ liftIO (exitWith (ExitFailure 1))- where- makeOption (OLogging i) = setLogLevel i- makeOption TypeCase = setTypeCase True- makeOption TypeInType = setTypeInType True- makeOption NoCoverage = setCoverage False- makeOption ErrContext = setErrContext True- makeOption _ = return ()--getFile :: Opt -> Maybe String-getFile (Filename str) = Just str-getFile _ = Nothing--getBC :: Opt -> Maybe String-getBC (BCAsm str) = Just str-getBC _ = Nothing--getFOVM :: Opt -> Maybe String-getFOVM (FOVM str) = Just str-getFOVM _ = Nothing--getOutput :: Opt -> Maybe String-getOutput (Output str) = Just str-getOutput _ = Nothing--getNewOutput :: Opt -> Maybe String-getNewOutput (NewOutput str) = Just str-getNewOutput _ = Nothing--getIBCSubDir :: Opt -> Maybe String-getIBCSubDir (IBCSubDir str) = Just str-getIBCSubDir _ = Nothing--getImportDir :: Opt -> Maybe String-getImportDir (ImportDir str) = Just str-getImportDir _ = Nothing--opt :: (Opt -> Maybe a) -> [Opt] -> [a]-opt = mapMaybe + when (ShowLibdir `elem` opts) $ liftIO showLibdir+ case opt getPkgClean opts of+ [] -> return ()+ fs -> do liftIO $ mapM_ cleanPkg fs+ liftIO $ exitWith ExitSuccess+ case opt getPkg opts of+ [] -> idrisMain opts -- in Idris.REPL+ fs -> liftIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs usage = do putStrLn usagemsg exitWith ExitSuccess@@ -130,43 +58,17 @@ exitWith ExitSuccess showLibs = do dir <- getDataDir- putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts"+ putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts -lgmp -lpthread" exitWith ExitSuccess +showLibdir = do dir <- getDataDir+ putStrLn $ dir ++ "/"+ exitWith ExitSuccess+ showIncs = do dir <- getDataDir putStrLn $ "-I" ++ dir ++ "/rts" exitWith ExitSuccess -parseArgs :: [String] -> IO [Opt]-parseArgs [] = return []-parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)-parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)-parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)-parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)-parseArgs ("-no":n:ns) = liftM (\x -> NoREPL : NewOutput n : x) (parseArgs ns)-parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)-parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)-parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)-parseArgs ("--errorcontext":ns) = liftM (ErrContext : ) (parseArgs ns)-parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)-parseArgs ("--link":ns) = liftM (ShowLibs : ) (parseArgs ns)-parseArgs ("--include":ns) = liftM (ShowIncs : ) (parseArgs ns)-parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)-parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)-parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)-parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)-parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs ns)-parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)-parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)--ver = showVersion version--banner = " ____ __ _ \n" ++ - " / _/___/ /____(_)____ \n" ++- " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++- " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++- " /___/\\__,_/_/ /_/____/ Type :? for help \n" - usagemsg = "Idris version " ++ ver ++ "\n" ++ "--------------" ++ map (\x -> '-') ver ++ "\n" ++ "Usage: idris [input file] [options]\n" ++@@ -178,6 +80,8 @@ "\t--noprelude Don't import the prelude\n" ++ "\t--typeintype Disable universe checking\n" ++ "\t--log [level] Set debugging log level\n" ++- "\t--link Show library directories and exit (for C linking)\n" ++- "\t--include Show include directories and exit (for C linking)\n"+ "\t--dumpc [file] Dump generated C code\n" +++ "\t--libdir Show library install directory and exit\n" +++ "\t--link Show C library directories and exit (for C linking)\n" +++ "\t--include Show C include directories and exit (for C linking)\n"
+ src/Pkg/PParser.hs view
@@ -0,0 +1,102 @@+module Pkg.PParser where++import Core.CoreParser+import Core.TT+import Idris.REPL+import Idris.AbsSyntaxTree++import Paths_idris++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++type TokenParser a = PTok.TokenParser a++type PParser = GenParser Char PkgDesc++lexer :: TokenParser PkgDesc+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++data PkgDesc = PkgDesc { pkgname :: String,+ libdeps :: [String],+ objs :: [String],+ makefile :: Maybe String,+ idris_opts :: [Opt],+ sourcedir :: String,+ modules :: [Name],+ idris_main :: Name,+ execout :: Maybe String+ }+ deriving Show++defaultPkg = PkgDesc "" [] [] Nothing [] "" [] (UN "") Nothing++parseDesc :: FilePath -> IO PkgDesc+parseDesc fp = do p <- readFile fp+ case runParser pPkg defaultPkg fp p of+ Left err -> fail (show err)+ Right x -> return x++pPkg :: PParser PkgDesc+pPkg = do reserved "package"; p <- identifier + st <- getState+ setState (st { pkgname = p })+ many1 pClause + st <- getState+ return st++pClause :: PParser ()+pClause = do reserved "executable"; lchar '=';+ exec <- iName []+ st <- getState+ setState (st { execout = Just (show exec) })+ <|> do reserved "main"; lchar '=';+ main <- iName []+ st <- getState+ setState (st { idris_main = main })+ <|> do reserved "sourcedir"; lchar '=';+ src <- identifier+ st <- getState+ setState (st { sourcedir = src })+ <|> do reserved "opts"; lchar '=';+ opts <- strlit+ st <- getState+ let args = parseArgs (words opts)+ setState (st { idris_opts = args })+ <|> do reserved "modules"; lchar '=';+ ms <- sepBy1 (iName []) (lchar ',') + st <- getState+ setState (st { modules = modules st ++ ms })+ <|> do reserved "libs"; lchar '=';+ ls <- sepBy1 identifier (lchar ',')+ st <- getState+ setState (st { libdeps = libdeps st ++ ls })+ <|> do reserved "objs"; lchar '=';+ ls <- sepBy1 identifier (lchar ',')+ st <- getState+ setState (st { objs = libdeps st ++ ls })+ <|> do reserved "makefile"; lchar '=';+ mk <- iName []+ st <- getState+ setState (st { makefile = Just (show mk) })+
+ src/Pkg/Package.hs view
@@ -0,0 +1,137 @@+module Pkg.Package where++import System.Process+import System.Directory+import System.Exit+import System.IO++import Util.System++import Control.Monad+import Data.List++import Core.TT+import Idris.REPL+import Idris.AbsSyntax++import Pkg.PParser++import Paths_idris++-- To build a package:+-- * read the package description+-- * check all the library dependencies exist+-- * invoke the makefile if there is one+-- * invoke idris on each module, with idris_opts+-- * install everything into datadir/pname, if install flag is set++buildPkg :: Bool -> (Bool, FilePath) -> IO ()+buildPkg warnonly (install, fp) + = do pkgdesc <- parseDesc fp+ ok <- mapM (testLib warnonly (pkgname pkgdesc)) (libdeps pkgdesc)+ when (and ok) $+ do make (makefile pkgdesc)+ dir <- getCurrentDirectory+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc+ case (execout pkgdesc) of+ Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)+ (modules pkgdesc)+ Just o -> do let exec = dir ++ "/" ++ o+ buildMod + (NoREPL : Verbose : Output exec : idris_opts pkgdesc) + (idris_main pkgdesc)+ setCurrentDirectory dir+ when install $ installPkg pkgdesc++cleanPkg :: FilePath -> IO ()+cleanPkg fp + = do pkgdesc <- parseDesc fp+ clean (makefile pkgdesc)+ dir <- getCurrentDirectory+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc+ mapM_ rmIBC (modules pkgdesc)+ case execout pkgdesc of+ Nothing -> return ()+ Just s -> do let exec = dir ++ "/" ++ s+ putStrLn $ "Removing " ++ exec+ system $ "rm -f " ++ exec + return ()++installPkg :: PkgDesc -> IO ()+installPkg pkgdesc+ = do dir <- getCurrentDirectory+ setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc+ case (execout pkgdesc) of+ Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)+ Just o -> return () -- do nothing, keep executable locally, for noe+ mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)++buildMod :: [Opt] -> Name -> IO ()+buildMod opts n = do let f = map slash $ show n+ idris (Filename f : opts) + return ()+ where slash '.' = '/'+ slash x = x++buildMods :: [Opt] -> [Name] -> IO ()+buildMods opts ns = do let f = map ((map slash) . show) ns+ idris (map Filename f ++ opts) + return ()+ where slash '.' = '/'+ slash x = x++testLib :: Bool -> String -> String -> IO Bool+testLib warn p f + = do d <- getDataDir+ gcc <- getCC+ (tmpf, tmph) <- tempfile+ hClose tmph+ e <- system $ gcc ++ " " ++ d ++ "/rts/libtest.c -l" ++ f ++ " -o " ++ tmpf+ case e of+ ExitSuccess -> return True+ _ -> do if warn + then do putStrLn $ "Not building " ++ p ++ + " due to missing library " ++ f+ return False+ else fail $ "Missing library " ++ f++rmIBC :: Name -> IO ()+rmIBC m = do let f = toIBCFile m + putStrLn $ "Removing " ++ f+ system $ "rm -f " ++ f+ return ()+ +toIBCFile (UN n) = n ++ ".ibc"+toIBCFile (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ toIBCFile n ++installIBC :: String -> Name -> IO ()+installIBC p m = do let f = toIBCFile m+ d <- getDataDir+ let destdir = d ++ "/" ++ p ++ "/" ++ getDest m+ putStrLn $ "Installing " ++ f ++ " to " ++ destdir+ system $ "mkdir -p " ++ destdir + system $ "install " ++ f ++ " " ++ destdir+ return ()+ where getDest (UN n) = ""+ getDest (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ getDest n ++installObj :: String -> String -> IO ()+installObj p o = do d <- getDataDir+ let destdir = d ++ "/" ++ p ++ "/"+ putStrLn $ "Installing " ++ o ++ " to " ++ destdir+ system $ "mkdir -p " ++ destdir + system $ "install " ++ o ++ " " ++ destdir+ return ()++make :: Maybe String -> IO ()+make Nothing = return ()+make (Just s) = do system $ "make -f " ++ s+ return ()++clean :: Maybe String -> IO ()+clean Nothing = return ()+clean (Just s) = do system $ "make -f " ++ s ++ " clean"+ return ()+++
+ src/Util/System.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE CPP #-}+module Util.System(tempfile,environment,getCC) where++-- System helper functions.++import System.Environment+import System.IO+#if MIN_VERSION_base(4,0,0)+import Control.Exception as CE+#endif++#if MIN_VERSION_base(4,0,0)+catchIO :: IO a -> (IOError -> IO a) -> IO a+catchIO = CE.catch+#else+catchIO = catch+#endif++getCC :: IO String+getCC = do env <- environment "IDRIS_CC"+ case env of+ Nothing -> return "gcc"+ Just cc -> return cc++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 = catchIO (do e <- getEnv x+ return (Just e))+ (\_ -> return Nothing)