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