Permalink
Browse files

First baby steps towards a new RTS (and towards removing epic depende…

…ncy)
  • Loading branch information...
1 parent 4bbbf1d commit ffc7b69a483b57d4da99547735f27e6c639ac107 Edwin Brady committed May 14, 2012
Showing with 237 additions and 9 deletions.
  1. +18 −3 Setup.hs
  2. +3 −1 idris.cabal
  3. +22 −0 rts/Makefile
  4. +91 −0 rts/closure.c
  5. +79 −0 rts/closure.h
  6. +2 −2 src/Core/CoreParser.hs
  7. +3 −0 src/Idris/AbsSyntax.hs
  8. +2 −2 src/Idris/Compiler.hs
  9. +2 −0 src/Idris/Parser.hs
  10. +15 −1 src/Main.hs
View
@@ -26,9 +26,22 @@ installStdLib pkg local verbosity copy
, "TARGET=" ++ idir
, "IDRIS=" ++ icmd
]
+ putStrLn $ "Installing run time system in " ++ idir ++ "/rts"
make verbosity
- [ "-C", "support", "install"
- , "TARGET=" ++ idir
+ [ "-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
]
@@ -40,7 +53,7 @@ checkStdLib local verbosity
, "IDRIS=" ++ icmd
]
make verbosity
- [ "-C", "support", "check"
+ [ "-C", "rts", "check"
, "IDRIS=" ++ icmd
]
@@ -53,6 +66,8 @@ main = defaultMainWithHooks $ simpleUserHooks
, 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
View
@@ -40,9 +40,11 @@ Description: Idris is a general purpose language with full dependent types.
Cabal-Version: >= 1.6
Build-type: Custom
+Data-files: rts/libidris_rts.a rts/closure.h
Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
lib/control/monad/*.idr lib/language/*.idr
tutorial/examples/*.idr
+ rts/*.c rts/*.h rts/Makefile
source-repository head
type: git
@@ -70,7 +72,7 @@ Executable idris
Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
containers, process, transformers, filepath, directory,
- binary, bytestring, epic>=0.9.3, pretty
+ binary, bytestring, epic>=0.9.3.1, pretty
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, TemplateHaskell
View
@@ -0,0 +1,22 @@
+OBJS = closure.o
+HDRS = closure.h
+CFLAGS = -g
+
+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)
+
+closure.o: closure.h
+
+.PHONY:
View
@@ -0,0 +1,91 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "closure.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_ptr = valstack;
+ vm -> intstack = intstack;
+ vm -> intstack_ptr = intstack;
+ vm -> floatstack = floatstack;
+ vm -> floatstack_ptr = floatstack;
+ vm -> stack_max = stack_size;
+ vm -> heap = malloc(heap_size);
+ return vm;
+}
+
+void* allocate(VM* vm, int size) {
+ return malloc(size); // TMP!
+}
+
+void* allocThunk(VM* vm, int argspace) {
+ Closure* cl = allocate(vm, sizeof(ClosureType) +
+ sizeof(VAL) * (argspace + 1) +
+ sizeof(int) * 2);
+ cl -> ty = THUNK;
+ return (void*)cl;
+}
+
+void* allocCon(VM* vm, int arity) {
+ Closure* cl = allocate(vm, sizeof(ClosureType) +
+ sizeof(int) +
+ sizeof(VAL) * arity);
+ cl -> ty = CON;
+ return (void*)cl;
+}
+
+VAL mkInt(VM* vm, int val) {
+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(int));
+ cl -> ty = INT;
+ cl -> info.i = val;
+ return cl;
+}
+
+VAL mkFloat(VM* vm, double val) {
+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(double));
+ cl -> ty = FLOAT;
+ cl -> info.f = val;
+ return cl;
+}
+
+VAL mkStr(VM* vm, char* str) {
+ Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) * strlen(str));
+ cl -> ty = STRING;
+ strcpy(cl -> info.str, str);
+ return cl;
+}
+
+VAL mkThunk(VM* vm, func fn, int args, int arity) {
+ int i;
+ Closure* cl = allocThunk(vm, arity);
+ cl -> info.t.fn = fn;
+ cl -> info.t.arity = arity;
+ cl -> info.t.numargs = args;
+ VAL** argptr = &(cl -> info.t.args);
+
+ for (i = 0; i < args; ++i) {
+ VAL* v = POP;
+ *argptr++ = v;
+ }
+}
+
+VAL mkCon(VM* vm, int tag, int arity) {
+ Closure* cl = allocCon(vm, arity);
+
+ int i;
+ cl -> info.c.tag = tag;
+ VAL** argptr = &(cl -> info.c.args);
+
+ for (i = 0; i < arity; ++i) {
+ VAL* v = POP;
+ *argptr++ = v;
+ }
+
+}
+
View
@@ -0,0 +1,79 @@
+#ifndef _CLOSURE_H
+#define _CLOSURE_H
+
+
+// Closures
+typedef void* VAL;
+
+typedef struct {
+ VAL* valstack;
+ int* intstack;
+ double* floatstack;
+ VAL* valstack_ptr;
+ int* intstack_ptr;
+ double* floatstack_ptr;
+ void* heap;
+ int stack_max;
+} VM;
+
+VM* init_vm(int stack_size, size_t heap_size);
+
+// Functions all take a pointer to their VM, and return nothing.
+typedef void(*func)(VM*);
+
+typedef enum {
+ THUNK, CON, INT, FLOAT, STRING, UNIT, PTR
+} ClosureType;
+
+typedef struct {
+ VAL fn;
+ int arity;
+ int numargs;
+ VAL* args;
+} thunk;
+
+typedef struct {
+ int tag;
+ VAL* args;
+} con;
+
+typedef struct {
+ ClosureType ty;
+ union {
+ thunk t;
+ con c;
+ int i;
+ double f;
+ char* str;
+ void* ptr;
+ } info;
+} Closure;
+
+// Stack manipulation instructions
+
+#define PUSH(i) *(vm->valstack_ptr++) = i;
+#define POP --vm->valstack_ptr;
+
+#define PUSHINT(i) *(vm->intstack_ptr++) = i;
+#define POPINT --vm->intstack_ptr;
+
+#define PUSHFLOAT(i) *(vm->floatstack_ptr++) = i;
+#define POPFLOAT --vm->floatstack_ptr;
+
+#define SLIDE(n) *(vm->valstack_ptr-n) = *(vm->valstack_ptr); vm->valstack_ptr-=n;
+#define SLIDEINT(n) *(vm->intstack_ptr-n) = *(vm->intstack_ptr); vm->floatstack_ptr-=n;
+#define SLIDEFLOAT(n) *(vm->floatstack_ptr-n) = *(vm->floatstack_ptr); vm->floatstack_ptr-=n;
+
+#define DISCARD(n) vm->valstack_ptr-=n;
+#define DISCARDINT(n) vm->intstack_ptr-=n;
+#define DISCARDFLOAT(n) vm->floatstack_ptr-=n;
+
+// Creating new values (each value placed at the top of the stack)
+VAL mkInt(VM* vm, int val);
+VAL mkFloat(VM* vm, double val);
+VAL mkStr(VM* vm, char* str);
+
+VAL mkThunk(VM* vm, func fn, int args, int arity);
+VAL mkCon(VM* vm, int tag, int arity);
+
+#endif
View
@@ -23,8 +23,8 @@ idrisDef = haskellDef {
"do", "dsl", "import", "impossible",
"case", "of", "total",
"infix", "infixl", "infixr",
- "where", "with", "syntax", "proof",
- "using", "params", "namespace", "class", "instance",
+ "where", "with", "syntax", "proof", "postulate",
+ "using", "namespace", "class", "instance",
"public", "private", "abstract",
"Int", "Integer", "Float", "Char", "String", "Ptr"]
}
View
@@ -404,6 +404,8 @@ data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
data Opt = Filename String
| Ver
| Usage
+ | ShowLibs
+ | ShowIncs
| NoPrelude
| NoREPL
| OLogging Int
@@ -474,6 +476,7 @@ 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)
{-!
View
@@ -37,14 +37,14 @@ compile f tm
hdrs' <- liftIO $ mapM (inDir ddir) hdrs
let incs = map Include hdrs'
so <- getSO
- let ilib = ddir ++ "/libidris.a"
+-- let ilib = ddir ++ "/libidris.a"
case so of
Nothing ->
do m <- epicMain tm
let mainval = EpicFn (name "main") m
liftIO $ compileObjWith []
(mkProgram (incs ++ mainval : ds)) (f ++ ".o")
- liftIO $ link ((f ++ ".o") : ilib : objs ++ (map ("-l"++) libs)) f
+ liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
where checkMVs = do i <- get
case idris_metavars i \\ primDefs of
[] -> return ()
View
@@ -621,6 +621,8 @@ pAccessibility
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 ']'
View
@@ -42,6 +42,8 @@ runIdris opts =
let importdirs = opt getImportDir 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
@@ -96,6 +98,14 @@ usage = do putStrLn usagemsg
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)
@@ -107,6 +117,8 @@ 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)
@@ -131,5 +143,7 @@ usagemsg = "Idris version " ++ ver ++ "\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--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"

0 comments on commit ffc7b69

Please sign in to comment.