2ec60c8 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -3,6 +3,7 @@ New in 0.9.3:

3

4User visible changes:

5

6+* Added binding forms to syntax rules

6* Named class instances

7* Named class instances

7* Added ':set' command, with options 'errorcontext' for displaying local

8* Added ':set' command, with options 'errorcontext' for displaying local

8 variables in scope when a unification error occurs, and 'showimplicits'

9 variables in scope when a unification error occurs, and 'showimplicits'

rts/closure.c+7

@@ -1,5 +1,7 @@

1#include <stdlib.h>

2+#include <stdio.h>

2#include <string.h>

3#include <string.h>

4+#include <unistd.h>

3

5

4#include "closure.h"

6#include "closure.h"

5

7

@@ -17,6 +19,7 @@ VM* init_vm(int stack_size, size_t heap_size) {

17 vm -> floatstack_ptr = floatstack;

19 vm -> floatstack_ptr = floatstack;

18 vm -> stack_max = stack_size;

20 vm -> stack_max = stack_size;

19 vm -> heap = malloc(heap_size);

21 vm -> heap = malloc(heap_size);

22+ vm -> ret = NULL;

20 return vm;

23 return vm;

21}

24}

22

25

@@ -95,3 +98,7 @@ void EVAL(int update) {

95

98

96}

99}

97

100

101+void stackOverflow() {

102+ fprintf(stderr, "Stack overflow");

103+ exit(-1);

104+}

rts/closure.h+15−4

@@ -14,6 +14,7 @@ typedef struct {

14 double* floatstack_ptr;

15 void* heap;

16 int stack_max;

17+ VAL ret;

17} VM;

18} VM;

18

19

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

20VM* init_vm(int stack_size, size_t heap_size);

@@ -21,6 +22,15 @@ VM* init_vm(int stack_size, size_t heap_size);

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

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

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

23typedef void(*func)(VM*);

23

24

25+#define EXTEND(n) if (vm->valstack_ptr-vm->valstack + n < vm -> stack_max) \

26+ { vm->valstack_ptr+=(n) } else { stackOverflow(vm); }

27+#define CLEAR(n) vm->valstack_ptr-=(n)

28+#define SLIDE(drop, keep) \

29+ for (i=1; i<=keep; ++i) { \

30+ *(vm->valstack_ptr-i-drop) = *(vm->valstack_ptr-i); \

31+ } \

32+ vm->valstack_ptr-=(drop)

33+

24typedef enum {

34typedef enum {

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

35 THUNK, CON, INT, FLOAT, STRING, UNIT, PTR

26} ClosureType;

36} ClosureType;

