57c8ed3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'module' keyword to declare default namespace. 'main' must be in namespace 'main'

commit57c8ed3ba479a36389d8736593da92cf64eb0dbd authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 29 Nov 2011, 12:04 (15 years ago) parent6bef4f9

9 files changed+26−24

compare with master

unifiedsplit

lib/either.idr+2 lib/list.idr+2−3 lib/maybe.idr+1−3 lib/prelude.idr+2−3 lib/vect.idr+2−3 samples/interp.idr+1−3 src/Idris/Compiler.hs+1−1 src/Idris/Parser.hs+14−5 test/test001/test001.idr+1−3

lib/either.idr+2

@@ -1,3 +1,5 @@

1+module either;

13import builtins;

35data Either a b = Left a | Right b;

lib/list.idr+2−3

@@ -1,6 +1,6 @@

1−import builtins;

1+module list;

3−namespace list {

3+import builtins;

55infixr 7 :: ;

@@ -38,4 +38,3 @@ filter pred (x :: xs) with (pred x, filter pred xs) {

3838 filter pred (x :: xs) | (False, fxs) = fxs;

3939}

4040

41−}

lib/maybe.idr+1−3

@@ -1,5 +1,4 @@

1−

2−namespace maybe {

1+module maybe;

43data Maybe a = Nothing | Just a;

@@ -11,4 +10,3 @@ maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b;

1110maybe_bind Nothing k = Nothing;

1211maybe_bind (Just x) k = k x;

1312

14−}

lib/prelude.idr+2−3

@@ -1,3 +1,5 @@

1+module prelude;

13import builtins;

24import nat;

35import list;

@@ -8,8 +10,6 @@ import io;

810

911-- Show and instances

1012

11−namespace prelude {

12−

1313class Show a where {

1414 show : a -> String;

1515}

@@ -117,4 +117,3 @@ print = putStrLn . show;

117117readLine : IO String;

118118readLine = mkForeign (FFun "readStr" Nil FString);

119119

120−}

lib/vect.idr+2−3

@@ -1,6 +1,6 @@

1−import nat;

1+module vect;

3−namespace vect {

3+import nat;

55data Fin : Nat -> Set where

66 fO : Fin (S k)

@@ -35,4 +35,3 @@ vfilter p (x :: xs) with (vfilter p xs) {

3535 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

3636}

3737

38−}

samples/interp.idr+1−3

@@ -1,4 +1,4 @@

1−namespace main {

1+module main;

33data Ty = TyInt | TyBool| TyFun Ty Ty;

@@ -74,8 +74,6 @@ test = interp Nil eProg 2 2;

7474testFac : Int;

7575testFac = interp Nil eFac 4;

7676

77−}

78−

7977main : IO ();

8078main = print testFac;

8179

src/Idris/Compiler.hs+1−1

@@ -33,7 +33,7 @@ ename x = name ("idris_" ++ show x)

3333aname x = name ("a_" ++ show x)

3434

3535epicMain = effect_ $ ref (ename (UN "run__IO")) @@

36− ref (ename (UN "main"))

36+ ref (ename (NS (UN "main") ["main"]))

3737

3838class ToEpic a where

3939 epic :: a -> Idris E.Term

src/Idris/Parser.hs+14−5

@@ -70,9 +70,12 @@ loadModule f

7070loadSource :: FilePath -> Idris ()

7171loadSource f = do iLOG ("Reading " ++ f)

7272 file <- lift $ readFile f

73− (modules, rest, pos) <- parseImports f file

73+ (mname, modules, rest, pos) <- parseImports f file

7474 mapM_ loadModule modules

75− ds <- parseProg defaultSyntax f rest pos

75+ ds' <- parseProg (defaultSyntax {syn_namespace = mname }) f rest pos

76+ let ds = case mname of

77+ [] -> ds'

78+ (x:_) -> [PNamespace x ds']

7679 logLvl 3 (dumpDecls ds)

7780 i <- getIState

7881 logLvl 10 (show (toAlist (idris_implicits i)))

@@ -87,13 +90,14 @@ parseTac i = runParser (do t <- pTactic defaultSyntax

8790 eof

8891 return t) i "(proof)"

8992

90−parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

93+parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)

9194parseImports fname input

9295 = do i <- get

93− case (runParser (do ps <- many pImport

96+ case (runParser (do mname <- pHeader

97+ ps <- many pImport

9498 rest <- getInput

9599 pos <- getPosition

96− return ((ps, rest, pos), i)) i fname input) of

100+ return ((mname, ps, rest, pos), i)) i fname input) of

97101 Left err -> fail (ishow err)

98102 Right (x, i) -> do put i

99103 return x

@@ -101,6 +105,11 @@ parseImports fname input

101105 fname ++ ":" ++ show ln ++ ":parse error"

102106-- show (map messageString (errorMessages err))

103107

108+pHeader :: IParser [String]

109+pHeader = try (do reserved "module"; i <- identifier; lchar ';'

110+ return [i])

111+ <|> return []

112+

104113

105114pfc :: IParser FC

106115pfc = do s <- getPosition

test/test001/test001.idr+1−3