Implicit "module Main" added
When there is no module header, it is assumed that the module is the
Main module. This is mostly to ensure all names are qualified.
%unqualified is for the (rare, and probably builtins only) case where no
name qualification is desired.
commit9aa723e0d38db89c2f3032e425fa2b4d028dffe4
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 18 Jan 2014, 22:11 (13 years ago)
parentcaed480
libs/prelude/Builtins.idr+2
@@ -1,3 +1,5 @@
1+%unqualified
2+
13%access public
24%default total
35
libs/prelude/IO.idr+2
@@ -1,3 +1,5 @@
1+%unqualified
2+
13import Prelude.List
24
35%access public
src/Idris/Parser.hs+3−1
@@ -81,7 +81,9 @@ moduleHeader = try (do reserved "module"
8181 i <- identifier
8282 option ';' (lchar ';')
8383 return (moduleName i))
84− <|> return []
84+ <|> try (do lchar '%'; reserved "unqualified"
85+ return [])
86+ <|> return (moduleName "Main")
8587 where moduleName x = case span (/='.') x of
8688 (x, "") -> [x]
8789 (x, '.':y) -> x : moduleName y
test/reg003/expected+1−6
@@ -1,7 +1,2 @@
1−reg003a.idr:4:20:When elaborating constructor ECons:
1+reg003a.idr:4:20:When elaborating constructor Main.ECons:
22No such variable OddList
3−reg003a.idr:7:20:When elaborating constructor OCons:
4−No such variable EvenList
5−reg003a.idr:9:8:When elaborating type of test:
6−No such variable EvenList
7−reg003a.idr:10:1:No type declaration for test
test/test010/expected+1−1
@@ -1,3 +1,3 @@
1−test010.idr:13:1:foo is possibly not total due to: MkBad
1+test010.idr:13:1:Main.foo is possibly not total due to: Main.MkBad
22test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad
33test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad