f24a675 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add the possibility to "import Module as Alias".

f24a675Matus Tejiscak13 years ago

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)

@@ -135,7 +136,8 @@ data IState = IState {

135 idris_colourTheme :: ColourTheme,

136 idris_colourTheme :: ColourTheme,

136 idris_outh :: Handle,

137 idris_outh :: Handle,

137 idris_errorhandlers :: [Name],

138 idris_errorhandlers :: [Name],

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

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

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

139 }

141 }

140

142

141data SizeChange = Smaller | Same | Bigger | Unknown

143data SizeChange = Smaller | Same | Bigger | Unknown

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

202 emptyContext

204 emptyContext

203 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

204 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

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

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

206

208

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

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

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

210-- 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 . fst) 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+14−8

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

52import Data.List

53import Data.Monoid

54import Data.Char

55+import qualified Data.Map as M

55import qualified Data.HashSet as HS

56import qualified Data.HashSet as HS

56import qualified Data.Text as T

57import qualified Data.Text as T

57import qualified Data.ByteString.UTF8 as UTF8

58import qualified Data.ByteString.UTF8 as UTF8

@@ -91,13 +92,14 @@ moduleHeader = try (do reserved "module"

91{- | Parses an import statement

92{- | Parses an import statement

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

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

93 -}

94 -}

94−import_ :: IdrisParser String

95+import_ :: IdrisParser (String, Maybe String)

95import_ = do reserved "import"

96import_ = do reserved "import"

96 id <- identifier

97 id <- identifier

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

97 option ';' (lchar ';')

99 option ';' (lchar ';')

98− return (toPath id)

100+ return (toPath id, toPath <$> newName)

99 <?> "import statement"

101 <?> "import statement"

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

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

101

103

102{- | Parses program source

104{- | Parses program source

103 Prog ::= Decl* EOF;

105 Prog ::= Decl* EOF;

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

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

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

935

937

936-- | Parse module header and imports

938-- | Parse module header and imports

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

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

938parseImports fname input

940parseImports fname input

939 = do i <- getIState

941 = do i <- getIState

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

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

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

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

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

943 -- none anyway)

945 -- none anyway)

944 return x

946 return x

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

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

946 imports = do whiteSpace

948 imports = do whiteSpace

947 mname <- moduleHeader

949 mname <- moduleHeader

948 ps <- many import_

950 ps <- many import_

@@ -1053,13 +1055,17 @@ loadSource h lidr f

1053 let def_total = default_total i

1055 let def_total = default_total i

1054 file_in <- runIO $ readFile f

1056 file_in <- runIO $ readFile f

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

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

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

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

1059+ let modules = map fst imports

1060+ modAliases = M.fromList

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

1062+ prep = map T.pack . Spl.splitOn "/"

1057 i <- getIState

1063 i <- getIState

1058 putIState (i { default_access = Hidden })

1064 putIState (i { default_access = Hidden })

1059 clearIBC -- start a new .ibc file

1065 clearIBC -- start a new .ibc file

1060 mapM_ (addIBC . IBCImport) modules

1066 mapM_ (addIBC . IBCImport) modules

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

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

1062− f file pos

1068+ ds' <- parseProg syntax f file pos

1063 unless (null ds') $ do

1069 unless (null ds') $ do

1064 let ds = namespaces mname ds'

1070 let ds = namespaces mname ds'

1065 logLvl 3 (showDecls True ds)

1071 logLvl 3 (showDecls True ds)