git.iko.soy/Idris-dev
on master help sign in
Merge pull request #924 from david-christiansen/prover-new-commands

Prover commands for evaluation and typechecking expressions

commit151d4ef48ad37e5e534b7e31a43a9051d75abe10 authorEdwin Brady <edwin.brady@gmail.com> dateSun 23 Feb 2014, 23:55 (13 years ago) parent3771dd1af0171e
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
@@ -698,6 +698,8 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
698698 | Reflect t
699699 | Fill t
700700 | GoalType String (PTactic' t)
701+ | TCheck t
702+ | TEval t
701703 | Qed | Abandon
702704 deriving (Show, Eq, Functor)
703705{-!
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
@@ -488,7 +488,7 @@ process h fn (Check (PRef _ n))
488488 case lookup t (idris_metavars ist) of
489489 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
490490 showMetavarInfo imp ist n i
491− Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
491+ Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
492492 [] -> ihPrintError h $ "No such variable " ++ show n
493493 where
494494 showMetavarInfo imp ist n i