git.iko.soy/Idris-dev
on aef8dc1 help sign in
Idris-dev/src/Idris/Core/ProofState.hs
994 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 (Maybe ImplicitInfo) 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,
197 CantUnify True t t' (Msg "") (errEnv env) 0,
198 [], Unify)] })
199 merge acc ns
200 | otherwise = merge ((n, t): acc) ns
202unify' :: Context -> Env -> TT Name -> TT Name ->
203 StateT TState TC [(Name, TT Name)]
204unify' ctxt env topx topy =
205 do ps <- get
206 let while = while_elaborating ps
207 let dont = dontunify ps
208 let inj = injective ps
209 (u, fails) <- traceWhen (unifylog ps)
210 ("Trying " ++ show (topx, topy) ++
211 "\nNormalised " ++ show (normalise ctxt env topx,
212 normalise ctxt env topy) ++
213 " in " ++ show env ++
214 "\nHoles: " ++ show (holes ps)
215 ++ "\nInjective: " ++ show (injective ps)
216 ++ "\n") $
217 lift $ unify ctxt env topx topy inj (holes ps)
218 (map fst (notunified ps)) while
219 let notu = filter (\ (n, t) -> case t of
220-- P _ _ _ -> False
221 _ -> n `elem` dont) u
222 traceWhen (unifylog ps)
223 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
224 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
225 ++ "\nNot unified:\n" ++ show (notunified ps)
226 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
227-- ++ show (pterm ps)
228 ++ "\n----------") $
229 do let (h, ns) = unified ps
230 -- solve in results (maybe unify should do this itself...)
231 let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
232 -- if a metavar has multiple solutions, make a new unification
233 -- problem for each.
234 uns <- mergeSolutions env (u' ++ ns)
235 ps <- get
236 let (ns', probs') = updateProblems ps uns (fails ++ problems ps)
237 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
238 traceWhen (unifylog ps)
239 ("Now solved: " ++ show ns' ++
240 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
241 put (ps { problems = probs' ++ probs_notu,
242 unified = (h, ns'),
243 injective = updateInj u (injective ps),
244 notunified = notu' })
245 return u
246 where updateInj ((n, a) : us) inj
247 | (P _ n' _, _) <- unApply a,
248 n `elem` inj = updateInj us (n':inj)
249 | (P _ n' _, _) <- unApply a,
250 n' `elem` inj = updateInj us (n:inj)
251 updateInj (_ : us) inj = updateInj us inj
252 updateInj [] inj = inj
254nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
255nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
257dropUntil :: (a -> Bool) -> [a] -> [a]
258dropUntil p [] = []
259dropUntil p (x:xs) | p x = xs
260 | otherwise = dropUntil p xs
262doneElaboratingAppPS :: Name -> ProofState -> ProofState
263doneElaboratingAppPS f ps = let while = while_elaborating ps
264 while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
265 in ps { while_elaborating = while' }
267doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
268doneElaboratingArgPS f x ps = let while = while_elaborating ps
269 while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
270 in ps { while_elaborating = while' }
272getName :: Monad m => String -> StateT TState m Name
273getName tag = do ps <- get
274 let n = nextname ps
275 put (ps { nextname = n+1 })
276 return $ sMN n tag
278action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
279action a = do ps <- get
280 put (a ps)
282query :: Monad m => (ProofState -> r) -> StateT TState m r
283query q = do ps <- get
284 return $ q ps
286addLog :: Monad m => String -> StateT TState m ()
287addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
289newProof :: Name -> Context -> Type -> ProofState
290newProof n ctxt ty = let h = holeName 0
291 ty' = vToP ty in
292 PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
293 (P Bound h ty'))) ty [] (h, []) [] []
294 Nothing [] []
295 [] [] []
296 Nothing ctxt "" False False [] []
298type TState = ProofState -- [TacticAction])
299type RunTactic = RunTactic' TState
301envAtFocus :: ProofState -> TC Env
302envAtFocus ps
303 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
304 return (premises g)
305 | otherwise = fail "No holes"
307goalAtFocus :: ProofState -> TC (Binder Type)
308goalAtFocus ps
309 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
310 return (goalType g)
311 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
313tactic :: Hole -> RunTactic -> StateT TState TC ()
314tactic h f = do ps <- get
315 (tm', _) <- atHole h f (context ps) [] (pterm ps)
316 ps <- get -- might have changed while processing
317 put (ps { pterm = tm' })
319computeLet :: Context -> Name -> Term -> Term
320computeLet ctxt n tm = cl [] tm where
321 cl env (Bind n' (Let t v) sc)
322 | n' == n = let v' = normalise ctxt env v in
323 Bind n' (Let t v') sc
324 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
325 cl env (App f a) = App (cl env f) (cl env a)
326 cl env t = t
328attack :: RunTactic
329attack ctxt env (Bind x (Hole t) sc)
330 = do h <- getName "hole"
331 action (\ps -> ps { holes = h : holes ps })
332 return $ Bind x (Guess t (newtm h)) sc
333 where
334 newtm h = Bind h (Hole t) (P Bound h t)
335attack ctxt env _ = fail "Not an attackable hole"
337claim :: Name -> Raw -> RunTactic
338claim n ty ctxt env t =
339 do (tyv, tyt) <- lift $ check ctxt env ty
340 lift $ isType ctxt env tyt
341 action (\ps -> let (g:gs) = holes ps in
342 ps { holes = g : n : gs } )
343 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
345reorder_claims :: RunTactic
346reorder_claims ctxt env t
347 = -- trace (showSep "\n" (map show (scvs t))) $
348 let (bs, sc) = scvs t []
349 newbs = reverse (sortB (reverse bs)) in
350 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
351 return (bindAll newbs sc)
352 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
353 scvs sc acc = (reverse acc, sc)
355 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
356 sortB [] = []
357 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
358 | otherwise = sortB (insertB x xs)
360 insertB x [] = [x]
361 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
362 | otherwise = y : insertB x ys
364 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
365 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
366 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
368focus :: Name -> RunTactic
369focus n ctxt env t = do action (\ps -> let hs = holes ps in
370 if n `elem` hs
371 then ps { holes = n : (hs \\ [n]) }
372 else ps)
373 ps <- get
374 return t
376movelast :: Name -> RunTactic
377movelast n ctxt env t = do action (\ps -> let hs = holes ps in
378 if n `elem` hs
379 then ps { holes = (hs \\ [n]) ++ [n] }
380 else ps)
381 return t
383instanceArg :: Name -> RunTactic
384instanceArg n ctxt env (Bind x (Hole t) sc)
385 = do action (\ps -> let hs = holes ps
386 is = instances ps in
387 ps { holes = (hs \\ [x]) ++ [x],
388 instances = x:is })
389 return (Bind x (Hole t) sc)
391autoArg :: Name -> RunTactic
392autoArg n ctxt env (Bind x (Hole t) sc)
393 = do action (\ps -> case lookup x (autos ps) of
394 Nothing ->
395 let hs = holes ps in
396 ps { holes = (hs \\ [x]) ++ [x],
397 autos = (x, refsIn t) : autos ps }
398 Just _ -> ps)
399 return (Bind x (Hole t) sc)
401setinj :: Name -> RunTactic
402setinj n ctxt env (Bind x b sc)
403 = do action (\ps -> let is = injective ps in
404 ps { injective = n : is })
405 return (Bind x b sc)
407defer :: [Name] -> Name -> RunTactic
408defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
409 do let env' = filter (\(n, t) -> n `notElem` dropped) env
410 action (\ps -> let hs = holes ps in
411 ps { holes = hs \\ [x] })
412 return (Bind n (GHole (length env') (mkTy (reverse env') t))
413 (mkApp (P Ref n ty) (map getP (reverse env'))))
414 where
415 mkTy [] t = t
416 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
418 getP (n, b) = P Bound n (binderTy b)
420-- as defer, but build the type and application explicitly
421deferType :: Name -> Raw -> [Name] -> RunTactic
422deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
423 do (fty, _) <- lift $ check ctxt env fty_in
424 action (\ps -> let hs = holes ps
425 ds = deferred ps in
426 ps { holes = hs \\ [x],
427 deferred = n : ds })
428 return (Bind n (GHole 0 fty)
429 (mkApp (P Ref n ty) (map getP args)))
430 where
431 getP n = case lookup n env of
432 Just b -> P Bound n (binderTy b)
433 Nothing -> error ("deferType can't find " ++ show n)
435regret :: RunTactic
436regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
437 do action (\ps -> let hs = holes ps in
438 ps { holes = hs \\ [x] })
439 return sc
440regret ctxt env (Bind x (Hole t) _)
441 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
443exact :: Raw -> RunTactic
444exact guess ctxt env (Bind x (Hole ty) sc) =
445 do (val, valty) <- lift $ check ctxt env guess
446 lift $ converts ctxt env valty ty
447 return $ Bind x (Guess ty val) sc
448exact _ _ _ _ = fail "Can't fill here."
450-- As exact, but attempts to solve other goals by unification
452fill :: Raw -> RunTactic
453fill guess ctxt env (Bind x (Hole ty) sc) =
454 do (val, valty) <- lift $ check ctxt env guess
455-- let valtyn = normalise ctxt env valty
456-- let tyn = normalise ctxt env ty
457 ns <- unify' ctxt env valty ty
458 ps <- get
459 let (uh, uns) = unified ps
460-- put (ps { unified = (uh, uns ++ ns) })
461-- addLog (show (uh, uns ++ ns))
462 return $ Bind x (Guess ty val) sc
463fill _ _ _ _ = fail "Can't fill here."
465-- As fill, but attempts to solve other goals by matching
467match_fill :: Raw -> RunTactic
468match_fill guess ctxt env (Bind x (Hole ty) sc) =
469 do (val, valty) <- lift $ check ctxt env guess
470-- let valtyn = normalise ctxt env valty
471-- let tyn = normalise ctxt env ty
472 ns <- match_unify' ctxt env valty ty
473 ps <- get
474 let (uh, uns) = unified ps
475-- put (ps { unified = (uh, uns ++ ns) })
476-- addLog (show (uh, uns ++ ns))
477 return $ Bind x (Guess ty val) sc
478match_fill _ _ _ _ = fail "Can't fill here."
480prep_fill :: Name -> [Name] -> RunTactic
481prep_fill f as ctxt env (Bind x (Hole ty) sc) =
482 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
483 return $ Bind x (Guess ty val) sc
484prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
486complete_fill :: RunTactic
487complete_fill ctxt env (Bind x (Guess ty val) sc) =
488 do let guess = forget val
489 (val', valty) <- lift $ check ctxt env guess
490 ns <- unify' ctxt env valty ty
491 ps <- get
492 let (uh, uns) = unified ps
493-- put (ps { unified = (uh, uns ++ ns) })
494 return $ Bind x (Guess ty val) sc
495complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
497-- When solving something in the 'dont unify' set, we should check
498-- that the guess we are solving it with unifies with the thing unification
499-- found for it, if anything.
501solve :: RunTactic
502solve ctxt env (Bind x (Guess ty val) sc)
503 = do ps <- get
504 let (uh, uns) = unified ps
505 dropdots <-
506 case lookup x (notunified ps) of
507 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
508 do match_unify' ctxt env tm val
509 return [x]
510 _ -> return []
511 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
512 holes ps \\ [x],
513 solved = Just (x, val),
514 notunified = updateNotunified [(x,val)]
515 (notunified ps),
516 recents = x : recents ps,
517 instances = instances ps \\ [x],
518 dotted = dropUnified dropdots (dotted ps) })
519 let tm' = subst x val sc in
520 return tm'
521 where dropUnified ddots [] = []
522 dropUnified ddots ((x, es) : ds)
523 | x `elem` ddots || any (\e -> e `elem` ddots) es
524 = dropUnified ddots ds
525 | otherwise = (x, es) : dropUnified ddots ds
526solve _ _ h@(Bind x t sc)
527 = do ps <- get
528 case findType x sc of
529 Just t -> lift $ tfail (CantInferType (show t))
530 _ -> lift $ tfail (IncompleteTerm h)
531 where findType x (Bind n (Let t v) sc)
532 = findType x v `mplus` findType x sc
533 findType x (Bind n t sc)
534 | P _ x' _ <- binderTy t, x == x' = Just n
535 | otherwise = findType x sc
536 findType x _ = Nothing
538introTy :: Raw -> Maybe Name -> RunTactic
539introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
540 do let n = case mn of
541 Just name -> name
542 Nothing -> x
543 let t' = case t of
544 x@(Bind y (Pi _ s _) _) -> x
545 _ -> hnf ctxt env t
546 (tyv, tyt) <- lift $ check ctxt env ty
547-- ns <- lift $ unify ctxt env tyv t'
548 case t' of
549 Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in
550 do ns <- unify' ctxt env s tyv
551 ps <- get
552 let (uh, uns) = unified ps
553-- put (ps { unified = (uh, uns ++ ns) })
554 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
555 _ -> lift $ tfail $ CantIntroduce t'
556introTy ty n ctxt env _ = fail "Can't introduce here."
558intro :: Maybe Name -> RunTactic
559intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
560 do let n = case mn of
561 Just name -> name
562 Nothing -> x
563 let t' = case t of
564 x@(Bind y (Pi _ s _) _) -> x
565 _ -> hnf ctxt env t
566 case t' of
567 Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $
568 let t' = subst y (P Bound n s) t in
569 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
570 _ -> lift $ tfail $ CantIntroduce t'
571intro n ctxt env _ = fail "Can't introduce here."
573forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
574forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
575 do (tyv, tyt) <- lift $ check ctxt env ty
576 unify' ctxt env tyt (TType (UVar 0))
577 unify' ctxt env t (TType (UVar 0))
578 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
579forall n impl ty ctxt env _ = fail "Can't pi bind here"
581patvar :: Name -> RunTactic
582patvar n ctxt env (Bind x (Hole t) sc) =
583 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
584 holes ps \\ [x],
585 solved = Just (x, P Bound n t),
586 notunified = updateNotunified [(x,P Bound n t)]
587 (notunified ps),
588 injective = addInj n x (injective ps)
589 })
590 return $ Bind n (PVar t) (subst x (P Bound n t) sc)
591 where addInj n x ps | x `elem` ps = n : ps
592 | otherwise = ps
593patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
595letbind :: Name -> Raw -> Raw -> RunTactic
596letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
597 do (tyv, tyt) <- lift $ check ctxt env ty
598 (valv, valt) <- lift $ check ctxt env val
599 lift $ isType ctxt env tyt
600 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
601letbind n ty val ctxt env _ = fail "Can't let bind here"
603expandLet :: Name -> Term -> RunTactic
604expandLet n v ctxt env tm =
605 return $ subst n v tm
607rewrite :: Raw -> RunTactic
608rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
609 do (tmv, tmt) <- lift $ check ctxt env tm
610 let tmt' = normalise ctxt env tmt
611 case unApply tmt' of
612 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
613 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
614 let newt = mkP l r l t
615 let sc = forget $ (Bind x (Hole newt)
616 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))
617 [lt, l, r, p, tmv, xp]))
618 (scv, sct) <- lift $ check ctxt env sc
619 return scv
620 _ -> lift $ tfail (NotEquality tmv tmt')
621 where rname = sMN 0 "replaced"
622rewrite _ _ _ _ = fail "Can't rewrite here"
624-- To make the P for rewrite, replace syntactic occurrences of l in ty with
625-- an x, and put \x : lt in front
626mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
627mkP lt l r ty | l == ty = lt
628mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
629 a' = if (r /= a) then mkP lt l r a else a in
630 App f' a'
631mkP lt l r (Bind n b sc)
632 = let b' = mkPB b
633 sc' = if (r /= sc) then mkP lt l r sc else sc in
634 Bind n b' sc'
635 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
636 v' = if (r /= v) then mkP lt l r v else v in
637 Let t' v'
638 mkPB b = let ty = binderTy b
639 ty' = if (r /= ty) then mkP lt l r ty else ty in
640 b { binderTy = ty' }
641mkP lt l r x = x
643casetac :: Raw -> Bool -> RunTactic
644casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
645 (tmv, tmt) <- lift $ check ctxt env tm
646 let tmt' = normalise ctxt env tmt
647 let (tacn, tacstr, tactt) = if induction
648 then (ElimN, "an eliminator", "Induction")
649 else (CaseN, "a case function", "Case analysis")
650 case unApply tmt' of
651 (P _ tnm _, tyargs) -> do
652 case lookupTy (SN (tacn tnm)) ctxt of
653 [elimTy] -> do
654 param_pos <- case lookupMetaInformation tnm ctxt of
655 [DataMI param_pos] -> return param_pos
656 m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
657 _ -> return []
658 let (params, indicies) = splitTyArgs param_pos tyargs
659 let args = getArgTys elimTy
660 let pmargs = take (length params) args
661 let args' = drop (length params) args
662 let propTy = head args'
663 let restargs = init $ tail args'
664 let consargs = take (length restargs - length indicies) $ restargs
665 let indxargs = drop (length restargs - length indicies) $ restargs
666 let scr = last $ tail args'
667 let indxnames = makeIndexNames indicies
668 currentNames <- query $ allTTNames . getProofTerm . pterm
669 let tmnm = case tm of
670 Var nm -> uniqueNameCtxt ctxt nm currentNames
671 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
672 let tmvar = P Bound tmnm tmt'
673 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
674 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
675 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
676 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
677 action (\ps -> ps {holes = holes ps \\ [x],
678 recents = x : recents ps })
679 mapM_ addConsHole (reverse consargs')
680 let res' = forget $ res
681 (scv, sct) <- lift $ check ctxt env res'
682 let (scv', _) = specialise ctxt env [] scv
683 return scv'
684 [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
685 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
686 _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
687 where scname = sMN 0 "scarg"
688 makeConsArg (nm, ty) = P Bound nm ty
689 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
690 bindConsArgs [] v = v
691 addConsHole (nm, ty) =
692 action (\ps -> ps { holes = nm : holes ps })
693 splitTyArgs param_pos tyargs =
694 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
695 in (map snd params, map snd indicies)
696 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
697 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
698 let var = P Bound idnm idxt
699 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
700induction tm induction ctxt env _ = do fail "Can't do induction here"
703equiv :: Raw -> RunTactic
704equiv tm ctxt env (Bind x (Hole t) sc) =
705 do (tmv, tmt) <- lift $ check ctxt env tm
706 lift $ converts ctxt env tmv t
707 return $ Bind x (Hole tmv) sc
708equiv tm ctxt env _ = fail "Can't equiv here"
710patbind :: Name -> RunTactic
711patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
712 do let t' = case t of
713 x@(Bind y (PVTy s) t) -> x
714 _ -> hnf ctxt env t
715 case t' of
716 Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in
717 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
718 _ -> fail "Nothing to pattern bind"
719patbind n ctxt env _ = fail "Can't pattern bind here"
721compute :: RunTactic
722compute ctxt env (Bind x (Hole ty) sc) =
723 do return $ Bind x (Hole (normalise ctxt env ty)) sc
724compute ctxt env t = return t
726hnf_compute :: RunTactic
727hnf_compute ctxt env (Bind x (Hole ty) sc) =
728 do let ty' = hnf ctxt env ty in
729-- trace ("HNF " ++ show (ty, ty')) $
730 return $ Bind x (Hole ty') sc
731hnf_compute ctxt env t = return t
733-- reduce let bindings only
734simplify :: RunTactic
735simplify ctxt env (Bind x (Hole ty) sc) =
736 do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
737simplify ctxt env t = return t
739check_in :: Raw -> RunTactic
740check_in t ctxt env tm =
741 do (val, valty) <- lift $ check ctxt env t
742 addLog (showEnv env val ++ " : " ++ showEnv env valty)
743 return tm
745eval_in :: Raw -> RunTactic
746eval_in t ctxt env tm =
747 do (val, valty) <- lift $ check ctxt env t
748 let val' = normalise ctxt env val
749 let valty' = normalise ctxt env valty
750 addLog (showEnv env val ++ " : " ++
751 showEnv env valty ++
752-- " in " ++ show env ++
753 " ==>\n " ++
754 showEnv env val' ++ " : " ++
755 showEnv env valty')
756 return tm
758start_unify :: Name -> RunTactic
759start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
760 return tm
762tmap f (a, b, c) = (f a, b, c)
764solve_unified :: RunTactic
765solve_unified ctxt env tm =
766 do ps <- get
767 let (_, ns) = unified ps
768 let unify = dropGiven (dontunify ps) ns (holes ps)
769 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
770 holes ps \\ map fst unify,
771 recents = recents ps ++ map fst unify })
772 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
773 return (updateSolvedTerm unify tm)
775dropGiven du [] hs = []
776dropGiven du ((n, P Bound t ty) : us) hs
777 | n `elem` du && not (t `elem` du)
778 && n `elem` hs && t `elem` hs
779 = (t, P Bound n ty) : dropGiven du us hs
780dropGiven du (u@(n, _) : us) hs
781 | n `elem` du = dropGiven du us hs
782-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
783dropGiven du (u : us) hs = u : dropGiven du us hs
785keepGiven du [] hs = []
786keepGiven du ((n, P Bound t ty) : us) hs
787 | n `elem` du && not (t `elem` du)
788 && n `elem` hs && t `elem` hs
789 = keepGiven du us hs
790keepGiven du (u@(n, _) : us) hs
791 | n `elem` du = u : keepGiven du us hs
792keepGiven du (u : us) hs = keepGiven du us hs
794updateEnv [] e = e
795updateEnv ns [] = []
796updateEnv ns ((n, b) : env)
797 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
799updateError [] err = err
800updateError ns (At f e) = At f (updateError ns e)
801updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
802updateError ns (ElaboratingArg f a env e)
803 = ElaboratingArg f a env (updateError ns e)
804updateError ns (CantUnify b l r e xs sc)
805 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc
806updateError ns e = e
808solveInProblems x val [] = []
809solveInProblems x val ((l, r, env, err) : ps)
810 = ((psubst x val l, psubst x val r,
811 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
813mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
814mergeNotunified env holes ns = mnu ns [] [] where
815 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
816 mnu ((n, t):ns) ns_acc ps_acc
817 | Just t' <- lookup n ns, t /= t'
818 = mnu ns ((n,t') : ns_acc)
819 ((t,t',True, env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)
820 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
822updateNotunified [] nu = nu
823updateNotunified ns nu = up nu where
824 up [] = []
825 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
826 ((n, t') : up nus)
828updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
829 -> ([(Name, TT Name)], Fails)
830-- updateProblems ctxt [] ps inj holes = ([], ps)
831updateProblems ps updates probs = up updates probs where
832 hs = holes ps
833 inj = injective ps
834 ctxt = context ps
835 usupp = map fst (notunified ps)
837 up ns [] = (ns, [])
838 up ns (prob@(x, y, ready, env, err, while, um) : ps) =
839 let (x', newx) = updateSolvedTerm' ns x
840 (y', newy) = updateSolvedTerm' ns y
841 err' = updateError ns err
842 env' = updateEnv ns env in
843 if newx || newy || ready ||
844 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
845 case unify ctxt env' x' y' inj hs usupp while of
846 OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $
847 up (ns ++ v) ps
848 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
849 let (ns', ps') = up ns ps in
850 (ns', (x',y', False, env',err', while, um) : ps')
851 else -- trace ("SKIPPING " ++ show (x,y,ready)) $
852 let (ns', ps') = up ns ps in
853 (ns', (x',y', False, env',err', while, um) : ps')
855-- attempt to solve remaining problems with match_unify
856matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
857 -> ([(Name, TT Name)], Fails)
858matchProblems all ps updates probs = up updates probs where
859 hs = holes ps
860 inj = injective ps
861 ctxt = context ps
863 up ns [] = (ns, [])
864 up ns ((x, y, ready, env, err, while, um) : ps)
865 | all || um == Match =
866 let x' = updateSolvedTerm ns x
867 y' = updateSolvedTerm ns y
868 err' = updateError ns err
869 env' = updateEnv ns env in
870 case match_unify ctxt env' x' y' inj hs while of
871 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
872 up (ns ++ v) ps
873 _ -> let (ns', ps') = up ns ps in
874 (ns', (x', y', True, env', err', while, um) : ps')
875 up ns (p : ps) = let (ns', ps') = up ns ps in
876 (ns', p : ps')
878processTactic :: Tactic -> ProofState -> TC (ProofState, String)
879processTactic QED ps = case holes ps of
880 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)
881 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
882 return (ps { done = True, pterm = mkProofTerm tm' },
883 "Proof complete: " ++ showEnv [] tm')
884 _ -> fail "Still holes to fill."
885processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
886processTactic Undo ps = case previous ps of
887 Nothing -> Error . Msg $ "Nothing to undo."
888 Just pold -> return (pold, "")
889processTactic EndUnify ps
890 = let (h, ns_in) = unified ps
891 ns = dropGiven (dontunify ps) ns_in (holes ps)
892 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
893 (ns'', probs') = updateProblems ps ns' (problems ps)
894 tm' = updateSolved ns'' (pterm ps) in
895 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $
896 return (ps { pterm = tm',
897 unified = (h, []),
898 problems = probs',
899 notunified = updateNotunified ns'' (notunified ps),
900 recents = recents ps ++ map fst ns'',
901 holes = holes ps \\ map fst ns'' }, "")
902processTactic UnifyAll ps
903 = let tm' = updateSolved (notunified ps) (pterm ps) in
904 return (ps { pterm = tm',
905 notunified = [],
906 recents = recents ps ++ map fst (notunified ps),
907 holes = holes ps \\ map fst (notunified ps) }, "")
908processTactic (Reorder n) ps
909 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
910 return (ps' { previous = Just ps, plog = "" }, plog ps')
911processTactic (ComputeLet n) ps
912 = return (ps { pterm = mkProofTerm $
913 computeLet (context ps) n
914 (getProofTerm (pterm ps)) }, "")
915processTactic UnifyProblems ps
916 = do let (ns', probs') = updateProblems ps [] (problems ps)
917 pterm' = updateSolved ns' (pterm ps)
918 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $
919 return (ps { pterm = pterm', solved = Nothing, problems = probs',
920 previous = Just ps, plog = "",
921 notunified = updateNotunified ns' (notunified ps),
922 recents = recents ps ++ map fst ns',
923 holes = holes ps \\ (map fst ns') }, plog ps)
924processTactic (MatchProblems all) ps
925 = do let (ns', probs') = matchProblems all ps [] (problems ps)
926 (ns'', probs'') = matchProblems all ps ns' probs'
927 pterm' = updateSolved ns'' (pterm ps)
928 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns'')) $
929 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
930 previous = Just ps, plog = "",
931 notunified = updateNotunified ns'' (notunified ps),
932 recents = recents ps ++ map fst ns'',
933 holes = holes ps \\ (map fst ns'') }, plog ps)
934processTactic t ps
935 = case holes ps of
936 [] -> fail "Nothing to fill in."
937 (h:_) -> do ps' <- execStateT (process t h) ps
938 let (ns', probs')
939 = case solved ps' of
940 Just s -> traceWhen (unifylog ps')
941 ("SOLVED " ++ show s) $
942 updateProblems ps [s] (problems ps')
943 _ -> ([], problems ps')
944 -- rechecking problems may find more solutions, so
945 -- apply them here
946 let pterm'' = updateSolved ns' (pterm ps')
947 traceWhen (unifylog ps) ("Dropping holes: " ++ show (map fst ns')) $
948 return (ps' { pterm = pterm'',
949 solved = Nothing,
950 problems = probs',
951 notunified = updateNotunified ns' (notunified ps'),
952 previous = Just ps, plog = "",
953 recents = recents ps' ++ map fst ns',
954 holes = holes ps' \\ (map fst ns')}, plog ps')
956process :: Tactic -> Name -> StateT TState TC ()
957process EndUnify _
958 = do ps <- get
959 let (h, _) = unified ps
960 tactic (Just h) solve_unified
961process t h = tactic (Just h) (mktac t)
962 where mktac Attack = attack
963 mktac (Claim n r) = claim n r
964 mktac (Exact r) = exact r
965 mktac (Fill r) = fill r
966 mktac (MatchFill r) = match_fill r
967 mktac (PrepFill n ns) = prep_fill n ns
968 mktac CompleteFill = complete_fill
969 mktac Regret = regret
970 mktac Solve = solve
971 mktac (StartUnify n) = start_unify n
972 mktac Compute = compute
973 mktac Simplify = Idris.Core.ProofState.simplify
974 mktac HNF_Compute = hnf_compute
975 mktac (Intro n) = intro n
976 mktac (IntroTy ty n) = introTy ty n
977 mktac (Forall n i t) = forall n i t
978 mktac (LetBind n t v) = letbind n t v
979 mktac (ExpandLet n b) = expandLet n b
980 mktac (Rewrite t) = rewrite t
981 mktac (Induction t) = casetac t True
982 mktac (CaseTac t) = casetac t False
983 mktac (Equiv t) = equiv t
984 mktac (PatVar n) = patvar n
985 mktac (PatBind n) = patbind n
986 mktac (CheckIn r) = check_in r
987 mktac (EvalIn r) = eval_in r
988 mktac (Focus n) = focus n
989 mktac (Defer ns n) = defer ns n
990 mktac (DeferType n t a) = deferType n t a
991 mktac (Instance n) = instanceArg n
992 mktac (AutoArg n) = autoArg n
993 mktac (SetInjective n) = setinj n
994 mktac (MoveLast n) = movelast n