git.iko.soy/Idris-dev
on fadeecd help sign in
Idris-dev/src/Core/ProofState.hs
685 lines 29 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 :: [Name],
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 | SetInjective Name
72 | MoveLast Name
73 | ProofState
74 | Undo
75 | QED
76 deriving Show
78-- Some utilites on proof and tactic states
80instance Show ProofState where
81 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
82 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)
83 = let OK g = goal (Just h) tm
84 wkenv = premises g in
85 "Other goals: " ++ show hs ++ "\n" ++
86 showPs wkenv (reverse wkenv) ++ "\n" ++
87 "-------------------------------- (" ++ show nm ++
88 ") -------\n " ++
89 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
90 where showPs env [] = ""
91 showPs env ((n, Let t v):bs)
92 = " " ++ show n ++ " : " ++
93 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
94 showEnv env ({- normalise ctxt env -} v) ++
95 "\n" ++ showPs env bs
96 showPs env ((n, b):bs)
97 = " " ++ show n ++ " : " ++
98 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
99 "\n" ++ showPs env bs
100 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
101 " =?= " ++ showEnv ps v
102 showG ps b = showEnv ps (binderTy b)
104instance Pretty ProofState where
105 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =
106 if size nm > breakingSize then
107 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
108 else
109 pretty nm <> colon <+> text " no more goals."
110 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =
111 let OK g = goal (Just h) tm in
112 let wkEnv = premises g in
113 text "Other goals" <+> colon <+> pretty hs $$
114 prettyPs wkEnv (reverse wkEnv) $$
115 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
116 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
117 where
118 prettyGoal ps (Guess t v) =
119 if size v > breakingSize then
120 prettyEnv ps t <+> text "=?=" $$
121 nest nestingSize (prettyEnv ps v)
122 else
123 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
124 prettyGoal ps b = prettyEnv ps $ binderTy b
126 prettyPs env [] = empty
127 prettyPs env ((n, Let t v):bs) =
128 nest nestingSize (pretty n <+> colon <+>
129 if size v > breakingSize then
130 prettyEnv env t <+> text "=" $$
131 nest nestingSize (prettyEnv env v) $$
132 nest nestingSize (prettyPs env bs)
133 else
134 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
135 nest nestingSize (prettyPs env bs))
136 prettyPs env ((n, b):bs) =
137 if size (binderTy b) > breakingSize then
138 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
139 else
140 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
141 nest nestingSize (prettyPs env bs))
143same Nothing n = True
144same (Just x) n = x == n
146hole (Hole _) = True
147hole (Guess _ _) = True
148hole _ = False
150holeName i = MN i "hole"
152qshow :: Fails -> String
153qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
155unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
156unify' ctxt env topx topy =
157 do ps <- get
158 let dont = dontunify ps
159 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $
160 lift $ unify ctxt env topx topy dont (holes ps)
161-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
162-- -- " in " ++ show env ++
163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
165-- ++ show (pterm ps)
166-- ++ "\n----------") $
167 case fails of
168-- [] -> return u
169 err ->
170 do ps <- get
171 let (h, ns) = unified ps
172 let (ns', probs') = updateProblems (context ps) (u ++ ns)
173 (err ++ problems ps)
174 (injective ps)
175 (holes ps)
176 put (ps { problems = probs',
177 unified = (h, ns') })
178 return u
180getName :: Monad m => String -> StateT TState m Name
181getName tag = do ps <- get
182 let n = nextname ps
183 put (ps { nextname = n+1 })
184 return $ MN n tag
186action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
187action a = do ps <- get
188 put (a ps)
190addLog :: Monad m => String -> StateT TState m ()
191addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
193newProof :: Name -> Context -> Type -> ProofState
194newProof n ctxt ty = let h = holeName 0
195 ty' = vToP ty in
196 PS n [h] [] 1 (Bind h (Hole ty')
197 (P Bound h ty')) ty [] (h, [])
198 Nothing [] []
199 [] []
200 Nothing ctxt "" False
202type TState = ProofState -- [TacticAction])
203type RunTactic = Context -> Env -> Term -> StateT TState TC Term
204type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
206envAtFocus :: ProofState -> TC Env
207envAtFocus ps
208 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
209 return (premises g)
210 | otherwise = fail "No holes"
212goalAtFocus :: ProofState -> TC (Binder Type)
213goalAtFocus ps
214 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
215 return (goalType g)
216 | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
218goal :: Hole -> Term -> TC Goal
219goal h tm = g [] tm where
220 g env (Bind n b sc) | hole b && same h n = return $ GD env b
221 | otherwise
222 = gb env b `mplus` g ((n, b):env) sc
223 g env (App f a) = g env f `mplus` g env a
224 g env t = fail "Can't find hole"
226 gb env (Let t v) = g env t `mplus` g env v
227 gb env (Guess t v) = g env t `mplus` g env v
228 gb env t = g env (binderTy t)
230tactic :: Hole -> RunTactic -> StateT TState TC ()
231tactic h f = do ps <- get
232 tm' <- atH (context ps) [] (pterm ps)
233 ps <- get -- might have changed while processing
234 put (ps { pterm = tm' })
235 where
236 atH c env binder@(Bind n b sc)
237 | hole b && same h n = f c env binder
238 | otherwise
239 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
240 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
241 atH c env t = return t
243 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
244 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
245 atHb c env t = do ty' <- atH c env (binderTy t)
246 return $ t { binderTy = ty' }
248attack :: RunTactic
249attack ctxt env (Bind x (Hole t) sc)
250 = do h <- getName "hole"
251 action (\ps -> ps { holes = h : holes ps })
252 return $ Bind x (Guess t (newtm h)) sc
253 where
254 newtm h = Bind h (Hole t) (P Bound h t)
255attack ctxt env _ = fail "Not an attackable hole"
257claim :: Name -> Raw -> RunTactic
258claim n ty ctxt env t =
259 do (tyv, tyt) <- lift $ check ctxt env ty
260 lift $ isType ctxt env tyt
261 action (\ps -> let (g:gs) = holes ps in
262 ps { holes = g : n : gs } )
263 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
265reorder_claims :: RunTactic
266reorder_claims ctxt env t
267 = -- trace (showSep "\n" (map show (scvs t))) $
268 let (bs, sc) = scvs t []
269 newbs = reverse (sortB (reverse bs)) in
270 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
271 return (bindAll newbs sc)
272 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
273 scvs sc acc = (reverse acc, sc)
275 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
276 sortB [] = []
277 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
278 | otherwise = sortB (insertB x xs)
280 insertB x [] = [x]
281 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
282 | otherwise = y : insertB x ys
284 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
285 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
286 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
288focus :: Name -> RunTactic
289focus n ctxt env t = do action (\ps -> let hs = holes ps in
290 if n `elem` hs
291 then ps { holes = n : (hs \\ [n]) }
292 else ps)
293 ps <- get
294 return t
296movelast :: Name -> RunTactic
297movelast n ctxt env t = do action (\ps -> let hs = holes ps in
298 if n `elem` hs
299 then ps { holes = (hs \\ [n]) ++ [n] }
300 else ps)
301 return t
303instanceArg :: Name -> RunTactic
304instanceArg n ctxt env (Bind x (Hole t) sc)
305 = do action (\ps -> let hs = holes ps
306 is = instances ps in
307 ps { holes = (hs \\ [x]) ++ [x],
308 instances = x:is })
309 return (Bind x (Hole t) sc)
311setinj :: Name -> RunTactic
312setinj n ctxt env (Bind x (Hole t) sc)
313 = do action (\ps -> let is = injective ps in
314 ps { injective = n : is })
315 return (Bind x (Hole t) sc)
317defer :: Name -> RunTactic
318defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
319 do action (\ps -> let hs = holes ps in
320 ps { holes = hs \\ [x] })
321 return (Bind n (GHole (mkTy (reverse env) t))
322 (mkApp (P Ref n ty) (map getP (reverse env))))
323 where
324 mkTy [] t = t
325 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
327 getP (n, b) = P Bound n (binderTy b)
329-- as defer, but build the type and application explicitly
330deferType :: Name -> Raw -> [Name] -> RunTactic
331deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
332 do (fty, _) <- lift $ check ctxt env fty_in
333 action (\ps -> let hs = holes ps
334 ds = deferred ps in
335 ps { holes = hs \\ [x],
336 deferred = n : ds })
337 return (Bind n (GHole fty)
338 (mkApp (P Ref n ty) (map getP args)))
339 where
340 getP n = case lookup n env of
341 Just b -> P Bound n (binderTy b)
342 Nothing -> error ("deferType can't find " ++ show n)
344regret :: RunTactic
345regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
346 do action (\ps -> let hs = holes ps in
347 ps { holes = hs \\ [x] })
348 return sc
349regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
351exact :: Raw -> RunTactic
352exact guess ctxt env (Bind x (Hole ty) sc) =
353 do (val, valty) <- lift $ check ctxt env guess
354 lift $ converts ctxt env valty ty
355 return $ Bind x (Guess ty val) sc
356exact _ _ _ _ = fail "Can't fill here."
358-- As exact, but attempts to solve other goals by unification
360fill :: Raw -> RunTactic
361fill guess ctxt env (Bind x (Hole ty) sc) =
362 do (val, valty) <- lift $ check ctxt env guess
363-- let valtyn = normalise ctxt env valty
364-- let tyn = normalise ctxt env ty
365 ns <- unify' ctxt env valty ty
366 ps <- get
367 let (uh, uns) = unified ps
368-- put (ps { unified = (uh, uns ++ ns) })
369-- addLog (show (uh, uns ++ ns))
370 return $ Bind x (Guess ty val) sc
371fill _ _ _ _ = fail "Can't fill here."
373prep_fill :: Name -> [Name] -> RunTactic
374prep_fill f as ctxt env (Bind x (Hole ty) sc) =
375 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
376 return $ Bind x (Guess ty val) sc
377prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
379complete_fill :: RunTactic
380complete_fill ctxt env (Bind x (Guess ty val) sc) =
381 do let guess = forget val
382 (val', valty) <- lift $ check ctxt env guess
383 ns <- unify' ctxt env valty ty
384 ps <- get
385 let (uh, uns) = unified ps
386-- put (ps { unified = (uh, uns ++ ns) })
387 return $ Bind x (Guess ty val) sc
388complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
390solve :: RunTactic
391solve ctxt env (Bind x (Guess ty val) sc)
392 | True = do ps <- get
393 let (uh, uns) = unified ps
394 action (\ps -> ps { holes = holes ps \\ [x],
395 solved = Just (x, val),
396-- problems = solveInProblems
397-- x val (problems ps),
398 -- dontunify = dontunify ps \\ [x],
399 -- unified = (uh, uns ++ [(x, val)]),
400 instances = instances ps \\ [x] })
401 return $ {- Bind x (Let ty val) sc -}
402 instantiate val (pToV x sc)
403 | otherwise = lift $ tfail $ IncompleteTerm val
404solve _ _ h@(Bind x t sc)
405 = do ps <- get
406 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
408introTy :: Raw -> Maybe Name -> RunTactic
409introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
410 do let n = case mn of
411 Just name -> name
412 Nothing -> x
413 let t' = case t of
414 x@(Bind y (Pi s) _) -> x
415 _ -> hnf ctxt env t
416 (tyv, tyt) <- lift $ check ctxt env ty
417-- ns <- lift $ unify ctxt env tyv t'
418 case t' of
419 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
420 do ns <- unify' ctxt env s tyv
421 ps <- get
422 let (uh, uns) = unified ps
423-- put (ps { unified = (uh, uns ++ ns) })
424 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
425 _ -> lift $ tfail $ CantIntroduce t'
426introTy ty n ctxt env _ = fail "Can't introduce here."
428intro :: Maybe Name -> RunTactic
429intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
430 do let n = case mn of
431 Just name -> name
432 Nothing -> x
433 let t' = case t of
434 x@(Bind y (Pi s) _) -> x
435 _ -> hnf ctxt env t
436 case t' of
437 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
438 let t' = instantiate (P Bound n s) (pToV y t) in
439 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
440 _ -> lift $ tfail $ CantIntroduce t'
441intro n ctxt env _ = fail "Can't introduce here."
443forall :: Name -> Raw -> RunTactic
444forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
445 do (tyv, tyt) <- lift $ check ctxt env ty
446 unify' ctxt env tyt (TType (UVar 0))
447 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
448forall n ty ctxt env _ = fail "Can't pi bind here"
450patvar :: Name -> RunTactic
451patvar n ctxt env (Bind x (Hole t) sc) =
452 do action (\ps -> ps { holes = holes ps \\ [x] })
453 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
454patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
456letbind :: Name -> Raw -> Raw -> RunTactic
457letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
458 do (tyv, tyt) <- lift $ check ctxt env ty
459 (valv, valt) <- lift $ check ctxt env val
460 lift $ isType ctxt env tyt
461 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
462letbind n ty val ctxt env _ = fail "Can't let bind here"
464rewrite :: Raw -> RunTactic
465rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
466 do (tmv, tmt) <- lift $ check ctxt env tm
467 let tmt' = normalise ctxt env tmt
468 case unApply tmt' of
469 (P _ (UN "=") _, [lt,rt,l,r]) ->
470 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
471 let newt = mkP l r l t
472 let sc = forget $ (Bind x (Hole newt)
473 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
474 [lt, l, r, p, tmv, xp]))
475 (scv, sct) <- lift $ check ctxt env sc
476 return scv
477 _ -> fail "Not an equality type"
478 where
479 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
480 -- an x, and put \x : lt in front
481 mkP lt l r ty | l == ty = lt
482 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
483 a' = if (r /= a) then mkP lt l r a else a in
484 App f' a'
485 mkP lt l r (Bind n b sc)
486 = let b' = mkPB b
487 sc' = if (r /= sc) then mkP lt l r sc else sc in
488 Bind n b' sc'
489 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
490 v' = if (r /= v) then mkP lt l r v else v in
491 Let t' v'
492 mkPB b = let ty = binderTy b
493 ty' = if (r /= ty) then mkP lt l r ty else ty in
494 b { binderTy = ty' }
495 mkP lt l r x = x
497 rname = MN 0 "replaced"
498rewrite _ _ _ _ = fail "Can't rewrite here"
500patbind :: Name -> RunTactic
501patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
502 do let t' = case t of
503 x@(Bind y (PVTy s) t) -> x
504 _ -> hnf ctxt env t
505 case t' of
506 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
507 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
508 _ -> fail "Nothing to pattern bind"
509patbind n ctxt env _ = fail "Can't pattern bind here"
511compute :: RunTactic
512compute ctxt env (Bind x (Hole ty) sc) =
513 do return $ Bind x (Hole (normalise ctxt env ty)) sc
514compute ctxt env t = return t
516hnf_compute :: RunTactic
517hnf_compute ctxt env (Bind x (Hole ty) sc) =
518 do let ty' = hnf ctxt env ty in
519-- trace ("HNF " ++ show (ty, ty')) $
520 return $ Bind x (Hole ty') sc
521hnf_compute ctxt env t = return t
523check_in :: Raw -> RunTactic
524check_in t ctxt env tm =
525 do (val, valty) <- lift $ check ctxt env t
526 addLog (showEnv env val ++ " : " ++ showEnv env valty)
527 return tm
529eval_in :: Raw -> RunTactic
530eval_in t ctxt env tm =
531 do (val, valty) <- lift $ check ctxt env t
532 let val' = normalise ctxt env val
533 let valty' = normalise ctxt env valty
534 addLog (showEnv env val ++ " : " ++
535 showEnv env valty ++
536-- " in " ++ show env ++
537 " ==>\n " ++
538 showEnv env val' ++ " : " ++
539 showEnv env valty')
540 return tm
542start_unify :: Name -> RunTactic
543start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
544 return tm
546tmap f (a, b, c) = (f a, b, c)
548solve_unified :: RunTactic
549solve_unified ctxt env tm =
550 do ps <- get
551 let (_, ns) = unified ps
552 let unify = dropGiven (dontunify ps) ns (holes ps)
553 action (\ps -> ps { holes = holes ps \\ map fst unify })
554 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
555 return (updateSolved unify tm)
556 where
558dropGiven du [] hs = []
559dropGiven du ((n, P Bound t ty) : us) hs
560 | n `elem` du && not (t `elem` du)
561 && n `elem` hs && t `elem` hs
562 = (t, P Bound n ty) : dropGiven du us hs
563dropGiven du (u@(n, _) : us) hs
564 | n `elem` du = dropGiven du us hs
565-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
566dropGiven du (u : us) hs = u : dropGiven du us hs
568updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
569 updateSolved' xs x
570updateSolved' xs (Bind n (Hole ty) t)
571 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
572updateSolved' xs (Bind n b t)
573 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
574updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
575updateSolved' xs (P _ n _)
576 | Just v <- lookup n xs = v
577updateSolved' xs t = t
579updateEnv ns [] = []
580updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
582updateError ns (CantUnify b l r e xs sc)
583 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
584updateError ns e = e
586solveInProblems x val [] = []
587solveInProblems x val ((l, r, env, err) : ps)
588 = ((instantiate val (pToV x l), instantiate val (pToV x r),
589 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
591updateProblems ctxt ns ps inj holes = up ns ps where
592 up ns [] = (ns, [])
593 up ns ((x, y, env, err) : ps) =
594 let x' = updateSolved ns x
595 y' = updateSolved ns y
596 err' = updateError ns err
597 env' = updateEnv ns env in
598 case unify ctxt env' x' y' inj holes of
599 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
600 up (ns ++ v) ps
601 _ -> let (ns', ps') = up ns ps in
602 (ns', (x',y',env',err') : ps')
604processTactic :: Tactic -> ProofState -> TC (ProofState, String)
605processTactic QED ps = case holes ps of
606 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
607 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
608 return (ps { done = True, pterm = tm' },
609 "Proof complete: " ++ showEnv [] tm')
610 _ -> fail "Still holes to fill."
611processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
612processTactic Undo ps = case previous ps of
613 Nothing -> fail "Nothing to undo."
614 Just pold -> return (pold, "")
615processTactic EndUnify ps
616 = let (h, ns_in) = unified ps
617 ns = dropGiven (dontunify ps) ns_in (holes ps)
618 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
619 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
620 (injective ps) (holes ps)
621 tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
622 updateSolved ns'' (pterm ps) in
623 return (ps { pterm = tm',
624 unified = (h, []),
625 problems = probs',
626 holes = holes ps \\ map fst ns'' }, "")
627processTactic (Reorder n) ps
628 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
629 return (ps' { previous = Just ps, plog = "" }, plog ps')
630processTactic t ps
631 = case holes ps of
632 [] -> fail "Nothing to fill in."
633 (h:_) -> do ps' <- execStateT (process t h) ps
634 let pterm' = case solved ps' of
635 Just s -> updateSolved [s] (pterm ps')
636 _ -> pterm ps'
637 let (ns', probs')
638 = case solved ps' of
639 Just s -> updateProblems (context ps')
640 [s] (problems ps')
641 (injective ps')
642 (holes ps')
643 _ -> ([], problems ps')
644 -- rechecking problems may find more solutions, so
645 -- apply them here
646 let pterm'' = updateSolved ns' pterm'
647 return (ps' { pterm = pterm'',
648 solved = Nothing,
649 problems = probs',
650 previous = Just ps, plog = "",
651 holes = holes ps' \\ (map fst ns')}, plog ps')
653process :: Tactic -> Name -> StateT TState TC ()
654process EndUnify _
655 = do ps <- get
656 let (h, _) = unified ps
657 tactic (Just h) solve_unified
658process t h = tactic (Just h) (mktac t)
659 where mktac Attack = attack
660 mktac (Claim n r) = claim n r
661 mktac (Exact r) = exact r
662 mktac (Fill r) = fill r
663 mktac (PrepFill n ns) = prep_fill n ns
664 mktac CompleteFill = complete_fill
665 mktac Regret = regret
666 mktac Solve = solve
667 mktac (StartUnify n) = start_unify n
668 mktac Compute = compute
669 mktac HNF_Compute = hnf_compute
670 mktac (Intro n) = intro n
671 mktac (IntroTy ty n) = introTy ty n
672 mktac (Forall n t) = forall n t
673 mktac (LetBind n t v) = letbind n t v
674 mktac (Rewrite t) = rewrite t
675 mktac (PatVar n) = patvar n
676 mktac (PatBind n) = patbind n
677 mktac (CheckIn r) = check_in r
678 mktac (EvalIn r) = eval_in r
679 mktac (Focus n) = focus n
680 mktac (Defer n) = defer n
681 mktac (DeferType n t a) = deferType n t a
682 mktac (Instance n) = instanceArg n
683 mktac (SetInjective n) = setinj n
684 mktac (MoveLast n) = movelast n