Add erasure postulates for unsafePerformPrimIO.
commit17ff3b5882015c98ce7173eaa02e9da3b5b59464
authorMatus Tejiscak <ziman@functor.sk>
dateSun 20 Apr 2014, 15:03 (13 years ago)
parente07c13d
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
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