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

git.iko.soy/Idris-dev

Proper and complete parenthasization of infix operator names.

commit7d3894345b42bc0f875e0a89c8455ec03af319d2 authorbmsherman <bmsherman@users.noreply.github.com> dateSat 21 Jun 2014, 12:24 (12 years ago) parentc4ce749

5 files changed+47−43

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+35−31 src/Idris/Docs.hs+4−4 src/Idris/Output.hs+1−1 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+6−6

src/Idris/AbsSyntaxTree.hs+35−31

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

11851185 prettySe p bnd e

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

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

11891189 prettySe p bnd (PLam n ty sc) =

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

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

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

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

12301230 | UN nm <- basename f

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

1232− if isAlpha (thead nm)

1233− then prettyName (ppopt_impl ppo) bnd f

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

1232+ prettyNamePossParen True (ppopt_impl ppo) bnd f

12351233 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

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

12381236 | UN nm <- basename op

12391237 , not (tnull nm) &&

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

12411239 case getExps args of

1242− [] -> enclose lparen rparen opName

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

1240+ [] -> opName True

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

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

12451243 in bracket p precedence $ inFix l r

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

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

12481246 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

12501248 f = getFixity (opStr op)

12511249 left l = case f of

12521250 Nothing -> prettySe (-1) bnd l

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

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

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

12591257 inFix l r = align . group $

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

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

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

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

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

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

14241422

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

14261424prettyDocumentedIst ist (name, ty, docs) =

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

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

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

14291427

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

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

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

14351433

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

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

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

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

1440− -> Doc OutputAnnotation

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

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

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

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

1445− | otherwise = strName n

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

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

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

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

1435+prettyNamePossParen

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

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

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

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

1440+ -> Doc OutputAnnotation

1441+prettyNamePossParen infixParen showNS bnd n

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

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

1444+ where fullName = text nameSpace <> parenthasize (text (baseName 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

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

1452+ _ -> ""

1453+ isInfix = case baseName n of

1454+ "" -> False

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

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

14571461

14581462

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

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

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

14751479showDImp ppo (PDatadecl n ty cons)

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

14781482

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

14801484showDecls 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 (prettyNamePossParen 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" <+> prettyNamePossParen 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) -> prettyNamePossParen True False params' nm <+> maybe empty showDoc md) params)

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

136136

137137getDocs :: Name -> Idris Docs

138138getDocs n

src/Idris/Output.hs+1−1

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

7474 let infixes = idris_infixes ist

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

7676 ihRenderResult h output

77− where fullName n = prettyNamePossParen True bnd n

77+ where fullName n = prettyNamePossParen True True bnd n

7878 ppOverload ppo infixes n tm =

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

8080

src/Idris/Prover.hs+1−1

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

101101

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

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

105105 iputGoal rendered

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

107107 let OK ty = goalAtFocus ps

src/Idris/REPL.hs+6−6

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

367367 where pn ist = displaySpans .

368368 renderPretty 0.9 1000 .

369369 fmap (fancifyAnnots ist) .

370− prettyName True []

370+ prettyNamePossParen True True []

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

372372 case splitName n of

373373 Left err -> iPrintError err

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

379379 where pn ist = displaySpans .

380380 renderPretty 0.9 1000 .

381381 fmap (fancifyAnnots ist) .

382− prettyName True []

382+ prettyNamePossParen True True []

383383

384384splitName :: String -> Either String Name

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

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

928928 ist <- getIState

929929 ihRenderResult h . vsep $

930930 map (\(n, ns) ->

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

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

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

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

933933 calls

934934

935935process h fn (CallsWho n) =

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

937937 ist <- getIState

938938 ihRenderResult h . vsep $

939939 map (\(n, ns) ->

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

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

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

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

942942 calls

943943-- IdrisDoc

944944process h fn (MakeDoc s) =