@@ -60,10 +70,6 @@ typedef struct {

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

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

61#define POPFLOAT --vm->floatstack_ptr;

71#define POPFLOAT --vm->floatstack_ptr;

62

72

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;

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

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

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

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

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

@@ -78,4 +84,9 @@ VAL mkCon(VM* vm, int tag, int arity);

78

84

79void EVAL(int update);

85void EVAL(int update);

80

86

87+// Handle stack overflow.

88+// Just reports an error and exits.

89+

90+void stackOverflow();

91+

81#endif

92#endif

src/Idris/AbsSyntax.hs+1

@@ -790,6 +790,7 @@ deriving instance Binary Syntax

790

791data SSymbol = Keyword Name

792 | Symbol String

793+ | Binding Name

793 | Expr Name

794 | Expr Name

794 | SimpleExpr Name

795 | SimpleExpr Name

795 deriving Show

796 deriving Show

src/Idris/IBC.hs+4

@@ -1408,6 +1408,8 @@ instance Binary SSymbol where

1408 put x1

1409 SimpleExpr x1 -> do putWord8 3

1410 put x1

1411+ Binding x1 -> do putWord8 4

1412+ put x1

1411 get

1413 get

1412 = do i <- getWord8

1414 = do i <- getWord8

1413 case i of

1415 case i of

@@ -1419,4 +1421,6 @@ instance Binary SSymbol where

1419 return (Expr x1)

1421 return (Expr x1)

1420 3 -> do x1 <- get

1422 3 -> do x1 <- get

1421 return (SimpleExpr x1)

1423 return (SimpleExpr x1)

1424+ 4 -> do x1 <- get

1425+ return (Binding x1)

1422 _ -> error "Corrupted binary data for SSymbol"

1426 _ -> error "Corrupted binary data for SSymbol"

src/Idris/Parser.hs+16−6

@@ -397,6 +397,8 @@ pSyntaxRule syn

397pSynSym :: IParser SSymbol

398pSynSym = try (do lchar '['; n <- pName; lchar ']'

399 return (Expr n))

400+ <|> try (do lchar '{'; n <- pName; lchar '}'

401+ return (Binding n))

400 <|> do n <- iName []

402 <|> do n <- iName []

401 return (Keyword n)

403 return (Keyword n)

402 <|> do sym <- strlit

404 <|> do sym <- strlit

@@ -556,6 +558,8 @@ pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules

556 valid (Rule _ _ TermSyntax) = not (inPattern syn)

558 valid (Rule _ _ TermSyntax) = not (inPattern syn)

557

559

558

560

561+data SynMatch = SynTm PTerm | SynBind Name

562+

559pExt :: SyntaxInfo -> Syntax -> IParser PTerm

563pExt :: SyntaxInfo -> Syntax -> IParser PTerm

560pExt syn (Rule ssym ptm _)

564pExt syn (Rule ssym ptm _)

561 = do smap <- mapM pSymbol ssym

565 = do smap <- mapM pSymbol ssym

@@ -564,21 +568,27 @@ pExt syn (Rule ssym ptm _)

564 where

568 where

565 pSymbol (Keyword n) = do reserved (show n); return Nothing

569 pSymbol (Keyword n) = do reserved (show n); return Nothing

566 pSymbol (Expr n) = do tm <- pExpr syn

570 pSymbol (Expr n) = do tm <- pExpr syn

567− return $ Just (n, tm)

571+ return $ Just (n, SynTm tm)

568 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn

572 pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn

569− return $ Just (n, tm)

573+ return $ Just (n, SynTm tm)

574+ pSymbol (Binding n) = do b <- pName

575+ return $ Just (n, SynBind b)

570 pSymbol (Symbol s) = do symbol s

576 pSymbol (Symbol s) = do symbol s

571 return Nothing

577 return Nothing

572 dropn n [] = []

578 dropn n [] = []

573 dropn n ((x,t) : xs) | n == x = xs

579 dropn n ((x,t) : xs) | n == x = xs

574 | otherwise = (x,t):dropn n xs

580 | otherwise = (x,t):dropn n xs

575

581

582+ updateB ns n = case lookup n ns of

583+ Just (SynBind t) -> t

584+ _ -> n

585+

576 update ns (PRef fc n) = case lookup n ns of

586 update ns (PRef fc n) = case lookup n ns of

577− Just t -> t

587+ Just (SynTm t) -> t

578 _ -> PRef fc n

588 _ -> PRef fc n

579− update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)

589+ update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

580− update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)

590+ update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)

581− update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)

591+ update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)

582 (update (dropn n ns) sc)

592 (update (dropn n ns) sc)

583 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

593 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

584 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

594 update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)

src/RTS/Bytecode.hs+13−11

@@ -11,7 +11,7 @@ import Control.Monad.State

11

12type Local = Int

13

14−data BAtom = BP Name | BL Local | BC Const

14+data BAtom = BP Name Int | BL Local | BC Const

15 deriving Show

16

17-- Like SC, but with explicit evaluation, de Bruijn levels for locals, and all

@@ -38,12 +38,12 @@ data BAlt = BConCase Tag [Name] Int Bytecode

38 deriving Show

39

40bcdefs :: [(Name, SCDef)] -> [(Name, (Int, Bytecode))]

41−bcdefs = map (\ (n, s) -> (n, bc s))

