b01a78e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Quick hack at :info for exploring type classes

commitb01a78ed3f164cc50aaf192c304cfc84e43dea6a authorEdwin Brady <edwin@fozzie.(none)> dateSat 7 Apr 2012, 01:09 (15 years ago) parent8c5ca29

3 files changed+31−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−3 src/Idris/REPL.hs+24−1 src/Idris/REPLParser.hs+2

src/Idris/AbsSyntax.hs+5−3

@@ -361,12 +361,14 @@ setTypeCase t = do i <- get

361361

362362-- Commands in the REPL

363363

364−data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

364+data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

365365 | Reload | Edit

366366 | Compile String | Execute | ExecVal PTerm

367− | Metavars | Prove Name | AddProof | Universes

367+ | Metavars | Prove Name | AddProof | Universes

368368 | TTShell

369+ | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

370+ | Info Name | DebugInfo Name

371+ | Search PTerm

370372 | NOP

371373

372374-- Parsed declarations

src/Idris/REPL.hs+24−1

@@ -187,11 +187,17 @@ process fn (TotCheck n) = do i <- get

187187 case lookupTotal n (tt_ctxt i) of

188188 [t] -> iputStrLn (showTotal t i)

189189 _ -> return ()

190−process fn (Info n) = do i <- get

190+process fn (DebugInfo n)

191+ = do i <- get

191192 let oi = lookupCtxtName Nothing n (idris_optimisation i)

192193 when (not (null oi)) $ iputStrLn (show oi)

193194 let si = lookupCtxt Nothing n (idris_statics i)

194195 when (not (null si)) $ iputStrLn (show si)

196+process fn (Info n) = do i <- get

197+ case lookupCtxt Nothing n (idris_classes i) of

198+ [c] -> classInfo c

199+ _ -> iputStrLn "Not a class"

200+process fn (Search t) = iputStrLn "Not implemented"

195201process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

196202 ctxt <- getContext

197203 ist <- get

@@ -238,6 +244,23 @@ process fn Metavars

238244 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs

239245process fn NOP = return ()

240246

247+classInfo :: ClassInfo -> Idris ()

248+classInfo ci = do iputStrLn "Methods:\n"

249+ mapM_ dumpMethod (class_methods ci)

250+ iputStrLn ""

251+ iputStrLn "Instances:\n"

252+ mapM_ dumpInstance (class_instances ci)

253+

254+dumpMethod :: (Name, (FnOpts, PTerm)) -> Idris ()

255+dumpMethod (n, (_, t)) = iputStrLn $ show n ++ " : " ++ show t

256+

257+dumpInstance :: Name -> Idris ()

258+dumpInstance n = do i <- get

259+ ctxt <- getContext

260+ imp <- impShow

261+ case lookupTy Nothing n ctxt of

262+ ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts

263+

241264showTotal t@(Partial (Other ns)) i

242265 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)

243266showTotal t i = show t

src/Idris/REPLParser.hs+2

@@ -37,7 +37,9 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

3737 <|> try (do cmd ["total"]; do n <- pName; eof; return (TotCheck n))

3838 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

3939 <|> try (do cmd ["u", "universes"]; eof; return Universes)

40+ <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))

4041 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

42+ <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

4143 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

4244 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

4345 <|> do eof; return NOP