git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1543 from david-christiansen/pprint-printdef
9fa6e53David Christiansen
src/Idris/AbsSyntaxTree.hs+3−4
compare with master
unifiedsplit
@@ -1246,10 +1246,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1246 text "\\" <> bindingOf n False <+> text "=>" <$>
1246 text "\\" <> bindingOf n False <+> text "=>" <$>
1247 prettySe 10 ((n, False):bnd) sc
1247 prettySe 10 ((n, False):bnd) sc
1248 prettySe p bnd (PLet n ty v sc) =
1248 prettySe p bnd (PLet n ty v sc) =
1249− bracket p 2 $
1249+ bracket p 2 . group . align $
1250− kwd "let" <+> bindingOf n False <+> text "=" </>
1250+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1251− prettySe 10 bnd v <+> kwd "in" </>
1252− prettySe 10 ((n, False):bnd) sc
1251+ kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1253 prettySe p bnd (PPi (Exp l s _) n ty sc)
1252 prettySe p bnd (PPi (Exp l s _) n ty sc)
1254 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1253 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1255 bracket p 2 . group $
1254 bracket p 2 . group $
src/Idris/IdeSlave.hs+2
@@ -218,6 +218,7 @@ data IdeSlaveCommand = REPLCompletions String
218 | TermNormalise [(Name, Bool)] Term
218 | TermNormalise [(Name, Bool)] Term
219 | TermShowImplicits [(Name, Bool)] Term
219 | TermShowImplicits [(Name, Bool)] Term
220 | TermNoImplicits [(Name, Bool)] Term
220 | TermNoImplicits [(Name, Bool)] Term
221+ | PrintDef String
221
222
222sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223sexpToCommand :: SExp -> Maybe IdeSlaveCommand
223sexpToCommand (SexpList (x:[])) = sexpToCommand x
224sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -260,6 +261,7 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])
260 Just (TermShowImplicits bnd tm)
261 Just (TermShowImplicits bnd tm)
261sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
262 Just (TermNoImplicits bnd tm)
263 Just (TermNoImplicits bnd tm)
264+sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
263sexpToCommand _ = Nothing
265sexpToCommand _ = Nothing
264
266
265parseMessage :: String -> Either Err (SExp, Integer)
267parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+34−8
@@ -81,7 +81,7 @@ import Control.Concurrent.MVar
81import Network
81import Network
82import Control.Concurrent
82import Control.Concurrent
83import Data.Maybe
83import Data.Maybe
84−import Data.List
84+import Data.List hiding (group)
85import Data.Char
85import Data.Char
86import Data.Version
86import Data.Version
87import Data.Word (Word)
87import Data.Word (Word)
@@ -477,6 +477,16 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
477 ideSlaveForceTermImplicits h id bnd True tm
477 ideSlaveForceTermImplicits h id bnd True tm
478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
478runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
479 ideSlaveForceTermImplicits h id bnd False tm
479 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+
480
490
481-- | Show a term for IDESlave with the specified implicitness
491-- | Show a term for IDESlave with the specified implicitness
482ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
492ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
@@ -1172,26 +1182,42 @@ process fn (MakeDoc s) =
1172 Left err -> iPrintError err
1182 Left err -> iPrintError err
1173process fn (PrintDef n) =
1183process fn (PrintDef n) =
1174 do ist <- getIState
1184 do ist <- getIState
1185+ ctxt <- getContext
1175 let patdefs = idris_patdefs ist
1186 let patdefs = idris_patdefs ist
1187+ tyinfo = idris_datatypes ist
1176− result = map (ppDef ist) (lookupCtxtName n patdefs)
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))
1177 case result of
1191 case result of
1178 [] -> iPrintError "Not found"
1192 [] -> iPrintError "Not found"
1179 outs -> iRenderResult . vsep $ outs
1193 outs -> iRenderResult . vsep $ outs
1180 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1194 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1181 ppDef ist (n, (clauses, missing)) =
1195 ppDef ist (n, (clauses, missing)) =
1182 prettyName True True [] n <+> colon <+>
1196 prettyName True True [] n <+> colon <+>
1183− pprintPTerm (ppOptionIst ist) [] [] [] (delabTy ist n) <$>
1197+ align (pprintDelabTy ist n) <$>
1184 indent 2 (ppClauses ist clauses <> ppMissing missing)
1198 indent 2 (ppClauses ist clauses <> ppMissing missing)
1185 ppClauses ist [] = text "No clauses."
1199 ppClauses ist [] = text "No clauses."
1186 ppClauses ist cs = vsep (map pp cs)
1200 ppClauses ist cs = vsep (map pp cs)
1187 where pp (vars, lhs, rhs) =
1201 where pp (vars, lhs, rhs) =
1202+ let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1188− let ppTm = pprintPTerm (ppOptionIst ist)
1203+ pprintPTerm (ppOptionIst ist)
1189− (zip vars (repeat False))
1204+ (zip vars (repeat False))
1190− [] [] .
1205+ [] [] .
1191− delab ist
1206+ delab ist $
1207+ t
1192− in ppTm lhs <+> text "=" <+> ppTm rhs
1208+ in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1193 ppMissing _ = empty
1209 ppMissing _ = empty
1194
1210
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)
1195
1221
1196showTotal :: Totality -> IState -> String
1222showTotal :: Totality -> IState -> String
1197showTotal t@(Partial (Other ns)) i
1223showTotal t@(Partial (Other ns)) i