git.iko.soy/Idris-dev
on e4fc71a help sign in
Idris-dev/src/Core/ProofState.hs
705 lines 30 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,
9 dropGiven, keepGiven) where
11import Core.Typecheck
12import Core.Evaluate
13import Core.TT
14import Core.Unify
16import Control.Monad.State
17import Control.Applicative hiding (empty)
18import Data.List
19import Debug.Trace
21import Util.Pretty
23data ProofState = PS { thname :: Name,
24 holes :: [Name], -- holes still to be solved
25 usedns :: [Name], -- used names, don't use again
26 nextname :: Int, -- name supply
27 pterm :: Term, -- current proof term
28 ptype :: Type, -- original goal
29 dontunify :: [Name], -- explicitly given by programmer, leave it
30 unified :: (Name, [(Name, Term)]),
31 notunified :: [(Name, Term)],
32 solved :: Maybe (Name, Term),
33 problems :: Fails,
34 injective :: [Name],
35 deferred :: [Name], -- names we'll need to define
36 instances :: [Name], -- instance arguments (for type classes)
37 previous :: Maybe ProofState, -- for undo
38 context :: Context,
39 plog :: String,
40 done :: Bool
41 }
43data Goal = GD { premises :: Env,
44 goalType :: Binder Term
45 }
47data Tactic = Attack
48 | Claim Name Raw
49 | Reorder Name
50 | Exact Raw
51 | Fill Raw
52 | PrepFill Name [Name]
53 | CompleteFill
54 | Regret
55 | Solve
56 | StartUnify Name
57 | EndUnify
58 | Compute
59 | HNF_Compute
60 | EvalIn Raw
61 | CheckIn Raw
62 | Intro (Maybe Name)
63 | IntroTy Raw (Maybe Name)
64 | Forall Name Raw
65 | LetBind Name Raw Raw
66 | Rewrite Raw
67 | PatVar Name
68 | PatBind Name
69 | Focus Name
70 | Defer Name
71 | DeferType Name Raw [Name]
72 | Instance Name
73 | SetInjective Name
74 | MoveLast Name
75 | ProofState
76 | Undo
77 | QED
78 deriving Show
80-- Some utilites on proof and tactic states
82instance Show ProofState where
83 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
84 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _)
85 = let OK g = goal (Just h) tm
86 wkenv = premises g in
87 "Other goals: " ++ show hs ++ "\n" ++
88 showPs wkenv (reverse wkenv) ++ "\n" ++
89 "-------------------------------- (" ++ show nm ++
90 ") -------\n " ++
91 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
92 where showPs env [] = ""
93 showPs env ((n, Let t v):bs)
94 = " " ++ show n ++ " : " ++
95 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
96 showEnv env ({- normalise ctxt env -} v) ++
97 "\n" ++ showPs env bs
98 showPs env ((n, b):bs)
99 = " " ++ show n ++ " : " ++
100 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
101 "\n" ++ showPs env bs
102 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
103 " =?= " ++ showEnv ps v
104 showG ps b = showEnv ps (binderTy b)
106instance Pretty ProofState where
107 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _) =
108 if size nm > breakingSize then
109 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
110 else
111 pretty nm <> colon <+> text " no more goals."
112 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _) =
113 let OK g = goal (Just h) tm in
114 let wkEnv = premises g in
115 text "Other goals" <+> colon <+> pretty hs $$
116 prettyPs wkEnv (reverse wkEnv) $$
117 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
118 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
119 where
120 prettyGoal ps (Guess t v) =
121 if size v > breakingSize then
122 prettyEnv ps t <+> text "=?=" $$
123 nest nestingSize (prettyEnv ps v)
124 else
125 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
126 prettyGoal ps b = prettyEnv ps $ binderTy b
128 prettyPs env [] = empty
129 prettyPs env ((n, Let t v):bs) =
130 nest nestingSize (pretty n <+> colon <+>
131 if size v > breakingSize then
132 prettyEnv env t <+> text "=" $$
133 nest nestingSize (prettyEnv env v) $$
134 nest nestingSize (prettyPs env bs)
135 else
136 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
137 nest nestingSize (prettyPs env bs))
138 prettyPs env ((n, b):bs) =
139 if size (binderTy b) > breakingSize then
140 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
141 else
142 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
143 nest nestingSize (prettyPs env bs))
145same Nothing n = True
146same (Just x) n = x == n
148hole (Hole _) = True
149hole (Guess _ _) = True
150hole _ = False
152holeName i = MN i "hole"
154qshow :: Fails -> String
155qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
157unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
158unify' ctxt env topx topy =
159 do ps <- get
160 let dont = dontunify ps
161 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $
162 lift $ unify ctxt env topx topy dont (holes ps)
163-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
164-- -- " in " ++ show env ++
165-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
166-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
167-- ++ show (pterm ps)
168-- ++ "\n----------") $
169 case fails of
170-- [] -> return u
171 err ->
172 do ps <- get
173 let (h, ns) = unified ps
174 let (ns', probs') = updateProblems (context ps) (u ++ ns)
175 (err ++ problems ps)
176 (injective ps)
177 (holes ps)
178 put (ps { problems = probs',
179 unified = (h, ns') })
180 return u
182getName :: Monad m => String -> StateT TState m Name
183getName tag = do ps <- get
184 let n = nextname ps
185 put (ps { nextname = n+1 })
186 return $ MN n tag
188action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
189action a = do ps <- get
190 put (a ps)
192addLog :: Monad m => String -> StateT TState m ()
193addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
195newProof :: Name -> Context -> Type -> ProofState
196newProof n ctxt ty = let h = holeName 0
197 ty' = vToP ty in
198 PS n [h] [] 1 (Bind h (Hole ty')
199 (P Bound h ty')) ty [] (h, []) []
200 Nothing [] []
201 [] []
202 Nothing ctxt "" False
204type TState = ProofState -- [TacticAction])
205type RunTactic = Context -> Env -> Term -> StateT TState TC Term
206type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
208envAtFocus :: ProofState -> TC Env
209envAtFocus ps
210 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
211 return (premises g)
212 | otherwise = fail "No holes"
214goalAtFocus :: ProofState -> TC (Binder Type)
215goalAtFocus ps
216 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
217 return (goalType g)
218 | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
220goal :: Hole -> Term -> TC Goal
221goal h tm = g [] tm where
222 g env (Bind n b sc) | hole b && same h n = return $ GD env b
223 | otherwise
224 = gb env b `mplus` g ((n, b):env) sc
225 g env (App f a) = g env f `mplus` g env a
226 g env t = fail "Can't find hole"
228 gb env (Let t v) = g env t `mplus` g env v
229 gb env (Guess t v) = g env t `mplus` g env v
230 gb env t = g env (binderTy t)
232tactic :: Hole -> RunTactic -> StateT TState TC ()
233tactic h f = do ps <- get
234 tm' <- atH (context ps) [] (pterm ps)
235 ps <- get -- might have changed while processing
236 put (ps { pterm = tm' })
237 where
238 atH c env binder@(Bind n b sc)
239 | hole b && same h n = f c env binder
240 | otherwise
241 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
242 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
243 atH c env t = return t
245 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
246 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
247 atHb c env t = do ty' <- atH c env (binderTy t)
248 return $ t { binderTy = ty' }
250attack :: RunTactic
251attack ctxt env (Bind x (Hole t) sc)
252 = do h <- getName "hole"
253 action (\ps -> ps { holes = h : holes ps })
254 return $ Bind x (Guess t (newtm h)) sc
255 where
256 newtm h = Bind h (Hole t) (P Bound h t)
257attack ctxt env _ = fail "Not an attackable hole"
259claim :: Name -> Raw -> RunTactic
260claim n ty ctxt env t =
261 do (tyv, tyt) <- lift $ check ctxt env ty
262 lift $ isType ctxt env tyt
263 action (\ps -> let (g:gs) = holes ps in
264 ps { holes = g : n : gs } )
265 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
267reorder_claims :: RunTactic
268reorder_claims ctxt env t
269 = -- trace (showSep "\n" (map show (scvs t))) $
270 let (bs, sc) = scvs t []
271 newbs = reverse (sortB (reverse bs)) in
272 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
273 return (bindAll newbs sc)
274 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
275 scvs sc acc = (reverse acc, sc)
277 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
278 sortB [] = []
279 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
280 | otherwise = sortB (insertB x xs)
282 insertB x [] = [x]
283 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
284 | otherwise = y : insertB x ys
286 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
287 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
288 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
290focus :: Name -> RunTactic
291focus n ctxt env t = do action (\ps -> let hs = holes ps in
292 if n `elem` hs
293 then ps { holes = n : (hs \\ [n]) }
294 else ps)
295 ps <- get
296 return t
298movelast :: Name -> RunTactic
299movelast n ctxt env t = do action (\ps -> let hs = holes ps in
300 if n `elem` hs
301 then ps { holes = (hs \\ [n]) ++ [n] }
302 else ps)
303 return t
305instanceArg :: Name -> RunTactic
306instanceArg n ctxt env (Bind x (Hole t) sc)
307 = do action (\ps -> let hs = holes ps
308 is = instances ps in
309 ps { holes = (hs \\ [x]) ++ [x],
310 instances = x:is })
311 return (Bind x (Hole t) sc)
313setinj :: Name -> RunTactic
314setinj n ctxt env (Bind x (Hole t) sc)
315 = do action (\ps -> let is = injective ps in
316 ps { injective = n : is })
317 return (Bind x (Hole t) sc)
319defer :: Name -> RunTactic
320defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
321 do action (\ps -> let hs = holes ps in
322 ps { holes = hs \\ [x] })
323 return (Bind n (GHole (mkTy (reverse env) t))
324 (mkApp (P Ref n ty) (map getP (reverse env))))
325 where
326 mkTy [] t = t
327 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
329 getP (n, b) = P Bound n (binderTy b)
331-- as defer, but build the type and application explicitly
332deferType :: Name -> Raw -> [Name] -> RunTactic
333deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
334 do (fty, _) <- lift $ check ctxt env fty_in
335 action (\ps -> let hs = holes ps
336 ds = deferred ps in
337 ps { holes = hs \\ [x],
338 deferred = n : ds })
339 return (Bind n (GHole fty)
340 (mkApp (P Ref n ty) (map getP args)))
341 where
342 getP n = case lookup n env of
343 Just b -> P Bound n (binderTy b)
344 Nothing -> error ("deferType can't find " ++ show n)
346regret :: RunTactic
347regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
348 do action (\ps -> let hs = holes ps in
349 ps { holes = hs \\ [x] })
350 return sc
351regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
353exact :: Raw -> RunTactic
354exact guess ctxt env (Bind x (Hole ty) sc) =
355 do (val, valty) <- lift $ check ctxt env guess
356 lift $ converts ctxt env valty ty
357 return $ Bind x (Guess ty val) sc
358exact _ _ _ _ = fail "Can't fill here."
360-- As exact, but attempts to solve other goals by unification
362fill :: Raw -> RunTactic
363fill guess ctxt env (Bind x (Hole ty) sc) =
364 do (val, valty) <- lift $ check ctxt env guess
365-- let valtyn = normalise ctxt env valty
366-- let tyn = normalise ctxt env ty
367 ns <- unify' ctxt env valty ty
368 ps <- get
369 let (uh, uns) = unified ps
370-- put (ps { unified = (uh, uns ++ ns) })
371-- addLog (show (uh, uns ++ ns))
372 return $ Bind x (Guess ty val) sc
373fill _ _ _ _ = fail "Can't fill here."
375prep_fill :: Name -> [Name] -> RunTactic
376prep_fill f as ctxt env (Bind x (Hole ty) sc) =
377 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
378 return $ Bind x (Guess ty val) sc
379prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
381complete_fill :: RunTactic
382complete_fill ctxt env (Bind x (Guess ty val) sc) =
383 do let guess = forget val
384 (val', valty) <- lift $ check ctxt env guess
385 ns <- unify' ctxt env valty ty
386 ps <- get
387 let (uh, uns) = unified ps
388-- put (ps { unified = (uh, uns ++ ns) })
389 return $ Bind x (Guess ty val) sc
390complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
392-- When solving something in the 'dont unify' set, we should check
393-- that the guess we are solving it with unifies with the thing unification
394-- found for it, if anything.
396solve :: RunTactic
397solve ctxt env (Bind x (Guess ty val) sc)
398 | True = do ps <- get
399 let (uh, uns) = unified ps
400 case lookup x (notunified ps) of
401 Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $
402 -- return []
403 unify' ctxt env tm val
404 _ -> return []
405 action (\ps -> ps { holes = holes ps \\ [x],
406 solved = Just (x, val),
407-- problems = solveInProblems
408-- x val (problems ps),
409 -- dontunify = dontunify ps \\ [x],
410 -- unified = (uh, uns ++ [(x, val)]),
411 instances = instances ps \\ [x] })
412 return $ {- Bind x (Let ty val) sc -}
413 instantiate val (pToV x sc)
414 | otherwise = lift $ tfail $ IncompleteTerm val
415solve _ _ h@(Bind x t sc)
416 = do ps <- get
417 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
419introTy :: Raw -> Maybe Name -> RunTactic
420introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
421 do let n = case mn of
422 Just name -> name
423 Nothing -> x
424 let t' = case t of
425 x@(Bind y (Pi s) _) -> x
426 _ -> hnf ctxt env t
427 (tyv, tyt) <- lift $ check ctxt env ty
428-- ns <- lift $ unify ctxt env tyv t'
429 case t' of
430 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
431 do ns <- unify' ctxt env s tyv
432 ps <- get
433 let (uh, uns) = unified ps
434-- put (ps { unified = (uh, uns ++ ns) })
435 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
436 _ -> lift $ tfail $ CantIntroduce t'
437introTy ty n ctxt env _ = fail "Can't introduce here."
439intro :: Maybe Name -> RunTactic
440intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
441 do let n = case mn of
442 Just name -> name
443 Nothing -> x
444 let t' = case t of
445 x@(Bind y (Pi s) _) -> x
446 _ -> hnf ctxt env t
447 case t' of
448 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
449 let t' = instantiate (P Bound n s) (pToV y t) in
450 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
451 _ -> lift $ tfail $ CantIntroduce t'
452intro n ctxt env _ = fail "Can't introduce here."
454forall :: Name -> Raw -> RunTactic
455forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
456 do (tyv, tyt) <- lift $ check ctxt env ty
457 unify' ctxt env tyt (TType (UVar 0))
458 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
459forall n ty ctxt env _ = fail "Can't pi bind here"
461patvar :: Name -> RunTactic
462patvar n ctxt env (Bind x (Hole t) sc) =
463 do action (\ps -> ps { holes = holes ps \\ [x] })
464 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
465patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
467letbind :: Name -> Raw -> Raw -> RunTactic
468letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
469 do (tyv, tyt) <- lift $ check ctxt env ty
470 (valv, valt) <- lift $ check ctxt env val
471 lift $ isType ctxt env tyt
472 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
473letbind n ty val ctxt env _ = fail "Can't let bind here"
475rewrite :: Raw -> RunTactic
476rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
477 do (tmv, tmt) <- lift $ check ctxt env tm
478 let tmt' = normalise ctxt env tmt
479 case unApply tmt' of
480 (P _ (UN "=") _, [lt,rt,l,r]) ->
481 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
482 let newt = mkP l r l t
483 let sc = forget $ (Bind x (Hole newt)
484 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
485 [lt, l, r, p, tmv, xp]))
486 (scv, sct) <- lift $ check ctxt env sc
487 return scv
488 _ -> fail "Not an equality type"
489 where
490 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
491 -- an x, and put \x : lt in front
492 mkP lt l r ty | l == ty = lt
493 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
494 a' = if (r /= a) then mkP lt l r a else a in
495 App f' a'
496 mkP lt l r (Bind n b sc)
497 = let b' = mkPB b
498 sc' = if (r /= sc) then mkP lt l r sc else sc in
499 Bind n b' sc'
500 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
501 v' = if (r /= v) then mkP lt l r v else v in
502 Let t' v'
503 mkPB b = let ty = binderTy b
504 ty' = if (r /= ty) then mkP lt l r ty else ty in
505 b { binderTy = ty' }
506 mkP lt l r x = x
508 rname = MN 0 "replaced"
509rewrite _ _ _ _ = fail "Can't rewrite here"
511patbind :: Name -> RunTactic
512patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
513 do let t' = case t of
514 x@(Bind y (PVTy s) t) -> x
515 _ -> hnf ctxt env t
516 case t' of
517 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
518 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
519 _ -> fail "Nothing to pattern bind"
520patbind n ctxt env _ = fail "Can't pattern bind here"
522compute :: RunTactic
523compute ctxt env (Bind x (Hole ty) sc) =
524 do return $ Bind x (Hole (normalise ctxt env ty)) sc
525compute ctxt env t = return t
527hnf_compute :: RunTactic
528hnf_compute ctxt env (Bind x (Hole ty) sc) =
529 do let ty' = hnf ctxt env ty in
530-- trace ("HNF " ++ show (ty, ty')) $
531 return $ Bind x (Hole ty') sc
532hnf_compute ctxt env t = return t
534check_in :: Raw -> RunTactic
535check_in t ctxt env tm =
536 do (val, valty) <- lift $ check ctxt env t
537 addLog (showEnv env val ++ " : " ++ showEnv env valty)
538 return tm
540eval_in :: Raw -> RunTactic
541eval_in t ctxt env tm =
542 do (val, valty) <- lift $ check ctxt env t
543 let val' = normalise ctxt env val
544 let valty' = normalise ctxt env valty
545 addLog (showEnv env val ++ " : " ++
546 showEnv env valty ++
547-- " in " ++ show env ++
548 " ==>\n " ++
549 showEnv env val' ++ " : " ++
550 showEnv env valty')
551 return tm
553start_unify :: Name -> RunTactic
554start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
555 return tm
557tmap f (a, b, c) = (f a, b, c)
559solve_unified :: RunTactic
560solve_unified ctxt env tm =
561 do ps <- get
562 let (_, ns) = unified ps
563 let unify = dropGiven (dontunify ps) ns (holes ps)
564 action (\ps -> ps { holes = holes ps \\ map fst unify })
565 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
566 return (updateSolved unify tm)
567 where
569dropGiven du [] hs = []
570dropGiven du ((n, P Bound t ty) : us) hs
571 | n `elem` du && not (t `elem` du)
572 && n `elem` hs && t `elem` hs
573 = (t, P Bound n ty) : dropGiven du us hs
574dropGiven du (u@(n, _) : us) hs
575 | n `elem` du = dropGiven du us hs
576-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
577dropGiven du (u : us) hs = u : dropGiven du us hs
579keepGiven du [] hs = []
580keepGiven du ((n, P Bound t ty) : us) hs
581 | n `elem` du && not (t `elem` du)
582 && n `elem` hs && t `elem` hs
583 = keepGiven du us hs
584keepGiven du (u@(n, _) : us) hs
585 | n `elem` du = u : keepGiven du us hs
586keepGiven du (u : us) hs = keepGiven du us hs
588updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
589 updateSolved' xs x
590updateSolved' xs (Bind n (Hole ty) t)
591 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
592updateSolved' xs (Bind n b t)
593 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
594updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
595updateSolved' xs (P _ n _)
596 | Just v <- lookup n xs = v
597updateSolved' xs t = t
599updateEnv ns [] = []
600updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
602updateError ns (CantUnify b l r e xs sc)
603 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
604updateError ns e = e
606solveInProblems x val [] = []
607solveInProblems x val ((l, r, env, err) : ps)
608 = ((instantiate val (pToV x l), instantiate val (pToV x r),
609 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
611updateProblems ctxt ns ps inj holes = up ns ps where
612 up ns [] = (ns, [])
613 up ns ((x, y, env, err) : ps) =
614 let x' = updateSolved ns x
615 y' = updateSolved ns y
616 err' = updateError ns err
617 env' = updateEnv ns env in
618 case unify ctxt env' x' y' inj holes of
619 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
620 up (ns ++ v) ps
621 _ -> let (ns', ps') = up ns ps in
622 (ns', (x',y',env',err') : ps')
624processTactic :: Tactic -> ProofState -> TC (ProofState, String)
625processTactic QED ps = case holes ps of
626 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
627 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
628 return (ps { done = True, pterm = tm' },
629 "Proof complete: " ++ showEnv [] tm')
630 _ -> fail "Still holes to fill."
631processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
632processTactic Undo ps = case previous ps of
633 Nothing -> fail "Nothing to undo."
634 Just pold -> return (pold, "")
635processTactic EndUnify ps
636 = let (h, ns_in) = unified ps
637 ns = dropGiven (dontunify ps) ns_in (holes ps)
638 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
639 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
640 (injective ps) (holes ps)
641 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
642 updateSolved ns'' (pterm ps) in
643 return (ps { pterm = tm',
644 unified = (h, []),
645 problems = probs',
646 holes = holes ps \\ map fst ns'' }, "")
647processTactic (Reorder n) ps
648 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
649 return (ps' { previous = Just ps, plog = "" }, plog ps')
650processTactic t ps
651 = case holes ps of
652 [] -> fail "Nothing to fill in."
653 (h:_) -> do ps' <- execStateT (process t h) ps
654 let pterm' = case solved ps' of
655 Just s -> updateSolved [s] (pterm ps')
656 _ -> pterm ps'
657 let (ns', probs')
658 = case solved ps' of
659 Just s -> updateProblems (context ps')
660 [s] (problems ps')
661 (injective ps')
662 (holes ps')
663 _ -> ([], problems ps')
664 -- rechecking problems may find more solutions, so
665 -- apply them here
666 let pterm'' = updateSolved ns' pterm'
667 return (ps' { pterm = pterm'',
668 solved = Nothing,
669 problems = probs',
670 previous = Just ps, plog = "",
671 holes = holes ps' \\ (map fst ns')}, plog ps')
673process :: Tactic -> Name -> StateT TState TC ()
674process EndUnify _
675 = do ps <- get
676 let (h, _) = unified ps
677 tactic (Just h) solve_unified
678process t h = tactic (Just h) (mktac t)
679 where mktac Attack = attack
680 mktac (Claim n r) = claim n r
681 mktac (Exact r) = exact r
682 mktac (Fill r) = fill r
683 mktac (PrepFill n ns) = prep_fill n ns
684 mktac CompleteFill = complete_fill
685 mktac Regret = regret
686 mktac Solve = solve
687 mktac (StartUnify n) = start_unify n
688 mktac Compute = compute
689 mktac HNF_Compute = hnf_compute
690 mktac (Intro n) = intro n
691 mktac (IntroTy ty n) = introTy ty n
692 mktac (Forall n t) = forall n t
693 mktac (LetBind n t v) = letbind n t v
694 mktac (Rewrite t) = rewrite t
695 mktac (PatVar n) = patvar n
696 mktac (PatBind n) = patbind n
697 mktac (CheckIn r) = check_in r
698 mktac (EvalIn r) = eval_in r
699 mktac (Focus n) = focus n
700 mktac (Defer n) = defer n
701 mktac (DeferType n t a) = deferType n t a
702 mktac (Instance n) = instanceArg n
703 mktac (SetInjective n) = setinj n
704 mktac (MoveLast n) = movelast n