41+bcdefs xs = map (\ (n, s) -> (n, bc xs s)) xs

42

43−bc (SCDef args max c) = (length args,

43+bc all (SCDef args max c) = (length args,

44− BGetArgs (map fst args) (bcExp max (length args) c))

44+ BGetArgs (map fst args) (bcExp all max (length args) c))

45

46−bcExp v arity x

46+bcExp all v arity x

47 = let (code, max) = runState (bc' True arity x) v

48 space = max - arity in

49 if (space > 0) then BReserve space code else code

@@ -53,14 +53,16 @@ bcExp v arity x

53 next = do s <- get

54 put (s + 1)

55 return s

56−

56+ scarity n = case lookup n all of

57+ Just (SCDef args _ _) -> length args

58+

57 bc' :: Bool -> Int -> SCExp -> State Int Bytecode

59 bc' :: Bool -> Int -> SCExp -> State Int Bytecode

58− bc' tl d (SRef n) = if tl then return $ BTailApp (BP n) []

60+ bc' tl d (SRef n) = if tl then return $ BTailApp (BP n (scarity n)) []

59− else return $ BApp (BP n) []

61+ else return $ BApp (BP n (scarity n)) []

60 bc' tl d (SLoc i) = do ref i; return $ BAtom (BL i)

62 bc' tl d (SLoc i) = do ref i; return $ BAtom (BL i)

61 bc' tl d (SApp f args)

63 bc' tl d (SApp f args)

62 = do f' <- case f of

64 = do f' <- case f of

63− SRef n -> return $ BAtom (BP n)

65+ SRef n -> return $ BAtom (BP n (scarity n))

64 _ -> bc' False d f

66 _ -> bc' False d f

65 args' <- mapM (bc' False d) args

67 args' <- mapM (bc' False d) args

66 let bapp = if tl then BTailApp else BApp

68 let bapp = if tl then BTailApp else BApp

@@ -69,8 +71,8 @@ bcExp v arity x

69 bc -> do v <- next

71 bc -> do v <- next

70 mkApp (\x -> BLet v bc (bapp (BL v) x)) args' []

72 mkApp (\x -> BLet v bc (bapp (BL v) x)) args' []

