43da4b1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1758 from david-christiansen/feature/case-delab

Improve delaboration and pretty-printing for "case"

commit43da4b1d780a98838dd3884f45cfd815cdb074d8 authorDavid Christiansen <david@davidchristiansen.dk> dateSun 30 Nov 2014, 14:59 (12 years ago) parent9d3ce13 8ff9748

8 files changed+95−24

compare with master

unifiedsplit

idris.cabal+5 src/Idris/AbsSyntaxTree.hs+24−6 src/Idris/Delaborate.hs+30−2 src/Idris/ElabTerm.hs−16 test/delab001/delab001.idr+16 test/delab001/expected+13 test/delab001/input+4 test/delab001/run+3

idris.cabal+5

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

313313 test/buffer001-disabled/run

314314 test/buffer001-disabled/expected

315315

316+ test/delab001/*.idr

317+ test/delab001/run

318+ test/delab001/expected

319+ test/delab001/input

320+

316321 test/dsl001/run

317322 test/dsl001/*.idr

318323 test/dsl001/expected

src/Idris/AbsSyntaxTree.hs+24−6

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

13641364 else if null args

13651365 then fp

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

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

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

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

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

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

13691370 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

13711388

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

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

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

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

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

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

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

15401556 -> 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 "_"

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

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

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

15451563 baseName (UN n) = T.unpack n

15461564 baseName (NS n ns) = baseName n

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

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

15481566 baseName other = show other

15491567 nameSpace = case n of

15501568 (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

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

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

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

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

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

73+

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 =

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

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

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

7782 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

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

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

130135

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

131159-- | How far to indent sub-errors

132160errorIndent :: Int

133161errorIndent = 8

src/Idris/ElabTerm.hs−16

@@ -763,22 +763,6 @@ elab ist info emode opts fn tm

763763 = n `elem` ns

764764 || any (\x -> x `elem` ns) (allTTNames (binderTy b))

765765

766− -- FIXME: This probably doesn't help us here, but leaving

767− -- it in temporarily... if this comment is still here in master,

768− -- please delete the code!

769− chaseDeps env acc [] = filter (\(n, _) -> n `elem` acc) env

770− chaseDeps env acc ((n,b) : args)

771− = let ns = allTTNames (binderTy b) in

772− extendAcc ns acc args

773− where

774− extendAcc [] acc args = chaseDeps env acc args

775− extendAcc (n:ns) acc args

776− | elem n acc = extendAcc ns acc args

777− | otherwise = case lookup n env of

778− Just b -> extendAcc ns (n : acc)

779− ((n,b) : args)

780− Nothing -> extendAcc ns acc args

781−

782766 elab' ina fc (PUnifyLog t) = do unifyLog True

783767 elab' ina fc t

784768 unifyLog False

test/delab001/delab001.idrnew file+16

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

1+module Case

3+foo : Nat -> String

4+foo n = case n of

5+ Z => "z"

6+ S _ => "s"

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

@@ -0,0 +1,13 @@

1+Type checking ./delab001.idr

2+foo : Nat -> String

3+foo n = case n of

4+ 0 => "z"

5+ S _ => "s"

6+bar : Nat -> String -> String

7+bar x y = case x of

8+ 0 => y

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

10+append : List a -> List a -> List a

11+append xs ys = case xs of

12+ [] => ys

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

test/delab001/inputnew file+4

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

1+:consolewidth infinite

2+:printdef foo

3+:printdef bar

4+: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