Permalink
Browse files

Added binding form to syntax rules (and updated tutorial accordingly)

  • Loading branch information...
Edwin Brady
Edwin Brady committed May 30, 2012
1 parent 0e997ee commit 2ec60c8f2b14f80694735a933e800b00d5af6342
Showing with 177 additions and 33 deletions.
  1. +1 −0 CHANGELOG
  2. +7 −0 rts/closure.c
  3. +15 −4 rts/closure.h
  4. +1 −0 src/Idris/AbsSyntax.hs
  5. +4 −0 src/Idris/IBC.hs
  6. +16 −6 src/Idris/Parser.hs
  7. +13 −11 src/RTS/Bytecode.hs
  8. +57 −3 src/RTS/CodegenC.hs
  9. +7 −8 src/RTS/PreC.hs
  10. +1 −0 test/README
  11. +12 −0 test/test013/expected
  12. +4 −0 test/test013/run
  13. +15 −0 test/test013/test013.idr
  14. +24 −1 tutorial/syntax.tex
View
@@ -3,6 +3,7 @@ New in 0.9.3:
User visible changes:
+* Added binding forms to syntax rules
* Named class instances
* Added ':set' command, with options 'errorcontext' for displaying local
variables in scope when a unification error occurs, and 'showimplicits'
View
@@ -1,5 +1,7 @@
#include <stdlib.h>
+#include <stdio.h>
#include <string.h>
+#include <unistd.h>
#include "closure.h"
@@ -17,6 +19,7 @@ VM* init_vm(int stack_size, size_t heap_size) {
vm -> floatstack_ptr = floatstack;
vm -> stack_max = stack_size;
vm -> heap = malloc(heap_size);
+ vm -> ret = NULL;
return vm;
}
@@ -95,3 +98,7 @@ void EVAL(int update) {
}
+void stackOverflow() {
+ fprintf(stderr, "Stack overflow");
+ exit(-1);
+}
View
@@ -14,13 +14,23 @@ typedef struct {
double* floatstack_ptr;
void* heap;
int stack_max;
+ VAL ret;
} 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*);
+#define EXTEND(n) if (vm->valstack_ptr-vm->valstack + n < vm -> stack_max) \
+ { vm->valstack_ptr+=(n) } else { stackOverflow(vm); }
+#define CLEAR(n) vm->valstack_ptr-=(n)
+#define SLIDE(drop, keep) \
+ for (i=1; i<=keep; ++i) { \
+ *(vm->valstack_ptr-i-drop) = *(vm->valstack_ptr-i); \
+ } \
+ vm->valstack_ptr-=(drop)
+
typedef enum {
THUNK, CON, INT, FLOAT, STRING, UNIT, PTR
} ClosureType;
@@ -60,10 +70,6 @@ typedef struct {
#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;
@@ -78,4 +84,9 @@ VAL mkCon(VM* vm, int tag, int arity);
void EVAL(int update);
+// Handle stack overflow.
+// Just reports an error and exits.
+
+void stackOverflow();
+
#endif
View
@@ -790,6 +790,7 @@ deriving instance Binary Syntax
data SSymbol = Keyword Name
| Symbol String
+ | Binding Name
| Expr Name
| SimpleExpr Name
deriving Show
View
@@ -1408,6 +1408,8 @@ instance Binary SSymbol where
put x1
SimpleExpr x1 -> do putWord8 3
put x1
+ Binding x1 -> do putWord8 4
+ put x1
get
= do i <- getWord8
case i of
@@ -1419,4 +1421,6 @@ instance Binary SSymbol where
return (Expr x1)
3 -> do x1 <- get
return (SimpleExpr x1)
+ 4 -> do x1 <- get
+ return (Binding x1)
_ -> error "Corrupted binary data for SSymbol"
View
@@ -397,6 +397,8 @@ pSyntaxRule syn
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
@@ -556,6 +558,8 @@ pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules
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
@@ -564,21 +568,27 @@ pExt syn (Rule ssym ptm _)
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)
View
@@ -11,7 +11,7 @@ import Control.Monad.State
type Local = Int
-data BAtom = BP Name | BL Local | BC Const
+data BAtom = BP Name Int | BL Local | BC Const
deriving Show
-- Like SC, but with explicit evaluation, de Bruijn levels for locals, and all
@@ -38,12 +38,12 @@ data BAlt = BConCase Tag [Name] Int Bytecode
deriving Show
bcdefs :: [(Name, SCDef)] -> [(Name, (Int, Bytecode))]
-bcdefs = map (\ (n, s) -> (n, bc s))
+bcdefs xs = map (\ (n, s) -> (n, bc xs s)) xs
-bc (SCDef args max c) = (length args,
- BGetArgs (map fst args) (bcExp max (length args) c))
+bc all (SCDef args max c) = (length args,
+ BGetArgs (map fst args) (bcExp all max (length args) c))
-bcExp v arity x
+bcExp all v arity x
= let (code, max) = runState (bc' True arity x) v
space = max - arity in
if (space > 0) then BReserve space code else code
@@ -53,14 +53,16 @@ bcExp v arity x
next = do s <- get
put (s + 1)
return s
-
+ scarity n = case lookup n all of
+ Just (SCDef args _ _) -> length args
+
bc' :: Bool -> Int -> SCExp -> State Int Bytecode
- bc' tl d (SRef n) = if tl then return $ BTailApp (BP n) []
- else return $ BApp (BP n) []
+ bc' tl d (SRef n) = if tl then return $ BTailApp (BP n (scarity n)) []
+ else return $ BApp (BP n (scarity n)) []
bc' tl d (SLoc i) = do ref i; return $ BAtom (BL i)
bc' tl d (SApp f args)
= do f' <- case f of
- SRef n -> return $ BAtom (BP n)
+ SRef n -> return $ BAtom (BP n (scarity n))
_ -> bc' False d f
args' <- mapM (bc' False d) args
let bapp = if tl then BTailApp else BApp
@@ -69,8 +71,8 @@ bcExp v arity x
bc -> do v <- next
mkApp (\x -> BLet v bc (bapp (BL v) x)) args' []
bc' tl d (SLazyApp f args) = do args' <- mapM (bc' False d) args
- let bapp = if tl then BTailApp else BApp
- mkApp (\x -> bapp (BP f) x) args' []
+ -- let bapp = if tl then BTailApp else BApp
+ mkApp (\x -> BLazy (BP f (scarity f)) x) args' []
bc' tl d (SLet n val sc) = do v' <- bc' False d val
sc' <- bc' False (d + 1) sc
return $ BLet d v' sc'
View
@@ -17,6 +17,7 @@ import System.Process
import System.IO
import System.Directory
import System.Environment
+import Debug.Trace
import Paths_idris
@@ -72,18 +73,19 @@ codegenC :: Name -> Int -> PreC -> String
codegenC n args prec
= "/* " ++ show prec ++ " */\n\n" ++
"void " ++ cname n ++ "(VM* vm) {\n" ++
+ indent 1 ++ "int i;\n" ++
concatMap (cg 1) prec ++ "}\n\n"
indent i = take (i * 4) (repeat ' ')
reg RVal = "vm->ret"
-reg (LVar v) = "*(vm->stack-" ++ show v ++ ")"
+reg (LVar v) = "*(vm->valstack_ptr-" ++ show v ++ ")"
catom :: CAtom -> String
catom (CL l) = reg (LVar l)
catom (CC (I i)) = "MKINT(" ++ show i ++ ")"
catom (CC v) = "const(" ++ show v ++ ")"
-catom (CP n) = cname n
+catom (CP n i) = "MKCLOSURE(" ++ cname n ++ ", " ++ show i ++ ")"
off o (CL i) = CL (i + o)
off o x = x
@@ -111,6 +113,22 @@ assignFn i r f args
setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "
++ setArgs (i + 1) as
+assignClosure i lazy r atom args
+ = indent i ++ reg r ++ " = APPLY(" ++ catom atom ++ ", " ++ show (length args) ++
+ ");\n" ++
+ indent i ++ setArgs 0 args ++ "\n" ++
+ if not lazy then
+ indent i ++ "if (READY(" ++ reg r ++ ")) {\n" ++
+ indent (i + 1) ++ reg r ++ " = EVAL(" ++ reg r ++ ");\n" ++
+ indent i ++ "} else {\n" ++
+ indent (i + 1) ++ "// do nothing \n" ++
+ indent i ++ "}\n"
+ else ""
+ where
+ setArgs i [] = ""
+ setArgs i (a : as) = "ADDARG(" ++ show i ++ ", " ++ reg r ++ ", " ++ catom a ++ "); "
+ ++ setArgs (i + 1) as
+
doTailCall i d f args
= indent i ++ "EXTEND(" ++ show (length args) ++ ");\n" ++
indent i ++ setArgs 1 (map (off (length args)) (reverse args)) ++ "\n" ++
@@ -121,11 +139,36 @@ doTailCall i d f args
setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "
++ setArgs (i + 1) as
+assignFCall i r cfn rt args
+ = indent i ++ reg r ++ " = " ++ fromC rt ++
+ "(" ++
+ cfn ++ "(" ++ showSep ", " (map toCa args) ++ "))" ++ ";\n"
+ where fromC (Just IType) = "MKINT"
+ fromC (Just StrType) = "MKSTR"
+ fromC _ = "MKVAL"
+
+ toC (Just IType) = "GETINT"
+ toC (Just StrType) = "GETSTR"
+ toC _ = "GETVAL"
+
+ toCa (a, ty) = toC ty ++ "(" ++ catom a ++ ")"
+
+assignPrimOp i r p args
+ = indent i ++ reg r ++ " = " ++ op p args ++ ";\n"
+
cg :: Int -> CInst -> String
cg i (ASSIGN r (CCon t args))
= assignCon i r t args
cg i (ASSIGN r (CExactApp f args))
= assignFn i r f args
+cg i (ASSIGN r (CApp f args))
+ = assignClosure i False r f args
+cg i (ASSIGN r (CLazy f args))
+ = assignClosure i True r f args
+cg i (ASSIGN r (CFCall cfn rt args))
+ = assignFCall i r cfn rt args
+cg i (ASSIGN r (CPrimOp p args))
+ = assignPrimOp i r p args
cg i (ASSIGN r (CAtom e)) = indent i ++ reg r ++ " = " ++ catom e ++ ";\n"
cg i (RESERVE s) = indent i ++ "EXTEND(" ++ show s ++ ");\n"
cg i (CLEAR s) = indent i ++ "CLEAR(" ++ show s ++ ");\n"
@@ -145,9 +188,10 @@ cg i (SWITCH v bs def)
branch (t, c) = indent i ++ "case " ++ show t ++ ":\n" ++
concatMap (cg (i+1)) c ++
indent (i+1) ++ "break;\n"
+cg i (TAILCALL d f args) = assignClosure i False RVal f args -- doTailClosure i d f args
cg i (TAILCALLEXACT d f args) = doTailCall i d f args
cg i (ERROR s) = indent i ++ "ERROR(" ++ show s ++ ")\n";
-cg i _ = indent i ++ "NOT DONE;\n"
+cg i x = trace (show x ++ " not done") $ indent i ++ "NOT DONE;\n"
cname :: Name -> String
cname (UN s) = "_I_" ++ toC s
@@ -162,3 +206,13 @@ toC s = concatMap special s
proto :: Name -> String
proto n = "void " ++ cname n ++ "(VM* vm);\n"
+op AddI [l, r] = "INTOP(+, " ++ catom l ++ ", " ++ catom r ++ ")"
+op SubI [l, r] = "INTOP(-, " ++ catom l ++ ", " ++ catom r ++ ")"
+op MulI [l, r] = "INTOP(*, " ++ catom l ++ ", " ++ catom r ++ ")"
+op DivI [l, r] = "INTOP(/, " ++ catom l ++ ", " ++ catom r ++ ")"
+
+op ConcatS [l,r] = "CONCAT(" ++ catom l ++ ", " ++ catom r ++ ")"
+
+op o args = trace (show (op, args) ++ " operator undefined")
+ $ "0 /* Op not defined " ++ show o ++ " */"
+
View
@@ -9,7 +9,7 @@ import RTS.SC
import Control.Monad.State
-data CAtom = CP Name | CL Local | CC Const
+data CAtom = CP Name Int | CL Local | CC Const
deriving Show
data CExp = CAtom CAtom
@@ -46,19 +46,18 @@ type PreC = [CInst]
preCdefs :: [(Name, (Int, Bytecode))] -> [(Name, (Int, PreC))]
preCdefs xs = map (\ (n, (i, b)) -> (n, preC xs b)) xs
-atom res (BP n) = CP n
-atom res (BL n) = CL (res - n)
-atom res (BC c) = CC c
+atom res (BP n i) = CP n i
+atom res (BL n) = CL (res - n)
+atom res (BC c) = CC c
preC :: [(Name, (Int, Bytecode))] -> Bytecode -> (Int, PreC)
preC all (BGetArgs ns bc) = (length ns, pc RVal (length ns) bc)
where arity n = do (i, b) <- lookup n all
return i
- exact (BP n) as = case arity n of
- Just i -> i == length as
- Nothing -> False
+ exact (BP n i) as = i == length as
exact _ as = False
- getName (BP n) = n
+
+ getName (BP n i) = n
pc loc d (BAtom b) = [ASSIGN loc (CAtom (atom d b))]
pc loc d (BApp f as)
View
@@ -12,3 +12,4 @@ Tests:
010: total
011: record projection and update
012: various error regressions
+013: binding syntax
View
@@ -0,0 +1,12 @@
+Counting:
+Number 1
+Number 2
+Number 3
+Number 4
+Number 5
+Number 6
+Number 7
+Number 8
+Number 9
+Number 10
+Done!
View
@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test013.idr -o test013
+./test013
+rm -f test013 test013.ibc
Oops, something went wrong.

0 comments on commit 2ec60c8

Please sign in to comment.