git.iko.soy/Idris-dev
on 9f65713 help sign in
Idris-dev/src/Idris/Prover.hs
113 lines 4.4 kB history raw
1module Idris.Prover where
3import Core.Elaborate hiding (Tactic(..))
4import Core.TT
5import Core.Evaluate
6import Core.CaseTree
7import Core.Typecheck
9import Idris.AbsSyntax
10import Idris.Delaborate
11import Idris.ElabDecls
12import Idris.ElabTerm
13import Idris.Parser
14import Idris.Error
16import System.Console.Readline
17import Control.Monad.State
19prover :: Name -> Idris ()
20prover x = do ctxt <- getContext
21 i <- get
22 case lookupTy Nothing x ctxt of
23 [t] -> if elem x (idris_metavars i)
24 then prove ctxt x t
25 else fail $ show x ++ " is not a metavariable"
26 _ -> fail "No such metavariable"
28dumpProof :: Name -> [String] -> IO ()
29dumpProof n ps = do putStrLn $ show n ++ " = proof {"
30 mapM_ (\x -> putStrLn $ " " ++ x ++ ";") ps
31 putStrLn "};\n"
33prove :: Context -> Name -> Type -> Idris ()
34prove ctxt n ty
35 = do let ps = initElaborator n ctxt ty
36 (tm, prf) <- ploop True ("-" ++ show n) [] (ES ps "" Nothing)
37 iLOG $ "Adding " ++ show tm
38 lift $ dumpProof n prf
39 let tree = simpleCase False [(P Ref n ty, tm)]
40 logLvl 3 (show tree)
41 (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm
42 updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)
43 solveDeferred n
45elabStep :: ElabState -> Elab a -> Idris (a, ElabState)
46elabStep st e = do case runStateT e st of
47 OK (a, st') -> return (a, st')
48 Error a -> do i <- get
49 fail (pshow i a)
51dumpState :: IState -> ProofState -> IO ()
52dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
53dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ _ ctxy _ _)
54 = do let OK ty = goalAtFocus ps
55 let OK env = envAtFocus ps
56 putStrLn $ "Other goals: " ++ show hs ++ "\n"
57 putStr $ showPs (reverse env)
58 putStrLn $ "---------------------------------- (" ++ show nm
59 ++ ") --------"
60 putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
61 where
62 tshow t = show (delab ist t)
64 showPs [] = ""
65 showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
66 showPs ((n, Let t v) : bs)
67 = " " ++ show n ++ " = " ++ tshow v ++ " : " ++
68 tshow t ++ "\n" ++ showPs bs
69 showPs ((n, b) : bs)
70 = " " ++ show n ++ " : " ++
71 tshow (binderTy b) ++ "\n" ++ showPs bs
73 showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
74 showG b = tshow (binderTy b)
76lifte :: ElabState -> Elab a -> Idris a
77lifte st e = do (v, _) <- elabStep st e
78 return v
80ploop :: Bool -> String -> [String] -> ElabState -> Idris (Term, [String])
81ploop d prompt prf e
82 = do i <- get
83 when d $ lift $ dumpState i (proof e)
84 x <- lift $ readline (prompt ++ "> ")
85 (cmd, step) <- case x of
86 Nothing -> fail "Abandoned"
87 Just input -> do lift $ addHistory input
88 return (parseTac i input, input)
89 (d, st, done, prf') <- idrisCatch
90 (case cmd of
91 Left err -> do iputStrLn (show err)
92 return (False, e, False, prf)
93 Right Undo ->
94 do (_, st) <- elabStep e loadState
95 return (True, st, False, init prf)
96 Right ProofState ->
97 return (True, e, False, prf)
98 Right ProofTerm ->
99 do tm <- lifte e get_term
100 iputStrLn $ "TT: " ++ show tm ++ "\n"
101 return (False, e, False, prf)
102 Right Qed -> do hs <- lifte e get_holes
103 when (not (null hs)) $ fail "Incomplete proof"
104 return (False, e, True, prf)
105 Right tac -> do (_, e) <- elabStep e saveState
106 (_, st) <- elabStep e (runTac True i tac)
107 return (True, st, False, prf ++ [step]))
108 (\err -> do iputStrLn (report err)
109 return (False, e, False, prf))
110 if done then do (tm, _) <- elabStep st get_term
111 return (tm, prf')
112 else ploop d prompt prf' st