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

git.iko.soy/Idris-dev

Add :printdef command to show the definition of a pattern-matching operation

commit893b9803dbc2d9699a30d04a79ca119e2c7e0e33 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 2 Sep 2014, 15:54 (12 years ago) parent2a8d607

5 files changed+27−2

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Help.hs+2−1 src/Idris/REPL.hs+22 src/Idris/REPLParser.hs+1

src/Idris/AbsSyntaxTree.hs+1

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

363363 | CallsWho Name

364364 | MakeDoc String -- IdrisDoc

365365 | Warranty

366+ | PrintDef Name

366367

367368data Opt = Filename String

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

180180 ctxt <- getContext

181181 ist <- getIState

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

184184 (idris_patdefs ist) })

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

186186 case lookupTy n ctxt of

src/Idris/Help.hs+2−1

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

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

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

7171 ([":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")

7374 ]

7475

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

569569 iPrintResult ""

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

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

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

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

573574

574575

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

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

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

11741175 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

11751197

11761198

11771199showTotal :: Totality -> IState -> String

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

138139