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

git.iko.soy/Idris-dev

Add :total command

commit9864c25af0cda62063d311e10043f026c9447f0e authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 1 Feb 2012, 16:31 (15 years ago) parent7142d7e

3 files changed+15−7

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−1 src/Idris/REPL.hs+12−6 src/Idris/REPLParser.hs+1

src/Idris/AbsSyntax.hs+2−1

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

322322

323323-- Commands in the REPL

324324

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

326+ | Reload | Edit

326327 | Compile String | Execute | ExecVal PTerm

327328 | Metavars | Prove Name | AddProof | Universes

328329 | TTShell

src/Idris/REPL.hs+12−6

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

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

183183 liftIO $ putStr " = "

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

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

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

189− [t] -> showTotal t i

190− _ -> ""

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

186+ case lookupTotal n (tt_ctxt i) of

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

188+ _ -> return ()

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

192190 let oi = lookupCtxt Nothing n (idris_optimisation i)

193191 liftIO $ print oi

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

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

233231process fn NOP = return ()

234232

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+

235240displayHelp = let vstr = showVersion version in

236241 "\nIdris version " ++ vstr ++ "\n" ++

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

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

246251 ([""], "", ""),

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

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

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

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

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

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

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

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

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

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

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

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

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