git.iko.soy/Idris-dev
on 7871ecb help sign in
Idris-dev/src/Idris/Core/ProofState.hs
1048 lines 47 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
7module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
9 doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
11import Idris.Core.Typecheck
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import Idris.Core.Unify
15import Idris.Core.ProofTerm
17import Control.Monad.State.Strict
18import Control.Applicative hiding (empty)
19import Control.Arrow ((***))
20import Data.List
21import Debug.Trace
23import Util.Pretty hiding (fill)
25data ProofState = PS { thname :: Name,
26 holes :: [Name], -- ^ holes still to be solved
27 usedns :: [Name], -- ^ used names, don't use again
28 nextname :: Int, -- ^ name supply
29 pterm :: ProofTerm, -- ^ current proof term
30 ptype :: Type, -- ^ original goal
31 dontunify :: [Name], -- ^ explicitly given by programmer, leave it
32 unified :: (Name, [(Name, Term)]),
33 notunified :: [(Name, Term)],
34 dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment
35 -- either hole or something in env must turn up in the 'notunified' list during elaboration
36 solved :: Maybe (Name, Term),
37 problems :: Fails,
38 injective :: [Name],
39 deferred :: [Name], -- ^ names we'll need to define
40 instances :: [Name], -- ^ instance arguments (for type classes)
41 autos :: [(Name, [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 ->
158 (TT Name, Maybe Provenance) ->
159 (TT Name, Maybe Provenance) ->
160 StateT TState TC [(Name, TT Name)]
161match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
162 do ps <- get
163 let while = while_elaborating ps
164 let dont = dontunify ps
165 let inj = injective ps
166 traceWhen (unifylog ps)
167 ("Matching " ++ show (topx, topy) ++
168 " in " ++ show env ++
169 "\nHoles: " ++ show (holes ps)
170 ++ "\n"
171 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
172 ) $
173 case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of
174 OK u -> traceWhen (unifylog ps)
175 ("Matched " ++ show u) $
176 do let (h, ns) = unified ps
177 put (ps { unified = (h, u ++ ns) })
178 return u
179 Error e -> traceWhen (unifylog ps)
180 ("No match " ++ show e) $
181 do put (ps { problems = (topx, topy, True,
182 env, e, while, Match) :
183 problems ps })
184 return []
185-- traceWhen (unifylog ps)
186-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++
187-- "\nSolved: " ++ show u
188-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)
189-- -- ++ show (pterm ps)
190-- ++ "\n----------") $
192mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
193mergeSolutions env ns = merge [] ns
194 where
195 merge acc [] = return (reverse acc)
196 merge acc ((n, t) : ns)
197 | Just t' <- lookup n ns
198 = do ps <- get
199 let probs = problems ps
200 put (ps { problems = probs ++ [(t,t',True,env,
201 CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
202 [], Unify)] })
203 merge acc ns
204 | otherwise = merge ((n, t): acc) ns
206unify' :: Context -> Env ->
207 (TT Name, Maybe Provenance) ->
208 (TT Name, Maybe Provenance) ->
209 StateT TState TC [(Name, TT Name)]
210unify' ctxt env (topx, xfrom) (topy, yfrom) =
211 do ps <- get
212 let while = while_elaborating ps
213 let dont = dontunify ps
214 let inj = injective ps
215 (u, fails) <- traceWhen (unifylog ps)
216 ("Trying " ++ show (topx, topy) ++
217 "\nNormalised " ++ show (normalise ctxt env topx,
218 normalise ctxt env topy) ++
219 " in " ++ show env ++
220 "\nHoles: " ++ show (holes ps)
221 ++ "\nInjective: " ++ show (injective ps)
222 ++ "\n") $
223 lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)
224 (map fst (notunified ps)) while
225 let notu = filter (\ (n, t) -> case t of
226-- P _ _ _ -> False
227 _ -> n `elem` dont) u
228 traceWhen (unifylog ps)
229 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
230 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
231 ++ "\nNot unified:\n" ++ show (notunified ps)
232 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
233-- ++ show (pterm ps)
234 ++ "\n----------") $
235 do let (h, ns) = unified ps
236 -- solve in results (maybe unify should do this itself...)
237 let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
238 -- if a metavar has multiple solutions, make a new unification
239 -- problem for each.
240 uns <- mergeSolutions env (u' ++ ns)
241 ps <- get
242 let (ns', probs') = updateProblems ps uns (fails ++ problems ps)
243 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
244 traceWhen (unifylog ps)
245 ("Now solved: " ++ show ns' ++
246 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
247 put (ps { problems = probs' ++ probs_notu,
248 unified = (h, ns'),
249 injective = updateInj u (injective ps),
250 notunified = notu' })
251 return u
252 where updateInj ((n, a) : us) inj
253 | (P _ n' _, _) <- unApply a,
254 n `elem` inj = updateInj us (n':inj)
255 | (P _ n' _, _) <- unApply a,
256 n' `elem` inj = updateInj us (n:inj)
257 updateInj (_ : us) inj = updateInj us inj
258 updateInj [] inj = inj
260nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
261nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
263dropUntil :: (a -> Bool) -> [a] -> [a]
264dropUntil p [] = []
265dropUntil p (x:xs) | p x = xs
266 | otherwise = dropUntil p xs
268doneElaboratingAppPS :: Name -> ProofState -> ProofState
269doneElaboratingAppPS f ps = let while = while_elaborating ps
270 while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
271 in ps { while_elaborating = while' }
273doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
274doneElaboratingArgPS f x ps = let while = while_elaborating ps
275 while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
276 in ps { while_elaborating = while' }
278getName :: Monad m => String -> StateT TState m Name
279getName tag = do ps <- get
280 let n = nextname ps
281 put (ps { nextname = n+1 })
282 return $ sMN n tag
284action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
285action a = do ps <- get
286 put (a ps)
288query :: Monad m => (ProofState -> r) -> StateT TState m r
289query q = do ps <- get
290 return $ q ps
292addLog :: Monad m => String -> StateT TState m ()
293addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
295newProof :: Name -> Context -> Type -> ProofState
296newProof n ctxt ty = let h = holeName 0
297 ty' = vToP ty
298 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
299 (P Bound h ty'))) ty [] (h, []) [] []
300 Nothing [] []
301 [] [] []
302 Nothing ctxt "" False False [] []
304type TState = ProofState -- [TacticAction])
305type RunTactic = RunTactic' TState
307envAtFocus :: ProofState -> TC Env
308envAtFocus ps
309 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
310 return (premises g)
311 | otherwise = fail "No holes"
313goalAtFocus :: ProofState -> TC (Binder Type)
314goalAtFocus ps
315 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
316 return (goalType g)
317 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
319tactic :: Hole -> RunTactic -> StateT TState TC ()
320tactic h f = do ps <- get
321 (tm', _) <- atHole h f (context ps) [] (pterm ps)
322 ps <- get -- might have changed while processing
323 put (ps { pterm = tm' })
325computeLet :: Context -> Name -> Term -> Term
326computeLet ctxt n tm = cl [] tm where
327 cl env (Bind n' (Let t v) sc)
328 | n' == n = let v' = normalise ctxt env v in
329 Bind n' (Let t v') sc
330 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
331 cl env (App f a) = App (cl env f) (cl env a)
332 cl env t = t
334attack :: RunTactic
335attack ctxt env (Bind x (Hole t) sc)
336 = do h <- getName "hole"
337 action (\ps -> ps { holes = h : holes ps })
338 return $ Bind x (Guess t (newtm h)) sc
339 where
340 newtm h = Bind h (Hole t) (P Bound h t)
341attack ctxt env _ = fail "Not an attackable hole"
343claim :: Name -> Raw -> RunTactic
344claim n ty ctxt env t =
345 do (tyv, tyt) <- lift $ check ctxt env ty
346 lift $ isType ctxt env tyt
347 action (\ps -> let (g:gs) = holes ps in
348 ps { holes = g : n : gs } )
349 return $ Bind n (Hole tyv) t
351-- If the current goal is 'retty', make a claim which is a function that
352-- can compute a retty from argty (i.e a claim 'argty -> retty')
353claimFn :: Name -> Name -> Raw -> RunTactic
354claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =
355 do (tyv, tyt) <- lift $ check ctxt env argty
356 lift $ isType ctxt env tyt
357 action (\ps -> let (g:gs) = holes ps in
358 ps { holes = g : n : gs } )
359 return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t
360claimFn _ _ _ ctxt env _ = fail "Can't make function type here"
362reorder_claims :: RunTactic
363reorder_claims ctxt env t
364 = -- trace (showSep "\n" (map show (scvs t))) $
365 let (bs, sc) = scvs t []
366 newbs = reverse (sortB (reverse bs)) in
367 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
368 return (bindAll newbs sc)
369 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
370 scvs sc acc = (reverse acc, sc)
372 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
373 sortB [] = []
374 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
375 | otherwise = sortB (insertB x xs)
377 insertB x [] = [x]
378 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
379 | otherwise = y : insertB x ys
381 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
382 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
383 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
385focus :: Name -> RunTactic
386focus n ctxt env t = do action (\ps -> let hs = holes ps in
387 if n `elem` hs
388 then ps { holes = n : (hs \\ [n]) }
389 else ps)
390 ps <- get
391 return t
393movelast :: Name -> RunTactic
394movelast n ctxt env t = do action (\ps -> let hs = holes ps in
395 if n `elem` hs
396 then ps { holes = (hs \\ [n]) ++ [n] }
397 else ps)
398 return t
400instanceArg :: Name -> RunTactic
401instanceArg n ctxt env (Bind x (Hole t) sc)
402 = do action (\ps -> let hs = holes ps
403 is = instances ps in
404 ps { holes = (hs \\ [x]) ++ [x],
405 instances = x:is })
406 return (Bind x (Hole t) sc)
408autoArg :: Name -> RunTactic
409autoArg n ctxt env (Bind x (Hole t) sc)
410 = do action (\ps -> case lookup x (autos ps) of
411 Nothing ->
412 let hs = holes ps in
413 ps { holes = (hs \\ [x]) ++ [x],
414 autos = (x, refsIn t) : autos ps }
415 Just _ -> ps)
416 return (Bind x (Hole t) sc)
418setinj :: Name -> RunTactic
419setinj n ctxt env (Bind x b sc)
420 = do action (\ps -> let is = injective ps in
421 ps { injective = n : is })
422 return (Bind x b sc)
424defer :: [Name] -> Name -> RunTactic
425defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
426 do let env' = filter (\(n, t) -> n `notElem` dropped) env
427 action (\ps -> let hs = holes ps in
428 ps { holes = hs \\ [x] })
429 return (Bind n (GHole (length env') (mkTy (reverse env') t))
430 (mkApp (P Ref n ty) (map getP (reverse env'))))
431 where
432 mkTy [] t = t
433 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
435 getP (n, b) = P Bound n (binderTy b)
437-- as defer, but build the type and application explicitly
438deferType :: Name -> Raw -> [Name] -> RunTactic
439deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
440 do (fty, _) <- lift $ check ctxt env fty_in
441 action (\ps -> let hs = holes ps
442 ds = deferred ps in
443 ps { holes = hs \\ [x],
444 deferred = n : ds })
445 return (Bind n (GHole 0 fty)
446 (mkApp (P Ref n ty) (map getP args)))
447 where
448 getP n = case lookup n env of
449 Just b -> P Bound n (binderTy b)
450 Nothing -> error ("deferType can't find " ++ show n)
452regret :: RunTactic
453regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
454 do action (\ps -> let hs = holes ps in
455 ps { holes = hs \\ [x] })
456 return sc
457regret ctxt env (Bind x (Hole t) _)
458 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
460unifyGoal :: Raw -> RunTactic
461unifyGoal tm ctxt env h@(Bind x b sc) =
462 do (tmv, _) <- lift $ check ctxt env tm
463 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
464 return h
466exact :: Raw -> RunTactic
467exact guess ctxt env (Bind x (Hole ty) sc) =
468 do (val, valty) <- lift $ check ctxt env guess
469 lift $ converts ctxt env valty ty
470 return $ Bind x (Guess ty val) sc
471exact _ _ _ _ = fail "Can't fill here."
473-- As exact, but attempts to solve other goals by unification
475fill :: Raw -> RunTactic
476fill guess ctxt env (Bind x (Hole ty) sc) =
477 do (val, valty) <- lift $ check ctxt env guess
478-- let valtyn = normalise ctxt env valty
479-- let tyn = normalise ctxt env ty
480 ns <- unify' ctxt env (valty, Just $ SourceTerm val)
481 (ty, Just (chkPurpose val ty))
482 ps <- get
483 let (uh, uns) = unified ps
484-- put (ps { unified = (uh, uns ++ ns) })
485-- addLog (show (uh, uns ++ ns))
486 return $ Bind x (Guess ty val) sc
487 where
488 -- some expected types show up commonly in errors and indicate a
489 -- specific problem.
490 -- argTy -> retTy suggests a function applied to too many arguments
491 chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))
492 = TooManyArgs val
493 chkPurpose _ _ = ExpectedType
494fill _ _ _ _ = fail "Can't fill here."
496-- As fill, but attempts to solve other goals by matching
498match_fill :: Raw -> RunTactic
499match_fill guess ctxt env (Bind x (Hole ty) sc) =
500 do (val, valty) <- lift $ check ctxt env guess
501-- let valtyn = normalise ctxt env valty
502-- let tyn = normalise ctxt env ty
503 ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
504 (ty, Just ExpectedType)
505 ps <- get
506 let (uh, uns) = unified ps
507-- put (ps { unified = (uh, uns ++ ns) })
508-- addLog (show (uh, uns ++ ns))
509 return $ Bind x (Guess ty val) sc
510match_fill _ _ _ _ = fail "Can't fill here."
512prep_fill :: Name -> [Name] -> RunTactic
513prep_fill f as ctxt env (Bind x (Hole ty) sc) =
514 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
515 return $ Bind x (Guess ty val) sc
516prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
518complete_fill :: RunTactic
519complete_fill ctxt env (Bind x (Guess ty val) sc) =
520 do let guess = forget val
521 (val', valty) <- lift $ check ctxt env guess
522 ns <- unify' ctxt env (valty, Just $ SourceTerm val')
523 (ty, Just ExpectedType)
524 ps <- get
525 let (uh, uns) = unified ps
526-- put (ps { unified = (uh, uns ++ ns) })
527 return $ Bind x (Guess ty val) sc
528complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
530-- When solving something in the 'dont unify' set, we should check
531-- that the guess we are solving it with unifies with the thing unification
532-- found for it, if anything.
534solve :: RunTactic
535solve ctxt env (Bind x (Guess ty val) sc)
536 = do ps <- get
537 let (uh, uns) = unified ps
538 dropdots <-
539 case lookup x (notunified ps) of
540 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
541 do match_unify' ctxt env (tm, Just InferredVal)
542 (val, Just GivenVal)
543 return [x]
544 _ -> return []
545 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
546 holes ps \\ [x],
547 solved = Just (x, val),
548 dontunify = filter (/= x) (dontunify ps),
549 notunified = updateNotunified [(x,val)]
550 (notunified ps),
551 recents = x : recents ps,
552 instances = instances ps \\ [x],
553 dotted = dropUnified dropdots (dotted ps) })
554 let tm' = subst x val sc in
555 return tm'
556 where dropUnified ddots [] = []
557 dropUnified ddots ((x, es) : ds)
558 | x `elem` ddots || any (\e -> e `elem` ddots) es
559 = dropUnified ddots ds
560 | otherwise = (x, es) : dropUnified ddots ds
561solve _ _ h@(Bind x t sc)
562 = do ps <- get
563 case findType x sc of
564 Just t -> lift $ tfail (CantInferType (show t))
565 _ -> lift $ tfail (IncompleteTerm h)
566 where findType x (Bind n (Let t v) sc)
567 = findType x v `mplus` findType x sc
568 findType x (Bind n t sc)
569 | P _ x' _ <- binderTy t, x == x' = Just n
570 | otherwise = findType x sc
571 findType x _ = Nothing
573introTy :: Raw -> Maybe Name -> RunTactic
574introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
575 do let n = case mn of
576 Just name -> name
577 Nothing -> x
578 let t' = case t of
579 x@(Bind y (Pi _ s _) _) -> x
580 _ -> hnf ctxt env t
581 (tyv, tyt) <- lift $ check ctxt env ty
582-- ns <- lift $ unify ctxt env tyv t'
583 case t' of
584 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in
585 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
586 ps <- get
587 let (uh, uns) = unified ps
588-- put (ps { unified = (uh, uns ++ ns) })
589 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
590 _ -> lift $ tfail $ CantIntroduce t'
591introTy ty n ctxt env _ = fail "Can't introduce here."
593intro :: Maybe Name -> RunTactic
594intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
595 do let n = case mn of
596 Just name -> name
597 Nothing -> x
598 let t' = case t of
599 x@(Bind y (Pi _ s _) _) -> x
600 _ -> hnf ctxt env t
601 case t' of
602 Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $
603 let t' = subst y (P Bound n s) t in
604 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
605 _ -> lift $ tfail $ CantIntroduce t'
606intro n ctxt env _ = fail "Can't introduce here."
608forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
609forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
610 do (tyv, tyt) <- lift $ check ctxt env ty
611 unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)
612 unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)
613 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
614forall n impl ty ctxt env _ = fail "Can't pi bind here"
616patvar :: Name -> RunTactic
617patvar n ctxt env (Bind x (Hole t) sc) =
618 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
619 holes ps \\ [x],
620 solved = Just (x, P Bound n t),
621 dontunify = filter (/=x) (dontunify ps),
622 notunified = updateNotunified [(x,P Bound n t)]
623 (notunified ps),
624 injective = addInj n x (injective ps)
625 })
626 return $ Bind n (PVar t) (subst x (P Bound n t) sc)
627 where addInj n x ps | x `elem` ps = n : ps
628 | otherwise = ps
629patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
631letbind :: Name -> Raw -> Raw -> RunTactic
632letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
633 do (tyv, tyt) <- lift $ check ctxt env ty
634 (valv, valt) <- lift $ check ctxt env val
635 lift $ isType ctxt env tyt
636 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
637letbind n ty val ctxt env _ = fail "Can't let bind here"
639expandLet :: Name -> Term -> RunTactic
640expandLet n v ctxt env tm =
641 return $ subst n v tm
643rewrite :: Raw -> RunTactic
644rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
645 do (tmv, tmt) <- lift $ check ctxt env tm
646 let tmt' = normalise ctxt env tmt
647 case unApply tmt' of
648 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
649 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
650 let newt = mkP l r l t
651 let sc = forget $ (Bind x (Hole newt)
652 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))
653 [lt, l, r, p, tmv, xp]))
654 (scv, sct) <- lift $ check ctxt env sc
655 return scv
656 _ -> lift $ tfail (NotEquality tmv tmt')
657 where rname = sMN 0 "replaced"
658rewrite _ _ _ _ = fail "Can't rewrite here"
660-- To make the P for rewrite, replace syntactic occurrences of l in ty with
661-- an x, and put \x : lt in front
662mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
663mkP lt l r ty | l == ty = lt
664mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
665 a' = if (r /= a) then mkP lt l r a else a in
666 App f' a'
667mkP lt l r (Bind n b sc)
668 = let b' = mkPB b
669 sc' = if (r /= sc) then mkP lt l r sc else sc in
670 Bind n b' sc'
671 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
672 v' = if (r /= v) then mkP lt l r v else v in
673 Let t' v'
674 mkPB b = let ty = binderTy b
675 ty' = if (r /= ty) then mkP lt l r ty else ty in
676 b { binderTy = ty' }
677mkP lt l r x = x
679casetac :: Raw -> Bool -> RunTactic
680casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
681 (tmv, tmt) <- lift $ check ctxt env tm
682 let tmt' = normalise ctxt env tmt
683 let (tacn, tacstr, tactt) = if induction
684 then (ElimN, "eliminator", "Induction")
685 else (CaseN, "case analysis", "Case analysis")
686 case unApply tmt' of
687 (P _ tnm _, tyargs) -> do
688 case lookupTy (SN (tacn tnm)) ctxt of
689 [elimTy] -> do
690 param_pos <- case lookupMetaInformation tnm ctxt of
691 [DataMI param_pos] -> return param_pos
692 m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
693 _ -> return []
694 let (params, indicies) = splitTyArgs param_pos tyargs
695 let args = getArgTys elimTy
696 let pmargs = take (length params) args
697 let args' = drop (length params) args
698 let propTy = head args'
699 let restargs = init $ tail args'
700 let consargs = take (length restargs - length indicies) $ restargs
701 let indxargs = drop (length restargs - length indicies) $ restargs
702 let scr = last $ tail args'
703 let indxnames = makeIndexNames indicies
704 currentNames <- query $ allTTNames . getProofTerm . pterm
705 let tmnm = case tm of
706 Var nm -> uniqueNameCtxt ctxt nm currentNames
707 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
708 let tmvar = P Bound tmnm tmt'
709 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
710 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
711 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
712 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
713 action (\ps -> ps {holes = holes ps \\ [x],
714 recents = x : recents ps })
715 mapM_ addConsHole (reverse consargs')
716 let res' = forget $ res
717 (scv, sct) <- lift $ check ctxt env res'
718 let (scv', _) = specialise ctxt env [] scv
719 return scv'
720 [] -> lift $ tfail $ NoEliminator tacstr tmt'
721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
722 _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
723 tmt'
724 where scname = sMN 0 "scarg"
725 makeConsArg (nm, ty) = P Bound nm ty
726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
727 bindConsArgs [] v = v
728 addConsHole (nm, ty) =
729 action (\ps -> ps { holes = nm : holes ps })
730 splitTyArgs param_pos tyargs =
731 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
732 in (map snd params, map snd indicies)
733 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
734 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
735 let var = P Bound idnm idxt
736 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
737induction tm induction ctxt env _ = do fail "Can't do induction here"
740equiv :: Raw -> RunTactic
741equiv tm ctxt env (Bind x (Hole t) sc) =
742 do (tmv, tmt) <- lift $ check ctxt env tm
743 lift $ converts ctxt env tmv t
744 return $ Bind x (Hole tmv) sc
745equiv tm ctxt env _ = fail "Can't equiv here"
747patbind :: Name -> RunTactic
748patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
749 do let t' = case t of
750 x@(Bind y (PVTy s) t) -> x
751 _ -> hnf ctxt env t
752 case t' of
753 Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in
754 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
755 _ -> fail "Nothing to pattern bind"
756patbind n ctxt env _ = fail "Can't pattern bind here"
758compute :: RunTactic
759compute ctxt env (Bind x (Hole ty) sc) =
760 do return $ Bind x (Hole (normalise ctxt env ty)) sc
761compute ctxt env t = return t
763hnf_compute :: RunTactic
764hnf_compute ctxt env (Bind x (Hole ty) sc) =
765 do let ty' = hnf ctxt env ty in
766-- trace ("HNF " ++ show (ty, ty')) $
767 return $ Bind x (Hole ty') sc
768hnf_compute ctxt env t = return t
770-- reduce let bindings only
771simplify :: RunTactic
772simplify ctxt env (Bind x (Hole ty) sc) =
773 do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
774simplify ctxt env t = return t
776check_in :: Raw -> RunTactic
777check_in t ctxt env tm =
778 do (val, valty) <- lift $ check ctxt env t
779 addLog (showEnv env val ++ " : " ++ showEnv env valty)
780 return tm
782eval_in :: Raw -> RunTactic
783eval_in t ctxt env tm =
784 do (val, valty) <- lift $ check ctxt env t
785 let val' = normalise ctxt env val
786 let valty' = normalise ctxt env valty
787 addLog (showEnv env val ++ " : " ++
788 showEnv env valty ++
789-- " in " ++ show env ++
790 " ==>\n " ++
791 showEnv env val' ++ " : " ++
792 showEnv env valty')
793 return tm
795start_unify :: Name -> RunTactic
796start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
797 return tm
799tmap f (a, b, c) = (f a, b, c)
801solve_unified :: RunTactic
802solve_unified ctxt env tm =
803 do ps <- get
804 let (_, ns) = unified ps
805 let unify = dropGiven (dontunify ps) ns (holes ps)
806 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
807 holes ps \\ map fst unify,
808 recents = recents ps ++ map fst unify })
809 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
810 return (updateSolvedTerm unify tm)
812dropGiven du [] hs = []
813dropGiven du ((n, P Bound t ty) : us) hs
814 | n `elem` du && not (t `elem` du)
815 && n `elem` hs && t `elem` hs
816 = (t, P Bound n ty) : dropGiven du us hs
817dropGiven du (u@(n, _) : us) hs
818 | n `elem` du = dropGiven du us hs
819-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
820dropGiven du (u : us) hs = u : dropGiven du us hs
822keepGiven du [] hs = []
823keepGiven du ((n, P Bound t ty) : us) hs
824 | n `elem` du && not (t `elem` du)
825 && n `elem` hs && t `elem` hs
826 = keepGiven du us hs
827keepGiven du (u@(n, _) : us) hs
828 | n `elem` du = u : keepGiven du us hs
829keepGiven du (u : us) hs = keepGiven du us hs
831updateEnv [] e = e
832updateEnv ns [] = []
833updateEnv ns ((n, b) : env)
834 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
836updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t
837updateProv ns p = p
839updateError [] err = err
840updateError ns (At f e) = At f (updateError ns e)
841updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
842updateError ns (ElaboratingArg f a env e)
843 = ElaboratingArg f a env (updateError ns e)
844updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
845 = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)
846 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
847updateError ns e = e
849solveInProblems x val [] = []
850solveInProblems x val ((l, r, env, err) : ps)
851 = ((psubst x val l, psubst x val r,
852 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
854mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
855mergeNotunified env holes ns = mnu ns [] [] where
856 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
857 mnu ((n, t):ns) ns_acc ps_acc
858 | Just t' <- lookup n ns, t /= t'
859 = mnu ns ((n,t') : ns_acc)
860 ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)
861 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
863updateNotunified [] nu = nu
864updateNotunified ns nu = up nu where
865 up [] = []
866 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
867 ((n, t') : up nus)
869getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
870getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)
871getProvenance _ = (Nothing, Nothing)
873updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
874 -> ([(Name, TT Name)], Fails)
875-- updateProblems ctxt [] ps inj holes = ([], ps)
876updateProblems ps updates probs = up updates probs where
877 hs = holes ps
878 inj = injective ps
879 ctxt = context ps
880 ulog = unifylog ps
881 usupp = map fst (notunified ps)
882 dont = dontunify ps
884 up ns [] = (ns, [])
885 up ns (prob@(x, y, ready, env, err, while, um) : ps) =
886 let (x', newx) = updateSolvedTerm' ns x
887 (y', newy) = updateSolvedTerm' ns y
888 (lp, rp) = getProvenance err
889 err' = updateError ns err
890 env' = updateEnv ns env in
891 if newx || newy || ready ||
892 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
893 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
894 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
895 let v' = filter (\(n, _) -> n `notElem` dont) v in
896 up (ns ++ v') ps
897 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
898 let (ns', ps') = up ns ps in
899 (ns', (x',y', False, env',err', while, um) : ps')
900 else -- trace ("SKIPPING " ++ show (x,y,ready)) $
901 let (ns', ps') = up ns ps in
902 (ns', (x',y', False, env',err', while, um) : ps')
904-- attempt to solve remaining problems with match_unify
905matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
906 -> ([(Name, TT Name)], Fails)
907matchProblems all ps updates probs = up updates probs where
908 hs = holes ps
909 inj = injective ps
910 ctxt = context ps
912 up ns [] = (ns, [])
913 up ns ((x, y, ready, env, err, while, um) : ps)
914 | all || um == Match =
915 let x' = updateSolvedTerm ns x
916 y' = updateSolvedTerm ns y
917 (lp, rp) = getProvenance err
918 err' = updateError ns err
919 env' = updateEnv ns env in
920 case match_unify ctxt env' (x', lp) (y', rp) inj hs while of
921 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
922 up (ns ++ v) ps
923 _ -> let (ns', ps') = up ns ps in
924 (ns', (x', y', True, env', err', while, um) : ps')
925 up ns (p : ps) = let (ns', ps') = up ns ps in
926 (ns', p : ps')
928processTactic :: Tactic -> ProofState -> TC (ProofState, String)
929processTactic QED ps = case holes ps of
930 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)
931 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
932 return (ps { done = True, pterm = mkProofTerm tm' },
933 "Proof complete: " ++ showEnv [] tm')
934 _ -> fail "Still holes to fill."
935processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
936processTactic Undo ps = case previous ps of
937 Nothing -> Error . Msg $ "Nothing to undo."
938 Just pold -> return (pold, "")
939processTactic EndUnify ps
940 = let (h, ns_in) = unified ps
941 ns = dropGiven (dontunify ps) ns_in (holes ps)
942 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
943 (ns'', probs') = updateProblems ps ns' (problems ps)
944 tm' = updateSolved ns'' (pterm ps) in
945 traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $
946 return (ps { pterm = tm',
947 unified = (h, []),
948 problems = probs',
949 notunified = updateNotunified ns'' (notunified ps),
950 recents = recents ps ++ map fst ns'',
951 holes = holes ps \\ map fst ns'' }, "")
952processTactic UnifyAll ps
953 = let tm' = updateSolved (notunified ps) (pterm ps) in
954 return (ps { pterm = tm',
955 notunified = [],
956 recents = recents ps ++ map fst (notunified ps),
957 holes = holes ps \\ map fst (notunified ps) }, "")
958processTactic (Reorder n) ps
959 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
960 return (ps' { previous = Just ps, plog = "" }, plog ps')
961processTactic (ComputeLet n) ps
962 = return (ps { pterm = mkProofTerm $
963 computeLet (context ps) n
964 (getProofTerm (pterm ps)) }, "")
965processTactic UnifyProblems ps
966 = do let (ns', probs') = updateProblems ps [] (problems ps)
967 pterm' = updateSolved ns' (pterm ps)
968 traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
969 return (ps { pterm = pterm', solved = Nothing, problems = probs',
970 previous = Just ps, plog = "",
971 notunified = updateNotunified ns' (notunified ps),
972 recents = recents ps ++ map fst ns',
973 holes = holes ps \\ (map fst ns') }, plog ps)
974processTactic (MatchProblems all) ps
975 = do let (ns', probs') = matchProblems all ps [] (problems ps)
976 (ns'', probs'') = matchProblems all ps ns' probs'
977 pterm' = updateSolved ns'' (pterm ps)
978 traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show (map fst ns'')) $
979 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
980 previous = Just ps, plog = "",
981 notunified = updateNotunified ns'' (notunified ps),
982 recents = recents ps ++ map fst ns'',
983 holes = holes ps \\ (map fst ns'') }, plog ps)
984processTactic t ps
985 = case holes ps of
986 [] -> fail "Nothing to fill in."
987 (h:_) -> do ps' <- execStateT (process t h) ps
988 let (ns_in, probs')
989 = case solved ps' of
990 Just s -> traceWhen (unifylog ps)
991 ("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $
992 updateProblems ps' [s] (problems ps')
993 _ -> ([], problems ps')
994 -- rechecking problems may find more solutions, so
995 -- apply them here
996 let ns' = dropGiven (dontunify ps') ns_in (holes ps')
997 let pterm'' = updateSolved ns' (pterm ps')
998 traceWhen (unifylog ps)
999 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++
1000 "(Toplevel) Dropping holes: " ++ show (map fst ns')) $
1001 return (ps' { pterm = pterm'',
1002 solved = Nothing,
1003 problems = probs',
1004 notunified = updateNotunified ns' (notunified ps'),
1005 previous = Just ps, plog = "",
1006 recents = recents ps' ++ map fst ns',
1007 holes = holes ps' \\ (map fst ns')}, plog ps')
1009process :: Tactic -> Name -> StateT TState TC ()
1010process EndUnify _
1011 = do ps <- get
1012 let (h, _) = unified ps
1013 tactic (Just h) solve_unified
1014process t h = tactic (Just h) (mktac t)
1015 where mktac Attack = attack
1016 mktac (Claim n r) = claim n r
1017 mktac (ClaimFn n bn r) = claimFn n bn r
1018 mktac (Exact r) = exact r
1019 mktac (Fill r) = fill r
1020 mktac (MatchFill r) = match_fill r
1021 mktac (PrepFill n ns) = prep_fill n ns
1022 mktac CompleteFill = complete_fill
1023 mktac Solve = solve
1024 mktac (StartUnify n) = start_unify n
1025 mktac Compute = compute
1026 mktac Simplify = Idris.Core.ProofState.simplify
1027 mktac HNF_Compute = hnf_compute
1028 mktac (Intro n) = intro n
1029 mktac (IntroTy ty n) = introTy ty n
1030 mktac (Forall n i t) = forall n i t
1031 mktac (LetBind n t v) = letbind n t v
1032 mktac (ExpandLet n b) = expandLet n b
1033 mktac (Rewrite t) = rewrite t
1034 mktac (Induction t) = casetac t True
1035 mktac (CaseTac t) = casetac t False
1036 mktac (Equiv t) = equiv t
1037 mktac (PatVar n) = patvar n
1038 mktac (PatBind n) = patbind n
1039 mktac (CheckIn r) = check_in r
1040 mktac (EvalIn r) = eval_in r
1041 mktac (Focus n) = focus n
1042 mktac (Defer ns n) = defer ns n
1043 mktac (DeferType n t a) = deferType n t a
1044 mktac (Instance n) = instanceArg n
1045 mktac (AutoArg n) = autoArg n
1046 mktac (SetInjective n) = setinj n
1047 mktac (MoveLast n) = movelast n
1048 mktac (UnifyGoal r) = unifyGoal r