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