034ea04 · Idris-dev · git.iko.soy

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

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

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)

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

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 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-- 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 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 = 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 (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 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 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 "")

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−