1963600 · Idris-dev · git.iko.soy

src/Idris/Erasure.hs+11−2

compare with master

unifiedsplit

@@ -497,9 +497,18 @@ buildDepMap ci used externs ctx startNames

497 Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n

498

499 -- convert applications of lambdas to lets

500− -- Note that this transformation preserves de bruijn numbering

500+ -- note that this transformation preserves de bruijn numbering

501 lamToLet :: Term -> Term

502+ lamToLet tm = lamToLet' args f

503+ where

504+ (f, args) = unApply tm

505+

506+ lamToLet' :: [Term] -> Term -> Term

502− lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm

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

503

512

504 -- split "\x_i -> T(x_i)" into [x_i] and T

513 -- split "\x_i -> T(x_i)" into [x_i] and T

505 unfoldLams :: Term -> ([Name], Term)

514 unfoldLams :: Term -> ([Name], Term)

test/TestData.hs+2−1

@@ -240,7 +240,8 @@ testFamiliesData = [

240 ( 48, ANY ),

241 ( 52, C_CG ),

242 ( 67, ANY ),

243− ( 75, ANY )]),

243+ ( 75, ANY ),

244+ ( 76, ANY )]),

244 ("regression", "Regression",

245 ("regression", "Regression",

245 [ ( 1 , ANY ),

246 [ ( 1 , ANY ),

246 ( 2 , ANY )]),

247 ( 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