35ec145 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added lazy application to IRTS

commit35ec1456d831bcd17b10e70907ad02352d005045 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 4 Sep 2012, 20:11 (14 years ago) parent99fd819

6 files changed+44−4

compare with master

unifiedsplit

CHANGELOG+1 iif/lazy.iif+21 src/IRTS/CodegenC.hs+2−2 src/IRTS/Defunctionalise.hs+12 src/IRTS/LParser.hs+7−2 src/IRTS/Lang.hs+1

CHANGELOG+1

@@ -9,6 +9,7 @@ User visible changes:

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

1010 for displaying elaborated terms in full

1111* Added '--errorcontext' command line switch

12+* Added ':proofs' and ':rmproofs' commands

1213* Various minor REPL improvements and fixes

1314

1415Internal changes:

iif/lazy.iifnew file+21

@@ -0,0 +1,21 @@

1+data Nil 0

2+data Cons 2

4+fun countFrom(x) = Cons(x, countFrom@(x+1))

6+fun take(n, xs) = case n of {

7+ 0 => Nil

8+ | _ => case xs of {

9+ Nil => Nil

10+ | Cons(y, ys) => Cons(y, take(n-1, ys))

11+ }

12+ }

13+

14+fun dumpList(xs) = case xs of {

15+ Nil => "END"

16+ | Cons(y, ys) => %IntString(y) ++ ", " ++ dumpList(ys)

17+ }

18+

19+fun double(x) = x + x

20+

21+fun main() = %WriteString(dumpList(take(5, countFrom(10))))

src/IRTS/CodegenC.hs+2−2

@@ -182,8 +182,8 @@ doOp LFloatStr [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"

182182doOp LStrFloat [x] = "idris_castStrFloat(vm, " ++ creg x ++ ")"

183183

184184doOp LReadStr [] = "idris_readStr(vm, stdin)"

185−doOp LPrintNum [x] = "NULL; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

186−doOp LPrintStr [x] = "NULL; puts(GETSTR(" ++ creg x ++ "))"

185+doOp LPrintNum [x] = creg x ++ "; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

186+doOp LPrintStr [x] = creg x ++ "; puts(GETSTR(" ++ creg x ++ "))"

187187doOp _ _ = "FAIL"

188188

189189tempfile :: IO (FilePath, Handle)

src/IRTS/Defunctionalise.hs+12

@@ -47,6 +47,13 @@ addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))

4747 [LFun _ as _] -> let arity = length as in

4848 fixApply tc n args' arity

4949 [] -> chainAPPLY (LV (Glob n)) args'

50+ aa env (LLazyApp n args)

51+ = let args' = map (aa env) args in

52+ case lookupCtxt Nothing n defs of

53+ [LConstructor _ i ar] -> LApp False n args'

54+ [LFun _ as _] -> let arity = length as in

55+ fixLazyApply n args' arity

56+ [] -> chainAPPLY (LV (Glob n)) args'

5057 aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)

5158 aa env (LCon i n args) = LCon i n (map (aa env) args)

5259 aa env (LCase e alts) = LCase (eEVAL (aa env e)) (map (aaAlt env) alts)

@@ -66,6 +73,11 @@ addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))

6673 | length args == ar = LApp tc n args

6774 | length args < ar = LApp tc (mkUnderCon n (ar - length args)) args

6875 | length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)

76+

77+ fixLazyApply n args ar

78+ | length args == ar = LApp False (mkFnCon n) args

79+ | length args < ar = LApp False (mkUnderCon n (ar - length args)) args

80+ | length args > ar = chainAPPLY (LApp False n (take ar args)) (drop ar args)

6981

7082 chainAPPLY f [] = f

7183 chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as

src/IRTS/LParser.hs+7−2

@@ -52,7 +52,7 @@ fovm f = do defs <- parseFOVM f

5252 let defuns = defunctionalise nexttag ctxtIn

5353-- print defuns

5454 let checked = checkDefs defuns (toAlist defuns)

55−-- print checked

55+ print checked

5656 case checked of

5757 OK c -> codegenC c "a.out" True ["math.h"] "" TRACE

5858 Error e -> fail $ show e

@@ -117,10 +117,15 @@ pLExp' = try (do lchar '%'; pCast)

117117 <|> try (do lchar '%'; pPrim)

118118 <|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True)

119119 x <- iName [];

120+ lazy <- option False (do lchar '@'; return True)

120121 lchar '('

121122 args <- sepBy pLExp (lchar ',')

122123 lchar ')'

123− if null args then return (LV (Glob x)) else return (LApp tc x args))

124+ if null args

125+ then if lazy then return (LLazyApp x [])

126+ else return (LV (Glob x))

127+ else if lazy then return (LLazyApp x args)

128+ else return (LApp tc x args))

124129 <|> do lchar '('; e <- pLExp; lchar ')'; return e

125130 <|> pLConst

126131 <|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp

src/IRTS/Lang.hs+1

@@ -7,6 +7,7 @@ data LVar = Loc Int | Glob Name

88data LExp = LV LVar

99 | LApp Bool Name [LExp] -- True = tail call

10+ | LLazyApp Name [LExp] -- True = tail call

1011 | LLet Name LExp LExp -- name just for pretty printing

1112 | LCon Int Name [LExp]

1213 | LCase LExp [LAlt]