git.iko.soy/Idris-dev
on baff441 help sign in
Idris-dev/src/Idris/Prover.hs
170 lines 6.6 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
16import Idris.Completion
18import System.Console.Haskeline
19import System.Console.Haskeline.History
20import Control.Monad.State
22import Util.Pretty
23import Debug.Trace
25prover :: Bool -> Name -> Idris ()
26prover lit x =
27 do ctxt <- getContext
28 i <- getIState
29 case lookupTy Nothing x ctxt of
30 [t] -> if elem x (idris_metavars i)
31 then prove ctxt lit x t
32 else fail $ show x ++ " is not a metavariable"
33 _ -> fail "No such metavariable"
35showProof :: Bool -> Name -> [String] -> String
36showProof lit n ps
37 = bird ++ show n ++ " = proof {" ++ break ++
38 showSep break (map (\x -> " " ++ x ++ ";") ps) ++
39 break ++ "}\n"
40 where bird = if lit then "> " else ""
41 break = "\n" ++ bird
43proverSettings :: ElabState [PDecl] -> Settings Idris
44proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings
45 where assumptionNames = case envAtFocus (proof e) of
46 OK env -> names env
47 names [] = []
48 names ((MN _ _, _) : bs) = names bs
49 names ((n, _) : bs) = show n : names bs
51prove :: Context -> Bool -> Name -> Type -> Idris ()
52prove ctxt lit n ty
53 = do let ps = initElaborator n ctxt ty
54 (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
55 iLOG $ "Adding " ++ show tm
56 iputStrLn $ showProof lit n prf
57 i <- getIState
58 let proofs = proof_list i
59 putIState (i { proof_list = (n, prf) : proofs })
60 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
61 logLvl 3 (show tree)
62 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
63 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
64 "Expected type:" ++ show ty)
65 case converts ctxt [] ty pty of
66 OK _ -> return ()
67 Error e -> ierror (CantUnify False ty pty e [] 0)
68 ptm' <- applyOpts ptm
69 updateContext (addCasedef n True False True False
70 [Right (P Ref n ty, ptm)]
71 [([], P Ref n ty, ptm)]
72 [([], P Ref n ty, ptm')] ty)
73 solveDeferred n
74elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
75elabStep st e = do case runStateT e st of
76 OK (a, st') -> return (a, st')
77 Error a -> do i <- getIState
78 fail (pshow i a)
80dumpState :: IState -> ProofState -> IO ()
81dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) =
82 putStrLn . render $ pretty nm <> colon <+> text "No more goals."
83dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do
84 let OK ty = goalAtFocus ps
85 let OK env = envAtFocus ps
86 putStrLn . render $
87 prettyOtherGoals hs $$
88 prettyAssumptions env $$
89 prettyGoal ty
90 where
91 -- XXX
92 tPretty t = pretty $ delab ist t
94 prettyPs [] = empty
95 prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
96 prettyPs ((n, Let t v) : bs) =
97 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
98 tPretty t $$ prettyPs bs)
99 prettyPs ((n, b) : bs) =
100 pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
102 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
103 prettyG b = tPretty $ binderTy b
105 prettyGoal ty =
106 text "---------- Goal: ----------" $$
107 pretty h <> colon $$ nest nestingSize (prettyG ty)
109 prettyAssumptions env =
110 if length env == 0 then
111 empty
112 else
113 text "---------- Assumptions: ----------" $$
114 nest nestingSize (prettyPs $ reverse env)
116 prettyOtherGoals hs =
117 if length hs == 0 then
118 empty
119 else
120 text "---------- Other goals: ----------" $$
121 pretty hs
123lifte :: ElabState [PDecl] -> ElabD a -> Idris a
124lifte st e = do (v, _) <- elabStep st e
125 return v
127ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
128ploop d prompt prf e h
129 = do i <- getIState
130 when d $ liftIO $ dumpState i (proof e)
131 (x, h') <- runInputT (proverSettings e) $
132 -- Manually track the history so that we can use the proof state
133 do _ <- case h of
134 Just history -> putHistory history
135 Nothing -> return ()
136 l <- getInputLine (prompt ++ "> ")
137 h' <- getHistory
138 return (l, Just h')
139 (cmd, step) <- case x of
140 Nothing -> fail "Abandoned"
141 Just input -> do return (parseTac i input, input)
142 case cmd of
143 Right Abandon -> fail "Abandoned"
144 _ -> return ()
145 (d, st, done, prf') <- idrisCatch
146 (case cmd of
147 Left err -> do iputStrLn (show err)
148 return (False, e, False, prf)
149 Right Undo ->
150 do (_, st) <- elabStep e loadState
151 return (True, st, False, init prf)
152 Right ProofState ->
153 return (True, e, False, prf)
154 Right ProofTerm ->
155 do tm <- lifte e get_term
156 iputStrLn $ "TT: " ++ show tm ++ "\n"
157 return (False, e, False, prf)
158 Right Qed -> do hs <- lifte e get_holes
159 when (not (null hs)) $ fail "Incomplete proof"
160 return (False, e, True, prf)
161 Right tac -> do (_, e) <- elabStep e saveState
162 (_, st) <- elabStep e (runTac True i tac)
163-- trace (show (problems (proof st))) $
164 return (True, st, False, prf ++ [step]))
165 (\err -> do iputStrLn (show err)
166 return (False, e, False, prf))
167 if done then do (tm, _) <- elabStep st get_term
168 return (tm, prf')
169 else ploop d prompt prf' st h'