4abeeeb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1598 from jfdm/tidyup/lift-todos-2

4abeeebEdwin Brady12 years ago

src/IRTS/DumpBC.hs+1−1

compare with master

unifiedsplit

@@ -65,7 +65,7 @@ serializeBC n bc = indent n ++

65 "OP " ++ serializeReg a ++ " " ++ show b ++ " [" ++ interMap c ", " serializeReg ++ "]"

66 NULL r -> "NULL " ++ serializeReg r

67 ERROR s -> "ERROR \"" ++ s ++ "\"" -- FIXME: s may contain quotes

68−

68+ -- Issue #1596

69serialize :: [(Name, [BC])] -> String

70serialize decls =

71 interMap decls "\n\n" serializeDecl

src/Idris/Chaser.hs+5−1

@@ -70,7 +70,7 @@ getIModTime (LIDR i) = getModificationTime i

71buildTree :: [FilePath] -> -- already guaranteed built

72 FilePath -> Idris [ModuleTree]

73−buildTree built fp = btree [] fp

73+buildTree built fp = btree [] fp

74-- = idrisCatch (btree [] fp)

75-- (\e -> do now <- runIO $ getCurrentTime

76-- iputStrLn (show e)

@@ -114,6 +114,10 @@ buildTree built fp = btree [] fp

114

115 -- FIXME: It's also not up to date if anything it imports has

116 -- been modified since its own ibc has.

117+ --

118+ -- Issue #1592 on the issue tracker.

119+ --

120+ -- https://github.com/idris-lang/Idris-dev/issues/1592

117

121

118 checkIBCUpToDate fn (LIDR src) = older fn src

122 checkIBCUpToDate fn (LIDR src) = older fn src

119 checkIBCUpToDate fn (IDR src) = older fn src

123 checkIBCUpToDate fn (IDR src) = older fn src

src/Idris/DataOpts.hs+1−1

@@ -97,6 +97,7 @@ applyDataOptRT n tag arity uniq args

98 -- Nat special cases

99 -- TODO: Would be nice if this was configurable in idris source!

100+ -- Issue #1597 https://github.com/idris-lang/Idris-dev/issues/1597

100 doOpts (NS (UN z) [nat, prelude]) []

101 doOpts (NS (UN z) [nat, prelude]) []

101 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"

102 | z == txt "Z" && nat == txt "Nat" && prelude == txt "Prelude"

102 = Constant (BI 0)

103 = Constant (BI 0)

@@ -105,4 +106,3 @@ applyDataOptRT n tag arity uniq args

105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106

107

107 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

108 doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

108−

src/Idris/Delaborate.hs+39−29

@@ -104,10 +104,10 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

104 (de env [] l) (de env [] r)

105 | n == sUN "Sg_intro" = PDPair un IsTerm (de env [] l) Placeholder

106 (de env [] r)

107− deFn env f@(P _ n _) args

107+ deFn env f@(P _ n _) args

108− | n `elem` map snd env

108+ | n `elem` map snd env

109 = PApp un (de env [] f) (map pexp (map (de env []) args))

110− deFn env (P _ n _) args

110+ deFn env (P _ n _) args

111 | not mvs = case lookup n (idris_metavars ist) of

112 Just (Just _, mi, _) ->

113 mkMVApp n (drop mi (map (de env []) args))

@@ -170,10 +170,10 @@ pprintErr' i (InternalMsg s) =

170pprintErr' i (CantUnify _ x_in y_in e sc s) =

171 let (x_ns, y_ns, nms) = renameMNs x_in y_in

172 (x, y) = addImplicitDiffs (delab i x_ns) (delab i y_ns) in

173− text "Can't unify" <> indented (annTm x_ns

173+ text "Can't unify" <> indented (annTm x_ns

174 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

175 ++ zip nms (repeat False)) x)) <$>

176− text "with" <> indented (annTm y_ns

176+ text "with" <> indented (annTm y_ns

177 (pprintTerm' i (map (\ (n, b) -> (n, False)) sc

178 ++ zip nms (repeat False)) y)) <>

