git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3522 from ziman/fix-lam-to-let

Support nested lambdas in lamToLet.

commit1963600d1f8fb31007e0cb4a6a61642787f3ee5c authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateWed 23 Nov 2016, 11:49 (10 years ago) parent078c167ddd53cd
6 files changed+29−3
compare with master
unifiedsplit
src/Idris/Erasure.hs+11−2 test/TestData.hs+2−1 test/reg076/expected+1 test/reg076/input test/reg076/reg076.idr+11 test/reg076/run+4
src/Idris/Erasure.hs+11−2
@@ -497,9 +497,18 @@ buildDepMap ci used externs ctx startNames
497497 Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n
498498
499499 -- convert applications of lambdas to lets
500− -- Note that this transformation preserves de bruijn numbering
500+ -- note that this transformation preserves de bruijn numbering
501501 lamToLet :: Term -> Term
502− lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm
502+ lamToLet tm = lamToLet' args f
503+ where
504+ (f, args) = unApply tm
505+
506+ lamToLet' :: [Term] -> Term -> Term
507+ lamToLet' (v:vs) (Bind n (Lam ty) tm) = Bind n (Let ty v) $ lamToLet' vs tm
508+ lamToLet' [] tm = tm
509+ lamToLet' vs tm = error $
510+ "Erasure.hs:lamToLet': unexpected input: "
511+ ++ "vs = " ++ show vs ++ ", tm = " ++ show tm
503512
504513 -- split "\x_i -> T(x_i)" into [x_i] and T
505514 unfoldLams :: Term -> ([Name], Term)
test/TestData.hs+2−1
@@ -240,7 +240,8 @@ testFamiliesData = [
240240 ( 48, ANY ),
241241 ( 52, C_CG ),
242242 ( 67, ANY ),
243− ( 75, ANY )]),
243+ ( 75, ANY ),
244+ ( 76, ANY )]),
244245 ("regression", "Regression",
245246 [ ( 1 , ANY ),
246247 ( 2 , ANY )]),
test/reg076/expectednew file+1
@@ -0,0 +1 @@
1+3
test/reg076/inputnew file

No changes to the content.

test/reg076/reg076.idrnew file+11
@@ -0,0 +1,11 @@
1+data Op = Add | Mul
2+
3+binop : Op -> Integer -> Integer -> Integer
4+binop Add = (+)
5+binop Mul = (*)
6+
7+doOp : Op -> IO Integer
8+doOp op = pure (binop op 1 2)
9+
10+main : IO ()
11+main = doOp Add >>= print
test/reg076/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --port none reg076.idr -o reg076
3+./reg076
4+rm -f *.ibc reg076