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

CHANGELOG+1

compare with master

unifiedsplit

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

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

10 for displaying elaborated terms in full

11* Added '--errorcontext' command line switch

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

12* Various minor REPL improvements and fixes

13* Various minor REPL improvements and fixes

13

14

14Internal changes:

15Internal changes:

iif/lazy.iifnew file+21

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

1+data Nil 0

2+data Cons 2

3+

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

5+

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 ++ ")"

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

183

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

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

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

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

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

187doOp _ _ = "FAIL"

188

189tempfile :: 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))

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

48 fixApply tc n args' arity

49 [] -> 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'

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

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

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

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

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

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

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

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

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

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

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

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

69

81

70 chainAPPLY f [] = f

82 chainAPPLY f [] = f

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

83 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

52 let defuns = defunctionalise nexttag ctxtIn

53-- print defuns

54 let checked = checkDefs defuns (toAlist defuns)

55−-- print checked

55+ print checked

56 case checked of

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

58 Error e -> fail $ show e

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

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

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

119 x <- iName [];

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

120 lchar '('

121 lchar '('

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

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

122 lchar ')'

123 lchar ')'

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)

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

128+ else return (LApp tc x args))

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

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

125 <|> pLConst

130 <|> pLConst

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

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

src/IRTS/Lang.hs+1

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

7

8data LExp = LV LVar

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

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

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

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

11 | LCon Int Name [LExp]

12 | LCon Int Name [LExp]

12 | LCase LExp [LAlt]

13 | LCase LExp [LAlt]