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

lib/either.idr+2

compare with master

unifiedsplit

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

1+module either;

2+

1import builtins;

3import builtins;

2

4

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

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

lib/list.idr+2−3

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

1−import builtins;

1+module list;

2

3−namespace list {

3+import builtins;

4

5infixr 7 :: ;

6

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

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

39}

40

41−}

lib/maybe.idr+1−3

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

1−

2−namespace maybe {

1+module maybe;

3

2

4data Maybe a = Nothing | Just a;

3data Maybe a = Nothing | Just a;

5

4

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

11maybe_bind Nothing k = Nothing;

10maybe_bind Nothing k = Nothing;

12maybe_bind (Just x) k = k x;

11maybe_bind (Just x) k = k x;

13

12

14−}

lib/prelude.idr+2−3

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

1+module prelude;

2+

1import builtins;

3import builtins;

2import nat;

4import nat;

3import list;

5import list;

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

8

10

9-- Show and instances

11-- Show and instances

10

12

11−namespace prelude {

12−

13class Show a where {

14 show : a -> String;

15}

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

117readLine : IO String;

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

119

120−}

lib/vect.idr+2−3

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

1−import nat;

1+module vect;

2

3−namespace vect {

3+import nat;

4

5data Fin : Nat -> Set where

6 fO : Fin (S k)

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

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

36}

37

38−}

samples/interp.idr+1−3

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

1−namespace main {

1+module main;

2

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

4

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

74testFac : Int;

75testFac = interp Nil eFac 4;

76

77−}

78−

79main : IO ();

77main : IO ();

80main = print testFac;

78main = print testFac;

81

79

src/Idris/Compiler.hs+1−1

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

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

34

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

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

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

37

38class ToEpic a where

39 epic :: a -> Idris E.Term

src/Idris/Parser.hs+14−5

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

70loadSource :: FilePath -> Idris ()

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

72 file <- lift $ readFile f

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

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

74 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']

76 logLvl 3 (dumpDecls ds)

79 logLvl 3 (dumpDecls ds)

77 i <- getIState

80 i <- getIState

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

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

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

87 eof

90 eof

88 return t) i "(proof)"

91 return t) i "(proof)"

89

92

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

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

91parseImports fname input

94parseImports fname input

92 = do i <- get

95 = do i <- get

96+ case (runParser (do mname <- pHeader

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

97+ ps <- many pImport

94 rest <- getInput

98 rest <- getInput

95 pos <- getPosition

99 pos <- getPosition

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

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

97 Left err -> fail (ishow err)

101 Left err -> fail (ishow err)

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

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

99 return x

103 return x

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

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

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

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

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

103

107

108+pHeader :: IParser [String]

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

110+ return [i])

111+ <|> return []

112+

104

113

105pfc :: IParser FC

114pfc :: IParser FC

106pfc = do s <- getPosition

115pfc = do s <- getPosition

test/test001/test001.idr+1−3