git.iko.soy/Idris-dev
on 1b6709f help sign in
Idris-dev/src/Core/ProofState.hs
341 lines 13 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
7module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), processTactic) where
10import Core.Typecheck
11import Core.Evaluate
12import Core.TT
13import Core.Unify
15import Control.Monad.State
16import Control.Applicative
17import Data.List
18import Debug.Trace
20data ProofState = PS { thname :: Name,
21 holes :: [Name], -- holes still to be solved
22 nextname :: Int, -- name supply
23 pterm :: Term, -- current proof term
24 ptype :: Type, -- original goal
25 unified :: (Name, [(Name, Term)]),
26 defer :: [(Name, Type)], -- names we'll need to define
27 previous :: Maybe ProofState, -- for undo
28 context :: Context,
29 plog :: String,
30 done :: Bool
31 }
33data Goal = GD { premises :: Env,
34 goalType :: Binder Term
35 }
37data Tactic = Attack
38 | Claim Name Raw
39 | Exact Raw
40 | Fill Raw
41 | Regret
42 | Solve
43 | StartUnify Name
44 | EndUnify
45 | Compute
46 | EvalIn Raw
47 | CheckIn Raw
48 | Intro Name
49 | Forall Name Raw
50 | PatVar Name
51 | Focus Name
52 | MoveLast Name
53 | ProofState
54 | Undo
55 | QED
57-- Some utilites on proof and tactic states
59instance Show ProofState where
60 show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
61 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
62 = let OK g = goal (Just h) tm
63 wkenv = premises g in
64 "Other goals: " ++ show hs ++ "\n" ++
65 showPs wkenv (reverse wkenv) ++ "\n" ++
66 "-------------------------------- (" ++ show nm ++
67 ") -------\n " ++
68 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
69 where showPs env [] = ""
70 showPs env ((n, Let t v):bs)
71 = " " ++ show n ++ " : " ++
72 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
73 showEnv env ({- normalise ctxt env -} v) ++
74 "\n" ++ showPs env bs
75 showPs env ((n, b):bs)
76 = " " ++ show n ++ " : " ++
77 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
78 "\n" ++ showPs env bs
79 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
80 " =?= " ++ showEnv ps v
81 showG ps b = showEnv ps (binderTy b)
83same Nothing n = True
84same (Just x) n = x == n
86hole (Hole _) = True
87hole (Guess _ _) = True
88hole _ = False
90holeName i = MN i "hole"
92getName :: Monad m => String -> StateT TState m Name
93getName tag = do ps <- get
94 let n = nextname ps
95 put (ps { nextname = n+1 })
96 return $ MN n tag
98action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
99action a = do ps <- get
100 put (a ps)
102addLog :: Monad m => String -> StateT TState m ()
103addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
105newProof :: Name -> Context -> Type -> ProofState
106newProof n ctxt ty = let h = holeName 0
107 ty' = vToP ty in
108 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
109 Nothing ctxt "" False
111type TState = ProofState -- [TacticAction])
112type RunTactic = Context -> Env -> Term -> StateT TState TC Term
113type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
115envAtFocus :: ProofState -> TC Env
116envAtFocus ps
117 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
118 return (premises g)
119 | otherwise = fail "No holes"
121goalAtFocus :: ProofState -> TC Type
122goalAtFocus ps
123 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
124 return (binderTy (goalType g))
126goal :: Hole -> Term -> TC Goal
127goal h tm = g [] tm where
128 g env (Bind n b sc) | hole b && same h n = return $ GD env b
129 | otherwise
130 = gb env b `mplus` g ((n, b):env) sc
131 g env (App f a) = g env f `mplus` g env a
132 g env t = Error "Can't find hole"
134 gb env (Let t v) = g env t `mplus` g env v
135 gb env (Guess t v) = g env t `mplus` g env v
136 gb env t = g env (binderTy t)
138tactic :: Hole -> RunTactic -> StateT TState TC ()
139tactic h f = do ps <- get
140 tm' <- atH (context ps) [] (pterm ps)
141 ps <- get -- might have changed while processing
142 put (ps { pterm = tm' })
143 where
144 atH c env binder@(Bind n b sc)
145 | hole b && same h n = f c env binder
146 | otherwise
147 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
148 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
149 atH c env t = return t
151 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
152 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
153 atHb c env t = do ty' <- atH c env (binderTy t)
154 return $ t { binderTy = ty' }
156attack :: RunTactic
157attack ctxt env (Bind x (Hole t) sc)
158 = do h <- getName "hole"
159 action (\ps -> ps { holes = h : holes ps })
160 return $ Bind x (Guess t (newtm h)) sc
161 where
162 newtm h = Bind h (Hole t) (P Bound h t)
163attack ctxt env _ = fail "Not an attackable hole"
165claim :: Name -> Raw -> RunTactic
166claim n ty ctxt env t =
167 do (tyv, tyt) <- lift $ check ctxt env ty
168 lift $ isSet ctxt env tyt
169 action (\ps -> let (g:gs) = holes ps in
170 ps { holes = g : n : gs } )
171 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
173focus :: Name -> RunTactic
174focus n ctxt env t = do action (\ps -> let hs = holes ps in
175 if n `elem` hs
176 then ps { holes = n : (hs \\ [n]) }
177 else ps)
178 return t
180movelast :: Name -> RunTactic
181movelast n ctxt env t = do action (\ps -> let hs = holes ps in
182 if n `elem` hs
183 then ps { holes = (hs \\ [n]) ++ [n] }
184 else ps)
185 return t
187-- Hmmm. YAGNI?
188regret :: RunTactic
189regret = undefined
191exact :: Raw -> RunTactic
192exact guess ctxt env (Bind x (Hole ty) sc) =
193 do (val, valty) <- lift $ check ctxt env guess
194 lift $ converts ctxt env valty ty
195 return $ Bind x (Guess ty val) sc
196exact _ _ _ _ = fail "Can't fill here."
198-- As exact, but attempts to solve other goals by unification
200fill :: Raw -> RunTactic
201fill guess ctxt env (Bind x (Hole ty) sc) =
202 do (val, valty) <- lift $ check ctxt env guess
203 ns <- lift $ unify ctxt env valty ty
204 ps <- get
205 let (uh, uns) = unified ps
206 put (ps { unified = (uh, uns ++ ns) })
207-- addLog (show (uh, uns ++ ns))
208 return $ Bind x (Guess ty val) sc
209fill _ _ _ _ = fail "Can't fill here."
211solve :: RunTactic
212solve ctxt env (Bind x (Guess ty val) sc)
213 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
214 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
215 | otherwise = fail "I see a hole in your solution."
216solve _ _ _ = fail "Not a guess."
218intro :: Name -> RunTactic
219intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
220 do let t' = normalise ctxt env t
221 case t' of
222 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
223 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
224 _ -> fail "Nothing to introduce"
225intro ctxt env _ _ = fail "Can't introduce here."
227forall :: Name -> Raw -> RunTactic
228forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
229 do (tyv, tyt) <- lift $ check ctxt env ty
230 lift $ isSet ctxt env tyt
231 lift $ isSet ctxt env t
232 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
234patvar :: Name -> RunTactic
235patvar n ctxt env (Bind x (Hole t) sc) =
236 do action (\ps -> ps { holes = holes ps \\ [x] })
237 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
239compute :: RunTactic
240compute ctxt env (Bind x (Hole ty) sc) =
241 do return $ Bind x (Hole (normalise ctxt env ty)) sc
243check_in :: Raw -> RunTactic
244check_in t ctxt env tm =
245 do (val, valty) <- lift $ check ctxt env t
246 addLog (showEnv env val ++ " : " ++ showEnv env valty)
247 return tm
249eval_in :: Raw -> RunTactic
250eval_in t ctxt env tm =
251 do (val, valty) <- lift $ check ctxt env t
252 let val' = normalise ctxt env val
253 let valty' = normalise ctxt env valty
254 addLog (showEnv env val ++ " : " ++
255 showEnv env valty ++
256-- " in " ++ show env ++
257 " ==>\n " ++
258 showEnv env val' ++ " : " ++
259 showEnv env valty')
260 return tm
262start_unify :: Name -> RunTactic
263start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
264 return tm
266solve_unified :: RunTactic
267solve_unified ctxt env tm =
268 do ps <- get
269 let (_, ns) = unified ps
270 action (\ps -> ps { holes = holes ps \\ map fst ns })
271-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
272 return (updateSolved ns tm)
273 where
274 updateSolved xs (Bind n (Hole ty) t)
275 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
276 updateSolved xs (Bind n b t)
277 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
278 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
279 updateSolved xs (P _ n _)
280 | Just v <- lookup n xs = v
281 updateSolved xs t = t
283-- shuffleHoles :: Term -> Term
284-- shuffleHoles tm = shuffle [] tm
285-- where
286-- shuffle ns (Bind n b sc)
287-- |
289processTactic :: Tactic -> ProofState -> TC (ProofState, String)
290processTactic QED ps = case holes ps of
291 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
292 (tm', ty') <- recheck (context ps) [] tm
293 return (ps { done = True, pterm = tm' },
294 "Proof complete: " ++ showEnv [] tm')
295 _ -> Error "Still holes to fill."
296processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
297processTactic Undo ps = case previous ps of
298 Nothing -> Error "Nothing to undo."
299 Just pold -> return (pold, "")
300processTactic EndUnify ps = let (h, ns) = unified ps
301 tm' = updateSolved ns (pterm ps) in
302 return (ps { pterm = tm',
303 unified = (h, []),
304 holes = holes ps \\ map fst ns }, "")
305 where
306 updateSolved xs (Bind n (Hole ty) t)
307 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
308 updateSolved xs (Bind n b t)
309 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
310 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
311 updateSolved xs (P _ n _)
312 | Just v <- lookup n xs = v
313 updateSolved xs t = t
314processTactic t ps
315 = case holes ps of
316 [] -> Error "Nothing to fill in."
317 (h:_) -> do let n = nextname ps
318 ps' <- execStateT (process t h) ps
319 return (ps' { previous = Just ps, plog = "" }, plog ps')
321process :: Tactic -> Name -> StateT TState TC ()
322process EndUnify _
323 = do ps <- get
324 let (h, _) = unified ps
325 tactic (Just h) solve_unified
326process t h = tactic (Just h) (mktac t)
327 where mktac Attack = attack
328 mktac (Claim n r) = claim n r
329 mktac (Exact r) = exact r
330 mktac (Fill r) = fill r
331 mktac Regret = regret
332 mktac Solve = solve
333 mktac (StartUnify n) = start_unify n
334 mktac Compute = compute
335 mktac (Intro n) = intro n
336 mktac (Forall n t) = forall n t
337 mktac (PatVar n) = patvar n
338 mktac (CheckIn r) = check_in r
339 mktac (EvalIn r) = eval_in r
340 mktac (Focus n) = focus n
341 mktac (MoveLast n) = movelast n