git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2859 from ziman/fix-segfault

Fix segfault in case-lambdas

commit32cc7dc71efcbea5e4c7019109172c0ebdae1633 authorEdwin Brady <edwin.brady@gmail.com> dateMon 14 Dec 2015, 10:08 (11 years ago) parent2767cd445e67fd
5 files changed+35−6
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Erasure.hs+3−6 test/reg067/expected+1 test/reg067/reg067.idr+23 test/reg067/run+5
idris.cabal+3
@@ -310,6 +310,9 @@ Extra-source-files:
310310 test/reg066/run
311311 test/reg066/*.idr
312312 test/reg066/expected
313+ test/reg067/run
314+ test/reg067/*.idr
315+ test/reg067/expected
313316
314317 test/basic001/run
315318 test/basic001/*.idr
src/Idris/Erasure.hs+3−6
@@ -414,7 +414,7 @@ buildDepMap ci used externs ctx startNames
414414 V i -> snd (bs !! i) cd `union` unconditionalDeps args
415415
416416 -- 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)
418418
419419 -- and we interpret applied lets as lambdas
420420 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
491491
492492 -- convert applications of lambdas to lets
493493 -- Note that this transformation preserves de bruijn numbering
494− lamToLet :: [Term] -> 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)
497− lamToLet (x:xs) t = App Complete (lamToLet xs t) x
498− lamToLet [] t = t
494+ lamToLet :: Term -> Term
495+ lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm
499496
500497 -- split "\x_i -> T(x_i)" into [x_i] and T
501498 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