c997a48 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -18,7 +18,7 @@ Description: Idris is an experimental language with full dependent types.

18Cabal-Version: >= 1.6

19Build-type: Simple

20

21−Data-files: *.idr

21+Data-files: *.idr prelude/*.idr

22Data-dir: lib

23

24Executable idris

lib/Makefile−1

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

1−SRCS = prelude.idr list.idr nat.idr prelude.idr vect.idr

2

1

3check: .PHONY

2check: .PHONY

4 for x in *.idr ; do \

3 for x in *.idr ; do \

lib/io.idr+1−1

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

1−import list;

1+import prelude.list;

2

3data IO a = prim__IO a;

4

lib/prelude.idr+6−5

@@ -1,13 +1,14 @@

1module prelude;

2

3import builtins;

4−import nat;

5−import list;

6−import maybe;

7−import either;

8−import vect;

9import io;

4import io;

10

5

6+import prelude.nat;

7+import prelude.list;

8+import prelude.maybe;

9+import prelude.either;

10+import prelude.vect;

11+

11-- Show and instances

12-- Show and instances

12

13

13class Show a where {

14class Show a where {

lib/either.idr → lib/prelude/either.idrrenamed

The content is the same.

lib/list.idr → lib/prelude/list.idrrenamed

The content is the same.

lib/maybe.idr → lib/prelude/maybe.idrrenamed

The content is the same.

lib/nat.idr → lib/prelude/nat.idrrenamed+1−1

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

1−module nat;

1+module prelude.nat;

2

3import builtins;

4

lib/vect.idr → lib/prelude/vect.idrrenamed+1−1

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

1module vect;

2

3−import nat;

3+import prelude.nat;

4

5data Fin : Nat -> Set where

6 fO : Fin (S k)

src/Idris/Parser.hs+13−6

@@ -72,10 +72,9 @@ loadSource f = do iLOG ("Reading " ++ f)

72 file <- lift $ readFile f

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

74 mapM_ loadModule modules

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

75+ ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })

76+ f rest pos

76− let ds = case mname of

77+ let ds = namespaces mname ds'

77− [] -> ds'

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

79 logLvl 3 (dumpDecls ds)

78 logLvl 3 (dumpDecls ds)

80 i <- getIState

79 i <- getIState

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

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

@@ -84,6 +83,9 @@ loadSource f = do iLOG ("Reading " ++ f)

84 mapM_ (elabDecl toplevel) ds

83 mapM_ (elabDecl toplevel) ds

85 iLOG ("Finished " ++ f)

84 iLOG ("Finished " ++ f)

86 return ()

85 return ()

86+ where

87+ namespaces [] ds = ds

88+ namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

87

89

88parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

90parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

89parseTac i = runParser (do t <- pTactic defaultSyntax

91parseTac i = runParser (do t <- pTactic defaultSyntax

@@ -107,8 +109,11 @@ parseImports fname input

107

109

108pHeader :: IParser [String]

110pHeader :: IParser [String]

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

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

110− return [i])

112+ return (parseName i))

111 <|> return []

113 <|> return []

114+ where parseName x = case span (/='.') x of

115+ (x, "") -> [x]

116+ (x, '.':y) -> x : parseName y

112

117

113

118

114pfc :: IParser FC

119pfc :: IParser FC

@@ -123,7 +128,9 @@ pImport :: IParser String

123pImport = do reserved "import"

128pImport = do reserved "import"

124 f <- identifier

129 f <- identifier

125 lchar ';'

130 lchar ';'

126− return f

131+ return (map dot f)

132+ where dot '.' = '/'

133+ dot c = c

127

134

128parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]

135parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]

129parseProg syn fname input pos

136parseProg syn fname input pos

src/Idris/REPL.hs+1−1

@@ -174,7 +174,7 @@ displayHelp = let vstr = showVersion version in

174 "\nIdris version " ++ vstr ++ "\n" ++

175 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

176 concatMap cmdInfo help

177− where cmdInfo (cmds, args, text) = " " ++ col 16 10 (showSep " " cmds) args text

177+ where cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) args text

178 col c1 c2 l m r =

179 l ++ take (c1 - length l) (repeat ' ') ++

180 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"