380e1ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' into error-reflection

380e1caDavid Raymond Christiansen13 years ago

CHANGELOG+5

compare with master

unifiedsplit

@@ -10,11 +10,16 @@ New in 0.9.11:

10* General improvements in error messages, especially %error_reverse

11 annotation, which allows a hint as to how to display a term in error

12 messages

13+* --ideslave mode now transmits semantic information about many of the

14+ strings that it emits, which can be used by clients to implement

15+ semantic highlighting like that of the REPL. This has been implemented

16+ in the Emacs mode and the IRC bot, which can serve as examples.

14Internal changes

18Internal changes

16* Faster elaboration

20* Faster elaboration

17* Smaller .ibc files

21* Smaller .ibc files

22+* Pretty-printer now used for all term output

20New in 0.9.10:

25New in 0.9.10:

idris.cabal+7−1

@@ -323,6 +323,12 @@ Extra-source-files:

323 test/test038/run

324 test/test038/expected

325 test/test038/*.idr

326+ test/test039/run

327+ test/test039/expected

328+ test/test039/*.idr

329+ test/test040/run

330+ test/test040/expected

331+ test/test040/*.idr

326

332

327source-repository head

333source-repository head

328 type: git

334 type: git

@@ -442,7 +448,7 @@ Library

442 , ansi-wl-pprint

448 , ansi-wl-pprint

443 , binary

449 , binary

444 , bytestring

450 , bytestring

445− , containers

451+ , containers >= 0.5

446 , directory

452 , directory

447 , directory >= 1.2

453 , directory >= 1.2

448 , filepath

454 , filepath

jsrts/Runtime-common.js+17

@@ -49,3 +49,20 @@ var __IDRRT__tailcall = function(k) {

50 return ret;

51};

52+

53+var __IDRRT__EVALTC = function(arg0) {

54+ var ret = (arg0 instanceof __IDRRT__Con && __IDRLT__mEVAL0[arg0.tag])?(__IDRLT__mEVAL0[arg0.tag](arg0)):(arg0);

55+ while (ret instanceof __IDRRT__Cont)

56+ ret = ret.k();

57+

58+ return ret;

59+};

60+

61+var __IDRRT__APPLYTC = function(fn0, arg0) {

62+ var ev = __IDRRT__EVALTC(fn0);

63+ var ret = (ev instanceof __IDRRT__Con && __IDRLT__mAPPLY0[ev.tag])?(__IDRLT__mAPPLY0[ev.tag](fn0,arg0,ev)):(null)

64+ while (ret instanceof __IDRRT__Cont)

65+ ret = ret.k();

66+

67+ return ret;

68+}

src/IRTS/CodegenJavaScript.hs+174−26

@@ -246,14 +246,17 @@ jsLet name value body =

246 ) [value]

247

248

249−jsSubst :: String -> JS -> JS -> JS

249+jsSubst :: JS -> JS -> JS -> JS

250−jsSubst var new (JSVar old)

250+jsSubst var new old

251+ | var == old = new

252+

253+jsSubst (JSIdent var) new (JSVar old)

251 | var == translateVariableName old = new

254 | var == translateVariableName old = new

252− | otherwise = JSVar old

255+ | otherwise = JSVar old

253

256

254−jsSubst var new (JSIdent old)

257+jsSubst var new old@(JSIdent _)

255 | var == old = new

258 | var == old = new

256− | otherwise = JSIdent old

259+ | otherwise = old

257

260

258jsSubst var new (JSArray fields) =

261jsSubst var new (JSArray fields) =

259 JSArray (map (jsSubst var new) fields)

262 JSArray (map (jsSubst var new) fields)

@@ -261,25 +264,25 @@ jsSubst var new (JSArray fields) =

261jsSubst var new (JSNew con vals) =

264jsSubst var new (JSNew con vals) =

262 JSNew con $ map (jsSubst var new) vals

265 JSNew con $ map (jsSubst var new) vals

263

266

264−jsSubst var new (JSApp (JSProj (JSFunction args body) "apply") vals)

267+jsSubst (JSIdent var) new (JSApp (JSProj (JSFunction args body) "apply") vals)

265 | var `notElem` args =

268 | var `notElem` args =

266− JSApp (JSProj (JSFunction args (jsSubst var new body)) "apply") (

269+ JSApp (JSProj (JSFunction args (jsSubst (JSIdent var) new body)) "apply") (

267− map (jsSubst var new) vals

270+ map (jsSubst (JSIdent var) new) vals

268 )

271 )

269 | otherwise =

272 | otherwise =

270 JSApp (JSProj (JSFunction args body) "apply") (

273 JSApp (JSProj (JSFunction args body) "apply") (

271− map (jsSubst var new) vals

274+ map (jsSubst (JSIdent var) new) vals

272 )

275 )

273

276

274−jsSubst var new (JSApp (JSFunction [arg] body) vals)

277+jsSubst (JSIdent var) new (JSApp (JSFunction [arg] body) vals)

275 | var /= arg =

278 | var /= arg =

276 JSApp (JSFunction [arg] (

279 JSApp (JSFunction [arg] (

277− jsSubst var new body

280+ jsSubst (JSIdent var) new body

278− )) $ map (jsSubst var new) vals

281+ )) $ map (jsSubst (JSIdent var) new) vals

279 | otherwise =

282 | otherwise =

280 JSApp (JSFunction [arg] (

283 JSApp (JSFunction [arg] (

281 body

284 body

282− )) $ map (jsSubst var new) vals

285+ )) $ map (jsSubst (JSIdent var) new) vals

283

286

284jsSubst var new (JSApp lhs rhs) =

287jsSubst var new (JSApp lhs rhs) =

285 JSApp (jsSubst var new lhs) (map (jsSubst var new) rhs)

288 JSApp (jsSubst var new lhs) (map (jsSubst var new) rhs)

@@ -324,7 +327,7 @@ removeAllocations (JSSeq body) =

324 removeHelper :: [JS] -> [JS]

327 removeHelper :: [JS] -> [JS]

325 removeHelper [js] = [js]

328 removeHelper [js] = [js]

326 removeHelper ((JSAlloc name (Just val@(JSIdent _))):js) =

329 removeHelper ((JSAlloc name (Just val@(JSIdent _))):js) =

327− map (jsSubst name val) (removeHelper js)

330+ map (jsSubst (JSIdent name) val) (removeHelper js)

328 removeHelper (j:js) = j : removeHelper js

331 removeHelper (j:js) = j : removeHelper js

329

332

330removeAllocations (JSFunction args body) =

333removeAllocations (JSFunction args body) =

@@ -378,7 +381,7 @@ isJSConstant js

378

381

379inlineJS :: JS -> JS

382inlineJS :: JS -> JS

380inlineJS (JSReturn (JSApp (JSFunction ["cse"] body) [val@(JSVar _)])) =

383inlineJS (JSReturn (JSApp (JSFunction ["cse"] body) [val@(JSVar _)])) =

381− inlineJS $ jsSubst "cse" val body

384+ inlineJS $ jsSubst (JSIdent "cse") val body

382

385

383inlineJS (JSReturn (JSApp (JSFunction [arg] cond@(JSCond _)) [val])) =

386inlineJS (JSReturn (JSApp (JSFunction [arg] cond@(JSCond _)) [val])) =

384 JSSeq [ JSAlloc arg (Just (inlineJS val))

387 JSSeq [ JSAlloc arg (Just (inlineJS val))

@@ -394,7 +397,7 @@ inlineJS (JSApp (JSProj (JSFunction args (JSReturn body)) "apply") [

394 inlineApply [] body _ = inlineJS body

397 inlineApply [] body _ = inlineJS body

395 inlineApply (a:as) body n =

398 inlineApply (a:as) body n =

396 inlineApply as (

399 inlineApply as (

397− jsSubst a (JSIndex (JSProj var "vars") (JSNum (JSInt n))) body

400+ jsSubst (JSIdent a) (JSIndex (JSProj var "vars") (JSNum (JSInt n))) body

398 ) (n + 1)

401 ) (n + 1)

399

402

400inlineJS (JSApp (JSIdent "__IDR__mEVAL0") [val])

403inlineJS (JSApp (JSIdent "__IDR__mEVAL0") [val])

@@ -408,33 +411,43 @@ inlineJS (JSApp (JSIdent "__IDRRT__tailcall") [

408inlineJS (JSApp (JSFunction [arg] (JSReturn ret)) [val])

411inlineJS (JSApp (JSFunction [arg] (JSReturn ret)) [val])

409 | JSNew con [tag, vals] <- ret

412 | JSNew con [tag, vals] <- ret

410 , opt <- inlineJS val =

413 , opt <- inlineJS val =

411− JSNew con [tag, jsSubst arg opt vals]

414+ JSNew con [tag, jsSubst (JSIdent arg) opt vals]

412

415

413 | JSNew con [JSFunction [] (JSReturn (JSApp fun vars))] <- ret

416 | JSNew con [JSFunction [] (JSReturn (JSApp fun vars))] <- ret

414 , opt <- inlineJS val =

417 , opt <- inlineJS val =

415 JSNew con [JSFunction [] (

418 JSNew con [JSFunction [] (

419+ JSReturn (

420+ JSApp (

421+ jsSubst (JSIdent arg) opt fun

422+ ) (

416− JSReturn $ JSApp (jsSubst arg opt fun) (map (jsSubst arg opt) vars)

423+ map (jsSubst (JSIdent arg) opt) vars

424+ )

425+ )

417 )]

426 )]

418

427

419 | JSApp (JSProj obj field) args <- ret

428 | JSApp (JSProj obj field) args <- ret

420 , opt <- inlineJS val =

429 , opt <- inlineJS val =

430+ JSApp (

421− JSApp (JSProj (jsSubst arg opt obj) field) $ map (jsSubst arg opt) args

431+ JSProj (jsSubst (JSIdent arg) opt obj) field

432+ ) (

433+ map (jsSubst (JSIdent arg) opt) args

434+ )

422

435

423 | JSIndex (JSProj obj field) idx <- ret

436 | JSIndex (JSProj obj field) idx <- ret

424 , opt <- inlineJS val =

437 , opt <- inlineJS val =

425 JSIndex (JSProj (

438 JSIndex (JSProj (

426− jsSubst arg opt obj

439+ jsSubst (JSIdent arg) opt obj

427 ) field

440 ) field

428− ) (jsSubst arg opt idx)

441+ ) (jsSubst (JSIdent arg) opt idx)

429

442

430 | JSOp op lhs rhs <- ret

443 | JSOp op lhs rhs <- ret

431 , opt <- inlineJS val =

444 , opt <- inlineJS val =

432− JSOp op (jsSubst arg opt lhs) $

445+ JSOp op (jsSubst (JSIdent arg) opt lhs) $

433− (jsSubst arg opt rhs)

446+ (jsSubst (JSIdent arg) opt rhs)

434

447

435 | JSApp (JSIdent fun) args <- ret

448 | JSApp (JSIdent fun) args <- ret

436 , opt <- inlineJS val =

449 , opt <- inlineJS val =

437− JSApp (JSIdent fun) $ map (jsSubst arg opt) args

450+ JSApp (JSIdent fun) $ map (jsSubst (JSIdent arg) opt) args

438

451

439inlineJS (JSApp fun args) =

452inlineJS (JSApp fun args) =

440 JSApp (inlineJS fun) (map inlineJS args)

453 JSApp (inlineJS fun) (map inlineJS args)

@@ -480,6 +493,11 @@ reduceJS js = reduceLoop [] ([], js)

480funName :: JS -> String

493funName :: JS -> String

481funName (JSAlloc fun _) = fun

494funName (JSAlloc fun _) = fun

482

495

496+elimDeadLoop :: [JS] -> [JS]

497+elimDeadLoop js

498+ | ret <- deadEvalApplyCases js

499+ , ret /= js = elimDeadLoop ret

500+ | otherwise = js

483

501

484deadEvalApplyCases :: [JS] -> [JS]

502deadEvalApplyCases :: [JS] -> [JS]

485deadEvalApplyCases js =

503deadEvalApplyCases js =

@@ -816,6 +834,131 @@ reduceConstants js

816 , ret /= js = reduceConstants ret

834 , ret /= js = reduceConstants ret

817 | otherwise = js

835 | otherwise = js

818

836

837+

838+elimDuplicateEvals :: JS -> JS

839+elimDuplicateEvals (JSAlloc fun (Just (JSFunction args (JSSeq seq)))) =

840+ JSAlloc fun $ Just (JSFunction args $ JSSeq (elimHelper seq))

841+ where

842+ elimHelper :: [JS] -> [JS]

843+ elimHelper (j@(JSAlloc var (Just val)):js) =

844+ j : map (jsSubst val (JSIdent var)) (elimHelper js)

845+ elimHelper (j:js) =

846+ j : elimHelper js

847+ elimHelper [] = []

848+

849+elimDuplicateEvals js = js

850+

851+optimizeEvalTailcalls :: (String, String) -> JS -> JS

852+optimizeEvalTailcalls (fun, tc) js =

853+ optHelper js

854+ where

855+ optHelper :: JS -> JS

856+ optHelper (JSApp (JSIdent "__IDRRT__tailcall") [

857+ JSFunction [] (JSReturn (JSApp (JSIdent n) args))

858+ ])

859+ | n == fun = JSApp (JSIdent tc) $ map optHelper args

860+

861+ optHelper (JSFunction args body) =

862+ JSFunction args $ optHelper body

863+

864+ optHelper (JSSeq seq) =

865+ JSSeq $ map optHelper seq

866+

867+ optHelper (JSReturn ret) =

868+ JSReturn $ optHelper ret

869+

870+ optHelper (JSApp lhs rhs) =

871+ JSApp (optHelper lhs) (map optHelper rhs)

872+

873+ optHelper (JSNew con args) =

874+ JSNew con $ map optHelper args

875+

876+ optHelper (JSOp op lhs rhs) =

877+ JSOp op (optHelper lhs) (optHelper rhs)

878+

879+ optHelper (JSProj obj field) =

880+ JSProj (optHelper obj) field

881+

882+ optHelper (JSArray vals) =

883+ JSArray $ map optHelper vals

884+

885+ optHelper (JSAssign lhs rhs) =

886+ JSAssign (optHelper lhs) (optHelper rhs)

887+

888+ optHelper (JSAlloc var (Just val)) =

889+ JSAlloc var (Just $ optHelper val)

890+

891+ optHelper (JSIndex lhs rhs) =

892+ JSIndex (optHelper lhs) (optHelper rhs)

893+

894+ optHelper (JSCond conds) =

895+ JSCond $ map (optHelper *** optHelper) conds

896+

897+ optHelper (JSTernary c t f) =

898+ JSTernary (

899+ optHelper c

900+ ) (

901+ optHelper t

902+ ) (

903+ optHelper f

904+ )

905+

906+ optHelper js = js

907+

908+

909+removeInstanceChecks :: JS -> JS

910+removeInstanceChecks (JSCond conds) =

911+ JSCond $ map (removeHelper *** removeInstanceChecks) conds

912+ where

913+ removeHelper (

914+ JSOp "&&" (JSOp "instanceof" _ (JSIdent "__IDRRT__Con")) check

915+ ) = removeHelper check

916+ removeHelper js = js

917+

918+removeInstanceChecks (JSFunction args body) =

919+ JSFunction args $ removeInstanceChecks body

920+

921+removeInstanceChecks (JSSeq seq) =

922+ JSSeq $ map removeInstanceChecks seq

923+

924+removeInstanceChecks (JSReturn ret) =

925+ JSReturn $ removeInstanceChecks ret

926+

927+removeInstanceChecks (JSApp lhs rhs) =

928+ JSApp (removeInstanceChecks lhs) $ map removeInstanceChecks rhs

929+

930+removeInstanceChecks (JSNew con args) =

931+ JSNew con $ map removeInstanceChecks args

932+

933+removeInstanceChecks (JSOp op lhs rhs) =

934+ JSOp op (removeInstanceChecks lhs) (removeInstanceChecks rhs)

935+

936+removeInstanceChecks (JSProj obj field) =

937+ JSProj (removeInstanceChecks obj) field

938+

939+removeInstanceChecks (JSArray vals) =

940+ JSArray $ map removeInstanceChecks vals

941+

942+removeInstanceChecks (JSAssign lhs rhs) =

943+ JSAssign (removeInstanceChecks lhs) (removeInstanceChecks rhs)

944+

945+removeInstanceChecks (JSAlloc var (Just val)) =

946+ JSAlloc var (Just $ removeInstanceChecks val)

947+

948+removeInstanceChecks (JSIndex lhs rhs) =

949+ JSIndex (removeInstanceChecks lhs) (removeInstanceChecks rhs)

950+

951+removeInstanceChecks (JSTernary c t f) =

952+ JSTernary (

953+ removeInstanceChecks c

954+ ) (

955+ removeInstanceChecks t

956+ ) (

957+ removeInstanceChecks f

958+ )

959+

960+removeInstanceChecks js = js

961+

819reduceLoop :: [String] -> ([JS], [JS]) -> [JS]

962reduceLoop :: [String] -> ([JS], [JS]) -> [JS]

820reduceLoop reduced (cons, program) =

963reduceLoop reduced (cons, program) =

821 case partition findConstructors program of

964 case partition findConstructors program of

@@ -942,8 +1085,13 @@ codegenJavaScript target definitions filename outputType = do

942 constRemoved = map reduceConstants reduced

1085 constRemoved = map reduceConstants reduced

943 constrInit = initConstructors constRemoved

1086 constrInit = initConstructors constRemoved

944 removeAlloc = map removeAllocations constrInit

1087 removeAlloc = map removeAllocations constrInit

945− deadElim = deadEvalApplyCases removeAlloc

1088+ deadElim = elimDeadLoop removeAlloc

946− js = inlineFunctions deadElim in

1089+ inlined = inlineFunctions deadElim

1090+ elimDup = map elimDuplicateEvals inlined

1091+ evalTC = map (optimizeEvalTailcalls ("__IDR__mEVAL0", "__IDRRT__EVALTC")) elimDup

1092+ applyTC = map (optimizeEvalTailcalls ("__IDR__mAPPLY0", "__IDRRT__APPLYTC")) evalTC

1093+ remChecks = map removeInstanceChecks applyTC

1094+ js = remChecks in

947 map compileJS js

1095 map compileJS js

948

1096

949 mainLoop :: JS

1097 mainLoop :: JS

src/Idris/AbsSyntaxTree.hs+5−2

@@ -26,6 +26,7 @@ import Data.List

26import Data.Char

27import qualified Data.Map as M

28import qualified Data.Text as T

29+import qualified Data.Map as M

29import Data.Either

30import Data.Either

30import qualified Data.Set as S

31import qualified Data.Set as S

31import Data.Word (Word)

32import Data.Word (Word)

@@ -142,7 +143,9 @@ data IState = IState {

142 idris_outh :: Handle,

143 idris_outh :: Handle,

143 idris_errorhandlers :: [Name], -- ^ Global error handlers

144 idris_errorhandlers :: [Name], -- ^ Global error handlers

144 idris_nameIdx :: (Int, Ctxt (Int, Name)),

145 idris_nameIdx :: (Int, Ctxt (Int, Name)),

145− idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers

146+ idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

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

148+

146 }

149 }

147

150

148data SizeChange = Smaller | Same | Bigger | Unknown

151data SizeChange = Smaller | Same | Bigger | Unknown

@@ -211,7 +214,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

211 emptyContext

214 emptyContext

212 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

215 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

213 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

216 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

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

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

215

218

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

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

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

220-- 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/Delaborate.hs+1−1

@@ -185,7 +185,7 @@ pprintErr' i (NotInjective p x y) =

185 pprintTerm i (delab i y)

186pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

187pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

188− cat (punctuate comma (map text as))

188+ cat (punctuate (comma <> space) (map text as))

189pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

190pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

191pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)

src/Idris/ElabTerm.hs+3−1

@@ -232,7 +232,9 @@ elab ist info pattern opts fn tm

232 let (tc, _) = unApply ty

233 let as' = pruneByType tc ctxt as

234 tryAll (zip (map (elab' ina) as') (map showHd as'))

235− where showHd (PApp _ h _) = show h

235+ where showHd (PApp _ (PRef _ n) _) = show n

236+ showHd (PRef _ n) = show n

237+ showHd (PApp _ h _) = show h

236 showHd x = show x

238 showHd x = show x

237 elab' ina (PAlternative False as)

239 elab' ina (PAlternative False as)

238 = trySeq as

240 = trySeq as

src/Idris/ParseExpr.hs+1

@@ -757,6 +757,7 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;

757 <?> "quote goal expression"

758

759{- | Parses a dependent type signature

760+

760@

761@

761Pi ::=

762Pi ::=

762 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

763 '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

src/Idris/ParseHelpers.hs+34−19

@@ -25,13 +25,14 @@ 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

32import System.FilePath

33import System.FilePath

34−-- | Idris parser with state used during parsing

35+-- | Idris parser with state used during parsing

35type IdrisParser = StateT IState IdrisInnerParser

36type IdrisParser = StateT IState IdrisInnerParser

37newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

38newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

@@ -40,7 +41,7 @@ newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

40instance TokenParsing IdrisInnerParser where

41instance TokenParsing IdrisInnerParser where

41 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

42 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

43−-- | Generalized monadic parsing constraint type

44+-- | Generalized monadic parsing constraint type

44type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

45type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

46-- | Helper to run Idris inner parser based stateT parsers

47-- | Helper to run Idris inner parser based stateT parsers

@@ -49,7 +50,7 @@ runparser p i inputname = parseString (runInnerParser (evalStateT p i)) (Directe

50{- * Space, comments and literals (token/lexing like parsers) -}

51{- * Space, comments and literals (token/lexing like parsers) -}

52−-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

53+-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)

53simpleWhiteSpace :: MonadicParsing m => m ()

54simpleWhiteSpace :: MonadicParsing m => m ()

54simpleWhiteSpace = satisfy isSpace *> pure ()

55simpleWhiteSpace = satisfy isSpace *> pure ()

@@ -68,9 +69,12 @@ isDocCommentMarker '^' = True

68isDocCommentMarker _ = False

69isDocCommentMarker _ = False

70{- | Consumes a single-line comment

71{- | Consumes a single-line comment

72+

73+@

71 SingleLineComment_t ::= '--' EOL_t

74 SingleLineComment_t ::= '--' EOL_t

72 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

75 | '--' ~DocCommentMarker_t ~EOL_t* EOL_t

73 ;

76 ;

77+@

74 -}

78 -}

75singleLineComment :: MonadicParsing m => m ()

79singleLineComment :: MonadicParsing m => m ()

76singleLineComment = try (string "--" *> eol *> pure ())

80singleLineComment = try (string "--" *> eol *> pure ())

@@ -78,18 +82,22 @@ singleLineComment = try (string "--" *> eol *> pure ())

78 <?> ""

82 <?> ""

80{- | Consumes a multi-line comment

84{- | Consumes a multi-line comment

85+

86+@

81 MultiLineComment_t ::=

87 MultiLineComment_t ::=

82 '{ -- }'

88 '{ -- }'

83 | '{ -' ~DocCommentMarker_t InCommentChars_t

89 | '{ -' ~DocCommentMarker_t InCommentChars_t

84 ;

90 ;

91+@

93+@

86 InCommentChars_t ::=

94 InCommentChars_t ::=

87 '- }'

95 '- }'

88 | MultiLineComment_t InCommentChars_t

96 | MultiLineComment_t InCommentChars_t

89 | ~'- }'+ InCommentChars_t

97 | ~'- }'+ InCommentChars_t

90 ;

98 ;

99+@

91− -}

100+-}

92−

93multiLineComment :: MonadicParsing m => m ()

101multiLineComment :: MonadicParsing m => m ()

94multiLineComment = try (string "{-" *> (string "-}") *> pure ())

102multiLineComment = try (string "{-" *> (string "-}") *> pure ())

95 <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

103 <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars

@@ -106,9 +114,12 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())

106 startEnd = "{}-"

114 startEnd = "{}-"

107

115

108{-| Parses a documentation comment (similar to haddoc) given a marker character

116{-| Parses a documentation comment (similar to haddoc) given a marker character

117+

118+@

109 DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t

119 DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t

110 | '{ -' DocCommentMarket_t ~'- }'* '- }'

120 | '{ -' DocCommentMarket_t ~'- }'* '- }'

111 ;

121 ;

122+@

112 -}

123 -}

113docComment :: MonadicParsing m => Char -> m String

124docComment :: MonadicParsing m => Char -> m String

114docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

125docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)

@@ -138,14 +149,14 @@ natural = Tok.natural

138integer :: MonadicParsing m => m Integer

149integer :: MonadicParsing m => m Integer

139integer = Tok.integer

150integer = Tok.integer

140

151

141−-- | Parses a floating point number

152+-- | Parses a floating point number

142float :: MonadicParsing m => m Double

153float :: MonadicParsing m => m Double

143float = Tok.double

154float = Tok.double

144

155

145{- * Symbols, identifiers, names and operators -}

156{- * Symbols, identifiers, names and operators -}

146

157

147

158

148−-- | Idris Style for parsing identifiers/reserved keywords

159+-- | Idris Style for parsing identifiers/reserved keywords

149idrisStyle :: MonadicParsing m => IdentifierStyle m

160idrisStyle :: MonadicParsing m => IdentifierStyle m

150idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier

161idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier

151 where _styleName = "Idris"

162 where _styleName = "Idris"

@@ -210,14 +221,18 @@ maybeWithNS parser ascend bad = do

210

221

211-- | Parses a name

222-- | Parses a name

212name :: IdrisParser Name

223name :: IdrisParser Name

213−name = do i <- get

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

214− iName (syntax_keywords i)

225+ keywords <- syntax_keywords <$> get

215− <?> "name"

226+ aliases <- module_aliases <$> get

216−

227+ unalias aliases <$> iName keywords

217−

228+ where

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

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

231+ unalias aliases name = name

232+

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

233+{- | List of all initial segments in ascending order of a list. Every

219− initial segment ends right before an element satisfying the given

234+such initial segment ends right before an element satisfying the given

220− condition.

235+condition.

221-}

236-}

222initsEndAt :: (a -> Bool) -> [a] -> [[a]]

237initsEndAt :: (a -> Bool) -> [a] -> [[a]]

223initsEndAt p [] = []

238initsEndAt p [] = []

@@ -226,7 +241,7 @@ initsEndAt p (x:xs) | p x = [] : x_inits_xs

226 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]

241 where x_inits_xs = [x : cs | cs <- initsEndAt p xs]

227

242

228

243

229−{- | Create a `Name' from a pair of strings representing a base name and its

244+{- | Create a `Name' from a pair of strings representing a base name and its

230 namespace.

245 namespace.

231-}

246-}

232mkName :: (String, String) -> Name

247mkName :: (String, String) -> Name

@@ -304,7 +319,7 @@ lastIndent = do ist <- get

304 (x : xs) -> return x

319 (x : xs) -> return x

305 _ -> return 1

320 _ -> return 1

306

321

307−-- | Applies parser in an indented position

322+-- | Applies parser in an indented position

308indented :: IdrisParser a -> IdrisParser a

323indented :: IdrisParser a -> IdrisParser a

309indented p = notEndBlock *> p <* keepTerminator

324indented p = notEndBlock *> p <* keepTerminator

310

325

@@ -326,7 +341,7 @@ indentedBlock1 p = do openBlock

326 closeBlock

341 closeBlock

327 return res

342 return res

328

343

329−-- | Applies parser to get a block with exactly one (possibly indented) statement

344+-- | Applies parser to get a block with exactly one (possibly indented) statement

330indentedBlockS :: IdrisParser a -> IdrisParser a

345indentedBlockS :: IdrisParser a -> IdrisParser a

331indentedBlockS p = do openBlock

346indentedBlockS p = do openBlock

332 pushIndent

347 pushIndent

@@ -452,7 +467,7 @@ accessibility = do reserved "public"; return Public

452 <|> do reserved "private"; return Hidden

467 <|> do reserved "private"; return Hidden

453 <?> "accessibility modifier"

468 <?> "accessibility modifier"

454

469

455−-- | Adds accessibility option for function

470+-- | Adds accessibility option for function

456addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

471addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

457addAcc n a = do i <- get

472addAcc n a = do i <- get

458 put (i { hide_list = (n, a) : hide_list i })

473 put (i { hide_list = (n, a) : hide_list i })

src/Idris/Parser.hs+179−35

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

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

48import Control.Monad.State.Strict

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

@@ -63,6 +66,7 @@ import System.FilePath

63import System.IO

66import System.IO

65{-

68{-

69+@

66 grammar shortcut notation:

70 grammar shortcut notation:

67 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)

71 ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)

68 RULE? = optional rule (i.e. RULE or nothing)

72 RULE? = optional rule (i.e. RULE or nothing)

@@ -70,12 +74,16 @@ import System.IO

70 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)

74 RULE+ = repeated rule with at least one match (i.e. RULE one or more times)

71 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)

75 RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)

72 RULE{n} = rule repeated n times

76 RULE{n} = rule repeated n times

77+@

73-}

78-}

75{- * Main grammar -}

80{- * Main grammar -}

77{- | Parses module definition

82{- | Parses module definition

83+

84+@

78 ModuleHeader ::= 'module' Identifier_t ';'?;

85 ModuleHeader ::= 'module' Identifier_t ';'?;

86+@

79-}

87-}

80moduleHeader :: IdrisParser [String]

88moduleHeader :: IdrisParser [String]

81moduleHeader = try (do reserved "module"

89moduleHeader = try (do reserved "module"

@@ -90,18 +98,26 @@ moduleHeader = try (do reserved "module"

90 (x, '.':y) -> x : moduleName y

98 (x, '.':y) -> x : moduleName y

92{- | Parses an import statement

100{- | Parses an import statement

101+

102+@

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

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

104+@

94 -}

105 -}

95−import_ :: IdrisParser String

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

107+import_ = do fc <- getFC

96−import_ = do reserved "import"

108+ reserved "import"

97 id <- identifier

109 id <- identifier

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

98 option ';' (lchar ';')

111 option ';' (lchar ';')

99− return (toPath id)

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

100 <?> "import statement"

113 <?> "import statement"

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

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

102

115

103{- | Parses program source

116{- | Parses program source

117+

118+@

104 Prog ::= Decl* EOF;

119 Prog ::= Decl* EOF;

120+@

105 -}

121 -}

106prog :: SyntaxInfo -> IdrisParser [PDecl]

122prog :: SyntaxInfo -> IdrisParser [PDecl]

107prog syn = do whiteSpace

123prog syn = do whiteSpace

@@ -111,7 +127,9 @@ prog syn = do whiteSpace

111 let c = (concat decls)

127 let c = (concat decls)

112 return c

128 return c

113

129

114−{- | Parses a top-level declaration

130+{-| Parses a top-level declaration

131+

132+@

115Decl ::=

133Decl ::=

116 Decl'

134 Decl'

117 | Using

135 | Using

@@ -126,6 +144,7 @@ Decl ::=

126 | Transform

144 | Transform

127 | Import!

145 | Import!

128 ;

146 ;

147+@

129-}

148-}

130decl :: SyntaxInfo -> IdrisParser [PDecl]

149decl :: SyntaxInfo -> IdrisParser [PDecl]

131decl syn = do notEndBlock

150decl syn = do notEndBlock

@@ -151,6 +170,8 @@ decl syn = do notEndBlock

151 return [d']

170 return [d']

152

171

153{- | Parses a top-level declaration with possible syntax sugar

172{- | Parses a top-level declaration with possible syntax sugar

173+

174+@

154Decl' ::=

175Decl' ::=

155 Fixity

176 Fixity

156 | FunDecl'

177 | FunDecl'

@@ -158,6 +179,7 @@ Decl' ::=

158 | Record

179 | Record

159 | SyntaxDecl

180 | SyntaxDecl

160 ;

181 ;

182+@

161-}

183-}

162decl' :: SyntaxInfo -> IdrisParser PDecl

184decl' :: SyntaxInfo -> IdrisParser PDecl

163decl' syn = fixity

185decl' syn = fixity

@@ -168,7 +190,10 @@ decl' syn = fixity

168 <?> "declaration"

190 <?> "declaration"

169

191

170{- | Parses a syntax extension declaration (and adds the rule to parser state)

192{- | Parses a syntax extension declaration (and adds the rule to parser state)

193+

194+@

171 SyntaxDecl ::= SyntaxRule;

195 SyntaxDecl ::= SyntaxRule;

196+@

172-}

197-}

173syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

198syntaxDecl :: SyntaxInfo -> IdrisParser PDecl

174syntaxDecl syn = do s <- syntaxRule syn

199syntaxDecl syn = do s <- syntaxRule syn

@@ -186,17 +211,24 @@ syntaxDecl syn = do s <- syntaxRule syn

186 ename (Keyword n) = Just n

211 ename (Keyword n) = Just n

187 ename _ = Nothing

212 ename _ = Nothing

188

213

189−{- | Parses a syntax extension declaration

214+{- | Parses a syntax extension declaration

215+

216+@

190−SyntaxRuleOpts ::= 'term' | 'pattern';

217+SyntaxRuleOpts ::= 'term' | 'pattern';

218+@

191

219

220+@

192SyntaxRule ::=

221SyntaxRule ::=

193 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;

222 SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;

223+@

194

224

225+@

195SyntaxSym ::= '[' Name_t ']'

226SyntaxSym ::= '[' Name_t ']'

196 | '{' Name_t '}'

227 | '{' Name_t '}'

197 | Name_t

228 | Name_t

198 | StringLiteral_t

229 | StringLiteral_t

199 ;

230 ;

231+@

200-}

232-}

201syntaxRule :: SyntaxInfo -> IdrisParser Syntax

233syntaxRule :: SyntaxInfo -> IdrisParser Syntax

202syntaxRule syn

234syntaxRule syn

@@ -232,11 +264,14 @@ syntaxRule syn

232

264

233

265

234{- | Parses a syntax symbol (either binding variable, keyword or expression)

266{- | Parses a syntax symbol (either binding variable, keyword or expression)

267+

268+@

235SyntaxSym ::= '[' Name_t ']'

269SyntaxSym ::= '[' Name_t ']'

236 | '{' Name_t '}'

270 | '{' Name_t '}'

237 | Name_t

271 | Name_t

238 | StringLiteral_t

272 | StringLiteral_t

239 ;

273 ;

274+@

240 -}

275 -}

241syntaxSym :: IdrisParser SSymbol

276syntaxSym :: IdrisParser SSymbol

242syntaxSym = try (do lchar '['; n <- name; lchar ']'

277syntaxSym = try (do lchar '['; n <- name; lchar ']'

@@ -250,7 +285,10 @@ syntaxSym = try (do lchar '['; n <- name; lchar ']'

250 <?> "syntax symbol"

285 <?> "syntax symbol"

251

286

252{- | Parses a function declaration with possible syntax sugar

287{- | Parses a function declaration with possible syntax sugar

288+

289+@

253 FunDecl ::= FunDecl';

290 FunDecl ::= FunDecl';

291+@

254-}

292-}

255fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

293fnDecl :: SyntaxInfo -> IdrisParser [PDecl]

256fnDecl syn = try (do notEndBlock

294fnDecl syn = try (do notEndBlock

@@ -259,13 +297,16 @@ fnDecl syn = try (do notEndBlock

259 let d' = fmap (desugar syn i) d

297 let d' = fmap (desugar syn i) d

260 return [d']) <?> "function declaration"

298 return [d']) <?> "function declaration"

261

299

262−{- Parses a function declaration

300+{-| Parses a function declaration

301+

302+@

263 FunDecl' ::=

303 FunDecl' ::=

264 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator

304 DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator

265 | Postulate

305 | Postulate

266 | Pattern

306 | Pattern

267 | CAF

307 | CAF

268 ;

308 ;

309+@

269-}

310-}

270fnDecl' :: SyntaxInfo -> IdrisParser PDecl

311fnDecl' :: SyntaxInfo -> IdrisParser PDecl

271fnDecl' syn = checkFixity $

312fnDecl' syn = checkFixity $

@@ -309,23 +350,29 @@ fnDecl' syn = checkFixity $

309 | otherwise = return True

350 | otherwise = return True

310 fixityOK _ = return True

351 fixityOK _ = return True

311

352

312−{- Parses function options given initial options

353+{-| Parses function options given initial options

354+

355+@

313FnOpts ::= 'total'

356FnOpts ::= 'total'

314 | 'partial'

357 | 'partial'

315 | 'implicit'

358 | 'implicit'

316 | '%' 'assert_total'

359 | '%' 'assert_total'

317 | '%' 'error_handler'

360 | '%' 'error_handler'

318− | '%' 'reflection'

361+ | '%' 'reflection'

319 | '%' 'specialise' '[' NameTimesList? ']'

362 | '%' 'specialise' '[' NameTimesList? ']'

320 ;

363 ;

364+@

321

365

366+@

322NameTimes ::= FnName Natural?;

367NameTimes ::= FnName Natural?;

368+@

323

369

370+@

324NameTimesList ::=

371NameTimesList ::=

325 NameTimes

372 NameTimes

326 | NameTimes ',' NameTimesList

373 | NameTimes ',' NameTimesList

327 ;

374 ;

328−

375+@

329-}

376-}

330-- FIXME: Check compatability for function options (i.e. partal/total)

377-- FIXME: Check compatability for function options (i.e. partal/total)

331fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

378fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

@@ -356,9 +403,11 @@ fnOpts opts

356

403

357{- | Parses a postulate

404{- | Parses a postulate

358

405

406+@

359Postulate ::=

407Postulate ::=

360 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator

408 DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator

361 ;

409 ;

410+@

362-}

411-}

363postulate :: SyntaxInfo -> IdrisParser PDecl

412postulate :: SyntaxInfo -> IdrisParser PDecl

364postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

413postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

@@ -384,9 +433,11 @@ postulate syn = do doc <- try $ do doc <- option "" (docComment '|')

384

433

385{- | Parses a using declaration

434{- | Parses a using declaration

386

435

436+@

387Using ::=

437Using ::=

388 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock

438 'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock

389 ;

439 ;

440+@

390 -}

441 -}

391using_ :: SyntaxInfo -> IdrisParser [PDecl]

442using_ :: SyntaxInfo -> IdrisParser [PDecl]

392using_ syn =

443using_ syn =

@@ -398,11 +449,13 @@ using_ syn =

398 return (concat ds)

449 return (concat ds)

399 <?> "using declaration"

450 <?> "using declaration"

400

451

401−{- | Parses a parameters declaration

452+{- | Parses a parameters declaration

402

453

454+@

403Params ::=

455Params ::=

404 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock

456 'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock

405 ;

457 ;

458+@

406 -}

459 -}

407params :: SyntaxInfo -> IdrisParser [PDecl]

460params :: SyntaxInfo -> IdrisParser [PDecl]

408params syn =

461params syn =

@@ -417,9 +470,11 @@ params syn =

417

470

418{- | Parses a mutual declaration (for mutually recursive functions)

471{- | Parses a mutual declaration (for mutually recursive functions)

419

472

473+@

420Mutual ::=

474Mutual ::=

421 'mutual' OpenBlock Decl* CloseBlock

475 'mutual' OpenBlock Decl* CloseBlock

422 ;

476 ;

477+@

423-}

478-}

424mutual :: SyntaxInfo -> IdrisParser [PDecl]

479mutual :: SyntaxInfo -> IdrisParser [PDecl]

425mutual syn =

480mutual syn =

@@ -432,11 +487,13 @@ mutual syn =

432 return [PMutual fc (concat ds)]

487 return [PMutual fc (concat ds)]

433 <?> "mutual block"

488 <?> "mutual block"

434

489

435−{- | Parses a namespace declaration

490+{-| Parses a namespace declaration

436

491

492+@

437Namespace ::=

493Namespace ::=

438 'namespace' identifier OpenBlock Decl+ CloseBlock

494 'namespace' identifier OpenBlock Decl+ CloseBlock

439 ;

495 ;

496+@

440-}

497-}

441namespace :: SyntaxInfo -> IdrisParser [PDecl]

498namespace :: SyntaxInfo -> IdrisParser [PDecl]

442namespace syn =

499namespace syn =

@@ -447,9 +504,12 @@ namespace syn =

447 return [PNamespace n (concat ds)]

504 return [PNamespace n (concat ds)]

448 <?> "namespace declaration"

505 <?> "namespace declaration"

449

506

450−{- |Parses a methods block (for instances)

507+{- | Parses a methods block (for instances)

508+

509+@

451 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

510 InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

511+@

452− -}

512+-}

453instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

513instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

454instanceBlock syn = do reserved "where"

514instanceBlock syn = do reserved "where"

455 openBlock

515 openBlock

@@ -458,16 +518,20 @@ instanceBlock syn = do reserved "where"

458 return (concat ds)

518 return (concat ds)

459 <?> "instance block"

519 <?> "instance block"

460

520

461−{- |Parses a methods and instances block (for type classes)

521+{- | Parses a methods and instances block (for type classes)

462

522

523+@

463MethodOrInstance ::=

524MethodOrInstance ::=

464 FnDecl

525 FnDecl

465 | Instance

526 | Instance

466 ;

527 ;

528+@

467

529

530+@

468ClassBlock ::=

531ClassBlock ::=

469 'where' OpenBlock MethodOrInstance* CloseBlock

532 'where' OpenBlock MethodOrInstance* CloseBlock

470 ;

533 ;

534+@

471-}

535-}

472classBlock :: SyntaxInfo -> IdrisParser [PDecl]

536classBlock :: SyntaxInfo -> IdrisParser [PDecl]

473classBlock syn = do reserved "where"

537classBlock syn = do reserved "where"

@@ -477,16 +541,20 @@ classBlock syn = do reserved "where"

477 return (concat ds)

541 return (concat ds)

478 <?> "class block"

542 <?> "class block"

479

543

480−{- |Parses a type class declaration

544+{-| Parses a type class declaration

481

545

546+@

482ClassArgument ::=

547ClassArgument ::=

483 Name

548 Name

484 | '(' Name ':' Expr ')'

549 | '(' Name ':' Expr ')'

485 ;

550 ;

551+@

486

552

553+@

487Class ::=

554Class ::=

488 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?

555 DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?

489 ;

556 ;

557+@

490-}

558-}

491class_ :: SyntaxInfo -> IdrisParser [PDecl]

559class_ :: SyntaxInfo -> IdrisParser [PDecl]

492class_ syn = do (doc, acc) <- try (do

560class_ syn = do (doc, acc) <- try (do

@@ -507,13 +575,17 @@ class_ syn = do (doc, acc) <- try (do

507 <|> do i <- name;

575 <|> do i <- name;

508 return (i, PType)

576 return (i, PType)

509

577

510−{- |Parses a type class instance declaration

578+{- | Parses a type class instance declaration

511

579

580+@

512 Instance ::=

581 Instance ::=

513 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

582 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

514 ;

583 ;

584+@

515

585

586+@

516− InstanceName ::= '[' Name ']';

587+InstanceName ::= '[' Name ']';

588+@

517-}

589-}

518instance_ :: SyntaxInfo -> IdrisParser [PDecl]

590instance_ :: SyntaxInfo -> IdrisParser [PDecl]

519instance_ syn = do reserved "instance"; fc <- getFC

591instance_ syn = do reserved "instance"; fc <- getFC

@@ -534,20 +606,27 @@ instance_ syn = do reserved "instance"; fc <- getFC

534

606

535

607

536{- | Parses a using declaration list

608{- | Parses a using declaration list

609+

610+@

537UsingDeclList ::=

611UsingDeclList ::=

538 UsingDeclList'

612 UsingDeclList'

539 | NameList TypeSig

613 | NameList TypeSig

540 ;

614 ;

615+@

541

616

617+@

542UsingDeclList' ::=

618UsingDeclList' ::=

543 UsingDecl

619 UsingDecl

544 | UsingDecl ',' UsingDeclList'

620 | UsingDecl ',' UsingDeclList'

545 ;

621 ;

622+@

546

623

624+@

547NameList ::=

625NameList ::=

548 Name

626 Name

549 | Name ',' NameList

627 | Name ',' NameList

550 ;

628 ;

629+@

551-}

630-}

552usingDeclList :: SyntaxInfo -> IdrisParser [Using]

631usingDeclList :: SyntaxInfo -> IdrisParser [Using]

553usingDeclList syn

632usingDeclList syn

@@ -559,10 +638,13 @@ usingDeclList syn

559 <?> "using declaration list"

638 <?> "using declaration list"

560

639

561{- |Parses a using declaration

640{- |Parses a using declaration

641+

642+@

562UsingDecl ::=

643UsingDecl ::=

563 FnName TypeSig

644 FnName TypeSig

564 | FnName FnName+

645 | FnName FnName+

565 ;

646 ;

647+@

566-}

648-}

567usingDecl :: SyntaxInfo -> IdrisParser Using

649usingDecl :: SyntaxInfo -> IdrisParser Using

568usingDecl syn = try (do x <- fnName

650usingDecl syn = try (do x <- fnName

@@ -574,8 +656,11 @@ usingDecl syn = try (do x <- fnName

574 return (UConstraint c xs)

656 return (UConstraint c xs)

575 <?> "using declaration"

657 <?> "using declaration"

576

658

577−{- | Parse a clause with patterns

659+{- | Parse a clause with patterns

660+

661+@

578Pattern ::= Clause;

662Pattern ::= Clause;

663+@

579-}

664-}

580pattern :: SyntaxInfo -> IdrisParser PDecl

665pattern :: SyntaxInfo -> IdrisParser PDecl

581pattern syn = do fc <- getFC

666pattern syn = do fc <- getFC

@@ -584,7 +669,10 @@ pattern syn = do fc <- getFC

584 <?> "pattern"

669 <?> "pattern"

585

670

586{- | Parse a constant applicative form declaration

671{- | Parse a constant applicative form declaration

672+

673+@

587− CAF ::= 'let' FnName '=' Expr Terminator;

674+CAF ::= 'let' FnName '=' Expr Terminator;

675+@

588-}

676-}

589caf :: SyntaxInfo -> IdrisParser PDecl

677caf :: SyntaxInfo -> IdrisParser PDecl

590caf syn = do reserved "let"

678caf syn = do reserved "let"

@@ -597,7 +685,10 @@ caf syn = do reserved "let"

597 <?> "constant applicative form declaration"

685 <?> "constant applicative form declaration"

598

686

599{- | Parse an argument expression

687{- | Parse an argument expression

688+

689+@

600− ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

690+ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};

691+@

601-}

692-}

602argExpr :: SyntaxInfo -> IdrisParser PTerm

693argExpr :: SyntaxInfo -> IdrisParser PTerm

603argExpr syn = let syn' = syn { inPattern = True } in

694argExpr syn = let syn' = syn { inPattern = True } in

@@ -605,12 +696,17 @@ argExpr syn = let syn' = syn { inPattern = True } in

605 <?> "argument expression"

696 <?> "argument expression"

606

697

607{- | Parse a right hand side of a function

698{- | Parse a right hand side of a function

699+

700+@

608RHS ::= '=' Expr

701RHS ::= '=' Expr

609 | '?=' RHSName? Expr

702 | '?=' RHSName? Expr

610 | 'impossible'

703 | 'impossible'

611 ;

704 ;

705+@

612

706

707+@

613RHSName ::= '{' FnName '}';

708RHSName ::= '{' FnName '}';

709+@

614-}

710-}

615rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

711rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

616rhs syn n = do lchar '='; expr syn

712rhs syn n = do lchar '='; expr syn

@@ -633,16 +729,28 @@ rhs syn n = do lchar '='; expr syn

633 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))

729 addLet nm r = (PLet (sUN "value") Placeholder r (PMetavar nm))

634

730

635{- |Parses a function clause

731{- |Parses a function clause

732+

733+@

636RHSOrWithBlock ::= RHS WhereOrTerminator

734RHSOrWithBlock ::= RHS WhereOrTerminator

637 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

735 | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock

638 ;

736 ;

737+@

738+

739+@

639Clause ::= WExpr+ RHSOrWithBlock

740Clause ::= WExpr+ RHSOrWithBlock

640 | SimpleExpr '<==' FnName RHS WhereOrTerminator

741 | SimpleExpr '<==' FnName RHS WhereOrTerminator

641 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}

742 | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}

642 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

743 | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock

643 ;

744 ;

745+@

746+

747+@

644ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

748ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;

749+@

750+

751+@

645−WhereOrTerminator ::= WhereBlock | Terminator;

752+WhereOrTerminator ::= WhereBlock | Terminator;

753+@

646-}

754-}

647clause :: SyntaxInfo -> IdrisParser PClause

755clause :: SyntaxInfo -> IdrisParser PClause

648clause syn

756clause syn

@@ -771,17 +879,23 @@ clause syn

771 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)

879 fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)

772 fillLHSD n c a x = x

880 fillLHSD n c a x = x

773

881

774−{- |Parses with pattern

882+{-| Parses with pattern

883+

884+@

775− WExpr ::= '|' Expr';

885+WExpr ::= '|' Expr';

886+@

776-}

887-}

777wExpr :: SyntaxInfo -> IdrisParser PTerm

888wExpr :: SyntaxInfo -> IdrisParser PTerm

778wExpr syn = do lchar '|'

889wExpr syn = do lchar '|'

779 expr' syn

890 expr' syn

780 <?> "with pattern"

891 <?> "with pattern"

781

892

782−{- |Parses a where block

893+{- | Parses a where block

894+

895+@

783WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

896WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

897+@

784− -}

898+-}

785whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

899whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

786whereBlock n syn

900whereBlock n syn

787 = do reserved "where"

901 = do reserved "where"

@@ -791,6 +905,8 @@ whereBlock n syn

791 <?> "where block"

905 <?> "where block"

792

906

793{- |Parses a code generation target language name

907{- |Parses a code generation target language name

908+

909+@

794Codegen ::= 'C'

910Codegen ::= 'C'

795 | 'Java'

911 | 'Java'

796 | 'JavaScript'

912 | 'JavaScript'

@@ -798,6 +914,7 @@ Codegen ::= 'C'

798 | 'LLVM'

914 | 'LLVM'

799 | 'Bytecode'

915 | 'Bytecode'

800 ;

916 ;

917+@

801-}

918-}

802codegen_ :: IdrisParser Codegen

919codegen_ :: IdrisParser Codegen

803codegen_ = do reserved "C"; return ViaC

920codegen_ = do reserved "C"; return ViaC

@@ -809,13 +926,18 @@ codegen_ = do reserved "C"; return ViaC

809 <?> "code generation language"

926 <?> "code generation language"

810

927

811{- |Parses a compiler directive

928{- |Parses a compiler directive

929+@

812StringList ::=

930StringList ::=

813 String

931 String

814 | String ',' StringList

932 | String ',' StringList

815 ;

933 ;

934+@

816

935

936+@

817Directive ::= '%' Directive';

937Directive ::= '%' Directive';

938+@

818

939

940+@

819Directive' ::= 'lib' CodeGen String_t

941Directive' ::= 'lib' CodeGen String_t

820 | 'link' CodeGen String_t

942 | 'link' CodeGen String_t

821 | 'flag' CodeGen String_t

943 | 'flag' CodeGen String_t

@@ -831,6 +953,7 @@ Directive' ::= 'lib' CodeGen String_t

831 | 'language' 'TypeProviders'

953 | 'language' 'TypeProviders'

832 | 'language' 'ErrorReflection'

954 | 'language' 'ErrorReflection'

833 ;

955 ;

956+@

834-}

957-}

835directive :: SyntaxInfo -> IdrisParser [PDecl]

958directive :: SyntaxInfo -> IdrisParser [PDecl]

836directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;

959directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;

@@ -899,15 +1022,22 @@ pLangExt = (reserved "TypeProviders" >> return TypeProviders)

899 <|> (reserved "ErrorReflection" >> return ErrorReflection)

1022 <|> (reserved "ErrorReflection" >> return ErrorReflection)

900

1023

901{- | Parses a totality

1024{- | Parses a totality

1025+

1026+@

902Totality ::= 'partial' | 'total'

1027Totality ::= 'partial' | 'total'

1028+@

1029+

903-}

1030-}

904totality :: IdrisParser Bool

1031totality :: IdrisParser Bool

905totality

1032totality

906 = do reserved "total"; return True

1033 = do reserved "total"; return True

907 <|> do reserved "partial"; return False

1034 <|> do reserved "partial"; return False

908

1035

909−{- | Parses a type provider

1036+{- | Parses a type provider

1037+

1038+@

910Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1039Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;

1040+@

911 -}

1041 -}

912provider :: SyntaxInfo -> IdrisParser [PDecl]

1042provider :: SyntaxInfo -> IdrisParser [PDecl]

913provider syn = do try (lchar '%' *> reserved "provide");

1043provider syn = do try (lchar '%' *> reserved "provide");

@@ -919,7 +1049,10 @@ provider syn = do try (lchar '%' *> reserved "provide");

919 <?> "type provider"

1049 <?> "type provider"

920

1050

921{- | Parses a transform

1051{- | Parses a transform

1052+

1053+@

922Transform ::= '%' 'transform' Expr '==>' Expr

1054Transform ::= '%' 'transform' Expr '==>' Expr

1055+@

923-}

1056-}

924transform :: SyntaxInfo -> IdrisParser [PDecl]

1057transform :: SyntaxInfo -> IdrisParser [PDecl]

925transform syn = do try (lchar '%' *> reserved "transform")

1058transform syn = do try (lchar '%' *> reserved "transform")

@@ -945,7 +1078,7 @@ parseTactic :: IState -> String -> Result PTactic

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

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

946

1079

947-- | Parse module header and imports

1080-- | 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)

949parseImports fname input

1082parseImports fname input

950 = do i <- getIState

1083 = do i <- getIState

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

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

@@ -953,7 +1086,7 @@ parseImports fname input

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

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

954 -- none anyway)

1087 -- none anyway)

955 return x

1088 return x

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

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

957 imports = do whiteSpace

1090 imports = do whiteSpace

958 mname <- moduleHeader

1091 mname <- moduleHeader

959 ps <- many import_

1092 ps <- many import_

@@ -1064,13 +1197,24 @@ loadSource h lidr f

1064 let def_total = default_total i

1197 let def_total = default_total i

1065 file_in <- runIO $ readFile f

1198 file_in <- runIO $ readFile f

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

1199 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+

1068 i <- getIState

1212 i <- getIState

1069− putIState (i { default_access = Hidden })

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

1070 clearIBC -- start a new .ibc file

1214 clearIBC -- start a new .ibc file

1071− mapM_ (addIBC . IBCImport) modules

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

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

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

1073− f file pos

1217+ ds' <- parseProg syntax f file pos

1074 unless (null ds') $ do

1218 unless (null ds') $ do

1075 let ds = namespaces mname ds'

1219 let ds = namespaces mname ds'

1076 logLvl 3 (show $ showDecls True ds)

1220 logLvl 3 (show $ showDecls True ds)

src/Pkg/Package.hs+2−2

@@ -24,14 +24,14 @@ import Pkg.PParser

25import Paths_idris (getDataDir)

27−-- | Run the package through the idris compiler.

28−--

29-- To build a package:

27-- To build a package:

30-- * read the package description

28-- * read the package description

31-- * check all the library dependencies exist

29-- * check all the library dependencies exist

32-- * invoke the makefile if there is one

30-- * invoke the makefile if there is one

33-- * invoke idris on each module, with idris_opts

31-- * invoke idris on each module, with idris_opts

34-- * install everything into datadir/pname, if install flag is set

32-- * install everything into datadir/pname, if install flag is set

33+

34+-- | Run the package through the idris compiler.

35buildPkg :: Bool -> (Bool, FilePath) -> IO ()

36buildPkg warnonly (install, fp)

37 = do pkgdesc <- parseDesc fp

test/test039/FunErrTest.idr → test/test038/FunErrTest.idrrenamed

The content is the same.

test/test038/expected+4−29

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

1−True

1+FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

2−False

2+Could not prove that [] has at least two elements.

3−True

3+FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

4−False

4+Could not prove that tail [(fromInteger 1)] refl has at least two elements.

5−True

6−False

7−True

8−False

9−True

10−False

11−False

12−True

13−False

14−True

15−True

16−False

17−True

18−False

19−True

20−False

21−False

22−True

23−False

24−False

25−False

26−True

27−False

28−True

29−False

test/test038/run+2−4

@@ -1,5 +1,3 @@

1#!/usr/bin/env bash

2−idris $@ -o test038 test038.idr --nocolour

2+idris $@ FunErrTest.idr --nocolour --check

3−./test038

4−rm -f test038 *.ibc

3+rm -f *.ibc

5−

test/test039/expected+29−4

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

1−FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

1+True

2−Could not prove that [] has at least two elements.

2+False

3−FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

3+True

4−Could not prove that tail [(fromInteger 1)] refl has at least two elements.

4+False

5+True

6+False

7+True

8+False

9+True

10+False

11+False

12+True

13+False

14+True

15+True

16+False

17+True

18+False

19+True

20+False

21+False

22+True

23+False

24+False

25+False

26+True

27+False

28+True

29+False

test/test039/run+4−2

@@ -1,3 +1,5 @@

1#!/usr/bin/env bash

2−idris $@ FunErrTest.idr --nocolour --check

2+idris $@ -o test038 test038.idr --nocolour

3+./test038

3−rm -f *.ibc

4+rm -f test038 *.ibc

test/test038/test038.idr → test/test039/test038.idrrenamed

The content is the same.

test/test040/A.idrnew file+4

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

1+module A

3+num : Nat

4+num = 0

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

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

1+module B.C

3+num : Nat

4+num = 1

test/test040/Faulty.idrnew file+7

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

1+module Faulty

3+import A

4+import B.C

6+fault : num = Z

7+fault = refl

test/test040/Main.idrnew file+16

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

1+module Main

3+import A as X

4+import B.C as Y

6+checkX : X.num = Z

7+checkX = refl

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

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+rm -f *.ibc B/*.ibc