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