151d4ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #924 from david-christiansen/prover-new-commands

151d4efEdwin Brady13 years ago

CHANGELOG+2

compare with master

unifiedsplit

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

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

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

9* 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

11New in 0.9.11:

13New in 0.9.11:

12--------------

14--------------

src/Idris/AbsSyntax.hs+10−10

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

549 IdeSlave n -> ideSlaveReturnAnnotated n h output

550

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

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

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

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

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

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

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

555− ist <- getIState

555+ ist <- getIState

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

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

557− case idris_outputmode ist of

557+ case idris_outputmode ist of

558− RawOutput -> consoleDisplayAnnotated h output

558+ RawOutput -> consoleDisplayAnnotated h output

559− IdeSlave n -> ideSlaveReturnAnnotated n h output

559+ IdeSlave n -> ideSlaveReturnAnnotated n h output

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

560+ where fullName n = prettyName True bnd n

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

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

562

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

564ihRenderResult h d = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+2

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

698 | Reflect t

699 | Fill t

700 | GoalType String (PTactic' t)

701+ | TCheck t

702+ | TEval t

701 | Qed | Abandon

703 | Qed | Abandon

702 deriving (Show, Eq, Functor)

704 deriving (Show, Eq, Functor)

703{-!

705{-!

src/Idris/Completion.hs+6−1

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

45 , ("fill", Just ExprTArg)

46 , ("try", Just AltsTArg)

47 , ("induction", Just NameTArg)

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

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

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

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

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

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

49 "intros", "compute", "trivial", "solve", "attack",

53 "intros", "compute", "trivial", "solve", "attack",

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

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

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

168

172

169

173

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

174completeTactic :: [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

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

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

173 completeArg Nothing = noCompletion (prev, next)

178 completeArg Nothing = noCompletion (prev, next)

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

179 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) (

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

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

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

1176+ <|> do lchar ':';

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

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

1177 <?> "tactic"

1187 <?> "tactic"

1178 where

1188 where

1179 imp :: IdrisParser Bool

1189 imp :: IdrisParser Bool

src/Idris/Prover.hs+61−2

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

10import Idris.Delaborate

11import Idris.ElabDecls

12import Idris.ElabTerm

13−import Idris.Parser

13+import Idris.Parser hiding (params)

14import Idris.Error

15import Idris.DataOpts

16import Idris.Completion

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

21import System.Console.Haskeline

22import System.Console.Haskeline.History

23import Control.Monad.State.Strict

24+import Control.DeepSeq

25import Util.Pretty

26import Util.Pretty

26import Debug.Trace

27import Debug.Trace

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

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

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

201 iPrintResult "Proof completed!"

202 iPrintResult "Proof completed!"

202 return (False, e, True, prf)

203 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)

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

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

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

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

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

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

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

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

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

212 return (tm, prf')

271 return (tm, prf')

213 else ploop d prompt prf' st h'

272 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))

488 case lookup t (idris_metavars ist) of

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

490 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)

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

493 where

494 showMetavarInfo imp ist n i