af0171e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands: * :t, :type gives the type of an expression * :e, :eval normalises the expression and prints the result These work within the proof environment, so evaluating expressions that contain references to hypotheses is allowed.

commitaf0171ee6bff164b5918a942fc5c3074141bc3a9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 23 Feb 2014, 18:05 (13 years ago) parentecfb293

7 files changed+93−15

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntax.hs+10−10 src/Idris/AbsSyntaxTree.hs+2 src/Idris/Completion.hs+6−1 src/Idris/ParseExpr.hs+11−1 src/Idris/Prover.hs+61−2 src/Idris/REPL.hs+1−1

CHANGELOG+2

@@ -7,6 +7,8 @@ New in 0.9.12:

77* JavaScript and Node codegen now understand the %include directive

88* Concept up 'null' is now understood in the JavaScript and Node codegen

99* Lots of performance patches for generated JavaScript

10+* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11+ or show the type of expressions

1012

1113New in 0.9.11:

1214--------------

src/Idris/AbsSyntax.hs+10−10

@@ -549,16 +549,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState

549549 IdeSlave n -> ideSlaveReturnAnnotated n h output

550550

551551-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

552−ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()

553−ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n

554−ihPrintFunTypes h n overloads = do imp <- impShow

555− ist <- getIState

556− let output = vsep (map (uncurry (ppOverload imp)) overloads)

557− case idris_outputmode ist of

558− RawOutput -> consoleDisplayAnnotated h output

559− IdeSlave n -> ideSlaveReturnAnnotated n h output

560− where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)

561− ppOverload imp n tm = fullName n <+> colon <+> align (prettyImp imp tm)

552+ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

553+ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

554+ihPrintFunTypes h bnd n overloads = do imp <- impShow

555+ ist <- getIState

556+ let output = vsep (map (uncurry (ppOverload imp)) overloads)

557+ case idris_outputmode ist of

558+ RawOutput -> consoleDisplayAnnotated h output

559+ IdeSlave n -> ideSlaveReturnAnnotated n h output

560+ where fullName n = prettyName True bnd n

561+ ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd tm)

562562

563563ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

564564ihRenderResult h d = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+2

@@ -697,6 +697,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

697697 | Reflect t

698698 | Fill t