71 bc' tl d (SLazyApp f args) = do args' <- mapM (bc' False d) args

73 bc' tl d (SLazyApp f args) = do args' <- mapM (bc' False d) args

72− let bapp = if tl then BTailApp else BApp

74+ -- let bapp = if tl then BTailApp else BApp

73− mkApp (\x -> bapp (BP f) x) args' []

75+ mkApp (\x -> BLazy (BP f (scarity f)) x) args' []

74 bc' tl d (SLet n val sc) = do v' <- bc' False d val

76 bc' tl d (SLet n val sc) = do v' <- bc' False d val

75 sc' <- bc' False (d + 1) sc

77 sc' <- bc' False (d + 1) sc

76 return $ BLet d v' sc'

78 return $ BLet d v' sc'

src/RTS/CodegenC.hs+57−3

@@ -17,6 +17,7 @@ import System.Process

17import System.IO

18import System.Directory

19import System.Environment

20+import Debug.Trace

20

21

21import Paths_idris

22import Paths_idris

22

23

@@ -72,18 +73,19 @@ codegenC :: Name -> Int -> PreC -> String

72codegenC n args prec

73codegenC n args prec

73 = "/* " ++ show prec ++ " */\n\n" ++

74 = "/* " ++ show prec ++ " */\n\n" ++

74 "void " ++ cname n ++ "(VM* vm) {\n" ++

75 "void " ++ cname n ++ "(VM* vm) {\n" ++

76+ indent 1 ++ "int i;\n" ++

75 concatMap (cg 1) prec ++ "}\n\n"

77 concatMap (cg 1) prec ++ "}\n\n"

76

78

77indent i = take (i * 4) (repeat ' ')

79indent i = take (i * 4) (repeat ' ')

78

80

79reg RVal = "vm->ret"

81reg RVal = "vm->ret"

80−reg (LVar v) = "*(vm->stack-" ++ show v ++ ")"

82+reg (LVar v) = "*(vm->valstack_ptr-" ++ show v ++ ")"

81

83

82catom :: CAtom -> String

84catom :: CAtom -> String

83catom (CL l) = reg (LVar l)

85catom (CL l) = reg (LVar l)

84catom (CC (I i)) = "MKINT(" ++ show i ++ ")"

86catom (CC (I i)) = "MKINT(" ++ show i ++ ")"

85catom (CC v) = "const(" ++ show v ++ ")"

87catom (CC v) = "const(" ++ show v ++ ")"

86−catom (CP n) = cname n

88+catom (CP n i) = "MKCLOSURE(" ++ cname n ++ ", " ++ show i ++ ")"

87

89

88off o (CL i) = CL (i + o)

90off o (CL i) = CL (i + o)

89off o x = x

91off o x = x

@@ -111,6 +113,22 @@ assignFn i r f args

111 setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "

113 setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "

112 ++ setArgs (i + 1) as

114 ++ setArgs (i + 1) as

113

115

116+assignClosure i lazy r atom args

117+ = indent i ++ reg r ++ " = APPLY(" ++ catom atom ++ ", " ++ show (length args) ++

118+ ");\n" ++

119+ indent i ++ setArgs 0 args ++ "\n" ++

120+ if not lazy then

121+ indent i ++ "if (READY(" ++ reg r ++ ")) {\n" ++

122+ indent (i + 1) ++ reg r ++ " = EVAL(" ++ reg r ++ ");\n" ++

123+ indent i ++ "} else {\n" ++

124+ indent (i + 1) ++ "// do nothing \n" ++

125+ indent i ++ "}\n"

126+ else ""

127+ where

128+ setArgs i [] = ""

129+ setArgs i (a : as) = "ADDARG(" ++ show i ++ ", " ++ reg r ++ ", " ++ catom a ++ "); "

130+ ++ setArgs (i + 1) as

131+

114doTailCall i d f args

132doTailCall i d f args

115 = indent i ++ "EXTEND(" ++ show (length args) ++ ");\n" ++

133 = indent i ++ "EXTEND(" ++ show (length args) ++ ");\n" ++

116 indent i ++ setArgs 1 (map (off (length args)) (reverse args)) ++ "\n" ++

134 indent i ++ setArgs 1 (map (off (length args)) (reverse args)) ++ "\n" ++

@@ -121,11 +139,36 @@ doTailCall i d f args

121 setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "

139 setArgs i (a : as) = reg (LVar i) ++ " = " ++ catom a ++ "; "

122 ++ setArgs (i + 1) as

140 ++ setArgs (i + 1) as

123

141

142+assignFCall i r cfn rt args

143+ = indent i ++ reg r ++ " = " ++ fromC rt ++

144+ "(" ++

145+ cfn ++ "(" ++ showSep ", " (map toCa args) ++ "))" ++ ";\n"

146+ where fromC (Just IType) = "MKINT"

147+ fromC (Just StrType) = "MKSTR"

148+ fromC _ = "MKVAL"

149+

150+ toC (Just IType) = "GETINT"

151+ toC (Just StrType) = "GETSTR"

152+ toC _ = "GETVAL"

153+

154+ toCa (a, ty) = toC ty ++ "(" ++ catom a ++ ")"

155+

156+assignPrimOp i r p args

157+ = indent i ++ reg r ++ " = " ++ op p args ++ ";\n"

158+

124cg :: Int -> CInst -> String

159cg :: Int -> CInst -> String

125cg i (ASSIGN r (CCon t args))

160cg i (ASSIGN r (CCon t args))

126 = assignCon i r t args

161 = assignCon i r t args

127cg i (ASSIGN r (CExactApp f args))

162cg i (ASSIGN r (CExactApp f args))

128 = assignFn i r f args

163 = assignFn i r f args

164+cg i (ASSIGN r (CApp f args))

165+ = assignClosure i False r f args

166+cg i (ASSIGN r (CLazy f args))

167+ = assignClosure i True r f args

168+cg i (ASSIGN r (CFCall cfn rt args))

169+ = assignFCall i r cfn rt args

170+cg i (ASSIGN r (CPrimOp p args))

171+ = assignPrimOp i r p args

129cg i (ASSIGN r (CAtom e)) = indent i ++ reg r ++ " = " ++ catom e ++ ";\n"

172cg i (ASSIGN r (CAtom e)) = indent i ++ reg r ++ " = " ++ catom e ++ ";\n"

130cg i (RESERVE s) = indent i ++ "EXTEND(" ++ show s ++ ");\n"

173cg i (RESERVE s) = indent i ++ "EXTEND(" ++ show s ++ ");\n"

131cg i (CLEAR s) = indent i ++ "CLEAR(" ++ show s ++ ");\n"

174cg i (CLEAR s) = indent i ++ "CLEAR(" ++ show s ++ ");\n"

@@ -145,9 +188,10 @@ cg i (SWITCH v bs def)

145 branch (t, c) = indent i ++ "case " ++ show t ++ ":\n" ++

188 branch (t, c) = indent i ++ "case " ++ show t ++ ":\n" ++

146 concatMap (cg (i+1)) c ++

189 concatMap (cg (i+1)) c ++

147 indent (i+1) ++ "break;\n"

190 indent (i+1) ++ "break;\n"

191+cg i (TAILCALL d f args) = assignClosure i False RVal f args -- doTailClosure i d f args

148cg i (TAILCALLEXACT d f args) = doTailCall i d f args

192cg i (TAILCALLEXACT d f args) = doTailCall i d f args

149cg i (ERROR s) = indent i ++ "ERROR(" ++ show s ++ ")\n";

193cg i (ERROR s) = indent i ++ "ERROR(" ++ show s ++ ")\n";

150−cg i _ = indent i ++ "NOT DONE;\n"

194+cg i x = trace (show x ++ " not done") $ indent i ++ "NOT DONE;\n"

151

195

152cname :: Name -> String

196cname :: Name -> String

153cname (UN s) = "_I_" ++ toC s

197cname (UN s) = "_I_" ++ toC s

@@ -162,3 +206,13 @@ toC s = concatMap special s

162proto :: Name -> String

206proto :: Name -> String

163proto n = "void " ++ cname n ++ "(VM* vm);\n"

207proto n = "void " ++ cname n ++ "(VM* vm);\n"

164

208

209+op AddI [l, r] = "INTOP(+, " ++ catom l ++ ", " ++ catom r ++ ")"

210+op SubI [l, r] = "INTOP(-, " ++ catom l ++ ", " ++ catom r ++ ")"

211+op MulI [l, r] = "INTOP(*, " ++ catom l ++ ", " ++ catom r ++ ")"

212+op DivI [l, r] = "INTOP(/, " ++ catom l ++ ", " ++ catom r ++ ")"

213+

214+op ConcatS [l,r] = "CONCAT(" ++ catom l ++ ", " ++ catom r ++ ")"

215+

216+op o args = trace (show (op, args) ++ " operator undefined")

217+ $ "0 /* Op not defined " ++ show o ++ " */"

218+

src/RTS/PreC.hs+7−8

@@ -9,7 +9,7 @@ import RTS.SC

9

10import Control.Monad.State

11

12−data CAtom = CP Name | CL Local | CC Const

12+data CAtom = CP Name Int | CL Local | CC Const

13 deriving Show

14

15data CExp = CAtom CAtom

@@ -46,19 +46,18 @@ type PreC = [CInst]

46preCdefs :: [(Name, (Int, Bytecode))] -> [(Name, (Int, PreC))]

47preCdefs xs = map (\ (n, (i, b)) -> (n, preC xs b)) xs

48

49−atom res (BP n) = CP n

49+atom res (BP n i) = CP n i

50−atom res (BL n) = CL (res - n)

50+atom res (BL n) = CL (res - n)

51−atom res (BC c) = CC c

51+atom res (BC c) = CC c

52

53preC :: [(Name, (Int, Bytecode))] -> Bytecode -> (Int, PreC)

54preC all (BGetArgs ns bc) = (length ns, pc RVal (length ns) bc)

55 where arity n = do (i, b) <- lookup n all

56 return i

57− exact (BP n) as = case arity n of

58− Just i -> i == length as

57+ exact (BP n i) as = i == length as

59− Nothing -> False

60 exact _ as = False

58 exact _ as = False

59+

61− getName (BP n) = n

60+ getName (BP n i) = n

62

61

63 pc loc d (BAtom b) = [ASSIGN loc (CAtom (atom d b))]

62 pc loc d (BAtom b) = [ASSIGN loc (CAtom (atom d b))]

64 pc loc d (BApp f as)

63 pc loc d (BApp f as)

test/README+1

@@ -12,3 +12,4 @@ Tests:

12010: total

13011: record projection and update

14012: various error regressions

15+013: binding syntax

test/test013/expectednew file+12

@@ -0,0 +1,12 @@

1+Counting:

2+Number 1

3+Number 2

4+Number 3

5+Number 4

6+Number 5

7+Number 6

8+Number 7

9+Number 8

10+Number 9

11+Number 10

12+Done!

test/test013/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris test013.idr -o test013

3+./test013

4+rm -f test013 test013.ibc

test/test013/test013.idrnew file+15

@@ -0,0 +1,15 @@

1+module main

2+

3+forLoop : List a -> (a -> IO ()) -> IO ()

4+forLoop [] f = return ()

5+forLoop (x :: xs) f = do f x

6+ forLoop xs f

7+

8+syntax for {x} "in" [xs] [body] = forLoop xs (\x => body)

9+

10+main : IO ()

11+main = do putStrLn "Counting:"

12+ for x in [1..10] do

13+ putStrLn $ "Number " ++ show x

14+ putStrLn "Done!"

15+

tutorial/syntax.tex+24−1

@@ -41,7 +41,10 @@ be valid identifiers

41and \texttt{[e]} here, which stand for arbitrary expressions. To avoid parsing ambiguities,

42these expressions cannot use syntax extensions at the top level (though they can be used

43in parentheses).

44+\item \textbf{Names} --- included in braces, which stand for names which may be bound

45+on the right hand side.

44−\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}

46+\item \textbf{Symbols} --- included in quotations marks, e.g. \texttt{":="}. This can

47+also be used to include reserved words in syntax rules, such as \texttt{"let"} or \texttt{"in"}.

45\end{itemize}

48\end{itemize}

46

49

47\noindent

50\noindent

@@ -92,5 +95,25 @@ term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma

92In terms, the syntax \texttt{[x...y]} will generate a proof obligation

95In terms, the syntax \texttt{[x...y]} will generate a proof obligation

93\texttt{bounds\_lemma} (possibly renamed).

96\texttt{bounds\_lemma} (possibly renamed).

94

97

98+Finally, syntax rules may be used to introduce alternative binding forms. For

99+exampe, a \texttt{for} loop binds a variable on each iteration:

100+

101+\begin{SaveVerbatim}{forloop}

102+

103+syntax for {x} "in" [xs] [body] = forLoop xs (\x => body)

104+

105+main : IO ()

106+main = do for x in [1..10] do

107+ putStrLn ("Number " ++ show x)

108+ putStrLn "Done!"

109+

110+\end{SaveVerbatim}

111+\useverb{forloop}

112+

113+\noindent

114+Note that we have used the \texttt{\{x\}} form to state that \texttt{x} represents

115+a bound variable, substituted on the right hand side. We have also put \texttt{"in"} in

116+quotation marks since it is already a reserved word.

117+

95\input{dsl}

118\input{dsl}

96

119