fee6a00 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+4−2

compare with master

unifiedsplit

@@ -25,6 +25,7 @@ import Control.Monad.Trans.Error

25import Data.List

26import Data.Char

27import qualified Data.Text as T

28+import qualified Data.Map as M

28import Data.Either

29import Data.Either

29import Data.Word (Word)

30import Data.Word (Word)

30

31

@@ -137,7 +138,8 @@ data IState = IState {

137 idris_colourTheme :: ColourTheme,

138 idris_colourTheme :: ColourTheme,

138 idris_outh :: Handle,

139 idris_outh :: Handle,

139 idris_errorhandlers :: [Name],

140 idris_errorhandlers :: [Name],

140− idris_nameIdx :: (Int, Ctxt (Int, Name))

141+ idris_nameIdx :: (Int, Ctxt (Int, Name)),

142+ module_aliases :: M.Map [T.Text] [T.Text]

141 }

143 }

142

144

143data SizeChange = Smaller | Same | Bigger | Unknown

145data SizeChange = Smaller | Same | Bigger | Unknown

@@ -204,7 +206,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

204 emptyContext

206 emptyContext

205 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

207 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

206 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

208 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

207− True defaultTheme stdout [] (0, emptyContext)

209+ True defaultTheme stdout [] (0, emptyContext) M.empty

208

210

209-- | The monad for the main REPL - reading and processing files and updating

211-- | The monad for the main REPL - reading and processing files and updating

210-- global state (hence the IO inner monad).

212-- global state (hence the IO inner monad).

src/Idris/Chaser.hs+1−1

@@ -132,7 +132,7 @@ buildTree built fp = btree [] fp

132 file_in <- runIO $ readFile f

133 file <- if lit then tclift $ unlit f file_in else return file_in

134 (_, modules, _) <- parseImports f file

135− ms <- mapM (btree done) modules

135+ ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]

136 return (concat ms)

137 else return [] -- IBC with no source available

138-- (\c -> return []) -- error, can't chase modules here

src/Idris/ParseHelpers.hs+9−4

@@ -25,6 +25,7 @@ import qualified Data.List.Split as Spl

25import Data.List

26import Data.Monoid

27import Data.Char

28+import qualified Data.Map as M

28import qualified Data.HashSet as HS

29import qualified Data.HashSet as HS

29import qualified Data.Text as T

30import qualified Data.Text as T

30import qualified Data.ByteString.UTF8 as UTF8

31import qualified Data.ByteString.UTF8 as UTF8

@@ -210,10 +211,14 @@ maybeWithNS parser ascend bad = do

210

211

211-- | Parses a name

212-- | Parses a name

212name :: IdrisParser Name

213name :: IdrisParser Name

213−name = do i <- get

214+name = (<?> "name") $ do

214− iName (syntax_keywords i)

215+ keywords <- syntax_keywords <$> get

215− <?> "name"

216+ aliases <- module_aliases <$> get

216−

217+ unalias aliases <$> iName keywords

218+ where

219+ unalias :: M.Map [T.Text] [T.Text] -> Name -> Name

220+ unalias aliases (NS n ns) | Just ns' <- M.lookup ns aliases = NS n ns'

221+ unalias aliases name = name

217

222

