git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Idris/Prover.hs
146 lines 5.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
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 let proofs = proof_list i
48 put (i { proof_list = (n, prf) : proofs })
49 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
50 logLvl 3 (show tree)
51 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
52 ptm' <- applyOpts ptm
53 updateContext (addCasedef n True False True
54 [Right (P Ref n ty, ptm)]
55 [([], P Ref n ty, ptm)]
56 [([], P Ref n ty, ptm')] ty)
57 solveDeferred n
58elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
59elabStep st e = do case runStateT e st of
60 OK (a, st') -> return (a, st')
61 Error a -> do i <- get
62 fail (pshow i a)
64dumpState :: IState -> ProofState -> IO ()
65dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) =
66 putStrLn . render $ pretty nm <> colon <+> text "No more goals."
67dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ problems i _ _ ctxy _ _) = do
68 let OK ty = goalAtFocus ps
69 let OK env = envAtFocus ps
70 putStrLn . render $
71 prettyOtherGoals hs $$
72 prettyAssumptions env $$
73 prettyGoal ty
74 where
75 -- XXX
76 tPretty t = pretty $ delab ist t
78 prettyPs [] = empty
79 prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
80 prettyPs ((n, Let t v) : bs) =
81 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
82 tPretty t $$ prettyPs bs)
83 prettyPs ((n, b) : bs) =
84 pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
86 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
87 prettyG b = tPretty $ binderTy b
89 prettyGoal ty =
90 text "---------- Goal: ----------" $$
91 pretty h <> colon $$ nest nestingSize (prettyG ty)
93 prettyAssumptions env =
94 if length env == 0 then
95 empty
96 else
97 text "---------- Assumptions: ----------" $$
98 nest nestingSize (prettyPs $ reverse env)
100 prettyOtherGoals hs =
101 if length hs == 0 then
102 empty
103 else
104 text "---------- Other goals: ----------" $$
105 pretty hs
107lifte :: ElabState [PDecl] -> ElabD a -> Idris a
108lifte st e = do (v, _) <- elabStep st e
109 return v
111ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
112ploop d prompt prf e
113 = do i <- get
114 when d $ liftIO $ dumpState i (proof e)
115 x <- lift $ getInputLine (prompt ++ "> ")
116 (cmd, step) <- case x of
117 Nothing -> fail "Abandoned"
118 Just input -> do return (parseTac i input, input)
119 case cmd of
120 Right Abandon -> fail "Abandoned"
121 _ -> return ()
122 (d, st, done, prf') <- idrisCatch
123 (case cmd of
124 Left err -> do iputStrLn (show err)
125 return (False, e, False, prf)
126 Right Undo ->
127 do (_, st) <- elabStep e loadState
128 return (True, st, False, init prf)
129 Right ProofState ->
130 return (True, e, False, prf)
131 Right ProofTerm ->
132 do tm <- lifte e get_term
133 iputStrLn $ "TT: " ++ show tm ++ "\n"
134 return (False, e, False, prf)
135 Right Qed -> do hs <- lifte e get_holes
136 when (not (null hs)) $ fail "Incomplete proof"
137 return (False, e, True, prf)
138 Right tac -> do (_, e) <- elabStep e saveState
139 (_, st) <- elabStep e (runTac True i tac)
140 return (True, st, False, prf ++ [step]))
141 (\err -> do iputStrLn (show err)
142 return (False, e, False, prf))
143 if done then do (tm, _) <- elabStep st get_term
144 return (tm, prf')
145 else ploop d prompt prf' st