@@ -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
@@ -63,6 +66,7 @@ import System.FilePath
6366import System.IO
6467
6568{-
69+@
6670 grammar shortcut notation:
6771 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
6872 RULE? = optional rule (i.e. RULE or nothing)
@@ -70,12 +74,16 @@ import System.IO
7074 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
7175 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
7276 RULE{n} = rule repeated n times
77+@
7378-}
7479
7580{- * Main grammar -}
7681
7782{- | Parses module definition
83+
84+@
7885 ModuleHeader ::= 'module' Identifier_t ';'?;
86+@
7987-}
8088moduleHeader :: IdrisParser [String]
8189moduleHeader = try (do reserved "module"
@@ -90,18 +98,26 @@ moduleHeader = try (do reserved "module"
9098 (x, '.':y) -> x : moduleName y
9199
92100{- | Parses an import statement
101+
102+@
93103 Import ::= 'import' Identifier_t ';'?;
104+@
94105 -}
95−import_ :: IdrisParser String
96−import_ = do reserved "import"
106+import_ :: IdrisParser (String, Maybe String, FC)
107+import_ = do fc <- getFC
108+ reserved "import"
97109 id <- identifier
110+ newName <- optional (reserved "as" *> identifier)
98111 option ';' (lchar ';')
99− return (toPath id)
112+ return (toPath id, toPath <$> newName, fc)
100113 <?> "import statement"
101− where toPath f = foldl1' (</>) (Spl.splitOn "." f)
114+ where toPath = foldl1' (</>) . Spl.splitOn "."
102115
103116{- | Parses program source
117+
118+@
104119 Prog ::= Decl* EOF;
120+@
105121 -}
106122prog :: SyntaxInfo -> IdrisParser [PDecl]
107123prog syn = do whiteSpace
@@ -111,7 +127,9 @@ prog syn = do whiteSpace
111127 let c = (concat decls)
112128 return c
113129
114−{- | Parses a top-level declaration
130+{-| Parses a top-level declaration
131+
132+@
115133Decl ::=
116134 Decl'
117135 | Using
@@ -126,6 +144,7 @@ Decl ::=
126144 | Transform
127145 | Import!
128146 ;
147+@
129148-}
130149decl :: SyntaxInfo -> IdrisParser [PDecl]
131150decl syn = do notEndBlock
@@ -151,6 +170,8 @@ decl syn = do notEndBlock
151170 return [d']
152171
153172{- | Parses a top-level declaration with possible syntax sugar
173+
174+@
154175Decl' ::=
155176 Fixity
156177 | FunDecl'
@@ -158,6 +179,7 @@ Decl' ::=
158179 | Record
159180 | SyntaxDecl
160181 ;
182+@
161183-}
162184decl' :: SyntaxInfo -> IdrisParser PDecl
163185decl' syn = fixity
@@ -168,7 +190,10 @@ decl' syn = fixity
168190 <?> "declaration"
169191
170192{- | Parses a syntax extension declaration (and adds the rule to parser state)
193+
194+@
171195 SyntaxDecl ::= SyntaxRule;
196+@
172197-}
173198syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
174199syntaxDecl syn = do s <- syntaxRule syn
@@ -186,17 +211,24 @@ syntaxDecl syn = do s <- syntaxRule syn
186211 ename (Keyword n) = Just n
187212 ename _ = Nothing
188213
189−{- | Parses a syntax extension declaration
190−SyntaxRuleOpts ::= 'term' | 'pattern';
214+{- | Parses a syntax extension declaration
215+
216+@
217+SyntaxRuleOpts ::= 'term' | 'pattern';
218+@
191219
220+@
192221SyntaxRule ::=
193222 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
223+@
194224
225+@
195226SyntaxSym ::= '[' Name_t ']'
196227 | '{' Name_t '}'
197228 | Name_t
198229 | StringLiteral_t
199230 ;
231+@
200232-}
201233syntaxRule :: SyntaxInfo -> IdrisParser Syntax
202234syntaxRule syn
@@ -232,11 +264,14 @@ syntaxRule syn
232264
233265
234266{- | Parses a syntax symbol (either binding variable, keyword or expression)
267+
268+@
235269SyntaxSym ::= '[' Name_t ']'
236270 | '{' Name_t '}'
237271 | Name_t
238272 | StringLiteral_t
239273 ;
274+@
240275 -}
241276syntaxSym :: IdrisParser SSymbol
242277syntaxSym = try (do lchar '['; n <- name; lchar ']'
@@ -250,7 +285,10 @@ syntaxSym = try (do lchar '['; n <- name; lchar ']'
250285 <?> "syntax symbol"
251286
252287{- | Parses a function declaration with possible syntax sugar
288+
289+@
253290 FunDecl ::= FunDecl';
291+@
254292-}
255293fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
256294fnDecl syn = try (do notEndBlock
@@ -259,13 +297,16 @@ fnDecl syn = try (do notEndBlock
259297 let d' = fmap (desugar syn i) d
260298 return [d']) <?> "function declaration"
261299
262−{- Parses a function declaration
300+{-| Parses a function declaration
301+
302+@
263303 FunDecl' ::=
264304 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
265305 | Postulate
266306 | Pattern
267307 | CAF
268308 ;
309+@
269310-}
270311fnDecl' :: SyntaxInfo -> IdrisParser PDecl
271312fnDecl' syn = checkFixity $
@@ -309,23 +350,29 @@ fnDecl' syn = checkFixity $
309350 | otherwise = return True
310351 fixityOK _ = return True
311352
312−{- Parses function options given initial options
353+{-| Parses function options given initial options
354+
355+@
313356FnOpts ::= 'total'
314357 | 'partial'
315358 | 'implicit'
316359 | '%' 'assert_total'
317360 | '%' 'error_handler'
318− | '%' 'reflection'
361+ | '%' 'reflection'
319362 | '%' 'specialise' '[' NameTimesList? ']'
320363 ;
364+@
321365
366+@
322367NameTimes ::= FnName Natural?;
368+@
323369
370+@
324371NameTimesList ::=
325372 NameTimes
326373 | NameTimes ',' NameTimesList
327374 ;
328−
375+@
329376-}
330377-- FIXME: Check compatability for function options (i.e. partal/total)
331378fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
@@ -356,9 +403,11 @@ fnOpts opts
356403
357404{- | Parses a postulate
358405
406+@
359407Postulate ::=
360408 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
361409 ;
410+@
362411-}
363412postulate :: SyntaxInfo -> IdrisParser PDecl
364413postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
@@ -384,9 +433,11 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
384433
385434{- | Parses a using declaration
386435
436+@
387437Using ::=
388438 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
389439 ;
440+@
390441 -}
391442using_ :: SyntaxInfo -> IdrisParser [PDecl]
392443using_ syn =
@@ -398,11 +449,13 @@ using_ syn =
398449 return (concat ds)
399450 <?> "using declaration"
400451
401−{- | Parses a parameters declaration
452+{- | Parses a parameters declaration
402453
454+@
403455Params ::=
404456 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
405457 ;
458+@
406459 -}
407460params :: SyntaxInfo -> IdrisParser [PDecl]
408461params syn =
@@ -417,9 +470,11 @@ params syn =
417470
418471{- | Parses a mutual declaration (for mutually recursive functions)
419472
473+@
420474Mutual ::=
421475 'mutual' OpenBlock Decl* CloseBlock
422476 ;
477+@
423478-}
424479mutual :: SyntaxInfo -> IdrisParser [PDecl]
425480mutual syn =
@@ -432,11 +487,13 @@ mutual syn =
432487 return [PMutual fc (concat ds)]
433488 <?> "mutual block"
434489
435−{- | Parses a namespace declaration
490+{-| Parses a namespace declaration
436491
492+@
437493Namespace ::=
438494 'namespace' identifier OpenBlock Decl+ CloseBlock
439495 ;
496+@
440497-}
441498namespace :: SyntaxInfo -> IdrisParser [PDecl]
442499namespace syn =
@@ -447,9 +504,12 @@ namespace syn =
447504 return [PNamespace n (concat ds)]
448505 <?> "namespace declaration"
449506
450−{- |Parses a methods block (for instances)
507+{- | Parses a methods block (for instances)
508+
509+@
451510 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
452− -}
511+@
512+-}
453513instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
454514instanceBlock syn = do reserved "where"
455515 openBlock
@@ -458,16 +518,20 @@ instanceBlock syn = do reserved "where"
458518 return (concat ds)
459519 <?> "instance block"
460520
461−{- |Parses a methods and instances block (for type classes)
521+{- | Parses a methods and instances block (for type classes)
462522
523+@
463524MethodOrInstance ::=
464525 FnDecl
465526 | Instance
466527 ;
528+@
467529
530+@
468531ClassBlock ::=
469532 'where' OpenBlock MethodOrInstance* CloseBlock
470533 ;
534+@
471535-}
472536classBlock :: SyntaxInfo -> IdrisParser [PDecl]
473537classBlock syn = do reserved "where"
@@ -477,16 +541,20 @@ classBlock syn = do reserved "where"
477541 return (concat ds)
478542 <?> "class block"
479543
480−{- |Parses a type class declaration
544+{-| Parses a type class declaration
481545
546+@
482547ClassArgument ::=
483548 Name
484549 | '(' Name ':' Expr ')'
485550 ;
551+@
486552
553+@
487554Class ::=
488555 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
489556 ;
557+@
490558-}
491559class_ :: SyntaxInfo -> IdrisParser [PDecl]
492560class_ syn = do (doc, acc) <- try (do
@@ -507,13 +575,17 @@ class_ syn = do (doc, acc) <- try (do
507575 <|> do i <- name;
508576 return (i, PType)
509577
510−{- |Parses a type class instance declaration
578+{- | Parses a type class instance declaration
511579
580+@
512581 Instance ::=
513582 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
514583 ;
584+@
515585
516− InstanceName ::= '[' Name ']';
586+@
587+InstanceName ::= '[' Name ']';
588+@
517589-}
518590instance_ :: SyntaxInfo -> IdrisParser [PDecl]
519591instance_ syn = do reserved "instance"; fc <- getFC
@@ -534,20 +606,27 @@ instance_ syn = do reserved "instance"; fc <- getFC
534606
535607
536608{- | Parses a using declaration list
609+
610+@
537611UsingDeclList ::=
538612 UsingDeclList'
539613 | NameList TypeSig
540614 ;
615+@
541616
617+@
542618UsingDeclList' ::=
543619 UsingDecl
544620 | UsingDecl ',' UsingDeclList'
545621 ;
622+@
546623
624+@
547625NameList ::=
548626 Name
549627 | Name ',' NameList
550628 ;
629+@
551630-}
552631usingDeclList :: SyntaxInfo -> IdrisParser [Using]
553632usingDeclList syn
@@ -559,10 +638,13 @@ usingDeclList syn
559638 <?> "using declaration list"
560639
561640{- |Parses a using declaration
641+
642+@
562643UsingDecl ::=
563644 FnName TypeSig
564645 | FnName FnName+
565646 ;
647+@
566648-}
567649usingDecl :: SyntaxInfo -> IdrisParser Using
568650usingDecl syn = try (do x <- fnName
@@ -574,8 +656,11 @@ usingDecl syn = try (do x <- fnName
574656 return (UConstraint c xs)
575657 <?> "using declaration"
576658
577−{- | Parse a clause with patterns
659+{- | Parse a clause with patterns
660+
661+@
578662Pattern ::= Clause;
663+@
579664-}
580665pattern :: SyntaxInfo -> IdrisParser PDecl
581666pattern syn = do fc <- getFC
@@ -584,7 +669,10 @@ pattern syn = do fc <- getFC
584669 <?> "pattern"
585670
586671{- | Parse a constant applicative form declaration
587− CAF ::= 'let' FnName '=' Expr Terminator;
672+
673+@
674+CAF ::= 'let' FnName '=' Expr Terminator;
675+@
588676-}
589677caf :: SyntaxInfo -> IdrisParser PDecl
590678caf syn = do reserved "let"
@@ -597,7 +685,10 @@ caf syn = do reserved "let"
597685 <?> "constant applicative form declaration"
598686
599687{- | Parse an argument expression
600− ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
688+
689+@
690+ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
691+@
601692-}
602693argExpr :: SyntaxInfo -> IdrisParser PTerm
603694argExpr syn = let syn' = syn { inPattern = True } in
@@ -605,12 +696,17 @@ argExpr syn = let syn' = syn { inPattern = True } in
605696 <?> "argument expression"
606697
607698{- | Parse a right hand side of a function
699+
700+@
608701RHS ::= '=' Expr
609702 | '?=' RHSName? Expr
610703 | 'impossible'
611704 ;
705+@
612706
707+@
613708RHSName ::= '{' FnName '}';
709+@
614710-}
615711rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
616712rhs syn n = do lchar '='; expr syn
@@ -633,16 +729,28 @@ rhs syn n = do lchar '='; expr syn
633729 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))
634730
635731{- |Parses a function clause
732+
733+@
636734RHSOrWithBlock ::= RHS WhereOrTerminator
637735 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
638736 ;
737+@
738+
739+@
639740Clause ::= WExpr+ RHSOrWithBlock
640741 | SimpleExpr '<==' FnName RHS WhereOrTerminator
641742 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
642743 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
643744 ;
745+@
746+
747+@
644748ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
645−WhereOrTerminator ::= WhereBlock | Terminator;
749+@
750+
751+@
752+WhereOrTerminator ::= WhereBlock | Terminator;
753+@
646754-}
647755clause :: SyntaxInfo -> IdrisParser PClause
648756clause syn
@@ -771,17 +879,23 @@ clause syn
771879 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
772880 fillLHSD n c a x = x
773881
774−{- |Parses with pattern
775− WExpr ::= '|' Expr';
882+{-| Parses with pattern
883+
884+@
885+WExpr ::= '|' Expr';
886+@
776887-}
777888wExpr :: SyntaxInfo -> IdrisParser PTerm
778889wExpr syn = do lchar '|'
779890 expr' syn
780891 <?> "with pattern"
781892
782−{- |Parses a where block
893+{- | Parses a where block
894+
895+@
783896WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
784− -}
897+@
898+-}
785899whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
786900whereBlock n syn
787901 = do reserved "where"
@@ -791,6 +905,8 @@ whereBlock n syn
791905 <?> "where block"
792906
793907{- |Parses a code generation target language name
908+
909+@
794910Codegen ::= 'C'
795911 | 'Java'
796912 | 'JavaScript'
@@ -798,6 +914,7 @@ Codegen ::= 'C'
798914 | 'LLVM'
799915 | 'Bytecode'
800916 ;
917+@
801918-}
802919codegen_ :: IdrisParser Codegen
803920codegen_ = do reserved "C"; return ViaC
@@ -809,13 +926,18 @@ codegen_ = do reserved "C"; return ViaC
809926 <?> "code generation language"
810927
811928{- |Parses a compiler directive
929+@
812930StringList ::=
813931 String
814932 | String ',' StringList
815933 ;
934+@
816935
936+@
817937Directive ::= '%' Directive';
938+@
818939
940+@
819941Directive' ::= 'lib' CodeGen String_t
820942 | 'link' CodeGen String_t
821943 | 'flag' CodeGen String_t
@@ -831,6 +953,7 @@ Directive' ::= 'lib' CodeGen String_t
831953 | 'language' 'TypeProviders'
832954 | 'language' 'ErrorReflection'
833955 ;
956+@
834957-}
835958directive :: SyntaxInfo -> IdrisParser [PDecl]
836959directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
@@ -899,15 +1022,22 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)
8991022 <|> (reserved "ErrorReflection" >> return ErrorReflection)
9001023
9011024{- | Parses a totality
1025+
1026+@
9021027Totality ::= 'partial' | 'total'
1028+@
1029+
9031030-}
9041031totality :: IdrisParser Bool
9051032totality
9061033 = do reserved "total"; return True
9071034 <|> do reserved "partial"; return False
9081035
909−{- | Parses a type provider
1036+{- | Parses a type provider
1037+
1038+@
9101039Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
1040+@
9111041 -}
9121042provider :: SyntaxInfo -> IdrisParser [PDecl]
9131043provider syn = do try (lchar '%' *> reserved "provide");
@@ -919,7 +1049,10 @@ provider syn = do try (lchar '%' *> reserved "provide");
9191049 <?> "type provider"
9201050
9211051{- | Parses a transform
1052+
1053+@
9221054Transform ::= '%' 'transform' Expr '==>' Expr
1055+@
9231056-}
9241057transform :: SyntaxInfo -> IdrisParser [PDecl]
9251058transform syn = do try (lchar '%' *> reserved "transform")
@@ -945,7 +1078,7 @@ parseTactic :: IState -> String -> Result PTactic
9451078parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"
9461079
9471080-- | Parse module header and imports
948−parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
1081+parseImports :: FilePath -> String -> Idris ([String], [(String, Maybe String, FC)], Maybe Delta)
9491082parseImports fname input
9501083 = do i <- getIState
9511084 case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
@@ -953,7 +1086,7 @@ parseImports fname input
9531086 Success (x, i) -> do -- Discard state updates (there should be
9541087 -- none anyway)
9551088 return x
956− where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
1089+ where imports :: IdrisParser (([String], [(String, Maybe String, FC)], Maybe Delta), IState)
9571090 imports = do whiteSpace
9581091 mname <- moduleHeader
9591092 ps <- many import_
@@ -1064,13 +1197,24 @@ loadSource h lidr f
10641197 let def_total = default_total i
10651198 file_in <- runIO $ readFile f
10661199 file <- if lidr then tclift $ unlit f file_in else return file_in
1067− (mname, modules, pos) <- parseImports f file
1200+ (mname, imports, pos) <- parseImports f file
1201+
1202+ -- process and check module aliases
1203+ let modAliases = M.fromList
1204+ [(prep alias, prep realName) | (realName, Just alias, fc) <- imports]
1205+ prep = map T.pack . reverse . Spl.splitOn "/"
1206+ aliasNames = [(alias, fc) | (_, Just alias, fc) <- imports]
1207+ histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1208+ case map head . filter ((/= 1) . length) $ histogram of
1209+ [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases)
1210+ (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1211+
10681212 i <- getIState
1069− putIState (i { default_access = Hidden })
1213+ putIState (i { default_access = Hidden, module_aliases = modAliases })
10701214 clearIBC -- start a new .ibc file
1071− mapM_ (addIBC . IBCImport) modules
1072− ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
1073− f file pos
1215+ mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1216+ let syntax = defaultSyntax{ syn_namespace = reverse mname }
1217+ ds' <- parseProg syntax f file pos
10741218 unless (null ds') $ do
10751219 let ds = namespaces mname ds'
10761220 logLvl 3 (show $ showDecls True ds)