@@ -0,0 +1,91 @@
1+module Idris.Prover where
2+
3+import Core.Elaborate hiding (Tactic(..))
4+import Core.TT
5+import Core.Evaluate
6+import Core.CaseTree
7+import Core.Typecheck
8+
9+import Idris.AbsSyntax
10+import Idris.Delaborate
11+import Idris.ElabDecls
12+import Idris.Parser
13+import Idris.Error
14+
15+import System.Console.Readline
16+import Control.Monad.State
17+
18+prover :: Name -> Idris ()
19+prover x = do ctxt <- getContext
20+ i <- get
21+ case lookupTy x ctxt of
22+ Just t -> if elem x (idris_metavars i)
23+ then prove ctxt x t
24+ else fail $ show x ++ " is not a metavariable"
25+ _ -> fail "No such metavariable"
26+
27+prove :: Context -> Name -> Type -> Idris ()
28+prove ctxt n ty
29+ = do let ps = initElaborator n ctxt ty
30+ tm <- ploop True ("-" ++ show n) (ps, "")
31+ iLOG $ "Adding " ++ show tm
32+ let tree = simpleCase False [(P Ref n ty, tm)]
33+ logLvl 3 (show tree)
34+ (ptm, pty) <- tclift $ recheck ctxt [] tm
35+ updateContext (addCasedef n False [(P Ref n ty, ptm)] ty)
36+ solveDeferred n
37+
38+elabStep :: ElabState -> Elab a -> Idris (a, ElabState)
39+elabStep st e = do case runStateT e st of
40+ OK (a, st') -> return (a, st')
41+ Error a -> do i <- get
42+ fail (pshow i a)
43+
44+dumpState :: IState -> ProofState -> IO ()
45+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
46+dumpState ist ps@(PS nm (h:hs) _ tm _ _ i _ cyxy _ _)
47+ = do let OK ty = goalAtFocus ps
48+ let OK env = envAtFocus ps
49+ putStrLn $ "Other goals: " ++ show hs ++ "\n"
50+ putStr $ showPs (reverse env)
51+ putStrLn $ "---------------------------------- (" ++ show nm
52+ ++ ") --------"
53+ putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
54+ where
55+ tshow t = show (delab ist t)
56+
57+ showPs [] = ""
58+ showPs ((n, Let t v) : bs)
59+ = " " ++ show n ++ " : " ++
60+ tshow t ++ " = " ++ tshow v ++ "\n" ++ showPs bs
61+ showPs ((n, b) : bs)
62+ = " " ++ show n ++ " : " ++
63+ tshow (binderTy b) ++ "\n" ++ showPs bs
64+
65+ showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
66+ showG b = tshow (binderTy b)
67+
68+ploop :: Bool -> String -> ElabState -> Idris Term
69+ploop d prompt e
70+ = do i <- get
71+ when d $ lift $ dumpState i (proof e)
72+ x <- lift $ readline (prompt ++ "> ")
73+ cmd <- case x of
74+ Nothing -> fail "Abandoned"
75+ Just input -> do lift $ addHistory input
76+ return (parseTac i input)
77+ (d, st, done) <- idrisCatch
78+ (case cmd of
79+ Left err -> do iputStrLn (show err)
80+ return (False, e, False)
81+ Right Qed -> do (hs, _) <- elabStep e get_holes
82+ when (not (null hs)) $ fail "Incomplete proof"
83+ return (False, e, True)
84+ Right tac -> do (_, st) <- elabStep e (runTac tac)
85+ return (True, st, False))
86+ (\err -> do iputStrLn (report err)
87+ return (False, e, False))
88+ if done then do (tm, _) <- elabStep st get_term
89+ return tm
90+ else ploop d prompt st
91+