git.iko.soy/Idris-dev
on e4cefe8 help sign in
Idris-dev/src/Core/ProofState.hs
520 lines 21 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(..), Goal(..), 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 solved :: Maybe (Name, Term),
27 problems :: Fails,
28 injective :: [(Term, Term, Term)],
29 deferred :: [Name], -- names we'll need to define
30 instances :: [Name], -- instance arguments (for type classes)
31 previous :: Maybe ProofState, -- for undo
32 context :: Context,
33 plog :: String,
34 done :: Bool
35 }
37data Goal = GD { premises :: Env,
38 goalType :: Binder Term
39 }
41data Tactic = Attack
42 | Claim Name Raw
43 | Reorder Name
44 | Exact Raw
45 | Fill Raw
46 | PrepFill Name [Name]
47 | CompleteFill
48 | Regret
49 | Solve
50 | StartUnify Name
51 | EndUnify
52 | Compute
53 | EvalIn Raw
54 | CheckIn Raw
55 | Intro (Maybe Name)
56 | IntroTy Raw (Maybe Name)
57 | Forall Name Raw
58 | LetBind Name Raw Raw
59 | Rewrite Raw
60 | PatVar Name
61 | PatBind Name
62 | Focus Name
63 | Defer Name
64 | Instance Name
65 | MoveLast Name
66 | ProofState
67 | Undo
68 | QED
69 deriving Show
71-- Some utilites on proof and tactic states
73instance Show ProofState where
74 show (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
75 show (PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _)
76 = let OK g = goal (Just h) tm
77 wkenv = premises g in
78 "Other goals: " ++ show hs ++ "\n" ++
79 showPs wkenv (reverse wkenv) ++ "\n" ++
80 "-------------------------------- (" ++ show nm ++
81 ") -------\n " ++
82 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
83 where showPs env [] = ""
84 showPs env ((n, Let t v):bs)
85 = " " ++ show n ++ " : " ++
86 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
87 showEnv env ({- normalise ctxt env -} v) ++
88 "\n" ++ showPs env bs
89 showPs env ((n, b):bs)
90 = " " ++ show n ++ " : " ++
91 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
92 "\n" ++ showPs env bs
93 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
94 " =?= " ++ showEnv ps v
95 showG ps b = showEnv ps (binderTy b)
97same Nothing n = True
98same (Just x) n = x == n
100hole (Hole _) = True
101hole (Guess _ _) = True
102hole _ = False
104holeName i = MN i "hole"
106unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
107unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy
108 addInj inj
109 case fails of
110 [] -> return u
111 err ->
112 do ps <- get
113 put (ps { problems = err ++ problems ps })
114 return []
116getName :: Monad m => String -> StateT TState m Name
117getName tag = do ps <- get
118 let n = nextname ps
119 put (ps { nextname = n+1 })
120 return $ MN n tag
122action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
123action a = do ps <- get
124 put (a ps)
126addLog :: Monad m => String -> StateT TState m ()
127addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
129newProof :: Name -> Context -> Type -> ProofState
130newProof n ctxt ty = let h = holeName 0
131 ty' = vToP ty in
132 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])
133 Nothing [] []
134 [] []
135 Nothing ctxt "" False
137type TState = ProofState -- [TacticAction])
138type RunTactic = Context -> Env -> Term -> StateT TState TC Term
139type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
141envAtFocus :: ProofState -> TC Env
142envAtFocus ps
143 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
144 return (premises g)
145 | otherwise = fail "No holes"
147goalAtFocus :: ProofState -> TC (Binder Type)
148goalAtFocus ps
149 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
150 return (goalType g)
152goal :: Hole -> Term -> TC Goal
153goal h tm = g [] tm where
154 g env (Bind n b sc) | hole b && same h n = return $ GD env b
155 | otherwise
156 = gb env b `mplus` g ((n, b):env) sc
157 g env (App f a) = g env f `mplus` g env a
158 g env t = fail "Can't find hole"
160 gb env (Let t v) = g env t `mplus` g env v
161 gb env (Guess t v) = g env t `mplus` g env v
162 gb env t = g env (binderTy t)
164tactic :: Hole -> RunTactic -> StateT TState TC ()
165tactic h f = do ps <- get
166 tm' <- atH (context ps) [] (pterm ps)
167 ps <- get -- might have changed while processing
168 put (ps { pterm = tm' })
169 where
170 atH c env binder@(Bind n b sc)
171 | hole b && same h n = f c env binder
172 | otherwise
173 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
174 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
175 atH c env t = return t
177 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
178 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
179 atHb c env t = do ty' <- atH c env (binderTy t)
180 return $ t { binderTy = ty' }
182attack :: RunTactic
183attack ctxt env (Bind x (Hole t) sc)
184 = do h <- getName "hole"
185 action (\ps -> ps { holes = h : holes ps })
186 return $ Bind x (Guess t (newtm h)) sc
187 where
188 newtm h = Bind h (Hole t) (P Bound h t)
189attack ctxt env _ = fail "Not an attackable hole"
191claim :: Name -> Raw -> RunTactic
192claim n ty ctxt env t =
193 do (tyv, tyt) <- lift $ check ctxt env ty
194 lift $ isSet ctxt env tyt
195 action (\ps -> let (g:gs) = holes ps in
196 ps { holes = g : n : gs } )
197 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
199reorder_claims :: RunTactic
200reorder_claims ctxt env t
201 = -- trace (showSep "\n" (map show (scvs t))) $
202 let (bs, sc) = scvs t []
203 newbs = reverse (sortB (reverse bs)) in
204 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
205 return (bindAll newbs sc)
206 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
207 scvs sc acc = (reverse acc, sc)
209 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
210 sortB [] = []
211 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
212 | otherwise = sortB (insertB x xs)
214 insertB x [] = [x]
215 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
216 | otherwise = y : insertB x ys
218 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
219 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
220 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
222focus :: Name -> RunTactic
223focus n ctxt env t = do action (\ps -> let hs = holes ps in
224 if n `elem` hs
225 then ps { holes = n : (hs \\ [n]) }
226 else ps)
227 return t
229movelast :: Name -> RunTactic
230movelast n ctxt env t = do action (\ps -> let hs = holes ps in
231 if n `elem` hs
232 then ps { holes = (hs \\ [n]) ++ [n] }
233 else ps)
234 return t
236instanceArg :: Name -> RunTactic
237instanceArg n ctxt env (Bind x (Hole t) sc)
238 = do action (\ps -> let hs = holes ps
239 is = instances ps in
240 ps { holes = (hs \\ [x]) ++ [x],
241 instances = x:is })
242 return (Bind x (Hole t) sc)
244defer :: Name -> RunTactic
245defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
246 do action (\ps -> let hs = holes ps in
247 ps { holes = hs \\ [x] })
248 return (Bind n (GHole (mkTy (reverse env) t))
249 (mkApp (P Ref n ty) (map getP (reverse env))))
250 where
251 mkTy [] t = t
252 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
254 getP (n, b) = P Bound n (binderTy b)
256-- Hmmm. YAGNI?
257regret :: RunTactic
258regret = undefined
260addInj :: [(Term, Term, Term)] -> StateT TState TC ()
261addInj inj = do ps <- get
262 put (ps { injective = inj ++ injective ps })
264exact :: Raw -> RunTactic
265exact guess ctxt env (Bind x (Hole ty) sc) =
266 do (val, valty) <- lift $ check ctxt env guess
267 lift $ converts ctxt env valty ty
268 return $ Bind x (Guess ty val) sc
269exact _ _ _ _ = fail "Can't fill here."
271-- As exact, but attempts to solve other goals by unification
273fill :: Raw -> RunTactic
274fill guess ctxt env (Bind x (Hole ty) sc) =
275 do (val, valty) <- lift $ check ctxt env guess
276 s <- get
277 ns <- unify' ctxt env valty ty
278 ps <- get
279 let (uh, uns) = unified ps
280 put (ps { unified = (uh, uns ++ ns) })
281-- addLog (show (uh, uns ++ ns))
282 return $ Bind x (Guess ty val) sc
283fill _ _ _ _ = fail "Can't fill here."
285prep_fill :: Name -> [Name] -> RunTactic
286prep_fill f as ctxt env (Bind x (Hole ty) sc) =
287 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
288 return $ Bind x (Guess ty val) sc
289prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
291complete_fill :: RunTactic
292complete_fill ctxt env (Bind x (Guess ty val) sc) =
293 do let guess = forget val
294 (val', valty) <- lift $ check ctxt env guess
295 ns <- unify' ctxt env valty ty
296 ps <- get
297 let (uh, uns) = unified ps
298 put (ps { unified = (uh, uns ++ ns) })
299 return $ Bind x (Guess ty val) sc
300complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
302solve :: RunTactic
303solve ctxt env (Bind x (Guess ty val) sc)
304 | pureTerm val = do ps <- get
305 let (uh, uns) = unified ps
306 action (\ps -> ps { holes = holes ps \\ [x],
307 solved = Just (x, val),
308 -- unified = (uh, uns ++ [(x, val)]),
309 instances = instances ps \\ [x] })
310 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
311 | otherwise = lift $ tfail $ IncompleteTerm val
312solve _ _ h = fail $ "Not a guess " ++ show h
314introTy :: Raw -> Maybe Name -> RunTactic
315introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
316 do let n = case mn of
317 Just name -> name
318 Nothing -> x
319 let t' = normalise ctxt env t
320 (tyv, tyt) <- lift $ check ctxt env ty
321-- ns <- lift $ unify ctxt env tyv t'
322 case t' of
323 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
324 do ns <- unify' ctxt env s tyv
325 ps <- get
326 let (uh, uns) = unified ps
327 put (ps { unified = (uh, uns ++ ns) })
328 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
329 _ -> fail "Nothing to introduce"
330introTy ty n ctxt env _ = fail "Can't introduce here."
332intro :: Maybe Name -> RunTactic
333intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
334 do let n = case mn of
335 Just name -> name
336 Nothing -> x
337 let t' = normalise ctxt env t
338 case t' of
339 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
340 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
341 _ -> fail "Nothing to introduce"
342intro n ctxt env _ = fail "Can't introduce here."
344forall :: Name -> Raw -> RunTactic
345forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
346 do (tyv, tyt) <- lift $ check ctxt env ty
347 lift $ isSet ctxt env tyt
348 lift $ isSet ctxt env t
349 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
350forall n ty ctxt env _ = fail "Can't pi bind here"
352patvar :: Name -> RunTactic
353patvar n ctxt env (Bind x (Hole t) sc) =
354 do action (\ps -> ps { holes = holes ps \\ [x] })
355 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
356patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
358letbind :: Name -> Raw -> Raw -> RunTactic
359letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
360 do (tyv, tyt) <- lift $ check ctxt env ty
361 (valv, valt) <- lift $ check ctxt env val
362 lift $ isSet ctxt env tyt
363 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
364letbind n ty val ctxt env _ = fail "Can't let bind here"
366rewrite :: Raw -> RunTactic
367rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
368 do (tmv, tmt) <- lift $ check ctxt env tm
369 case unApply tmt of
370 (P _ (UN "=") _, [lt,rt,l,r]) ->
371 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
372 let newt = mkP l r l t
373 let sc = forget $ (Bind x (Hole newt)
374 (mkApp (P Ref (UN "replace") (Set (UVal 0)))
375 [lt, l, r, p, tmv, xp]))
376 (scv, sct) <- lift $ check ctxt env sc
377 return scv
378 _ -> fail "Not an equality type"
379 where
380 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
381 -- and x, and put \x : lt in front
382 mkP lt l r ty | l == ty = lt
383 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
384 a' = if (r /= a) then mkP lt l r a else a in
385 App f' a'
386 mkP lt l r x = x
388 rname = MN 0 "replaced"
389rewrite _ _ _ _ = fail "Can't rewrite here"
391patbind :: Name -> RunTactic
392patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
393 do let t' = normalise ctxt env t
394 case t' of
395 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
396 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
397 _ -> fail "Nothing to pattern bind"
398patbind n ctxt env _ = fail "Can't pattern bind here"
400compute :: RunTactic
401compute ctxt env (Bind x (Hole ty) sc) =
402 do return $ Bind x (Hole (normalise ctxt env ty)) sc
404check_in :: Raw -> RunTactic
405check_in t ctxt env tm =
406 do (val, valty) <- lift $ check ctxt env t
407 addLog (showEnv env val ++ " : " ++ showEnv env valty)
408 return tm
410eval_in :: Raw -> RunTactic
411eval_in t ctxt env tm =
412 do (val, valty) <- lift $ check ctxt env t
413 let val' = normalise ctxt env val
414 let valty' = normalise ctxt env valty
415 addLog (showEnv env val ++ " : " ++
416 showEnv env valty ++
417-- " in " ++ show env ++
418 " ==>\n " ++
419 showEnv env val' ++ " : " ++
420 showEnv env valty')
421 return tm
423start_unify :: Name -> RunTactic
424start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
425 return tm
427tmap f (a, b, c) = (f a, b, c)
429solve_unified :: RunTactic
430solve_unified ctxt env tm =
431 do ps <- get
432 let (_, ns) = unified ps
433 action (\ps -> ps { holes = holes ps \\ map fst ns })
434 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
435 action (\ps -> ps { injective = map (tmap (updateSolved ns)) (injective ps) })
436 return (updateSolved ns tm)
438updateSolved xs (Bind n (Hole ty) t)
439 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
440updateSolved xs (Bind n b t)
441 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
442updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
443updateSolved xs (P _ n _)
444 | Just v <- lookup n xs = v
445updateSolved xs t = t
447updateProblems ns [] = []
448updateProblems ns ((x, y, env, err) : ps) =
449 let x' = updateSolved ns x
450 y' = updateSolved ns y in
451 (x',y',env,err) : updateProblems ns ps
453processTactic :: Tactic -> ProofState -> TC (ProofState, String)
454processTactic QED ps = case holes ps of
455 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
456 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
457 return (ps { done = True, pterm = tm' },
458 "Proof complete: " ++ showEnv [] tm')
459 _ -> fail "Still holes to fill."
460processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
461processTactic Undo ps = case previous ps of
462 Nothing -> fail "Nothing to undo."
463 Just pold -> return (pold, "")
464processTactic EndUnify ps
465 = let (h, ns) = unified ps
466 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
467 tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $
468 updateSolved ns' (pterm ps)
469 probs' = updateProblems ns' (problems ps) in
470 case probs' of
471 [] -> return (ps { pterm = tm',
472 unified = (h, []),
473 injective = map (tmap (updateSolved ns'))
474 (injective ps),
475 holes = holes ps \\ map fst ns' }, "")
476 errs@((_,_,_,err):_) -> tfail err
477processTactic (Reorder n) ps
478 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
479 return (ps' { previous = Just ps, plog = "" }, plog ps')
480processTactic t ps
481 = case holes ps of
482 [] -> fail "Nothing to fill in."
483 (h:_) -> do ps' <- execStateT (process t h) ps
484 let pterm' = case solved ps' of
485 Just s -> updateSolved [s] (pterm ps')
486 _ -> pterm ps'
487 return (ps' { pterm = pterm',
488 solved = Nothing,
489 previous = Just ps, plog = "" }, plog ps')
491process :: Tactic -> Name -> StateT TState TC ()
492process EndUnify _
493 = do ps <- get
494 let (h, _) = unified ps
495 tactic (Just h) solve_unified
496process t h = tactic (Just h) (mktac t)
497 where mktac Attack = attack
498 mktac (Claim n r) = claim n r
499 mktac (Exact r) = exact r
500 mktac (Fill r) = fill r
501 mktac (PrepFill n ns) = prep_fill n ns
502 mktac CompleteFill = complete_fill
503 mktac Regret = regret
504 mktac Solve = solve
505 mktac (StartUnify n) = start_unify n
506 mktac Compute = compute
507 mktac (Intro n) = intro n
508 mktac (IntroTy ty n) = introTy ty n
509 mktac (Forall n t) = forall n t
510 mktac (LetBind n t v) = letbind n t v
511 mktac (Rewrite t) = rewrite t
512 mktac (PatVar n) = patvar n
513 mktac (PatBind n) = patbind n
514 mktac (CheckIn r) = check_in r
515 mktac (EvalIn r) = eval_in r
516 mktac (Focus n) = focus n
517 mktac (Defer n) = defer n
518 mktac (Instance n) = instanceArg n
519 mktac (MoveLast n) = movelast n