ffc7b69 · Idris-dev · git.iko.soy

Setup.hs+18−3

compare with master

unifiedsplit

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

26 , "TARGET=" ++ idir

27 , "IDRIS=" ++ icmd

28 ]

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

29 make verbosity

30 make verbosity

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

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

31− , "TARGET=" ++ idir

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"

32 , "IDRIS=" ++ icmd

45 , "IDRIS=" ++ icmd

33 ]

46 ]

34

47

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

40 , "IDRIS=" ++ icmd

53 , "IDRIS=" ++ icmd

41 ]

54 ]

42 make verbosity

55 make verbosity

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

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

44 , "IDRIS=" ++ icmd

57 , "IDRIS=" ++ icmd

45 ]

58 ]

46

59

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

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

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

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

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

55 NoCopyDest

68 NoCopyDest

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

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

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

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

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

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

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

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

idris.cabal+3−1

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

40Cabal-Version: >= 1.6

41Build-type: Custom

42

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

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

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

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

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

45 tutorial/examples/*.idr

46 tutorial/examples/*.idr

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

46

48

47source-repository head

49source-repository head

48 type: git

50 type: git

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

70

72

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

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

72 containers, process, transformers, filepath, directory,

74 containers, process, transformers, filepath, directory,

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

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

74

76

75 Extensions: MultiParamTypeClasses, FunctionalDependencies,

77 Extensions: MultiParamTypeClasses, FunctionalDependencies,

76 FlexibleInstances, TemplateHaskell

78 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 {

23 "do", "dsl", "import", "impossible",

24 "case", "of", "total",

25 "infix", "infixl", "infixr",

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

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

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

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

28 "public", "private", "abstract",

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

30 }

src/Idris/AbsSyntax.hs+3

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

404data Opt = Filename String

405 | Ver

406 | Usage

407+ | ShowLibs

408+ | ShowIncs

407 | NoPrelude

409 | NoPrelude

408 | NoREPL

410 | NoREPL

409 | OLogging Int

411 | OLogging Int

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

474tacimpl = TacImp False Dynamic

476tacimpl = TacImp False Dynamic

475

477

476data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

478data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen

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

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

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

478 deriving (Show, Eq)

481 deriving (Show, Eq)

479{-!

482{-!

src/Idris/Compiler.hs+2−2

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

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

38 let incs = map Include hdrs'

39 so <- getSO

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

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

41 case so of

42 Nothing ->

43 do m <- epicMain tm

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

45 liftIO $ compileObjWith []

46 (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

48 where checkMVs = do i <- get

49 case idris_metavars i \\ primDefs of

50 [] -> return ()

src/Idris/Parser.hs+2

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

621

622pFnOpts :: IParser [FnOpt]

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

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

625+ return (CExport c : xs))

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

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

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

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

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

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

src/Main.hs+15−1

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

42 let importdirs = opt getImportDir opts

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

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

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

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

45 setREPL runrepl

47 setREPL runrepl

46 setVerbose runrepl

48 setVerbose runrepl

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

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

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

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

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

97 exitWith ExitSuccess

99 exitWith ExitSuccess

98

100

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+

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

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

100parseArgs [] = return []

110parseArgs [] = return []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

145 "\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"

135

149