22b2548 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1323 from bmsherman/parenthasizeInfix

Parenthasize infix names in REPL output

commit22b2548df26e10d2cebad8bab6b9cae3f9ecc0a3 authorDavid Christiansen <david@davidchristiansen.dk> dateSat 21 Jun 2014, 21:29 (12 years ago) parentfc6f5fe c4eca4f

5 files changed+45−36

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+31−23 src/Idris/Docs.hs+4−4 src/Idris/Output.hs+2−1 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+7−7

src/Idris/AbsSyntaxTree.hs+31−23

@@ -1197,7 +1197,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

11971197 prettySe p bnd e

11981198 | Just str <- slist p bnd e = str

11991199 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1200− prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

1200+ prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

12011201 prettySe p bnd (PLam n ty sc) =

12021202 bracket p 2 . group . align . hang 2 $

12031203 text "\\" <> bindingOf n False <+> text "=>" <$>

@@ -1241,24 +1241,22 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12411241 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

12421242 | UN nm <- basename f

12431243 , not (ppopt_impl ppo) && null (getExps args) =

1244− if isAlpha (thead nm)

1245− then prettyName (ppopt_impl ppo) bnd f

1246− else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

1244+ prettyName True (ppopt_impl ppo) bnd f

12471245 prettySe p bnd (PAppBind _ (PRef _ f) [])

1248− | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f

1246+ | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

12491247 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators

12501248 | UN nm <- basename op

12511249 , not (tnull nm) &&

12521250 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

12531251 case getExps args of

1254− [] -> enclose lparen rparen opName

1255− [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1252+ [] -> opName True

1253+ [x] -> group (opName True <$> group (prettySe 0 bnd x))

12561254 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

12571255 in bracket p precedence $ inFix l r

12581256 (l:r:rest) -> bracket p 1 $

12591257 enclose lparen rparen (inFix l r) <+>

12601258 align (group (vsep (map (prettyArgSe bnd) rest)))

1261− where opName = prettyName (ppopt_impl ppo) bnd op

1259+ where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

12621260 f = getFixity (opStr op)

12631261 left l = case f of

12641262 Nothing -> prettySe (-1) bnd l

@@ -1269,7 +1267,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12691267 Just (Infixr p') -> prettySe p' bnd r

12701268 Just f' -> prettySe (prec f'-1) bnd r

12711269 inFix l r = align . group $

1272− (left l <+> opName) <$> group (right r)

1270+ (left l <+> opName False) <$> group (right r)

12731271 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

12741272 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

12751273 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

@@ -1436,7 +1434,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

14361434

14371435prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation

14381436prettyDocumentedIst ist (name, ty, docs) =

1439− prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1437+ prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

14401438 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

14411439

14421440-- | Pretty-printer helper for the binding site of a name

@@ -1446,18 +1444,28 @@ bindingOf :: Name -- ^^ the bound name

14461444bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

14471445

14481446-- | Pretty-printer helper for names that attaches the correct annotations

1449−prettyName :: Bool -- ^^ whether to show namespaces

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

1451− -> Name -- ^^ the name to pprint

1452− -> Doc OutputAnnotation

1453−prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1454− | otherwise = annotate (AnnName n Nothing Nothing Nothing) (text (strName n))

1455− where strName (UN n) = T.unpack n

1456− strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1457− | otherwise = strName n

1458− strName n | n == falseTy = "_|_"

1459− strName (MN i s) = T.unpack s

1460− strName other = show other

1447+prettyName

1448+ :: Bool -- ^^ whether the name should be parenthasized if it is an infix operator

1449+ -> Bool -- ^^ whether to show namespaces

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

1451+ -> Name -- ^^ the name to pprint

1452+ -> Doc OutputAnnotation

1453+prettyName infixParen showNS bnd n

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

1455+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

1456+ where fullName = text nameSpace <> parenthasize (text (baseName n))

1457+ baseName (UN n) = T.unpack n

1458+ baseName (NS n ns) = baseName n

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

1460+ baseName n | n == falseTy = "_|_"

1461+ baseName other = show other

1462+ nameSpace = case n of

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

1464+ _ -> ""

1465+ isInfix = case baseName n of

1466+ "" -> False

1467+ (c : _) -> not (isAlpha c)

1468+ parenthasize = if isInfix && infixParen then enclose lparen rparen else id

14611469

14621470

14631471showCImp :: PPOption -> PClause -> Doc OutputAnnotation

@@ -1478,7 +1486,7 @@ showCImp ppo (PWith _ n l ws r w)

14781486showDImp :: PPOption -> PData -> Doc OutputAnnotation

14791487showDImp ppo (PDatadecl n ty cons)

14801488 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1481− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))

