Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Added lazy application to IRTS

  • Loading branch information...
commit 35ec1456d831bcd17b10e70907ad02352d005045 1 parent 99fd819
Edwin Brady authored
View
1  CHANGELOG
@@ -9,6 +9,7 @@ User visible changes:
variables in scope when a unification error occurs, and 'showimplicits'
for displaying elaborated terms in full
* Added '--errorcontext' command line switch
+* Added ':proofs' and ':rmproofs' commands
* Various minor REPL improvements and fixes
Internal changes:
View
21 iif/lazy.iif
@@ -0,0 +1,21 @@
+data Nil 0
+data Cons 2
+
+fun countFrom(x) = Cons(x, countFrom@(x+1))
+
+fun take(n, xs) = case n of {
+ 0 => Nil
+ | _ => case xs of {
+ Nil => Nil
+ | Cons(y, ys) => Cons(y, take(n-1, ys))
+ }
+ }
+
+fun dumpList(xs) = case xs of {
+ Nil => "END"
+ | Cons(y, ys) => %IntString(y) ++ ", " ++ dumpList(ys)
+ }
+
+fun double(x) = x + x
+
+fun main() = %WriteString(dumpList(take(5, countFrom(10))))
View
4 src/IRTS/CodegenC.hs
@@ -182,8 +182,8 @@ doOp LFloatStr [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"
doOp LStrFloat [x] = "idris_castStrFloat(vm, " ++ creg x ++ ")"
doOp LReadStr [] = "idris_readStr(vm, stdin)"
-doOp LPrintNum [x] = "NULL; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"
-doOp LPrintStr [x] = "NULL; puts(GETSTR(" ++ creg x ++ "))"
+doOp LPrintNum [x] = creg x ++ "; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"
+doOp LPrintStr [x] = creg x ++ "; puts(GETSTR(" ++ creg x ++ "))"
doOp _ _ = "FAIL"
tempfile :: IO (FilePath, Handle)
View
12 src/IRTS/Defunctionalise.hs
@@ -47,6 +47,13 @@ addApps defs (n, LFun _ args e) = (n, LFun n args (aa args e))
[LFun _ as _] -> let arity = length as in
fixApply tc n args' arity
[] -> chainAPPLY (LV (Glob n)) args'
+ aa env (LLazyApp n args)
+ = let args' = map (aa env) args in
+ case lookupCtxt Nothing n defs of
+ [LConstructor _ i ar] -> LApp False n args'
+ [LFun _ as _] -> let arity = length as in
+ fixLazyApply n args' arity
+ [] -> chainAPPLY (LV (Glob n)) args'
aa env (LLet n v sc) = LLet n (aa env v) (aa (n : env) sc)
aa env (LCon i n args) = LCon i n (map (aa env) args)
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))
| length args == ar = LApp tc n args
| length args < ar = LApp tc (mkUnderCon n (ar - length args)) args
| length args > ar = chainAPPLY (LApp tc n (take ar args)) (drop ar args)
+
+ fixLazyApply n args ar
+ | length args == ar = LApp False (mkFnCon n) args
+ | length args < ar = LApp False (mkUnderCon n (ar - length args)) args
+ | length args > ar = chainAPPLY (LApp False n (take ar args)) (drop ar args)
chainAPPLY f [] = f
chainAPPLY f (a : as) = chainAPPLY (LApp False (MN 0 "APPLY") [f, a]) as
View
9 src/IRTS/LParser.hs
@@ -52,7 +52,7 @@ fovm f = do defs <- parseFOVM f
let defuns = defunctionalise nexttag ctxtIn
-- print defuns
let checked = checkDefs defuns (toAlist defuns)
--- print checked
+ print checked
case checked of
OK c -> codegenC c "a.out" True ["math.h"] "" TRACE
Error e -> fail $ show e
@@ -117,10 +117,15 @@ pLExp' = try (do lchar '%'; pCast)
<|> try (do lchar '%'; pPrim)
<|> try (do tc <- option False (do lchar '%'; reserved "tc"; return True)
x <- iName [];
+ lazy <- option False (do lchar '@'; return True)
lchar '('
args <- sepBy pLExp (lchar ',')
lchar ')'
- if null args then return (LV (Glob x)) else return (LApp tc x args))
+ if null args
+ then if lazy then return (LLazyApp x [])
+ else return (LV (Glob x))
+ else if lazy then return (LLazyApp x args)
+ else return (LApp tc x args))
<|> do lchar '('; e <- pLExp; lchar ')'; return e
<|> pLConst
<|> do reserved "let"; x <- iName []; lchar '='; v <- pLExp
View
1  src/IRTS/Lang.hs
@@ -7,6 +7,7 @@ data LVar = Loc Int | Glob Name
data LExp = LV LVar
| LApp Bool Name [LExp] -- True = tail call
+ | LLazyApp Name [LExp] -- True = tail call
| LLet Name LExp LExp -- name just for pretty printing
| LCon Int Name [LExp]
| LCase LExp [LAlt]
Please sign in to comment.
Something went wrong with that request. Please try again.