9864c25 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add :total command

9864c25Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

@@ -322,7 +322,8 @@ setTypeCase t = do i <- get

322

323-- Commands in the REPL

324

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

326+ | Reload | Edit

326 | Compile String | Execute | ExecVal PTerm

327 | Compile String | Execute | ExecVal PTerm

327 | Metavars | Prove Name | AddProof | Universes

328 | Metavars | Prove Name | AddProof | Universes

328 | TTShell

329 | TTShell

src/Idris/REPL.hs+12−6

@@ -182,12 +182,10 @@ process fn (Defn n) = do i <- get

182 where printCase i (lhs, rhs) = do liftIO $ putStr $ showImp True (delab i lhs)

183 liftIO $ putStr " = "

184 liftIO $ putStrLn $ showImp True (delab i rhs)

185− showTotal t@(Partial (Other ns)) i

185+process fn (TotCheck n) = do i <- get

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

187− showTotal t i = show t

188− showTotalN i n = case lookupTotal n (tt_ctxt i) of

186+ case lookupTotal n (tt_ctxt i) of

189− [t] -> showTotal t i

187+ [t] -> iputStrLn (showTotal t i)

190− _ -> ""

188+ _ -> return ()

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

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

192 let oi = lookupCtxt Nothing n (idris_optimisation i)

190 let oi = lookupCtxt Nothing n (idris_optimisation i)

193 liftIO $ print oi

191 liftIO $ print oi

@@ -232,6 +230,13 @@ process fn Metavars

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

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

233process fn NOP = return ()

231process fn NOP = return ()

234

232

233+showTotal t@(Partial (Other ns)) i

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

235+showTotal t i = show t

236+showTotalN i n = case lookupTotal n (tt_ctxt i) of

237+ [t] -> showTotal t i

238+ _ -> ""

239+

235displayHelp = let vstr = showVersion version in

240displayHelp = let vstr = showVersion version in

236 "\nIdris version " ++ vstr ++ "\n" ++

241 "\nIdris version " ++ vstr ++ "\n" ++

237 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

242 "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++

@@ -246,6 +251,7 @@ help =

246 ([""], "", ""),

251 ([""], "", ""),

247 (["<expr>"], "", "Evaluate an expression"),

252 (["<expr>"], "", "Evaluate an expression"),

248 ([":t"], "<expr>", "Check the type of an expression"),

253 ([":t"], "<expr>", "Check the type of an expression"),

254+ ([":total"], "<name>", "Check the totality of a name"),

249 ([":r",":reload"], "", "Reload current file"),

255 ([":r",":reload"], "", "Reload current file"),

250 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

256 ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),

251 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

257 ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),

src/Idris/REPLParser.hs+1

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

34 <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))

35 <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))

36 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

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

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

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

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

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

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

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