on master help sign in
Merge branch 'fix-unsafeperformio' of https://github.com/ziman/idris into ziman-fix-unsafeperformio

Conflicts: idris.cabal

commitb2f9f854b5c4df97699f22cd1a6f97b214ab7c43 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 20 Apr 2014, 16:44 (13 years ago) parent22f47ff4ed9178
5 files changed+18
idris.cabal+3 src/Idris/Erasure.hs+1 test/reg040/expected+1 test/reg040/reg040.idr+7 test/reg040/run+6
idris.cabal+3
@@ -231,6 +231,9 @@ Extra-source-files:
231231 test/reg039/run
232232 test/reg039/*.idr
233233 test/reg039/expected
234+ test/reg040/run
235+ test/reg040/*.idr
236+ test/reg040/expected
234237 test/reg041/run
235238 test/reg041/*.idr
236239 test/reg041/expected
src/Idris/Erasure.hs+1
@@ -203,6 +203,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
203203 -- among Idris.Primitives.primitives
204204 , mn "__MkPair" [2,3]
205205 , it "prim_fork" [0]
206+ , it "unsafePerformPrimIO" [1]
206207
207208 -- believe_me is a primitive but it only uses its third argument
208209 -- it is special-cased in usedNames above
test/reg040/expectednew file+1
@@ -0,0 +1 @@
1+42
test/reg040/reg040.idrnew file+7
@@ -0,0 +1,7 @@
1+-- The regression that this tests for is defunct unsafePerformIO
2+
3+io : IO Int
4+io = return 42
5+
6+main : IO ()
7+main = print $ unsafePerformIO io
test/reg040/runnew file+6
@@ -0,0 +1,6 @@
1+#!/usr/bin/env bash
2+
3+idris --warnreach reg040.idr -o reg040
4+./reg040
5+
6+rm -f reg040 *.ibc