218{- | List of all initial segments in ascending order of a list. Every such

223{- | List of all initial segments in ascending order of a list. Every such

219 initial segment ends right before an element satisfying the given

224 initial segment ends right before an element satisfying the given

src/Idris/Parser.hs+27−11

@@ -47,11 +47,14 @@ import Control.Monad

47import Control.Monad.Error (throwError, catchError)

48import Control.Monad.State.Strict

49

50+import Data.Function

50import Data.Maybe

51import Data.Maybe

51import qualified Data.List.Split as Spl

52import qualified Data.List.Split as Spl

52import Data.List

53import Data.List

53import Data.Monoid

54import Data.Monoid

54import Data.Char

55import Data.Char

56+import Data.Ord

57+import qualified Data.Map as M

55import qualified Data.HashSet as HS

58import qualified Data.HashSet as HS

56import qualified Data.Text as T

59import qualified Data.Text as T

57import qualified Data.ByteString.UTF8 as UTF8

60import qualified Data.ByteString.UTF8 as UTF8

@@ -91,13 +94,15 @@ moduleHeader = try (do reserved "module"

91{- | Parses an import statement

94{- | Parses an import statement

92 Import ::= 'import' Identifier_t ';'?;

95 Import ::= 'import' Identifier_t ';'?;

93 -}

96 -}

94−import_ :: IdrisParser String

97+import_ :: IdrisParser (String, Maybe String, FC)

98+import_ = do fc <- getFC

95−import_ = do reserved "import"

99+ reserved "import"

96 id <- identifier

100 id <- identifier

101+ newName <- optional (reserved "as" *> identifier)

97 option ';' (lchar ';')

102 option ';' (lchar ';')

98− return (toPath id)

103+ return (toPath id, toPath <$> newName, fc)

99 <?> "import statement"

104 <?> "import statement"

100− where toPath f = foldl1' (</>) (Spl.splitOn "." f)

105+ where toPath = foldl1' (</>) . Spl.splitOn "."

101

106

102{- | Parses program source

107{- | Parses program source

103 Prog ::= Decl* EOF;

108 Prog ::= Decl* EOF;

@@ -934,7 +939,7 @@ parseTactic :: IState -> String -> Result PTactic

934parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

939parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

935

940

936-- | Parse module header and imports

941-- | Parse module header and imports

937−parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)

942+parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)

938parseImports fname input

943parseImports fname input

939 = do i <- getIState

944 = do i <- getIState

940 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

945 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of

@@ -942,7 +947,7 @@ parseImports fname input

942 Success (x, i) -> do -- Discard state updates (there should be

947 Success (x, i) -> do -- Discard state updates (there should be

943 -- none anyway)

948 -- none anyway)

944 return x

949 return x

945− where imports :: IdrisParser (([String], [String], Maybe Delta), IState)

950+ where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)

946 imports = do whiteSpace

951 imports = do whiteSpace

947 mname <- moduleHeader

952 mname <- moduleHeader

948 ps <- many import_

953 ps <- many import_

@@ -1053,13 +1058,24 @@ loadSource h lidr f

1053 let def_total = default_total i

1058 let def_total = default_total i

1054 file_in <- runIO $ readFile f

1059 file_in <- runIO $ readFile f

1055 file <- if lidr then tclift $ unlit f file_in else return file_in

1060 file <- if lidr then tclift $ unlit f file_in else return file_in

1056− (mname, modules, pos) <- parseImports f file

1061+ (mname, imports, pos) <- parseImports f file

1062+

1063+ -- process and check module aliases

1064+ let modAliases = M.fromList

1065+ [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]

1066+ prep = map T.pack . reverse . Spl.splitOn "/"

1067+ aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]

1068+ histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames

1069+ case map head . filter ((/= 1) . length) $ histogram of

1070+ [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)

1071+ (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n

1072+

1057 i <- getIState

1073 i <- getIState

1058− putIState (i { default_access = Hidden })

1074+ putIState (i { default_access = Hidden, module_aliases = modAliases })

1059 clearIBC -- start a new .ibc file

1075 clearIBC -- start a new .ibc file

1060− mapM_ (addIBC . IBCImport) modules

1076+ mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

1061− ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })

1077+ let syntax = defaultSyntax{ syn_namespace = reverse mname }

1062− f file pos

1078+ ds' <- parseProg syntax f file pos

1063 unless (null ds') $ do

1079 unless (null ds') $ do

1064 let ds = namespaces mname ds'

1080 let ds = namespaces mname ds'

1065 logLvl 3 (show $ showDecls True ds)

1081 logLvl 3 (show $ showDecls True ds)

test/test040/A.idrnew file+4

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

1+module A

2+

3+num : Nat

4+num = 0

test/test040/B/C.idrnew file+4

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

1+module B.C

2+

3+num : Nat

4+num = 1

test/test040/Faulty.idrnew file+7

@@ -0,0 +1,7 @@

1+module Faulty

2+

3+import A

4+import B.C

5+

6+fault : num = Z

7+fault = refl

test/test040/Main.idrnew file+16

@@ -0,0 +1,16 @@

1+module Main

2+

3+import A as X

4+import B.C as Y

5+

6+checkX : X.num = Z

7+checkX = refl

8+

9+checkY : Y.num = S Z

10+checkY = refl

11+

12+checkAX : X.num = A.num

13+checkAX = refl

14+

15+checkBY : Y.num = B.C.num

16+checkBY = refl

test/test040/Multiple.idrnew file+4

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

1+module Multiple

2+

3+import Prelude.Vect as X

4+import Prelude.List as X

test/test040/expectednew file+4

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

1+MAIN-PASS

2+Faulty.idr:6:7:When elaborating type of Faulty.fault:

3+Can't disambiguate name: A.num, B.C.num

4+Multiple.idr:3:1:import alias not unique: "X"

test/test040/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+idris $@ Main.idr --nocolour --check && echo MAIN-PASS

3+idris $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

4+idris $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

5+find -name \*.ibc -delete