git.iko.soy/Idris-dev
on 0cb9b4e help sign in
Idris-dev/src/Idris/Core/ProofState.hs
1134 lines 51 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 Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
9 doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
11import Idris.Core.Typecheck
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import Idris.Core.Unify
15import Idris.Core.ProofTerm
17import Control.Monad.State.Strict
18import Control.Applicative hiding (empty)
19import Control.Arrow ((***))
20import Data.List
21import Debug.Trace
23import Util.Pretty hiding (fill)
25data ProofState = PS { thname :: Name,
26 holes :: [Name], -- ^ holes still to be solved
27 usedns :: [Name], -- ^ used names, don't use again
28 nextname :: Int, -- ^ name supply
29 pterm :: ProofTerm, -- ^ current proof term
30 ptype :: Type, -- ^ original goal
31 dontunify :: [Name], -- ^ explicitly given by programmer, leave it
32 unified :: (Name, [(Name, Term)]),
33 notunified :: [(Name, Term)],
34 dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment
35 -- either hole or something in env must turn up in the 'notunified' list during elaboration
36 solved :: Maybe (Name, Term),
37 problems :: Fails,
38 injective :: [Name],
39 deferred :: [Name], -- ^ names we'll need to define
40 instances :: [Name], -- ^ instance arguments (for type classes)
41 autos :: [(Name, ([FailContext], [Name]))], -- ^ unsolved 'auto' implicits with their holes
42 psnames :: [Name], -- ^ Local names okay to use in proof search
43 previous :: Maybe ProofState, -- ^ for undo
44 context :: Context,
45 datatypes :: Ctxt TypeInfo,
46 plog :: String,
47 unifylog :: Bool,
48 done :: Bool,
49 recents :: [Name],
50 while_elaborating :: [FailContext]
51 }
53data Tactic = Attack
54 | Claim Name Raw
55 | ClaimFn Name Name Raw
56 | Reorder Name
57 | Exact Raw
58 | Fill Raw
59 | MatchFill Raw
60 | PrepFill Name [Name]
61 | CompleteFill
62 | Regret
63 | Solve
64 | StartUnify Name
65 | EndUnify
66 | UnifyAll
67 | Compute
68 | ComputeLet Name
69 | Simplify
70 | HNF_Compute
71 | EvalIn Raw
72 | CheckIn Raw
73 | Intro (Maybe Name)
74 | IntroTy Raw (Maybe Name)
75 | Forall Name (Maybe ImplicitInfo) Raw
76 | LetBind Name Raw Raw
77 | ExpandLet Name Term
78 | Rewrite Raw
79 | Induction Raw
80 | CaseTac Raw
81 | Equiv Raw
82 | PatVar Name
83 | PatBind Name
84 | Focus Name
85 | Defer [Name] Name
86 | DeferType Name Raw [Name]
87 | Instance Name
88 | AutoArg Name
89 | SetInjective Name
90 | MoveLast Name
91 | MatchProblems Bool
92 | UnifyProblems
93 | UnifyGoal Raw
94 | UnifyTerms Raw Raw
95 | ProofState
96 | Undo
97 | QED
98 deriving Show
100-- Some utilites on proof and tactic states
102instance Show ProofState where
103 show ps | [] <- holes ps
104 = show (thname ps) ++ ": no more goals"
105 show ps | (h : hs) <- holes ps
106 = let tm = pterm ps
107 nm = thname ps
108 OK g = goal (Just h) tm
109 wkenv = premises g in
110 "Other goals: " ++ show hs ++ "\n" ++
111 showPs wkenv (reverse wkenv) ++ "\n" ++
112 "-------------------------------- (" ++ show nm ++
113 ") -------\n " ++
114 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
115 where showPs env [] = ""
116 showPs env ((n, Let t v):bs)
117 = " " ++ show n ++ " : " ++
118 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
119 showEnv env ({- normalise ctxt env -} v) ++
120 "\n" ++ showPs env bs
121 showPs env ((n, b):bs)
122 = " " ++ show n ++ " : " ++
123 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
124 "\n" ++ showPs env bs
125 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
126 " =?= " ++ showEnv ps v
127 showG ps b = showEnv ps (binderTy b)
129instance Pretty ProofState OutputAnnotation where
130 pretty ps | [] <- holes ps =
131 pretty (thname ps) <+> colon <+> text " no more goals."
132 pretty ps | (h : hs) <- holes ps =
133 let tm = pterm ps
134 OK g = goal (Just h) tm
135 nm = thname ps in
136 let wkEnv = premises g in
137 text "Other goals" <+> colon <+> pretty hs <+>
138 prettyPs wkEnv (reverse wkEnv) <+>
139 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
140 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
141 where
142 prettyGoal ps (Guess t v) =
143 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
144 prettyGoal ps b = prettyEnv ps $ binderTy b
146 prettyPs env [] = empty
147 prettyPs env ((n, Let t v):bs) =
148 nest nestingSize (pretty n <+> colon <+>
149 prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
150 nest nestingSize (prettyPs env bs))
151 prettyPs env ((n, b):bs) =
152 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
153 nest nestingSize (prettyPs env bs))
155holeName i = sMN i "hole"
157qshow :: Fails -> String
158qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)
160match_unify' :: Context -> Env ->
161 (TT Name, Maybe Provenance) ->
162 (TT Name, Maybe Provenance) ->
163 StateT TState TC [(Name, TT Name)]
164match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
165 do ps <- get
166 let while = while_elaborating ps
167 let dont = dontunify ps
168 let inj = injective ps
169 traceWhen (unifylog ps)
170 ("Matching " ++ show (topx, topy) ++
171 " in " ++ show env ++
172 "\nHoles: " ++ show (holes ps)
173 ++ "\n"
174 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
175 ) $
176 case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of
177 OK u -> traceWhen (unifylog ps)
178 ("Matched " ++ show u) $
179 do let (h, ns) = unified ps
180 put (ps { unified = (h, u ++ ns) })
181 return u
182 Error e -> traceWhen (unifylog ps)
183 ("No match " ++ show e) $
184 do put (ps { problems = (topx, topy, True,
185 env, e, while, Match) :
186 problems ps })
187 return []
188-- traceWhen (unifylog ps)
189-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++
190-- "\nSolved: " ++ show u
191-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)
192-- -- ++ show (pterm ps)
193-- ++ "\n----------") $
195mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
196mergeSolutions env ns = merge [] ns
197 where
198 merge acc [] = return (reverse acc)
199 merge acc ((n, t) : ns)
200 | Just t' <- lookup n ns
201 = do ps <- get
202 let probs = problems ps
203 put (ps { problems = probs ++ [(t,t',True,env,
204 CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
205 [], Unify)] })
206 merge acc ns
207 | otherwise = merge ((n, t): acc) ns
209dropSwaps :: [(Name, TT Name)] -> [(Name, TT Name)]
210dropSwaps [] = []
211dropSwaps (p@(x, P _ y _) : xs) | solvedIn y x xs = dropSwaps xs
212 where solvedIn _ _ [] = False
213 solvedIn y x ((y', P _ x' _) : xs) | y == y' && x == x' = True
214 solvedIn y x (_ : xs) = solvedIn y x xs
215dropSwaps (p : xs) = p : dropSwaps xs
217unify' :: Context -> Env ->
218 (TT Name, Maybe Provenance) ->
219 (TT Name, Maybe Provenance) ->
220 StateT TState TC [(Name, TT Name)]
221unify' ctxt env (topx, xfrom) (topy, yfrom) =
222 do ps <- get
223 let while = while_elaborating ps
224 let dont = dontunify ps
225 let inj = injective ps
226 (u, fails) <- traceWhen (unifylog ps)
227 ("Trying " ++ show (topx, topy) ++
228 "\nNormalised " ++ show (normalise ctxt env topx,
229 normalise ctxt env topy) ++
230 " in\n" ++ show env ++
231 "\nHoles: " ++ show (holes ps)
232 ++ "\nInjective: " ++ show (injective ps)
233 ++ "\n") $
234 lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)
235 (map fst (notunified ps)) while
236 let notu = filter (\ (n, t) -> case t of
237-- P _ _ _ -> False
238 _ -> n `elem` dont) u
239 traceWhen (unifylog ps)
240 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
241 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
242 ++ "\nNot unified:\n" ++ show (notunified ps)
243 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
244-- ++ show (pterm ps)
245 ++ "\n----------") $
246 do let (h, ns) = unified ps
247 -- solve in results (maybe unify should do this itself...)
248 let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
249 -- if a metavar has multiple solutions, make a new unification
250 -- problem for each.
251 uns <- mergeSolutions env (u' ++ ns)
252 ps <- get
253 let (ns_p, probs') = updateProblems ps uns (fails ++ problems ps)
254 let ns' = dropSwaps ns_p
255 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
256 traceWhen (unifylog ps)
257 ("Now solved: " ++ show ns' ++
258 "\nNow problems: " ++ qshow (probs' ++ probs_notu) ++
259 "\nNow injective: " ++ show (updateInj u (injective ps))) $
260 put (ps { problems = probs' ++ probs_notu,
261 unified = (h, ns'),
262 injective = updateInj u (injective ps),
263 notunified = notu' })
264 return u
265 where updateInj ((n, a) : us) inj
266 | (P _ n' _, _) <- unApply a,
267 n `elem` inj = updateInj us (n':inj)
268 | (P _ n' _, _) <- unApply a,
269 n' `elem` inj = updateInj us (n:inj)
270 updateInj (_ : us) inj = updateInj us inj
271 updateInj [] inj = inj
273nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
274nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
276dropUntil :: (a -> Bool) -> [a] -> [a]
277dropUntil p [] = []
278dropUntil p (x:xs) | p x = xs
279 | otherwise = dropUntil p xs
281doneElaboratingAppPS :: Name -> ProofState -> ProofState
282doneElaboratingAppPS f ps = let while = while_elaborating ps
283 while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
284 in ps { while_elaborating = while' }
286doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
287doneElaboratingArgPS f x ps = let while = while_elaborating ps
288 while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
289 in ps { while_elaborating = while' }
291getName :: Monad m => String -> StateT TState m Name
292getName tag = do ps <- get
293 let n = nextname ps
294 put (ps { nextname = n+1 })
295 return $ sMN n tag
297action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
298action a = do ps <- get
299 put (a ps)
301query :: Monad m => (ProofState -> r) -> StateT TState m r
302query q = do ps <- get
303 return $ q ps
305addLog :: Monad m => String -> StateT TState m ()
306addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
308newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
309newProof n ctxt datatypes ty =
310 let h = holeName 0
311 ty' = vToP ty
312 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
313 (P Bound h ty'))) ty [] (h, []) [] []
314 Nothing [] []
315 [] [] [] []
316 Nothing ctxt datatypes "" False False [] []
318type TState = ProofState -- [TacticAction])
319type RunTactic = RunTactic' TState
321envAtFocus :: ProofState -> TC Env
322envAtFocus ps
323 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
324 return (premises g)
325 | otherwise = fail "No holes"
327goalAtFocus :: ProofState -> TC (Binder Type)
328goalAtFocus ps
329 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
330 return (goalType g)
331 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
333tactic :: Hole -> RunTactic -> StateT TState TC ()
334tactic h f = do ps <- get
335 (tm', _) <- atHole h f (context ps) [] (pterm ps)
336 ps <- get -- might have changed while processing
337 put (ps { pterm = tm' })
339computeLet :: Context -> Name -> Term -> Term
340computeLet ctxt n tm = cl [] tm where
341 cl env (Bind n' (Let t v) sc)
342 | n' == n = let v' = normalise ctxt env v in
343 Bind n' (Let t v') sc
344 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
345 cl env (App s f a) = App s (cl env f) (cl env a)
346 cl env t = t
348attack :: RunTactic
349attack ctxt env (Bind x (Hole t) sc)
350 = do h <- getName "hole"
351 action (\ps -> ps { holes = h : holes ps })
352 return $ Bind x (Guess t (newtm h)) sc
353 where
354 newtm h = Bind h (Hole t) (P Bound h t)
355attack ctxt env _ = fail "Not an attackable hole"
357claim :: Name -> Raw -> RunTactic
358claim n ty ctxt env t =
359 do (tyv, tyt) <- lift $ check ctxt env ty
360 lift $ isType ctxt env tyt
361 action (\ps -> let (g:gs) = holes ps in
362 ps { holes = g : n : gs } )
363 return $ Bind n (Hole tyv) t
365-- If the current goal is 'retty', make a claim which is a function that
366-- can compute a retty from argty (i.e a claim 'argty -> retty')
367claimFn :: Name -> Name -> Raw -> RunTactic
368claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =
369 do (tyv, tyt) <- lift $ check ctxt env argty
370 lift $ isType ctxt env tyt
371 action (\ps -> let (g:gs) = holes ps in
372 ps { holes = g : n : gs } )
373 return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t
374claimFn _ _ _ ctxt env _ = fail "Can't make function type here"
376reorder_claims :: RunTactic
377reorder_claims ctxt env t
378 = -- trace (showSep "\n" (map show (scvs t))) $
379 let (bs, sc) = scvs t []
380 newbs = reverse (sortB (reverse bs)) in
381 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
382 return (bindAll newbs sc)
383 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
384 scvs sc acc = (reverse acc, sc)
386 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
387 sortB [] = []
388 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
389 | otherwise = sortB (insertB x xs)
391 insertB x [] = [x]
392 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
393 | otherwise = y : insertB x ys
395 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
396 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
397 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
399focus :: Name -> RunTactic
400focus n ctxt env t = do action (\ps -> let hs = holes ps in
401 if n `elem` hs
402 then ps { holes = n : (hs \\ [n]) }
403 else ps)
404 ps <- get
405 return t
407movelast :: Name -> RunTactic
408movelast n ctxt env t = do action (\ps -> let hs = holes ps in
409 if n `elem` hs
410 then ps { holes = (hs \\ [n]) ++ [n] }
411 else ps)
412 return t
414instanceArg :: Name -> RunTactic
415instanceArg n ctxt env (Bind x (Hole t) sc)
416 = do action (\ps -> let hs = holes ps
417 is = instances ps in
418 ps { holes = (hs \\ [x]) ++ [x],
419 instances = x:is })
420 return (Bind x (Hole t) sc)
421instanceArg n ctxt env _
422 = fail "The current focus is not a hole."
424autoArg :: Name -> RunTactic
425autoArg n ctxt env (Bind x (Hole t) sc)
426 = do action (\ps -> case lookup x (autos ps) of
427 Nothing ->
428 let hs = holes ps in
429 ps { holes = (hs \\ [x]) ++ [x],
430 autos = (x, (while_elaborating ps, refsIn t)) : autos ps }
431 Just _ -> ps)
432 return (Bind x (Hole t) sc)
433autoArg n ctxt env _
434 = fail "The current focus not a hole."
436setinj :: Name -> RunTactic
437setinj n ctxt env (Bind x b sc)
438 = do action (\ps -> let is = injective ps in
439 ps { injective = n : is })
440 return (Bind x b sc)
442defer :: [Name] -> Name -> RunTactic
443defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
444 do let env' = filter (\(n, t) -> n `notElem` dropped) env
445 action (\ps -> let hs = holes ps in
446 ps { usedns = n : usedns ps,
447 holes = hs \\ [x] })
448 ps <- get
449 return (Bind n (GHole (length env') (psnames ps) (mkTy (reverse env') t))
450 (mkApp (P Ref n ty) (map getP (reverse env'))))
451 where
452 mkTy [] t = t
453 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
455 getP (n, b) = P Bound n (binderTy b)
456defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."
458-- as defer, but build the type and application explicitly
459deferType :: Name -> Raw -> [Name] -> RunTactic
460deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
461 do (fty, _) <- lift $ check ctxt env fty_in
462 action (\ps -> let hs = holes ps
463 ds = deferred ps in
464 ps { holes = hs \\ [x],
465 deferred = n : ds })
466 return (Bind n (GHole 0 [] fty)
467 (mkApp (P Ref n ty) (map getP args)))
468 where
469 getP n = case lookup n env of
470 Just b -> P Bound n (binderTy b)
471 Nothing -> error ("deferType can't find " ++ show n)
472deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."
474regret :: RunTactic
475regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
476 do action (\ps -> let hs = holes ps in
477 ps { holes = hs \\ [x] })
478 return sc
479regret ctxt env (Bind x (Hole t) _)
480 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
481regret _ _ _ = fail "The current focus is not a hole."
483unifyGoal :: Raw -> RunTactic
484unifyGoal tm ctxt env h@(Bind x b sc) =
485 do (tmv, _) <- lift $ check ctxt env tm
486 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
487 return h
488unifyGoal _ _ _ _ = fail "The focus is not a binder."
490unifyTerms :: Raw -> Raw -> RunTactic
491unifyTerms tm1 tm2 ctxt env h =
492 do (tm1v, _) <- lift $ check ctxt env tm1
493 (tm2v, _) <- lift $ check ctxt env tm2
494 ns' <- unify' ctxt env (tm1v, Nothing) (tm2v, Nothing)
495 return h
497exact :: Raw -> RunTactic
498exact guess ctxt env (Bind x (Hole ty) sc) =
499 do (val, valty) <- lift $ check ctxt env guess
500 lift $ converts ctxt env valty ty
501 return $ Bind x (Guess ty val) sc
502exact _ _ _ _ = fail "Can't fill here."
504-- As exact, but attempts to solve other goals by unification
506fill :: Raw -> RunTactic
507fill guess ctxt env (Bind x (Hole ty) sc) =
508 do (val, valty) <- lift $ check ctxt env guess
509-- let valtyn = normalise ctxt env valty
510-- let tyn = normalise ctxt env ty
511 ns <- unify' ctxt env (valty, Just $ SourceTerm val)
512 (ty, Just (chkPurpose val ty))
513 ps <- get
514 let (uh, uns) = unified ps
515-- put (ps { unified = (uh, uns ++ ns) })
516-- addLog (show (uh, uns ++ ns))
517 return $ Bind x (Guess ty val) sc
518 where
519 -- some expected types show up commonly in errors and indicate a
520 -- specific problem.
521 -- argTy -> retTy suggests a function applied to too many arguments
522 chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))
523 = TooManyArgs val
524 chkPurpose _ _ = ExpectedType
525fill _ _ _ _ = fail "Can't fill here."
527-- As fill, but attempts to solve other goals by matching
529match_fill :: Raw -> RunTactic
530match_fill guess ctxt env (Bind x (Hole ty) sc) =
531 do (val, valty) <- lift $ check ctxt env guess
532-- let valtyn = normalise ctxt env valty
533-- let tyn = normalise ctxt env ty
534 ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
535 (ty, Just ExpectedType)
536 ps <- get
537 let (uh, uns) = unified ps
538-- put (ps { unified = (uh, uns ++ ns) })
539-- addLog (show (uh, uns ++ ns))
540 return $ Bind x (Guess ty val) sc
541match_fill _ _ _ _ = fail "Can't fill here."
543prep_fill :: Name -> [Name] -> RunTactic
544prep_fill f as ctxt env (Bind x (Hole ty) sc) =
545 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
546 return $ Bind x (Guess ty val) sc
547prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
549complete_fill :: RunTactic
550complete_fill ctxt env (Bind x (Guess ty val) sc) =
551 do let guess = forget val
552 (val', valty) <- lift $ check ctxt env guess
553 ns <- unify' ctxt env (valty, Just $ SourceTerm val')
554 (ty, Just ExpectedType)
555 ps <- get
556 let (uh, uns) = unified ps
557-- put (ps { unified = (uh, uns ++ ns) })
558 return $ Bind x (Guess ty val) sc
559complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
561-- When solving something in the 'dont unify' set, we should check
562-- that the guess we are solving it with unifies with the thing unification
563-- found for it, if anything.
565solve :: RunTactic
566solve ctxt env (Bind x (Guess ty val) sc)
567 = do ps <- get
568 let (uh, uns) = unified ps
569 dropdots <-
570 case lookup x (notunified ps) of
571 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
572 do match_unify' ctxt env (tm, Just InferredVal)
573 (val, Just GivenVal)
574 return [x]
575 _ -> return []
576 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
577 holes ps \\ [x],
578 solved = Just (x, val),
579 dontunify = filter (/= x) (dontunify ps),
580 notunified = updateNotunified [(x,val)]
581 (notunified ps),
582 recents = x : recents ps,
583 instances = instances ps \\ [x],
584 dotted = dropUnified dropdots (dotted ps) })
585 let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
586 return locked
587 where dropUnified ddots [] = []
588 dropUnified ddots ((x, es) : ds)
589 | x `elem` ddots || any (\e -> e `elem` ddots) es
590 = dropUnified ddots ds
591 | otherwise = (x, es) : dropUnified ddots ds
593 tryLock :: [Name] -> Term -> (Term, Bool)
594 tryLock hs tm@(App Complete _ _) = (tm, True)
595 tryLock hs tm@(App s f a) =
596 let (f', fl) = tryLock hs f
597 (a', al) = tryLock hs a in
598 if fl && al then (App Complete f' a', True)
599 else (App s f' a', False)
600 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)
601 tryLock hs t@(Bind n (Hole _) sc) = (t, False)
602 tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)
603 tryLock hs t@(Bind n (Let ty val) sc)
604 = let (ty', tyl) = tryLock hs ty
605 (val', vall) = tryLock hs val
606 (sc', scl) = tryLock hs sc in
607 (Bind n (Let ty' val') sc', tyl && vall && scl)
608 tryLock hs t@(Bind n b sc)
609 = let (bt', btl) = tryLock hs (binderTy b)
610 (val', vall) = tryLock hs val
611 (sc', scl) = tryLock hs sc in
612 (Bind n (b { binderTy = bt' }) sc', btl && scl)
613 tryLock hs t = (t, True)
615solve _ _ h@(Bind x t sc)
616 = do ps <- get
617 case findType x sc of
618 Just t -> lift $ tfail (CantInferType (show t))
619 _ -> lift $ tfail (IncompleteTerm h)
620 where findType x (Bind n (Let t v) sc)
621 = findType x v `mplus` findType x sc
622 findType x (Bind n t sc)
623 | P _ x' _ <- binderTy t, x == x' = Just n
624 | otherwise = findType x sc
625 findType x _ = Nothing
627introTy :: Raw -> Maybe Name -> RunTactic
628introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
629 do let n = case mn of
630 Just name -> name
631 Nothing -> x
632 let t' = case t of
633 x@(Bind y (Pi _ s _) _) -> x
634 _ -> hnf ctxt env t
635 (tyv, tyt) <- lift $ check ctxt env ty
636-- ns <- lift $ unify ctxt env tyv t'
637 case t' of
638 Bind y (Pi _ s _) t -> let t' = updsubst y (P Bound n s) t in
639 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
640 ps <- get
641 let (uh, uns) = unified ps
642-- put (ps { unified = (uh, uns ++ ns) })
643 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
644 _ -> lift $ tfail $ CantIntroduce t'
645introTy ty n ctxt env _ = fail "Can't introduce here."
647intro :: Maybe Name -> RunTactic
648intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
649 do let t' = case t of
650 x@(Bind y (Pi _ s _) _) -> x
651 _ -> hnf ctxt env t
652 case t' of
653 Bind y (Pi _ s _) t ->
654 let n = case mn of
655 Just name -> name
656 Nothing -> y
657 -- It's important that this be subst and not updsubst,
658 -- because we want to substitute even in portions of
659 -- terms that we know do not contain holes.
660 t' = subst y (P Bound n s) t
661 in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
662 _ -> lift $ tfail $ CantIntroduce t'
663intro n ctxt env _ = fail "Can't introduce here."
665forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
666forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
667 do (tyv, tyt) <- lift $ check ctxt env ty
668 unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)
669 unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)
670 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
671forall n impl ty ctxt env _ = fail "Can't pi bind here"
673patvar :: Name -> RunTactic
674patvar n ctxt env (Bind x (Hole t) sc) =
675 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
676 holes ps \\ [x],
677 solved = Just (x, P Bound n t),
678 dontunify = filter (/=x) (dontunify ps),
679 notunified = updateNotunified [(x,P Bound n t)]
680 (notunified ps),
681 injective = addInj n x (injective ps)
682 })
683 return $ Bind n (PVar t) (updsubst x (P Bound n t) sc)
684 where addInj n x ps | x `elem` ps = n : ps
685 | otherwise = ps
686patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
688letbind :: Name -> Raw -> Raw -> RunTactic
689letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
690 do (tyv, tyt) <- lift $ check ctxt env ty
691 (valv, valt) <- lift $ check ctxt env val
692 lift $ isType ctxt env tyt
693 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
694letbind n ty val ctxt env _ = fail "Can't let bind here"
696expandLet :: Name -> Term -> RunTactic
697expandLet n v ctxt env tm =
698 return $ updsubst n v tm
700rewrite :: Raw -> RunTactic
701rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
702 do (tmv, tmt) <- lift $ check ctxt env tm
703 let tmt' = normalise ctxt env tmt
704 case unApply tmt' of
705 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
706 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
707 let newt = mkP l r l t
708 let sc = forget $ (Bind x (Hole newt)
709 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))
710 [lt, l, r, p, tmv, xp]))
711 (scv, sct) <- lift $ check ctxt env sc
712 return scv
713 _ -> lift $ tfail (NotEquality tmv tmt')
714 where rname = sMN 0 "replaced"
715rewrite _ _ _ _ = fail "Can't rewrite here"
717-- To make the P for rewrite, replace syntactic occurrences of l in ty with
718-- an x, and put \x : lt in front
719mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
720mkP lt l r ty | l == ty = lt
721mkP lt l r (App s f a) = let f' = if (r /= f) then mkP lt l r f else f
722 a' = if (r /= a) then mkP lt l r a else a in
723 App s f' a'
724mkP lt l r (Bind n b sc)
725 = let b' = mkPB b
726 sc' = if (r /= sc) then mkP lt l r sc else sc in
727 Bind n b' sc'
728 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
729 v' = if (r /= v) then mkP lt l r v else v in
730 Let t' v'
731 mkPB b = let ty = binderTy b
732 ty' = if (r /= ty) then mkP lt l r ty else ty in
733 b { binderTy = ty' }
734mkP lt l r x = x
736casetac :: Raw -> Bool -> RunTactic
737casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
738 (tmv, tmt) <- lift $ check ctxt env tm
739 let tmt' = normalise ctxt env tmt
740 let (tacn, tacstr, tactt) = if induction
741 then (ElimN, "eliminator", "Induction")
742 else (CaseN (FC' emptyFC), "case analysis", "Case analysis")
743 case unApply tmt' of
744 (P _ tnm _, tyargs) -> do
745 case lookupTy (SN (tacn tnm)) ctxt of
746 [elimTy] -> do
747 param_pos <- case lookupMetaInformation tnm ctxt of
748 [DataMI param_pos] -> return param_pos
749 m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
750 _ -> return []
751 let (params, indicies) = splitTyArgs param_pos tyargs
752 let args = getArgTys elimTy
753 let pmargs = take (length params) args
754 let args' = drop (length params) args
755 let propTy = head args'
756 let restargs = init $ tail args'
757 let consargs = take (length restargs - length indicies) $ restargs
758 let indxargs = drop (length restargs - length indicies) $ restargs
759 let scr = last $ tail args'
760 let indxnames = makeIndexNames indicies
761 currentNames <- query $ allTTNames . getProofTerm . pterm
762 let tmnm = case tm of
763 Var nm -> uniqueNameCtxt ctxt nm currentNames
764 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
765 let tmvar = P Bound tmnm tmt'
766 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
767 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
768 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
769 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
770 action (\ps -> ps {holes = holes ps \\ [x],
771 recents = x : recents ps })
772 mapM_ addConsHole (reverse consargs')
773 let res' = forget $ res
774 (scv, sct) <- lift $ check ctxt env res'
775 let (scv', _) = specialise ctxt env [] scv
776 return scv'
777 [] -> lift $ tfail $ NoEliminator tacstr tmt'
778 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
779 _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
780 tmt'
781 where scname = sMN 0 "scarg"
782 makeConsArg (nm, ty) = P Bound nm ty
783 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
784 bindConsArgs [] v = v
785 addConsHole (nm, ty) =
786 action (\ps -> ps { holes = nm : holes ps })
787 splitTyArgs param_pos tyargs =
788 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
789 in (map snd params, map snd indicies)
790 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
791 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
792 let var = P Bound idnm idxt
793 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
794casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"
797equiv :: Raw -> RunTactic
798equiv tm ctxt env (Bind x (Hole t) sc) =
799 do (tmv, tmt) <- lift $ check ctxt env tm
800 lift $ converts ctxt env tmv t
801 return $ Bind x (Hole tmv) sc
802equiv tm ctxt env _ = fail "Can't equiv here"
804patbind :: Name -> RunTactic
805patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
806 do let t' = case t of
807 x@(Bind y (PVTy s) t) -> x
808 _ -> hnf ctxt env t
809 case t' of
810 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in
811 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
812 _ -> fail "Nothing to pattern bind"
813patbind n ctxt env _ = fail "Can't pattern bind here"
815compute :: RunTactic
816compute ctxt env (Bind x (Hole ty) sc) =
817 do return $ Bind x (Hole (normalise ctxt env ty)) sc
818compute ctxt env t = return t
820hnf_compute :: RunTactic
821hnf_compute ctxt env (Bind x (Hole ty) sc) =
822 do let ty' = hnf ctxt env ty in
823-- trace ("HNF " ++ show (ty, ty')) $
824 return $ Bind x (Hole ty') sc
825hnf_compute ctxt env t = return t
827-- reduce let bindings only
828simplify :: RunTactic
829simplify ctxt env (Bind x (Hole ty) sc) =
830 do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
831simplify ctxt env t = return t
833check_in :: Raw -> RunTactic
834check_in t ctxt env tm =
835 do (val, valty) <- lift $ check ctxt env t
836 addLog (showEnv env val ++ " : " ++ showEnv env valty)
837 return tm
839eval_in :: Raw -> RunTactic
840eval_in t ctxt env tm =
841 do (val, valty) <- lift $ check ctxt env t
842 let val' = normalise ctxt env val
843 let valty' = normalise ctxt env valty
844 addLog (showEnv env val ++ " : " ++
845 showEnv env valty ++
846-- " in " ++ show env ++
847 " ==>\n " ++
848 showEnv env val' ++ " : " ++
849 showEnv env valty')
850 return tm
852start_unify :: Name -> RunTactic
853start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
854 return tm
856tmap f (a, b, c) = (f a, b, c)
858solve_unified :: RunTactic
859solve_unified ctxt env tm =
860 do ps <- get
861 let (_, ns) = unified ps
862 let unify = dropGiven (dontunify ps) ns (holes ps)
863 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
864 holes ps \\ map fst unify,
865 recents = recents ps ++ map fst unify })
866 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
867 return (updateSolvedTerm unify tm)
869dropGiven du [] hs = []
870dropGiven du ((n, P Bound t ty) : us) hs
871 | n `elem` du && not (t `elem` du)
872 && n `elem` hs && t `elem` hs
873 = (t, P Bound n ty) : dropGiven du us hs
874dropGiven du (u@(n, _) : us) hs
875 | n `elem` du = dropGiven du us hs
876-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
877dropGiven du (u : us) hs = u : dropGiven du us hs
879keepGiven du [] hs = []
880keepGiven du ((n, P Bound t ty) : us) hs
881 | n `elem` du && not (t `elem` du)
882 && n `elem` hs && t `elem` hs
883 = keepGiven du us hs
884keepGiven du (u@(n, _) : us) hs
885 | n `elem` du = u : keepGiven du us hs
886keepGiven du (u : us) hs = keepGiven du us hs
888updateEnv [] e = e
889updateEnv ns [] = []
890updateEnv ns ((n, b) : env)
891 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
893updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t
894updateProv ns p = p
896updateError [] err = err
897updateError ns (At f e) = At f (updateError ns e)
898updateError ns (Elaborating s n ty e) = Elaborating s n ty (updateError ns e)
899updateError ns (ElaboratingArg f a env e)
900 = ElaboratingArg f a env (updateError ns e)
901updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
902 = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)
903 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
904updateError ns e = e
906updateRes ns [] = []
907updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts
909solveInProblems x val [] = []
910solveInProblems x val ((l, r, env, err) : ps)
911 = ((psubst x val l, psubst x val r,
912 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
914mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
915mergeNotunified env holes ns = mnu ns [] [] where
916 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
917 mnu ((n, t):ns) ns_acc ps_acc
918 | Just t' <- lookup n ns, t /= t'
919 = mnu ns ((n,t') : ns_acc)
920 ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)
921 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
923updateNotunified [] nu = nu
924updateNotunified ns nu = up nu where
925 up [] = []
926 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
927 ((n, t') : up nus)
929getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
930getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)
931getProvenance _ = (Nothing, Nothing)
933setReady (x, y, _, env, err, c, at) = (x, y, True, env, err, c, at)
935updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
936 -> ([(Name, TT Name)], Fails)
937-- updateProblems ctxt [] ps inj holes = ([], ps)
938updateProblems ps updates probs = rec 10 updates probs
939 where
940 -- keep trying if we make progress, but not too many times...
941 rec 0 us fs = (us, fs)
942 rec n us fs = case up us [] fs of
943 res@(_, []) -> res
944 res@(us', _) | length us' == length us -> res
945 (us', fs') -> rec (n - 1) us' fs'
947 hs = holes ps
948 inj = injective ps
949 ctxt = context ps
950 ulog = unifylog ps
951 usupp = map fst (notunified ps)
952 dont = dontunify ps
954 up ns acc [] = (ns, map (updateNs ns) (reverse acc))
955 up ns acc (prob@(x, y, ready, env, err, while, um) : ps) =
956 let (x', newx) = updateSolvedTerm' ns x
957 (y', newy) = updateSolvedTerm' ns y
958 (lp, rp) = getProvenance err
959 err' = updateError ns err
960 env' = updateEnv ns env in
961 if newx || newy || ready ||
962 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
963 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
964 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
965 let v' = filter (\(n, _) -> n `notElem` dont) v in
966 up (ns ++ v') acc ps
967 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
968 up ns ((x',y',False,env',err',while,um) : acc) ps
969 else -- trace ("SKIPPING " ++ show (x,y,ready)) $
970 up ns ((x',y', False, env',err', while, um) : acc) ps
972 updateNs ns (x, y, t, env, err, fc, fa)
973 = let (x', newx) = updateSolvedTerm' ns x
974 (y', newy) = updateSolvedTerm' ns y in
975 (x', y', newx || newy,
976 updateEnv ns env, updateError ns err, fc, fa)
978-- attempt to solve remaining problems with match_unify
979matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
980 -> ([(Name, TT Name)], Fails)
981matchProblems all ps updates probs = up updates probs where
982 hs = holes ps
983 inj = injective ps
984 ctxt = context ps
986 up ns [] = (ns, [])
987 up ns ((x, y, ready, env, err, while, um) : ps)
988 | all || um == Match =
989 let x' = updateSolvedTerm ns x
990 y' = updateSolvedTerm ns y
991 (lp, rp) = getProvenance err
992 err' = updateError ns err
993 env' = updateEnv ns env in
994 case match_unify ctxt env' (x', lp) (y', rp) inj hs while of
995 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
996 up (ns ++ v) ps
997 _ -> let (ns', ps') = up ns ps in
998 (ns', (x', y', True, env', err', while, um) : ps')
999 up ns (p : ps) = let (ns', ps') = up ns ps in
1000 (ns', p : ps')
1002processTactic :: Tactic -> ProofState -> TC (ProofState, String)
1003processTactic QED ps = case holes ps of
1004 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)
1005 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
1006 return (ps { done = True, pterm = mkProofTerm tm' },
1007 "Proof complete: " ++ showEnv [] tm')
1008 _ -> fail "Still holes to fill."
1009processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
1010processTactic Undo ps = case previous ps of
1011 Nothing -> Error . Msg $ "Nothing to undo."
1012 Just pold -> return (pold, "")
1013processTactic EndUnify ps
1014 = let (h, ns_in) = unified ps
1015 ns = dropGiven (dontunify ps) ns_in (holes ps)
1016 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
1017 (ns'', probs') = updateProblems ps ns' (problems ps)
1018 tm' = updateSolved ns'' (pterm ps) in
1019 traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $
1020 return (ps { pterm = tm',
1021 unified = (h, []),
1022 problems = probs',
1023 notunified = updateNotunified ns'' (notunified ps),
1024 recents = recents ps ++ map fst ns'',
1025 holes = holes ps \\ map fst ns'' }, "")
1026processTactic UnifyAll ps
1027 = let tm' = updateSolved (notunified ps) (pterm ps) in
1028 return (ps { pterm = tm',
1029 notunified = [],
1030 recents = recents ps ++ map fst (notunified ps),
1031 holes = holes ps \\ map fst (notunified ps) }, "")
1032processTactic (Reorder n) ps
1033 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
1034 return (ps' { previous = Just ps, plog = "" }, plog ps')
1035processTactic (ComputeLet n) ps
1036 = return (ps { pterm = mkProofTerm $
1037 computeLet (context ps) n
1038 (getProofTerm (pterm ps)) }, "")
1039processTactic UnifyProblems ps
1040 = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))
1041 pterm' = updateSolved ns' (pterm ps)
1042 traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
1043 return (ps { pterm = pterm', solved = Nothing, problems = probs',
1044 previous = Just ps, plog = "",
1045 notunified = updateNotunified ns' (notunified ps),
1046 recents = recents ps ++ map fst ns',
1047 dotted = filter (notIn ns') (dotted ps),
1048 holes = holes ps \\ (map fst ns') }, plog ps)
1049 where notIn ns (h, _) = h `notElem` map fst ns
1050processTactic (MatchProblems all) ps
1051 = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))
1052 (ns'', probs'') = matchProblems all ps ns' probs'
1053 pterm' = orderUpdateSolved ns'' (resetProofTerm (pterm ps))
1054 traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show ns'') $
1055 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
1056 previous = Just ps, plog = "",
1057 notunified = updateNotunified ns'' (notunified ps),
1058 recents = recents ps ++ map fst ns'',
1059 holes = holes ps \\ (map fst ns'') }, plog ps)
1060 where
1061 orderUpdateSolved [] t = t
1062 orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)
1063processTactic t ps
1064 = case holes ps of
1065 [] -> case t of
1066 Focus _ -> return (ps, "") -- harmless to refocus when done, since
1067 -- 'focus' doesn't fail
1068 _ -> fail $ "Nothing to fill in."
1069 (h:_) -> do ps' <- execStateT (process t h) ps
1070 let (ns_in, probs')
1071 = case solved ps' of
1072 Just s -> traceWhen (unifylog ps)
1073 ("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $
1074 updateProblems ps' [s] (problems ps')
1075 _ -> ([], problems ps')
1076 -- rechecking problems may find more solutions, so
1077 -- apply them here
1078 let ns' = dropGiven (dontunify ps') ns_in (holes ps')
1079 let pterm'' = updateSolved ns' (pterm ps')
1080 traceWhen (unifylog ps)
1081 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++
1082 "(Toplevel) Dropping holes: " ++ show (map fst ns') ++ "\n" ++
1083 "Holes were: " ++ show (holes ps')) $
1084 return (ps' { pterm = pterm'',
1085 solved = Nothing,
1086 problems = probs',
1087 notunified = updateNotunified ns' (notunified ps'),
1088 previous = Just ps, plog = "",
1089 recents = recents ps' ++ map fst ns',
1090 holes = holes ps' \\ (map fst ns')
1091 }, plog ps')
1093process :: Tactic -> Name -> StateT TState TC ()
1094process EndUnify _
1095 = do ps <- get
1096 let (h, _) = unified ps
1097 tactic (Just h) solve_unified
1098process t h = tactic (Just h) (mktac t)
1099 where mktac Attack = attack
1100 mktac (Claim n r) = claim n r
1101 mktac (ClaimFn n bn r) = claimFn n bn r
1102 mktac (Exact r) = exact r
1103 mktac (Fill r) = fill r
1104 mktac (MatchFill r) = match_fill r
1105 mktac (PrepFill n ns) = prep_fill n ns
1106 mktac CompleteFill = complete_fill
1107 mktac Solve = solve
1108 mktac (StartUnify n) = start_unify n
1109 mktac Compute = compute
1110 mktac Simplify = Idris.Core.ProofState.simplify
1111 mktac HNF_Compute = hnf_compute
1112 mktac (Intro n) = intro n
1113 mktac (IntroTy ty n) = introTy ty n
1114 mktac (Forall n i t) = forall n i t
1115 mktac (LetBind n t v) = letbind n t v
1116 mktac (ExpandLet n b) = expandLet n b
1117 mktac (Rewrite t) = rewrite t
1118 mktac (Induction t) = casetac t True
1119 mktac (CaseTac t) = casetac t False
1120 mktac (Equiv t) = equiv t
1121 mktac (PatVar n) = patvar n
1122 mktac (PatBind n) = patbind n
1123 mktac (CheckIn r) = check_in r
1124 mktac (EvalIn r) = eval_in r
1125 mktac (Focus n) = focus n
1126 mktac (Defer ns n) = defer ns n
1127 mktac (DeferType n t a) = deferType n t a
1128 mktac (Instance n) = instanceArg n
1129 mktac (AutoArg n) = autoArg n
1130 mktac (SetInjective n) = setinj n
1131 mktac (MoveLast n) = movelast n
1132 mktac (UnifyGoal r) = unifyGoal r
1133 mktac (UnifyTerms x y) = unifyTerms x y