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