7d38943 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Proper and complete parenthasization of infix operator names.

7d38943bmsherman12 years ago

src/Idris/AbsSyntaxTree.hs+35−31

compare with master

unifiedsplit

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

1185 prettySe p bnd e

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

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

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

1188+ prettySe p bnd (PRef fc n) = prettyNamePossParen True (ppopt_impl ppo) bnd n

1189 prettySe p bnd (PLam n ty sc) =

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

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

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

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

1230 | UN nm <- basename f

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

1232− if isAlpha (thead nm)

1232+ prettyNamePossParen True (ppopt_impl ppo) bnd f

1233− then prettyName (ppopt_impl ppo) bnd f

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

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

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

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

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

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

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

1238 | UN nm <- basename op

1236 | UN nm <- basename op

1239 , not (tnull nm) &&

1237 , not (tnull nm) &&

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

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

1241 case getExps args of

1239 case getExps args of

1242− [] -> enclose lparen rparen opName

1240+ [] -> opName True

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

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

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

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

1245 in bracket p precedence $ inFix l r

1243 in bracket p precedence $ inFix l r

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

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

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

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

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

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

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

1247+ where opName isPrefix = prettyNamePossParen isPrefix (ppopt_impl ppo) bnd op

1250 f = getFixity (opStr op)

1248 f = getFixity (opStr op)

1251 left l = case f of

1249 left l = case f of

1252 Nothing -> prettySe (-1) bnd l

1250 Nothing -> prettySe (-1) bnd l

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

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

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

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

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

1259 inFix l r = align . group $

1257 inFix l r = align . group $

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

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

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

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

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

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

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

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

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

1424

1422

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

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

1426prettyDocumentedIst ist (name, ty, docs) =

1424prettyDocumentedIst ist (name, ty, docs) =

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

1425+ prettyNamePossParen True True [] name <+> colon <+> align (prettyIst ist ty) <$>

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

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

1429

1427

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

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

@@ -1434,26 +1432,32 @@ bindingOf :: Name -- ^^ the bound name

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

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

1435

1433

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

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

1435+prettyNamePossParen

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

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

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

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

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

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

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

1440− -> Doc OutputAnnotation

1440+ -> Doc OutputAnnotation

1441+prettyNamePossParen infixParen showNS bnd n

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

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

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

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

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

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

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

1446+ baseName (NS n ns) = baseName n

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

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

1449+ baseName other = show other

1450+ nameSpace = case n of

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

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

1445− | otherwise = strName n

1452+ _ -> ""

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

1453+ isInfix = case baseName n of

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

1454+ "" -> False

1448− strName other = show other

1449−

1450−prettyNamePossParen :: Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation

1451−prettyNamePossParen showNS bnd n = parenthasize (prettyName showNS bnd n) where

1452− UN basename = case n of

1453− NS n' _ -> n'

1454− _ -> n

1455− isInfix = not (isAlpha (thead basename))

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

1456− parenthasize = if isInfix then enclose lparen rparen else id

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

1457+

1458+

1459+prettyName :: Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation

1460+prettyName = prettyNamePossParen False

1457

1461

1458

1462

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

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

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

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

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

1475showDImp ppo (PDatadecl n ty cons)

1479showDImp ppo (PDatadecl n ty cons)

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

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

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

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

1478

1482

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

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

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

1484showDecls 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 (prettyNamePossParen 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" <+> prettyNamePossParen 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) -> prettyNamePossParen 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 (prettyNamePossParen True False params' . fst) params))

136

137getDocs :: Name -> Idris Docs

138getDocs n

src/Idris/Output.hs+1−1

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

74 let infixes = idris_infixes ist

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

76 ihRenderResult h output

77− where fullName n = prettyNamePossParen True bnd n

77+ where fullName n = prettyNamePossParen True True bnd n

78 ppOverload ppo infixes n tm =

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

src/Idris/Prover.hs+1−1

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

101

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

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

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

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

105 iputGoal rendered

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

107 let OK ty = goalAtFocus ps

src/Idris/REPL.hs+6−6

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

367 where pn ist = displaySpans .

368 renderPretty 0.9 1000 .

369 fmap (fancifyAnnots ist) .

370− prettyName True []

370+ prettyNamePossParen True True []

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

372 case splitName n of

373 Left err -> iPrintError err

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

379 where pn ist = displaySpans .

380 renderPretty 0.9 1000 .

381 fmap (fancifyAnnots ist) .

382− prettyName True []

382+ prettyNamePossParen True True []

383

384splitName :: String -> Either String Name

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

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

928 ist <- getIState

929 ihRenderResult h . vsep $

930 map (\(n, ns) ->

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

931+ text "Callers of" <+> prettyNamePossParen True True [] n <$>

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

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

933 calls

934

935process h fn (CallsWho n) =

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

937 ist <- getIState

938 ihRenderResult h . vsep $

939 map (\(n, ns) ->

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

940+ prettyNamePossParen True True [] n <+> text "calls:" <$>

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

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

942 calls

943-- IdrisDoc

944process h fn (MakeDoc s) =