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

Major improvements to pretty-printing and :printdef

commit9fa6e53ae964164276b63e02578b544e2496e72c authorDavid Christiansen <david@davidchristiansen.dk> dateWed 24 Sep 2014, 14:57 (12 years ago) parentd63c212fe8927c
3 files changed+39−12
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+3−4 src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+34−8
src/Idris/AbsSyntaxTree.hs+3−4
@@ -1246,10 +1246,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12461246 text "\\" <> bindingOf n False <+> text "=>" <$>
12471247 prettySe 10 ((n, False):bnd) sc
12481248 prettySe p bnd (PLet n ty v sc) =
1249− bracket p 2 $
1250− kwd "let" <+> bindingOf n False <+> text "=" </>
1251− prettySe 10 bnd v <+> kwd "in" </>
1252− prettySe 10 ((n, False):bnd) sc
1249+ bracket p 2 . group . align $
1250+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1251+ kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
12531252 prettySe p bnd (PPi (Exp l s _) n ty sc)
12541253 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
12551254 bracket p 2 . group $
src/Idris/IdeSlave.hs+2
@@ -218,6 +218,7 @@ data IdeSlaveCommand = REPLCompletions String
218218 | TermNormalise [(Name, Bool)] Term
219219 | TermShowImplicits [(Name, Bool)] Term
220220 | TermNoImplicits [(Name, Bool)] Term
221+ | PrintDef String
221222
222223sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223224sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -260,6 +261,7 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
260261 Just (TermShowImplicits bnd tm)
261262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262263 Just (TermNoImplicits bnd tm)
264+sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
263265sexpToCommand _ = Nothing
264266
265267parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+34−8
@@ -81,7 +81,7 @@ import Control.Concurrent.MVar
8181import Network
8282import Control.Concurrent
8383import Data.Maybe
84−import Data.List
84+import Data.List hiding (group)
8585import Data.Char
8686import Data.Version
8787import Data.Word (Word)
@@ -477,6 +477,16 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
477477 ideSlaveForceTermImplicits h id bnd True tm
478478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
479479 ideSlaveForceTermImplicits h id bnd False tm
480+runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =
481+ case splitName name of
482+ Left err -> iPrintError err
483+ Right n -> process "(ideslave)" (PrintDef n)
484+ where splitName :: String -> Either String Name
485+ splitName s = case reverse $ splitOn "." s of
486+ [] -> Left ("Didn't understand name '" ++ s ++ "'")
487+ [n] -> Right $ sUN n
488+ (n:ns) -> Right $ sNS (sUN n) ns
489+
480490
481491-- | Show a term for IDESlave with the specified implicitness
482492ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
@@ -1172,26 +1182,42 @@ process fn (MakeDoc s) =
11721182 Left err -> iPrintError err
11731183process fn (PrintDef n) =
11741184 do ist <- getIState
1185+ ctxt <- getContext
11751186 let patdefs = idris_patdefs ist
1176− result = map (ppDef ist) (lookupCtxtName n patdefs)
1187+ tyinfo = idris_datatypes ist
1188+ result = map (ppDef ist) (lookupCtxtName n patdefs) ++
1189+ map (ppTy ist) (lookupCtxtName n tyinfo) ++
1190+ map (ppCon ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
11771191 case result of
11781192 [] -> iPrintError "Not found"
11791193 outs -> iRenderResult . vsep $ outs
11801194 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
11811195 ppDef ist (n, (clauses, missing)) =
11821196 prettyName True True [] n <+> colon <+>
1183− pprintPTerm (ppOptionIst ist) [] [] [] (delabTy ist n) <$>
1197+ align (pprintDelabTy ist n) <$>
11841198 indent 2 (ppClauses ist clauses <> ppMissing missing)
11851199 ppClauses ist [] = text "No clauses."
11861200 ppClauses ist cs = vsep (map pp cs)
11871201 where pp (vars, lhs, rhs) =
1188− let ppTm = pprintPTerm (ppOptionIst ist)
1189− (zip vars (repeat False))
1190− [] [] .
1191− delab ist
1192− in ppTm lhs <+> text "=" <+> ppTm rhs
1202+ let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1203+ pprintPTerm (ppOptionIst ist)
1204+ (zip vars (repeat False))
1205+ [] [] .
1206+ delab ist $
1207+ t
1208+ in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
11931209 ppMissing _ = empty
11941210
1211+ ppTy :: IState -> (Name, TypeInfo) -> Doc OutputAnnotation
1212+ ppTy ist (n, TI constructors isCodata _ _ _)
1213+ = kwd key <+> prettyName True True [] n <+> colon <+>
1214+ align (pprintDelabTy ist n) <+> kwd "where" <$>
1215+ indent 2 (vsep (map (ppCon ist) constructors))
1216+ where
1217+ key | isCodata = "codata"
1218+ | otherwise = "data"
1219+ kwd = annotate AnnKeyword . text
1220+ ppCon ist n = prettyName True False [] n <+> colon <+> align (pprintDelabTy ist n)
11951221
11961222showTotal :: Totality -> IState -> String
11971223showTotal t@(Partial (Other ns)) i