git.iko.soy/Idris-dev
on 85cf83f help sign in
Idris-dev/src/Idris/Core/ProofState.hs
993 lines 44 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 | Reorder Name
54 | Exact Raw
55 | Fill Raw
56 | MatchFill Raw
57 | PrepFill Name [Name]
58 | CompleteFill
59 | Regret
60 | Solve
61 | StartUnify Name
62 | EndUnify
63 | UnifyAll
64 | Compute
65 | ComputeLet Name
66 | Simplify
67 | HNF_Compute
68 | EvalIn Raw
69 | CheckIn Raw
70 | Intro (Maybe Name)
71 | IntroTy Raw (Maybe Name)
72 | Forall Name Raw
73 | LetBind Name Raw Raw
74 | ExpandLet Name Term
75 | Rewrite Raw
76 | Induction Raw
77 | CaseTac Raw
78 | Equiv Raw
79 | PatVar Name
80 | PatBind Name
81 | Focus Name
82 | Defer [Name] Name
83 | DeferType Name Raw [Name]
84 | Instance Name
85 | AutoArg Name
86 | SetInjective Name
87 | MoveLast Name
88 | MatchProblems Bool
89 | UnifyProblems
90 | ProofState
91 | Undo
92 | QED
93 deriving Show
95-- Some utilites on proof and tactic states
97instance Show ProofState where
98 show ps | [] <- holes ps
99 = show (thname ps) ++ ": no more goals"
100 show ps | (h : hs) <- holes ps
101 = let tm = pterm ps
102 nm = thname ps
103 OK g = goal (Just h) tm
104 wkenv = premises g in
105 "Other goals: " ++ show hs ++ "\n" ++
106 showPs wkenv (reverse wkenv) ++ "\n" ++
107 "-------------------------------- (" ++ show nm ++
108 ") -------\n " ++
109 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
110 where showPs env [] = ""
111 showPs env ((n, Let t v):bs)
112 = " " ++ show n ++ " : " ++
113 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
114 showEnv env ({- normalise ctxt env -} v) ++
115 "\n" ++ showPs env bs
116 showPs env ((n, b):bs)
117 = " " ++ show n ++ " : " ++
118 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
119 "\n" ++ showPs env bs
120 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
121 " =?= " ++ showEnv ps v
122 showG ps b = showEnv ps (binderTy b)
124instance Pretty ProofState OutputAnnotation where
125 pretty ps | [] <- holes ps =
126 pretty (thname ps) <+> colon <+> text " no more goals."
127 pretty ps | (h : hs) <- holes ps =
128 let tm = pterm ps
129 OK g = goal (Just h) tm
130 nm = thname ps in
131 let wkEnv = premises g in
132 text "Other goals" <+> colon <+> pretty hs <+>
133 prettyPs wkEnv (reverse wkEnv) <+>
134 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
135 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
136 where
137 prettyGoal ps (Guess t v) =
138 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
139 prettyGoal ps b = prettyEnv ps $ binderTy b
141 prettyPs env [] = empty
142 prettyPs env ((n, Let t v):bs) =
143 nest nestingSize (pretty n <+> colon <+>
144 prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
145 nest nestingSize (prettyPs env bs))
146 prettyPs env ((n, b):bs) =
147 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
148 nest nestingSize (prettyPs env bs))
150holeName i = sMN i "hole"
152qshow :: Fails -> String
153qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)
155match_unify' :: Context -> Env -> TT Name -> TT Name ->
156 StateT TState TC [(Name, TT Name)]
157match_unify' ctxt env topx topy =
158 do ps <- get
159 let while = while_elaborating ps
160 let dont = dontunify ps
161 let inj = injective ps
162 traceWhen (unifylog ps)
163 ("Matching " ++ show (topx, topy) ++
164 " in " ++ show env ++
165 "\nHoles: " ++ show (holes ps)
166 ++ "\n"
167 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
168 ) $
169 case match_unify ctxt env topx topy inj (holes ps) while of
170 OK u -> traceWhen (unifylog ps)
171 ("Matched " ++ show u) $
172 do let (h, ns) = unified ps
173 put (ps { unified = (h, u ++ ns) })
174 return u
175 Error e -> traceWhen (unifylog ps)
176 ("No match " ++ show e) $
177 do put (ps { problems = (topx, topy, True,
178 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',True,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 -- solve in results (maybe unify should do this itself...)
230 let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
231 -- if a metavar has multiple solutions, make a new unification
232 -- problem for each.
233 uns <- mergeSolutions env (u' ++ ns)
234 ps <- get
235 let (ns', probs') = updateProblems ps uns (fails ++ problems ps)
236 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
237 traceWhen (unifylog ps)
238 ("Now solved: " ++ show ns' ++
239 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
240 put (ps { problems = probs' ++ probs_notu,
241 unified = (h, ns'),
242 injective = updateInj u (injective ps),
243 notunified = notu' })
244 return u
245 where updateInj ((n, a) : us) inj
246 | (P _ n' _, _) <- unApply a,
247 n `elem` inj = updateInj us (n':inj)
248 | (P _ n' _, _) <- unApply a,
249 n' `elem` inj = updateInj us (n:inj)
250 updateInj (_ : us) inj = updateInj us inj
251 updateInj [] inj = inj
253nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
254nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
256dropUntil :: (a -> Bool) -> [a] -> [a]
257dropUntil p [] = []
258dropUntil p (x:xs) | p x = xs
259 | otherwise = dropUntil p xs
261doneElaboratingAppPS :: Name -> ProofState -> ProofState
262doneElaboratingAppPS f ps = let while = while_elaborating ps
263 while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
264 in ps { while_elaborating = while' }
266doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
267doneElaboratingArgPS f x ps = let while = while_elaborating ps
268 while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
269 in ps { while_elaborating = while' }
271getName :: Monad m => String -> StateT TState m Name
272getName tag = do ps <- get
273 let n = nextname ps
274 put (ps { nextname = n+1 })
275 return $ sMN n tag
277action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
278action a = do ps <- get
279 put (a ps)
281query :: Monad m => (ProofState -> r) -> StateT TState m r
282query q = do ps <- get
283 return $ q ps
285addLog :: Monad m => String -> StateT TState m ()
286addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
288newProof :: Name -> Context -> Type -> ProofState
289newProof n ctxt ty = let h = holeName 0
290 ty' = vToP ty in
291 PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
292 (P Bound h ty'))) ty [] (h, []) [] []
293 Nothing [] []
294 [] [] []
295 Nothing ctxt "" False False [] []
297type TState = ProofState -- [TacticAction])
298type RunTactic = RunTactic' TState
300envAtFocus :: ProofState -> TC Env
301envAtFocus ps
302 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
303 return (premises g)
304 | otherwise = fail "No holes"
306goalAtFocus :: ProofState -> TC (Binder Type)
307goalAtFocus ps
308 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
309 return (goalType g)
310 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
312tactic :: Hole -> RunTactic -> StateT TState TC ()
313tactic h f = do ps <- get
314 (tm', _) <- atHole h f (context ps) [] (pterm ps)
315 ps <- get -- might have changed while processing
316 put (ps { pterm = tm' })
318computeLet :: Context -> Name -> Term -> Term
319computeLet ctxt n tm = cl [] tm where
320 cl env (Bind n' (Let t v) sc)
321 | n' == n = let v' = normalise ctxt env v in
322 Bind n' (Let t v') sc
323 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
324 cl env (App f a) = App (cl env f) (cl env a)
325 cl env t = t
327attack :: RunTactic
328attack ctxt env (Bind x (Hole t) sc)
329 = do h <- getName "hole"
330 action (\ps -> ps { holes = h : holes ps })
331 return $ Bind x (Guess t (newtm h)) sc
332 where
333 newtm h = Bind h (Hole t) (P Bound h t)
334attack ctxt env _ = fail "Not an attackable hole"
336claim :: Name -> Raw -> RunTactic
337claim n ty ctxt env t =
338 do (tyv, tyt) <- lift $ check ctxt env ty
339 lift $ isType ctxt env tyt
340 action (\ps -> let (g:gs) = holes ps in
341 ps { holes = g : n : gs } )
342 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
344reorder_claims :: RunTactic
345reorder_claims ctxt env t
346 = -- trace (showSep "\n" (map show (scvs t))) $
347 let (bs, sc) = scvs t []
348 newbs = reverse (sortB (reverse bs)) in
349 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
350 return (bindAll newbs sc)
351 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
352 scvs sc acc = (reverse acc, sc)
354 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
355 sortB [] = []
356 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
357 | otherwise = sortB (insertB x xs)
359 insertB x [] = [x]
360 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
361 | otherwise = y : insertB x ys
363 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
364 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
365 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
367focus :: Name -> RunTactic
368focus n ctxt env t = do action (\ps -> let hs = holes ps in
369 if n `elem` hs
370 then ps { holes = n : (hs \\ [n]) }
371 else ps)
372 ps <- get
373 return t
375movelast :: Name -> RunTactic
376movelast n ctxt env t = do action (\ps -> let hs = holes ps in
377 if n `elem` hs
378 then ps { holes = (hs \\ [n]) ++ [n] }
379 else ps)
380 return t
382instanceArg :: Name -> RunTactic
383instanceArg n ctxt env (Bind x (Hole t) sc)
384 = do action (\ps -> let hs = holes ps
385 is = instances ps in
386 ps { holes = (hs \\ [x]) ++ [x],
387 instances = x:is })
388 return (Bind x (Hole t) sc)
390autoArg :: Name -> RunTactic
391autoArg n ctxt env (Bind x (Hole t) sc)
392 = do action (\ps -> case lookup x (autos ps) of
393 Nothing ->
394 let hs = holes ps in
395 ps { holes = (hs \\ [x]) ++ [x],
396 autos = (x, refsIn t) : autos ps }
397 Just _ -> ps)
398 return (Bind x (Hole t) sc)
400setinj :: Name -> RunTactic
401setinj n ctxt env (Bind x b sc)
402 = do action (\ps -> let is = injective ps in
403 ps { injective = n : is })
404 return (Bind x b sc)
406defer :: [Name] -> Name -> RunTactic
407defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
408 do let env' = filter (\(n, t) -> n `notElem` dropped) env
409 action (\ps -> let hs = holes ps in
410 ps { holes = hs \\ [x] })
411 return (Bind n (GHole (length env') (mkTy (reverse env') t))
412 (mkApp (P Ref n ty) (map getP (reverse env'))))
413 where
414 mkTy [] t = t
415 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b) (TType (UVar 0))) (mkTy bs t)
417 getP (n, b) = P Bound n (binderTy b)
419-- as defer, but build the type and application explicitly
420deferType :: Name -> Raw -> [Name] -> RunTactic
421deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
422 do (fty, _) <- lift $ check ctxt env fty_in
423 action (\ps -> let hs = holes ps
424 ds = deferred ps in
425 ps { holes = hs \\ [x],
426 deferred = n : ds })
427 return (Bind n (GHole 0 fty)
428 (mkApp (P Ref n ty) (map getP args)))
429 where
430 getP n = case lookup n env of
431 Just b -> P Bound n (binderTy b)
432 Nothing -> error ("deferType can't find " ++ show n)
434regret :: RunTactic
435regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
436 do action (\ps -> let hs = holes ps in
437 ps { holes = hs \\ [x] })
438 return sc
439regret ctxt env (Bind x (Hole t) _)
440 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
442exact :: Raw -> RunTactic
443exact guess ctxt env (Bind x (Hole ty) sc) =
444 do (val, valty) <- lift $ check ctxt env guess
445 lift $ converts ctxt env valty ty
446 return $ Bind x (Guess ty val) sc
447exact _ _ _ _ = fail "Can't fill here."
449-- As exact, but attempts to solve other goals by unification
451fill :: Raw -> RunTactic
452fill guess ctxt env (Bind x (Hole ty) sc) =
453 do (val, valty) <- lift $ check ctxt env guess
454-- let valtyn = normalise ctxt env valty
455-- let tyn = normalise ctxt env ty
456 ns <- unify' ctxt env valty ty
457 ps <- get
458 let (uh, uns) = unified ps
459-- put (ps { unified = (uh, uns ++ ns) })
460-- addLog (show (uh, uns ++ ns))
461 return $ Bind x (Guess ty val) sc
462fill _ _ _ _ = fail "Can't fill here."
464-- As fill, but attempts to solve other goals by matching
466match_fill :: Raw -> RunTactic
467match_fill guess ctxt env (Bind x (Hole ty) sc) =
468 do (val, valty) <- lift $ check ctxt env guess
469-- let valtyn = normalise ctxt env valty
470-- let tyn = normalise ctxt env ty
471 ns <- match_unify' ctxt env valty ty
472 ps <- get
473 let (uh, uns) = unified ps
474-- put (ps { unified = (uh, uns ++ ns) })
475-- addLog (show (uh, uns ++ ns))
476 return $ Bind x (Guess ty val) sc
477match_fill _ _ _ _ = fail "Can't fill here."
479prep_fill :: Name -> [Name] -> RunTactic
480prep_fill f as ctxt env (Bind x (Hole ty) sc) =
481 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
482 return $ Bind x (Guess ty val) sc
483prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
485complete_fill :: RunTactic
486complete_fill ctxt env (Bind x (Guess ty val) sc) =
487 do let guess = forget val
488 (val', valty) <- lift $ check ctxt env guess
489 ns <- unify' ctxt env valty ty
490 ps <- get
491 let (uh, uns) = unified ps
492-- put (ps { unified = (uh, uns ++ ns) })
493 return $ Bind x (Guess ty val) sc
494complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
496-- When solving something in the 'dont unify' set, we should check
497-- that the guess we are solving it with unifies with the thing unification
498-- found for it, if anything.
500solve :: RunTactic
501solve ctxt env (Bind x (Guess ty val) sc)
502 = do ps <- get
503 let (uh, uns) = unified ps
504 dropdots <-
505 case lookup x (notunified ps) of
506 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
507 do match_unify' ctxt env tm val
508 return [x]
509 _ -> return []
510 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
511 holes ps \\ [x],
512 solved = Just (x, val),
513 notunified = updateNotunified [(x,val)]
514 (notunified ps),
515 recents = x : recents ps,
516 instances = instances ps \\ [x],
517 dotted = dropUnified dropdots (dotted ps) })
518 let tm' = subst x val sc in
519 return tm'
520 where dropUnified ddots [] = []
521 dropUnified ddots ((x, es) : ds)
522 | x `elem` ddots || any (\e -> e `elem` ddots) es
523 = dropUnified ddots ds
524 | otherwise = (x, es) : dropUnified ddots ds
525solve _ _ h@(Bind x t sc)
526 = do ps <- get
527 case findType x sc of
528 Just t -> lift $ tfail (CantInferType (show t))
529 _ -> lift $ tfail (IncompleteTerm h)
530 where findType x (Bind n (Let t v) sc)
531 = findType x v `mplus` findType x sc
532 findType x (Bind n t sc)
533 | P _ x' _ <- binderTy t, x == x' = Just n
534 | otherwise = findType x sc
535 findType x _ = Nothing
537introTy :: Raw -> Maybe Name -> RunTactic
538introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
539 do let n = case mn of
540 Just name -> name
541 Nothing -> x
542 let t' = case t of
543 x@(Bind y (Pi s _) _) -> x
544 _ -> hnf ctxt env t
545 (tyv, tyt) <- lift $ check ctxt env ty
546-- ns <- lift $ unify ctxt env tyv t'
547 case t' of
548 Bind y (Pi s _) t -> let t' = subst y (P Bound n s) t in
549 do ns <- unify' ctxt env s tyv
550 ps <- get
551 let (uh, uns) = unified ps
552-- put (ps { unified = (uh, uns ++ ns) })
553 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
554 _ -> lift $ tfail $ CantIntroduce t'
555introTy ty n ctxt env _ = fail "Can't introduce here."
557intro :: Maybe Name -> RunTactic
558intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
559 do let n = case mn of
560 Just name -> name
561 Nothing -> x
562 let t' = case t of
563 x@(Bind y (Pi s _) _) -> x
564 _ -> hnf ctxt env t
565 case t' of
566 Bind y (Pi s _) t -> -- trace ("in type " ++ show t') $
567 let t' = subst y (P Bound n s) t in
568 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
569 _ -> lift $ tfail $ CantIntroduce t'
570intro n ctxt env _ = fail "Can't introduce here."
572forall :: Name -> Raw -> RunTactic
573forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
574 do (tyv, tyt) <- lift $ check ctxt env ty
575 unify' ctxt env tyt (TType (UVar 0))
576 unify' ctxt env t (TType (UVar 0))
577 return $ Bind n (Pi tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
578forall n ty ctxt env _ = fail "Can't pi bind here"
580patvar :: Name -> RunTactic
581patvar n ctxt env (Bind x (Hole t) sc) =
582 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
583 holes ps \\ [x],
584 solved = Just (x, P Bound n t),
585 notunified = updateNotunified [(x,P Bound n t)]
586 (notunified ps),
587 injective = addInj n x (injective ps)
588 })
589 return $ Bind n (PVar t) (subst x (P Bound n t) sc)
590 where addInj n x ps | x `elem` ps = n : ps
591 | otherwise = ps
592patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
594letbind :: Name -> Raw -> Raw -> RunTactic
595letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
596 do (tyv, tyt) <- lift $ check ctxt env ty
597 (valv, valt) <- lift $ check ctxt env val
598 lift $ isType ctxt env tyt
599 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
600letbind n ty val ctxt env _ = fail "Can't let bind here"
602expandLet :: Name -> Term -> RunTactic
603expandLet n v ctxt env tm =
604 return $ subst n v tm
606rewrite :: Raw -> RunTactic
607rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
608 do (tmv, tmt) <- lift $ check ctxt env tm
609 let tmt' = normalise ctxt env tmt
610 case unApply tmt' of
611 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
612 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
613 let newt = mkP l r l t
614 let sc = forget $ (Bind x (Hole newt)
615 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))
616 [lt, l, r, p, tmv, xp]))
617 (scv, sct) <- lift $ check ctxt env sc
618 return scv
619 _ -> lift $ tfail (NotEquality tmv tmt')
620 where rname = sMN 0 "replaced"
621rewrite _ _ _ _ = fail "Can't rewrite here"
623-- To make the P for rewrite, replace syntactic occurrences of l in ty with
624-- an x, and put \x : lt in front
625mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
626mkP lt l r ty | l == ty = lt
627mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
628 a' = if (r /= a) then mkP lt l r a else a in
629 App f' a'
630mkP lt l r (Bind n b sc)
631 = let b' = mkPB b
632 sc' = if (r /= sc) then mkP lt l r sc else sc in
633 Bind n b' sc'
634 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
635 v' = if (r /= v) then mkP lt l r v else v in
636 Let t' v'
637 mkPB b = let ty = binderTy b
638 ty' = if (r /= ty) then mkP lt l r ty else ty in
639 b { binderTy = ty' }
640mkP lt l r x = x
642casetac :: Raw -> Bool -> RunTactic
643casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
644 (tmv, tmt) <- lift $ check ctxt env tm
645 let tmt' = normalise ctxt env tmt
646 let (tacn, tacstr, tactt) = if induction
647 then (ElimN, "an eliminator", "Induction")
648 else (CaseN, "a case function", "Case analysis")
649 case unApply tmt' of
650 (P _ tnm _, tyargs) -> do
651 case lookupTy (SN (tacn tnm)) ctxt of
652 [elimTy] -> do
653 param_pos <- case lookupMetaInformation tnm ctxt of
654 [DataMI param_pos] -> return param_pos
655 m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
656 _ -> return []
657 let (params, indicies) = splitTyArgs param_pos tyargs
658 let args = getArgTys elimTy
659 let pmargs = take (length params) args
660 let args' = drop (length params) args
661 let propTy = head args'
662 let restargs = init $ tail args'
663 let consargs = take (length restargs - length indicies) $ restargs
664 let indxargs = drop (length restargs - length indicies) $ restargs
665 let scr = last $ tail args'
666 let indxnames = makeIndexNames indicies
667 currentNames <- query $ allTTNames . getProofTerm . pterm
668 let tmnm = case tm of
669 Var nm -> uniqueNameCtxt ctxt nm currentNames
670 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
671 let tmvar = P Bound tmnm tmt'
672 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
673 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
674 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
675 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
676 action (\ps -> ps {holes = holes ps \\ [x],
677 recents = x : recents ps })
678 mapM_ addConsHole (reverse consargs')
679 let res' = forget $ res
680 (scv, sct) <- lift $ check ctxt env res'
681 let (scv', _) = specialise ctxt env [] scv
682 return scv'
683 [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
684 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
685 _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
686 where scname = sMN 0 "scarg"
687 makeConsArg (nm, ty) = P Bound nm ty
688 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
689 bindConsArgs [] v = v
690 addConsHole (nm, ty) =
691 action (\ps -> ps { holes = nm : holes ps })
692 splitTyArgs param_pos tyargs =
693 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
694 in (map snd params, map snd indicies)
695 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
696 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
697 let var = P Bound idnm idxt
698 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
699induction tm induction ctxt env _ = do fail "Can't do induction here"
702equiv :: Raw -> RunTactic
703equiv tm ctxt env (Bind x (Hole t) sc) =
704 do (tmv, tmt) <- lift $ check ctxt env tm
705 lift $ converts ctxt env tmv t
706 return $ Bind x (Hole tmv) sc
707equiv tm ctxt env _ = fail "Can't equiv here"
709patbind :: Name -> RunTactic
710patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
711 do let t' = case t of
712 x@(Bind y (PVTy s) t) -> x
713 _ -> hnf ctxt env t
714 case t' of
715 Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in
716 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
717 _ -> fail "Nothing to pattern bind"
718patbind n ctxt env _ = fail "Can't pattern bind here"
720compute :: RunTactic
721compute ctxt env (Bind x (Hole ty) sc) =
722 do return $ Bind x (Hole (normalise ctxt env ty)) sc
723compute ctxt env t = return t
725hnf_compute :: RunTactic
726hnf_compute ctxt env (Bind x (Hole ty) sc) =
727 do let ty' = hnf ctxt env ty in
728-- trace ("HNF " ++ show (ty, ty')) $
729 return $ Bind x (Hole ty') sc
730hnf_compute ctxt env t = return t
732-- reduce let bindings only
733simplify :: RunTactic
734simplify ctxt env (Bind x (Hole ty) sc) =
735 do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
736simplify ctxt env t = return t
738check_in :: Raw -> RunTactic
739check_in t ctxt env tm =
740 do (val, valty) <- lift $ check ctxt env t
741 addLog (showEnv env val ++ " : " ++ showEnv env valty)
742 return tm
744eval_in :: Raw -> RunTactic
745eval_in t ctxt env tm =
746 do (val, valty) <- lift $ check ctxt env t
747 let val' = normalise ctxt env val
748 let valty' = normalise ctxt env valty
749 addLog (showEnv env val ++ " : " ++
750 showEnv env valty ++
751-- " in " ++ show env ++
752 " ==>\n " ++
753 showEnv env val' ++ " : " ++
754 showEnv env valty')
755 return tm
757start_unify :: Name -> RunTactic
758start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
759 return tm
761tmap f (a, b, c) = (f a, b, c)
763solve_unified :: RunTactic
764solve_unified ctxt env tm =
765 do ps <- get
766 let (_, ns) = unified ps
767 let unify = dropGiven (dontunify ps) ns (holes ps)
768 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
769 holes ps \\ map fst unify,
770 recents = recents ps ++ map fst unify })
771 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
772 return (updateSolvedTerm unify tm)
774dropGiven du [] hs = []
775dropGiven du ((n, P Bound t ty) : us) hs
776 | n `elem` du && not (t `elem` du)
777 && n `elem` hs && t `elem` hs
778 = (t, P Bound n ty) : dropGiven du us hs
779dropGiven du (u@(n, _) : us) hs
780 | n `elem` du = dropGiven du us hs
781-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
782dropGiven du (u : us) hs = u : dropGiven du us hs
784keepGiven du [] hs = []
785keepGiven du ((n, P Bound t ty) : us) hs
786 | n `elem` du && not (t `elem` du)
787 && n `elem` hs && t `elem` hs
788 = keepGiven du us hs
789keepGiven du (u@(n, _) : us) hs
790 | n `elem` du = u : keepGiven du us hs
791keepGiven du (u : us) hs = keepGiven du us hs
793updateEnv [] e = e
794updateEnv ns [] = []
795updateEnv ns ((n, b) : env)
796 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
798updateError [] err = err
799updateError ns (At f e) = At f (updateError ns e)
800updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
801updateError ns (ElaboratingArg f a env e)
802 = ElaboratingArg f a env (updateError ns e)
803updateError ns (CantUnify b l r e xs sc)
804 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc
805updateError ns e = e
807solveInProblems x val [] = []
808solveInProblems x val ((l, r, env, err) : ps)
809 = ((psubst x val l, psubst x val r,
810 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
812mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
813mergeNotunified env holes ns = mnu ns [] [] where
814 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
815 mnu ((n, t):ns) ns_acc ps_acc
816 | Just t' <- lookup n ns, t /= t'
817 = mnu ns ((n,t') : ns_acc)
818 ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)
819 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
821updateNotunified [] nu = nu
822updateNotunified ns nu = up nu where
823 up [] = []
824 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
825 ((n, t') : up nus)
827updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
828 -> ([(Name, TT Name)], Fails)
829-- updateProblems ctxt [] ps inj holes = ([], ps)
830updateProblems ps updates probs = up updates probs where
831 hs = holes ps
832 inj = injective ps
833 ctxt = context ps
834 usupp = map fst (notunified ps)
836 up ns [] = (ns, [])
837 up ns (prob@(x, y, ready, env, err, while, um) : ps) =
838 let (x', newx) = updateSolvedTerm' ns x
839 (y', newy) = updateSolvedTerm' ns y
840 err' = updateError ns err
841 env' = updateEnv ns env in
842 if newx || newy || ready ||
843 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
844 case unify ctxt env' x' y' inj hs usupp while of
845 OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $
846 up (ns ++ v) ps
847 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
848 let (ns', ps') = up ns ps in
849 (ns', (x',y', False, env',err', while, um) : ps')
850 else -- trace ("SKIPPING " ++ show (x,y,ready)) $
851 let (ns', ps') = up ns ps in
852 (ns', (x',y', False, env',err', while, um) : ps')
854-- attempt to solve remaining problems with match_unify
855matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
856 -> ([(Name, TT Name)], Fails)
857matchProblems all ps updates probs = up updates probs where
858 hs = holes ps
859 inj = injective ps
860 ctxt = context ps
862 up ns [] = (ns, [])
863 up ns ((x, y, ready, env, err, while, um) : ps)
864 | all || um == Match =
865 let x' = updateSolvedTerm ns x
866 y' = updateSolvedTerm ns y
867 err' = updateError ns err
868 env' = updateEnv ns env in
869 case match_unify ctxt env' x' y' inj hs while of
870 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
871 up (ns ++ v) ps
872 _ -> let (ns', ps') = up ns ps in
873 (ns', (x', y', True, env', err', while, um) : ps')
874 up ns (p : ps) = let (ns', ps') = up ns ps in
875 (ns', p : ps')
877processTactic :: Tactic -> ProofState -> TC (ProofState, String)
878processTactic QED ps = case holes ps of
879 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)
880 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
881 return (ps { done = True, pterm = mkProofTerm tm' },
882 "Proof complete: " ++ showEnv [] tm')
883 _ -> fail "Still holes to fill."
884processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
885processTactic Undo ps = case previous ps of
886 Nothing -> Error . Msg $ "Nothing to undo."
887 Just pold -> return (pold, "")
888processTactic EndUnify ps
889 = let (h, ns_in) = unified ps
890 ns = dropGiven (dontunify ps) ns_in (holes ps)
891 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
892 (ns'', probs') = updateProblems ps ns' (problems ps)
893 tm' = updateSolved ns'' (pterm ps) in
894 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $
895 return (ps { pterm = tm',
896 unified = (h, []),
897 problems = probs',
898 notunified = updateNotunified ns'' (notunified ps),
899 recents = recents ps ++ map fst ns'',
900 holes = holes ps \\ map fst ns'' }, "")
901processTactic UnifyAll ps
902 = let tm' = updateSolved (notunified ps) (pterm ps) in
903 return (ps { pterm = tm',
904 notunified = [],
905 recents = recents ps ++ map fst (notunified ps),
906 holes = holes ps \\ map fst (notunified ps) }, "")
907processTactic (Reorder n) ps
908 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
909 return (ps' { previous = Just ps, plog = "" }, plog ps')
910processTactic (ComputeLet n) ps
911 = return (ps { pterm = mkProofTerm $
912 computeLet (context ps) n
913 (getProofTerm (pterm ps)) }, "")
914processTactic UnifyProblems ps
915 = do let (ns', probs') = updateProblems ps [] (problems ps)
916 pterm' = updateSolved ns' (pterm ps)
917 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $
918 return (ps { pterm = pterm', solved = Nothing, problems = probs',
919 previous = Just ps, plog = "",
920 notunified = updateNotunified ns' (notunified ps),
921 recents = recents ps ++ map fst ns',
922 holes = holes ps \\ (map fst ns') }, plog ps)
923processTactic (MatchProblems all) ps
924 = do let (ns', probs') = matchProblems all ps [] (problems ps)
925 (ns'', probs'') = matchProblems all ps ns' probs'
926 pterm' = updateSolved ns'' (pterm ps)
927 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $
928 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
929 previous = Just ps, plog = "",
930 notunified = updateNotunified ns'' (notunified ps),
931 recents = recents ps ++ map fst ns'',
932 holes = holes ps \\ (map fst ns'') }, plog ps)
933processTactic t ps
934 = case holes ps of
935 [] -> fail "Nothing to fill in."
936 (h:_) -> do ps' <- execStateT (process t h) ps
937 let (ns', probs')
938 = case solved ps' of
939 Just s -> traceWhen (unifylog ps')
940 ("SOLVED " ++ show s) $
941 updateProblems ps [s] (problems ps')
942 _ -> ([], problems ps')
943 -- rechecking problems may find more solutions, so
944 -- apply them here
945 let pterm'' = updateSolved ns' (pterm ps')
946 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $
947 return (ps' { pterm = pterm'',
948 solved = Nothing,
949 problems = probs',
950 notunified = updateNotunified ns' (notunified ps'),
951 previous = Just ps, plog = "",
952 recents = recents ps' ++ map fst ns',
953 holes = holes ps' \\ (map fst ns')}, plog ps')
955process :: Tactic -> Name -> StateT TState TC ()
956process EndUnify _
957 = do ps <- get
958 let (h, _) = unified ps
959 tactic (Just h) solve_unified
960process t h = tactic (Just h) (mktac t)
961 where mktac Attack = attack
962 mktac (Claim n r) = claim n r
963 mktac (Exact r) = exact r
964 mktac (Fill r) = fill r
965 mktac (MatchFill r) = match_fill r
966 mktac (PrepFill n ns) = prep_fill n ns
967 mktac CompleteFill = complete_fill
968 mktac Regret = regret
969 mktac Solve = solve
970 mktac (StartUnify n) = start_unify n
971 mktac Compute = compute
972 mktac Simplify = Idris.Core.ProofState.simplify
973 mktac HNF_Compute = hnf_compute
974 mktac (Intro n) = intro n
975 mktac (IntroTy ty n) = introTy ty n
976 mktac (Forall n t) = forall n t
977 mktac (LetBind n t v) = letbind n t v
978 mktac (ExpandLet n b) = expandLet n b
979 mktac (Rewrite t) = rewrite t
980 mktac (Induction t) = casetac t True
981 mktac (CaseTac t) = casetac t False
982 mktac (Equiv t) = equiv t
983 mktac (PatVar n) = patvar n
984 mktac (PatBind n) = patbind n
985 mktac (CheckIn r) = check_in r
986 mktac (EvalIn r) = eval_in r
987 mktac (Focus n) = focus n
988 mktac (Defer ns n) = defer ns n
989 mktac (DeferType n t a) = deferType n t a
990 mktac (Instance n) = instanceArg n
991 mktac (AutoArg n) = autoArg n
992 mktac (SetInjective n) = setinj n
993 mktac (MoveLast n) = movelast n