git.iko.soy/Idris-dev
on master help sign in
Merge pull request #806 from ziman/import-as

Support for "import Module as Alias"

commitfee6a0030008e87be36e82edc201be2561654926 authorEdwin Brady <edwin.brady@gmail.com> dateThu 30 Jan 2014, 02:16 (13 years ago) parent694832fbd3d70d
11 files changed+85−18
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/Chaser.hs+1−1 src/Idris/ParseHelpers.hs+9−4 src/Idris/Parser.hs+27−11 test/test040/A.idr+4 test/test040/B/C.idr+4 test/test040/Faulty.idr+7 test/test040/Main.idr+16 test/test040/Multiple.idr+4 test/test040/expected+4 test/test040/run+5
src/Idris/AbsSyntaxTree.hs+4−2
@@ -25,6 +25,7 @@ import Control.Monad.Trans.Error
2525import Data.List
2626import Data.Char
2727import qualified Data.Text as T
28+import qualified Data.Map as M
2829import Data.Either
2930import Data.Word (Word)
3031
@@ -137,7 +138,8 @@ data IState = IState {
137138 idris_colourTheme :: ColourTheme,
138139 idris_outh :: Handle,
139140 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]
141143 }
142144
143145data SizeChange = Smaller | Same | Bigger | Unknown
@@ -204,7 +206,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
204206 emptyContext
205207 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
206208 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
207− True defaultTheme stdout [] (0, emptyContext)
209+ True defaultTheme stdout [] (0, emptyContext) M.empty
208210
209211-- | The monad for the main REPL - reading and processing files and updating
210212-- global state (hence the IO inner monad).
src/Idris/Chaser.hs+1−1
@@ -132,7 +132,7 @@ buildTree built fp = btree [] fp
132132 file_in <- runIO $ readFile f
133133 file <- if lit then tclift $ unlit f file_in else return file_in
134134 (_, modules, _) <- parseImports f file
135− ms <- mapM (btree done) modules
135+ ms <- mapM (btree done) [realName | (realName, alias, fc) <- modules]
136136 return (concat ms)
137137 else return [] -- IBC with no source available
138138-- (\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
2525import Data.List
2626import Data.Monoid
2727import Data.Char
28+import qualified Data.Map as M
2829import qualified Data.HashSet as HS
2930import qualified Data.Text as T
3031import qualified Data.ByteString.UTF8 as UTF8
@@ -210,10 +211,14 @@ maybeWithNS parser ascend bad = do
210211
211212-- | Parses a name
212213name :: IdrisParser Name
213−name = do i <- get
214− iName (syntax_keywords i)
215− <?> "name"
216−
214+name = (<?> "name") $ do
215+ keywords <- syntax_keywords <$> get
216+ aliases <- module_aliases <$> get
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
217222
218223{- | List of all initial segments in ascending order of a list. Every such
219224 initial segment ends right before an element satisfying the given
src/Idris/Parser.hs+27−11
@@ -47,11 +47,14 @@ import Control.Monad
4747import Control.Monad.Error (throwError, catchError)
4848import Control.Monad.State.Strict
4949
50+import Data.Function
5051import Data.Maybe
5152import qualified Data.List.Split as Spl
5253import Data.List
5354import Data.Monoid
5455import Data.Char
56+import Data.Ord
57+import qualified Data.Map as M
5558import qualified Data.HashSet as HS
5659import qualified Data.Text as T
5760import qualified Data.ByteString.UTF8 as UTF8
@@ -91,13 +94,15 @@ moduleHeader = try (do reserved "module"
9194{- | Parses an import statement
9295 Import ::= 'import' Identifier_t ';'?;
9396 -}
94−import_ :: IdrisParser String
95−import_ = do reserved "import"
97+import_ :: IdrisParser (String, Maybe String, FC)
98+import_ = do fc <- getFC
99+ reserved "import"
96100 id <- identifier
101+ newName <- optional (reserved "as" *> identifier)
97102 option ';' (lchar ';')
98− return (toPath id)
103+ return (toPath id, toPath <$> newName, fc)
99104 <?> "import statement"
100− where toPath f = foldl1' (</>) (Spl.splitOn "." f)
105+ where toPath = foldl1' (</>) . Spl.splitOn "."
101106
102107{- | Parses program source
103108 Prog ::= Decl* EOF;
@@ -934,7 +939,7 @@ parseTactic :: IState -> String -> Result PTactic
934939parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
935940
936941-- | 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)
938943parseImports fname input
939944 = do i <- getIState
940945 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
@@ -942,7 +947,7 @@ parseImports fname input
942947 Success (x, i) -> do -- Discard state updates (there should be
943948 -- none anyway)
944949 return x
945− where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
950+ where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
946951 imports = do whiteSpace
947952 mname <- moduleHeader
948953 ps <- many import_
@@ -1053,13 +1058,24 @@ loadSource h lidr f
10531058 let def_total = default_total i
10541059 file_in <- runIO $ readFile f
10551060 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+
10571073 i <- getIState
1058− putIState (i { default_access = Hidden })
1074+ putIState (i { default_access = Hidden, module_aliases = modAliases })
10591075 clearIBC -- start a new .ibc file
1060− mapM_ (addIBC . IBCImport) modules
1061− ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
1062− f file pos
1076+ mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1077+ let syntax = defaultSyntax{ syn_namespace = reverse mname }
1078+ ds' <- parseProg syntax f file pos
10631079 unless (null ds') $ do
10641080 let ds = namespaces mname ds'
10651081 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