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