git.iko.soy/Idris-dev
on df5bf81 help sign in
Idris-dev/src/Core/ProofState.hs
682 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 (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)
159-- trace ("Unified " ++ show (topx, topy) ++ show (injective ps) ++
160-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
161-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps)) $
162 case fails of
163-- [] -> return u
164 err ->
165 do ps <- get
166 let (h, ns) = unified ps
167 let (ns', probs') = updateProblems (context ps) (u ++ ns)
168 (err ++ problems ps)
169 (injective ps)
170 (holes ps)
171 put (ps { problems = probs',
172 unified = (h, ns') })
173 return u
175getName :: Monad m => String -> StateT TState m Name
176getName tag = do ps <- get
177 let n = nextname ps
178 put (ps { nextname = n+1 })
179 return $ MN n tag
181action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
182action a = do ps <- get
183 put (a ps)
185addLog :: Monad m => String -> StateT TState m ()
186addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
188newProof :: Name -> Context -> Type -> ProofState
189newProof n ctxt ty = let h = holeName 0
190 ty' = vToP ty in
191 PS n [h] [] 1 (Bind h (Hole ty')
192 (P Bound h ty')) ty [] (h, [])
193 Nothing [] []
194 [] []
195 Nothing ctxt "" False
197type TState = ProofState -- [TacticAction])
198type RunTactic = Context -> Env -> Term -> StateT TState TC Term
199type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
201envAtFocus :: ProofState -> TC Env
202envAtFocus ps
203 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
204 return (premises g)
205 | otherwise = fail "No holes"
207goalAtFocus :: ProofState -> TC (Binder Type)
208goalAtFocus ps
209 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
210 return (goalType g)
211 | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
213goal :: Hole -> Term -> TC Goal
214goal h tm = g [] tm where
215 g env (Bind n b sc) | hole b && same h n = return $ GD env b
216 | otherwise
217 = gb env b `mplus` g ((n, b):env) sc
218 g env (App f a) = g env f `mplus` g env a
219 g env t = fail "Can't find hole"
221 gb env (Let t v) = g env t `mplus` g env v
222 gb env (Guess t v) = g env t `mplus` g env v
223 gb env t = g env (binderTy t)
225tactic :: Hole -> RunTactic -> StateT TState TC ()
226tactic h f = do ps <- get
227 tm' <- atH (context ps) [] (pterm ps)
228 ps <- get -- might have changed while processing
229 put (ps { pterm = tm' })
230 where
231 atH c env binder@(Bind n b sc)
232 | hole b && same h n = f c env binder
233 | otherwise
234 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
235 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
236 atH c env t = return t
238 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
239 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
240 atHb c env t = do ty' <- atH c env (binderTy t)
241 return $ t { binderTy = ty' }
243attack :: RunTactic
244attack ctxt env (Bind x (Hole t) sc)
245 = do h <- getName "hole"
246 action (\ps -> ps { holes = h : holes ps })
247 return $ Bind x (Guess t (newtm h)) sc
248 where
249 newtm h = Bind h (Hole t) (P Bound h t)
250attack ctxt env _ = fail "Not an attackable hole"
252claim :: Name -> Raw -> RunTactic
253claim n ty ctxt env t =
254 do (tyv, tyt) <- lift $ check ctxt env ty
255 lift $ isType ctxt env tyt
256 action (\ps -> let (g:gs) = holes ps in
257 ps { holes = g : n : gs } )
258 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
260reorder_claims :: RunTactic
261reorder_claims ctxt env t
262 = -- trace (showSep "\n" (map show (scvs t))) $
263 let (bs, sc) = scvs t []
264 newbs = reverse (sortB (reverse bs)) in
265 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
266 return (bindAll newbs sc)
267 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
268 scvs sc acc = (reverse acc, sc)
270 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
271 sortB [] = []
272 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
273 | otherwise = sortB (insertB x xs)
275 insertB x [] = [x]
276 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
277 | otherwise = y : insertB x ys
279 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
280 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
281 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
283focus :: Name -> RunTactic
284focus n ctxt env t = do action (\ps -> let hs = holes ps in
285 if n `elem` hs
286 then ps { holes = n : (hs \\ [n]) }
287 else ps)
288 ps <- get
289 return t
291movelast :: Name -> RunTactic
292movelast n ctxt env t = do action (\ps -> let hs = holes ps in
293 if n `elem` hs
294 then ps { holes = (hs \\ [n]) ++ [n] }
295 else ps)
296 return t
298instanceArg :: Name -> RunTactic
299instanceArg n ctxt env (Bind x (Hole t) sc)
300 = do action (\ps -> let hs = holes ps
301 is = instances ps in
302 ps { holes = (hs \\ [x]) ++ [x],
303 instances = x:is })
304 return (Bind x (Hole t) sc)
306setinj :: Name -> RunTactic
307setinj n ctxt env (Bind x (Hole t) sc)
308 = do action (\ps -> let is = injective ps in
309 ps { injective = n : is })
310 return (Bind x (Hole t) sc)
312defer :: Name -> RunTactic
313defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
314 do action (\ps -> let hs = holes ps in
315 ps { holes = hs \\ [x] })
316 return (Bind n (GHole (mkTy (reverse env) t))
317 (mkApp (P Ref n ty) (map getP (reverse env))))
318 where
319 mkTy [] t = t
320 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
322 getP (n, b) = P Bound n (binderTy b)
324-- as defer, but build the type and application explicitly
325deferType :: Name -> Raw -> [Name] -> RunTactic
326deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
327 do (fty, _) <- lift $ check ctxt env fty_in
328 action (\ps -> let hs = holes ps
329 ds = deferred ps in
330 ps { holes = hs \\ [x],
331 deferred = n : ds })
332 return (Bind n (GHole fty)
333 (mkApp (P Ref n ty) (map getP args)))
334 where
335 getP n = case lookup n env of
336 Just b -> P Bound n (binderTy b)
337 Nothing -> error ("deferType can't find " ++ show n)
339regret :: RunTactic
340regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
341 do action (\ps -> let hs = holes ps in
342 ps { holes = hs \\ [x] })
343 return sc
344regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
346exact :: Raw -> RunTactic
347exact guess ctxt env (Bind x (Hole ty) sc) =
348 do (val, valty) <- lift $ check ctxt env guess
349 lift $ converts ctxt env valty ty
350 return $ Bind x (Guess ty val) sc
351exact _ _ _ _ = fail "Can't fill here."
353-- As exact, but attempts to solve other goals by unification
355fill :: Raw -> RunTactic
356fill guess ctxt env (Bind x (Hole ty) sc) =
357 do (val, valty) <- lift $ check ctxt env guess
358 s <- get
359-- let valtyn = normalise ctxt env valty
360-- let tyn = normalise ctxt env ty
361 ns <- unify' ctxt env valty ty
362 ps <- get
363 let (uh, uns) = unified ps
364-- put (ps { unified = (uh, uns ++ ns) })
365-- addLog (show (uh, uns ++ ns))
366 return $ Bind x (Guess ty val) sc
367fill _ _ _ _ = fail "Can't fill here."
369prep_fill :: Name -> [Name] -> RunTactic
370prep_fill f as ctxt env (Bind x (Hole ty) sc) =
371 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
372 return $ Bind x (Guess ty val) sc
373prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
375complete_fill :: RunTactic
376complete_fill ctxt env (Bind x (Guess ty val) sc) =
377 do let guess = forget val
378 (val', valty) <- lift $ check ctxt env guess
379 ns <- unify' ctxt env valty ty
380 ps <- get
381 let (uh, uns) = unified ps
382-- put (ps { unified = (uh, uns ++ ns) })
383 return $ Bind x (Guess ty val) sc
384complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
386solve :: RunTactic
387solve ctxt env (Bind x (Guess ty val) sc)
388 | True = do ps <- get
389 let (uh, uns) = unified ps
390 action (\ps -> ps { holes = holes ps \\ [x],
391 solved = Just (x, val),
392-- problems = solveInProblems
393-- x val (problems ps),
394 -- dontunify = dontunify ps \\ [x],
395 -- unified = (uh, uns ++ [(x, val)]),
396 instances = instances ps \\ [x] })
397 return $ {- Bind x (Let ty val) sc -}
398 instantiate val (pToV x sc)
399 | otherwise = do ps <- get
400 lift $ tfail $ IncompleteTerm val
401solve _ _ h = do ps <- get
402 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
404introTy :: Raw -> Maybe Name -> RunTactic
405introTy ty 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 (tyv, tyt) <- lift $ check ctxt env ty
413-- ns <- lift $ unify ctxt env tyv t'
414 case t' of
415 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
416 do ns <- unify' ctxt env s tyv
417 ps <- get
418 let (uh, uns) = unified ps
419-- put (ps { unified = (uh, uns ++ ns) })
420 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
421 _ -> fail "Nothing to introduce"
422introTy ty n ctxt env _ = fail "Can't introduce here."
424intro :: Maybe Name -> RunTactic
425intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
426 do let n = case mn of
427 Just name -> name
428 Nothing -> x
429 let t' = case t of
430 x@(Bind y (Pi s) _) -> x
431 _ -> hnf ctxt env t
432 case t' of
433 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
434 let t' = instantiate (P Bound n s) (pToV y t) in
435 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
436 _ -> fail "Nothing to introduce"
437intro n ctxt env _ = fail "Can't introduce here."
439forall :: Name -> Raw -> RunTactic
440forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
441 do (tyv, tyt) <- lift $ check ctxt env ty
442 lift $ isType ctxt env tyt
443 lift $ isType ctxt env t
444 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
445forall n ty ctxt env _ = fail "Can't pi bind here"
447patvar :: Name -> RunTactic
448patvar n ctxt env (Bind x (Hole t) sc) =
449 do action (\ps -> ps { holes = holes ps \\ [x] })
450 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
451patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
453letbind :: Name -> Raw -> Raw -> RunTactic
454letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
455 do (tyv, tyt) <- lift $ check ctxt env ty
456 (valv, valt) <- lift $ check ctxt env val
457 lift $ isType ctxt env tyt
458 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
459letbind n ty val ctxt env _ = fail "Can't let bind here"
461rewrite :: Raw -> RunTactic
462rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
463 do (tmv, tmt) <- lift $ check ctxt env tm
464 let tmt' = normalise ctxt env tmt
465 case unApply tmt' of
466 (P _ (UN "=") _, [lt,rt,l,r]) ->
467 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
468 let newt = mkP l r l t
469 let sc = forget $ (Bind x (Hole newt)
470 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
471 [lt, l, r, p, tmv, xp]))
472 (scv, sct) <- lift $ check ctxt env sc
473 return scv
474 _ -> fail "Not an equality type"
475 where
476 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
477 -- an x, and put \x : lt in front
478 mkP lt l r ty | l == ty = lt
479 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
480 a' = if (r /= a) then mkP lt l r a else a in
481 App f' a'
482 mkP lt l r (Bind n b sc)
483 = let b' = mkPB b
484 sc' = if (r /= sc) then mkP lt l r sc else sc in
485 Bind n b' sc'
486 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
487 v' = if (r /= v) then mkP lt l r v else v in
488 Let t' v'
489 mkPB b = let ty = binderTy b
490 ty' = if (r /= ty) then mkP lt l r ty else ty in
491 b { binderTy = ty' }
492 mkP lt l r x = x
494 rname = MN 0 "replaced"
495rewrite _ _ _ _ = fail "Can't rewrite here"
497patbind :: Name -> RunTactic
498patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
499 do let t' = case t of
500 x@(Bind y (PVTy s) t) -> x
501 _ -> hnf ctxt env t
502 case t' of
503 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
504 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
505 _ -> fail "Nothing to pattern bind"
506patbind n ctxt env _ = fail "Can't pattern bind here"
508compute :: RunTactic
509compute ctxt env (Bind x (Hole ty) sc) =
510 do return $ Bind x (Hole (normalise ctxt env ty)) sc
511compute ctxt env t = return t
513hnf_compute :: RunTactic
514hnf_compute ctxt env (Bind x (Hole ty) sc) =
515 do let ty' = hnf ctxt env ty in
516-- trace ("HNF " ++ show (ty, ty')) $
517 return $ Bind x (Hole ty') sc
518hnf_compute ctxt env t = return t
520check_in :: Raw -> RunTactic
521check_in t ctxt env tm =
522 do (val, valty) <- lift $ check ctxt env t
523 addLog (showEnv env val ++ " : " ++ showEnv env valty)
524 return tm
526eval_in :: Raw -> RunTactic
527eval_in t ctxt env tm =
528 do (val, valty) <- lift $ check ctxt env t
529 let val' = normalise ctxt env val
530 let valty' = normalise ctxt env valty
531 addLog (showEnv env val ++ " : " ++
532 showEnv env valty ++
533-- " in " ++ show env ++
534 " ==>\n " ++
535 showEnv env val' ++ " : " ++
536 showEnv env valty')
537 return tm
539start_unify :: Name -> RunTactic
540start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
541 return tm
543tmap f (a, b, c) = (f a, b, c)
545solve_unified :: RunTactic
546solve_unified ctxt env tm =
547 do ps <- get
548 let (_, ns) = unified ps
549 let unify = dropGiven (dontunify ps) ns (holes ps)
550 action (\ps -> ps { holes = holes ps \\ map fst unify })
551 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
552 return (updateSolved unify tm)
553 where
555dropGiven du [] hs = []
556dropGiven du ((n, P Bound t ty) : us) hs
557 | n `elem` du && not (t `elem` du)
558 && n `elem` hs && t `elem` hs
559 = (t, P Bound n ty) : dropGiven du us hs
560dropGiven du (u@(n, _) : us) hs
561 | n `elem` du = dropGiven du us hs
562-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
563dropGiven du (u : us) hs = u : dropGiven du us hs
565updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
566 updateSolved' xs x
567updateSolved' xs (Bind n (Hole ty) t)
568 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
569updateSolved' xs (Bind n b t)
570 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
571updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
572updateSolved' xs (P _ n _)
573 | Just v <- lookup n xs = v
574updateSolved' xs t = t
576updateEnv ns [] = []
577updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
579updateError ns (CantUnify b l r e xs sc)
580 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
581updateError ns e = e
583solveInProblems x val [] = []
584solveInProblems x val ((l, r, env, err) : ps)
585 = ((instantiate val (pToV x l), instantiate val (pToV x r),
586 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
588updateProblems ctxt ns ps inj holes = up ns ps where
589 up ns [] = (ns, [])
590 up ns ((x, y, env, err) : ps) =
591 let x' = updateSolved ns x
592 y' = updateSolved ns y
593 err' = updateError ns err
594 env' = updateEnv ns env in
595 case unify ctxt env' x' y' inj holes of
596 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
597 up (ns ++ v) ps
598 _ -> let (ns', ps') = up ns ps in
599 (ns', (x',y',env',err') : ps')
601processTactic :: Tactic -> ProofState -> TC (ProofState, String)
602processTactic QED ps = case holes ps of
603 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
604 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
605 return (ps { done = True, pterm = tm' },
606 "Proof complete: " ++ showEnv [] tm')
607 _ -> fail "Still holes to fill."
608processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
609processTactic Undo ps = case previous ps of
610 Nothing -> fail "Nothing to undo."
611 Just pold -> return (pold, "")
612processTactic EndUnify ps
613 = let (h, ns_in) = unified ps
614 ns = dropGiven (dontunify ps) ns_in (holes ps)
615 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
616 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
617 (injective ps) (holes ps)
618 tm' = -- trace ("Updating " ++ show ns' ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
619 updateSolved ns'' (pterm ps) in
620 return (ps { pterm = tm',
621 unified = (h, []),
622 problems = probs',
623 holes = holes ps \\ map fst ns'' }, "")
624processTactic (Reorder n) ps
625 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
626 return (ps' { previous = Just ps, plog = "" }, plog ps')
627processTactic t ps
628 = case holes ps of
629 [] -> fail "Nothing to fill in."
630 (h:_) -> do ps' <- execStateT (process t h) ps
631 let pterm' = case solved ps' of
632 Just s -> updateSolved [s] (pterm ps')
633 _ -> pterm ps'
634 let (ns', probs')
635 = case solved ps' of
636 Just s -> updateProblems (context ps')
637 [s] (problems ps')
638 (injective ps')
639 (holes ps')
640 _ -> ([], problems ps')
641 -- rechecking problems may find more solutions, so
642 -- apply them here
643 let pterm'' = updateSolved ns' pterm'
644 return (ps' { pterm = pterm'',
645 solved = Nothing,
646 problems = probs',
647 previous = Just ps, plog = "",
648 holes = holes ps' \\ (map fst ns')}, plog ps')
650process :: Tactic -> Name -> StateT TState TC ()
651process EndUnify _
652 = do ps <- get
653 let (h, _) = unified ps
654 tactic (Just h) solve_unified
655process t h = tactic (Just h) (mktac t)
656 where mktac Attack = attack
657 mktac (Claim n r) = claim n r
658 mktac (Exact r) = exact r
659 mktac (Fill r) = fill r
660 mktac (PrepFill n ns) = prep_fill n ns
661 mktac CompleteFill = complete_fill
662 mktac Regret = regret
663 mktac Solve = solve
664 mktac (StartUnify n) = start_unify n
665 mktac Compute = compute
666 mktac HNF_Compute = hnf_compute
667 mktac (Intro n) = intro n
668 mktac (IntroTy ty n) = introTy ty n
669 mktac (Forall n t) = forall n t
670 mktac (LetBind n t v) = letbind n t v
671 mktac (Rewrite t) = rewrite t
672 mktac (PatVar n) = patvar n
673 mktac (PatBind n) = patbind n
674 mktac (CheckIn r) = check_in r
675 mktac (EvalIn r) = eval_in r
676 mktac (Focus n) = focus n
677 mktac (Defer n) = defer n
678 mktac (DeferType n t a) = deferType n t a
679 mktac (Instance n) = instanceArg n
680 mktac (SetInjective n) = setinj n
681 mktac (MoveLast n) = movelast n