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