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