b01a78e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Quick hack at :info for exploring type classes

b01a78eEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+5−3

compare with master

unifiedsplit

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

361

362-- Commands in the REPL

363

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

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

365 | Reload | Edit

366 | Compile String | Execute | ExecVal PTerm

367− | Metavars | Prove Name | AddProof | Universes

367+ | Metavars | Prove Name | AddProof | Universes

368 | TTShell

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

370+ | Info Name | DebugInfo Name

371+ | Search PTerm

370 | NOP

372 | NOP

371

373

372-- Parsed declarations

374-- Parsed declarations

src/Idris/REPL.hs+24−1

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

187 case lookupTotal n (tt_ctxt i) of

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

189 _ -> return ()

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

190+process fn (DebugInfo n)

191+ = do i <- get

191 let oi = lookupCtxtName Nothing n (idris_optimisation i)

192 let oi = lookupCtxtName Nothing n (idris_optimisation i)

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

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

193 let si = lookupCtxt Nothing n (idris_statics i)

194 let si = lookupCtxt Nothing n (idris_statics i)

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

195 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"

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

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

196 ctxt <- getContext

202 ctxt <- getContext

197 ist <- get

203 ist <- get

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

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

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

239process fn NOP = return ()

245process fn NOP = return ()

240

246

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+

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

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

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

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

243showTotal t i = show t

266showTotal t i = show t

src/Idris/REPLParser.hs+2

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

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

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

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

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

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

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

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

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

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

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

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

43 <|> do eof; return NOP

45 <|> do eof; return NOP