ffc7b69 · Idris-dev · git.iko.soy

Setup.hs+18−3

@@ -26,9 +26,22 @@ installStdLib pkg local verbosity copy

2626 , "TARGET=" ++ idir

2727 , "IDRIS=" ++ icmd

2828 ]

29+ putStrLn $ "Installing run time system in " ++ idir ++ "/rts"

2930 make verbosity

30− [ "-C", "support", "install"

31− , "TARGET=" ++ idir

31+ [ "-C", "rts", "install"

32+ , "TARGET=" ++ idir ++ "/rts"

33+ , "IDRIS=" ++ icmd

34+ ]

35+

36+-- This is a hack. I don't know how to tell cabal that a data file needs

37+-- installing but shouldn't be in the distribution. And it won't make the

38+-- distribution if it's not there, so instead I just delete

39+-- the file after configure.

40+

41+removeLibIdris local verbosity

42+ = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

43+ make verbosity

44+ [ "-C", "rts", "clean"

3245 , "IDRIS=" ++ icmd

3346 ]

3447

@@ -40,7 +53,7 @@ checkStdLib local verbosity

4053 , "IDRIS=" ++ icmd

4154 ]

4255 make verbosity

43− [ "-C", "support", "check"

56+ [ "-C", "rts", "check"

4457 , "IDRIS=" ++ icmd

4558 ]

4659

@@ -53,6 +66,8 @@ main = defaultMainWithHooks $ simpleUserHooks

5366 , postInst = \ _ flags pkg lbi -> do

5467 installStdLib pkg lbi (S.fromFlag $ S.installVerbosity flags)

5568 NoCopyDest

69+ , postConf = \ _ flags _ lbi -> do

70+ removeLibIdris lbi (S.fromFlag $ S.configVerbosity flags)

5671 , postClean = \ _ flags _ _ -> do

5772 cleanStdLib (S.fromFlag $ S.cleanVerbosity flags)

5873 , postBuild = \ _ flags _ lbi -> do

idris.cabal+3−1

@@ -40,9 +40,11 @@ Description: Idris is a general purpose language with full dependent types.

4040Cabal-Version: >= 1.6

4141Build-type: Custom

4242

43+Data-files: rts/libidris_rts.a rts/closure.h

4344Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

4445 lib/control/monad/*.idr lib/language/*.idr

4546 tutorial/examples/*.idr

47+ rts/*.c rts/*.h rts/Makefile

4648

4749source-repository head

4850 type: git

@@ -70,7 +72,7 @@ Executable idris

7072

7173 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

7274 containers, process, transformers, filepath, directory,

73− binary, bytestring, epic>=0.9.3, pretty

75+ binary, bytestring, epic>=0.9.3.1, pretty

7476

7577 Extensions: MultiParamTypeClasses, FunctionalDependencies,

7678 FlexibleInstances, TemplateHaskell

rts/Makefilenew file+22

@@ -0,0 +1,22 @@

1+OBJS = closure.o

2+HDRS = closure.h

3+CFLAGS = -g

4+

5+LIBTARGET = libidris_rts.a

6+

7+check : $(LIBTARGET)

8+

9+$(LIBTARGET) : $(OBJS)

10+ ar r $(LIBTARGET) $(OBJS)

11+ ranlib $(LIBTARGET)

12+

13+install : .PHONY

14+ mkdir -p $(TARGET)

15+ install $(LIBTARGET) $(HDRS) $(TARGET)

16+

17+clean : .PHONY

18+ rm -f $(OBJS) $(LIBTARGET)

19+

20+closure.o: closure.h

21+

22+.PHONY:

rts/closure.cnew file+91

@@ -0,0 +1,91 @@

1+#include <stdlib.h>

2+#include <string.h>

3+

4+#include "closure.h"

5+

6+VM* init_vm(int stack_size, size_t heap_size) {

7+ VAL* valstack = malloc(stack_size*sizeof(VAL));

8+ int* intstack = malloc(stack_size*sizeof(int));

9+ double* floatstack = malloc(stack_size*sizeof(double));

10+

11+ VM* vm = malloc(sizeof(VM));

12+ vm -> valstack = valstack;

13+ vm -> valstack_ptr = valstack;

14+ vm -> intstack = intstack;

15+ vm -> intstack_ptr = intstack;

16+ vm -> floatstack = floatstack;

17+ vm -> floatstack_ptr = floatstack;

18+ vm -> stack_max = stack_size;

19+ vm -> heap = malloc(heap_size);

20+ return vm;

21+}

22+

23+void* allocate(VM* vm, int size) {

24+ return malloc(size); // TMP!

25+}

26+

27+void* allocThunk(VM* vm, int argspace) {

28+ Closure* cl = allocate(vm, sizeof(ClosureType) +

29+ sizeof(VAL) * (argspace + 1) +

30+ sizeof(int) * 2);

31+ cl -> ty = THUNK;

32+ return (void*)cl;

33+}

34+

35+void* allocCon(VM* vm, int arity) {

36+ Closure* cl = allocate(vm, sizeof(ClosureType) +

37+ sizeof(int) +

38+ sizeof(VAL) * arity);

39+ cl -> ty = CON;

40+ return (void*)cl;

41+}

42+

43+VAL mkInt(VM* vm, int val) {

44+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(int));

45+ cl -> ty = INT;

46+ cl -> info.i = val;

47+ return cl;

48+}

49+

50+VAL mkFloat(VM* vm, double val) {

51+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(double));

52+ cl -> ty = FLOAT;

53+ cl -> info.f = val;

54+ return cl;

55+}

56+

57+VAL mkStr(VM* vm, char* str) {

58+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) * strlen(str));

59+ cl -> ty = STRING;

60+ strcpy(cl -> info.str, str);

61+ return cl;

62+}

63+

64+VAL mkThunk(VM* vm, func fn, int args, int arity) {

65+ int i;

66+ Closure* cl = allocThunk(vm, arity);

67+ cl -> info.t.fn = fn;

68+ cl -> info.t.arity = arity;

69+ cl -> info.t.numargs = args;

70+ VAL** argptr = &(cl -> info.t.args);

71+

72+ for (i = 0; i < args; ++i) {

73+ VAL* v = POP;

74+ *argptr++ = v;

75+ }

76+}

77+

78+VAL mkCon(VM* vm, int tag, int arity) {

79+ Closure* cl = allocCon(vm, arity);

80+

81+ int i;

82+ cl -> info.c.tag = tag;

83+ VAL** argptr = &(cl -> info.c.args);

84+

85+ for (i = 0; i < arity; ++i) {

86+ VAL* v = POP;

87+ *argptr++ = v;

88+ }

89+

90+}

91+

rts/closure.hnew file+79

@@ -0,0 +1,79 @@

1+#ifndef _CLOSURE_H

2+#define _CLOSURE_H

3+

4+

5+// Closures

6+typedef void* VAL;

7+

8+typedef struct {

9+ VAL* valstack;

10+ int* intstack;

11+ double* floatstack;

12+ VAL* valstack_ptr;

13+ int* intstack_ptr;

14+ double* floatstack_ptr;

15+ void* heap;

16+ int stack_max;

17+} VM;

18+

19+VM* init_vm(int stack_size, size_t heap_size);

20+

21+// Functions all take a pointer to their VM, and return nothing.

22+typedef void(*func)(VM*);

23+

24+typedef enum {

25+ THUNK, CON, INT, FLOAT, STRING, UNIT, PTR

26+} ClosureType;

27+

28+typedef struct {

29+ VAL fn;

30+ int arity;

31+ int numargs;

32+ VAL* args;

33+} thunk;

34+

35+typedef struct {

36+ int tag;

37+ VAL* args;

38+} con;

39+

40+typedef struct {

41+ ClosureType ty;

42+ union {

43+ thunk t;

44+ con c;

45+ int i;

46+ double f;

47+ char* str;

48+ void* ptr;

49+ } info;

50+} Closure;

51+

52+// Stack manipulation instructions

53+

54+#define PUSH(i) *(vm->valstack_ptr++) = i;

55+#define POP --vm->valstack_ptr;

56+

57+#define PUSHINT(i) *(vm->intstack_ptr++) = i;

58+#define POPINT --vm->intstack_ptr;

59+

60+#define PUSHFLOAT(i) *(vm->floatstack_ptr++) = i;

61+#define POPFLOAT --vm->floatstack_ptr;

62+

63+#define SLIDE(n) *(vm->valstack_ptr-n) = *(vm->valstack_ptr); vm->valstack_ptr-=n;

64+#define SLIDEINT(n) *(vm->intstack_ptr-n) = *(vm->intstack_ptr); vm->floatstack_ptr-=n;

65+#define SLIDEFLOAT(n) *(vm->floatstack_ptr-n) = *(vm->floatstack_ptr); vm->floatstack_ptr-=n;

66+

67+#define DISCARD(n) vm->valstack_ptr-=n;

68+#define DISCARDINT(n) vm->intstack_ptr-=n;

69+#define DISCARDFLOAT(n) vm->floatstack_ptr-=n;

70+

71+// Creating new values (each value placed at the top of the stack)

72+VAL mkInt(VM* vm, int val);

73+VAL mkFloat(VM* vm, double val);

74+VAL mkStr(VM* vm, char* str);

75+

76+VAL mkThunk(VM* vm, func fn, int args, int arity);

77+VAL mkCon(VM* vm, int tag, int arity);

78+

79+#endif

src/Core/CoreParser.hs+2−2

@@ -23,8 +23,8 @@ idrisDef = haskellDef {

2323 "do", "dsl", "import", "impossible",

2424 "case", "of", "total",

2525 "infix", "infixl", "infixr",

26− "where", "with", "syntax", "proof",

27− "using", "params", "namespace", "class", "instance",

26+ "where", "with", "syntax", "proof", "postulate",

27+ "using", "namespace", "class", "instance",

2828 "public", "private", "abstract",

2929 "Int", "Integer", "Float", "Char", "String", "Ptr"]

3030 }

src/Idris/AbsSyntax.hs+3

@@ -404,6 +404,8 @@ data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

404404data Opt = Filename String

405405 | Ver

406406 | Usage

407+ | ShowLibs

408+ | ShowIncs

407409 | NoPrelude

408410 | NoREPL

409411 | OLogging Int

@@ -474,6 +476,7 @@ constraint = Constraint False Dynamic

474476tacimpl = TacImp False Dynamic

475477

476478data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

479+ | CExport String -- export, with a C name

477480 | Specialise [Name] -- specialise it, freeze these names

478481 deriving (Show, Eq)

479482{-!

src/Idris/Compiler.hs+2−2

@@ -37,14 +37,14 @@ compile f tm

3737 hdrs' <- liftIO $ mapM (inDir ddir) hdrs

3838 let incs = map Include hdrs'

3939 so <- getSO

40− let ilib = ddir ++ "/libidris.a"

40+-- let ilib = ddir ++ "/libidris.a"

4141 case so of

4242 Nothing ->

4343 do m <- epicMain tm

4444 let mainval = EpicFn (name "main") m

4545 liftIO $ compileObjWith []

4646 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")

47− liftIO $ link ((f ++ ".o") : ilib : objs ++ (map ("-l"++) libs)) f

47+ liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

4848 where checkMVs = do i <- get

4949 case idris_metavars i \\ primDefs of

5050 [] -> return ()

src/Idris/Parser.hs+2

@@ -621,6 +621,8 @@ pAccessibility

621621

622622pFnOpts :: IParser [FnOpt]

623623pFnOpts = do reserved "total"; xs <- pFnOpts; return (TotalFn : xs)

624+ <|> try (do lchar '%'; reserved "export"; c <- strlit; xs <- pFnOpts

625+ return (CExport c : xs))

624626 <|> do lchar '%'; reserved "assert_total"; xs <- pFnOpts; return (AssertTotal : xs)

625627 <|> do lchar '%'; reserved "specialise";

626628 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

src/Main.hs+15−1

@@ -42,6 +42,8 @@ runIdris opts =

4242 let importdirs = opt getImportDir opts

4343 when (Ver `elem` opts) $ liftIO showver

4444 when (Usage `elem` opts) $ liftIO usage

45+ when (ShowIncs `elem` opts) $ liftIO showIncs

46+ when (ShowLibs `elem` opts) $ liftIO showLibs

4547 setREPL runrepl

4648 setVerbose runrepl

4749 when (Verbose `elem` opts) $ setVerbose True

@@ -96,6 +98,14 @@ usage = do putStrLn usagemsg

9698showver = do putStrLn $ "Idris version " ++ ver

9799 exitWith ExitSuccess

98100

101+showLibs = do dir <- getDataDir

102+ putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts"

103+ exitWith ExitSuccess

104+

105+showIncs = do dir <- getDataDir

106+ putStrLn $ "-I" ++ dir ++ "/rts"

107+ exitWith ExitSuccess

108+

99109parseArgs :: [String] -> IO [Opt]

100110parseArgs [] = return []

101111parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

@@ -107,6 +117,8 @@ parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

107117parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)

108118parseArgs ("--errorcontext":ns) = liftM (ErrContext : ) (parseArgs ns)

109119parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

120+parseArgs ("--link":ns) = liftM (ShowLibs : ) (parseArgs ns)

121+parseArgs ("--include":ns) = liftM (ShowIncs : ) (parseArgs ns)

110122parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

111123parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

112124parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

@@ -131,5 +143,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

131143 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

132144 "\t--noprelude Don't import the prelude\n" ++

133145 "\t--typeintype Disable universe checking\n" ++

134− "\t--log [level] Set debugging log level\n"

146+ "\t--log [level] Set debugging log level\n" ++

147+ "\t--link Show library directories and exit (for C linking)\n" ++

148+ "\t--include Show include directories and exit (for C linking)\n"

135149