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