32cc7dc · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -310,6 +310,9 @@ Extra-source-files:

310 test/reg066/run

311 test/reg066/*.idr

312 test/reg066/expected

313+ test/reg067/run

314+ test/reg067/*.idr

315+ test/reg067/expected

313

316

314 test/basic001/run

317 test/basic001/run

315 test/basic001/*.idr

318 test/basic001/*.idr

src/Idris/Erasure.hs+3−6

@@ -414,7 +414,7 @@ buildDepMap ci used externs ctx startNames

414 V i -> snd (bs !! i) cd `union` unconditionalDeps args

415

416 -- we interpret applied lambdas as lets in order to reuse code here

417− Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)

417+ Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet app)

418

419 -- and we interpret applied lets as lambdas

420 Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

@@ -491,11 +491,8 @@ buildDepMap ci used externs ctx startNames

491

492 -- convert applications of lambdas to lets

493 -- Note that this transformation preserves de bruijn numbering

494− lamToLet :: [Term] -> Term -> Term

494+ lamToLet :: Term -> Term

495− lamToLet xs (App _ f x) = lamToLet (x:xs) f

496− lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)

495+ lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm

497− lamToLet (x:xs) t = App Complete (lamToLet xs t) x

498− lamToLet [] t = t

499

496

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

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

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

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

test/reg067/expectednew file+1

@@ -0,0 +1 @@

1+tst2["as"]

test/reg067/reg067.idrnew file+23

@@ -0,0 +1,23 @@

1+module Main

2+

3+-- https://github.com/idris-lang/Idris-dev/issues/2844

4+main_2844 : IO ()

5+main_2844 =

6+ let

7+ f =

8+ the

9+ ((String,String) -> String -> (String, Maybe String ))

10+ (\(_,s),y => (s, Just s))

11+ in

12+ case snd $ f ("tst","tst2") "cenas" of

13+ Just z => putStr z

14+

15+-- https://github.com/idris-lang/Idris-dev/issues/2493

16+main_2493 : IO ()

17+main_2493 = printLn $ doThing [1,2,3] [("as",1),("asasasas",4)]

18+ where

19+ doThing : List Nat -> List (v,Nat) -> List v

20+ doThing is g = foldr (\(v,i),res => if elem i is then v::res else res) List.Nil g

21+

22+main : IO ()

23+main = main_2844 *> main_2493

test/reg067/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+rm -f *.ibc reg067

3+idris $@ reg067.idr -o reg067 --warnreach

4+./reg067

5+rm -f *.ibc reg067