893b980 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -363,6 +363,7 @@ data Command = Quit

363 | CallsWho Name

364 | MakeDoc String -- IdrisDoc

365 | Warranty

366+ | PrintDef Name

366

367

367data Opt = Filename String

368data Opt = Filename String

368 | Quiet

369 | Quiet

src/Idris/Elab/Clause.hs+1−1

@@ -180,7 +180,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

180 ctxt <- getContext

181 ist <- getIState

182 let opt = idris_optimisation ist

183− putIState (ist { idris_patdefs = addDef n (force pdef', force pmissing)

183+ putIState (ist { idris_patdefs = addDef n (force pdef, force pmissing)

184 (idris_patdefs ist) })

185 let caseInfo = CaseInfo (inlinable opts) (dictionary opts)

186 case lookupTy n ctxt of

src/Idris/Help.hs+2−1

@@ -69,7 +69,8 @@ help =

69 ([":q",":quit"], NoArg, "Exit the Idris system"),

70 ([":w", ":warranty"], NoArg, "Displays warranty information"),

71 ([":let"], ManyArgs DeclArg, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"),

72− ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given")

72+ ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given"),

73+ ([":printdef"], NameArg, "Show the definition of a function")

73 ]

74 ]

74

75

75-- | Use these for completion, but don't show them in :help

76-- | Use these for completion, but don't show them in :help

src/Idris/REPL.hs+22

@@ -569,6 +569,7 @@ ideslaveProcess fn (Apropos a) = do process fn (Apropos a)

569 iPrintResult ""

570ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

571ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

572+ideslaveProcess fn (PrintDef n) = process fn (PrintDef n)

572ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

573ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

573

574

575

@@ -1172,6 +1173,27 @@ process fn (MakeDoc s) =

1172 else return . Left $ "Illegal name: " ++ head bad

1173 else return . Left $ "Illegal name: " ++ head bad

1173 case result of Right _ -> iputStrLn "IdrisDoc generated"

1174 case result of Right _ -> iputStrLn "IdrisDoc generated"

1174 Left err -> iPrintError err

1175 Left err -> iPrintError err

1176+process fn (PrintDef n) =

1177+ do ist <- getIState

1178+ let patdefs = idris_patdefs ist

1179+ result = map (ppDef ist) (lookupCtxtName n patdefs)

1180+ case result of

1181+ [] -> iPrintError "Not found"

1182+ outs -> iRenderResult . vsep $ outs

1183+ where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation

1184+ ppDef ist (n, (clauses, missing)) =

1185+ prettyName True True [] n <+> colon <+>

1186+ pprintPTerm (ppOptionIst ist) [] [] [] (delabTy ist n) <$>

1187+ indent 2 (ppClauses ist clauses <> ppMissing missing)

1188+ ppClauses ist [] = text "No clauses."

1189+ ppClauses ist cs = vsep (map pp cs)

1190+ where pp (vars, lhs, rhs) =

1191+ let ppTm = pprintPTerm (ppOptionIst ist)

1192+ (zip vars (repeat False))

1193+ [] [] .

1194+ delab ist

1195+ in ppTm lhs <+> text "=" <+> ppTm rhs

1196+ ppMissing _ = empty

1175

1197

1176

1198

1177showTotal :: Totality -> IState -> String

1199showTotal :: Totality -> IState -> String

src/Idris/REPLParser.hs+1

@@ -133,6 +133,7 @@ pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

133 <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)

134 <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

135 <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

136+ <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)

136 <|> do P.whiteSpace; do eof; return NOP

137 <|> do P.whiteSpace; do eof; return NOP

137 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

138 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

138

139