75c7597 · Idris-dev · git.iko.soy

idris.cabal+5

compare with master

unifiedsplit

@@ -313,6 +313,11 @@ Extra-source-files:

313 test/buffer001-disabled/run

314 test/buffer001-disabled/expected

315

316+ test/delab001/*.idr

317+ test/delab001/run

318+ test/delab001/expected

319+ test/delab001/input

320+

316 test/dsl001/run

321 test/dsl001/run

317 test/dsl001/*.idr

322 test/dsl001/*.idr

318 test/dsl001/expected

323 test/dsl001/expected

src/Idris/AbsSyntaxTree.hs+24−6

@@ -1364,12 +1364,28 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1364 else if null args

1365 then fp

1366 else fp <+> align (vsep (map (prettyArgS bnd) args))

1367− prettySe p bnd (PCase _ scr opts) =

1367+ prettySe p bnd (PCase _ scr cases) =

1368− kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody

1368+ align $ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <$>

1369+ indent 2 (vsep (map ppcase cases))

1369 where

1370 where

1370− prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1371+ ppcase (l, r) = nest nestingSize $

1372+ prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>

1373+ text "=>" <+>

1374+ prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r

1375+ -- Warning: this is a bit of a hack. At this stage, we don't have the

1376+ -- global context, so we can't determine which names are constructors,

1377+ -- which are types, and which are pattern variables on the LHS of the

1378+ -- case pattern. We use the heuristic that names without a namespace

1379+ -- are patvars, because right now case blocks in PTerms are always

1380+ -- delaborated from TT before being sent to the pretty-printer. If they

1381+ -- start getting printed directly, THIS WILL BREAK.

1382+ -- Potential solution: add a list of known patvars to the cases in

1383+ -- PCase, and have the delaborator fill it out, kind of like the pun

1384+ -- disambiguation on PDPair.

1385+ vars tm = filter noNS (allNamesIn tm)

1386+ noNS (NS _ _) = False

1387+ noNS _ = True

1371

1388

1372− sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1373 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1389 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1374 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1390 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1375 prettySe p bnd (PResolveTC _) = text "resolvetc"

1391 prettySe p bnd (PResolveTC _) = text "resolvetc"

@@ -1538,13 +1554,15 @@ prettyName

1538 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit

1554 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit

1539 -> Name -- ^^ the name to pprint

1555 -> Name -- ^^ the name to pprint

1540 -> Doc OutputAnnotation

1556 -> Doc OutputAnnotation

1541−prettyName infixParen showNS bnd n

1557+prettyName infixParen showNS bnd n

1558+ | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

1559+ | (UN n') <- n, isPrefixOf "_" $ T.unpack n' = text "_"

1542 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

1560 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

1543 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

1561 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

1544 where fullName = text nameSpace <> parenthesise (text (baseName n))

1562 where fullName = text nameSpace <> parenthesise (text (baseName n))

1545 baseName (UN n) = T.unpack n

1563 baseName (UN n) = T.unpack n

1546 baseName (NS n ns) = baseName n

1564 baseName (NS n ns) = baseName n

1547− baseName (MN i s) = T.unpack s

1565+ baseName (MN i s) = T.unpack s

1548 baseName other = show other

1566 baseName other = show other

1549 nameSpace = case n of

1567 nameSpace = case n of

1550 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

1568 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""

src/Idris/Delaborate.hs+30−2

@@ -70,8 +70,13 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

70 (de ((n,n):env) is sc)

71 de env [] (Bind n (Pi ty _) sc)

72 = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

73+

73− de env _ (Bind n (Let ty val) sc)

74+ de env imps (Bind n (Let ty val) sc)

75+ | isCaseApp sc

76+ , (P _ cOp _, args) <- unApply sc

77+ , Just caseblock <- delabCase env imps n val cOp args = caseblock

78+ | otherwise =

74− = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

79+ PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

75 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

80 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

76 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

81 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

77 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

82 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

@@ -128,6 +133,29 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

128 imp (PConstraint p l n _) arg = PConstraint p l n arg

133 imp (PConstraint p l n _) arg = PConstraint p l n arg

129 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

134 imp (PTacImplicit p l n sc _) arg = PTacImplicit p l n sc arg

130

135

136+ isCaseApp tm | P _ n _ <- fst (unApply tm) = isCN n

137+ | otherwise = False

138+ where isCN (NS n _) = isCN n

139+ isCN (SN (CaseN _)) = True

140+ isCN _ = False

141+

142+ delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm

143+ delabCase env imps scvar scrutinee caseName caseArgs =

144+ do cases <- case lookupCtxt caseName (idris_patdefs ist) of

145+ [(cases, _)] -> return cases

146+ _ -> Nothing

147+ return $ PCase un (de env imps scrutinee)

148+ [ (de (env ++ map (\n -> (n, n)) vars) imps (splitArg lhs),

149+ de (env ++ map (\n -> (n, n)) vars) imps rhs)

150+ | (vars, lhs, rhs) <- cases

151+ ]

152+ where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

153+ | otherwise = tm

154+ nonVar [] = error "Tried to delaborate empty case list"

155+ nonVar [x] = x

156+ nonVar (x@(App _ _) : _) = x

157+ nonVar (x@(P (DCon _ _ _) _ _) : _) = x

158+ nonVar (x:xs) = nonVar xs

131-- | How far to indent sub-errors

159-- | How far to indent sub-errors

132errorIndent :: Int

160errorIndent :: Int

133errorIndent = 8

161errorIndent = 8

test/delab001/delab001.idrnew file+16

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

1+module Case

2+

3+foo : Nat -> String

4+foo n = case n of

5+ Z => "z"

6+ S _ => "s"

7+

8+bar : Nat -> String -> String

9+bar x y = case x of

10+ Z => y

11+ S _ => y ++ y

12+

13+append : List a -> List a -> List a

14+append xs ys = case xs of

15+ Nil => ys

16+ (x :: xs) => x :: append xs ys

test/delab001/expectednew file+14

@@ -0,0 +1,14 @@

1+Type checking ./delab001.idr

2+*delab001> [?1049h[1;37r(B[m[4l[?7h[H[2J[37;1H[?1049l [?1l>foo : Nat -> String

3+foo n = case n of

4+ 0 => "z"

5+ S _ => "s"

6+*delab001> [?1049h[1;37r(B[m[4l[?7h[H[2J[37;1H[?1049l [?1l>bar : Nat -> String -> String

7+bar x y = case x of

8+ 0 => y

9+ S _ => (y ++ y)

10+*delab001> [?1049h[1;37r(B[m[4l[?7h[H[2J[37;1H[?1049l [?1l>append : List a -> List a -> List a

11+append xs ys = case xs of

12+ [] => ys

13+ (x :: xs) => (x :: (append xs ys))

14+*delab001> Bye bye

test/delab001/inputnew file+3

@@ -0,0 +1,3 @@

1+:printdef foo

2+:printdef bar

3+:printdef append

test/delab001/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --quiet --nocolor delab001.idr < input

3+rm -f *.ibc