93d645a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Identify tail calls while simplifying

commit93d645ac00e7a0232b0e2a8f5f310d7452724358 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 31 Aug 2012, 16:05 (14 years ago) parenteb57f08

5 files changed+44−28

compare with master

unifiedsplit

iif/testvm.iif+9−1 rts/idris_main.c+3 src/IRTS/CodegenC.hs+4 src/IRTS/LParser.hs+1 src/IRTS/Simplified.hs+27−27

iif/testvm.iif+9−1

@@ -6,6 +6,13 @@ fun plus(x, y) = case x of {

66 | S(k) => S (plus(k, y))

77 }

9+fun fact(x) = factAux(x, 1)

10+

11+fun factAux(x, acc) = case (x == 1) of {

12+ 0 => factAux(x-1, acc * x)

13+ | 1 => acc

14+ }

15+

916fun natToInt(x) = case x of {

1017 O => 0

1118 | S(k) => let y = natToInt(k) in y + 1

@@ -16,4 +23,5 @@ fun intToNat(x) = case x of {

1623 | _ => S (intToNat (x - 1))

1724 }

1825

19−fun main() = printNum(natToInt(plus(S(S(O)), intToNat(2))))

26+fun main() = printNum(natToInt(plus(intToNat(fact(6)), S(S(O)))))

27+

rts/idris_main.c+3

@@ -2,4 +2,7 @@ int main(int argc, char* argv[]) {

22 VM* vm = init_vm(1024000, 1024000);

44 _idris_main(vm, NULL);

5+#ifdef IDRIS_DEBUG

6+ printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

7+#endif

58}

src/IRTS/CodegenC.hs+4

@@ -81,6 +81,10 @@ bcc i (OP l fn args) = indent i ++ creg l ++ " = " ++ doOp fn args ++ ";\n"

8181

8282doOp LPlus [l, r] = "ADD(" ++ creg l ++ ", " ++ creg r ++ ")"

8383doOp LMinus [l, r] = "INTOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

84+doOp LTimes [l, r] = "MULT(" ++ creg l ++ ", " ++ creg r ++ ")"

85+doOp LDiv [l, r] = "INTOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

86+doOp LEq [l, r] = "INTOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

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

88+doOp LPrintStr [x] = "NULL; printf(GETSTR(" ++ creg x ++ "))"

8589doOp _ _ = "FAIL"

8690

src/IRTS/LParser.hs+1

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

5656 let h = concatMap toDecl (map fst bc)

5757 let cc = concatMap (uncurry toC) bc

5858 putStrLn "#include <idris_rts.h>\n"

59+ putStrLn "#define IDRIS_DEBUG\n"

5960 putStrLn h

6061 putStrLn cc

6162 d <- getDataDir

src/IRTS/Simplified.hs+27−27

@@ -34,29 +34,29 @@ ldefs :: State (LDefs, Int) LDefs

3434ldefs = do (l, h) <- get

3535 return l

3636

37−simplify :: LExp -> State (LDefs, Int) SExp

38−simplify (LV (Loc i)) = return (SV (Loc i))

39−simplify (LV (Glob x))

37+simplify :: Bool -> LExp -> State (LDefs, Int) SExp

38+simplify tl (LV (Loc i)) = return (SV (Loc i))

39+simplify tl (LV (Glob x))

4040 = do ctxt <- ldefs

4141 case lookupCtxt Nothing x ctxt of

4242 [LConstructor _ t 0] -> return $ SCon t x []

4343 _ -> return $ SV (Glob x)

44−simplify (LApp tc n args) = do args' <- mapM sVar args

45− mkapp (SApp tc n) args'

46−simplify (LLet n v e) = do v' <- simplify v

47− e' <- simplify e

48− return (SLet (Glob n) v' e')

49−simplify (LCon i n args) = do args' <- mapM sVar args

50− mkapp (SCon i n) args'

51−simplify (LCase e alts) = do v <- sVar e

52− alts' <- mapM sAlt alts

53− case v of

54− (x, Nothing) -> return (SCase x alts')

55− (Glob x, Just e) ->

56− return (SLet (Glob x) e (SCase (Glob x) alts'))

57−simplify (LConst c) = return (SConst c)

58−simplify (LOp p args) = do args' <- mapM sVar args

59− mkapp (SOp p) args'

44+simplify tl (LApp tc n args) = do args' <- mapM sVar args

45+ mkapp (SApp (tl || tc) n) args'

46+simplify tl (LLet n v e) = do v' <- simplify False v

47+ e' <- simplify tl e

48+ return (SLet (Glob n) v' e')

49+simplify tl (LCon i n args) = do args' <- mapM sVar args

50+ mkapp (SCon i n) args'

51+simplify tl (LCase e alts) = do v <- sVar e

52+ alts' <- mapM (sAlt tl) alts

53+ case v of

54+ (x, Nothing) -> return (SCase x alts')

55+ (Glob x, Just e) ->

56+ return (SLet (Glob x) e (SCase (Glob x) alts'))

57+simplify tl (LConst c) = return (SConst c)

58+simplify tl (LOp p args) = do args' <- mapM sVar args

59+ mkapp (SOp p) args'

6060

6161sVar (LV (Glob x))

6262 = do ctxt <- ldefs

@@ -64,7 +64,7 @@ sVar (LV (Glob x))

6464 [LConstructor _ t 0] -> sVar (LCon t x [])

6565 _ -> return (Glob x, Nothing)

6666sVar (LV x) = return (x, Nothing)

67−sVar e = do e' <- simplify e

67+sVar e = do e' <- simplify False e

6868 i <- hvar

6969 return (Glob (MN i "R"), Just e')

7070

@@ -75,12 +75,12 @@ mkapp f args = mkapp' f args [] where

7575 = do sc <- mkapp' f xs (x : args)

7676 return (SLet x e sc)

7777

78−sAlt (LConCase i n args e) = do e' <- simplify e

79− return (SConCase (-1) i n args e')

80−sAlt (LConstCase c e) = do e' <- simplify e

81− return (SConstCase c e')

82−sAlt (LDefaultCase e) = do e' <- simplify e

83− return (SDefaultCase e')

78+sAlt tl (LConCase i n args e) = do e' <- simplify tl e

79+ return (SConCase (-1) i n args e')

80+sAlt tl (LConstCase c e) = do e' <- simplify tl e

81+ return (SConstCase c e')

82+sAlt tl (LDefaultCase e) = do e' <- simplify tl e

83+ return (SDefaultCase e')

8484

8585checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, SDecl)]

8686checkDefs ctxt [] = return []

@@ -88,7 +88,7 @@ checkDefs ctxt (con@(n, LConstructor _ _ _) : xs)

8888 = do xs' <- checkDefs ctxt xs

8989 return xs'

9090checkDefs ctxt ((n, LFun n' args exp) : xs)

91− = do let sexp = evalState (simplify exp) (ctxt, 0)

91+ = do let sexp = evalState (simplify True exp) (ctxt, 0)

9292 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (-1)

9393 xs' <- checkDefs ctxt xs

9494 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')