1489+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))

14821490

14831491showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

14841492showDecls o ds = vsep (map (showDeclImp o) ds)

src/Idris/Docs.hs+4−4

@@ -37,7 +37,7 @@ showDoc d | nullDocstring d = empty

3737

3838pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

3939pprintFD ist (FD n doc args ty f)

40− = nest 4 (prettyName (ppopt_impl ppo) [] n <+> colon <+>

40+ = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

4141 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

4242 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

4343 renderDocstring doc <$>

@@ -79,7 +79,7 @@ pprintDocs ist (DataDoc t args)

7979 else nest 4 (text "Constructors:" <> line <>

8080 vsep (map (pprintFD ist) args))

8181pprintDocs ist (ClassDoc n doc meths params instances superclasses)

82− = nest 4 (text "Type class" <+> prettyName (ppopt_impl ppo) [] n <>

82+ = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

8383 if nullDocstring doc then empty else line <> renderDocstring doc)

8484 <> line <$>

8585 nest 4 (text "Parameters:" <$> prettyParameters)

@@ -131,8 +131,8 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

131131 (subclasses, instances') = partition isSubclass instances

132132

133133 prettyParameters = if any (isJust . snd) params

134− then vsep (map (\(nm,md) -> prettyName False params' nm <+> maybe empty showDoc md) params)

135− else hsep (punctuate comma (map (prettyName False params' . fst) params))

134+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty showDoc md) params)

135+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))

136136

137137getDocs :: Name -> Idris Docs

138138getDocs n

src/Idris/Output.hs+2−1

@@ -15,6 +15,7 @@ import Debug.Trace

1515

1616import System.IO (stdout, Handle, hPutStrLn)

1717

18+import Data.Char (isAlpha)

1819import Data.List (nub)

1920import Data.Maybe (fromMaybe)

2021

@@ -73,7 +74,7 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState

7374 let infixes = idris_infixes ist

7475 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

7576 ihRenderResult h output

76− where fullName n = prettyName True bnd n

77+ where fullName n = prettyName True True bnd n

7778 ppOverload ppo infixes n tm =

7879 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

7980

src/Idris/Prover.hs+1−1

@@ -107,7 +107,7 @@ elabStep st e = case runStateT eCheck st of

107107

108108dumpState :: IState -> ProofState -> Idris ()

109109dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

110− do rendered <- iRender $ prettyName False [] nm <> colon <+> text "No more goals."

110+ do rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."

111111 iputGoal rendered

112112dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do

113113 let OK ty = goalAtFocus ps

src/Idris/REPL.hs+7−7

@@ -410,7 +410,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

410410 where pn ist = displaySpans .

411411 renderPretty 0.9 1000 .

412412 fmap (fancifyAnnots ist) .

413− prettyName True []

413+ prettyName True True []

414414runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

415415 case splitName n of

416416 Left err -> iPrintError err

@@ -422,7 +422,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

422422 where pn ist = displaySpans .

423423 renderPretty 0.9 1000 .

424424 fmap (fancifyAnnots ist) .

425− prettyName True []

425+ prettyName True True []

426+

426427runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

427428 do ctxt <- getContext

428429 ist <- getIState

@@ -457,7 +458,6 @@ ideSlaveForceTermImplicits id bnd impl tm =

457458 fmap (fancifyAnnots ist) $ expl)

458459 runIO . putStrLn $ IdeSlave.convSExp "return" msg id

459460

460−

461461splitName :: String -> Either String Name

462462splitName s = case reverse $ splitOn "." s of

463463 [] -> Left ("Didn't understand name '" ++ s ++ "'")

@@ -1005,8 +1005,8 @@ process h fn (WhoCalls n) =

10051005 ist <- getIState

10061006 ihRenderResult h . vsep $

10071007 map (\(n, ns) ->

1008− text "Callers of" <+> prettyName True [] n <$>

1009− indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))

1008+ text "Callers of" <+> prettyName True True [] n <$>

1009+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

10101010 calls

10111011

10121012process h fn (CallsWho n) =

@@ -1014,8 +1014,8 @@ process h fn (CallsWho n) =

10141014 ist <- getIState

10151015 ihRenderResult h . vsep $

10161016 map (\(n, ns) ->

1017− prettyName True [] n <+> text "calls:" <$>

1018− indent 1 (vsep (map ((text "*" <+>) . align . prettyName True []) ns)))

1017+ prettyName True True [] n <+> text "calls:" <$>

1018+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

10191019 calls

10201020-- IdrisDoc

10211021process h fn (MakeDoc s) =