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