699699 | GoalType String (PTactic' t)

700+ | TCheck t

701+ | TEval t

700702 | Qed | Abandon

701703 deriving (Show, Eq, Functor)

702704{-!

src/Idris/Completion.hs+6−1

@@ -45,6 +45,10 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

4545 , ("fill", Just ExprTArg)

4646 , ("try", Just AltsTArg)

4747 , ("induction", Just NameTArg)

48+ , (":t", Just ExprTArg)

49+ , (":type", Just ExprTArg)

50+ , (":e", Just ExprTArg)

51+ , (":eval", Just ExprTArg)

4852 ] ++ map (\x -> (x, Nothing)) [

4953 "intros", "compute", "trivial", "solve", "attack",

5054 "state", "term", "undo", "qed", "abandon", ":q"

@@ -168,7 +172,8 @@ replCompletion (prev, next) = case firstWord of

168172

169173

170174completeTactic :: [String] -> String -> CompletionFunc Idris

171−completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs

175+completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $

176+ lookup tac tacticArgs

172177 where completeTacName = return $ ("", completeWith tactics tac)

173178 completeArg Nothing = noCompletion (prev, next)

174179 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!

src/Idris/ParseExpr.hs+11−1

@@ -1173,7 +1173,17 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11731173 <|> do reserved "undo"; return Undo

11741174 <|> do reserved "qed"; return Qed

11751175 <|> do reserved "abandon"; return Abandon

1176− <|> do lchar ':'; reserved "q"; return Abandon

1176+ <|> do lchar ':';

1177+ ( (do reserved "q"; return Abandon)

1178+ <|> (do (reserved "e" <|> reserved "eval");

1179+ t <- (indentPropHolds gtProp *> expr syn);

1180+ i <- get

1181+ return $ TEval (desugar syn i t))

1182+ <|> (do (reserved "t" <|> reserved "type");

1183+ t <- (indentPropHolds gtProp *> expr syn);

1184+ i <- get

1185+ return $ TCheck (desugar syn i t))

1186+ <?> "prover command")

11771187 <?> "tactic"

11781188 where

11791189 imp :: IdrisParser Bool

src/Idris/Prover.hs+61−2

@@ -10,7 +10,7 @@ import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.ElabDecls

1212import Idris.ElabTerm

13−import Idris.Parser

13+import Idris.Parser hiding (params)

1414import Idris.Error

1515import Idris.DataOpts

1616import Idris.Completion

@@ -21,6 +21,7 @@ import Text.Trifecta.Result(Result(..))

2121import System.Console.Haskeline

2222import System.Console.Haskeline.History

2323import Control.Monad.State.Strict

24+import Control.DeepSeq

2425

2526import Util.Pretty

2627import Debug.Trace

@@ -200,6 +201,64 @@ ploop d prompt prf e h

200201 when (not (null hs)) $ ifail "Incomplete proof"

201202 iPrintResult "Proof completed!"

202203 return (False, e, True, prf)

204+ Success (TCheck (PRef _ n)) ->

205+ do ctxt <- getContext

206+ ist <- getIState

207+ imp <- impShow

208+ idrisCatch (do

209+ let h = idris_outh ist

210+ OK env = envAtFocus (proof e)

211+ ctxt' = envCtxt env ctxt

212+ bnd = map (\x -> (fst x, False)) env

213+ ist' = ist { tt_ctxt = ctxt' }

214+ putIState ist'

215+ -- Unlike the REPL, metavars have no special treatment, to

216+ -- make it easier to see how to prove with them.

217+ case lookupNames n ctxt' of

218+ [] -> ihPrintError h $ "No such variable " ++ show n

219+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

220+ putIState ist

221+ return (False, e, False, prf))

222+ (\err -> do putIState ist ; ierror err)

223+ Success (TCheck t) ->

224+ do ist <- getIState

225+ ctxt <- getContext

226+ idrisCatch (do

227+ let OK env = envAtFocus (proof e)

228+ ctxt' = envCtxt env ctxt

229+ putIState ist { tt_ctxt = ctxt' }

230+ (tm, ty) <- elabVal toplevel False t

231+ let imp = opt_showimp (idris_options ist)

232+ ty' = normaliseC ctxt [] ty

233+ h = idris_outh ist

234+ case tm of

235+ TType _ ->

236+ ihPrintTermWithType h (prettyImp imp PType) type1Doc

237+ _ -> let bnd = map (\x -> (fst x, False)) env in

238+ ihPrintTermWithType h (pprintPTerm imp bnd (delab ist tm))

239+ (pprintPTerm imp bnd (delab ist ty))

240+ putIState ist

241+ return (False, e, False, prf))

242+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

243+ Success (TEval t) -> withErrorReflection $

244+ do ctxt <- getContext

245+ ist <- getIState

246+ idrisCatch (do

247+ let OK env = envAtFocus (proof e)

248+ ctxt' = envCtxt env ctxt

249+ ist' = ist { tt_ctxt = ctxt' }

250+ bnd = map (\x -> (fst x, False)) env

251+ putIState ist'

252+ (tm, ty) <- elabVal toplevel False t

253+ let tm' = force (normaliseAll ctxt' env tm)

254+ ty' = force (normaliseAll ctxt' env ty)

255+ imp = opt_showimp (idris_options ist')

256+ tmDoc = pprintPTerm imp bnd (delab ist' tm')

257+ tyDoc = pprintPTerm imp bnd (delab ist' ty')

258+ ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

259+ putIState ist

260+ return (False, e, False, prf))

261+ (\err -> do putIState ist ; ierror err)

203262 Success tac -> do (_, e) <- elabStep e saveState

204263 (_, st) <- elabStep e (runTac True i tac)

205264-- trace (show (problems (proof st))) $

@@ -211,4 +270,4 @@ ploop d prompt prf e h

211270 if done then do (tm, _) <- elabStep st get_term

212271 return (tm, prf')

213272 else ploop d prompt prf' st h'

214−

273+ where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

src/Idris/REPL.hs+1−1

@@ -496,7 +496,7 @@ process h fn (Check (PRef _ n))

496496 case lookup t (idris_metavars ist) of

497497 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

498498 showMetavarInfo imp ist n i

499− Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)

499+ Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

500500 [] -> ihPrintError h $ "No such variable " ++ show n

501501 where

502502 showMetavarInfo imp ist n i