idris 0.9.2.1 → 0.9.3
raw patch · 59 files changed
+4566/−1397 lines, 59 filesdep −epicdep ~haskelinesetup-changedbinary-added
Dependencies removed: epic
Dependency ranges changed: haskeline
Files
- Setup.hs +24/−0
- idris.cabal +14/−6
- lib/Makefile +4/−1
- lib/builtins.idr +10/−4
- lib/checkall.idr +2/−0
- lib/io.idr +13/−8
- lib/language/reflection.idr +11/−0
- lib/network/sockets.idr +78/−0
- lib/prelude.idr +2/−2
- lib/prelude/complex.idr +5/−0
- lib/prelude/list.idr +15/−1
- lib/prelude/nat.idr +10/−3
- lib/prelude/strings.idr +25/−0
- lib/prelude/vect.idr +5/−1
- lib/system.idr +3/−0
- rts/Makefile +22/−0
- rts/idris_gc.c +113/−0
- rts/idris_gc.h +9/−0
- rts/idris_gmp.c +242/−0
- rts/idris_gmp.h +26/−0
- rts/idris_main.c +8/−0
- rts/idris_rts.c +313/−0
- rts/idris_rts.h +155/−0
- rts/idris_stdfgn.c +30/−0
- rts/idris_stdfgn.h +17/−0
- rts/libidris_rts.a binary
- src/Core/CaseTree.hs +26/−13
- src/Core/CoreParser.hs +39/−13
- src/Core/Elaborate.hs +24/−7
- src/Core/Evaluate.hs +14/−7
- src/Core/ProofState.hs +9/−3
- src/Core/TT.hs +22/−12
- src/Core/Unify.hs +21/−14
- src/IRTS/Bytecode.hs +109/−0
- src/IRTS/CodegenC.hs +257/−0
- src/IRTS/Compiler.hs +210/−0
- src/IRTS/Defunctionalise.hs +142/−0
- src/IRTS/LParser.hs +257/−0
- src/IRTS/Lang.hs +193/−0
- src/IRTS/Simplified.hs +190/−0
- src/Idris/AbsSyntax.hs +61/−926
- src/Idris/AbsSyntaxTree.hs +976/−0
- src/Idris/Compiler.hs +39/−26
- src/Idris/Coverage.hs +2/−2
- src/Idris/DSL.hs +2/−2
- src/Idris/DataOpts.hs +5/−0
- src/Idris/Delaborate.hs +17/−3
- src/Idris/ElabDecls.hs +43/−30
- src/Idris/ElabTerm.hs +48/−11
- src/Idris/Error.hs +1/−0
- src/Idris/IBC.hs +272/−49
- src/Idris/Imports.hs +37/−21
- src/Idris/Parser.hs +65/−37
- src/Idris/Primitives.hs +77/−117
- src/Idris/Prover.hs +5/−4
- src/Idris/REPL.hs +118/−24
- src/Idris/REPLParser.hs +12/−1
- src/Idris/Transforms.hs +33/−20
- src/Main.hs +84/−29
Setup.hs view
@@ -26,7 +26,25 @@ , "TARGET=" ++ idir , "IDRIS=" ++ icmd ]+ putStrLn $ "Installing run time system in " ++ idir ++ "/rts"+ make verbosity+ [ "-C", "rts", "install"+ , "TARGET=" ++ idir ++ "/rts"+ , "IDRIS=" ++ icmd+ ] +-- This is a hack. I don't know how to tell cabal that a data file needs+-- installing but shouldn't be in the distribution. And it won't make the+-- distribution if it's not there, so instead I just delete+-- the file after configure.++removeLibIdris local verbosity+ = do let icmd = ".." </> buildDir local </> "idris" </> "idris"+ make verbosity+ [ "-C", "rts", "clean"+ , "IDRIS=" ++ icmd+ ]+ checkStdLib local verbosity = do let icmd = ".." </> buildDir local </> "idris" </> "idris" putStrLn $ "Building libraries..."@@ -34,6 +52,10 @@ [ "-C", "lib", "check" , "IDRIS=" ++ icmd ]+ make verbosity+ [ "-C", "rts", "check"+ , "IDRIS=" ++ icmd+ ] -- Install libraries during both copy and install -- See http://hackage.haskell.org/trac/hackage/ticket/718@@ -44,6 +66,8 @@ , postInst = \ _ flags pkg lbi -> do installStdLib pkg lbi (S.fromFlag $ S.installVerbosity flags) NoCopyDest+ , postConf = \ _ flags _ lbi -> do+ removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags) , postClean = \ _ flags _ _ -> do cleanStdLib (S.fromFlag $ S.cleanVerbosity flags) , postBuild = \ _ flags _ lbi -> do
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.2.1+Version: 0.9.3 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -40,8 +40,12 @@ Cabal-Version: >= 1.6 Build-type: Custom +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 Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr- lib/control/monad/*.idr tutorial/examples/*.idr+ lib/control/monad/*.idr lib/language/*.idr+ tutorial/examples/*.idr+ rts/*.c rts/*.h rts/Makefile source-repository head type: git@@ -56,7 +60,8 @@ Core.ShellParser, Core.Unify, Core.Elaborate, Core.CaseTree, Core.Constraints, - Idris.AbsSyntax, Idris.Parser, Idris.REPL,+ Idris.AbsSyntax, Idris.AbsSyntaxTree,+ Idris.Parser, Idris.REPL, Idris.REPLParser, Idris.ElabDecls, Idris.Error, Idris.Delaborate, Idris.Primitives, Idris.Imports, Idris.Compiler, Idris.Prover, Idris.ElabTerm,@@ -65,13 +70,16 @@ Util.Pretty, + IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,+ IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Compiler,+ Paths_idris - Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,+ Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline<0.7, containers, process, transformers, filepath, directory,- binary, bytestring, epic>=0.9.3, pretty+ binary, bytestring, pretty Extensions: MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TemplateHaskell- ghc-prof-options: -auto-all+ ghc-prof-options: -auto-all -caf-all ghc-options: -rtsopts
lib/Makefile view
@@ -7,19 +7,22 @@ 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 clean: .PHONY rm -f *.ibc rm -f prelude/*.ibc rm -f network/*.ibc+ rm -f language/*.ibc rm -f control/monad/*.ibc linecount: .PHONY- wc -l *.idr network/*.idr prelude/*.idr control/monad/*.idr+ wc -l *.idr network/*.idr language/*.idr prelude/*.idr control/monad/*.idr .PHONY:
lib/builtins.idr view
@@ -85,11 +85,11 @@ not True = False not False = True -infixl 5 ==, /=, ==.-infixl 6 <, <=, >, >=, <., <=., >., >=.+infixl 5 ==, /=+infixl 6 <, <=, >, >= infixl 7 <<, >>-infixl 8 +,-,++,+.,-.-infixl 9 *,/,*.,/.+infixl 8 +,-,+++infixl 9 *,/ --- Numeric operators @@ -127,6 +127,12 @@ data Ordering = LT | EQ | GT++instance Eq Ordering where+ LT == LT = True+ EQ == EQ = True+ GT == GT = True+ _ == _ = False class Eq a => Ord a where compare : a -> a -> Ordering
lib/checkall.idr view
@@ -25,5 +25,7 @@ import network.cgi +import language.reflection+ import control.monad.identity import control.monad.state
lib/io.idr view
@@ -8,6 +8,9 @@ io_bind : IO a -> (a -> IO b) -> IO b io_bind (prim__IO v) k = k v +unsafePerformIO : IO a -> a+-- compiled as primitive+ abstract io_return : a -> IO a io_return x = prim__IO x@@ -18,15 +21,16 @@ run__IO : IO () -> IO () run__IO v = io_bind v (\v' => io_return v') -data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit+data FTy = FInt | FFloat | FChar | FString | FPtr | FAny Set | FUnit interpFTy : FTy -> Set-interpFTy FInt = Int-interpFTy FFloat = Float-interpFTy FChar = Char-interpFTy FString = String-interpFTy FPtr = Ptr-interpFTy FUnit = ()+interpFTy FInt = Int+interpFTy FFloat = Float+interpFTy FChar = Char+interpFTy FString = String+interpFTy FPtr = Ptr+interpFTy (FAny t) = t+interpFTy FUnit = () ForeignTy : (xs:List FTy) -> (t:FTy) -> Set ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where @@ -40,6 +44,7 @@ Foreign (ForeignTy xs t) mkForeign : Foreign x -> x--- mkForeign compiled as primitive+mkLazyForeign : Foreign x -> x+-- mkForeign and mkLazyForeign compiled as primitives
+ lib/language/reflection.idr view
@@ -0,0 +1,11 @@+module language.reflection++TTName : Set+TTName = String++data TT = Var TTName+ | Lam TTName TT TT+ | Pi TTName TT TT+ | Let TTName TT TT TT+ | App TTName TT TT+
+ lib/network/sockets.idr view
@@ -0,0 +1,78 @@+%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.idr view
@@ -194,7 +194,7 @@ print x = putStrLn (show x) getLine : IO String-getLine = mkForeign (FFun "readStr" Nil FString)+getLine = return (prim__readString prim__stdin) putChar : Char -> IO () putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c@@ -230,7 +230,7 @@ closeFile (FHandle h) = do_fclose h do_fread : Ptr -> IO String-do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h+do_fread h = return (prim__readString h) fread : File -> IO String fread (FHandle h) = do_fread h
lib/prelude/complex.idr view
@@ -1,3 +1,8 @@+{-+ © 2012 Copyright Mekeor Melire+-}++ module prelude.complex import builtins
lib/prelude/list.idr view
@@ -88,6 +88,14 @@ drop (S n) [] = [] drop (S n) (x::xs) = drop n xs +takeWhile : (a -> Bool) -> List a -> List a+takeWhile p [] = []+takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []++dropWhile : (a -> Bool) -> List a -> List a+dropWhile p [] = []+dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs+ -------------------------------------------------------------------------------- -- Misc. --------------------------------------------------------------------------------@@ -101,12 +109,18 @@ length (x::xs) = 1 + length xs ----------------------------------------------------------------------------------- Building bigger lists+-- Building (bigger) lists -------------------------------------------------------------------------------- (++) : List a -> List a -> List a (++) [] right = right (++) (x::xs) right = x :: (xs ++ right)++repeat : a -> List a+repeat x = x :: repeat x++replicate : Nat -> a -> List a+replicate n x = take n (repeat x) -------------------------------------------------------------------------------- -- Instances
lib/prelude/nat.idr view
@@ -44,6 +44,14 @@ power base O = S O power base (S exp) = mult base $ power base exp +hyper : Nat -> Nat -> Nat -> Nat+hyper O a b = S b+hyper (S O) a O = a+hyper (S(S O)) a O = O+hyper n a O = S O+hyper (S pn) a (S pb) = hyper pn a (hyper (S pn) a pb)++ -------------------------------------------------------------------------------- -- Comparisons --------------------------------------------------------------------------------@@ -115,7 +123,7 @@ abs x = x - fromInteger = fromInteger'+ fromInteger x = fromInteger' x where %assert_total fromInteger' : Int -> Nat@@ -805,7 +813,7 @@ plusRightCancelStepCase = proof { intros; refine inductiveHypothesis;- refine succInjective;+ refine succInjective _ _ ?; rewrite sym (plusSuccRightSucc left right); rewrite sym (plusSuccRightSucc left' right); rewrite p;@@ -832,4 +840,3 @@ rewrite p; trivial; }-
lib/prelude/strings.idr view
@@ -62,3 +62,28 @@ trim : String -> String trim xs = ltrim (reverse (ltrim (reverse xs))) +words' : List Char -> List (List Char)+words' s = case dropWhile isSpace s of+ [] => []+ s' => let (w, s'') = break isSpace s'+ in w :: words' s''++words : String -> List String+words s = map pack $ words' $ unpack s++foldr1 : (a -> a -> a) -> List a -> a +foldr1 f [x] = x+foldr1 f (x::xs) = f x (foldr1 f xs)+++unwords' : List (List Char) -> List Char+unwords' [] = [] +unwords' ws = (foldr1 addSpace ws)+ where+ addSpace : List Char -> List Char -> List Char+ addSpace w s = w ++ (' ' :: s) + + +unwords : List String -> String+unwords = pack . unwords' . map unpack+
lib/prelude/vect.idr view
@@ -64,13 +64,17 @@ fromList (x::xs) = x :: fromList xs ----------------------------------------------------------------------------------- Building bigger vectors+-- Building (bigger) vectors -------------------------------------------------------------------------------- total (++) : Vect a m -> Vect a n -> Vect a (m + n) (++) [] ys = ys (++) (x::xs) ys = x :: xs ++ ys++replicate : (n : Nat) -> a -> Vect a n+replicate O x = []+replicate (S k) x = x :: replicate k x -------------------------------------------------------------------------------- -- Maps
lib/system.idr view
@@ -25,3 +25,6 @@ exit : Int -> IO () exit code = mkForeign (FFun "exit" [FInt] FUnit) code +usleep : Int -> IO ()+usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i+
+ rts/Makefile view
@@ -0,0 +1,22 @@+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++LIBTARGET = libidris_rts.a++check : $(LIBTARGET)++$(LIBTARGET) : $(OBJS)+ ar r $(LIBTARGET) $(OBJS)+ ranlib $(LIBTARGET)++install : .PHONY+ mkdir -p $(TARGET)+ install $(LIBTARGET) $(HDRS) $(TARGET)++clean : .PHONY+ rm -f $(OBJS) $(LIBTARGET)++idris_rts.o: idris_rts.h++.PHONY:
+ rts/idris_gc.c view
@@ -0,0 +1,113 @@+#include "idris_rts.h"+#include "idris_gc.h"+#include <assert.h>++VAL copy(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 = copy(vm, *((VAL*)(x->info.c.args)+i)); // recursive version+ *argptr = *((VAL*)(x->info.c.args)+i);+ 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;+ case FWD:+ return x->info.ptr;+ }+ x->ty = FWD;+ x->info.ptr = cl;+ return cl;+}++void cheney(VM *vm) {+ VAL* argptr;+ int i;+ char* scan = vm->heap;+ + while(scan < vm->heap_next) {+ size_t inc = *((size_t*)scan);+ VAL heap_item = (VAL)(scan+sizeof(size_t));+ // If it's a CON, copy its arguments+ switch(heap_item->ty) {+ case CON:+ argptr = (VAL*)(heap_item->info.c.args);+ for(i = 0; i < heap_item->info.c.arity; ++i) {+ // printf("Copying %d %p\n", heap_item->info.c.tag, *argptr);+ VAL newptr = copy(vm, *argptr);+ // printf("Got %p\t\t%p %p\n", newptr, scan, vm->heap_next);+ *argptr = newptr;+ argptr++;+ }+ break;+ }+ scan += inc;+ }+ assert(scan == vm->heap_next);+}++void gc(VM* vm) {+ // printf("Collecting\n");++ char* newheap = malloc(vm -> heap_size);+ char* oldheap = vm -> heap;+ if (vm->oldheap != NULL) free(vm->oldheap);++ vm->heap = newheap;+ vm->heap_next = newheap;+ vm->heap_end = newheap + vm->heap_size;++ vm->collections++;++ VAL* root;++ for(root = vm->valstack; root < vm->valstack_top; ++root) {+ *root = copy(vm, *root);+ }+ vm->ret = copy(vm, vm->ret);+ vm->reg1 = copy(vm, vm->reg1);++ cheney(vm);++ // After reallocation, if we've still more than half filled the new heap, grow the heap+ // for next time.++ if ((vm->heap_next - vm->heap) > vm->heap_size >> 1) {+ vm->heap_size += vm->heap_growth;+ } + vm->oldheap = oldheap;++ // gcInfo(vm, 0);+}++void gcInfo(VM* vm, int doGC) {+ printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top); + printf("Total allocations: %d\n", vm->allocations);+ printf("GCs: %d\n", vm->collections);+ printf("Final heap size %d\n", (int)(vm->heap_size));+ printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));+ if (doGC) { gc(vm); }+ printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));+}
+ rts/idris_gc.h view
@@ -0,0 +1,9 @@+#ifndef _IDRISGC_H+#define _IDRISGC_H++#include "idris_rts.h"++void gc(VM* vm);+void gcInfo(VM* vm, int doGC);++#endif
+ rts/idris_gmp.c view
@@ -0,0 +1,242 @@+#include "idris_rts.h"+#include <gmp.h>+#include <stdlib.h>+#include <string.h>++VAL MKBIGI(int val) {+ return MKINT((i_int)val);+}++VAL MKBIGC(VM* vm, char* val) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));++ mpz_init(*bigint);+ mpz_set_str(*bigint, val, 10);++ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;++ return cl;+}++VAL MKBIGM(VM* vm, void* big) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));++ mpz_init(*bigint);+ mpz_set(*bigint, *((mpz_t*)big));++ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;++ return cl;+}++VAL GETBIG(VM * vm, VAL x) {+ if (ISINT(x)) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));++ mpz_init(*bigint);+ mpz_set_si(*bigint, GETINT(x));++ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;++ return cl;+ } else {+ return x;+ }+}++VAL bigAdd(VM* vm, VAL x, VAL y) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));+ mpz_add(*bigint, GETMPZ(x), GETMPZ(y));+ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;+ return cl;+}++VAL bigSub(VM* vm, VAL x, VAL y) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));+ mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));+ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;+ return cl;+}++VAL bigMul(VM* vm, VAL x, VAL y) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));+ mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));+ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;+ return cl;+}++VAL bigDiv(VM* vm, VAL x, VAL y) {+ mpz_t* bigint;+ VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));+ bigint = allocate(vm, sizeof(mpz_t));+ mpz_div(*bigint, GETMPZ(x), GETMPZ(y));+ cl -> ty = BIGINT;+ cl -> info.ptr = (void*)bigint;+ return cl;+}++VAL idris_bigPlus(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ i_int vx = GETINT(x);+ i_int vy = GETINT(y);+ if ((vx <= 0 && vy >=0) || (vx >=0 && vy <=0)) {+ return ADD(x, y);+ }+ i_int res = vx + vy;+ if (res >= 1<<30 || res <= -(1 << 30)) {+ return bigAdd(vm, GETBIG(vm, x), GETBIG(vm, y));+ } else {+ return MKINT(res);+ }+ } else {+ return bigAdd(vm, GETBIG(vm, x), GETBIG(vm, y));+ }+}++VAL idris_bigMinus(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ i_int vx = GETINT(x);+ i_int vy = GETINT(y);+ if ((vx <= 0 && vy <=0) || (vx >=0 && vy <=0)) {+ return INTOP(-, x, y);+ }+ i_int res = vx - vy;+ if (res >= 1<<30 || res <= -(1 << 30)) {+ return bigSub(vm, GETBIG(vm, x), GETBIG(vm, y));+ } else {+ return MKINT(res);+ }+ } else {+ return bigSub(vm, GETBIG(vm, x), GETBIG(vm, y));+ }+}++VAL idris_bigTimes(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ i_int vx = GETINT(x);+ i_int vy = GETINT(y);+ // we could work out likelihood of overflow by checking the number+ // of necessary bits. Here's a quick conservative hack instead.+ if ((vx < (1<<15) && vy < (1<16)) ||+ (vx < (1<<16) && vy < (1<15)) ||+ (vx < (1<<20) && vy < (1<11)) ||+ (vx < (1<<11) && vy < (1<20)) ||+ (vx < (1<<23) && vy < (1<<8)) ||+ (vx < (1<<8) && vy < (1<<23))) { // ultra-conservative!+ return INTOP(*,x,y);+ } else {+ return bigMul(vm, GETBIG(vm, x), GETBIG(vm, y));+ }+ } else {+ return bigMul(vm, GETBIG(vm, x), GETBIG(vm, y));+ }+}++VAL idris_bigDivide(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return INTOP(/, x, y);+ } else {+ return bigDiv(vm, GETBIG(vm, x), GETBIG(vm, y));+ }+}++VAL bigEq(VM* vm, VAL x, VAL y) {+ return MKINT((i_int)(mpz_cmp(GETMPZ(x), GETMPZ(y)) == 0));+}++VAL bigLt(VM* vm, VAL x, VAL y) {+ return MKINT((i_int)(mpz_cmp(GETMPZ(x), GETMPZ(y)) < 0));+}++VAL bigGt(VM* vm, VAL x, VAL y) {+ return MKINT((i_int)(mpz_cmp(GETMPZ(x), GETMPZ(y)) > 0));+}++VAL bigLe(VM* vm, VAL x, VAL y) {+ return MKINT((i_int)(mpz_cmp(GETMPZ(x), GETMPZ(y)) <= 0));+}++VAL bigGe(VM* vm, VAL x, VAL y) {+ return MKINT((i_int)(mpz_cmp(GETMPZ(x), GETMPZ(y)) >= 0));+}++VAL idris_bigEq(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return MKINT((i_int)(GETINT(x) == GETINT(y)));+ } else {+ return bigEq(vm, x, y);+ }+}++VAL idris_bigLt(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return MKINT((i_int)(GETINT(x) < GETINT(y)));+ } else {+ return bigLt(vm, x, y);+ }+}++VAL idris_bigLe(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return MKINT((i_int)(GETINT(x) <= GETINT(y)));+ } else {+ return bigLe(vm, x, y);+ }+}++VAL idris_bigGt(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return MKINT((i_int)(GETINT(x) > GETINT(y)));+ } else {+ return bigGt(vm, x, y);+ }+}++VAL idris_bigGe(VM* vm, VAL x, VAL y) {+ if (ISINT(x) && ISINT(y)) {+ return MKINT((i_int)(GETINT(x) >= GETINT(y)));+ } else {+ return bigGe(vm, x, y);+ }+}+++VAL idris_castIntBig(VM* vm, VAL i) {+ return i;+}++VAL idris_castBigInt(VM* vm, VAL i) {+ if (ISINT(i)) {+ return i;+ } else {+ return MKINT((i_int)(mpz_get_ui(GETMPZ(i))));+ }+}++VAL idris_castStrBig(VM* vm, VAL i) {+ return MKBIGC(vm, GETSTR(i));+}++VAL idris_castBigStr(VM* vm, VAL i) {+ char* str = mpz_get_str(NULL, 10, GETMPZ(GETBIG(vm, i)));+ return MKSTR(vm, str);+}+
+ rts/idris_gmp.h view
@@ -0,0 +1,26 @@+#ifndef _IDRISGMP_H+#define _IDRISGMP_H++VAL MKBIGI(int val);+VAL MKBIGC(VM* vm, char* bigint);+VAL MKBIGM(VM* vm, void* bigint);++VAL idris_bigPlus(VM*, VAL x, VAL y);+VAL idris_bigMinus(VM*, VAL x, VAL y);+VAL idris_bigTimes(VM*, VAL x, VAL y);+VAL idris_bigDivide(VM*, VAL x, VAL y);++VAL idris_bigEq(VM*, VAL x, VAL y);+VAL idris_bigLt(VM*, VAL x, VAL y);+VAL idris_bigLe(VM*, VAL x, VAL y);+VAL idris_bigGt(VM*, VAL x, VAL y);+VAL idris_bigGe(VM*, VAL x, VAL y);++VAL idris_castIntBig(VM* vm, VAL i);+VAL idris_castBigInt(VM* vm, VAL i);+VAL idris_castStrBig(VM* vm, VAL i);+VAL idris_castBigStr(VM* vm, VAL i);++#define GETMPZ(x) *((mpz_t*)((x)->info.ptr))++#endif
+ rts/idris_main.c view
@@ -0,0 +1,8 @@+int main(int argc, char* argv[]) {+ VM* vm = init_vm(4096000, 2048000); // 1024000);+ _idris__123_runMain0_125_(vm, NULL);+ //_idris_main(vm, NULL);+#ifdef IDRIS_TRACE+ gcInfo(vm, 1);+#endif+}
+ rts/idris_rts.c view
@@ -0,0 +1,313 @@+#include <stdlib.h>+#include <stdio.h>+#include <string.h>+#include <unistd.h>+#include <stdarg.h>++#include "idris_rts.h"+#include "idris_gc.h"++VM* init_vm(int stack_size, size_t heap_size) {+ 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;+ return vm;+}++void* allocate(VM* vm, size_t size) {+// return malloc(size);+ if ((size & 7)!=0) {+ size = 8 + ((size >> 3) << 3);+ }+ vm->allocations += size + sizeof(size_t);+ if (vm -> heap_next + size < vm -> heap_end) {+ void* ptr = (void*)(vm->heap_next + sizeof(size_t));+ *((size_t*)(vm->heap_next)) = size + sizeof(size_t);+ vm -> heap_next += size + sizeof(size_t);+ bzero(ptr, size);+ return ptr;+ } else {+ gc(vm);+ return allocate(vm, size);+ }+}++void* allocCon(VM* vm, int arity) {+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity);+ cl -> ty = CON;+ if (arity == 0) {+ cl -> info.c.args = NULL;+ } else {+ cl -> info.c.args = (void*)((char*)cl + sizeof(Closure));+ }+ cl -> info.c.arity = arity;+// cl -> info.c.tag = 42424242;+// printf("%p\n", cl);+ return (void*)cl;+}++VAL MKFLOAT(VM* vm, double val) {+ Closure* cl = allocate(vm, sizeof(Closure));+ cl -> ty = FLOAT;+ cl -> info.f = val;+ return cl;+}++VAL MKSTR(VM* vm, char* str) {+ Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) ++ sizeof(char)*strlen(str)+1);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);++ strcpy(cl -> info.str, str);+ return cl;+}++VAL MKPTR(VM* vm, void* ptr) {+ Closure* cl = allocate(vm, sizeof(Closure));+ cl -> ty = PTR;+ cl -> info.ptr = ptr;+ return cl;+}++VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...) {+ int i;+ va_list args;++ va_start(args, arity);++// Closure* cl = allocCon(vm, arity);+ cl -> info.c.tag = tag;+ cl -> info.c.arity = arity;+ VAL* argptr = (VAL*)(cl -> info.c.args);+ // printf("... %p %p\n", cl, argptr);++ for (i = 0; i < arity; ++i) {+ VAL v = va_arg(args, VAL);+ *argptr = v;+ argptr++;+ }+ va_end(args);+ return cl;+}++void PROJECT(VM* vm, VAL r, int loc, int arity) {+ int i;+ VAL* argptr = (VAL*)(r -> info.c.args);+ + for(i = 0; i < arity; ++i) {+ LOC(i+loc) = *argptr++;+ }+}++void SLIDE(VM* vm, int args) {+ int i;+ for(i = 0; i < args; ++i) {+ LOC(i) = TOP(i);+ }+}++void dumpStack(VM* vm) {+ int i = 0;+ VAL* root;++ for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {+ printf("%d: ", i);+ dumpVal(*root);+ if (*root >= (VAL)(vm->heap) && *root < (VAL)(vm->heap_end)) { printf("OK"); }+ printf("\n");+ }+ printf("RET: ");+ dumpVal(vm->ret);+ printf("\n");+}++void dumpVal(VAL v) {+ if (v==NULL) return;+ int i;+ if (ISINT(v)) { + printf("%d ", (int)(GETINT(v)));+ return;+ }+ switch(v->ty) {+ case CON:+ printf("%d[", v->info.c.tag);+ for(i = 0; i < v->info.c.arity; ++i) {+ VAL* args = (VAL*)v->info.c.args;+ dumpVal(args[i]);+ }+ printf("] ");+ break;+ case FWD:+ printf("FWD ");+ dumpVal((VAL)(v->info.ptr));+ break;+ default:+ printf("val");+ }++}++VAL idris_castIntStr(VM* vm, VAL i) {+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);+ sprintf(cl -> info.str, "%d", (int)(GETINT(i)));+ return cl;+}++VAL idris_castStrInt(VM* vm, VAL i) {+ char *end;+ i_int v = strtol(GETSTR(i), &end, 10);+ if (*end == '\0' || *end == '\n' || *end == '\r') + return MKINT(v);+ else + return MKINT(0); +}++VAL idris_castFloatStr(VM* vm, VAL i) {+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);+ sprintf(cl -> info.str, "%g", GETFLOAT(i));+ return cl;+}++VAL idris_castStrFloat(VM* vm, VAL i) {+ return MKFLOAT(vm, strtod(GETSTR(i), NULL));+}++VAL idris_concat(VM* vm, VAL l, VAL r) {+ char *rs = GETSTR(r);+ char *ls = GETSTR(l);+ // dumpVal(l);+ // printf("\n");+ Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);+ strcpy(cl -> info.str, ls);+ strcat(cl -> info.str, rs); + return cl;+}++VAL idris_strlt(VM* vm, VAL l, VAL r) {+ char *ls = GETSTR(l);+ char *rs = GETSTR(r);++ return MKINT((i_int)(strcmp(ls, rs) < 0));+}++VAL idris_streq(VM* vm, VAL l, VAL r) {+ char *ls = GETSTR(l);+ char *rs = GETSTR(r);++ return MKINT((i_int)(strcmp(ls, rs) == 0));+}++VAL idris_strlen(VM* vm, VAL l) {+ return MKINT((i_int)(strlen(GETSTR(l))));+}++#define BUFSIZE 256++VAL idris_readStr(VM* vm, FILE* h) {+// Modified from 'safe-fgets.c' in the gdb distribution.+// (see http://www.gnu.org/software/gdb/current/)+ char *line_ptr;+ char* line_buf = (char *) malloc (BUFSIZE);+ int line_buf_size = BUFSIZE;++ /* points to last byte */+ line_ptr = line_buf + line_buf_size - 1;++ /* so we can see if fgets put a 0 there */+ *line_ptr = 1;+ if (fgets (line_buf, line_buf_size, h) == 0)+ return MKSTR(vm, "");++ /* we filled the buffer? */+ while (line_ptr[0] == 0 && line_ptr[-1] != '\n')+ {+ /* Make the buffer bigger and read more of the line */+ line_buf_size += BUFSIZE;+ line_buf = (char *) realloc (line_buf, line_buf_size);++ /* points to last byte again */+ line_ptr = line_buf + line_buf_size - 1;+ /* so we can see if fgets put a 0 there */+ *line_ptr = 1;++ if (fgets (line_buf + line_buf_size - BUFSIZE - 1, BUFSIZE + 1, h) == 0)+ return MKSTR(vm, "");+ }++ VAL str = MKSTR(vm, line_buf);+ free(line_buf);+ return str;+}++VAL idris_strHead(VM* vm, VAL str) {+ return MKINT((i_int)(GETSTR(str)[0]));+}++VAL idris_strTail(VM* vm, VAL str) {+ return MKSTR(vm, GETSTR(str)+1);+}++VAL idris_strCons(VM* vm, VAL x, VAL xs) {+ char *xstr = GETSTR(xs);+ Closure* cl = allocate(vm, sizeof(Closure) ++ strlen(xstr) + 2);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);+ cl -> info.str[0] = (char)(GETINT(x));+ strcpy(cl -> info.str+1, xstr);+ return cl;+}++VAL idris_strIndex(VM* vm, VAL str, VAL i) {+ return MKINT((i_int)(GETSTR(str)[GETINT(i)]));+}++VAL idris_strRev(VM* vm, VAL str) {+ char *xstr = GETSTR(str);+ Closure* cl = allocate(vm, sizeof(Closure) ++ strlen(xstr) + 1);+ cl -> ty = STRING;+ cl -> info.str = (char*)cl + sizeof(Closure);+ int y = 0;+ int x = strlen(xstr);++ cl-> info.str[x+1] = '\0';+ while(x>0) {+ cl -> info.str[y++] = xstr[--x];+ }+ return cl;+}+++void stackOverflow() {+ fprintf(stderr, "Stack overflow");+ exit(-1);+}+
+ rts/idris_rts.h view
@@ -0,0 +1,155 @@+#ifndef _IDRISRTS_H+#define _IDRISRTS_H++#include <stdlib.h>+#include <stdio.h>+#include <string.h>+#include <unistd.h>+#include <stdarg.h>++// Closures++typedef enum {+ CON, INT, BIGINT, FLOAT, STRING, UNIT, PTR, FWD+} ClosureType;++typedef struct {+ int tag;+ int arity;+ void* args;+} con;++typedef struct {+ ClosureType ty;+ union {+ con c;+ int i;+ double f;+ char* str;+ void* ptr;+ } info;+} Closure;++typedef Closure* VAL;++typedef struct {+ VAL* valstack;+ int* intstack;+ double* floatstack;+ VAL* valstack_top;+ VAL* valstack_base;+ int* intstack_ptr;+ double* floatstack_ptr;+ char* heap;+ char* oldheap;+ char* heap_next;+ char* heap_end;+ VAL* stack_max;+ size_t heap_size;+ size_t heap_growth;+ int allocations;+ int collections;+ VAL ret;+ VAL reg1;+} VM;++VM* init_vm(int stack_size, size_t heap_size);++// Functions all take a pointer to their VM, and previous stack base, +// and return nothing.+typedef void(*func)(VM*, VAL*);++// Register access ++#define RVAL (vm->ret)+#define LOC(x) (*(vm->valstack_base + (x)))+#define TOP(x) (*(vm->valstack_top + (x)))+#define REG1 (vm->reg1)++// Retrieving values++#define GETSTR(x) (((VAL)(x))->info.str) +#define GETPTR(x) (((VAL)(x))->info.ptr) +#define GETFLOAT(x) (((VAL)(x))->info.f)++#define TAG(x) (ISINT(x) ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag : (-1)) )++// Integers, floats and operators++typedef intptr_t i_int;++#define MKINT(x) ((void*)((x)<<1)+1)+#define GETINT(x) ((i_int)(x)>>1)+#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 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)))++// Stack management++#define INITFRAME VAL* myoldbase+#define REBASE vm->valstack_base = oldbase+#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \+ else { bzero(vm->valstack_top, (x)*sizeof(VAL)); }+#define ADDTOP(x) vm->valstack_top += (x)+#define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x)+#define BASETOP(x) vm->valstack_base = vm->valstack_top + (x)+#define STOREOLD myoldbase = vm->valstack_base++#define CALL(f) f(vm, myoldbase);+#define TAILCALL(f) f(vm, oldbase);++// Creating new values (each value placed at the top of the stack)+VAL MKFLOAT(VM* vm, double val);+VAL MKSTR(VM* vm, char* str);+VAL MKPTR(VM* vm, void* ptr);++VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);++#define SETTAG(x, a) (x)->info.c.tag = (a)+#define SETARG(x, i, a) ((VAL*)((x)->info.c.args))[i] = ((VAL)(a))++void PROJECT(VM* vm, VAL r, int loc, int arity); +void SLIDE(VM* vm, int args);++void* allocate(VM* vm, size_t size);+void* allocCon(VM* vm, int arity);++void dumpVal(VAL r);+void dumpStack(VM* vm);++// Casts++#define idris_castIntFloat(x) MKFLOAT(vm, (double)(GETINT(x)))+#define idris_castFloatInt(x) MKINT((i_int)(GETFLOAT(x)))++VAL idris_castIntStr(VM* vm, VAL i);+VAL idris_castStrInt(VM* vm, VAL i);+VAL idris_castFloatStr(VM* vm, VAL i);+VAL idris_castStrFloat(VM* vm, VAL i);++// String primitives++VAL idris_concat(VM* vm, VAL l, VAL r);+VAL idris_strlt(VM* vm, VAL l, VAL r);+VAL idris_streq(VM* vm, VAL l, VAL r);+VAL idris_strlen(VM* vm, VAL l);+VAL idris_readStr(VM* vm, FILE* h);++VAL idris_strHead(VM* vm, VAL str);+VAL idris_strTail(VM* vm, VAL str);+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);++// Handle stack overflow. +// Just reports an error and exits.++void stackOverflow();++#include "idris_gmp.h"++#endif
+ rts/idris_stdfgn.c view
@@ -0,0 +1,30 @@+#include "idris_stdfgn.h"+#include "idris_rts.h"++void putStr(char* str) {+ printf("%s", str);+}++void* fileOpen(char* name, char* mode) {+ FILE* f = fopen(name, mode);+ return (void*)f;+}++void fileClose(void* h) {+ FILE* f = (FILE*)h;+ fclose(f);+}++void fputStr(void* h, char* str) {+ FILE* f = (FILE*)h;+ fputs(str, f);+}++int isNull(void* ptr) {+ return ptr==NULL;+}++void* idris_stdin() {+ return (void*)stdin;+}+
+ rts/idris_stdfgn.h view
@@ -0,0 +1,17 @@+#ifndef _IDRISSTDFGN_H+#define _IDRISSTDFGN_H++// A collection of useful standard functions to be used by the prelude.++void putStr(char* str);+//char* readStr();++void* fileOpen(char* f, char* mode);+void fileClose(void* h);+//char* freadStr(void* h);+void fputStr(void*h, char* str);++int isNull(void* ptr);+void* idris_stdin();++#endif
+ rts/libidris_rts.a view
binary file changed (absent → 21048 bytes)
src/Core/CaseTree.hs view
@@ -11,10 +11,10 @@ data CaseDef = CaseDef [Name] SC [Term] deriving Show -data SC = Case Name [CaseAlt]+data SC = Case Name [CaseAlt] -- invariant: lowest tags first | STerm Term | UnmatchedCase String -- error message- deriving Show+ deriving (Show, Eq, Ord) {-! deriving instance Binary SC !-}@@ -22,7 +22,7 @@ data CaseAlt = ConCase Name Int [Name] SC | ConstCase Const SC | DefaultCase SC- deriving Show+ deriving (Show, Eq, Ord) {-! deriving instance Binary CaseAlt !-}@@ -53,19 +53,32 @@ nut ps (Bind n b sc) = nut (n:ps) sc nut ps _ = [] -simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef-simpleCase tc cover [] - = CaseDef [] (UnmatchedCase "No pattern clauses") []-simpleCase tc cover cs - = let pats = map (\ (l, r) -> (toPats tc l, (l, r))) cs- numargs = length (fst (head pats)) - ns = take numargs args- (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in- CaseDef ns (prune tree) (fst st)+simpleCase :: Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef+simpleCase tc cover fc [] + = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []+simpleCase tc cover fc cs + = let pats = map (\ (avs, l, r) -> (avs, toPats tc l, (l, r))) cs+ chkPats = mapM chkAccessible pats in+ case chkPats of+ OK pats ->+ let numargs = length (fst (head pats)) + ns = take numargs args+ (tree, st) = runState + (match ns pats (defaultCase cover)) ([], numargs) in+ return $ CaseDef ns (prune tree) (fst st)+ Error err -> Error (At fc err) where args = map (\i -> MN i "e") [0..] defaultCase True = STerm Erased defaultCase False = UnmatchedCase "Error" + chkAccessible (avs, l, c) = do mapM_ (acc l) avs+ return (l, c)++ acc [] n = Error (Inaccessible n) + acc (PV x : xs) n | x == n = OK ()+ acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n+ acc (_ : xs) n = acc xs n+ data Pat = PCon Name Int [Pat] | PConst Const | PV Name@@ -154,7 +167,7 @@ caseGroups :: [Name] -> [Group] -> SC -> State CS SC caseGroups (v:vs) gs err = do g <- altGroups gs- return $ Case v g+ return $ Case v (sort g) where altGroups [] = return [DefaultCase err] altGroups (ConGroup (CName n i) args : cs)
src/Core/CoreParser.hs view
@@ -1,6 +1,7 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} -module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef) where+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef,+ maybeWithNS) where import Core.TT @@ -22,10 +23,10 @@ reservedNames = ["let", "in", "data", "record", "Set", "do", "dsl", "import", "impossible", "case", "of", "total",- "infix", "infixl", "infixr", "prefix",- "where", "with", "forall", "syntax", "proof",- "using", "params", "namespace", "class", "instance",- "public", "private", "abstract",+ "infix", "infixl", "infixr", + "where", "with", "syntax", "proof", "postulate",+ "using", "namespace", "class", "instance",+ "public", "private", "abstract", "Int", "Integer", "Float", "Char", "String", "Ptr"] } @@ -60,15 +61,40 @@ return p iName :: [String] -> CParser a Name-iName bad = do x <- identifier- when (x `elem` bad) $ fail "Reserved identifier"- return $ mkNS (reverse (parseName x))+iName bad = maybeWithNS identifier False bad++-- Enhances a given parser to accept an optional namespace. All possible+-- namespace prefixes are tried in ascending / descending order, and+-- identifiers of a given list fail.+maybeWithNS :: CParser a String -> Bool -> [String] -> CParser a Name+maybeWithNS parser ascend bad = do+ i <- option "" (lookAhead identifier)+ when (i `elem` bad) $ fail "Reserved identifier"+ let transf = if ascend then id else reverse+ (x, xs) <- choice $ transf (parserNoNS : parsersNS i)+ return $ mkName (x, xs) where- mkNS [x] = UN x- mkNS (x:xs) = NS (UN x) xs - parseName x = case span (/= '.') x of- (x, "") -> [x]- (x, '.':y) -> x : parseName y+ parserNoNS = do x <- parser; return (x, "")+ parserNS ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)+ parsersNS i = [try (parserNS ns) | ns <- (initsEndAt (=='.') i)]++-- List of all initial segments in ascending order of a list. Every such+-- initial segment ends right before an element satisfying the given+-- condition.+initsEndAt :: (a -> Bool) -> [a] -> [[a]]+initsEndAt p [] = []+initsEndAt p (x:xs) | p x = [] : x_inits_xs+ | otherwise = x_inits_xs+ where x_inits_xs = [x : cs | cs <- initsEndAt p xs]++-- Create a `Name' from a pair of strings representing a base name and its+-- namespace.+mkName :: (String, String) -> Name+mkName (n, "") = UN n +mkName (n, ns) = NS (UN n) (reverse (parseNS ns))+ where parseNS x = case span (/= '.') x of+ (x, "") -> [x]+ (x, '.':y) -> x : parseNS y pDef :: CParser a (Name, RDef) pDef = try (do x <- iName []; lchar ':'; ty <- pTerm
src/Core/Elaborate.hs view
@@ -169,6 +169,10 @@ elog str = do ES p logs prev <- get put (ES p (logs ++ str ++ "\n") prev) +getLog :: Elab' aux String+getLog = do ES p logs _ <- get+ return logs+ -- The primitives, from ProofState attack :: Elab' aux ()@@ -313,16 +317,24 @@ -- HMMM: Actually, if we get it wrong, the typechecker will complain! -- so do nothing ptm <- get_term- let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))+ let dontunify = if null imps then [] -- do all we can + else+ map fst (filter (not.snd) (zip args (map fst imps))) ES (p, a) s prev <- get- let (n, hs) = unified p- let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)- put (ES (p { unified = unify }, a) s prev)+ let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dontunify)) $ + unified p+ let unify = dropGiven dontunify hs+ put (ES (p { unified = (n, unify) }, a) s prev) end_unify- return (map (updateUnify hs) args)+ return (map (updateUnify unify) args) where updateUnify hs n = case lookup n hs of Just (P _ t _) -> t _ -> n+ dropGiven du [] = []+ dropGiven du ((n, P a t ty) : us) | n `elem` du && not (t `elem` du)+ = (t, P a n ty) : dropGiven du us+ dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us+ dropGiven du (u : us) = u : dropGiven du us apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux () apply2 fn elabs = @@ -402,6 +414,12 @@ (do focus f; fun focus s; arg) complete_fill+ hs <- get_holes+ -- We don't need a and b in the hole queue any more since they were just for+ -- checking f, so discard them if they are still there. If they haven't been solved,+ -- regret will fail+ when (a `elem` hs) $ do focus a; regret + when (b `elem` hs) $ do focus b; regret end_unify -- Abstract over an argument of unknown type, giving a name for the hole@@ -429,8 +447,7 @@ tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs) where cantResolve :: Elab' aux a- cantResolve = fail $ "Couldn't resolve alternative: " - ++ showSep ", " (map snd xs)+ cantResolve = lift $ tfail $ CantResolveAlts (map snd xs) tryAll' :: [Elab' aux a] -> -- successes (Elab' aux a, Int) -> -- smallest failure
src/Core/Evaluate.hs view
@@ -7,7 +7,7 @@ Context, initContext, ctxtAlist, uconstraints, next_tvar, addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype, addCasedef, addOperator,- lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,+ lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal, lookupTyEnv, isConName, isFnName, Value(..)) where @@ -216,7 +216,8 @@ -- | 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- = do let val = lookupDefAcc Nothing n atRepl ctxt+ = -- trace (show n) $+ do let val = lookupDefAcc Nothing n atRepl ctxt case val of [(CaseOp inl _ _ ns tree _ _, Public)] -> if simpl && (not inl || elem n stk) @@ -558,7 +559,7 @@ data Def = Function Type Term | TyDecl NameType Type | Operator Type Int ([Value] -> Maybe Value)- | CaseOp Bool Type [(Term, Term)] -- Bool for inlineable+ | CaseOp Bool Type [([Name], Term, Term)] -- Bool for inlineable [Name] SC -- Compile time case definition [Name] SC -- Run time cae definitions {-! @@ -673,14 +674,15 @@ addCons (tag+1) cons (addDef n (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt) -addCasedef :: Name -> Bool -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->+addCasedef :: Name -> Bool -> Bool -> Bool -> + [([Name], Term, Term)] -> [([Name], Term, Term)] -> 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 ps', - simpleCase tcase covering psrt) of- (CaseDef args sc _, CaseDef args' sc' _) -> + 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 addDef n (CaseOp inl ty ps args sc args' sc', Public, Unchecked) ctxt in@@ -695,6 +697,11 @@ uctxt { definitions = ctxt' } tfst (a, _, _) = a++lookupNames :: Maybe [String] -> Name -> Context -> [Name]+lookupNames root n ctxt+ = let ns = lookupCtxtName root n (definitions ctxt) in+ map fst ns lookupTy :: Maybe [String] -> Name -> Context -> [Type] lookupTy root n ctxt
src/Core/ProofState.hs view
@@ -294,9 +294,12 @@ getP (n, b) = P Bound n (binderTy b) --- Hmmm. YAGNI? regret :: RunTactic-regret = undefined+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =+ do action (\ps -> let hs = holes ps in+ ps { holes = hs \\ [x] })+ return sc+regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved" addInj :: [(Term, Term, Term)] -> StateT TState TC () addInj inj = do ps <- get@@ -315,6 +318,8 @@ fill guess ctxt env (Bind x (Hole ty) sc) = do (val, valty) <- lift $ check ctxt env guess s <- get+-- let valtyn = normalise ctxt env valty+-- let tyn = normalise ctxt env ty ns <- unify' ctxt env valty ty ps <- get let (uh, uns) = unified ps@@ -407,7 +412,8 @@ rewrite :: Raw -> RunTactic rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' = do (tmv, tmt) <- lift $ check ctxt env tm- case unApply tmt of+ let tmt' = normalise ctxt env tmt+ case unApply tmt' of (P _ (UN "=") _, [lt,rt,l,r]) -> do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t) let newt = mkP l r l t
src/Core/TT.hs view
@@ -43,42 +43,50 @@ show (FC f l) = f ++ ":" ++ show l data Err = Msg String- | CantUnify Term Term Err Int -- Int is 'score' - how much we did unify+ | InternalMsg String+ | CantUnify Term Term Err [(Name, Type)] Int -- Int is 'score' - how much we did unify | NoSuchVariable Name | NotInjective Term Term Term | CantResolve Term+ | CantResolveAlts [String] | IncompleteTerm Term | UniverseError | ProgramLineComment+ | Inaccessible Name | At FC Err deriving Eq instance Sized Err where size (Msg msg) = length msg- size (CantUnify left right err score) = size left + size right + size err+ size (InternalMsg msg) = length msg+ size (CantUnify left right err _ score) = size left + size right + size err size (NoSuchVariable name) = size name size (NotInjective l c r) = size l + size c + size r size (CantResolve trm) = size trm+ size (CantResolveAlts _) = 1 size (IncompleteTerm trm) = size trm size UniverseError = 1 size ProgramLineComment = 1 size (At fc err) = size fc + size err+ 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 instance Show Err where show (Msg s) = s- show (CantUnify l r e i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "- ++ show e ++ " " ++ show i+ 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 (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) $$@@ -112,7 +120,7 @@ x >>= k = case x of OK v -> k v Error e -> Error e- fail e = Error (Msg e)+ fail e = Error (InternalMsg e) tfail :: Err -> TC a tfail e = Error e@@ -230,8 +238,8 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String | IType | BIType | FlType | ChType | StrType - | PtrType | Forgot- deriving Eq+ | PtrType | VoidType | Forgot+ deriving (Eq, Ord) {-! deriving instance Binary Const !-}@@ -251,6 +259,7 @@ pretty ChType = text "Char" pretty StrType = text "String" pretty PtrType = text "Ptr"+ pretty VoidType = text "Void" pretty Forgot = text "Forgot" data Raw = Var Name@@ -288,7 +297,7 @@ binderVal :: b } | PVar { binderTy :: b } | PVTy { binderTy :: b }- deriving (Show, Eq, Functor)+ deriving (Show, Eq, Ord, Functor) {-! deriving instance Binary Binder !-}@@ -373,7 +382,7 @@ type UCs = (Int, [UConstraint]) data NameType = Bound | Ref | DCon Int Int | TCon Int Int- deriving (Show)+ deriving (Show, Ord) {-! deriving instance Binary NameType !-}@@ -398,7 +407,7 @@ | Constant Const | Erased | Set UExp- deriving Functor+ deriving (Ord, Functor) {-! deriving instance Binary TT !-}@@ -599,6 +608,7 @@ show ChType = "Char" show StrType = "String" show PtrType = "Ptr"+ show VoidType = "Void" showEnv env t = showEnv' env t False showEnvDbg env t = showEnv' env t True
src/Core/Unify.hs view
@@ -25,12 +25,16 @@ unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)], Injs, Fails) unify ctxt env topx topy - = case runStateT - (un' False [] (normalise ctxt env topx) (normalise ctxt env topy))- (UI 0 [] []) of- OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)--- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s- Error e -> tfail e+ = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of+ -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])+ -- _ -> + let topxn = normalise ctxt env topx+ topyn = normalise ctxt env topy in+ case runStateT (un' False [] topxn topyn)+ (UI 0 [] []) of+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)+-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s+ Error e -> tfail e where notTrivial (x, P _ x' _) = x /= x' notTrivial _ = True@@ -76,18 +80,19 @@ un' fn bnames (App fx ax) (App fy ay) = do uplus -- do the second one if the first adds any errors (do hf <- un' True bnames fx fy - let ax' = normalise ctxt env (substNames hf ax)- let ay' = normalise ctxt env (substNames hf ay)+ let ax' = hnormalise hf ctxt env (substNames hf ax)+ let ay' = hnormalise hf ctxt env (substNames hf ay) ha <- un' False bnames ax' ay' sc 1 combine bnames hf ha) (do ha <- un' False bnames ax ay- let fx' = normalise ctxt env (substNames ha fx)- let fy' = normalise ctxt env (substNames ha fy)+ let fx' = hnormalise ha ctxt env (substNames ha fx)+ let fy' = hnormalise ha ctxt env (substNames ha fy) hf <- un' False bnames fx' fy' sc 1 combine bnames hf ha)-+ where hnormalise [] _ _ t = t+ hnormalise ns ctxt env t = normalise ctxt env t 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@@ -99,7 +104,7 @@ 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) s+ let err = CantUnify topx topy (CantUnify x y (Msg "") [] s) (errEnv env) s put (UI s i ((x, y, env, err) : f)) return [] -- lift $ tfail err @@ -119,8 +124,8 @@ 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)- s+ (CantUnify (binderTy x) (binderTy y) (Msg "") [] s)+ (errEnv env) s put (UI s i ((binderTy x, binderTy y, env, err) : f)) return [] -- lift $ tfail err @@ -131,6 +136,8 @@ Just t' -> do un' False bnames t t' sc 1 combine bnames as bs++errEnv = map (\(x, b) -> (x, binderTy b)) holeIn :: Env -> Name -> Bool holeIn env n = case lookup n env of
+ src/IRTS/Bytecode.hs view
@@ -0,0 +1,109 @@+module IRTS.Bytecode where++import IRTS.Lang+import IRTS.Simplified+import Core.TT+import Data.Maybe++{- We have: ++BASE: Current stack frame's base+TOP: Top of stack+OLDBASE: Passed in to each function, the previous stack frame's base++L i refers to the stack item at BASE + i+T i refers to the stack item at TOP + i++RVal is a register in which computed values (essentially, what a function+returns) are stored.++-}++data Reg = RVal | L Int | T Int | Tmp+ deriving (Show, Eq)++data BC = ASSIGN Reg Reg+ | ASSIGNCONST Reg Const+ | MKCON Reg Int [Reg]+ | CASE Reg [(Int, [BC])] (Maybe [BC])+ | PROJECT Reg Int Int -- get all args from reg, put them from Int onwards+ | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])+ | CALL Name+ | TAILCALL Name+ | FOREIGNCALL Reg FLang FType String [(FType, Reg)] + | SLIDE Int -- move this number from TOP to BASE + | REBASE -- set BASE = OLDBASE+ | RESERVE Int -- reserve n more stack items + -- (i.e. check there's space, grow if necessary)+ | ADDTOP Int -- move the top of stack up+ | TOPBASE Int -- set TOP = BASE + n+ | BASETOP Int -- set BASE = TOP + n+ | STOREOLD -- set OLDBASE = BASE+ | OP Reg PrimFn [Reg]+ | ERROR String+ deriving Show++toBC :: (Name, SDecl) -> (Name, [BC])+toBC (n, SFun n' args locs exp) + = (n, reserve locs ++ bc RVal exp True)+ where reserve 0 = []+ reserve n = [RESERVE n, ADDTOP n]++clean True = [TOPBASE 0, REBASE]+clean False = []++bc :: Reg -> SExp -> Bool -> -- returning+ [BC]+bc reg (SV (Glob n)) r = bc reg (SApp False n []) r+bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r+bc reg (SApp False f vs) r+ = RESERVE (length vs) : moveReg 0 vs+ ++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++ + assign reg RVal ++ clean r+bc reg (SApp True f vs) r+ = RESERVE (length vs) : moveReg 0 vs+ ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]+bc reg (SForeign l t fname args) r+ = FOREIGNCALL reg l t fname (map farg args) : clean r+ where farg (ty, Loc i) = (ty, L i)+bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r+bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r+ where getL (Loc x) = L x+bc reg (SConst i) r = ASSIGNCONST reg i : clean r+bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r+ where getL (Loc x) = L x+bc reg (SError str) r = [ERROR str]+bc reg (SCase (Loc l) alts) r + | isConst alts = constCase reg (L l) alts r+ | otherwise = conCase reg (L l) alts r++isConst [] = False+isConst (SConstCase _ _ : xs) = True+isConst (SConCase _ _ _ _ _ : xs) = False+isConst (_ : xs) = False++moveReg off [] = []+moveReg off (Loc x : xs) = assign (T off) (L x) ++ moveReg (off + 1) xs++assign r1 r2 | r1 == r2 = []+ | otherwise = [ASSIGN r1 r2]++conCase reg l xs r = [CASE l (mapMaybe (caseAlt l reg r) xs)+ (defaultAlt reg xs r)]++constCase reg l xs r = [CONSTCASE l (mapMaybe (constAlt l reg r) xs)+ (defaultAlt reg xs r)]++caseAlt l reg r (SConCase lvar tag _ args e) + = Just (tag, PROJECT l lvar (length args) : bc reg e r) +caseAlt l reg r _ = Nothing++constAlt l reg r (SConstCase c e) + = Just (c, bc reg e r) +constAlt l reg r _ = Nothing++defaultAlt reg [] r = Nothing+defaultAlt reg (SDefaultCase e : _) r = Just (bc reg e r)+defaultAlt reg (_ : xs) r = defaultAlt reg xs r++
+ src/IRTS/CodegenC.hs view
@@ -0,0 +1,257 @@+{-# LANGUAGE CPP #-}++module IRTS.CodegenC where++import IRTS.Bytecode+import IRTS.Lang+import IRTS.Simplified+import Core.TT+import Paths_idris++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)] ->+ String -> -- output file name+ Bool -> -- generate executable if True, only .o if False + [FilePath] -> -- include files+ String -> -- extra compiler flags+ DbgLevel ->+ IO ()+codegenC defs out exec incs libs dbg+ = do -- print defs+ let bc = map toBC defs+ let h = concatMap toDecl (map fst bc)+ let cc = concatMap (uncurry toC) bc+ d <- getDataDir+ mprog <- readFile (d ++ "/rts/idris_main.c")+ let cout = headers incs ++ debug dbg ++ h ++ cc ++ + (if exec then mprog else "")+ (tmpn, tmph) <- tempfile+ hPutStr tmph cout+ hFlush tmph+ hClose tmph+ let gcc = "gcc -x c " ++ + (if exec then "" else " - c ") +++ gccDbg dbg +++ " " ++ tmpn +++ " `idris --link` `idris --include` " ++ libs +++ " -lidris_rts -lgmp -o " ++ out+ -- putStrLn cout+ 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 (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs++debug TRACE = "#define IDRIS_TRACE\n\n"+debug _ = ""++gccDbg DEBUG = "-g"+gccDbg TRACE = "-O2"+gccDbg _ = "-O2"++cname :: Name -> String+cname n = "_idris_" ++ concatMap cchar (show n)+ where cchar x | isAlpha x || isDigit x = [x]+ | otherwise = "_" ++ show (fromEnum x) ++ "_"++indent i = take (i * 4) (repeat ' ')++creg RVal = "RVAL"+creg (L i) = "LOC(" ++ show i ++ ")"+creg (T i) = "TOP(" ++ show i ++ ")"+creg Tmp = "REG1"++toDecl :: Name -> String+toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n" ++toC :: Name -> [BC] -> String+toC f code + = -- "/* " ++ show code ++ "*/\n\n" ++ + "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" +++ indent 1 ++ "INITFRAME;\n" ++ + concatMap (bcc 1) code ++ "}\n\n"++bcc :: Int -> BC -> String+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"+bcc i (ASSIGNCONST l c) + = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"+ where+ mkConst (I i) = "MKINT(" ++ show i ++ ")"+ mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"+ | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"+ mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"+ mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"+ mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"+ mkConst _ = "MKINT(42424242)"+bcc i (MKCON l tag args)+ = indent i ++ creg Tmp ++ " = allocCon(vm, " ++ show (length args) ++ + "); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" +++ indent i ++ setArgs 0 args ++ "\n" ++ + indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"+ +-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " +++-- show (length args) ++ concatMap showArg args ++ ");\n"+ where showArg r = ", " ++ creg r+ setArgs i [] = ""+ setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x +++ "); " ++ setArgs (i + 1) xs++bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++ + ", " ++ show a ++ ");\n"+bcc i (CASE r code def) + = indent i ++ "switch(TAG(" ++ creg r ++ ")) {\n" +++ concatMap (showCase i) code +++ showDef i def +++ indent i ++ "}\n"+ where+ showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"+ ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"+ showDef i Nothing = ""+ showDef i (Just c) = indent i ++ "default:\n" + ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"+bcc i (CONSTCASE r code def) + = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" +++ concatMap (showCase i) code +++ showDef i def +++ indent i ++ "}\n"+ where+ showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"+ ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"+ showDef i Nothing = ""+ showDef i (Just c) = indent i ++ "default:\n" + ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"+bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"+bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"+bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"+bcc i REBASE = indent i ++ "REBASE;\n"+bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"+bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"+bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"+bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"+bcc i STOREOLD = indent i ++ "STOREOLD;\n"+bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"+bcc i (FOREIGNCALL l LANG_C rty fn args)+ = indent i ++ + c_irts rty (creg l ++ " = ") + (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"+ where fcall (t, arg) = irts_c t (creg arg)+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"+-- bcc i _ = indent i ++ "// not done yet\n"++c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ "))"+c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"+c_irts FString l x = l ++ "MKSTR(" ++ x ++ ")"+c_irts FUnit l x = x+c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"+c_irts FDouble l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"+c_irts FAny l x = l ++ x++irts_c FInt x = "GETINT(" ++ x ++ ")"+irts_c FChar x = "GETINT(" ++ x ++ ")"+irts_c FString x = "GETSTR(" ++ x ++ ")"+irts_c FUnit x = x+irts_c FPtr x = "GETPTR(" ++ x ++ ")"+irts_c FDouble x = "GETFLOAT(" ++ x ++ ")"+irts_c FAny x = x++doOp v LPlus [l, r] = v ++ "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LMinus [l, r] = v ++ "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LTimes [l, r] = v ++ "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LDiv [l, r] = v ++ "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LEq [l, r] = v ++ "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LLt [l, r] = v ++ "INTOP(<," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LLe [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"+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 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 ++ ")"+doOp v LFEq [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LFLt [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LFLe [l, r] = v ++ "FLOATBOP(<=," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LFGt [l, r] = v ++ "FLOATBOP(>," ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LFGe [l, r] = v ++ "FLOATBOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"++doOp v LBPlus [l, r] = v ++ "idris_bigPlus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBMinus [l, r] = v ++ "idris_bigMinus(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBTimes [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBDiv [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBEq [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBLt [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBLe [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBGt [l, r] = v ++ "idris_bigGt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LBGe [l, r] = v ++ "idris_bigGe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"++doOp v LStrConcat [l,r] = v ++ "idris_concat(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LStrLt [l,r] = v ++ "idris_strlt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LStrEq [l,r] = v ++ "idris_streq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"+doOp v LStrLen [x] = v ++ "idris_strlen(vm, " ++ creg x ++ ")"++doOp v LIntFloat [x] = v ++ "idris_castIntFloat(" ++ creg x ++ ")"+doOp v LFloatInt [x] = v ++ "idris_castFloatInt(" ++ creg x ++ ")"+doOp v LIntStr [x] = v ++ "idris_castIntStr(vm, " ++ creg x ++ ")"+doOp v LStrInt [x] = v ++ "idris_castStrInt(vm, " ++ creg x ++ ")"+doOp v LIntBig [x] = v ++ "idris_castIntBig(vm, " ++ creg x ++ ")"+doOp v LBigInt [x] = v ++ "idris_castBigInt(vm, " ++ creg x ++ ")"+doOp v LStrBig [x] = v ++ "idris_castStrBig(vm, " ++ creg x ++ ")"+doOp v LBigStr [x] = v ++ "idris_castBigStr(vm, " ++ creg x ++ ")"+doOp v LFloatStr [x] = v ++ "idris_castFloatStr(vm, " ++ creg x ++ ")"+doOp v LStrFloat [x] = v ++ "idris_castStrFloat(vm, " ++ creg x ++ ")"++doOp v LReadStr [x] = v ++ "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"+doOp _ LPrintNum [x] = "printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"+doOp _ LPrintStr [x] = "fputs(GETSTR(" ++ creg x ++ "), stdout)"++doOp v LFExp [x] = v ++ "MKFLOAT(exp(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFLog [x] = v ++ "MKFLOAT(log(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFSin [x] = v ++ "MKFLOAT(sin(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFCos [x] = v ++ "MKFLOAT(cos(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFTan [x] = v ++ "MKFLOAT(tan(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFASin [x] = v ++ "MKFLOAT(asin(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFACos [x] = v ++ "MKFLOAT(acos(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFATan [x] = v ++ "MKFLOAT(atan(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFSqrt [x] = v ++ "MKFLOAT(floor(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFFloor [x] = v ++ "MKFLOAT(ceil(GETFLOAT(" ++ creg x ++ ")))"+doOp v LFCeil [x] = v ++ "MKFLOAT(sqrt(GETFLOAT(" ++ creg x ++ ")))"++doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")"+doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"+doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"+doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"++doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"+doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"+doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"++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
@@ -0,0 +1,210 @@+{-# LANGUAGE PatternGuards #-}++module IRTS.Compiler where++import IRTS.Lang+import IRTS.Defunctionalise+import IRTS.Simplified+import IRTS.CodegenC++import Idris.AbsSyntax+import Core.TT+import Core.Evaluate+import Core.CaseTree++import Control.Monad.State+import Data.List+import System.Process+import System.IO+import System.Directory+import System.Environment++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+ 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 [] "" NONE+ Error e -> fail $ show e + where checkMVs = do i <- get+ case idris_metavars i \\ primDefs of+ [] -> return ()+ ms -> fail $ "There are undefined metavariables: " ++ show ms+ inDir d h = do let f = d ++ "/" ++ h+ ex <- doesFileExist f+ if ex then return f else return h++irMain :: TT Name -> Idris LDecl+irMain tm = do i <- ir tm+ return $ LFun (MN 0 "runMain") [] (LForce i)++allNames :: [Name] -> Name -> Idris [Name]+allNames ns n | n `elem` ns = return []+allNames ns n = do i <- get+ case lookupCtxt Nothing n (idris_callgraph i) of+ [ns'] -> do more <- mapM (allNames (n:ns)) ns' + return (nub (n : concat more))+ _ -> return [n]++mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]+mkDecls t used + = do i <- getIState+ let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)+ decls <- mapM build ds+ return decls++isCon (TyDecl _ _) = True+isCon _ = False++class ToIR a where+ ir :: a -> Idris LExp++build :: (Name, Def) -> Idris (Name, LDecl)+build (n, d)+ = do i <- getIState+ case lookup n (idris_scprims i) of+ Just (ar, op) -> + let args = map (\x -> MN x "op") [0..] in+ return (n, (LFun n (take ar args) + (LOp op (map (LV . Glob) (take ar args)))))+ _ -> do def <- mkLDecl n d+ logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def+ return (n, def)++declArgs args n (LLam xs x) = declArgs (args ++ xs) n x+declArgs args n x = LFun n args x ++mkLDecl n (Function tm _) = do e <- ir tm+ 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 (TCon t a) _) = return $ LConstructor n (-1) a+mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))++instance ToIR (TT Name) where + ir tm = ir' [] tm where+ ir' env tm@(App f a)+ | (P _ (UN "mkForeign") _, args) <- unApply tm+ = doForeign 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 "prim__IO") _, [v]) <- unApply tm+ = do v' <- ir' env v+ return v'+ | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm+ = do v' <- ir' env v + k' <- ir' env k+ return (LApp False k' [LForce v'])+ | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm+ = do size' <- ir' env size+ t' <- ir' env t+ return t' -- TODO $ malloc_ size' t'+ | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm+ = do t' <- ir' env t+ return t' -- TODO+ | (P (DCon t a) n _, args) <- unApply tm+ = irCon env t a n args+ | (f, args) <- unApply tm+ = do f' <- ir' env f+ 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 (Bind n (Lam _) sc)+ = do 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+ return $ LLet n v' sc'+ ir' env (Bind _ _ _) = return $ LConst (I 424242)+ ir' env (Constant c) = return $ LConst c+ ir' env _ = return $ LError "Impossible"++ irCon env t arity n args+ | length args == arity = buildApp env (LV (Glob n)) args+ | otherwise = let extra = satArgs (arity - length args) in+ do sc' <- irCon env t arity n + (args ++ map (\n -> P Bound n undefined) extra)+ return $ LLam extra sc'+ + satArgs n = map (\i -> MN i "sat") [1..n]++ buildApp env e [] = return e+ 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"++getFTypes :: TT Name -> [FType]+getFTypes tm = case unApply tm of+ (nil, []) -> []+ (cons, [ty, xs]) -> + let rest = getFTypes xs in+ mkIty' ty : rest++mkIty' (P _ (UN ty) _) = mkIty ty+mkIty' _ = FAny++mkIty "FInt" = FInt+mkIty "FFloat" = FDouble+mkIty "FChar" = FChar+mkIty "FString" = FString+mkIty "FPtr" = FPtr+mkIty "FUnit" = FUnit++instance ToIR ([Name], SC) where+ ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree+ tree' <- ir tree+ return $ LLam args tree'++instance ToIR SC where+ ir (STerm t) = ir t+ ir (UnmatchedCase str) = return $ LError str+ ir (Case n alts) = do alts' <- mapM mkIRAlt alts+ return $ LCase (LV (Glob n)) alts'+ where+ mkIRAlt (ConCase n t args rhs) + = do rhs' <- ir rhs+ return $ LConCase (-1) n args rhs'+ mkIRAlt (ConstCase (I i) rhs) + = do rhs' <- ir rhs+ return $ LConstCase (I i) rhs'+ mkIRAlt (ConstCase IType rhs) + = do rhs' <- ir rhs + return $ LDefaultCase rhs'+ mkIRAlt (ConstCase c rhs) + = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"+ mkIRAlt (DefaultCase rhs)+ = do rhs' <- ir rhs+ return $ LDefaultCase rhs'+++++
+ src/IRTS/Defunctionalise.hs view
@@ -0,0 +1,142 @@+module IRTS.Defunctionalise where++import IRTS.Lang+import Core.TT++import Debug.Trace+import Data.Maybe+import Data.List++defunctionalise :: Int -> LDefs -> LDefs +defunctionalise nexttag defs + = let all = toAlist defs+ -- sort newcons so that EVAL and APPLY cons get sequential tags+ newcons = sortBy conord $ concatMap toCons (getFn all)+ eval = mkEval newcons+ app = mkApply newcons+ condecls = declare nexttag newcons in+ addAlist (eval : app : condecls ++ (map (addApps defs) all)) emptyContext+ where conord (n, _, _) (n', _, _) = compare n n'++getFn :: [(Name, LDecl)] -> [(Name, Int)]+getFn xs = mapMaybe fnData xs+ where fnData (n, LFun _ args _) = Just (n, length args) + fnData _ = Nothing++-- To defunctionalise:+--+-- 1 Create a data constructor for each function+-- 2 Create a data constructor for each underapplication of a function+-- 3 Convert underapplications to their corresponding constructors+-- 4 Create an EVAL function which calls the appropriate function for data constructors+-- created as part of step 1+-- 5 Create an APPLY function which adds an argument to each underapplication (or calls+-- APPLY again for an exact application)+-- 6 Wrap overapplications in chains of APPLY+-- 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))+ where+ aa env (LV (Glob n)) | n `elem` env = LV (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'+ [LFun _ as _] -> let arity = length as in+ fixApply tc n args' arity+ [] -> chainAPPLY (LV (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'+ [LFun _ as _] -> let arity = length as in+ fixLazyApply n args' arity+ [] -> chainAPPLY (LV (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++ 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)++ 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)++ 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)+ + chainAPPLY f [] = f+ chainAPPLY f (a : as) = chainAPPLY (LApp False (LV (Glob (MN 0 "APPLY"))) [f, a]) as++eEVAL x = LApp False (LV (Glob (MN 0 "EVAL"))) [x]++data EvalApply a = EvalCase a+ | ApplyCase a+ deriving Show++-- 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 (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)))))))+ : 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) ++ + [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")))+ (mapMaybe evalCase xs +++ [LDefaultCase (LV (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"))])+ (mapMaybe applyCase xs)))+ where+ applyCase (n, t, ApplyCase x) = Just x+ applyCase _ = Nothing++declare :: Int -> [(Name, Int, EvalApply LAlt)] -> [(Name, LDecl)]+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)+++genArgs i = MN i "P_c" : genArgs (i + 1)++mkFnCon n = MN 0 ("P_" ++ show n)+mkUnderCon n 0 = n+mkUnderCon n missing = MN missing ("U_" ++ show n)+
+ src/IRTS/LParser.hs view
@@ -0,0 +1,257 @@+module IRTS.LParser where++import Core.CoreParser+import Core.TT+import IRTS.Lang+import IRTS.Simplified+import IRTS.Bytecode+import IRTS.CodegenC+import IRTS.Defunctionalise+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++import Data.List+import Control.Monad.State+import Debug.Trace+import Data.Maybe+import System.FilePath++type TokenParser a = PTok.TokenParser a++type LParser = GenParser Char ()++lexer :: TokenParser ()+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++fovm :: FilePath -> IO ()+fovm f = do defs <- parseFOVM f+ let (nexttag, tagged) = addTags 0 (liftAll defs)+ let ctxtIn = addAlist tagged emptyContext+ let defuns = defunctionalise nexttag ctxtIn+ putStrLn $ showSep "\n" (map show (toAlist defuns))+ let checked = checkDefs defuns (toAlist defuns)+-- print checked+ case checked of+ OK c -> codegenC c "a.out" True ["math.h"] "" TRACE+ Error e -> fail $ show e ++parseFOVM :: FilePath -> IO [(Name, LDecl)]+parseFOVM fname = do -- putStrLn $ "Reading " ++ fname+ fp <- readFile fname+ case runParser pProgram () fname fp of+ Left err-> fail (show err)+ Right x -> return x++pProgram :: LParser [(Name, LDecl)]+pProgram = do fs <- many1 pLDecl+ eof+ return fs ++pLDecl :: LParser (Name, LDecl)+pLDecl = do reserved "data"+ n <- iName []+ ar <- natural+ return (n, LConstructor n (-1) (fromInteger ar))+ <|> do reserved "fun"+ n <- iName []+ lchar '('+ args <- sepBy (iName []) (lchar ',')+ lchar ')'+ lchar '='+ def <- pLExp+ return (n, LFun n args def)++pLExp = buildExpressionParser optable pLExp' ++optable = [[binary "*" (\x y -> LOp LTimes [x,y]) AssocLeft,+ binary "/" (\x y -> LOp LDiv [x,y]) AssocLeft,+ binary "*." (\x y -> LOp LFTimes [x,y]) AssocLeft,+ binary "/." (\x y -> LOp LFDiv [x,y]) AssocLeft,+ binary "*:" (\x y -> LOp LBTimes [x,y]) AssocLeft,+ binary "/:" (\x y -> LOp LBDiv [x,y]) AssocLeft+ ],+ [+ binary "+" (\x y -> LOp LPlus [x,y]) AssocLeft,+ binary "-" (\x y -> LOp LMinus [x,y]) AssocLeft,+ binary "++" (\x y -> LOp LStrConcat [x,y]) AssocLeft,+ binary "+." (\x y -> LOp LFPlus [x,y]) AssocLeft,+ binary "-." (\x y -> LOp LFMinus [x,y]) AssocLeft,+ binary "+:" (\x y -> LOp LBPlus [x,y]) AssocLeft,+ binary "-:" (\x y -> LOp LBMinus [x,y]) AssocLeft+ ],+ [+ binary "==" (\x y -> LOp LEq [x, y]) AssocNone,+ binary "==." (\x y -> LOp LFEq [x, y]) AssocNone,+ binary "<" (\x y -> LOp LLt [x, y]) AssocNone,+ binary "<." (\x y -> LOp LFLt [x, y]) AssocNone,+ binary ">" (\x y -> LOp LGt [x, y]) AssocNone,+ binary ">." (\x y -> LOp LFGt [x, y]) AssocNone,+ binary "<=" (\x y -> LOp LLe [x, y]) AssocNone,+ binary "<=." (\x y -> LOp LFLe [x, y]) AssocNone,+ binary ">=" (\x y -> LOp LGe [x, y]) AssocNone,+ binary ">=." (\x y -> LOp LFGe [x, y]) AssocNone,++ binary "==:" (\x y -> LOp LBEq [x, y]) AssocNone,+ binary "<:" (\x y -> LOp LBLt [x, y]) AssocNone,+ binary ">:" (\x y -> LOp LBGt [x, y]) AssocNone,+ binary "<=:" (\x y -> LOp LBLe [x, y]) AssocNone,+ binary ">=:" (\x y -> LOp LBGe [x, y]) AssocNone+ ]]++binary name f assoc = Infix (do reservedOp name; return f) assoc++pLExp' :: LParser LExp+pLExp' = try (do lchar '%'; pCast)+ <|> try (do lchar '%'; pPrim)+ <|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True)+ x <- iName [];+ lazy <- option False (do lchar '@'; return True)+ lchar '('+ args <- sepBy pLExp (lchar ',')+ lchar ')'+ if null args + then if lazy then return (LLazyApp x [])+ else return (LV (Glob x)) + else if lazy then return (LLazyApp x args)+ else return (LApp tc (LV (Glob x)) args))+ <|> do lchar '('; e <- pLExp; lchar ')'; return e+ <|> pLConst+ <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp+ reserved "in"; e <- pLExp+ return (LLet x v e)+ <|> do lchar '\\'; xs <- sepBy (iName []) (lchar ',')+ symbol "=>"+ e <- pLExp+ return (LLam xs e)+ <|> do reserved "foreign"; l <- pLang; t <- pType+ fname <- strlit+ lchar '('+ fargs <- sepBy (do t' <- pType; e <- pLExp; return (t', e)) (lchar ',')+ lchar ')'+ return (LForeign l t fname fargs)+ <|> pCase+ <|> do x <- iName []+ return (LV (Glob x))+ +pLang = do reserved "C"; return LANG_C++pType = do reserved "Int"; return FInt+ <|> do reserved "Float"; return FDouble+ <|> do reserved "String"; return FString+ <|> do reserved "Unit"; return FUnit+ <|> do reserved "Ptr"; return FPtr+ <|> do reserved "Any"; return FAny++pCase :: LParser LExp+pCase = do reserved "case"; e <- pLExp; reserved "of"+ lchar '{'+ alts <- sepBy1 pAlt (lchar '|')+ lchar '}'+ return (LCase e alts)++pCast :: LParser LExp+pCast = do reserved "FloatString"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LFloatStr [e])+ <|> do reserved "StringFloat"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LStrFloat [e])+ <|> do reserved "FloatInt"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LFloatInt [e])+ <|> do reserved "IntFloat"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LIntFloat [e])+ <|> do reserved "StringInt"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LStrInt [e])+ <|> do reserved "IntString"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LIntStr [e])+ <|> do reserved "BigInt"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LBigInt [e])+ <|> do reserved "IntBig"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LIntBig [e])+ <|> do reserved "BigString"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LBigStr [e])+ <|> do reserved "StringBig"; lchar '('; e <- pLExp; lchar ')'+ return (LOp LStrBig [e])++pPrim :: LParser LExp+pPrim = do reserved "StrEq"; lchar '(';+ e <- pLExp; lchar ',';+ e' <- pLExp; lchar ')'; + return (LOp LStrEq [e, e'])+ <|> do reserved "StrLt"; lchar '('+ e <- pLExp; lchar ','; e' <- pLExp; + lchar ')'+ return (LOp LStrLt [e, e'])+ <|> do reserved "StrLen"; lchar '('; e <- pLExp; lchar ')';+ return (LOp LStrLen [e])+ <|> do reserved "ReadString"; lchar '('; e <- pLExp; lchar ')';+ return (LOp LReadStr [e])+ <|> do reserved "WriteString"; lchar '(';+ e <- pLExp; lchar ')'+ return (LOp LPrintStr [e])+ <|> do reserved "WriteInt"; lchar '('; + e <- pLExp; lchar ')';+ return (LOp LPrintNum [e])+ <|> do reserved "lazy"; lchar '(';+ e <- pLExp; lchar ')';+ return (LLazyExp e)+ <|> do reserved "StrHead"; lchar '('; e <- pLExp; lchar ')';+ return (LOp LStrHead [e])+ <|> do reserved "StrTail"; lchar '('; e <- pLExp; lchar ')';+ return (LOp LStrTail [e])+ <|> do reserved "StrRev"; lchar '('; e <- pLExp; lchar ')';+ return (LOp LStrRev [e])+ <|> do reserved "StrCons"; lchar '('; x <- pLExp; lchar ','; + xs <- pLExp; lchar ')';+ return (LOp LStrCons [x, xs])+ <|> do reserved "StrIndex"; lchar '('; x <- pLExp; lchar ','; + i <- pLExp; lchar ')';+ return (LOp LStrIndex [x, i])++pAlt :: LParser LAlt+pAlt = try (do x <- iName []+ lchar '('; args <- sepBy1 (iName []) (lchar ','); lchar ')'+ symbol "=>"+ rhs <- pLExp+ return (LConCase (-1) x args rhs))+ <|> do x <- iName [];+ symbol "=>"+ rhs <- pLExp+ return (LConCase (-1) x [] rhs)+ <|> do c <- natural+ symbol "=>"+ rhs <- pLExp+ return (LConstCase (I (fromInteger c)) rhs)+ <|> do symbol "_"+ symbol "=>"+ rhs <- pLExp+ return (LDefaultCase rhs)+++pLConst :: LParser LExp+pLConst = try (do f <- float; return $ LConst (Fl f))+ <|> try (do i <- natural; lchar ':'; return $ LConst (BI i)) + <|> try (do i <- natural; return $ LConst (I (fromInteger i))) + <|> try (do s <- strlit; return $ LConst (Str s))+ <|> try (do c <- chlit; return $ LConst (Ch c))+
+ src/IRTS/Lang.hs view
@@ -0,0 +1,193 @@+module IRTS.Lang where++import Core.TT+import Control.Monad.State hiding(lift)+import Data.List+import Debug.Trace++data LVar = Loc Int | Glob Name+ deriving (Show, Eq)++data LExp = LV LVar+ | LApp Bool LExp [LExp] -- True = tail call+ | LLazyApp Name [LExp] -- True = tail call+ | LLazyExp LExp+ | LForce LExp -- make sure Exp is evaluted+ | LLet Name LExp LExp -- name just for pretty printing+ | LLam [Name] LExp -- lambda, lifted out before compiling+ | LCon Int Name [LExp]+ | LCase LExp [LAlt]+ | LConst Const+ | LForeign FLang FType String [(FType, LExp)]+ | LOp PrimFn [LExp]+ | LError String+ deriving Eq++data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq | LLt | LLe | LGt | LGe+ | LFPlus | LFMinus | LFTimes | LFDiv | LFEq | LFLt | LFLe | LFGt | LFGe+ | LBPlus | LBMinus | LBTimes | LBDiv | LBEq | LBLt | LBLe | LBGt | LBGe+ | LStrConcat | LStrLt | LStrEq | LStrLen+ | LIntFloat | LFloatInt | LIntStr | LStrInt | LFloatStr | LStrFloat+ | LIntBig | LBigInt | LStrBig | LBigStr+ | LPrintNum | LPrintStr | LReadStr++ | LFExp | LFLog | LFSin | LFCos | LFTan | LFASin | LFACos | LFATan+ | LFSqrt | LFFloor | LFCeil++ | LStrHead | LStrTail | LStrCons | LStrIndex | LStrRev+ | LStdIn | LStdOut | LStdErr+ | LNoOp+ deriving (Show, Eq)++-- Supported target languages for foreign calls++data FLang = LANG_C+ deriving (Show, Eq)++data FType = FInt | FChar | FString | FUnit | FPtr | FDouble | FAny+ deriving (Show, Eq)++data LAlt = LConCase Int Name [Name] LExp+ | LConstCase Const LExp+ | LDefaultCase LExp+ deriving (Show, Eq)++data LDecl = LFun Name [Name] LExp -- name, arg names, definition+ | LConstructor Name Int Int -- constructor name, tag, arity+ deriving (Show, Eq)++type LDefs = Ctxt LDecl++addTags :: Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])+addTags i ds = tag i ds []+ where tag i ((n, LConstructor n' t a) : as) acc+ = tag (i + 1) as ((n, LConstructor n' i a) : acc) + tag i (x : as) acc = tag i as (x : acc)+ tag i [] acc = (i, reverse acc)++data LiftState = LS Name Int [(Name, LDecl)]++lname (NS n x) i = NS (lname n i) x+lname (UN n) i = MN i n+lname x i = MN i (show x)++liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]+liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs++lambdaLift :: Name -> LDecl -> [(Name, LDecl)]+lambdaLift n (LFun _ args e) + = let (e', (LS _ _ decls)) = runState (lift args e) (LS n 0 []) in+ (n, LFun n args e') : decls+lambdaLift n x = [(n, x)]++getNextName :: State LiftState Name+getNextName = do LS n i ds <- get+ put (LS n (i + 1) ds)+ return (lname n i)++addFn :: Name -> LDecl -> State LiftState ()+addFn fn d = do LS n i ds <- get+ put (LS n i ((fn, d) : ds))++lift :: [Name] -> LExp -> State LiftState LExp+lift env (LV v) = return (LV v) -- Lifting happens before these can exist...+lift env (LApp tc (LV (Glob n)) args) = do args' <- mapM (lift env) args+ return (LApp tc (LV (Glob n)) args')+lift env (LApp tc f args) = do f' <- lift env f+ fn <- getNextName+ addFn fn (LFun fn env f')+ args' <- mapM (lift env) args+ return (LApp tc (LV (Glob fn)) (map (LV . Glob) env ++ args'))+lift env (LLazyApp n args) = do args' <- mapM (lift env) args+ return (LLazyApp n args')+lift env (LLazyExp (LConst c)) = return (LConst c)+lift env (LLazyExp e) = do e' <- lift env e+ let usedArgs = nub $ usedIn env e'+ fn <- getNextName+ addFn fn (LFun fn usedArgs e')+ return (LLazyApp fn (map (LV . Glob) usedArgs))+lift env (LForce e) = do e' <- lift env e+ return (LForce e') +lift env (LLet n v e) = do v' <- lift env v+ e' <- lift (env ++ [n]) e+ return (LLet n v' e')+lift env (LLam args e) = do e' <- lift (env ++ args) e+ let usedArgs = nub $ usedIn env e'+ fn <- getNextName+ addFn fn (LFun fn (usedArgs ++ args) e')+ return (LApp False (LV (Glob fn)) (map (LV . Glob) usedArgs))+lift env (LCon i n args) = do args' <- mapM (lift env) args+ return (LCon i n args')+lift env (LCase e alts) = do alts' <- mapM liftA alts+ e' <- lift env e+ return (LCase e' alts')+ where+ liftA (LConCase i n args e) = do e' <- lift (env ++ args) e+ return (LConCase i n args e')+ liftA (LConstCase c e) = do e' <- lift env e+ return (LConstCase c e')+ liftA (LDefaultCase e) = do e' <- lift env e+ return (LDefaultCase e')+lift env (LConst c) = return (LConst c)+lift env (LForeign l t s args) = do args' <- mapM (liftF env) args+ return (LForeign l t s args')+ where+ liftF env (t, e) = do e' <- lift env e+ return (t, e')+lift env (LOp f args) = do args' <- mapM (lift env) args+ return (LOp f args')+lift env (LError str) = return $ LError str+++-- Return variables in list which are used in the expression++usedArg env n | n `elem` env = [n]+ | otherwise = []++usedIn :: [Name] -> LExp -> [Name]+usedIn env (LV (Glob n)) = usedArg env n +usedIn env (LApp _ e args) = usedIn env e ++ concatMap (usedIn env) args +usedIn env (LLazyApp n args) = concatMap (usedIn env) args ++ usedArg env n+usedIn env (LLazyExp e) = usedIn env e+usedIn env (LForce e) = usedIn env e+usedIn env (LLet n v e) = usedIn env v ++ usedIn (env \\ [n]) e+usedIn env (LLam ns e) = usedIn (env \\ ns) e+usedIn env (LCon i n args) = concatMap (usedIn env) args+usedIn env (LCase e alts) = concatMap (usedInA env) alts+ where usedInA env (LConCase i n ns e) = usedIn env e+ usedInA env (LConstCase c e) = usedIn env e+ usedInA env (LDefaultCase e) = usedIn env e+usedIn env (LForeign _ _ _ args) = concatMap (usedIn env) (map snd args)+usedIn env (LOp f args) = concatMap (usedIn env) args+usedIn env _ = []++instance Show LExp where+ show e = show' [] e where+ show' env (LV (Loc i)) = env!!i+ show' env (LV (Glob n)) = show n+ show' env (LApp _ e args) = show' env e ++ "(" +++ showSep ", " (map (show' env) args) ++")"+ show' env (LLazyExp e) = "%lazy(" ++ show' env e ++ ")" + show' env (LForce e) = "%force(" ++ show' env e ++ ")"+ show' env (LLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " +++ show' (env ++ [show n]) e+ show' env (LLam args e) = "\\ " ++ showSep "," (map show args) ++ " => " +++ show' (env ++ (map show args)) e+ show' env (LCon i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"+ show' env (LCase e alts) = "case " ++ show' env e ++ " of {\n\t" +++ showSep "\n\t| " (map (showAlt env) alts)+ show' env (LConst c) = show c+ show' env (LForeign lang ty n args)+ = "foreign " ++ n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"+ show' env (LOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"+ show' env (LError str) = "error " ++ show str++ showAlt env (LConCase _ n args e) + = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "+ ++ show' env e+ showAlt env (LConstCase c e) = show c ++ " => " ++ show' env e+ showAlt env (LDefaultCase e) = "_ => " ++ show' env e++++
+ src/IRTS/Simplified.hs view
@@ -0,0 +1,190 @@+module IRTS.Simplified where++import IRTS.Lang+import Core.TT+import Data.Maybe+import Control.Monad.State++-- Simplified expressions, where functions/constructors can only be applied +-- to variables++data SExp = SV LVar+ | SApp Bool Name [LVar]+ | SLet LVar SExp SExp+ | SCon Int Name [LVar]+ | SCase LVar [SAlt]+ | SConst Const+ | SForeign FLang FType String [(FType, LVar)]+ | SOp PrimFn [LVar]+ | SError String+ deriving Show++data SAlt = SConCase Int Int Name [Name] SExp+ | SConstCase Const SExp+ | SDefaultCase SExp+ deriving Show++data SDecl = SFun Name [Name] Int SExp+ deriving Show++hvar :: State (LDefs, Int) Int+hvar = do (l, h) <- get+ put (l, h + 1)+ return h++ldefs :: State (LDefs, Int) LDefs+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)) + = do ctxt <- ldefs+ case lookupCtxt Nothing x ctxt of+ [LConstructor _ t 0] -> return $ SCon t x []+ _ -> return $ SV (Glob x)+simplify tl (LApp tc (LV (Glob n)) args) + = do args' <- mapM sVar args+ mkapp (SApp (tl || tc) n) args'+simplify tl (LForeign 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+ 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+ 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+ mkapp (SOp p) args'+simplify tl (LError str) = return $ SError str++sVar (LV (Glob x))+ = do ctxt <- ldefs+ case lookupCtxt Nothing x ctxt of+ [LConstructor _ t 0] -> sVar (LCon t x [])+ _ -> return (Glob x, Nothing)+sVar (LV x) = return (x, Nothing)+sVar e = do e' <- simplify False e+ i <- hvar+ return (Glob (MN i "R"), Just e')++mkapp f args = mkapp' f args [] where+ mkapp' f [] args = return $ f (reverse args)+ mkapp' f ((x, Nothing) : xs) args = mkapp' f xs (x : args)+ mkapp' f ((x, Just e) : xs) args + = do sc <- mkapp' f xs (x : args)+ return (SLet x e sc)++mkfapp f args = mkapp' f args [] where+ mkapp' f [] args = return $ f (reverse args)+ mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)+ mkapp' f ((ty, (x, Just e)) : xs) args + = 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+ return (SConCase (-1) i n args e')+sAlt tl (LConstCase c e) = do e' <- simplify tl e+ return (SConstCase c e')+sAlt tl (LDefaultCase e) = do e' <- simplify tl e+ return (SDefaultCase e')++checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, SDecl)]+checkDefs ctxt [] = return []+checkDefs ctxt (con@(n, LConstructor _ _ _) : xs) + = do xs' <- checkDefs ctxt xs+ return xs'+checkDefs ctxt ((n, LFun 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+ return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')++lvar v = do i <- get+ put (max i v)++scopecheck :: LDefs -> [(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] ->+ if True -- ar == 0 + then return (SCon i n [])+ else fail $ "Codegen error: Constructor " ++ show n +++ " has arity " ++ show ar+ [_] -> return (SV (Glob n))+ [] -> fail $ "Codegen error: No such variable " ++ show n+ sc env (SApp tc f args)+ = do args' <- mapM (scVar env) args+ case lookupCtxt Nothing f ctxt of+ [LConstructor n tag ar] ->+ if True -- (ar == length args)+ then return $ SCon tag n args'+ else fail $ "Codegen error: Constructor " ++ show f ++ + " has arity " ++ show ar+ [_] -> return $ SApp tc f args'+ [] -> fail $ "Codegen error: No such variable " ++ show f+ sc env (SForeign l ty f args)+ = do args' <- mapM (\ (t, a) -> do a' <- scVar env a+ return (t, a')) args+ return $ SForeign l ty f args'+ sc env (SCon tag f args)+ = do args' <- mapM (scVar env) args+ case lookupCtxt Nothing f ctxt of+ [LConstructor n tag ar] ->+ if True -- (ar == length args)+ then return $ SCon tag n args'+ else fail $ "Codegen error: Constructor " ++ show f ++ + " has arity " ++ show ar+ _ -> fail $ "Codegen error: No such constructor " ++ show f+ sc env (SCase e alts)+ = do e' <- scVar env e+ alts' <- mapM (scalt env) alts+ return (SCase e' alts')+ sc env (SLet (Glob n) v e)+ = do let env' = env ++ [(n, length env)]+ v' <- sc env v+ n' <- scVar env' (Glob n)+ e' <- sc env' e+ return (SLet n' v' e')+ sc env (SOp prim args)+ = do args' <- mapM (scVar env) args+ return (SOp prim args')+ sc env x = return x++ scVar env (Glob n) =+ 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] ->+ fail $ "Codegen error : can't pass constructor here"+ [_] -> return (Glob n)+ [] -> fail $ "Codegen error: No such variable " ++ show n+ scVar _ x = return x++ 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] -> + if True -- (length args == ar) + then return i+ else fail $ "Codegen error: Constructor " ++ show n +++ " has arity " ++ show ar+ _ -> fail $ "Codegen error: No constructor " ++ show n+ e' <- sc env' e+ return (SConCase (length env) tag n args e')+ scalt env (SConstCase c e) = do e' <- sc env e+ return (SConstCase c e')+ scalt env (SDefaultCase e) = do e' <- sc env e+ return (SDefaultCase e')+
src/Idris/AbsSyntax.hs view
@@ -1,13 +1,16 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor, TypeSynonymInstances, PatternGuards #-} -module Idris.AbsSyntax where+module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where import Core.TT import Core.Evaluate import Core.Elaborate hiding (Tactic(..)) import Core.Typecheck+import Idris.AbsSyntaxTree +import Paths_idris+ import System.Console.Haskeline import Control.Monad.State@@ -18,94 +21,9 @@ import Debug.Trace -import qualified Epic.Epic as E- import Util.Pretty -data IOption = IOption { opt_logLevel :: Int,- opt_typecase :: Bool,- opt_typeintype :: Bool,- opt_coverage :: Bool,- opt_showimp :: Bool,- opt_repl :: Bool,- opt_verbose :: Bool- }- deriving (Show, Eq) -defaultOpts = IOption 0 False False True False True True---- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e--- without typechecking).--- This will include all the functions and data declarations, plus fixity declarations--- and syntax macros.--data IState = IState { tt_ctxt :: Context,- idris_constraints :: [(UConstraint, FC)],- idris_infixes :: [FixDecl],- idris_implicits :: Ctxt [PArg],- idris_statics :: Ctxt [Bool],- idris_classes :: Ctxt ClassInfo,- idris_dsls :: Ctxt DSL,- idris_optimisation :: Ctxt OptInfo, - idris_datatypes :: Ctxt TypeInfo,- idris_patdefs :: Ctxt [(Term, Term)], -- not exported- idris_flags :: Ctxt [FnOpt],- idris_callgraph :: Ctxt [Name],- idris_totcheck :: [(FC, Name)],- idris_log :: String,- idris_options :: IOption,- idris_name :: Int,- idris_metavars :: [Name],- syntax_rules :: [Syntax],- syntax_keywords :: [String],- imported :: [FilePath],- idris_prims :: [(Name, ([E.Name], E.Term))],- idris_objs :: [FilePath],- idris_libs :: [String],- idris_hdrs :: [String],- last_proof :: Maybe (Name, [String]),- errLine :: Maybe Int,- lastParse :: Maybe Name, - indent_stack :: [Int],- brace_stack :: [Maybe Int],- hide_list :: [(Name, Maybe Accessibility)],- default_access :: Accessibility,- ibc_write :: [IBCWrite],- compiled_so :: Maybe String- }- --- information that needs writing for the current module's .ibc file-data IBCWrite = IBCFix FixDecl- | IBCImp Name- | IBCStatic Name- | IBCClass Name- | IBCInstance Bool Name Name- | IBCDSL Name- | IBCData Name- | IBCOpt Name- | IBCSyntax Syntax- | IBCKeyword String- | IBCImport FilePath- | IBCObj FilePath- | IBCLib String- | IBCHeader String- | IBCAccess Name Accessibility- | IBCTotal Name Totality- | IBCFlags Name [FnOpt]- | IBCCG Name- | IBCDef Name -- i.e. main context- deriving Show--idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext- emptyContext emptyContext emptyContext emptyContext - emptyContext emptyContext- [] "" defaultOpts 6 [] [] [] [] [] [] [] [] - Nothing Nothing Nothing [] [] [] Hidden [] Nothing---- The monad for the main REPL - reading and processing files and updating --- global state (hence the IO inner monad).-type Idris = StateT IState (InputT IO)- getContext :: Idris Context getContext = do i <- get; return (tt_ctxt i) @@ -153,6 +71,9 @@ addToCG n ns = do i <- get put (i { idris_callgraph = addDef n ns (idris_callgraph i) }) +addToCalledG :: Name -> [Name] -> Idris ()+addToCalledG n ns = return () -- TODO+ -- Add a class instance function. Dodgy hack: Put integer instances first in the -- list so they are resolved by default. @@ -277,6 +198,16 @@ logLevel = do i <- get return (opt_logLevel (idris_options i)) +setErrContext :: Bool -> Idris ()+setErrContext t = do i <- get+ let opts = idris_options i+ let opt' = opts { opt_errContext = t }+ put (i { idris_options = opt' })++errContext :: Idris Bool+errContext = do i <- get+ return (opt_errContext (idris_options i))+ useREPL :: Idris Bool useREPL = do i <- get return (opt_repl (idris_options i))@@ -317,6 +248,26 @@ let opt' = opts { opt_coverage = t } put (i { idris_options = opt' }) +setIBCSubDir :: FilePath -> Idris ()+setIBCSubDir fp = do i <- get+ let opts = idris_options i+ let opt' = opts { opt_ibcsubdir = fp }+ put (i { idris_options = opt' })++valIBCSubDir :: IState -> Idris FilePath+valIBCSubDir i = return (opt_ibcsubdir (idris_options i))++setImportDirs :: [FilePath] -> Idris ()+setImportDirs fps = do i <- get+ let opts = idris_options i+ let opt' = opts { opt_importdirs = fps }+ 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]))+ impShow :: Idris Bool impShow = do i <- get return (opt_showimp (idris_options i))@@ -349,826 +300,7 @@ let opt' = opts { opt_typecase = t } put (i { idris_options = opt' }) --- Commands in the REPL -data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name- | Reload | Edit- | Compile String | Execute | ExecVal PTerm- | Metavars | Prove Name | AddProof | Universes- | TTShell - | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name | Info Name- | NOP---- Parsed declarations--data Fixity = Infixl { prec :: Int } - | Infixr { prec :: Int }- | InfixN { prec :: Int } - | PrefixN { prec :: Int }- deriving Eq-{-! -deriving instance Binary Fixity -!-}--instance Show Fixity where- show (Infixl i) = "infixl " ++ show i- show (Infixr i) = "infixr " ++ show i- show (InfixN i) = "infix " ++ show i- show (PrefixN i) = "prefix " ++ show i--data FixDecl = Fix Fixity String - deriving (Show, Eq)-{-! -deriving instance Binary FixDecl -!-}--instance Ord FixDecl where- compare (Fix x _) (Fix y _) = compare (prec x) (prec y)---data Static = Static | Dynamic- deriving (Show, Eq)-{-! -deriving instance Binary Static -!-}---- Mark bindings with their explicitness, and laziness-data Plicity = Imp { plazy :: Bool,- pstatic :: Static }- | Exp { plazy :: Bool,- pstatic :: Static }- | Constraint { plazy :: Bool,- pstatic :: Static }- | TacImp { plazy :: Bool,- pstatic :: Static,- pscript :: PTerm }- deriving (Show, Eq)--{-!-deriving instance Binary Plicity -!-}--impl = Imp False Dynamic-expl = Exp False Dynamic-constraint = Constraint False Dynamic-tacimpl = TacImp False Dynamic--data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen- | Specialise [Name] -- specialise it, freeze these names- deriving (Show, Eq)-{-!-deriving instance Binary FnOpt-!-}--type FnOpts = [FnOpt]--inlinable :: FnOpts -> Bool-inlinable = elem Inlinable--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- | PData SyntaxInfo FC (PData' t) -- data declaration- | PParams FC [(Name, t)] [PDecl' t] -- params block- | PNamespace String [PDecl' t] -- new namespace- | PRecord SyntaxInfo FC Name t Name t -- record declaration- | PClass SyntaxInfo FC - [t] -- constraints- Name- [(Name, t)] -- parameters- [PDecl' t] -- declarations- | PInstance SyntaxInfo FC [t] -- constraints- Name -- class- [t] -- parameters- t -- full instance type- [PDecl' t]- | PDSL Name (DSL' t)- | PSyntax FC Syntax- | PDirective (Idris ())- deriving Functor--data PClause' t = PClause FC Name t [t] t [PDecl' t]- | PWith FC Name t [t] t [PDecl' t]- | PClauseR FC [t] t [PDecl' t]- | PWithR FC [t] t [PDecl' t]- deriving Functor--data PData' t = PDatadecl { d_name :: Name,- d_tcon :: t,- d_cons :: [(Name, t, FC)] }- deriving Functor---- Handy to get a free function for applying PTerm -> PTerm functions--- across a program, by deriving Functor--type PDecl = PDecl' PTerm-type PData = PData' PTerm-type PClause = PClause' PTerm ---- get all the names declared in a decl--declared :: PDecl -> [Name]-declared (PFix _ _ _) = []-declared (PTy _ _ _ n t) = [n]-declared (PClauses _ _ n _) = [] -- not a declaration-declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts- where fstt (a, _, _) = a-declared (PParams _ _ ds) = concatMap declared ds-declared (PNamespace _ ds) = concatMap declared ds--- declared (PImport _) = []--defined :: PDecl -> [Name]-defined (PFix _ _ _) = []-defined (PTy _ _ _ n t) = []-defined (PClauses _ _ n _) = [n] -- not a declaration-defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts- where fstt (a, _, _) = a-defined (PParams _ _ ds) = concatMap defined ds-defined (PNamespace _ ds) = concatMap defined ds--- declared (PImport _) = []--updateN :: [(Name, Name)] -> Name -> Name-updateN ns n | Just n' <- lookup n ns = n'-updateN _ n = n--updateNs :: [(Name, Name)] -> PTerm -> PTerm-updateNs [] t = t-updateNs ns t = mapPT updateRef t- where updateRef (PRef fc f) = PRef fc (updateN ns f) - updateRef t = t---- updateDNs :: [(Name, Name)] -> PDecl -> PDecl--- updateDNs [] t = t--- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t--- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)--- where updateCNs ns (PClause n l ts r ds) --- = PClause (updateN ns n) (fmap (updateNs ns) l)--- (map (fmap (updateNs ns)) ts)--- (fmap (updateNs ns) r)--- (map (updateDNs ns) ds)--- updateDNs ns c = c---- High level language terms--data PTerm = PQuote Raw- | PRef FC Name- | PLam Name PTerm PTerm- | PPi Plicity Name PTerm PTerm- | PLet Name PTerm PTerm PTerm - | PTyped PTerm PTerm -- term with explicit type- | PApp FC PTerm [PArg]- | PCase FC PTerm [(PTerm, PTerm)]- | PTrue FC- | PFalse FC- | PRefl FC- | PResolveTC FC- | PEq FC PTerm PTerm- | PPair FC PTerm PTerm- | PDPair FC PTerm PTerm PTerm- | PAlternative [PTerm]- | PHidden PTerm -- irrelevant or hidden pattern- | PSet- | PConstant Const- | Placeholder- | PDoBlock [PDo]- | PIdiom FC PTerm- | PReturn FC- | PMetavar Name- | PProof [PTactic]- | PTactics [PTactic] -- as PProof, but no auto solving- | PElabError Err -- error to report on elaboration- | PImpossible -- special case for declaring when an LHS can't typecheck- deriving Eq-{-! -deriving instance Binary PTerm -!-}--mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm-mapPT f t = f (mpt t) where- mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)- mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)- mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)- mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)- mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)- mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)- mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)- mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)- mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)- mpt (PAlternative as) = PAlternative (map (mapPT f) as)- mpt (PHidden t) = PHidden (mapPT f t)- mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)- mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)- mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)- mpt x = x---data PTactic' t = Intro [Name] | Intros | Focus Name- | Refine Name [Bool] | Rewrite t | LetTac Name t- | Exact t | Compute | Trivial- | Solve- | Attack- | ProofState | ProofTerm | Undo- | Try (PTactic' t) (PTactic' t)- | TSeq (PTactic' t) (PTactic' t)- | Qed | Abandon- deriving (Show, Eq, Functor)-{-! -deriving instance Binary PTactic' -!-}--instance Sized a => Sized (PTactic' a) where- size (Intro nms) = 1 + size nms- size Intros = 1- size (Focus nm) = 1 + size nm- size (Refine nm bs) = 1 + size nm + length bs- size (Rewrite t) = 1 + size t- size (LetTac nm t) = 1 + size nm + size t- size (Exact t) = 1 + size t- size Compute = 1- size Trivial = 1- size Solve = 1- size Attack = 1- size ProofState = 1- size ProofTerm = 1- size Undo = 1- size (Try l r) = 1 + size l + size r- size (TSeq l r) = 1 + size l + size r- size Qed = 1- size Abandon = 1--type PTactic = PTactic' PTerm--data PDo' t = DoExp FC t- | DoBind FC Name t- | DoBindP FC t t- | DoLet FC Name t t- | DoLetP FC t t- deriving (Eq, Functor)-{-! -deriving instance Binary PDo' -!-}--instance Sized a => Sized (PDo' a) where- size (DoExp fc t) = 1 + size fc + size t- size (DoBind fc nm t) = 1 + size fc + size nm + size t- size (DoBindP fc l r) = 1 + size fc + size l + size r- size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r- size (DoLetP fc l r) = 1 + size fc + size l + size r--type PDo = PDo' PTerm---- The priority gives a hint as to elaboration order. Best to elaborate--- things early which will help give a more concrete type to other--- variables, e.g. a before (interpTy a).--data PArg' t = PImp { priority :: Int, - lazyarg :: Bool, pname :: Name, getTm :: t }- | PExp { priority :: Int,- lazyarg :: Bool, getTm :: t }- | PConstraint { priority :: Int,- lazyarg :: Bool, getTm :: t }- | PTacImplicit { priority :: Int,- lazyarg :: Bool, pname :: Name, - getScript :: t,- getTm :: t }- deriving (Show, Eq, Functor)--instance Sized a => Sized (PArg' a) where- size (PImp p l nm trm) = 1 + size nm + size trm- size (PExp p l trm) = 1 + size trm- size (PConstraint p l trm) = 1 + size trm- size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm--{-! -deriving instance Binary PArg' -!-}--pimp = PImp 0 True-pexp = PExp 0 False-pconst = PConstraint 0 False-ptacimp = PTacImplicit 0 True--type PArg = PArg' PTerm---- Type class data--data ClassInfo = CI { instanceName :: Name,- class_methods :: [(Name, (FnOpts, PTerm))],- class_defaults :: [(Name, Name)], -- method name -> default impl- class_params :: [Name],- class_instances :: [Name] }- deriving Show-{-! -deriving instance Binary ClassInfo -!-}--data OptInfo = Optimise { collapsible :: Bool,- forceable :: [Int], -- argument positions- recursive :: [Int] }- deriving Show-{-! -deriving instance Binary OptInfo -!-}---data TypeInfo = TI { con_names :: [Name] }- deriving Show-{-!-deriving instance Binary TypeInfo-!-}---- Syntactic sugar info --data DSL' t = DSL { dsl_bind :: t,- dsl_return :: t,- dsl_apply :: t,- dsl_pure :: t,- dsl_var :: Maybe t,- index_first :: Maybe t,- index_next :: Maybe t,- dsl_lambda :: Maybe t,- dsl_let :: Maybe t- }- deriving (Show, Functor)-{-!-deriving instance Binary DSL'-!-}--type DSL = DSL' PTerm--data SynContext = PatternSyntax | TermSyntax | AnySyntax- deriving Show-{-! -deriving instance Binary SynContext -!-}--data Syntax = Rule [SSymbol] PTerm SynContext- deriving Show-{-! -deriving instance Binary Syntax -!-}--data SSymbol = Keyword Name- | Symbol String- | Expr Name- | SimpleExpr Name- deriving Show-{-! -deriving instance Binary SSymbol -!-}--initDSL = DSL (PRef f (UN ">>=")) - (PRef f (UN "return"))- (PRef f (UN "<$>"))- (PRef f (UN "pure"))- Nothing- Nothing- Nothing- Nothing- Nothing- where f = FC "(builtin)" 0--data SyntaxInfo = Syn { using :: [(Name, PTerm)],- syn_params :: [(Name, PTerm)],- syn_namespace :: [String],- no_imp :: [Name],- decoration :: Name -> Name,- inPattern :: Bool,- dsl_info :: DSL }- deriving Show--defaultSyntax = Syn [] [] [] [] id False initDSL--expandNS :: SyntaxInfo -> Name -> Name-expandNS syn n@(NS _ _) = n-expandNS syn n = case syn_namespace syn of- [] -> n- xs -> NS n xs------ Pretty printing declarations and terms--instance Show PTerm where- show tm = showImp False tm--instance Pretty PTerm where- pretty = prettyImp False--instance Show PDecl where- show d = showDeclImp False d--instance Show PClause where- show c = showCImp True c--instance Show PData where- show d = showDImp False d--showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops-showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty-showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)-showDeclImp _ (PData _ _ d) = show d--showCImp :: Bool -> PClause -> String-showCImp impl (PClause _ n l ws r w) - = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r- ++ " where " ++ show w - where- showWs [] = ""- showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs-showCImp impl (PWith _ n l ws r w) - = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r- ++ " { " ++ show w ++ " } " - where- showWs [] = ""- showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs---showDImp :: Bool -> PData -> String-showDImp impl (PDatadecl n ty cons) - = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"- ++ showSep "\n\t| " - (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)--getImps :: [PArg] -> [(Name, PTerm)]-getImps [] = []-getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs-getImps (_ : xs) = getImps xs--getExps :: [PArg] -> [PTerm]-getExps [] = []-getExps (PExp _ _ tm : xs) = tm : getExps xs-getExps (_ : xs) = getExps xs--getConsts :: [PArg] -> [PTerm]-getConsts [] = []-getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs-getConsts (_ : xs) = getConsts xs--getAll :: [PArg] -> [PTerm]-getAll = map getTm --prettyImp :: Bool -> PTerm -> Doc-prettyImp impl = prettySe 10- where- prettySe p (PQuote r) =- if size r > breakingSize then- text "![" $$ pretty r <> text "]"- else- text "![" <> pretty r <> text "]"- prettySe p (PRef fc n) =- if impl then- pretty n- else- prettyBasic n- where- prettyBasic n@(UN _) = pretty n- prettyBasic (MN _ s) = text s- prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n- prettySe p (PLam n ty sc) =- bracket p 2 $- if size sc > breakingSize then- text "λ" <> pretty n <+> text "=>" $+$ pretty sc- else- text "λ" <> pretty n <+> text "=>" <+> pretty sc- prettySe p (PLet n ty v sc) =- bracket p 2 $- if size sc > breakingSize then- text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$- nest nestingSize (prettySe 10 sc)- else- text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>- prettySe 10 sc- prettySe p (PPi (Exp l s) n ty sc)- | n `elem` allNamesIn sc || impl =- let open = if l then text "|" <> lparen else lparen in- bracket p 2 $- if size sc > breakingSize then- open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>- st <+> text "->" $+$ prettySe 10 sc- else- open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>- st <+> text "->" <+> prettySe 10 sc- | otherwise =- bracket p 2 $- if size sc > breakingSize then- prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc- else- prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc- where- st =- case s of- Static -> text "[static]"- _ -> empty- prettySe p (PPi (Imp l s) n ty sc)- | impl =- let open = if l then text "|" <> lbrace else lbrace in- bracket p 2 $- if size sc > breakingSize then- open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>- st <+> text "->" <+> prettySe 10 sc- else- open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>- st <+> text "->" <+> prettySe 10 sc- | otherwise = prettySe 10 sc- where- st =- case s of- Static -> text $ "[static]"- _ -> empty- prettySe p (PPi (Constraint _ _) n ty sc) =- bracket p 2 $- if size sc > breakingSize then- prettySe 10 ty <+> text "=>" <+> prettySe 10 sc- else- prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc- prettySe p (PPi (TacImp _ _ s) n ty sc) =- bracket p 2 $- if size sc > breakingSize then- lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>- rbrace <+> text "->" $+$ prettySe 10 sc- else- lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>- rbrace <+> text "->" <+> prettySe 10 sc- prettySe p (PApp _ (PRef _ f) [])- | not impl = pretty f- prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)- | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =- let [l, r] = getExps args in- bracket p 1 $- if size r > breakingSize then- prettySe 1 l <+> pretty op $+$ prettySe 0 r- else- prettySe 1 l <+> pretty op <+> prettySe 0 r- prettySe p (PApp _ f as) =- let args = getExps as in- bracket p 1 $- prettySe 1 f <+>- if impl then- foldl fS empty as- -- foldr (<+>) empty $ map prettyArgS as- else- foldl fSe empty args- -- foldr (<+>) empty $ map prettyArgSe args- where- fS l r =- if size r > breakingSize then- l $+$ nest nestingSize (prettyArgS r)- else- l <+> prettyArgS r-- fSe l r =- if size r > breakingSize then- l $+$ nest nestingSize (prettyArgSe r)- else- l <+> prettyArgSe r- prettySe p (PCase _ scr opts) =- text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody- where- prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts-- sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r- prettySe p (PHidden tm) = text "." <> prettySe 0 tm- prettySe p (PRefl _) = text "refl"- prettySe p (PResolveTC _) = text "resolvetc"- prettySe p (PTrue _) = text "()"- prettySe p (PFalse _) = text "_|_"- prettySe p (PEq _ l r) =- bracket p 2 $- if size r > breakingSize then- prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)- else- prettySe 10 l <+> text "=" <+> prettySe 10 r- prettySe p (PTyped l r) =- lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen- prettySe p (PPair _ l r) =- if size r > breakingSize then- lparen <> prettySe 10 l <> text "," $+$- prettySe 10 r <> rparen- else- lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen- prettySe p (PDPair _ l t r) =- if size r > breakingSize then- lparen <> prettySe 10 l <+> text "**" $+$- prettySe 10 r <> rparen- else- lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen- prettySe p (PAlternative as) =- lparen <> text "|" <> prettyAs <> text "|" <> rparen- where- prettyAs =- foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as- prettySe p PSet = text "Set"- prettySe p (PConstant c) = pretty c- -- XXX: add pretty for tactics- prettySe p (PProof ts) =- text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace- prettySe p (PTactics ts) =- text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace- prettySe p (PMetavar n) = text "?" <> pretty n- prettySe p (PReturn f) = text "return"- prettySe p PImpossible = text "impossible"- prettySe p Placeholder = text "_"- prettySe p (PDoBlock _) = text "do block pretty not implemented"- prettySe p (PElabError s) = pretty s-- prettySe p _ = text "test"-- prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)- prettyArgS (PExp _ _ tm) = prettyArgSe tm- prettyArgS (PConstraint _ _ tm) = prettyArgSc tm- prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)-- prettyArgSe arg = prettySe 0 arg- prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace- prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace- prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace-- bracket outer inner doc- | inner > outer = lparen <> doc <> rparen- | otherwise = doc- -showImp :: Bool -> PTerm -> String-showImp impl tm = se 10 tm where- se p (PQuote r) = "![" ++ show r ++ "]"- se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"- else showbasic n- where showbasic n@(UN _) = show n- showbasic (MN _ s) = s- showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n- se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ - (if impl then " : " ++ se 10 ty else "") ++ " => " - ++ se 10 sc- se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++- " in " ++ se 10 sc - se p (PPi (Exp l s) n ty sc)- | n `elem` allNamesIn sc || impl- = bracket p 2 $- if l then "|(" else "(" ++ - show n ++ " : " ++ se 10 ty ++ - ") " ++ st ++- "-> " ++ se 10 sc- | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc- where st = case s of- Static -> "[static] "- _ -> ""- se p (PPi (Imp l s) n ty sc)- | impl = bracket p 2 $ if l then "|{" else "{" ++ - show n ++ " : " ++ se 10 ty ++ - "} " ++ st ++ "-> " ++ se 10 sc- | otherwise = se 10 sc- where st = case s of- Static -> "[static] "- _ -> ""- se p (PPi (Constraint _ _) n ty sc)- = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc- se p (PPi (TacImp _ _ s) n ty sc)- = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc- se p (PApp _ (PRef _ f) [])- | not impl = show f- se p (PApp _ (PRef _ op@(UN (f:_))) args)- | length (getExps args) == 2 && not impl && not (isAlpha f) - = let [l, r] = getExps args in- bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r- se p (PApp _ f as) - = let args = getExps as in- bracket p 1 $ se 1 f ++ if impl then concatMap sArg as- else concatMap seArg args- se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)- where sc (l, r) = se 10 l ++ " => " ++ se 10 r- se p (PHidden tm) = "." ++ se 0 tm- se p (PRefl _) = "refl"- se p (PResolveTC _) = "resolvetc"- se p (PTrue _) = "()"- se p (PFalse _) = "_|_"- se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r- se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"- se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"- se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"- se p (PAlternative as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"- se p PSet = "Set"- se p (PConstant c) = show c- se p (PProof ts) = "proof { " ++ show ts ++ "}"- se p (PTactics ts) = "tactics { " ++ show ts ++ "}"- se p (PMetavar n) = "?" ++ show n- se p (PReturn f) = "return"- se p PImpossible = "impossible"- se p Placeholder = "_"- se p (PDoBlock _) = "do block show not implemented"- se p (PElabError s) = show s--- se p x = "Not implemented"-- sArg (PImp _ _ n tm) = siArg (n, tm)- sArg (PExp _ _ tm) = seArg tm- sArg (PConstraint _ _ tm) = scArg tm- sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)-- seArg arg = " " ++ se 0 arg- siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"- scArg val = " {{" ++ se 10 val ++ "}}"- stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"-- bracket outer inner str | inner > outer = "(" ++ str ++ ")"- | otherwise = str--{-- PQuote Raw- | PRef FC Name- | PLam Name PTerm PTerm- | PPi Plicity Name PTerm PTerm- | PLet Name PTerm PTerm PTerm - | PTyped PTerm PTerm -- term with explicit type- | PApp FC PTerm [PArg]- | PCase FC PTerm [(PTerm, PTerm)]- | PTrue FC- | PFalse FC- | PRefl FC- | PResolveTC FC- | PEq FC PTerm PTerm- | PPair FC PTerm PTerm- | PDPair FC PTerm PTerm PTerm- | PAlternative [PTerm]- | PHidden PTerm -- irrelevant or hidden pattern- | PSet- | PConstant Const- | Placeholder- | PDoBlock [PDo]- | PIdiom FC PTerm- | PReturn FC- | PMetavar Name- | PProof [PTactic]- | PTactics [PTactic] -- as PProof, but no auto solving- | PElabError Err -- error to report on elaboration- | PImpossible -- special case for declaring when an LHS can't typecheck--}--instance Sized PTerm where- size (PQuote rawTerm) = size rawTerm- size (PRef fc name) = size name- size (PLam name ty bdy) = 1 + size ty + size bdy- size (PPi plicity name ty bdy) = 1 + size ty + size bdy- size (PLet name ty def bdy) = 1 + size ty + size def + size bdy- size (PTyped trm ty) = 1 + size trm + size ty- size (PApp fc name args) = 1 + size args- size (PCase fc trm bdy) = 1 + size trm + size bdy- size (PTrue fc) = 1- size (PFalse fc) = 1- size (PRefl fc) = 1- size (PResolveTC fc) = 1- size (PEq fc left right) = 1 + size left + size right- size (PPair fc left right) = 1 + size left + size right- size (PDPair fs left ty right) = 1 + size left + size ty + size right- size (PAlternative alts) = 1 + size alts- size (PHidden hidden) = size hidden- size PSet = 1- size (PConstant const) = 1 + size const- size Placeholder = 1- size (PDoBlock dos) = 1 + size dos- size (PIdiom fc term) = 1 + size term- size (PReturn fc) = 1- size (PMetavar name) = 1- size (PProof tactics) = size tactics- size (PElabError err) = size err- size PImpossible = 1--allNamesIn :: PTerm -> [Name]-allNamesIn tm = nub $ ni [] tm - where- ni env (PRef _ n) - | not (n `elem` env) = [n]- ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)- ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)- ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc- ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc- ni env (PHidden tm) = ni env tm- ni env (PEq _ l r) = ni env l ++ ni env r- ni env (PTyped l r) = ni env l ++ ni env r- ni env (PPair _ l r) = ni env l ++ ni env r- ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r- ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r- ni env (PAlternative ls) = concatMap (ni env) ls- ni env _ = []--namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]-namesIn uvars ist tm = nub $ ni [] tm - where- ni env (PRef _ n) - | not (n `elem` env) - = case lookupTy Nothing n (tt_ctxt ist) of- [] -> [n]- _ -> if n `elem` (map fst uvars) then [n] else []- ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)- ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)- ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc- ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc- ni env (PEq _ l r) = ni env l ++ ni env r- ni env (PTyped l r) = ni env l ++ ni env r- ni env (PPair _ l r) = ni env l ++ ni env r- ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r- ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r- ni env (PAlternative as) = concatMap (ni env) as- ni env (PHidden tm) = ni env tm- ni env _ = []- -- For inferring types of things bi = FC "builtin" 0@@ -1276,7 +408,7 @@ en (PTyped l r) = PTyped (en l) (en r) en (PPair f l r) = PPair f (en l) (en r) en (PDPair f l t r) = PDPair f (en l) (en t) (en r)- en (PAlternative as) = PAlternative (map en as)+ en (PAlternative a as) = PAlternative a (map en as) en (PHidden t) = PHidden (en t) en (PDoBlock ds) = PDoBlock (map (fmap en) ds) en (PProof ts) = PProof (map (fmap en) ts)@@ -1352,7 +484,7 @@ pri (PTyped l r) = pri l pri (PPair _ l r) = max 1 (max (pri l) (pri r)) pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))- pri (PAlternative as) = maximum (map pri as)+ pri (PAlternative a as) = maximum (map pri as) pri (PConstant _) = 0 pri Placeholder = 1 pri _ = 3@@ -1468,7 +600,7 @@ let isn = namesIn uvars ist l ++ namesIn uvars ist t ++ namesIn uvars ist r put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))- imps top env (PAlternative as)+ imps top env (PAlternative a as) = do (decls, ns) <- get let isn = concatMap (namesIn uvars ist) as put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))@@ -1501,9 +633,9 @@ addImpl' inpat env ist ptm = ai env ptm where ai env (PRef fc f) - | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []+ | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f [] ai env (PHidden (PRef fc f))- | not (f `elem` env) = handleErr $ aiFn False ist fc f []+ | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f [] ai env (PEq fc l r) = let l' = ai env l r' = ai env r in PEq fc l' r'@@ -1517,12 +649,12 @@ t' = ai env t r' = ai env r in PDPair fc l' t' r'- ai env (PAlternative as) = let as' = map (ai env) as in- PAlternative as'+ ai env (PAlternative a as) = let as' = map (ai env) as in+ PAlternative a as' ai env (PApp fc (PRef _ f) as) | not (f `elem` env) = let as' = map (fmap (ai env)) as in- handleErr $ aiFn False ist fc f as'+ handleErr $ aiFn inpat False ist fc f as' ai env (PApp fc f as) = let f' = ai env f as' = map (fmap (ai env)) as in mkPApp fc 1 f' as'@@ -1551,18 +683,18 @@ -- if in a pattern, and there are no arguments, and there's no possible -- names with zero explicit arguments, don't add implicits. -aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm-aiFn True ist fc f []+aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm+aiFn inpat True ist fc f [] = case lookupCtxt Nothing f (idris_implicits ist) of [] -> Right $ PRef fc f alts -> if (any (all imp) alts)- then aiFn False ist fc f [] -- use it as a constructor+ then aiFn inpat False ist fc f [] -- use it as a constructor else Right $ PRef fc f where imp (PExp _ _ _) = False imp _ = True-aiFn inpat ist fc f as+aiFn inpat expat ist fc f as | f `elem` primNames = Right $ PApp fc (PRef fc f) as-aiFn inpat ist fc f as+aiFn inpat expat ist fc f as -- This is where namespaces get resolved by adding PAlternative = case lookupCtxtName Nothing f (idris_implicits ist) of [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)@@ -1570,7 +702,7 @@ then Right $ PApp fc (PRef fc f) as else Right $ mkPApp fc (length as) (PRef fc f) as alts -> Right $- PAlternative $+ PAlternative True $ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)) alts where@@ -1588,14 +720,17 @@ insertImpl (PTacImplicit p l n sc ty : ps) given = case find n given [] of Just (tm, given') -> PTacImplicit p l n sc tm : insertImpl ps given'- Nothing -> PTacImplicit p l n sc sc- : insertImpl ps given+ Nothing -> if inpat + then PTacImplicit p l n sc Placeholder : insertImpl ps given+ else PTacImplicit p l n sc sc : insertImpl ps given insertImpl expected [] = [] insertImpl _ given = given find n [] acc = Nothing find n (PImp _ _ n' t : gs) acc | n == n' = Just (t, reverse acc ++ gs)+ find n (PTacImplicit _ _ n' _ t : gs) acc + | n == n' = Just (t, reverse acc ++ gs) find n (g : gs) acc = find n gs (g : acc) mkPApp fc a f [] = f@@ -1650,7 +785,7 @@ dumpDecl (PSyntax _ syn) = "syntax " ++ show syn dumpDecl (PClass _ _ cs n ps ds) = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds-dumpDecl (PInstance _ _ cs n _ t ds) +dumpDecl (PInstance _ _ cs n _ t _ ds) = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds dumpDecl _ = "..." -- dumpDecl (PImport i) = "import " ++ i@@ -1715,10 +850,10 @@ mt <- match' t t' mr <- match' r r' return (ml ++ mt ++ mr)- match (PAlternative as) (PAlternative as') + match (PAlternative a as) (PAlternative a' as') = do ms <- zipWithM match' as as' return (concat ms)- match a@(PAlternative as) b+ match a@(PAlternative _ as) b = do let ms = zipWith match' as (repeat b) case (rights (map toEither ms)) of (x: _) -> return x@@ -1774,7 +909,7 @@ sm (PTyped x y) = PTyped (sm x) (sm y) sm (PPair f x y) = PPair f (sm x) (sm y) sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)- sm (PAlternative as) = PAlternative (map sm as)+ sm (PAlternative a as) = PAlternative a (map sm as) sm (PHidden x) = PHidden (sm x) sm x = x @@ -1789,7 +924,7 @@ sm (PTyped x y) = PTyped (sm x) (sm y) sm (PPair f x y) = PPair f (sm x) (sm y) sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)- sm (PAlternative as) = PAlternative (map sm as)+ sm (PAlternative a as) = PAlternative a (map sm as) sm (PHidden x) = PHidden (sm x) sm x = x
+ src/Idris/AbsSyntaxTree.hs view
@@ -0,0 +1,976 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,+ TypeSynonymInstances, PatternGuards #-}++module Idris.AbsSyntaxTree where++import Core.TT+import Core.Evaluate+import Core.Elaborate hiding (Tactic(..))+import Core.Typecheck+import IRTS.Lang+import Util.Pretty++import Paths_idris++import System.Console.Haskeline++import Control.Monad.State++import Data.List+import Data.Char+import Data.Either++import Debug.Trace++data IOption = IOption { opt_logLevel :: Int,+ opt_typecase :: Bool,+ opt_typeintype :: Bool,+ opt_coverage :: Bool,+ opt_showimp :: Bool,+ opt_errContext :: Bool,+ opt_repl :: Bool,+ opt_verbose :: Bool,+ opt_ibcsubdir :: FilePath,+ opt_importdirs :: [FilePath]+ }+ deriving (Show, Eq)++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).+-- This will include all the functions and data declarations, plus fixity declarations+-- and syntax macros.++data IState = IState { tt_ctxt :: Context,+ idris_constraints :: [(UConstraint, FC)],+ idris_infixes :: [FixDecl],+ idris_implicits :: Ctxt [PArg],+ idris_statics :: Ctxt [Bool],+ idris_classes :: Ctxt ClassInfo,+ idris_dsls :: Ctxt DSL,+ idris_optimisation :: Ctxt OptInfo, + idris_datatypes :: Ctxt TypeInfo,+ idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported+ idris_flags :: Ctxt [FnOpt],+ idris_callgraph :: Ctxt [Name],+ idris_calledgraph :: Ctxt [Name],+ idris_totcheck :: [(FC, Name)],+ idris_log :: String,+ idris_options :: IOption,+ idris_name :: Int,+ idris_metavars :: [Name],+ syntax_rules :: [Syntax],+ syntax_keywords :: [String],+ imported :: [FilePath],+ idris_scprims :: [(Name, (Int, PrimFn))],+ idris_objs :: [FilePath],+ idris_libs :: [String],+ idris_hdrs :: [String],+ proof_list :: [(Name, [String])],+ errLine :: Maybe Int,+ lastParse :: Maybe Name, + indent_stack :: [Int],+ brace_stack :: [Maybe Int],+ hide_list :: [(Name, Maybe Accessibility)],+ default_access :: Accessibility,+ ibc_write :: [IBCWrite],+ compiled_so :: Maybe String+ }++primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]+ +-- information that needs writing for the current module's .ibc file+data IBCWrite = IBCFix FixDecl+ | IBCImp Name+ | IBCStatic Name+ | IBCClass Name+ | IBCInstance Bool Name Name+ | IBCDSL Name+ | IBCData Name+ | IBCOpt Name+ | IBCSyntax Syntax+ | IBCKeyword String+ | IBCImport FilePath+ | IBCObj FilePath+ | IBCLib String+ | IBCHeader String+ | IBCAccess Name Accessibility+ | IBCTotal Name Totality+ | IBCFlags Name [FnOpt]+ | IBCCG Name+ | IBCDef Name -- i.e. main context+ deriving Show++idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext+ emptyContext emptyContext emptyContext emptyContext + emptyContext emptyContext emptyContext+ [] "" defaultOpts 6 [] [] [] [] [] [] [] []+ [] Nothing Nothing [] [] [] Hidden [] Nothing++-- The monad for the main REPL - reading and processing files and updating +-- global state (hence the IO inner monad).+type Idris = StateT IState (InputT IO)++-- Commands in the REPL++data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name+ | Reload | Edit+ | Compile String | Execute | ExecVal PTerm+ | NewCompile String+ | Metavars | Prove Name | AddProof | RmProof | Proofs | Universes+ | TTShell + | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name + | Info Name | DebugInfo Name+ | Search PTerm+ | SetOpt Opt | UnsetOpt Opt+ | NOP++data Opt = Filename String+ | Ver+ | Usage+ | ShowLibs+ | ShowIncs+ | NoPrelude+ | NoREPL+ | OLogging Int+ | Output String+ | NewOutput String+ | TypeCase+ | TypeInType+ | NoCoverage + | ErrContext + | ShowImpl+ | Verbose+ | IBCSubDir String+ | ImportDir String+ | BCAsm String+ | FOVM String+ deriving Eq+++-- Parsed declarations++data Fixity = Infixl { prec :: Int } + | Infixr { prec :: Int }+ | InfixN { prec :: Int } + | PrefixN { prec :: Int }+ deriving Eq+{-! +deriving instance Binary Fixity +!-}++instance Show Fixity where+ show (Infixl i) = "infixl " ++ show i+ show (Infixr i) = "infixr " ++ show i+ show (InfixN i) = "infix " ++ show i+ show (PrefixN i) = "prefix " ++ show i++data FixDecl = Fix Fixity String + deriving (Show, Eq)+{-! +deriving instance Binary FixDecl +!-}++instance Ord FixDecl where+ compare (Fix x _) (Fix y _) = compare (prec x) (prec y)+++data Static = Static | Dynamic+ deriving (Show, Eq)+{-! +deriving instance Binary Static +!-}++-- Mark bindings with their explicitness, and laziness+data Plicity = Imp { plazy :: Bool,+ pstatic :: Static }+ | Exp { plazy :: Bool,+ pstatic :: Static }+ | Constraint { plazy :: Bool,+ pstatic :: Static }+ | TacImp { plazy :: Bool,+ pstatic :: Static,+ pscript :: PTerm }+ deriving (Show, Eq)++{-!+deriving instance Binary Plicity +!-}++impl = Imp False Dynamic+expl = Exp False Dynamic+constraint = Constraint False Dynamic+tacimpl = TacImp False Dynamic++data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen+ | CExport String -- export, with a C name+ | Specialise [Name] -- specialise it, freeze these names+ deriving (Show, Eq)+{-!+deriving instance Binary FnOpt+!-}++type FnOpts = [FnOpt]++inlinable :: FnOpts -> Bool+inlinable = elem Inlinable++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+ | PData SyntaxInfo FC (PData' t) -- data declaration+ | PParams FC [(Name, t)] [PDecl' t] -- params block+ | PNamespace String [PDecl' t] -- new namespace+ | PRecord SyntaxInfo FC Name t Name t -- record declaration+ | PClass SyntaxInfo FC + [t] -- constraints+ Name+ [(Name, t)] -- parameters+ [PDecl' t] -- declarations+ | PInstance SyntaxInfo FC [t] -- constraints+ Name -- class+ [t] -- parameters+ t -- full instance type+ (Maybe Name) -- explicit name+ [PDecl' t]+ | PDSL Name (DSL' t)+ | PSyntax FC Syntax+ | PDirective (Idris ())+ deriving Functor+{-!+deriving instance Binary PDecl'+!-}++data PClause' t = PClause FC Name t [t] t [PDecl' t]+ | PWith FC Name t [t] t [PDecl' t]+ | PClauseR FC [t] t [PDecl' t]+ | PWithR FC [t] t [PDecl' t]+ deriving Functor+{-!+deriving instance Binary PClause'+!-}++data PData' t = PDatadecl { d_name :: Name,+ d_tcon :: t,+ d_cons :: [(Name, t, FC)] }+ deriving Functor+{-!+deriving instance Binary PData'+!-}++-- Handy to get a free function for applying PTerm -> PTerm functions+-- across a program, by deriving Functor++type PDecl = PDecl' PTerm+type PData = PData' PTerm+type PClause = PClause' PTerm ++-- get all the names declared in a decl++declared :: PDecl -> [Name]+declared (PFix _ _ _) = []+declared (PTy _ _ _ n t) = [n]+declared (PClauses _ _ n _) = [] -- not a declaration+declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts+ where fstt (a, _, _) = a+declared (PParams _ _ ds) = concatMap declared ds+declared (PNamespace _ ds) = concatMap declared ds+-- declared (PImport _) = []++defined :: PDecl -> [Name]+defined (PFix _ _ _) = []+defined (PTy _ _ _ n t) = []+defined (PClauses _ _ n _) = [n] -- not a declaration+defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts+ where fstt (a, _, _) = a+defined (PParams _ _ ds) = concatMap defined ds+defined (PNamespace _ ds) = concatMap defined ds+-- declared (PImport _) = []++updateN :: [(Name, Name)] -> Name -> Name+updateN ns n | Just n' <- lookup n ns = n'+updateN _ n = n++updateNs :: [(Name, Name)] -> PTerm -> PTerm+updateNs [] t = t+updateNs ns t = mapPT updateRef t+ where updateRef (PRef fc f) = PRef fc (updateN ns f) + updateRef t = t++-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl+-- updateDNs [] t = t+-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t+-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)+-- where updateCNs ns (PClause n l ts r ds) +-- = PClause (updateN ns n) (fmap (updateNs ns) l)+-- (map (fmap (updateNs ns)) ts)+-- (fmap (updateNs ns) r)+-- (map (updateDNs ns) ds)+-- updateDNs ns c = c++-- High level language terms++data PTerm = PQuote Raw+ | PRef FC Name+ | PLam Name PTerm PTerm+ | PPi Plicity Name PTerm PTerm+ | PLet Name PTerm PTerm PTerm + | PTyped PTerm PTerm -- term with explicit type+ | PApp FC PTerm [PArg]+ | PCase FC PTerm [(PTerm, PTerm)]+ | PTrue FC+ | PFalse FC+ | PRefl FC+ | PResolveTC FC+ | PEq FC PTerm PTerm+ | PPair FC PTerm PTerm+ | PDPair FC PTerm PTerm PTerm+ | PAlternative Bool [PTerm] -- True if only one may work+ | PHidden PTerm -- irrelevant or hidden pattern+ | PSet+ | PConstant Const+ | Placeholder+ | PDoBlock [PDo]+ | PIdiom FC PTerm+ | PReturn FC+ | PMetavar Name+ | PProof [PTactic]+ | PTactics [PTactic] -- as PProof, but no auto solving+ | PElabError Err -- error to report on elaboration+ | PImpossible -- special case for declaring when an LHS can't typecheck+ deriving Eq+{-! +deriving instance Binary PTerm +!-}++mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm+mapPT f t = f (mpt t) where+ mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)+ mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)+ mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)+ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)+ mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)+ mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)+ mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)+ mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)+ mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)+ mpt (PHidden t) = PHidden (mapPT f t)+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)+ mpt x = x+++data PTactic' t = Intro [Name] | Intros | Focus Name+ | Refine Name [Bool] | Rewrite t | LetTac Name t+ | Exact t | Compute | Trivial+ | Solve+ | Attack+ | ProofState | ProofTerm | Undo+ | Try (PTactic' t) (PTactic' t)+ | TSeq (PTactic' t) (PTactic' t)+ | Qed | Abandon+ deriving (Show, Eq, Functor)+{-! +deriving instance Binary PTactic' +!-}++instance Sized a => Sized (PTactic' a) where+ size (Intro nms) = 1 + size nms+ size Intros = 1+ size (Focus nm) = 1 + size nm+ size (Refine nm bs) = 1 + size nm + length bs+ size (Rewrite t) = 1 + size t+ size (LetTac nm t) = 1 + size nm + size t+ size (Exact t) = 1 + size t+ size Compute = 1+ size Trivial = 1+ size Solve = 1+ size Attack = 1+ size ProofState = 1+ size ProofTerm = 1+ size Undo = 1+ size (Try l r) = 1 + size l + size r+ size (TSeq l r) = 1 + size l + size r+ size Qed = 1+ size Abandon = 1++type PTactic = PTactic' PTerm++data PDo' t = DoExp FC t+ | DoBind FC Name t+ | DoBindP FC t t+ | DoLet FC Name t t+ | DoLetP FC t t+ deriving (Eq, Functor)+{-! +deriving instance Binary PDo' +!-}++instance Sized a => Sized (PDo' a) where+ size (DoExp fc t) = 1 + size fc + size t+ size (DoBind fc nm t) = 1 + size fc + size nm + size t+ size (DoBindP fc l r) = 1 + size fc + size l + size r+ size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r+ size (DoLetP fc l r) = 1 + size fc + size l + size r++type PDo = PDo' PTerm++-- The priority gives a hint as to elaboration order. Best to elaborate+-- things early which will help give a more concrete type to other+-- variables, e.g. a before (interpTy a).++data PArg' t = PImp { priority :: Int, + lazyarg :: Bool, pname :: Name, getTm :: t }+ | PExp { priority :: Int,+ lazyarg :: Bool, getTm :: t }+ | PConstraint { priority :: Int,+ lazyarg :: Bool, getTm :: t }+ | PTacImplicit { priority :: Int,+ lazyarg :: Bool, pname :: Name, + getScript :: t,+ getTm :: t }+ deriving (Show, Eq, Functor)++instance Sized a => Sized (PArg' a) where+ size (PImp p l nm trm) = 1 + size nm + size trm+ size (PExp p l trm) = 1 + size trm+ size (PConstraint p l trm) = 1 + size trm+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm++{-! +deriving instance Binary PArg' +!-}++pimp = PImp 0 True+pexp = PExp 0 False+pconst = PConstraint 0 False+ptacimp = PTacImplicit 0 True++type PArg = PArg' PTerm++-- Type class data++data ClassInfo = CI { instanceName :: Name,+ class_methods :: [(Name, (FnOpts, PTerm))],+ class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl+ class_params :: [Name],+ class_instances :: [Name] }+ deriving Show+{-! +deriving instance Binary ClassInfo +!-}++data OptInfo = Optimise { collapsible :: Bool,+ forceable :: [Int], -- argument positions+ recursive :: [Int] }+ deriving Show+{-! +deriving instance Binary OptInfo +!-}+++data TypeInfo = TI { con_names :: [Name] }+ deriving Show+{-!+deriving instance Binary TypeInfo+!-}++-- Syntactic sugar info ++data DSL' t = DSL { dsl_bind :: t,+ dsl_return :: t,+ dsl_apply :: t,+ dsl_pure :: t,+ dsl_var :: Maybe t,+ index_first :: Maybe t,+ index_next :: Maybe t,+ dsl_lambda :: Maybe t,+ dsl_let :: Maybe t+ }+ deriving (Show, Functor)+{-!+deriving instance Binary DSL'+!-}++type DSL = DSL' PTerm++data SynContext = PatternSyntax | TermSyntax | AnySyntax+ deriving Show+{-! +deriving instance Binary SynContext +!-}++data Syntax = Rule [SSymbol] PTerm SynContext+ deriving Show+{-! +deriving instance Binary Syntax +!-}++data SSymbol = Keyword Name+ | Symbol String+ | Binding Name+ | Expr Name+ | SimpleExpr Name+ deriving Show+{-! +deriving instance Binary SSymbol +!-}++initDSL = DSL (PRef f (UN ">>=")) + (PRef f (UN "return"))+ (PRef f (UN "<$>"))+ (PRef f (UN "pure"))+ Nothing+ Nothing+ Nothing+ Nothing+ Nothing+ where f = FC "(builtin)" 0++data SyntaxInfo = Syn { using :: [(Name, PTerm)],+ syn_params :: [(Name, PTerm)],+ syn_namespace :: [String],+ no_imp :: [Name],+ decoration :: Name -> Name,+ inPattern :: Bool,+ implicitAllowed :: Bool,+ dsl_info :: DSL }+ deriving Show+{-!+deriving instance Binary SyntaxInfo+!-}++defaultSyntax = Syn [] [] [] [] id False False initDSL++expandNS :: SyntaxInfo -> Name -> Name+expandNS syn n@(NS _ _) = n+expandNS syn n = case syn_namespace syn of+ [] -> n+ xs -> NS n xs+++--- Pretty printing declarations and terms++instance Show PTerm where+ show tm = showImp False tm++instance Pretty PTerm where+ pretty = prettyImp False++instance Show PDecl where+ show d = showDeclImp False d++instance Show PClause where+ show c = showCImp True c++instance Show PData where+ show d = showDImp False d++showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops+showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty+showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)+showDeclImp _ (PData _ _ d) = show d++showCImp :: Bool -> PClause -> String+showCImp impl (PClause _ n l ws r w) + = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r+ ++ " where " ++ show w + where+ showWs [] = ""+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs+showCImp impl (PWith _ n l ws r w) + = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r+ ++ " { " ++ show w ++ " } " + where+ showWs [] = ""+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs+++showDImp :: Bool -> PData -> String+showDImp impl (PDatadecl n ty cons) + = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"+ ++ showSep "\n\t| " + (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)++getImps :: [PArg] -> [(Name, PTerm)]+getImps [] = []+getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs+getImps (_ : xs) = getImps xs++getExps :: [PArg] -> [PTerm]+getExps [] = []+getExps (PExp _ _ tm : xs) = tm : getExps xs+getExps (_ : xs) = getExps xs++getConsts :: [PArg] -> [PTerm]+getConsts [] = []+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs+getConsts (_ : xs) = getConsts xs++getAll :: [PArg] -> [PTerm]+getAll = map getTm ++prettyImp :: Bool -> PTerm -> Doc+prettyImp impl = prettySe 10+ where+ prettySe p (PQuote r) =+ if size r > breakingSize then+ text "![" $$ pretty r <> text "]"+ else+ text "![" <> pretty r <> text "]"+ prettySe p (PRef fc n) =+ if impl then+ pretty n+ else+ prettyBasic n+ where+ prettyBasic n@(UN _) = pretty n+ prettyBasic (MN _ s) = text s+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n+ prettySe p (PLam n ty sc) =+ bracket p 2 $+ if size sc > breakingSize then+ text "λ" <> pretty n <+> text "=>" $+$ pretty sc+ else+ text "λ" <> pretty n <+> text "=>" <+> pretty sc+ prettySe p (PLet n ty v sc) =+ bracket p 2 $+ if size sc > breakingSize then+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$+ nest nestingSize (prettySe 10 sc)+ else+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>+ prettySe 10 sc+ prettySe p (PPi (Exp l s) n ty sc)+ | n `elem` allNamesIn sc || impl =+ let open = if l then text "|" <> lparen else lparen in+ bracket p 2 $+ if size sc > breakingSize then+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>+ st <+> text "->" $+$ prettySe 10 sc+ else+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>+ st <+> text "->" <+> prettySe 10 sc+ | otherwise =+ bracket p 2 $+ if size sc > breakingSize then+ prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc+ else+ prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc+ where+ st =+ case s of+ Static -> text "[static]"+ _ -> empty+ prettySe p (PPi (Imp l s) n ty sc)+ | impl =+ let open = if l then text "|" <> lbrace else lbrace in+ bracket p 2 $+ if size sc > breakingSize then+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>+ st <+> text "->" <+> prettySe 10 sc+ else+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>+ st <+> text "->" <+> prettySe 10 sc+ | otherwise = prettySe 10 sc+ where+ st =+ case s of+ Static -> text $ "[static]"+ _ -> empty+ prettySe p (PPi (Constraint _ _) n ty sc) =+ bracket p 2 $+ if size sc > breakingSize then+ prettySe 10 ty <+> text "=>" <+> prettySe 10 sc+ else+ prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc+ prettySe p (PPi (TacImp _ _ s) n ty sc) =+ bracket p 2 $+ if size sc > breakingSize then+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>+ rbrace <+> text "->" $+$ prettySe 10 sc+ else+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>+ rbrace <+> text "->" <+> prettySe 10 sc+ prettySe p (PApp _ (PRef _ f) [])+ | not impl = pretty f+ prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)+ | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =+ let [l, r] = getExps args in+ bracket p 1 $+ if size r > breakingSize then+ prettySe 1 l <+> pretty op $+$ prettySe 0 r+ else+ prettySe 1 l <+> pretty op <+> prettySe 0 r+ prettySe p (PApp _ f as) =+ let args = getExps as in+ bracket p 1 $+ prettySe 1 f <+>+ if impl then+ foldl fS empty as+ -- foldr (<+>) empty $ map prettyArgS as+ else+ foldl fSe empty args+ -- foldr (<+>) empty $ map prettyArgSe args+ where+ fS l r =+ if size r > breakingSize then+ l $+$ nest nestingSize (prettyArgS r)+ else+ l <+> prettyArgS r++ fSe l r =+ if size r > breakingSize then+ l $+$ nest nestingSize (prettyArgSe r)+ else+ l <+> prettyArgSe r+ prettySe p (PCase _ scr opts) =+ text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody+ where+ prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts++ sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r+ prettySe p (PHidden tm) = text "." <> prettySe 0 tm+ prettySe p (PRefl _) = text "refl"+ prettySe p (PResolveTC _) = text "resolvetc"+ prettySe p (PTrue _) = text "()"+ prettySe p (PFalse _) = text "_|_"+ prettySe p (PEq _ l r) =+ bracket p 2 $+ if size r > breakingSize then+ prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)+ else+ prettySe 10 l <+> text "=" <+> prettySe 10 r+ prettySe p (PTyped l r) =+ lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen+ prettySe p (PPair _ l r) =+ if size r > breakingSize then+ lparen <> prettySe 10 l <> text "," $+$+ prettySe 10 r <> rparen+ else+ lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen+ prettySe p (PDPair _ l t r) =+ if size r > breakingSize then+ lparen <> prettySe 10 l <+> text "**" $+$+ prettySe 10 r <> rparen+ else+ lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen+ prettySe p (PAlternative a as) =+ lparen <> text "|" <> prettyAs <> text "|" <> rparen+ where+ prettyAs =+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as+ prettySe p PSet = text "Set"+ prettySe p (PConstant c) = pretty c+ -- XXX: add pretty for tactics+ prettySe p (PProof ts) =+ text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace+ prettySe p (PTactics ts) =+ text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace+ prettySe p (PMetavar n) = text "?" <> pretty n+ prettySe p (PReturn f) = text "return"+ prettySe p PImpossible = text "impossible"+ prettySe p Placeholder = text "_"+ prettySe p (PDoBlock _) = text "do block pretty not implemented"+ prettySe p (PElabError s) = pretty s++ prettySe p _ = text "test"++ prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)+ prettyArgS (PExp _ _ tm) = prettyArgSe tm+ prettyArgS (PConstraint _ _ tm) = prettyArgSc tm+ prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)++ prettyArgSe arg = prettySe 0 arg+ prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace+ prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace+ prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace++ bracket outer inner doc+ | inner > outer = lparen <> doc <> rparen+ | otherwise = doc+ +showImp :: Bool -> PTerm -> String+showImp impl tm = se 10 tm where+ se p (PQuote r) = "![" ++ show r ++ "]"+ se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"+ else showbasic n+ where showbasic n@(UN _) = show n+ showbasic (MN _ s) = s+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n+ se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ + (if impl then " : " ++ se 10 ty else "") ++ " => " + ++ se 10 sc+ se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v +++ " in " ++ se 10 sc + se p (PPi (Exp l s) n ty sc)+ | n `elem` allNamesIn sc || impl+ = bracket p 2 $+ if l then "|(" else "(" ++ + show n ++ " : " ++ se 10 ty ++ + ") " ++ st +++ "-> " ++ se 10 sc+ | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc+ where st = case s of+ Static -> "[static] "+ _ -> ""+ se p (PPi (Imp l s) n ty sc)+ | impl = bracket p 2 $ if l then "|{" else "{" ++ + show n ++ " : " ++ se 10 ty ++ + "} " ++ st ++ "-> " ++ se 10 sc+ | otherwise = se 10 sc+ where st = case s of+ Static -> "[static] "+ _ -> ""+ se p (PPi (Constraint _ _) n ty sc)+ = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc+ se p (PPi (TacImp _ _ s) n ty sc)+ = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc+ se p (PApp _ (PRef _ f) [])+ | not impl = show f+ se p (PApp _ (PRef _ op@(UN (f:_))) args)+ | length (getExps args) == 2 && not impl && not (isAlpha f) + = let [l, r] = getExps args in+ bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r+ se p (PApp _ f as) + = let args = getExps as in+ bracket p 1 $ se 1 f ++ if impl then concatMap sArg as+ else concatMap seArg args+ se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)+ where sc (l, r) = se 10 l ++ " => " ++ se 10 r+ se p (PHidden tm) = "." ++ se 0 tm+ se p (PRefl _) = "refl"+ se p (PResolveTC _) = "resolvetc"+ se p (PTrue _) = "()"+ se p (PFalse _) = "_|_"+ se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r+ se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"+ se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"+ se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"+ se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"+ se p PSet = "Set"+ se p (PConstant c) = show c+ se p (PProof ts) = "proof { " ++ show ts ++ "}"+ se p (PTactics ts) = "tactics { " ++ show ts ++ "}"+ se p (PMetavar n) = "?" ++ show n+ se p (PReturn f) = "return"+ se p PImpossible = "impossible"+ se p Placeholder = "_"+ se p (PDoBlock _) = "do block show not implemented"+ se p (PElabError s) = show s+-- se p x = "Not implemented"++ sArg (PImp _ _ n tm) = siArg (n, tm)+ sArg (PExp _ _ tm) = seArg tm+ sArg (PConstraint _ _ tm) = scArg tm+ sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)++ seArg arg = " " ++ se 0 arg+ siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"+ scArg val = " {{" ++ se 10 val ++ "}}"+ stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"++ bracket outer inner str | inner > outer = "(" ++ str ++ ")"+ | otherwise = str++{-+ PQuote Raw+ | PRef FC Name+ | PLam Name PTerm PTerm+ | PPi Plicity Name PTerm PTerm+ | PLet Name PTerm PTerm PTerm + | PTyped PTerm PTerm -- term with explicit type+ | PApp FC PTerm [PArg]+ | PCase FC PTerm [(PTerm, PTerm)]+ | PTrue FC+ | PFalse FC+ | PRefl FC+ | PResolveTC FC+ | PEq FC PTerm PTerm+ | PPair FC PTerm PTerm+ | PDPair FC PTerm PTerm PTerm+ | PAlternative [PTerm]+ | PHidden PTerm -- irrelevant or hidden pattern+ | PSet+ | PConstant Const+ | Placeholder+ | PDoBlock [PDo]+ | PIdiom FC PTerm+ | PReturn FC+ | PMetavar Name+ | PProof [PTactic]+ | PTactics [PTactic] -- as PProof, but no auto solving+ | PElabError Err -- error to report on elaboration+ | PImpossible -- special case for declaring when an LHS can't typecheck+-}++instance Sized PTerm where+ size (PQuote rawTerm) = size rawTerm+ size (PRef fc name) = size name+ size (PLam name ty bdy) = 1 + size ty + size bdy+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy+ size (PTyped trm ty) = 1 + size trm + size ty+ size (PApp fc name args) = 1 + size args+ size (PCase fc trm bdy) = 1 + size trm + size bdy+ size (PTrue fc) = 1+ size (PFalse fc) = 1+ size (PRefl fc) = 1+ size (PResolveTC fc) = 1+ size (PEq fc left right) = 1 + size left + size right+ size (PPair fc left right) = 1 + size left + size right+ size (PDPair fs left ty right) = 1 + size left + size ty + size right+ size (PAlternative a alts) = 1 + size alts+ size (PHidden hidden) = size hidden+ size PSet = 1+ size (PConstant const) = 1 + size const+ size Placeholder = 1+ size (PDoBlock dos) = 1 + size dos+ size (PIdiom fc term) = 1 + size term+ size (PReturn fc) = 1+ size (PMetavar name) = 1+ size (PProof tactics) = size tactics+ size (PElabError err) = size err+ size PImpossible = 1++allNamesIn :: PTerm -> [Name]+allNamesIn tm = nub $ ni [] tm + where+ ni env (PRef _ n) + | not (n `elem` env) = [n]+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc+ ni env (PHidden tm) = ni env tm+ ni env (PEq _ l r) = ni env l ++ ni env r+ ni env (PTyped l r) = ni env l ++ ni env r+ ni env (PPair _ l r) = ni env l ++ ni env r+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r+ ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r+ ni env (PAlternative a ls) = concatMap (ni env) ls+ ni env _ = []++namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]+namesIn uvars ist tm = nub $ ni [] tm + where+ ni env (PRef _ n) + | not (n `elem` env) + = case lookupTy Nothing n (tt_ctxt ist) of+ [] -> [n]+ _ -> if n `elem` (map fst uvars) then [n] else []+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc+ ni env (PEq _ l r) = ni env l ++ ni env r+ ni env (PTyped l r) = ni env l ++ ni env r+ ni env (PPair _ l r) = ni env l ++ ni env r+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r+ ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r+ ni env (PAlternative a as) = concatMap (ni env) as+ ni env (PHidden tm) = ni env tm+ ni env _ = []
src/Idris/Compiler.hs view
@@ -3,9 +3,11 @@ module Idris.Compiler where import Idris.AbsSyntax+import Core.TT++{- import Idris.Transforms -import Core.TT import Core.Evaluate import Core.CaseTree @@ -16,12 +18,16 @@ import System.Directory import System.Environment +import Paths_idris+ import Epic.Epic hiding (Term, Type, Name, fn, compile) import qualified Epic.Epic as E--primDefs = [UN "mkForeign", UN "FalseElim"]+-} compile :: FilePath -> Term -> Idris ()+compile f t = fail "Epic backend disabled"++{- compile f tm = do checkMVs let tmnames = namesUsed (STerm tm)@@ -30,8 +36,12 @@ objs <- getObjectFiles libs <- getLibs hdrs <- getHdrs- let incs = map Include hdrs+ ddir <- liftIO $ getDataDir+ -- if any includes exist in the data directory, use that+ hdrs' <- liftIO $ mapM (inDir ddir) hdrs+ let incs = map Include hdrs' so <- getSO+-- let ilib = ddir ++ "/libidris.a" case so of Nothing -> do m <- epicMain tm@@ -43,7 +53,11 @@ case idris_metavars i \\ primDefs of [] -> return () ms -> fail $ "There are undefined metavariables: " ++ show ms+ inDir d h = do let f = d ++ "/" ++ h+ ex <- doesFileExist f+ if ex then return f else return h + allNames :: [Name] -> Name -> Idris [Name] allNames ns n | n `elem` ns = return [] allNames ns n = do i <- get@@ -92,16 +106,21 @@ epic tm = epic' [] tm where epic' env tm@(App f a) | (P _ (UN "mkForeign") _, args) <- unApply tm- = doForeign args+ = doForeign False args+ | (P _ (UN "mkLazyForeign") _, args) <- unApply tm+ = doForeign True args+ | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm+ = epic' env arg | (P _ (UN "lazy") _, [_,arg]) <- unApply tm = do arg' <- epic' env arg return $ lazy_ arg' | (P _ (UN "prim__IO") _, [v]) <- unApply tm- = epic' env v+ = do v' <- epic' env v+ return (effect_ v') | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm = do v' <- epic' env v k' <- epic' env k- return (k' @@ (effect_ v'))+ return (effect_ (k' @@ (effect_ v'))) | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm = do size' <- epic' env size t' <- epic' env t@@ -144,24 +163,29 @@ buildApp env (e @@ x') xs -doForeign :: [TT Name] -> Idris E.Term-doForeign (_ : fgn : args)- | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn+doForeign :: Bool -> [TT Name] -> Idris E.Term+doForeign lazy (_ : fgn : args)+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn = let tys = getFTypes fgnArgTys- rty = mkEty ret in+ rty = mkEty' ret in do args' <- mapM epic args -- wrap it in a prim__IO -- return $ con_ 0 @@ impossible @@ - return $ lazy_ $ foreign_ rty fgnName (zip args' tys)+ if lazy + then return $ lazy_ $ foreignL_ rty fgnName (zip args' tys)+ else return $ lazy_ $ foreign_ rty fgnName (zip args' tys) | otherwise = fail "Badly formed foreign function call" getFTypes :: TT Name -> [E.Type] getFTypes tm = case unApply tm of (nil, []) -> []- (cons, [(P _ (UN ty) _), xs]) -> + (cons, [ty, xs]) -> let rest = getFTypes xs in- mkEty ty : rest + mkEty' ty : rest +mkEty' (P _ (UN ty) _) = mkEty ty+mkEty' _ = tyAny+ mkEty "FInt" = tyInt mkEty "FFloat" = tyFloat mkEty "FChar" = tyChar@@ -212,15 +236,4 @@ mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs return $ defaultcase rhs' -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 = catch (do e <- getEnv x- return (Just e))- (\_ -> return Nothing)-+-}
src/Idris/Coverage.hs view
@@ -140,7 +140,7 @@ data LexOrder = LexXX | LexEQ | LexLT deriving (Show, Eq, Ord) -calcTotality :: [Name] -> FC -> Name -> [(Term, Term)] -> Idris Totality+calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality calcTotality path fc n pats = do orders <- mapM ctot pats let order = sortBy cmpOrd $ concat orders@@ -177,7 +177,7 @@ [] -> [[]] -- recursive calls are all useless... xs -> xs - ctot (lhs, rhs) + ctot (_, lhs, rhs) | (_, args) <- unApply lhs = do -- check lhs doesn't use any dodgy names lhsOK <- mapM (chkOrd [] []) args
src/Idris/DSL.hs view
@@ -34,7 +34,7 @@ expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r) expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t) (expandDo dsl r)-expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)+expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as) expandDo dsl (PHidden t) = PHidden (expandDo dsl t) expandDo dsl (PReturn fc) = dsl_return dsl expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds @@ -81,7 +81,7 @@ v' i (PEq f l r) = PEq f (v' i l) (v' i r) v' i (PPair f l r) = PPair f (v' i l) (v' i r) v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)- v' i (PAlternative as) = PAlternative $ map (v' i) as+ v' i (PAlternative a as) = PAlternative a $ map (v' i) as v' i (PHidden t) = PHidden (v' i t) v' i (PIdiom f t) = PIdiom f (v' i t) v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)
src/Idris/DataOpts.hs view
@@ -60,6 +60,11 @@ y' <- applyOpts y return (x', y') +instance (Optimisable a, Optimisable b) => Optimisable (vs, a, b) where+ applyOpts (v, x, y) = do x' <- applyOpts x+ y' <- applyOpts y+ return (v, x', y')+ instance Optimisable a => Optimisable [a] where applyOpts = mapM applyOpts
src/Idris/Delaborate.hs view
@@ -10,6 +10,8 @@ import Debug.Trace +bugaddr = "https://github.com/edwinb/Idris-dev/issues"+ delab :: IState -> Term -> PTerm delab i tm = delab' i tm False @@ -50,7 +52,7 @@ deFn env (P _ n _) [ty, Bind x (Lam _) r] | n == UN "Exists" = PDPair un (PRef un x) (de env ty)- (de env (instantiate (P Bound x ty) r))+ (de ((x,x):env) (instantiate (P Bound x ty) r)) deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r) | n == eqTy = PEq un (de env l) (de env r) | n == UN "Ex_intro" = PDPair un (de env l) Placeholder@@ -70,20 +72,32 @@ pshow :: IState -> Err -> String pshow i (Msg s) = s-pshow i (CantUnify x y e s) +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) = "Can't unify " ++ show (delab i x) ++ " with " ++ show (delab i y) ++ -- " (" ++ show x ++ " and " ++ show y ++ ") " ++ case e of Msg "" -> ""- _ -> "\n\nSpecifically:\n\t " ++ pshow i e + _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++ + if (opt_errContext (idris_options i)) then showSc sc else ""+ where showSc [] = ""+ showSc xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))+ showVar (x, y) = "\t" ++ showbasic x ++ " : " ++ show (delab i y)+ showbasic n@(UN _) = show n+ showbasic (MN _ s) = s+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++ " when unifying " ++ show (delab i x) ++ " and " ++ 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 (NoSuchVariable n) = "No such variable " ++ show n pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t) pshow i UniverseError = "Universe inconsistency" pshow i ProgramLineComment = "Program line next to comment"+pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable" pshow i (At f e) = show f ++ ":" ++ pshow i e
src/Idris/ElabDecls.hs view
@@ -25,7 +25,6 @@ import Data.Maybe import Debug.Trace - recheckC fc env t = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...) ctxt <- getContext @@ -58,7 +57,7 @@ (cty, _) <- recheckC fc [] tyT addStatics n cty ty' logLvl 2 $ "---> " ++ show cty- let nty = normalise ctxt [] cty+ let nty = cty -- normalise ctxt [] cty ds <- checkDef fc [(n, nty)] addIBC (IBCDef n) addDeferred ds@@ -230,11 +229,11 @@ show r) pats)) ist <- get let tcase = opt_typecase (idris_options ist)- let pdef = map debind (map (simpl (tt_ctxt ist)) pats)+ let pdef = map debind $ map (simpl (tt_ctxt ist)) pats cov <- coverage pcover <- if cov - then do missing <- genClauses fc n (map fst pdef) cs+ then do missing <- genClauses fc n (map getLHS pdef) cs missing' <- filterM (checkPossible info fc True n) missing -- let missing' = mapMaybe (\x -> case x of -- Nothing -> Nothing@@ -243,7 +242,7 @@ logLvl 3 $ "Must be unreachable:\n" ++ showSep "\n" (map (showImp True) missing') ++ "\nAgainst: " ++- showSep "\n" (map (\t -> showImp True (delab ist t)) (map fst pdef))+ showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef)) if null missing' then return True else return False @@ -260,7 +259,7 @@ -- return False else return False pdef' <- applyOpts pdef - let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef+ tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover fc pdef ist <- get -- let wf = wellFounded ist n sc let tot = if pcover || AssertTotal `elem` opts@@ -279,7 +278,7 @@ iputStrLn $ show fc ++ ":warning - Unreachable case: " ++ show (delab ist x)) xs- let tree' = simpleCase tcase pcover pdef'+ tree' <- tclift $ simpleCase tcase pcover fc pdef' tclift $ sameLength pdef logLvl 3 (show tree) logLvl 3 $ "Optimised: " ++ show tree'@@ -299,18 +298,23 @@ do let ns = namesUsed sc \\ scargs logLvl 2 $ "Called names: " ++ show ns addToCG n ns+ addToCalledG n ns -- plus names in type! addIBC (IBCCG n) _ -> return () -- addIBC (IBCTotal n tot) [] -> return () where- debind (x, y) = (depat x, depat y)- depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)- depat x = x+ debind (x, y) = let (vs, x') = depat [] x + (_, y') = depat [] y in+ (vs, x', y')+ depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)+ depat acc x = (acc, x)+ + getLHS (_, l, _) = l simpl ctxt (x, y) = (x, simplify ctxt [] y) - sameLength ((x, _) : xs) + sameLength ((_, x, _) : xs) = do l <- sameLength xs let (f, as) = unApply x if (null xs || l == length as) then return (length as)@@ -376,7 +380,7 @@ let decls = concatMap declared whereblock let newargs = pvars ist lhs_tm let wb = map (expandParamsD ist decorate newargs decls) whereblock- logLvl 5 $ show wb+ logLvl 5 $ "Where block: " ++ show wb mapM_ (elabDecl' info) wb -- Now build the RHS, using the type of the LHS as the goal. i <- get -- new implicits from where block@@ -385,6 +389,7 @@ (expandParams decorate newargs decls rhs_in) logLvl 2 (showImp True rhs) ctxt <- getContext -- new context with where block added+ logLvl 5 "STARTING CHECK" ((rhs', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty [] (do pbinds lhs_tm@@ -393,6 +398,7 @@ tt <- get_term let (tm, ds) = runState (collectDeferred tt) [] return (tm, ds, is))+ logLvl 5 "DONE CHECK" logLvl 2 $ "---> " ++ show rhs' when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer def' <- checkDef fc defer@@ -582,7 +588,7 @@ [PTy syn fc [] n ty', PClauses fc (TCGen:o ++ opts) n cs] iLOG (show ds)- return (n, (defaultdec n, ds))+ return (n, ((defaultdec n, ds!!1), ds)) _ -> fail $ show n ++ " is not a method" defdecl _ _ _ = fail "Can't happen (defdecl)" @@ -664,17 +670,22 @@ Name -> -- the class [PTerm] -> -- class parameters (i.e. instance) PTerm -> -- full instance type+ Maybe Name -> -- explicit name [PDecl] -> Idris ()-elabInstance info syn fc cs n ps t ds+elabInstance info syn fc cs n ps t expn ds = do i <- get (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of [c] -> return c _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"- let iname = UN ('@':show n ++ "$" ++ show ps)+ let iname = case expn of+ Nothing -> UN ('@':show n ++ "$" ++ show ps)+ Just nm -> nm -- if the instance type matches any of the instances we have already,- -- then it's overlapping, so report an error- mapM_ (checkNotOverlapping i t) (class_instances ci) - addInstance intInst n iname+ -- and it's not a named instance, then it's overlapping, so report an error+ case expn of+ Nothing -> do mapM_ (checkNotOverlapping i t) (class_instances ci) + addInstance intInst n iname+ Just _ -> addInstance intInst n iname elabType info syn fc [] iname t let ips = zip (class_params ci) ps let ns = case n of@@ -685,7 +696,7 @@ (decorate ns n, op, coninsert cs t', t')) (class_methods ci) logLvl 3 (show (mtys, ips))- let ds' = insertDefaults (class_defaults ci) ns ds+ let ds' = insertDefaults i (class_defaults ci) ns ds iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci) mapM_ (warnMissing ds' ns) (map fst (class_methods ci)) mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')@@ -766,16 +777,16 @@ coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc) coninsert cs sc = conbind cs sc - insertDefaults :: [(Name, Name)] -> [String] -> [PDecl] -> [PDecl]- insertDefaults [] ns ds = ds- insertDefaults ((n,dn) : defs) ns ds - = insertDefaults defs ns (insertDef n dn ns ds)+ insertDefaults :: IState -> [(Name, (Name, PDecl))] -> [String] -> [PDecl] -> [PDecl]+ insertDefaults i [] ns ds = ds+ insertDefaults i ((n,(dn, clauses)) : defs) ns ds + = insertDefaults i defs ns (insertDef i n dn clauses ns ds) - insertDef meth def ns decls+ insertDef i meth def clauses ns decls | null $ filter (clauseFor meth ns) decls- = decls ++ [PClauses fc [Inlinable,TCGen] meth - [PClause fc meth (PApp fc (PRef fc meth) []) [] - (PApp fc (PRef fc def) []) []]]+ = let newd = expandParamsD i (\n -> meth) [] [def] clauses in+ -- trace (show newd) $ + decls ++ [newd] | otherwise = decls warnMissing decls ns meth@@ -854,9 +865,9 @@ Just ns -> info { namespace = Just (n:ns) } elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n elabClass info s f cs n ps ds-elabDecl' info (PInstance s f cs n ps t ds) +elabDecl' info (PInstance s f cs n ps t expn ds) = do iLOG $ "Elaborating instance " ++ show n- elabInstance info s f cs n ps t ds+ elabInstance info s f cs n ps t expn ds elabDecl' info (PRecord s f tyn ty cn cty) = do iLOG $ "Elaborating record " ++ show tyn elabRecord info s f tyn ty cn cty@@ -879,14 +890,16 @@ checkInferred :: FC -> PTerm -> PTerm -> Idris () checkInferred fc inf user =- do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" +++ do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++ showImp True user+ logLvl 10 $ "Checking match" i <- get tclift $ case matchClause' True i user inf of Right vs -> return () Left (x, y) -> tfail $ At fc (Msg $ "The type-checked term and given term do not match: " ++ show x ++ " and " ++ show y)+ logLvl 10 $ "Checked match" -- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user) -- Return whether inferred term is different from given term
src/Idris/ElabTerm.hs view
@@ -42,7 +42,9 @@ is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred tt) []- return (tm, ds, is)+ log <- getLog+ if (log /= "") then trace log $ return (tm, ds, is)+ else return (tm, ds, is) -- Build a term autogenerated as a typeclass method definition -- (Separate, so we don't go overboard resolving things that we don't@@ -55,7 +57,9 @@ is <- getAux tt <- get_term let (tm, ds) = runState (collectDeferred tt) []- return (tm, ds, is)+ log <- getLog+ if (log /= "") then trace log $ return (tm, ds, is)+ else return (tm, ds, is) -- Returns the set of declarations we need to add to complete the definition -- (most likely case blocks to elaborate)@@ -135,12 +139,20 @@ [pimp (MN 0 "a") t, pimp (MN 0 "P") Placeholder, pexp l, pexp r])- elab' ina (PAlternative as) - = let as' = pruneAlt as in- try (tryAll (zip (map (elab' ina) as') (map showHd as')))- (tryAll (zip (map (elab' ina) as) (map showHd as)))+ elab' ina (PAlternative True as) + = do ty <- goal+ ctxt <- get_context+ let (tc, _) = unApply ty+ let as' = pruneByType tc ctxt as+ let as'' = as' -- pruneAlt as'+ try (tryAll (zip (map (elab' ina) as'') (map showHd as'')))+ (tryAll (zip (map (elab' ina) as') (map showHd as'))) where showHd (PApp _ h _) = show h showHd x = show x+ elab' ina (PAlternative False as) + = trySeq as+ where trySeq [] = fail "All alternatives fail to elaborate"+ trySeq (x : xs) = try (elab' ina x) (trySeq xs) elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n) = do ctxt <- get_context let iscon = isConName Nothing n ctxt@@ -222,7 +234,9 @@ let isinf = f == inferCon || tcname f ctxt <- get_context let guarded = isConName Nothing f ctxt- try (do ns <- apply (Var f) (map isph args)+-- when True+ try+ (do ns <- apply (Var f) (map isph args) let (ns', eargs) = unzip $ sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))@@ -335,12 +349,12 @@ = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as) prune t = t - choose f (PAlternative as)+ choose f (PAlternative a as) = let as' = fmap (choose f) as fs = filter (headIs f) as' in case fs of [a] -> a- _ -> PAlternative as'+ _ -> PAlternative a as' choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as) choose f t = t @@ -348,6 +362,29 @@ headIs f (PApp _ f' _) = headIs f f' headIs f _ = True -- keep if it's not an application +-- Rule out alternatives that don't return the same type as the head of the goal+-- (If there are none left as a result, do nothing)++pruneByType :: Term -> Context -> [PTerm] -> [PTerm]+pruneByType (P _ n _) c as + = let as' = filter (headIs n) as in+ case as' of+ [] -> as+ _ -> as'+ where+ headIs f (PApp _ (PRef _ f') _) = typeHead f f'+ headIs f (PApp _ f' _) = headIs f f'+ headIs f (PPi _ _ _ sc) = headIs f sc+ headIs _ _ = True -- keep if it's not an application++ typeHead f f' = case lookupTy Nothing f' c of+ [ty] -> case unApply (getRetTy ty) of+ (P _ ftyn _, _) -> ftyn == f+ _ -> False+ _ -> False++pruneByType t _ as = as+ trivial :: IState -> ElabD () trivial ist = try (do elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0)) return ())@@ -416,7 +453,7 @@ [] -> [] [args] -> map isImp (snd args) -- won't be overloaded! args <- apply (Var n) imps--- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $+ -- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $ mapM_ (\ (_,n) -> do focus n t' <- goal let (tc', ttype) = unApply t'@@ -469,7 +506,7 @@ return (fn, a) -- FIXME: resolve ambiguities [(n, args)] -> return $ (n, map isImp args)- ns <- apply (Var fn') (map (\x -> (x,0)) imps)+ ns <- apply (Var fn') (map (\x -> (x, 0)) imps) when autoSolve solveAll where isImp (PImp _ _ _ _) = True isImp _ = False
src/Idris/Error.hs view
@@ -11,6 +11,7 @@ import Core.Constraints import System.Console.Haskeline+import System.Console.Haskeline.MonadException import Control.Monad.State import System.IO.Error(isUserError, ioeGetErrorString) import Data.Char
src/Idris/IBC.hs view
@@ -21,7 +21,7 @@ import Paths_idris ibcVersion :: Word8-ibcVersion = 17+ibcVersion = 19 data IBCFile = IBCFile { ver :: Word8, sourcefile :: FilePath,@@ -64,7 +64,8 @@ (_:_) -> fail "Can't write ibc when there are unsolved metavariables" [] -> return () ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src }) - idrisCatch (do liftIO $ encodeFile f ibcf+ idrisCatch (do liftIO $ createDirectoryIfMissing True (dropFileName f)+ liftIO $ encodeFile f ibcf iLOG "Written") (\c -> do iLOG $ "Failed " ++ show c) return ()@@ -154,9 +155,10 @@ pImports :: [FilePath] -> Idris () pImports fs - = do datadir <- liftIO $ getDataDir- mapM_ (\f -> do fp <- liftIO $ findImport [".", datadir] f- i <- getIState+ = do mapM_ (\f -> do i <- getIState+ ibcsd <- valIBCSubDir i+ ids <- allImportDirs i+ fp <- liftIO $ findImport ids ibcsd f if (f `elem` imported i) then iLOG $ "Already read " ++ f else do putIState (i { imported = f : imported i })@@ -800,6 +802,206 @@ _ -> error "Corrupted binary data for Plicity" +instance (Binary t) => Binary (PDecl' t) where+ put x+ = case x of+ PFix x1 x2 x3 -> do putWord8 0+ put x1+ put x2+ put x3+ PTy x1 x2 x3 x4 x5 -> do putWord8 1+ put x1+ put x2+ put x3+ put x4+ put x5+ PClauses x1 x2 x3 x4 -> do putWord8 2+ put x1+ put x2+ put x3+ put x4+ PData x1 x2 x3 -> do putWord8 3+ put x1+ put x2+ put x3+ PParams x1 x2 x3 -> do putWord8 4+ put x1+ put x2+ put x3+ PNamespace x1 x2 -> do putWord8 5+ put x1+ put x2+ PRecord x1 x2 x3 x4 x5 x6 -> do putWord8 6+ put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ PClass x1 x2 x3 x4 x5 x6 -> do putWord8 7+ put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 -> do putWord8 8+ put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ put x7+ put x8+ PDSL x1 x2 -> do putWord8 9+ put x1+ put x2+ get+ = do i <- getWord8+ case i of+ 0 -> do x1 <- get+ x2 <- get+ x3 <- get+ return (PFix x1 x2 x3)+ 1 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ return (PTy x1 x2 x3 x4 x5)+ 2 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ return (PClauses x1 x2 x3 x4)+ 3 -> do x1 <- get+ x2 <- get+ x3 <- get+ return (PData x1 x2 x3)+ 4 -> do x1 <- get+ x2 <- get+ x3 <- get+ return (PParams x1 x2 x3)+ 5 -> do x1 <- get+ x2 <- get+ return (PNamespace x1 x2)+ 6 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ return (PRecord x1 x2 x3 x4 x5 x6)+ 7 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ return (PClass x1 x2 x3 x4 x5 x6)+ 8 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ x7 <- get+ x8 <- get+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8)+ 9 -> do x1 <- get+ x2 <- get+ return (PDSL x1 x2)+ _ -> error "Corrupted binary data for PDecl'"++instance Binary SyntaxInfo where+ put (Syn x1 x2 x3 x4 x5 x6 x7 x8)+ = do put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ put x7+ put x8+ get+ = do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ x7 <- get+ x8 <- get+ return (Syn x1 x2 x3 x4 x5 x6 x7 x8)++instance (Binary t) => Binary (PClause' t) where+ put x+ = case x of+ PClause x1 x2 x3 x4 x5 x6 -> do putWord8 0+ put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ PWith x1 x2 x3 x4 x5 x6 -> do putWord8 1+ put x1+ put x2+ put x3+ put x4+ put x5+ put x6+ PClauseR x1 x2 x3 x4 -> do putWord8 2+ put x1+ put x2+ put x3+ put x4+ PWithR x1 x2 x3 x4 -> do putWord8 3+ put x1+ put x2+ put x3+ put x4+ get+ = do i <- getWord8+ case i of+ 0 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ return (PClause x1 x2 x3 x4 x5 x6)+ 1 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ x5 <- get+ x6 <- get+ return (PWith x1 x2 x3 x4 x5 x6)+ 2 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ return (PClauseR x1 x2 x3 x4)+ 3 -> do x1 <- get+ x2 <- get+ x3 <- get+ x4 <- get+ return (PWithR x1 x2 x3 x4)+ _ -> error "Corrupted binary data for PClause'"++instance (Binary t) => Binary (PData' t) where+ put (PDatadecl x1 x2 x3)+ = do put x1+ put x2+ put x3+ get+ = do x1 <- get+ x2 <- get+ x3 <- get+ return (PDatadecl x1 x2 x3)+ instance Binary PTerm where put x = case x of@@ -822,52 +1024,61 @@ put x2 put x3 put x4- PApp x1 x2 x3 -> do putWord8 5+ PTyped x1 x2 -> do putWord8 5+ put x1+ put x2+ PApp x1 x2 x3 -> do putWord8 6 put x1 put x2 put x3- PTrue x1 -> do putWord8 6+ PCase x1 x2 x3 -> do putWord8 7+ put x1+ put x2+ put x3+ PTrue x1 -> do putWord8 8 put x1- PFalse x1 -> do putWord8 7+ PFalse x1 -> do putWord8 9 put x1- PRefl x1 -> do putWord8 8+ PRefl x1 -> do putWord8 10 put x1- PResolveTC x1 -> do putWord8 9+ PResolveTC x1 -> do putWord8 11 put x1- PEq x1 x2 x3 -> do putWord8 10+ PEq x1 x2 x3 -> do putWord8 12 put x1 put x2 put x3- PPair x1 x2 x3 -> do putWord8 11+ PPair x1 x2 x3 -> do putWord8 13 put x1 put x2 put x3- PDPair x1 x2 x3 x4 -> do putWord8 12+ PDPair x1 x2 x3 x4 -> do putWord8 14 put x1 put x2 put x3 put x4- PAlternative x1 -> do putWord8 13- put x1- PHidden x1 -> do putWord8 14+ PAlternative x1 x2 -> do putWord8 15+ put x1+ put x2+ PHidden x1 -> do putWord8 16 put x1- PSet -> putWord8 15- PConstant x1 -> do putWord8 16+ PSet -> putWord8 17+ PConstant x1 -> do putWord8 18 put x1- Placeholder -> putWord8 17- PDoBlock x1 -> do putWord8 18+ Placeholder -> putWord8 19+ PDoBlock x1 -> do putWord8 20 put x1- PReturn x1 -> do putWord8 19+ PIdiom x1 x2 -> do putWord8 21+ put x1+ put x2+ PReturn x1 -> do putWord8 22 put x1- PMetavar x1 -> do putWord8 20+ PMetavar x1 -> do putWord8 23 put x1- PProof x1 -> do putWord8 21+ PProof x1 -> do putWord8 24 put x1- PTactics x1 -> do putWord8 22+ PTactics x1 -> do putWord8 25 put x1--- PElabError x1 -> do putWord8 23--- put x1- PImpossible -> putWord8 24+ PImpossible -> putWord8 27 get = do i <- getWord8 case i of@@ -892,52 +1103,60 @@ return (PLet x1 x2 x3 x4) 5 -> do x1 <- get x2 <- get+ return (PTyped x1 x2)+ 6 -> do x1 <- get+ x2 <- get x3 <- get return (PApp x1 x2 x3)- 6 -> do x1 <- get- return (PTrue x1) 7 -> do x1 <- get- return (PFalse x1)+ x2 <- get+ x3 <- get+ return (PCase x1 x2 x3) 8 -> do x1 <- get- return (PRefl x1)+ return (PTrue x1) 9 -> do x1 <- get- return (PResolveTC x1)+ return (PFalse x1) 10 -> do x1 <- get+ return (PRefl x1)+ 11 -> do x1 <- get+ return (PResolveTC x1)+ 12 -> do x1 <- get x2 <- get x3 <- get return (PEq x1 x2 x3)- 11 -> do x1 <- get+ 13 -> do x1 <- get x2 <- get x3 <- get return (PPair x1 x2 x3)- 12 -> do x1 <- get+ 14 -> do x1 <- get x2 <- get x3 <- get x4 <- get return (PDPair x1 x2 x3 x4)- 13 -> do x1 <- get- return (PAlternative x1)- 14 -> do x1 <- get- return (PHidden x1)- 15 -> return PSet+ 15 -> do x1 <- get+ x2 <- get+ return (PAlternative x1 x2) 16 -> do x1 <- get- return (PConstant x1)- 17 -> return Placeholder+ return (PHidden x1)+ 17 -> return PSet 18 -> do x1 <- get+ return (PConstant x1)+ 19 -> return Placeholder+ 20 -> do x1 <- get return (PDoBlock x1)- 19 -> do x1 <- get+ 21 -> do x1 <- get+ x2 <- get+ return (PIdiom x1 x2)+ 22 -> do x1 <- get return (PReturn x1)- 20 -> do x1 <- get+ 23 -> do x1 <- get return (PMetavar x1)- 21 -> do x1 <- get+ 24 -> do x1 <- get return (PProof x1)- 22 -> do x1 <- get+ 25 -> do x1 <- get return (PTactics x1)--- 23 -> do x1 <- get--- return (PElabError x1)- 24 -> return PImpossible+ 27 -> return PImpossible _ -> error "Corrupted binary data for PTerm"- instance (Binary t) => Binary (PTactic' t) where put x@@ -1189,6 +1408,8 @@ put x1 SimpleExpr x1 -> do putWord8 3 put x1+ Binding x1 -> do putWord8 4+ put x1 get = do i <- getWord8 case i of@@ -1200,4 +1421,6 @@ return (Expr x1) 3 -> do x1 <- get return (SimpleExpr x1)+ 4 -> do x1 <- get+ return (Binding x1) _ -> error "Corrupted binary data for SSymbol"
src/Idris/Imports.hs view
@@ -25,28 +25,44 @@ _ -> fp ++ ".lidr" -- Get name of byte compiled version of an import-ibcPath :: FilePath -> FilePath-ibcPath fp = let (n, ext) = splitExtension fp in- n ++ ".ibc"+ibcPath :: FilePath -> Bool -> FilePath -> FilePath+ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp+ d = if (not use_ibcsd) || ibcsd == ""+ then d_fp+ else d_fp ++ ibcsd ++ "/"+ n = dropExtension n_fp+ in d ++ n ++ ".ibc" -findImport :: [FilePath] -> FilePath -> IO IFileType-findImport [] fp = fail $ "Can't find import " ++ fp-findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)- let idrp = srcPath (d ++ "/" ++ fp)- let lidrp = lsrcPath (d ++ "/" ++ fp)- ibc <- doesFileExist ibcp- idr <- doesFileExist idrp- lidr <- doesFileExist lidrp--- when idr $ putStrLn $ idrp ++ " ok"--- when lidr $ putStrLn $ lidrp ++ " ok"--- when ibc $ putStrLn $ ibcp ++ " ok"- let isrc = if lidr then LIDR lidrp- else IDR idrp- if ibc - then return (IBC ibcp isrc)- else if (idr || lidr) - then return isrc- else findImport ds fp+ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath+ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp+ ibc <- doesFileExist ibcp+ return (if ibc+ then ibcp+ else ibcPath ibcsd False fp)++ibcPathNoFallback :: FilePath -> FilePath -> FilePath+ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp++findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType+findImport [] ibcsd fp = fail $ "Can't find import " ++ fp+findImport (d:ds) ibcsd fp = do let fp_full = d ++ "/" ++ fp+ ibcp <- ibcPathWithFallback ibcsd fp_full+ let idrp = srcPath fp_full+ let lidrp = lsrcPath fp_full+ ibc <- doesFileExist ibcp+ idr <- doesFileExist idrp+ lidr <- doesFileExist lidrp+-- when idr $ putStrLn $ idrp ++ " ok"+-- when lidr $ putStrLn $ lidrp ++ " ok"+-- when ibc $ putStrLn $ ibcp ++ " ok"+ let isrc = if lidr+ then LIDR lidrp+ else IDR idrp+ if ibc+ then return (IBC ibcp isrc)+ else if (idr || lidr) + then return isrc+ else findImport ds ibcsd fp -- find a specific filename somewhere in a path
src/Idris/Parser.hs view
@@ -57,9 +57,10 @@ loadModule :: FilePath -> Idris String loadModule f - = idrisCatch (do datadir <- liftIO $ getDataDir- fp <- liftIO $ findImport [".", datadir] f- i <- getIState+ = idrisCatch (do i <- getIState+ ibcsd <- valIBCSubDir i+ ids <- allImportDirs i+ fp <- liftIO $ findImport ids ibcsd f if (f `elem` imported i) then iLOG $ "Already read " ++ f else do putIState (i { imported = f : imported i })@@ -104,7 +105,8 @@ i <- get mapM_ checkDeclTotality (idris_totcheck i) iLOG ("Finished " ++ f)- let ibc = dropExtension f ++ ".ibc"+ ibcsd <- valIBCSubDir i+ let ibc = ibcPathNoFallback ibcsd f iucheck i <- getIState addHides (hide_list i)@@ -294,8 +296,8 @@ collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'-collect (PInstance f s cs n ps t ds : ds') - = PInstance f s cs n ps t (collect ds) : collect ds'+collect (PInstance f s cs n ps t en ds : ds') + = PInstance f s cs n ps t en (collect ds) : collect ds' collect (d : ds) = d : collect ds collect [] = [] @@ -373,7 +375,7 @@ when (length ns /= length (nub ns)) $ fail "Repeated variable in syntax rule" lchar '='- tm <- pExpr syn+ tm <- pExpr (impOK syn) pTerminator return (Rule (mkSimple syms) tm sty) where@@ -395,6 +397,8 @@ pSynSym :: IParser SSymbol pSynSym = try (do lchar '['; n <- pName; lchar ']' return (Expr n))+ <|> try (do lchar '{'; n <- pName; lchar '}'+ return (Binding n)) <|> do n <- iName [] return (Keyword n) <|> do sym <- strlit@@ -407,7 +411,7 @@ opts' <- pFnOpts n_in <- pfName let n = expandNS syn n_in- ty <- pTSig syn+ ty <- pTSig (impOK syn) fc <- pfc pTerminator -- ty' <- implicit syn n ty@@ -470,7 +474,7 @@ <|> try (do reserved "infix"; return InfixN) <|> try (do reserved "prefix"; return PrefixN) ---------- Tyoe classes ---------+--------- Type classes --------- pClass :: SyntaxInfo -> IParser [PDecl] pClass syn = do acc <- pAccessibility@@ -494,6 +498,10 @@ pInstance :: SyntaxInfo -> IParser [PDecl] pInstance syn = do reserved "instance" fc <- pfc+ en <- option Nothing+ (do lchar '['; n_in <- pfName; lchar ']'+ let n = expandNS syn n_in+ return (Just n)) cs <- pConstList syn cn <- pName args <- many1 (pSimpleExpr syn)@@ -502,7 +510,7 @@ reserved "where"; open_block ds <- many $ pFunDecl syn close_block- return [PInstance syn fc cs cn args t (concat ds)]+ return [PInstance syn fc cs cn args t en (concat ds)] --------- Expressions --------- @@ -550,6 +558,8 @@ valid (Rule _ _ TermSyntax) = not (inPattern syn) +data SynMatch = SynTm PTerm | SynBind Name+ pExt :: SyntaxInfo -> Syntax -> IParser PTerm pExt syn (Rule ssym ptm _) = do smap <- mapM pSymbol ssym@@ -558,27 +568,33 @@ where pSymbol (Keyword n) = do reserved (show n); return Nothing pSymbol (Expr n) = do tm <- pExpr syn- return $ Just (n, tm)+ return $ Just (n, SynTm tm) pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn- return $ Just (n, tm)+ return $ Just (n, SynTm tm)+ pSymbol (Binding n) = do b <- pName+ return $ Just (n, SynBind b) pSymbol (Symbol s) = do symbol s return Nothing dropn n [] = [] dropn n ((x,t) : xs) | n == x = xs | otherwise = (x,t):dropn n xs + updateB ns n = case lookup n ns of+ Just (SynBind t) -> t+ _ -> n+ update ns (PRef fc n) = case lookup n ns of- Just t -> t+ Just (SynTm t) -> t _ -> PRef fc n- update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)- update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc) - update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)+ update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)+ update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc) + update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val) (update (dropn n ns) sc) update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args) update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts) update ns (PPair fc l r) = PPair fc (update ns l) (update ns r) update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)- update ns (PAlternative as) = PAlternative (map (update ns) as)+ update ns (PAlternative a as) = PAlternative a (map (update ns) as) update ns (PHidden t) = PHidden (update ns t) update ns (PDoBlock ds) = PDoBlock $ upd ns ds where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds@@ -597,11 +613,15 @@ i <- getState UN n <- iName (syntax_keywords i) return (UN ('@':n))- -pfName = try pName- <|> do lchar '('; o <- operator; lchar ')'; return (UN o)+-- Parser for an operator in function position, i.e. enclosed by `()', with an+-- optional namespace.+pOpFront = maybeWithNS pOpFrontNoNS False []+ where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o +pfName = try pOpFront+ <|> pName+ pAccessibility' :: IParser Accessibility pAccessibility' = do reserved "public"; return Public@@ -615,6 +635,8 @@ pFnOpts :: IParser [FnOpt] pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)+ <|> try (do lchar '%'; reserved "export"; c <- strlit; xs <- pFnOpts+ return (CExport c : xs)) <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs) <|> do lchar '%'; reserved "specialise"; lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'@@ -654,10 +676,11 @@ <|> try (pList syn) <|> try (pAlt syn) <|> try (pIdiom syn)- <|> try (do lchar '('; bracketed syn)+ <|> 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)) <|> do lchar '_'; return Placeholder@@ -732,7 +755,7 @@ pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ',') symbol "|)"- return (PAlternative alts)+ return (PAlternative False alts) pHSimpleExpr syn = do lchar '.'@@ -790,9 +813,12 @@ mkSet (MN 0 n) = MN 0 ("set_" ++ n) mkSet (NS n s) = NS (mkSet n) s +noImp syn = syn { implicitAllowed = False }+impOK syn = syn { implicitAllowed = True }+ pTSig syn = do lchar ':'- cs <- pConstList syn- sc <- pExpr syn+ cs <- if implicitAllowed syn then pConstList syn else return []+ sc <- pExpr syn return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc) pLambda syn = do lchar '\\'@@ -829,12 +855,14 @@ symbol "->" sc <- pExpr syn return (bindList (PPi (Exp lazy st)) xt sc))- <|> try (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 '}' symbol "->"@@ -855,19 +883,19 @@ pConstList :: SyntaxInfo -> IParser [PTerm] pConstList syn = try (do lchar '(' - tys <- sepBy1 (pExpr' syn) (lchar ',')+ tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',') lchar ')' reservedOp "=>" return tys)- <|> try (do t <- pExpr syn+ <|> try (do t <- pExpr (noImp syn) reservedOp "=>" return [t]) <|> return [] -tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig 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 syn+ t <- pTSig (noImp syn) return (map (\x -> (x, t)) ns) tyOptDeclList syn = sepBy1 (do x <- pfName; @@ -975,7 +1003,7 @@ pRecord :: SyntaxInfo -> IParser PDecl pRecord syn = do acc <- pAccessibility reserved "record"; fc <- pfc- tyn_in <- pfName; ty <- pTSig syn+ tyn_in <- pfName; ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in reserved "where" open_block@@ -1001,7 +1029,7 @@ pData :: SyntaxInfo -> IParser PDecl pData syn = try (do acc <- pAccessibility reserved "data"; fc <- pfc- tyn_in <- pfName; ty <- pTSig syn+ tyn_in <- pfName; ty <- pTSig (impOK syn) let tyn = expandNS syn tyn_in reserved "where" open_block@@ -1041,7 +1069,7 @@ pConstructor syn = do cn_in <- pfName; fc <- pfc let cn = expandNS syn cn_in- ty <- pTSig syn+ ty <- pTSig (impOK syn) -- ty' <- implicit syn cn ty return (cn, ty, fc)
src/Idris/Primitives.hs view
@@ -6,17 +6,16 @@ import Idris.ElabTerm import Idris.AbsSyntax +import IRTS.Lang+ import Core.TT import Core.Evaluate -import Epic.Epic hiding (Term, Type, Name, fn)-import qualified Epic.Epic as E- data Prim = Prim { p_name :: Name, p_type :: Type, p_arity :: Int, p_def :: [Value] -> Maybe Value,- p_epic :: ([E.Name], E.Term),+ p_lexp :: (Int, PrimFn), p_total :: Totality } @@ -27,189 +26,148 @@ (Bind (UN "b") (Pi (Set (UVar (-2)))) (Bind (UN "x") (Pi (V 1)) (V 1))) -type ETm = E.Term-type EOp = E.Op--fun = E.fn-ref = E.ref--eOp :: EOp -> ([E.Name], ETm)-eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y")) --eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)-eOpFn ty rty op = ([E.name "x", E.name "y"], - foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])--strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]-intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]-charToInt x = x-intToChar x = x-intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]-bigIntToInt x = foreign_ tyInt "bigIntToInt" [(x, tyBigInt)]-strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]-bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]-strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]-floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]-intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]-floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]--floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]-floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]-floatSin x = foreign_ tyFloat "sin" [(x, tyFloat)]-floatCos x = foreign_ tyFloat "cos" [(x, tyFloat)]-floatTan x = foreign_ tyFloat "tan" [(x, tyFloat)]-floatASin x = foreign_ tyFloat "asin" [(x, tyFloat)]-floatACos x = foreign_ tyFloat "acos" [(x, tyFloat)]-floatATan x = foreign_ tyFloat "atan" [(x, tyFloat)]-floatFloor x = foreign_ tyFloat "floor" [(x, tyFloat)]-floatCeil x = foreign_ tyFloat "ceil" [(x, tyFloat)]-floatSqrt x = foreign_ tyFloat "sqrt" [(x, tyFloat)]--strIndex x i = foreign_ tyChar "strIndex" [(x, tyString), (i, tyInt)]-strHead x = foreign_ tyChar "strHead" [(x, tyString)]-strTail x = foreign_ tyString "strTail" [(x, tyString)]-strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]-strRev x = foreign_ tyString "strrev" [(x, tyString)]-strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]-strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]- total = Total [] partial = Partial NotCovering primitives = -- operators [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))- (eOp E.plus_) total,+ (2, LPlus) total, Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))- (eOp E.minus_) total,+ (2, LMinus) total, Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))- (eOp E.times_) total,+ (2, LTimes) total, Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))- (eOp E.divide_) partial,+ (2, LDiv) partial, Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))- (eOp E.eq_) total,+ (2, LEq) total, Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))- (eOp E.lt_) total,+ (2, LLt) total, Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))- (eOp E.lte_) total,+ (2, LLe) total, Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))- (eOp E.gt_) total,+ (2, LGt) total, Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))- (eOp E.gte_) total,+ (2, LGe) total, Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))- (eOp E.eq_) total,+ (2, LEq) total, Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))- (eOp E.lt_) total,+ (2, LLt) total, Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))- (eOp E.lte_) total,+ (2, LLe) total, Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))- (eOp E.gt_) total,+ (2, LGt) total, Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))- (eOp E.gte_) total,+ (2, LGe) total, Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))- (eOpFn tyBigInt tyBigInt "addBig") total,+ + (2, LBPlus) total, Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))- (eOpFn tyBigInt tyBigInt "subBig") total,+ (2, LBMinus) total, Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))- (eOpFn tyBigInt tyBigInt "mulBig") total,+ (2, LBTimes) total, Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))- (eOpFn tyBigInt tyBigInt "divBig") partial,+ (2, LBDiv) partial, Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))- (eOpFn tyBigInt tyInt "eqBig") total,+ (2, LBEq) total, Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))- (eOpFn tyBigInt tyInt "ltBig") total,+ (2, LBLt) total, Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))- (eOpFn tyBigInt tyInt "leBig") total,+ (2, LBLe) total, Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))- (eOpFn tyBigInt tyInt "gtBig") total,+ (2, LBGt) total, Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))- (eOpFn tyBigInt tyInt "geBig") total,+ (2, LBGe) total, Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))- (eOp E.plusF_) total,+ (2, LFPlus) total, Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))- (eOp E.minusF_) total,+ (2, LFMinus) total, Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))- (eOp E.timesF_) total,+ (2, LFTimes) total, Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))- (eOp E.divideF_) total,+ (2, LFDiv) total, Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))- (eOp E.eqF_) total,+ (2, LFEq) total, Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))- (eOp E.ltF_) total,+ (2, LFLt) total, Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))- (eOp E.lteF_) total,+ (2, LFLe) total, Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))- (eOp E.gtF_) total,+ (2, LFGt) total, Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))- (eOp E.gteF_) total,+ (2, LFGe) total, Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))- ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y") total,+ (2, LStrConcat) total, Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))- ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")) total,+ (2, LStrEq) total, Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))- ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")) total,+ (2, LStrLt) total, -- Conversions Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)- ([E.name "x"], strToInt (fun "x")) total,+ (1, LStrInt) total, Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)- ([E.name "x"], intToStr (fun "x")) total,+ (1, LIntStr) total, Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)- ([E.name "x"], charToInt (fun "x")) total,+ (1, LNoOp) total, Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)- ([E.name "x"], intToChar (fun "x")) total,+ (1, LNoOp) total, Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)- ([E.name "x"], intToBigInt (fun "x")) total,+ (1, LIntBig) total, Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)- ([E.name "x"], bigIntToInt (fun "x")) total,+ (1, LBigInt) total, Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)- ([E.name "x"], strToBigInt (fun "x")) total,+ (1, LStrBig) total, Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)- ([E.name "x"], bigIntToStr (fun "x")) total,+ (1, LBigStr) total, Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)- ([E.name "x"], strToFloat (fun "x")) total,+ (1, LStrFloat) total, Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)- ([E.name "x"], floatToStr (fun "x")) total,+ (1, LFloatStr) total, Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)- ([E.name "x"], intToFloat (fun "x")) total,+ (1, LIntFloat) total, Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)- ([E.name "x"], floatToInt (fun "x")) total,+ (1, LFloatInt) total, Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)- ([E.name "x"], floatExp (fun "x")) total, + (1, LFExp) total, Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)- ([E.name "x"], floatLog (fun "x")) total,+ (1, LFLog) total, Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)- ([E.name "x"], floatSin (fun "x")) total,+ (1, LFSin) total, Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)- ([E.name "x"], floatCos (fun "x")) total,+ (1, LFCos) total, Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)- ([E.name "x"], floatTan (fun "x")) total,+ (1, LFTan) total, Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)- ([E.name "x"], floatASin (fun "x")) total,+ (1, LFASin) total, Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)- ([E.name "x"], floatACos (fun "x")) total,+ (1, LFACos) total, Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)- ([E.name "x"], floatATan (fun "x")) total,+ (1, LFATan) total, Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)- ([E.name "x"], floatSqrt (fun "x")) total,+ (1, LFSqrt) total, Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)- ([E.name "x"], floatFloor (fun "x")) total,+ (1, LFFloor) total, Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)- ([E.name "x"], floatCeil (fun "x")) total,+ (1, LFCeil) total, Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)- ([E.name "x"], strHead (fun "x")) partial,+ (1, LStrHead) partial, Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)- ([E.name "x"], strTail (fun "x")) partial,+ (1, LStrTail) partial, Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)- ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs")) total,+ (2, LStrCons) total, Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)- ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")) partial,+ (2, LStrIndex) partial, Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)- ([E.name "x"], strRev (fun "x")) total,-+ (1, LStrRev) total,+ Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)+ (1, LReadStr) partial,+ -- Streams+ Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)+ (0, LStdIn) partial, Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)- ([E.name "a", E.name "b", E.name "x"], fun "x") total -- ahem+ (1, LNoOp) total -- ahem ] p_believeMe [_,_,x] = Just x@@ -310,12 +268,14 @@ p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs)) p_strRev _ = Nothing +p_cantreduce _ = Nothing+ elabPrim :: Prim -> Idris ()-elabPrim (Prim n ty i def epic tot) +elabPrim (Prim n ty i def sc tot) = do updateContext (addOperator n ty i def) setTotality n tot i <- getIState- putIState i { idris_prims = (n, epic) : idris_prims i }+ putIState i { idris_scprims = (n, sc) : idris_scprims i } elabPrims :: Idris () elabPrims = do mapM_ (elabDecl toplevel)
src/Idris/Prover.hs view
@@ -44,13 +44,14 @@ iLOG $ "Adding " ++ show tm iputStrLn $ showProof lit n prf i <- get- put (i { last_proof = Just (n, prf) })- let tree = simpleCase False True [(P Ref n ty, tm)]+ let proofs = proof_list i+ put (i { proof_list = (n, prf) : proofs })+ let tree = simpleCase False True (FC "proof" 0) [([], P Ref n ty, tm)] logLvl 3 (show tree) (ptm, pty) <- recheckC (FC "proof" 0) [] tm ptm' <- applyOpts ptm- updateContext (addCasedef n True False True [(P Ref n ty, ptm)] - [(P Ref n ty, ptm')] ty)+ updateContext (addCasedef n True False True [([], P Ref n ty, ptm)] + [([], P Ref n ty, ptm')] ty) solveDeferred n elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl]) elabStep st e = do case runStateT e st of
src/Idris/REPL.hs view
@@ -20,6 +20,13 @@ import Core.TT import Core.Constraints +import IRTS.Compiler++-- import RTS.SC+-- import RTS.Bytecode+-- import RTS.PreC+-- import RTS.CodegenC+ import System.Console.Haskeline as H import System.FilePath import System.Environment@@ -77,6 +84,10 @@ Right AddProof -> do idrisCatch (addProof fn orig) (\e -> iputStrLn (show e)) return (Just inputs)+ Right RmProof -> do rmProof orig+ return (Just inputs)+ Right Proofs -> do proofs orig+ return (Just inputs) Right Quit -> do iputStrLn "Bye bye" return Nothing Right cmd -> do idrisCatch (process fn cmd)@@ -110,14 +121,32 @@ liftIO $ copyFile f fb -- make a backup in case something goes wrong! prog <- liftIO $ readFile fb i <- get- case last_proof i of- Nothing -> iputStrLn "No proof to add"- Just (n, p) -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)- liftIO $ writeFile f (unlines prog')- iputStrLn $ "Added proof " ++ show n- put (i { last_proof = Nothing })- -- lift $ removeFile fb -- uncomment when less scared :)+ case proof_list i of+ [] -> iputStrLn "No proof to add"+ (n, p) : proofs -> do let prog' = insertScript (showProof (lit f) n p) (lines prog)+ liftIO $ writeFile f (unlines prog')+ iputStrLn $ "Added proof " ++ show n+ put (i { proof_list = proofs })+ -- lift $ removeFile fb -- uncomment when less scared :) +rmProof :: IState -> Idris ()+rmProof orig+ = do i <- get+ case proof_list i of+ [] -> iputStrLn "Nothing to remove"+ (n, p) : ps -> do iputStrLn $ "Removed proof " ++ show n+ let metavars = idris_metavars i+ put (i { proof_list = ps+ , idris_metavars = n : metavars+ })++proofs :: IState -> Idris ()+proofs orig+ = do i <- get+ case proof_list i of+ [] -> iputStrLn "No proofs"+ ps -> mapM_ (\(n, p) -> iputStrLn $ showProof False n p) ps+ insertScript :: String -> [String] -> [String] insertScript prf [] = "\n---------- Proofs ----------" : "" : [prf] insertScript prf (p@"---------- Proofs ----------" : "" : xs) @@ -142,7 +171,7 @@ -- [pexp t]) (tmpn, tmph) <- liftIO tempfile liftIO $ hClose tmph- compile tmpn tm+ compileC tmpn tm liftIO $ system tmpn return () where fc = FC "(input)" 0 @@ -180,29 +209,45 @@ case lookupTotal n (tt_ctxt i) of [t] -> iputStrLn (showTotal t i) _ -> return ()- where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)- liftIO $ putStr " = "- liftIO $ putStrLn $ showImp True (delab i rhs)+ where printCase i (_, lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)+ liftIO $ putStr " = "+ liftIO $ putStrLn $ showImp True (delab i rhs) process fn (TotCheck n) = do i <- get case lookupTotal n (tt_ctxt i) of [t] -> iputStrLn (showTotal t i) _ -> return ()-process fn (Info n) = do i <- get+process fn (DebugInfo n) + = do i <- get let oi = lookupCtxtName Nothing n (idris_optimisation i) when (not (null oi)) $ iputStrLn (show oi) let si = lookupCtxt Nothing n (idris_statics i) when (not (null si)) $ iputStrLn (show si)+ let d = lookupDef Nothing n (tt_ctxt i)+ when (not (null d)) $ liftIO $+ do print (head d)+process fn (Info n) = do i <- get+ case lookupCtxt Nothing n (idris_classes i) of+ [c] -> classInfo c+ _ -> iputStrLn "Not a class"+process fn (Search t) = iputStrLn "Not implemented" process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext ist <- get let tm' = specialise ctxt [] [] {- (idris_statics ist) -} tm iputStrLn (show (delab ist tm'))-process fn (Prove n) = do prover (lit fn) n- -- recheck totality- i <- get- totcheck (FC "(input)" 0, n)- mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)- mapM_ checkDeclTotality (idris_totcheck i)+process fn (Prove n') + = do ctxt <- getContext+ ist <- get+ n <- case lookupNames Nothing n' ctxt of+ [x] -> return x+ [] -> return n'+ ns -> fail $ pshow ist (CantResolveAlts (map show ns)) + prover (lit fn) n+ -- recheck totality+ i <- get+ totcheck (FC "(input)" 0, n)+ mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)+ mapM_ checkDeclTotality (idris_totcheck i) process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t ctxt <- getContext ist <- get@@ -219,16 +264,22 @@ -- (PRef (FC "main" 0) (NS (UN "main") ["main"])) (tmpn, tmph) <- liftIO tempfile liftIO $ hClose tmph- compile tmpn m+ compileC tmpn m liftIO $ system tmpn return () where fc = FC "main" 0 -process fn (Compile f) = do (m, _) <- elabVal toplevel False- (PApp fc - (PRef fc (UN "run__IO"))- [pexp $ PRef fc (NS (UN "main") ["main"])])- compile f m+process fn (NewCompile f) + = do (m, _) <- elabVal toplevel False+ (PApp fc (PRef fc (UN "run__IO"))+ [pexp $ PRef fc (NS (UN "main") ["main"])])+ compile f m where fc = FC "main" 0 +process fn (Compile f) + = do (m, _) <- elabVal toplevel False+ (PApp fc (PRef fc (UN "run__IO"))+ [pexp $ PRef fc (NS (UN "main") ["main"])])+ compileC f m+ where fc = FC "main" 0 process fn (LogLvl i) = setLogLevel i process fn Metavars = do ist <- get@@ -238,6 +289,32 @@ _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs process fn NOP = return () +process fn (SetOpt ErrContext) = setErrContext True+process fn (UnsetOpt ErrContext) = setErrContext False+process fn (SetOpt ShowImpl) = setImpShow True+process fn (UnsetOpt ShowImpl) = setImpShow False++process fn (SetOpt _) = iputStrLn "Not a valid option"+process fn (UnsetOpt _) = iputStrLn "Not a valid option"+++classInfo :: ClassInfo -> Idris ()+classInfo ci = do iputStrLn "Methods:\n"+ mapM_ dumpMethod (class_methods ci)+ iputStrLn ""+ iputStrLn "Instances:\n"+ mapM_ dumpInstance (class_instances ci)++dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()+dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t++dumpInstance :: Name -> Idris ()+dumpInstance n = do i <- get+ ctxt <- getContext+ imp <- impShow+ case lookupTy Nothing n ctxt of+ ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts+ showTotal t@(Partial (Other ns)) i = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns) showTotal t i = show t@@ -245,6 +322,18 @@ [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" ++@@ -259,15 +348,20 @@ ([""], "", ""), (["<expr>"], "", "Evaluate an expression"), ([":t"], "<expr>", "Check the type of an expression"),+ ([":i", ":info"], "<name>", "Display information about a type class"), ([":total"], "<name>", "Check the totality of a name"), ([":r",":reload"], "", "Reload current file"), ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"), ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"), ([":p",":prove"], "<name>", "Prove a metavariable"), ([":a",":addproof"], "", "Add last proof to source file"),+ ([":rmproof"], "", "Remove last proof from proof stack"),+ ([":proofs"], "", "Show proof stack"), ([":c",":compile"], "<filename>", "Compile to an executable <filename>"), ([":exec",":execute"], "", "Compile to an executable and run"), ([":?",":h",":help"], "", "Display this help text"),+ ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),+ ([":unset"], "<option>", "Unset an option"), ([":q",":quit"], "", "Exit the Idris system") ]
src/Idris/REPLParser.hs view
@@ -27,9 +27,12 @@ <|> 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 ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f)) <|> try (do cmd ["m", "metavars"]; eof; return Metavars)- <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n)) + <|> try (do cmd ["proofs"]; eof; return Proofs)+ <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n)) <|> try (do cmd ["a", "addproof"]; eof; return AddProof)+ <|> try (do cmd ["rmproof"]; eof; return RmProof) <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i))) <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t)) <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))@@ -37,8 +40,16 @@ <|> try (do cmd ["total"]; do n <- pName; eof; return (TotCheck n)) <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t)) <|> try (do cmd ["u", "universes"]; eof; return Universes)+ <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n)) <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))+ <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))+ <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))+ <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t)) <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t)) <|> do t <- pFullExpr defaultSyntax; return (Eval t) <|> do eof; return NOP++pOption :: IParser Opt+pOption = do discard (symbol "errorcontext"); return ErrContext+ <|> do discard (symbol "showimplicits"); return ShowImpl
src/Idris/Transforms.hs view
@@ -6,39 +6,52 @@ import Core.CaseTree import Core.TT +data TTOpt = TermTrans (TT Name -> TT Name) -- term transform+ | CaseTrans (SC -> SC) -- case expression transform+ class Transform a where- transform :: (a -> a) -> a -> a+ transform :: TTOpt -> a -> a instance Transform (TT Name) where- transform t x = t (trans' x) where- trans' (Bind n b sc) = Bind n (fmap (transform t) b) (transform t sc)- trans' (App f a) = App (transform t f) (transform t a)- trans' x = x--type TTOpt = TT Name -> TT Name+ transform o@(TermTrans t) tm = trans t tm where+ trans t (Bind n b tm) = t $ Bind n (transform o b) (trans t tm)+ trans t (App f a) = t $ App (trans t f) (trans t a)+ trans t tm = t tm+ transform _ tm = tm -optimisations :: [TTOpt]-optimisations = [zero, suc]+instance Transform a => Transform (Binder a) where+ transform t (Let ty v) = Let (transform t ty) (transform t v)+ transform t b = b { binderTy = transform t (binderTy b) } instance Transform SC where- transform t x = t (trans' x) where- trans' (Case n alts) = Case n (map transAlt alts)- trans' t = t+ transform o@(CaseTrans t) sc = trans t sc where+ trans t (Case n alts) = t (Case n (map (transform o) alts))+ trans t x = t x+ transform o@(TermTrans t) sc = trans t sc where+ trans t (Case n alts) = Case n (map (transform o) alts)+ trans t (STerm tm) = STerm (t tm)+ trans t x = x - transAlt (ConCase n i as sc) = ConCase n i as (trans' sc)- transAlt (ConstCase c sc) = ConstCase c (trans' sc)- transAlt (DefaultCase sc) = DefaultCase (trans' sc)+instance Transform CaseAlt where+ transform o (ConCase n i ns sc) = ConCase n i ns (transform o sc)+ transform o (ConstCase c sc) = ConstCase c (transform o sc)+ transform o (DefaultCase sc) = DefaultCase (transform o sc) -type CaseOpt = SC -> SC+natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase] -zero :: TTOpt-zero (P _ n _) | n == NS (UN "O") ["nat","prelude"] +zname = NS (UN "O") ["nat","prelude"] +sname = NS (UN "S") ["nat","prelude"] ++zero :: TT Name -> TT Name+zero (P _ n _) | n == zname = Constant (BI 0) zero x = x -suc :: TTOpt-suc (App (P _ s _) a) | s == NS (UN "S") ["nat","prelude"] +suc :: TT Name -> TT Name+suc (App (P _ s _) a) | s == sname = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a] suc x = x +natcase :: SC -> SC+natcase = undefined
src/Main.hs view
@@ -24,24 +24,15 @@ import Idris.Primitives import Idris.Imports import Idris.Error++import IRTS.Lang+import IRTS.LParser+ import Paths_idris -- Main program reads command line options, parses the main program, and gets -- on with the REPL. -data Opt = Filename String- | Ver- | Usage- | NoPrelude- | NoREPL- | OLogging Int- | Output String- | TypeCase- | TypeInType- | NoCoverage - | Verbose- deriving Eq- main = do xs <- getArgs opts <- parseArgs xs runInputT defaultSettings $ execStateT (runIdris opts) idrisInit@@ -51,12 +42,32 @@ 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+ 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 ()@@ -67,6 +78,9 @@ 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))@@ -75,16 +89,37 @@ 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 @@ -94,19 +129,35 @@ showver = do putStrLn $ "Idris version " ++ ver exitWith ExitSuccess +showLibs = do dir <- getDataDir+ putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts"+ 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 ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)-parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)-parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)-parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)-parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)-parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)-parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)+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 @@ -120,9 +171,13 @@ "--------------" ++ map (\x -> '-') ver ++ "\n" ++ "Usage: idris [input file] [options]\n" ++ "Options:\n" ++- "\t--check Type check only\n" ++- "\t-o [file] Generate executable\n" ++- "\t--noprelude Don't import the prelude\n" ++- "\t--typeintype Disable universe checking\n" ++- "\t--log [level] Set debugging log level\n"+ "\t--check Type check only\n" +++ "\t-o [file] Generate executable\n" +++ "\t-i [dir] Add directory to the list of import paths\n" +++ "\t--ibcsubdir [dir] Write IBC files into sub directory\n" +++ "\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"