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