179 case e of

@@ -183,10 +183,10 @@ pprintErr' i (CantUnify _ x_in y_in e sc s) =

183 if (opt_errContext (idris_options i)) then showSc i sc else empty

184pprintErr' i (CantConvert x y env) =

185 text "Can't convert" <>

186− indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

186+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

187 (delab i (flagUnique x)))) <$>

188 text "with" <>

189− indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

189+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env)

190 (delab i (flagUnique y)))) <>

191 if (opt_errContext (idris_options i)) then line <> showSc i env else empty

192 where flagUnique (Bind n (Pi t k@(UType u)) sc)

@@ -232,7 +232,7 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

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

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

234pprintErr' i UniverseError = text "Universe inconsistency"

235−pprintErr' i (UniqueError NullType n)

235+pprintErr' i (UniqueError NullType n)

236 = text "Borrowed name" <+> annName' n (showbasic n)

237 <+> text "must not be used on RHS"

238pprintErr' i (UniqueError _ n) = text "Unique name" <+> annName' n (showbasic n)

@@ -255,7 +255,8 @@ pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>

255pprintErr' i (ElaboratingArg f x _ e)

256 | isUN x =

257 text "When elaborating argument" <+>

258− annotate (AnnBoundName x False) (text (showbasic x)) <+> --TODO check plicity

258+ annotate (AnnBoundName x False) (text (showbasic x)) <+> -- TODO check plicity

259+ -- Issue #1591 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1591

259 text "to" <+> whatIsName <> annName f <> colon <>

260 text "to" <+> whatIsName <> annName f <> colon <>

