git.iko.soy/Idris-dev
on 602ce01 help sign in
Idris-dev/src/Idris/Prover.hs
143 lines 5.3 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
15import Idris.DataOpts
17import System.Console.Haskeline
18import Control.Monad.State
20import Util.Pretty
22prover :: Bool -> Name -> Idris ()
23prover lit x =
24 do ctxt <- getContext
25 i <- get
26 case lookupTy Nothing x ctxt of
27 [t] -> if elem x (idris_metavars i)
28 then prove ctxt lit x t
29 else fail $ show x ++ " is not a metavariable"
30 _ -> fail "No such metavariable"
32showProof :: Bool -> Name -> [String] -> String
33showProof lit n ps
34 = bird ++ show n ++ " = proof {" ++ break ++
35 showSep break (map (\x -> " " ++ x ++ ";") ps) ++
36 break ++ "}\n"
37 where bird = if lit then "> " else ""
38 break = "\n" ++ bird
40prove :: Context -> Bool -> Name -> Type -> Idris ()
41prove ctxt lit n ty
42 = do let ps = initElaborator n ctxt ty
43 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)
44 iLOG $ "Adding " ++ show tm
45 iputStrLn $ showProof lit n prf
46 i <- get
47 put (i { last_proof = Just (n, prf) })
48 let tree = simpleCase False True [(P Ref n ty, tm)]
49 logLvl 3 (show tree)
50 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
51 ptm' <- applyOpts ptm
52 updateContext (addCasedef n True False True [(P Ref n ty, ptm)]
53 [(P Ref n ty, ptm')] ty)
54 solveDeferred n
55elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
56elabStep st e = do case runStateT e st of
57 OK (a, st') -> return (a, st')
58 Error a -> do i <- get
59 fail (pshow i a)
61dumpState :: IState -> ProofState -> IO ()
62dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =
63 putStrLn . render $ pretty nm <> colon <+> text "No more goals."
64dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
65 let OK ty = goalAtFocus ps
66 let OK env = envAtFocus ps
67 putStrLn . render $
68 prettyOtherGoals hs $$
69 prettyAssumptions env $$
70 prettyGoal ty
71 where
72 -- XXX
73 tPretty t = pretty $ delab ist t
75 prettyPs [] = empty
76 prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
77 prettyPs ((n, Let t v) : bs) =
78 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
79 tPretty t $$ prettyPs bs)
80 prettyPs ((n, b) : bs) =
81 pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
83 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
84 prettyG b = tPretty $ binderTy b
86 prettyGoal ty =
87 text "---------- Goal: ----------" $$
88 pretty h <> colon $$ nest nestingSize (prettyG ty)
90 prettyAssumptions env =
91 if length env == 0 then
92 empty
93 else
94 text "---------- Assumptions: ----------" $$
95 nest nestingSize (prettyPs $ reverse env)
97 prettyOtherGoals hs =
98 if length hs == 0 then
99 empty
100 else
101 text "---------- Other goals: ----------" $$
102 pretty hs
104lifte :: ElabState [PDecl] -> ElabD a -> Idris a
105lifte st e = do (v, _) <- elabStep st e
106 return v
108ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
109ploop d prompt prf e
110 = do i <- get
111 when d $ liftIO $ dumpState i (proof e)
112 x <- lift $ getInputLine (prompt ++ "> ")
113 (cmd, step) <- case x of
114 Nothing -> fail "Abandoned"
115 Just input -> do return (parseTac i input, input)
116 case cmd of
117 Right Abandon -> fail "Abandoned"
118 _ -> return ()
119 (d, st, done, prf') <- idrisCatch
120 (case cmd of
121 Left err -> do iputStrLn (show err)
122 return (False, e, False, prf)
123 Right Undo ->
124 do (_, st) <- elabStep e loadState
125 return (True, st, False, init prf)
126 Right ProofState ->
127 return (True, e, False, prf)
128 Right ProofTerm ->
129 do tm <- lifte e get_term
130 iputStrLn $ "TT: " ++ show tm ++ "\n"
131 return (False, e, False, prf)
132 Right Qed -> do hs <- lifte e get_holes
133 when (not (null hs)) $ fail "Incomplete proof"
134 return (False, e, True, prf)
135 Right tac -> do (_, e) <- elabStep e saveState
136 (_, st) <- elabStep e (runTac True i tac)
137 return (True, st, False, prf ++ [step]))
138 (\err -> do iputStrLn (show err)
139 return (False, e, False, prf))
140 if done then do (tm, _) <- elabStep st get_term
141 return (tm, prf')
142 else ploop d prompt prf' st