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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1323 from bmsherman/parenthasizeInfix

22b2548David Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+31−23

compare with master

unifiedsplit

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

1197 prettySe p bnd e

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

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

1201 prettySe p bnd (PLam n ty sc) =

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

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

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

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

1242 | UN nm <- basename f

1243 , 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

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

1245 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

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

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

1250 | UN nm <- basename op

1248 | UN nm <- basename op

1251 , not (tnull nm) &&

1249 , not (tnull nm) &&

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

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

1253 case getExps args of

1251 case getExps args of

1254− [] -> enclose lparen rparen opName

1252+ [] -> opName True

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

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

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

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

1257 in bracket p precedence $ inFix l r

1255 in bracket p precedence $ inFix l r

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

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

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

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

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

1258 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

1262 f = getFixity (opStr op)

1260 f = getFixity (opStr op)

1263 left l = case f of

1261 left l = case f of

1264 Nothing -> prettySe (-1) bnd l

1262 Nothing -> prettySe (-1) bnd l

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

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

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

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

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

1271 inFix l r = align . group $

1269 inFix l r = align . group $

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

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

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

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

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

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

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

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

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

1436

1434

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

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

1438prettyDocumentedIst ist (name, ty, docs) =

1436prettyDocumentedIst ist (name, ty, docs) =

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

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

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

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

1441

1439

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

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

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

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

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

1447

1445

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

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

1447+prettyName

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

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

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

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

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

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

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

1452− -> Doc OutputAnnotation

1452+ -> Doc OutputAnnotation

1453+prettyName infixParen showNS bnd n

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

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

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

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

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

1455− where strName (UN n) = T.unpack 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

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

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

1457− | otherwise = strName n

1464+ _ -> ""

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

1465+ isInfix = case baseName n of

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

1466+ "" -> False

1460− strName other = show other

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

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

1461

1469

1462

1470

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

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

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

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

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

1479showDImp ppo (PDatadecl n ty cons)

1487showDImp ppo (PDatadecl n ty cons)

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

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

1482

1490

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

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

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

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

src/Idris/Docs.hs+4−4

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

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

39pprintFD 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 <+>

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

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

43 renderDocstring doc <$>

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

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

80 vsep (map (pprintFD ist) args))

81pprintDocs 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 <>

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

84 <> line <$>

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

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

131 (subclasses, instances') = partition isSubclass instances

132

133 prettyParameters = if any (isJust . snd) params

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

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

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

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

136

137getDocs :: Name -> Idris Docs

138getDocs n

src/Idris/Output.hs+2−1

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

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

18+import Data.Char (isAlpha)

18import Data.List (nub)

19import Data.List (nub)

19import Data.Maybe (fromMaybe)

20import Data.Maybe (fromMaybe)

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

73 let infixes = idris_infixes ist

74 let infixes = idris_infixes ist

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

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

75 ihRenderResult h output

76 ihRenderResult h output

76− where fullName n = prettyName True bnd n

77+ where fullName n = prettyName True True bnd n

77 ppOverload ppo infixes n tm =

78 ppOverload ppo infixes n tm =

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

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

src/Idris/Prover.hs+1−1

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

107

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

109dumpState 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."

111 iputGoal rendered

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

113 let OK ty = goalAtFocus ps

src/Idris/REPL.hs+7−7

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

410 where pn ist = displaySpans .

411 renderPretty 0.9 1000 .

412 fmap (fancifyAnnots ist) .

413− prettyName True []

413+ prettyName True True []

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

415 case splitName n of

416 Left err -> iPrintError err

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

422 where pn ist = displaySpans .

423 renderPretty 0.9 1000 .

424 fmap (fancifyAnnots ist) .

425− prettyName True []

425+ prettyName True True []

426+

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

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

427 do ctxt <- getContext

428 do ctxt <- getContext

428 ist <- getIState

429 ist <- getIState

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

457 fmap (fancifyAnnots ist) $ expl)

458 fmap (fancifyAnnots ist) $ expl)

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

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

459

460

460−

461splitName :: String -> Either String Name

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

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

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

1005 ist <- getIState

1006 ihRenderResult h . vsep $

1007 map (\(n, ns) ->

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

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

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

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

1010 calls

1011

1012process h fn (CallsWho n) =

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

1014 ist <- getIState

1015 ihRenderResult h . vsep $

1016 map (\(n, ns) ->

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

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

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

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

1019 calls

1020-- IdrisDoc

1021process h fn (MakeDoc s) =