git.iko.soy/Idris-dev
on 875eecc help sign in
Idris-dev/src/Core/ProofState.hs
628 lines 26 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, dropGiven) 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 usedns :: [Name], -- used names, don't use again
25 nextname :: Int, -- name supply
26 pterm :: Term, -- current proof term
27 ptype :: Type, -- original goal
28 dontunify :: [Name], -- explicitly given by programmer, leave it
29 unified :: (Name, [(Name, Term)]),
30 solved :: Maybe (Name, Term),
31 problems :: Fails,
32 injective :: [(Term, Term, Term)],
33 deferred :: [Name], -- names we'll need to define
34 instances :: [Name], -- instance arguments (for type classes)
35 previous :: Maybe ProofState, -- for undo
36 context :: Context,
37 plog :: String,
38 done :: Bool
39 }
41data Goal = GD { premises :: Env,
42 goalType :: Binder Term
43 }
45data Tactic = Attack
46 | Claim Name Raw
47 | Reorder Name
48 | Exact Raw
49 | Fill Raw
50 | PrepFill Name [Name]
51 | CompleteFill
52 | Regret
53 | Solve
54 | StartUnify Name
55 | EndUnify
56 | Compute
57 | HNF_Compute
58 | EvalIn Raw
59 | CheckIn Raw
60 | Intro (Maybe Name)
61 | IntroTy Raw (Maybe Name)
62 | Forall Name Raw
63 | LetBind Name Raw Raw
64 | Rewrite Raw
65 | PatVar Name
66 | PatBind Name
67 | Focus Name
68 | Defer Name
69 | DeferType Name Raw [Name]
70 | Instance Name
71 | MoveLast Name
72 | ProofState
73 | Undo
74 | QED
75 deriving Show
77-- Some utilites on proof and tactic states
79instance Show ProofState where
80 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
81 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)
82 = let OK g = goal (Just h) tm
83 wkenv = premises g in
84 "Other goals: " ++ show hs ++ "\n" ++
85 showPs wkenv (reverse wkenv) ++ "\n" ++
86 "-------------------------------- (" ++ show nm ++
87 ") -------\n " ++
88 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
89 where showPs env [] = ""
90 showPs env ((n, Let t v):bs)
91 = " " ++ show n ++ " : " ++
92 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
93 showEnv env ({- normalise ctxt env -} v) ++
94 "\n" ++ showPs env bs
95 showPs env ((n, b):bs)
96 = " " ++ show n ++ " : " ++
97 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
98 "\n" ++ showPs env bs
99 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
100 " =?= " ++ showEnv ps v
101 showG ps b = showEnv ps (binderTy b)
103instance Pretty ProofState where
104 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =
105 if size nm > breakingSize then
106 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
107 else
108 pretty nm <> colon <+> text " no more goals."
109 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =
110 let OK g = goal (Just h) tm in
111 let wkEnv = premises g in
112 text "Other goals" <+> colon <+> pretty hs $$
113 prettyPs wkEnv (reverse wkEnv) $$
114 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
115 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
116 where
117 prettyGoal ps (Guess t v) =
118 if size v > breakingSize then
119 prettyEnv ps t <+> text "=?=" $$
120 nest nestingSize (prettyEnv ps v)
121 else
122 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
123 prettyGoal ps b = prettyEnv ps $ binderTy b
125 prettyPs env [] = empty
126 prettyPs env ((n, Let t v):bs) =
127 nest nestingSize (pretty n <+> colon <+>
128 if size v > breakingSize then
129 prettyEnv env t <+> text "=" $$
130 nest nestingSize (prettyEnv env v) $$
131 nest nestingSize (prettyPs env bs)
132 else
133 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
134 nest nestingSize (prettyPs env bs))
135 prettyPs env ((n, b):bs) =
136 if size (binderTy b) > breakingSize then
137 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
138 else
139 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
140 nest nestingSize (prettyPs env bs))
142same Nothing n = True
143same (Just x) n = x == n
145hole (Hole _) = True
146hole (Guess _ _) = True
147hole _ = False
149holeName i = MN i "hole"
151unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
152unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy
153 addInj inj
154 case fails of
155 [] -> return u
156 err ->
157 do ps <- get
158 put (ps { problems = err ++ problems ps })
159 return []
161getName :: Monad m => String -> StateT TState m Name
162getName tag = do ps <- get
163 let n = nextname ps
164 put (ps { nextname = n+1 })
165 return $ MN n tag
167action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
168action a = do ps <- get
169 put (a ps)
171addLog :: Monad m => String -> StateT TState m ()
172addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
174newProof :: Name -> Context -> Type -> ProofState
175newProof n ctxt ty = let h = holeName 0
176 ty' = vToP ty in
177 PS n [h] [] 1 (Bind h (Hole ty')
178 (P Bound h ty')) ty [] (h, [])
179 Nothing [] []
180 [] []
181 Nothing ctxt "" False
183type TState = ProofState -- [TacticAction])
184type RunTactic = Context -> Env -> Term -> StateT TState TC Term
185type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
187envAtFocus :: ProofState -> TC Env
188envAtFocus ps
189 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
190 return (premises g)
191 | otherwise = fail "No holes"
193goalAtFocus :: ProofState -> TC (Binder Type)
194goalAtFocus ps
195 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
196 return (goalType g)
198goal :: Hole -> Term -> TC Goal
199goal h tm = g [] tm where
200 g env (Bind n b sc) | hole b && same h n = return $ GD env b
201 | otherwise
202 = gb env b `mplus` g ((n, b):env) sc
203 g env (App f a) = g env f `mplus` g env a
204 g env t = fail "Can't find hole"
206 gb env (Let t v) = g env t `mplus` g env v
207 gb env (Guess t v) = g env t `mplus` g env v
208 gb env t = g env (binderTy t)
210tactic :: Hole -> RunTactic -> StateT TState TC ()
211tactic h f = do ps <- get
212 tm' <- atH (context ps) [] (pterm ps)
213 ps <- get -- might have changed while processing
214 put (ps { pterm = tm' })
215 where
216 atH c env binder@(Bind n b sc)
217 | hole b && same h n = f c env binder
218 | otherwise
219 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
220 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
221 atH c env t = return t
223 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
224 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
225 atHb c env t = do ty' <- atH c env (binderTy t)
226 return $ t { binderTy = ty' }
228attack :: RunTactic
229attack ctxt env (Bind x (Hole t) sc)
230 = do h <- getName "hole"
231 action (\ps -> ps { holes = h : holes ps })
232 return $ Bind x (Guess t (newtm h)) sc
233 where
234 newtm h = Bind h (Hole t) (P Bound h t)
235attack ctxt env _ = fail "Not an attackable hole"
237claim :: Name -> Raw -> RunTactic
238claim n ty ctxt env t =
239 do (tyv, tyt) <- lift $ check ctxt env ty
240 lift $ isType ctxt env tyt
241 action (\ps -> let (g:gs) = holes ps in
242 ps { holes = g : n : gs } )
243 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
245reorder_claims :: RunTactic
246reorder_claims ctxt env t
247 = -- trace (showSep "\n" (map show (scvs t))) $
248 let (bs, sc) = scvs t []
249 newbs = reverse (sortB (reverse bs)) in
250 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
251 return (bindAll newbs sc)
252 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
253 scvs sc acc = (reverse acc, sc)
255 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
256 sortB [] = []
257 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
258 | otherwise = sortB (insertB x xs)
260 insertB x [] = [x]
261 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
262 | otherwise = y : insertB x ys
264 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
265 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
266 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
268focus :: Name -> RunTactic
269focus n ctxt env t = do action (\ps -> let hs = holes ps in
270 if n `elem` hs
271 then ps { holes = n : (hs \\ [n]) }
272 else ps)
273 ps <- get
274 return t
276movelast :: Name -> RunTactic
277movelast n ctxt env t = do action (\ps -> let hs = holes ps in
278 if n `elem` hs
279 then ps { holes = (hs \\ [n]) ++ [n] }
280 else ps)
281 return t
283instanceArg :: Name -> RunTactic
284instanceArg n ctxt env (Bind x (Hole t) sc)
285 = do action (\ps -> let hs = holes ps
286 is = instances ps in
287 ps { holes = (hs \\ [x]) ++ [x],
288 instances = x:is })
289 return (Bind x (Hole t) sc)
291defer :: Name -> RunTactic
292defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
293 do action (\ps -> let hs = holes ps in
294 ps { holes = hs \\ [x] })
295 return (Bind n (GHole (mkTy (reverse env) t))
296 (mkApp (P Ref n ty) (map getP (reverse env))))
297 where
298 mkTy [] t = t
299 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
301 getP (n, b) = P Bound n (binderTy b)
303-- as defer, but build the type and application explicitly
304deferType :: Name -> Raw -> [Name] -> RunTactic
305deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
306 do (fty, _) <- lift $ check ctxt env fty_in
307 action (\ps -> let hs = holes ps
308 ds = deferred ps in
309 ps { holes = hs \\ [x],
310 deferred = n : ds })
311 return (Bind n (GHole fty)
312 (mkApp (P Ref n ty) (map getP args)))
313 where
314 getP n = case lookup n env of
315 Just b -> P Bound n (binderTy b)
316 Nothing -> error ("deferType can't find " ++ show n)
318regret :: RunTactic
319regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
320 do action (\ps -> let hs = holes ps in
321 ps { holes = hs \\ [x] })
322 return sc
323regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
325addInj :: [(Term, Term, Term)] -> StateT TState TC ()
326addInj inj = do ps <- get
327 put (ps { injective = inj ++ injective ps })
329exact :: Raw -> RunTactic
330exact guess ctxt env (Bind x (Hole ty) sc) =
331 do (val, valty) <- lift $ check ctxt env guess
332 lift $ converts ctxt env valty ty
333 return $ Bind x (Guess ty val) sc
334exact _ _ _ _ = fail "Can't fill here."
336-- As exact, but attempts to solve other goals by unification
338fill :: Raw -> RunTactic
339fill guess ctxt env (Bind x (Hole ty) sc) =
340 do (val, valty) <- lift $ check ctxt env guess
341 s <- get
342-- let valtyn = normalise ctxt env valty
343-- let tyn = normalise ctxt env ty
344 ns <- unify' ctxt env valty ty
345 ps <- get
346 let (uh, uns) = unified ps
347 put (ps { unified = (uh, uns ++ ns) })
348-- addLog (show (uh, uns ++ ns))
349 return $ Bind x (Guess ty val) sc
350fill _ _ _ _ = fail "Can't fill here."
352prep_fill :: Name -> [Name] -> RunTactic
353prep_fill f as ctxt env (Bind x (Hole ty) sc) =
354 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
355 return $ Bind x (Guess ty val) sc
356prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
358complete_fill :: RunTactic
359complete_fill ctxt env (Bind x (Guess ty val) sc) =
360 do let guess = forget val
361 (val', valty) <- lift $ check ctxt env guess
362 ns <- unify' ctxt env valty ty
363 ps <- get
364 let (uh, uns) = unified ps
365 put (ps { unified = (uh, uns ++ ns) })
366 return $ Bind x (Guess ty val) sc
367complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
369solve :: RunTactic
370solve ctxt env (Bind x (Guess ty val) sc)
371 | pureTerm val = do ps <- get
372 let (uh, uns) = unified ps
373 action (\ps -> ps { holes = holes ps \\ [x],
374 solved = Just (x, val),
375 -- dontunify = dontunify ps \\ [x],
376 -- unified = (uh, uns ++ [(x, val)]),
377 instances = instances ps \\ [x] })
378 return $ {- Bind x (Let ty val) sc -}
379 instantiate val (pToV x sc)
380 | otherwise = lift $ tfail $ IncompleteTerm val
381solve _ _ h = do ps <- get
382 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
384introTy :: Raw -> Maybe Name -> RunTactic
385introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
386 do let n = case mn of
387 Just name -> name
388 Nothing -> x
389 let t' = case t of
390 x@(Bind y (Pi s) _) -> x
391 _ -> hnf ctxt env t
392 (tyv, tyt) <- lift $ check ctxt env ty
393-- ns <- lift $ unify ctxt env tyv t'
394 case t' of
395 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
396 do ns <- unify' ctxt env s tyv
397 ps <- get
398 let (uh, uns) = unified ps
399 put (ps { unified = (uh, uns ++ ns) })
400 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
401 _ -> fail "Nothing to introduce"
402introTy ty n ctxt env _ = fail "Can't introduce here."
404intro :: Maybe Name -> RunTactic
405intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
406 do let n = case mn of
407 Just name -> name
408 Nothing -> x
409 let t' = case t of
410 x@(Bind y (Pi s) _) -> x
411 _ -> hnf ctxt env t
412 case t' of
413 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
414 let t' = instantiate (P Bound n s) (pToV y t) in
415 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
416 _ -> fail "Nothing to introduce"
417intro n ctxt env _ = fail "Can't introduce here."
419forall :: Name -> Raw -> RunTactic
420forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
421 do (tyv, tyt) <- lift $ check ctxt env ty
422 lift $ isType ctxt env tyt
423 lift $ isType ctxt env t
424 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
425forall n ty ctxt env _ = fail "Can't pi bind here"
427patvar :: Name -> RunTactic
428patvar n ctxt env (Bind x (Hole t) sc) =
429 do action (\ps -> ps { holes = holes ps \\ [x] })
430 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
431patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
433letbind :: Name -> Raw -> Raw -> RunTactic
434letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
435 do (tyv, tyt) <- lift $ check ctxt env ty
436 (valv, valt) <- lift $ check ctxt env val
437 lift $ isType ctxt env tyt
438 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
439letbind n ty val ctxt env _ = fail "Can't let bind here"
441rewrite :: Raw -> RunTactic
442rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
443 do (tmv, tmt) <- lift $ check ctxt env tm
444 let tmt' = normalise ctxt env tmt
445 case unApply tmt' of
446 (P _ (UN "=") _, [lt,rt,l,r]) ->
447 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
448 let newt = mkP l r l t
449 let sc = forget $ (Bind x (Hole newt)
450 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
451 [lt, l, r, p, tmv, xp]))
452 (scv, sct) <- lift $ check ctxt env sc
453 return scv
454 _ -> fail "Not an equality type"
455 where
456 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
457 -- an x, and put \x : lt in front
458 mkP lt l r ty | l == ty = lt
459 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
460 a' = if (r /= a) then mkP lt l r a else a in
461 App f' a'
462 mkP lt l r (Bind n b sc)
463 = let b' = mkPB b
464 sc' = if (r /= sc) then mkP lt l r sc else sc in
465 Bind n b' sc'
466 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
467 v' = if (r /= v) then mkP lt l r v else v in
468 Let t' v'
469 mkPB b = let ty = binderTy b
470 ty' = if (r /= ty) then mkP lt l r ty else ty in
471 b { binderTy = ty' }
472 mkP lt l r x = x
474 rname = MN 0 "replaced"
475rewrite _ _ _ _ = fail "Can't rewrite here"
477patbind :: Name -> RunTactic
478patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
479 do let t' = case t of
480 x@(Bind y (PVTy s) t) -> x
481 _ -> hnf ctxt env t
482 case t' of
483 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
484 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
485 _ -> fail "Nothing to pattern bind"
486patbind n ctxt env _ = fail "Can't pattern bind here"
488compute :: RunTactic
489compute ctxt env (Bind x (Hole ty) sc) =
490 do return $ Bind x (Hole (normalise ctxt env ty)) sc
492hnf_compute :: RunTactic
493hnf_compute ctxt env (Bind x (Hole ty) sc) =
494 do let ty' = hnf ctxt env ty in
495-- trace ("HNF " ++ show (ty, ty')) $
496 return $ Bind x (Hole ty') sc
498check_in :: Raw -> RunTactic
499check_in t ctxt env tm =
500 do (val, valty) <- lift $ check ctxt env t
501 addLog (showEnv env val ++ " : " ++ showEnv env valty)
502 return tm
504eval_in :: Raw -> RunTactic
505eval_in t ctxt env tm =
506 do (val, valty) <- lift $ check ctxt env t
507 let val' = normalise ctxt env val
508 let valty' = normalise ctxt env valty
509 addLog (showEnv env val ++ " : " ++
510 showEnv env valty ++
511-- " in " ++ show env ++
512 " ==>\n " ++
513 showEnv env val' ++ " : " ++
514 showEnv env valty')
515 return tm
517start_unify :: Name -> RunTactic
518start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
519 return tm
521tmap f (a, b, c) = (f a, b, c)
523solve_unified :: RunTactic
524solve_unified ctxt env tm =
525 do ps <- get
526 let (_, ns) = unified ps
527 let unify = dropGiven (dontunify ps) ns
528 action (\ps -> ps { holes = holes ps \\ map fst unify })
529 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
530 action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) })
531 return (updateSolved unify tm)
532 where
534dropGiven du [] = []
535dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)
536 = (t, P Bound n ty) : dropGiven du us
537dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us
538-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
539dropGiven du (u : us) = u : dropGiven du us
541updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
542 updateSolved' xs x
543updateSolved' xs (Bind n (Hole ty) t)
544 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
545updateSolved' xs (Bind n b t)
546 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
547updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
548updateSolved' xs (P _ n _)
549 | Just v <- lookup n xs = v
550updateSolved' xs t = t
552updateProblems ns [] = []
553updateProblems ns ((x, y, env, err) : ps) =
554 let x' = updateSolved ns x
555 y' = updateSolved ns y in
556 (x',y',env,err) : updateProblems ns ps
558processTactic :: Tactic -> ProofState -> TC (ProofState, String)
559processTactic QED ps = case holes ps of
560 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
561 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
562 return (ps { done = True, pterm = tm' },
563 "Proof complete: " ++ showEnv [] tm')
564 _ -> fail "Still holes to fill."
565processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
566processTactic Undo ps = case previous ps of
567 Nothing -> fail "Nothing to undo."
568 Just pold -> return (pold, "")
569processTactic EndUnify ps
570 = let (h, ns_in) = unified ps
571 ns = dropGiven (dontunify ps) ns_in
572 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
573 tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $
574 updateSolved ns' (pterm ps)
575 probs' = updateProblems ns' (problems ps) in
576 case probs' of
577 [] -> return (ps { pterm = tm',
578 unified = (h, []),
579 injective = map (tmap (updateSolved ns'))
580 (injective ps),
581 holes = holes ps \\ map fst ns' }, "")
582 errs@((_,_,_,err):_) -> tfail err
583processTactic (Reorder n) ps
584 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
585 return (ps' { previous = Just ps, plog = "" }, plog ps')
586processTactic t ps
587 = case holes ps of
588 [] -> fail "Nothing to fill in."
589 (h:_) -> do ps' <- execStateT (process t h) ps
590 let pterm' = case solved ps' of
591 Just s -> updateSolved [s] (pterm ps')
592 _ -> pterm ps'
593 return (ps' { pterm = pterm',
594 solved = Nothing,
595 previous = Just ps, plog = "" }, plog ps')
597process :: Tactic -> Name -> StateT TState TC ()
598process EndUnify _
599 = do ps <- get
600 let (h, _) = unified ps
601 tactic (Just h) solve_unified
602process t h = tactic (Just h) (mktac t)
603 where mktac Attack = attack
604 mktac (Claim n r) = claim n r
605 mktac (Exact r) = exact r
606 mktac (Fill r) = fill r
607 mktac (PrepFill n ns) = prep_fill n ns
608 mktac CompleteFill = complete_fill
609 mktac Regret = regret
610 mktac Solve = solve
611 mktac (StartUnify n) = start_unify n
612 mktac Compute = compute
613 mktac HNF_Compute = hnf_compute
614 mktac (Intro n) = intro n
615 mktac (IntroTy ty n) = introTy ty n
616 mktac (Forall n t) = forall n t
617 mktac (LetBind n t v) = letbind n t v
618 mktac (Rewrite t) = rewrite t
619 mktac (PatVar n) = patvar n
620 mktac (PatBind n) = patbind n
621 mktac (CheckIn r) = check_in r
622 mktac (EvalIn r) = eval_in r
623 mktac (Focus n) = focus n
624 mktac (Defer n) = defer n
625 mktac (DeferType n t a) = deferType n t a
626 mktac (Instance n) = instanceArg n
627 mktac (MoveLast n) = movelast n