260 indented (pprintErr' i e)

261 indented (pprintErr' i e)

261 | otherwise =

262 | otherwise =

@@ -289,7 +290,11 @@ pprintErr' i (ReflectionFailed msg err) =

289

290

290-- Make sure the machine invented names are shown helpfully to the user, so

291-- Make sure the machine invented names are shown helpfully to the user, so

291-- that any names which differ internally also differ visibly

292-- that any names which differ internally also differ visibly

293+

292-- FIXME: I can't actually contrive an error to test this! Will revisit later...

294-- FIXME: I can't actually contrive an error to test this! Will revisit later...

295+--

296+-- Issue #1590 in the Issue tracker.

297+-- https://github.com/idris-lang/Idris-dev/issues/1590

293renameMNs :: Term -> Term -> (Term, Term, [Name])

298renameMNs :: Term -> Term -> (Term, Term, [Name])

294renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

299renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

295 newnames = evalState (getRenames [] ns) 1 in

300 newnames = evalState (getRenames [] ns) 1 in

@@ -307,7 +312,7 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

307 rename :: [(Name, Name)] -> Term -> Term

312 rename :: [(Name, Name)] -> Term -> Term

308 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

313 rename ns (P nt x t) | Just x' <- lookup x ns = P nt x' t

309 rename ns (App f a) = App (rename ns f) (rename ns a)

314 rename ns (App f a) = App (rename ns f) (rename ns a)

310− rename ns (Bind x b sc)

315+ rename ns (Bind x b sc)

311 = let b' = fmap (rename ns) b

316 = let b' = fmap (rename ns) b

312 sc' = rename ns sc in

317 sc' = rename ns sc in

313 case lookup x ns of

318 case lookup x ns of

@@ -318,15 +323,15 @@ renameMNs x y = let ns = nub $ allTTNames x ++ allTTNames y

318-- If the two terms only differ in their implicits, mark the implicits which

323-- If the two terms only differ in their implicits, mark the implicits which

319-- differ as AlwaysShow so that they appear in errors

324-- differ as AlwaysShow so that they appear in errors

320addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

325addImplicitDiffs :: PTerm -> PTerm -> (PTerm, PTerm)

321−addImplicitDiffs x y

326+addImplicitDiffs x y

322 = if (x `expLike` y) then addI x y else (x, y)

327 = if (x `expLike` y) then addI x y else (x, y)

323 where

328 where

324 addI :: PTerm -> PTerm -> (PTerm, PTerm)

329 addI :: PTerm -> PTerm -> (PTerm, PTerm)

325− addI (PApp fc f as) (PApp gc g bs)

330+ addI (PApp fc f as) (PApp gc g bs)

326 = let (as', bs') = addShows as bs in

331 = let (as', bs') = addShows as bs in

327 (PApp fc f as', PApp gc g bs')

332 (PApp fc f as', PApp gc g bs')

328 where addShows [] [] = ([], [])

333 where addShows [] [] = ([], [])

329− addShows (a:as) (b:bs)

334+ addShows (a:as) (b:bs)

330 = let (as', bs') = addShows as bs

335 = let (as', bs') = addShows as bs

331 (a', b') = addI (getTm a) (getTm b) in

336 (a', b') = addI (getTm a) (getTm b) in

332 if (not (a' `expLike` b'))

337 if (not (a' `expLike` b'))

@@ -334,20 +339,20 @@ addImplicitDiffs x y

334 getTm = a' } : as',

339 getTm = a' } : as',

335 b { argopts = AlwaysShow : argopts b,

340 b { argopts = AlwaysShow : argopts b,

336 getTm = b' } : bs')

341 getTm = b' } : bs')

337− else (a { getTm = a' } : as',

342+ else (a { getTm = a' } : as',

338 b { getTm = b' } : bs')

343 b { getTm = b' } : bs')

339− addI (PLam n a b) (PLam n' c d)

344+ addI (PLam n a b) (PLam n' c d)

340 = let (a', c') = addI a c

345 = let (a', c') = addI a c

341 (b', d') = addI b d in

346 (b', d') = addI b d in

342 (PLam n a' b', PLam n' c' d')

347 (PLam n a' b', PLam n' c' d')

343− addI (PPi p n a b) (PPi p' n' c d)

348+ addI (PPi p n a b) (PPi p' n' c d)

344 = let (a', c') = addI a c

349 = let (a', c') = addI a c

345 (b', d') = addI b d in

350 (b', d') = addI b d in

346 (PPi p n a' b', PPi p' n' c' d')

351 (PPi p n a' b', PPi p' n' c' d')

347− addI (PRefl fc a) (PRefl fc' b)

352+ addI (PRefl fc a) (PRefl fc' b)

348 = let (a', b') = addI a b in

353 = let (a', b') = addI a b in

349 (PRefl fc a', PRefl fc' b')

354 (PRefl fc a', PRefl fc' b')

350− addI (PEq fc at bt a b) (PEq fc' ct dt c d)

355+ addI (PEq fc at bt a b) (PEq fc' ct dt c d)

351 | trace (show (at,bt)) False = undefined

356 | trace (show (at,bt)) False = undefined

352 | at `expLike` ct && bt `expLike` dt

357 | at `expLike` ct && bt `expLike` dt

353 = let (a', c') = addI a c

358 = let (a', c') = addI a c

@@ -357,8 +362,8 @@ addImplicitDiffs x y

357 = let (at', ct') = addI at ct

362 = let (at', ct') = addI at ct

358 (bt', dt') = addI bt dt

363 (bt', dt') = addI bt dt

359 (a', c') = addI a c

364 (a', c') = addI a c

360− (b', d') = addI b d

365+ (b', d') = addI b d

361− showa = if at `expLike` ct then [] else [AlwaysShow]

366+ showa = if at `expLike` ct then [] else [AlwaysShow]

362 showb = if bt `expLike` dt then [] else [AlwaysShow] in

367 showb = if bt `expLike` dt then [] else [AlwaysShow] in

363 (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

368 (PApp fc (PRef fc eqTy) [(pimp (sUN "A") at' True)

364 { argopts = showa },

369 { argopts = showa },

@@ -370,12 +375,12 @@ addImplicitDiffs x y

370 (pimp (sUN "B") dt' True)

375 (pimp (sUN "B") dt' True)

371 { argopts = showb },

376 { argopts = showb },

372 pexp c', pexp d'])

377 pexp c', pexp d'])

373−

378+

374− addI (PPair fc pi a b) (PPair fc' pi' c d)

379+ addI (PPair fc pi a b) (PPair fc' pi' c d)

375 = let (a', c') = addI a c

380 = let (a', c') = addI a c

376 (b', d') = addI b d in

381 (b', d') = addI b d in

377 (PPair fc pi a' b', PPair fc' pi' c' d')

382 (PPair fc pi a' b', PPair fc' pi' c' d')

378− addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)

383+ addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)

379 = let (a', c') = addI a c

384 = let (a', c') = addI a c

380 (t', u') = addI t u

385 (t', u') = addI t u

381 (b', d') = addI b d in

386 (b', d') = addI b d in

@@ -387,19 +392,24 @@ addImplicitDiffs x y

387 expLike (PApp _ f as) (PApp _ f' as')

392 expLike (PApp _ f as) (PApp _ f' as')

388 = expLike f f' && length as == length as' &&

393 = expLike f f' && length as == length as' &&

389 and (zipWith expLike (getExps as) (getExps as'))

394 and (zipWith expLike (getExps as) (getExps as'))

390− expLike (PPi _ n s t) (PPi _ n' s' t')

395+ expLike (PPi _ n s t) (PPi _ n' s' t')

391 = n == n' && expLike s s' && expLike t t'

396 = n == n' && expLike s s' && expLike t t'

392− expLike (PLam n s t) (PLam n' s' t')

397+ expLike (PLam n s t) (PLam n' s' t')

393 = n == n' && expLike s s' && expLike t t'

398 = n == n' && expLike s s' && expLike t t'

394 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

399 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

395 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

400 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

396− expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

401+ expLike (PEq _ xt yt x y) (PEq _ xt' yt' x' y')

397 = expLike x x' && expLike y y'

402 = expLike x x' && expLike y y'

398 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

403 expLike (PRefl _ x) (PRefl _ x') = expLike x x'

399 expLike x y = x == y

404 expLike x y = x == y

400

405

406+-- Issue #1589 on the issue tracker

407+-- https://github.com/idris-lang/Idris-dev/issues/1589

408+--

409+-- Figure out why MNs are getting rewritte to UNs for top-level

410+-- pattern-matching functions

401isUN :: Name -> Bool

411isUN :: Name -> Bool

402−isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO figure out why MNs are getting rewritte to UNs for top-level pattern-matching functions

412+isUN (UN n) = not $ T.isPrefixOf (T.pack "__") n -- TODO

403isUN (NS n _) = isUN n

413isUN (NS n _) = isUN n

404isUN _ = False

414isUN _ = False

405

415

@@ -428,6 +438,8 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

428 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

438 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

429 let o = overview (fst docs)

439 let o = overview (fst docs)

430 -- TODO make width configurable

440 -- TODO make width configurable

441+ -- Issue #1588 on the Issue Tracker

442+ -- https://github.com/idris-lang/Idris-dev/issues/1588

431 out = displayS . renderPretty 1.0 50 $

443 out = displayS . renderPretty 1.0 50 $

432 renderDocstring (pprintDelab ist) o

444 renderDocstring (pprintDelab ist) o

433 return (out "")

445 return (out "")

@@ -460,5 +472,3 @@ showbasic n@(UN _) = show n

460showbasic (MN _ s) = str s

472showbasic (MN _ s) = str s

461showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

473showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

462showbasic (SN s) = show s

474showbasic (SN s) = show s

463−

464−

src/Idris/ParseData.hs+6−5

@@ -178,8 +178,6 @@ constructor syn

178 cn_in <- fnName; fc <- getFC

179 let cn = expandNS syn cn_in

180 lchar ':'

181− -- FIXME: 'forcenames' is an almighty hack! Need a better way of

182− -- erasing non-forceable things

183 fs <- option [] (do lchar '%'; reserved "erase"

181 fs <- option [] (do lchar '%'; reserved "erase"

184 sepBy1 name (lchar ','))

182 sepBy1 name (lchar ','))

185 ty <- typeExpr (allowImp syn)

183 ty <- typeExpr (allowImp syn)

@@ -206,7 +204,7 @@ simpleConstructor syn

206 return (doc', [], cn, args, fc, [])

204 return (doc', [], cn, args, fc, [])

207 <?> "constructor"

205 <?> "constructor"

208

206

209−{- | Parses a dsl block declaration

207+{- | Parses a dsl block declaration

210DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

208DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

211 -}

209 -}

212dsl :: SyntaxInfo -> IdrisParser PDecl

210dsl :: SyntaxInfo -> IdrisParser PDecl

@@ -235,6 +233,11 @@ dsl syn = do reserved "dsl"

235

233

236{- | Checks DSL for errors -}

234{- | Checks DSL for errors -}

237-- FIXME: currently does nothing, check if DSL is really sane

235-- FIXME: currently does nothing, check if DSL is really sane

236+--

237+-- Issue #1595 on the Issue Tracker

238+--

239+-- https://github.com/idris-lang/Idris-dev/issues/1595

240+--

238checkDSL :: DSL -> IdrisParser ()

241checkDSL :: DSL -> IdrisParser ()

239checkDSL dsl = return ()

242checkDSL dsl = return ()

240

243

@@ -253,5 +256,3 @@ overload syn = do o <- identifier <|> do reserved "let"

253 return (o, t)

256 return (o, t)

254 <?> "dsl overload declaratioN"

257 <?> "dsl overload declaratioN"

255 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]

258 where overloadable = ["let","lambda","pi","index_first","index_next","variable"]

256−

257−

src/Idris/ParseHelpers.hs+4−2

@@ -51,6 +51,7 @@ instance TokenParsing IdrisParser where

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

52 token p = do s <- get

53 (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

54+ -- See Issue #1594

54 r <- p

55 r <- p

55 (FC fn _ (el, ec)) <- getFC

56 (FC fn _ (el, ec)) <- getFC

56 whiteSpace

57 whiteSpace

@@ -316,7 +317,7 @@ operatorLetter = oneOf opChars

316-- | Parses an operator

317-- | Parses an operator

317operator :: MonadicParsing m => m String

318operator :: MonadicParsing m => m String

318operator = do op <- token . some $ operatorLetter

319operator = do op <- token . some $ operatorLetter

319− when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

320+ when (op `elem` [":", "=>", "->", "<-", "=", "?=", "|"]) $

320 fail $ op ++ " is not a valid operator"

321 fail $ op ++ " is not a valid operator"

321 return op

322 return op

322

323

@@ -343,6 +344,8 @@ getFC = do s <- position

343 let (dir, file) = splitFileName (fileName s)

344 let (dir, file) = splitFileName (fileName s)

344 let f = if dir == addTrailingPathSeparator "." then file else fileName s

345 let f = if dir == addTrailingPathSeparator "." then file else fileName s

345 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

346 return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

347+ -- Issue #1594 on the Issue Tracker.

348+ -- https://github.com/idris-lang/Idris-dev/issues/1594

346

349

347{-* Syntax helpers-}

350{-* Syntax helpers-}

348-- | Bind constraints to term

351-- | Bind constraints to term

@@ -574,4 +577,3 @@ collect (PInstance f s cs n ps t en ds : ds')

574 = PInstance f s cs n ps t en (collect ds) : collect ds'

577 = PInstance f s cs n ps t en (collect ds) : collect ds'

575collect (d : ds) = d : collect ds

578collect (d : ds) = d : collect ds

576collect [] = []

579collect [] = []

577−

src/Idris/Unlit.hs+4−2

@@ -23,9 +23,11 @@ check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

23check f l [x] = return ()

24check f l [] = return ()

26+-- Issue #1593 on the issue checker.

27+--

28+-- https://github.com/idris-lang/Idris-dev/issues/1593

29+--

26chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

30chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

27chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

31chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

28chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

32chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

29chkAdj f l _ _ = return ()

33chkAdj f l _ _ = return ()

30−

31−