git.iko.soy/Idris-dev
on 35ec145 help sign in
Idris-dev/src/Core/ProofState.hs
567 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)
297regret :: RunTactic
298regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
299 do action (\ps -> let hs = holes ps in
300 ps { holes = hs \\ [x] })
301 return sc
302regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
304addInj :: [(Term, Term, Term)] -> StateT TState TC ()
305addInj inj = do ps <- get
306 put (ps { injective = inj ++ injective ps })
308exact :: Raw -> RunTactic
309exact guess ctxt env (Bind x (Hole ty) sc) =
310 do (val, valty) <- lift $ check ctxt env guess
311 lift $ converts ctxt env valty ty
312 return $ Bind x (Guess ty val) sc
313exact _ _ _ _ = fail "Can't fill here."
315-- As exact, but attempts to solve other goals by unification
317fill :: Raw -> RunTactic
318fill guess ctxt env (Bind x (Hole ty) sc) =
319 do (val, valty) <- lift $ check ctxt env guess
320 s <- get
321-- let valtyn = normalise ctxt env valty
322-- let tyn = normalise ctxt env ty
323 ns <- unify' ctxt env valty ty
324 ps <- get
325 let (uh, uns) = unified ps
326 put (ps { unified = (uh, uns ++ ns) })
327-- addLog (show (uh, uns ++ ns))
328 return $ Bind x (Guess ty val) sc
329fill _ _ _ _ = fail "Can't fill here."
331prep_fill :: Name -> [Name] -> RunTactic
332prep_fill f as ctxt env (Bind x (Hole ty) sc) =
333 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
334 return $ Bind x (Guess ty val) sc
335prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
337complete_fill :: RunTactic
338complete_fill ctxt env (Bind x (Guess ty val) sc) =
339 do let guess = forget val
340 (val', valty) <- lift $ check ctxt env guess
341 ns <- unify' ctxt env valty ty
342 ps <- get
343 let (uh, uns) = unified ps
344 put (ps { unified = (uh, uns ++ ns) })
345 return $ Bind x (Guess ty val) sc
346complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
348solve :: RunTactic
349solve ctxt env (Bind x (Guess ty val) sc)
350 | pureTerm val = do ps <- get
351 let (uh, uns) = unified ps
352 action (\ps -> ps { holes = holes ps \\ [x],
353 solved = Just (x, val),
354 -- unified = (uh, uns ++ [(x, val)]),
355 instances = instances ps \\ [x] })
356 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
357 | otherwise = lift $ tfail $ IncompleteTerm val
358solve _ _ h = fail $ "Not a guess " ++ show h
360introTy :: Raw -> Maybe Name -> RunTactic
361introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
362 do let n = case mn of
363 Just name -> name
364 Nothing -> x
365 let t' = normalise ctxt env t
366 (tyv, tyt) <- lift $ check ctxt env ty
367-- ns <- lift $ unify ctxt env tyv t'
368 case t' of
369 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
370 do ns <- unify' ctxt env s tyv
371 ps <- get
372 let (uh, uns) = unified ps
373 put (ps { unified = (uh, uns ++ ns) })
374 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
375 _ -> fail "Nothing to introduce"
376introTy ty n ctxt env _ = fail "Can't introduce here."
378intro :: Maybe Name -> RunTactic
379intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
380 do let n = case mn of
381 Just name -> name
382 Nothing -> x
383 let t' = normalise ctxt env t
384 case t' of
385 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
386 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
387 _ -> fail "Nothing to introduce"
388intro n ctxt env _ = fail "Can't introduce here."
390forall :: Name -> Raw -> RunTactic
391forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
392 do (tyv, tyt) <- lift $ check ctxt env ty
393 lift $ isSet ctxt env tyt
394 lift $ isSet ctxt env t
395 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
396forall n ty ctxt env _ = fail "Can't pi bind here"
398patvar :: Name -> RunTactic
399patvar n ctxt env (Bind x (Hole t) sc) =
400 do action (\ps -> ps { holes = holes ps \\ [x] })
401 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
402patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
404letbind :: Name -> Raw -> Raw -> RunTactic
405letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
406 do (tyv, tyt) <- lift $ check ctxt env ty
407 (valv, valt) <- lift $ check ctxt env val
408 lift $ isSet ctxt env tyt
409 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
410letbind n ty val ctxt env _ = fail "Can't let bind here"
412rewrite :: Raw -> RunTactic
413rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
414 do (tmv, tmt) <- lift $ check ctxt env tm
415 let tmt' = normalise ctxt env tmt
416 case unApply tmt' of
417 (P _ (UN "=") _, [lt,rt,l,r]) ->
418 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
419 let newt = mkP l r l t
420 let sc = forget $ (Bind x (Hole newt)
421 (mkApp (P Ref (UN "replace") (Set (UVal 0)))
422 [lt, l, r, p, tmv, xp]))
423 (scv, sct) <- lift $ check ctxt env sc
424 return scv
425 _ -> fail "Not an equality type"
426 where
427 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
428 -- and x, and put \x : lt in front
429 mkP lt l r ty | l == ty = lt
430 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
431 a' = if (r /= a) then mkP lt l r a else a in
432 App f' a'
433 mkP lt l r x = x
435 rname = MN 0 "replaced"
436rewrite _ _ _ _ = fail "Can't rewrite here"
438patbind :: Name -> RunTactic
439patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
440 do let t' = normalise ctxt env t
441 case t' of
442 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
443 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
444 _ -> fail "Nothing to pattern bind"
445patbind n ctxt env _ = fail "Can't pattern bind here"
447compute :: RunTactic
448compute ctxt env (Bind x (Hole ty) sc) =
449 do return $ Bind x (Hole (normalise ctxt env ty)) sc
451check_in :: Raw -> RunTactic
452check_in t ctxt env tm =
453 do (val, valty) <- lift $ check ctxt env t
454 addLog (showEnv env val ++ " : " ++ showEnv env valty)
455 return tm
457eval_in :: Raw -> RunTactic
458eval_in t ctxt env tm =
459 do (val, valty) <- lift $ check ctxt env t
460 let val' = normalise ctxt env val
461 let valty' = normalise ctxt env valty
462 addLog (showEnv env val ++ " : " ++
463 showEnv env valty ++
464-- " in " ++ show env ++
465 " ==>\n " ++
466 showEnv env val' ++ " : " ++
467 showEnv env valty')
468 return tm
470start_unify :: Name -> RunTactic
471start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
472 return tm
474tmap f (a, b, c) = (f a, b, c)
476solve_unified :: RunTactic
477solve_unified ctxt env tm =
478 do ps <- get
479 let (_, ns) = unified ps
480 action (\ps -> ps { holes = holes ps \\ map fst ns })
481 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
482 action (\ps -> ps { injective = map (tmap (updateSolved ns)) (injective ps) })
483 return (updateSolved ns tm)
485updateSolved xs (Bind n (Hole ty) t)
486 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
487updateSolved xs (Bind n b t)
488 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
489updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
490updateSolved xs (P _ n _)
491 | Just v <- lookup n xs = v
492updateSolved xs t = t
494updateProblems ns [] = []
495updateProblems ns ((x, y, env, err) : ps) =
496 let x' = updateSolved ns x
497 y' = updateSolved ns y in
498 (x',y',env,err) : updateProblems ns ps
500processTactic :: Tactic -> ProofState -> TC (ProofState, String)
501processTactic QED ps = case holes ps of
502 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
503 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
504 return (ps { done = True, pterm = tm' },
505 "Proof complete: " ++ showEnv [] tm')
506 _ -> fail "Still holes to fill."
507processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
508processTactic Undo ps = case previous ps of
509 Nothing -> fail "Nothing to undo."
510 Just pold -> return (pold, "")
511processTactic EndUnify ps
512 = let (h, ns) = unified ps
513 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
514 tm' = -- trace ("Updating " ++ show ns' ++ " in " ++ show (pterm ps)) $
515 updateSolved ns' (pterm ps)
516 probs' = updateProblems ns' (problems ps) in
517 case probs' of
518 [] -> return (ps { pterm = tm',
519 unified = (h, []),
520 injective = map (tmap (updateSolved ns'))
521 (injective ps),
522 holes = holes ps \\ map fst ns' }, "")
523 errs@((_,_,_,err):_) -> tfail err
524processTactic (Reorder n) ps
525 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
526 return (ps' { previous = Just ps, plog = "" }, plog ps')
527processTactic t ps
528 = case holes ps of
529 [] -> fail "Nothing to fill in."
530 (h:_) -> do ps' <- execStateT (process t h) ps
531 let pterm' = case solved ps' of
532 Just s -> updateSolved [s] (pterm ps')
533 _ -> pterm ps'
534 return (ps' { pterm = pterm',
535 solved = Nothing,
536 previous = Just ps, plog = "" }, plog ps')
538process :: Tactic -> Name -> StateT TState TC ()
539process EndUnify _
540 = do ps <- get
541 let (h, _) = unified ps
542 tactic (Just h) solve_unified
543process t h = tactic (Just h) (mktac t)
544 where mktac Attack = attack
545 mktac (Claim n r) = claim n r
546 mktac (Exact r) = exact r
547 mktac (Fill r) = fill r
548 mktac (PrepFill n ns) = prep_fill n ns
549 mktac CompleteFill = complete_fill
550 mktac Regret = regret
551 mktac Solve = solve
552 mktac (StartUnify n) = start_unify n
553 mktac Compute = compute
554 mktac (Intro n) = intro n
555 mktac (IntroTy ty n) = introTy ty n
556 mktac (Forall n t) = forall n t
557 mktac (LetBind n t v) = letbind n t v
558 mktac (Rewrite t) = rewrite t
559 mktac (PatVar n) = patvar n
560 mktac (PatBind n) = patbind n
561 mktac (CheckIn r) = check_in r
562 mktac (EvalIn r) = eval_in r
563 mktac (Focus n) = focus n
564 mktac (Defer n) = defer n
565 mktac (Instance n) = instanceArg n
566 mktac (MoveLast n) = movelast n