git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1541 from david-christiansen/pprint-more-annots

Pretty-printer improvements

commit8cc769b89eaecb1fff12a202244df66365006e53 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 24 Sep 2014, 10:18 (12 years ago) parentc26f9aeba0b525
4 files changed+16−7
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+12−3 src/Idris/Output.hs+2−2 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+1−1
src/Idris/AbsSyntaxTree.hs+12−3
@@ -1342,9 +1342,18 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13421342 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
13431343 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
13441344 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1345− prettySe p bnd (PEq _ _ _ l r) =
1346− bracket p 2 . align . group $
1347− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1345+ prettySe p bnd (PEq _ lt rt l r)
1346+ | ppopt_impl ppo =
1347+ bracket p 1 $
1348+ enclose lparen rparen eq <+>
1349+ align (group (vsep (map (prettyArgS bnd)
1350+ [PImp 0 False [] (sUN "A") lt,
1351+ PImp 0 False [] (sUN "B") rt,
1352+ PExp 0 [] (sUN "x") l,
1353+ PExp 0 [] (sUN "y") r])))
1354+ | otherwise =
1355+ bracket p 2 . align . group $
1356+ prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
13481357 where eq = annName eqTy (text "=")
13491358 prettySe p bnd (PRewrite _ l r _) =
13501359 bracket p 2 $
src/Idris/Output.hs+2−2
@@ -68,7 +68,7 @@ iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
6868iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)
6969
7070-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
71−iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
71+iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()
7272iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n
7373iPrintFunTypes bnd n overloads = do ist <- getIState
7474 let ppo = ppOptionIst ist
@@ -77,7 +77,7 @@ iPrintFunTypes bnd n overloads = do ist <- getIState
7777 iRenderResult output
7878 where fullName n = prettyName True True bnd n
7979 ppOverload ppo infixes n tm =
80− fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
80+ fullName n <+> colon <+> align tm
8181
8282iRenderOutput :: Doc OutputAnnotation -> Idris ()
8383iRenderOutput doc =
src/Idris/Prover.hs+1−1
@@ -274,7 +274,7 @@ ploop fn d prompt prf e h
274274 -- make it easier to see how to prove with them.
275275 let action = case lookupNames n ctxt' of
276276 [] -> iPrintError $ "No such variable " ++ show n
277− ts -> iPrintFunTypes bnd n (map (\n -> (n, delabTy ist' n)) ts)
277+ ts -> iPrintFunTypes bnd n (map (\n -> (n, pprintDelabTy ist' n)) ts)
278278 putIState ist
279279 return (False, e, False, prf, Right action))
280280 (\err -> do putIState ist ; ierror err)
src/Idris/REPL.hs+1−1
@@ -819,7 +819,7 @@ process fn (Check (PRef _ n))
819819 case lookup t (idris_metavars ist) of
820820 Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $
821821 showMetavarInfo ppo ist n i
822− Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)
822+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
823823 [] -> iPrintError $ "No such variable " ++ show n
824824 where
825825 showMetavarInfo ppo ist n i