ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Edwin Brady 2012-05-30 11:32:57 +02:00
parent 0e997eeb09
commit 2ec60c8f2b
14 changed files with 177 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CHANGELOG
View File

@ -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'

7
rts/closure.c
View File

@ -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);
}

19
rts/closure.h
View File

@ -14,6 +14,7 @@ typedef struct {
double* floatstack_ptr;
void* heap;
int stack_max;
VAL ret;
} VM;
VM* init_vm(int stack_size, size_t heap_size);
@ -21,6 +22,15 @@ 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

1
src/Idris/AbsSyntax.hs
View File

@ -790,6 +790,7 @@ deriving instance Binary Syntax
data SSymbol = Keyword Name
| Symbol String
| Binding Name
| Expr Name
| SimpleExpr Name
deriving Show

4
src/Idris/IBC.hs
View File

@ -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"

22
src/Idris/Parser.hs
View File

@ -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)

24
src/RTS/Bytecode.hs
View File

@ -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'

60
src/RTS/CodegenC.hs
View File

@ -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 ++ " */"

15
src/RTS/PreC.hs
View File

@ -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)

1
test/README
View File

@ -12,3 +12,4 @@ Tests:
010: total
011: record projection and update
012: various error regressions
013: binding syntax

12
test/test013/expected Normal file
View File

@ -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!

4
test/test013/run Executable file
View File

@ -0,0 +1,4 @@
#!/bin/bash
idris test013.idr -o test013
./test013
rm -f test013 test013.ibc

15
test/test013/test013.idr Normal file
View File

@ -0,0 +1,15 @@
module main
forLoop : List a -> (a -> IO ()) -> IO ()
forLoop [] f = return ()
forLoop (x :: xs) f = do f x
forLoop xs f
syntax for {x} "in" [xs] [body] = forLoop xs (\x => body)
main : IO ()
main = do putStrLn "Counting:"
for x in [1..10] do
putStrLn $ "Number " ++ show x
putStrLn "Done!"

25
tutorial/syntax.tex
View File

@ -41,7 +41,10 @@ be valid identifiers
and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities,
these expressions cannot use syntax extensions at the top level (though they can be used
in parentheses).
\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}
\item \textbf{Names} --- included in braces, which stand for names which may be bound
on the right hand side.
\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}. This can
also be used to include reserved words in syntax rules, such as \texttt{"let"} or \texttt{"in"}.
\end{itemize}
\noindent
@ -92,5 +95,25 @@ term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
In terms, the syntax \texttt{[x...y]} will generate a proof obligation
\texttt{bounds\_lemma} (possibly renamed).
Finally, syntax rules may be used to introduce alternative binding forms. For
exampe, a \texttt{for} loop binds a variable on each iteration:
\begin{SaveVerbatim}{forloop}
syntax for {x} "in" [xs] [body] = forLoop xs (\x => body)
main : IO ()
main = do for x in [1..10] do
putStrLn ("Number " ++ show x)
putStrLn "Done!"
\end{SaveVerbatim}
\useverb{forloop}
\noindent
Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents
a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in
quotation marks since it is already a reserved word.
\input{dsl}