git.iko.soy/Idris-dev
on e7d962d help sign in
Idris-dev/src/Core/ProofState.hs
798 lines 33 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 Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic,
9 dropGiven, keepGiven) where
11import Core.Typecheck
12import Core.Evaluate
13import Core.TT
14import Core.Unify
16import Control.Monad.State
17import Control.Applicative hiding (empty)
18import Data.List
19import Debug.Trace
21import Util.Pretty
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 | Equiv Raw
73 | PatVar Name
74 | PatBind Name
75 | Focus Name
76 | Defer Name
77 | DeferType Name Raw [Name]
78 | Instance Name
79 | SetInjective Name
80 | MoveLast Name
81 | ProofState
82 | Undo
83 | QED
84 deriving Show
86-- Some utilites on proof and tactic states
88instance Show ProofState where
89 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _)
90 = show nm ++ ": no more goals"
91 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _)
92 = let OK g = goal (Just h) tm
93 wkenv = premises g in
94 "Other goals: " ++ show hs ++ "\n" ++
95 showPs wkenv (reverse wkenv) ++ "\n" ++
96 "-------------------------------- (" ++ show nm ++
97 ") -------\n " ++
98 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
99 where showPs env [] = ""
100 showPs env ((n, Let t v):bs)
101 = " " ++ show n ++ " : " ++
102 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
103 showEnv env ({- normalise ctxt env -} v) ++
104 "\n" ++ showPs env bs
105 showPs env ((n, b):bs)
106 = " " ++ show n ++ " : " ++
107 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
108 "\n" ++ showPs env bs
109 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
110 " =?= " ++ showEnv ps v
111 showG ps b = showEnv ps (binderTy b)
113instance Pretty ProofState where
114 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
115 if size nm > breakingSize then
116 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
117 else
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 if size v > breakingSize then
129 prettyEnv ps t <+> text "=?=" $$
130 nest nestingSize (prettyEnv ps v)
131 else
132 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
133 prettyGoal ps b = prettyEnv ps $ binderTy b
135 prettyPs env [] = empty
136 prettyPs env ((n, Let t v):bs) =
137 nest nestingSize (pretty n <+> colon <+>
138 if size v > breakingSize then
139 prettyEnv env t <+> text "=" $$
140 nest nestingSize (prettyEnv env v) $$
141 nest nestingSize (prettyPs env bs)
142 else
143 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
144 nest nestingSize (prettyPs env bs))
145 prettyPs env ((n, b):bs) =
146 if size (binderTy b) > breakingSize then
147 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
148 else
149 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
150 nest nestingSize (prettyPs env bs))
152same Nothing n = True
153same (Just x) n = x == n
155hole (Hole _) = True
156hole (Guess _ _) = True
157hole _ = False
159holeName i = MN i "hole"
161qshow :: Fails -> String
162qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
164match_unify' :: Context -> Env -> TT Name -> TT Name ->
165 StateT TState TC [(Name, TT Name)]
166match_unify' ctxt env topx topy =
167 do ps <- get
168 let dont = dontunify ps
169 u <- lift $ match_unify ctxt env topx topy dont (holes ps)
170 let (h, ns) = unified ps
171 put (ps { unified = (h, u ++ ns) })
172 return u
174unify' :: Context -> Env -> TT Name -> TT Name ->
175 StateT TState TC [(Name, TT Name)]
176unify' ctxt env topx topy =
177 do ps <- get
178 let dont = dontunify ps
179 (u, fails) <- traceWhen (unifylog ps)
180 ("Trying " ++ show (topx, topy) ++
181 " in " ++ show env ++
182 "\nHoles: " ++ show (holes ps) ++ "\n") $
183 lift $ unify ctxt env topx topy dont (holes ps)
184 traceWhen (unifylog ps)
185 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
186 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
187 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
188-- ++ show (pterm ps)
189 ++ "\n----------") $
190 case fails of
191-- [] -> return u
192 err ->
193 do ps <- get
194 let (h, ns) = unified ps
195 let (ns', probs') = updateProblems (context ps) (u ++ ns)
196 (err ++ problems ps)
197 (injective ps)
198 (holes ps)
199 put (ps { problems = probs',
200 unified = (h, ns') })
201 return u
203getName :: Monad m => String -> StateT TState m Name
204getName tag = do ps <- get
205 let n = nextname ps
206 put (ps { nextname = n+1 })
207 return $ MN n tag
209action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
210action a = do ps <- get
211 put (a ps)
213addLog :: Monad m => String -> StateT TState m ()
214addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
216newProof :: Name -> Context -> Type -> ProofState
217newProof n ctxt ty = let h = holeName 0
218 ty' = vToP ty in
219 PS n [h] [] 1 (Bind h (Hole ty')
220 (P Bound h ty')) ty [] (h, []) []
221 Nothing [] []
222 [] []
223 Nothing ctxt "" False False
225type TState = ProofState -- [TacticAction])
226type RunTactic = Context -> Env -> Term -> StateT TState TC Term
227type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
229envAtFocus :: ProofState -> TC Env
230envAtFocus ps
231 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
232 return (premises g)
233 | otherwise = fail "No holes"
235goalAtFocus :: ProofState -> TC (Binder Type)
236goalAtFocus ps
237 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
238 return (goalType g)
239 | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
241goal :: Hole -> Term -> TC Goal
242goal h tm = g [] tm where
243 g env (Bind n b@(Guess _ _) sc)
244 | same h n = return $ GD env b
245 | otherwise
246 = gb env b `mplus` g ((n, b):env) sc
247 g env (Bind n b sc) | hole b && same h n = return $ GD env b
248 | otherwise
249 = g ((n, b):env) sc `mplus` gb env b
250 g env (App f a) = g env f `mplus` g env a
251 g env t = fail "Can't find hole"
253 gb env (Let t v) = g env v `mplus` g env t
254 gb env (Guess t v) = g env v `mplus` g env t
255 gb env t = g env (binderTy t)
257tactic :: Hole -> RunTactic -> StateT TState TC ()
258tactic h f = do ps <- get
259 (tm', _) <- atH (context ps) [] (pterm ps)
260 ps <- get -- might have changed while processing
261 put (ps { pterm = tm' })
262 where
263 updated o = do o' <- o
264 return (o', True)
266 ulift2 c env op a b
267 = do (b', u) <- atH c env b
268 if u then return (op a b', True)
269 else do (a', u) <- atH c env a
270 return (op a' b', u)
272 -- Search the things most likely to contain the binding first!
274 atH :: Context -> Env -> Term -> StateT TState TC (Term, Bool)
275 atH c env binder@(Bind n b@(Guess t v) sc)
276 | same h n = updated (f c env binder)
277 | otherwise
278 = do -- binder first
279 (b', u) <- ulift2 c env Guess t v
280 if u then return (Bind n b' sc, True)
281 else do (sc', u) <- atH c ((n, b) : env) sc
282 return (Bind n b' sc', u)
283 atH c env binder@(Bind n b sc)
284 | hole b && same h n = updated (f c env binder)
285 | otherwise -- scope first
286 = do (sc', u) <- atH c ((n, b) : env) sc
287 if u then return (Bind n b sc', True)
288 else do (b', u) <- atHb c env b
289 return (Bind n b' sc', u)
290 atH c env (App f a) = ulift2 c env App f a
291 atH c env t = return (t, False)
293 atHb c env (Let t v) = ulift2 c env Let t v
294 atHb c env (Guess t v) = ulift2 c env Guess t v
295 atHb c env t = do (ty', u) <- atH c env (binderTy t)
296 return (t { binderTy = ty' }, u)
298computeLet :: Context -> Name -> Term -> Term
299computeLet ctxt n tm = cl [] tm where
300 cl env (Bind n' (Let t v) sc)
301 | n' == n = let v' = normalise ctxt env v in
302 Bind n' (Let t v') sc
303 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
304 cl env (App f a) = App (cl env f) (cl env a)
305 cl env t = t
307attack :: RunTactic
308attack ctxt env (Bind x (Hole t) sc)
309 = do h <- getName "hole"
310 action (\ps -> ps { holes = h : holes ps })
311 return $ Bind x (Guess t (newtm h)) sc
312 where
313 newtm h = Bind h (Hole t) (P Bound h t)
314attack ctxt env _ = fail "Not an attackable hole"
316claim :: Name -> Raw -> RunTactic
317claim n ty ctxt env t =
318 do (tyv, tyt) <- lift $ check ctxt env ty
319 lift $ isType ctxt env tyt
320 action (\ps -> let (g:gs) = holes ps in
321 ps { holes = g : n : gs } )
322 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
324reorder_claims :: RunTactic
325reorder_claims ctxt env t
326 = -- trace (showSep "\n" (map show (scvs t))) $
327 let (bs, sc) = scvs t []
328 newbs = reverse (sortB (reverse bs)) in
329 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
330 return (bindAll newbs sc)
331 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
332 scvs sc acc = (reverse acc, sc)
334 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
335 sortB [] = []
336 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
337 | otherwise = sortB (insertB x xs)
339 insertB x [] = [x]
340 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
341 | otherwise = y : insertB x ys
343 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
344 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
345 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
347focus :: Name -> RunTactic
348focus n ctxt env t = do action (\ps -> let hs = holes ps in
349 if n `elem` hs
350 then ps { holes = n : (hs \\ [n]) }
351 else ps)
352 ps <- get
353 return t
355movelast :: Name -> RunTactic
356movelast n ctxt env t = do action (\ps -> let hs = holes ps in
357 if n `elem` hs
358 then ps { holes = (hs \\ [n]) ++ [n] }
359 else ps)
360 return t
362instanceArg :: Name -> RunTactic
363instanceArg n ctxt env (Bind x (Hole t) sc)
364 = do action (\ps -> let hs = holes ps
365 is = instances ps in
366 ps { holes = (hs \\ [x]) ++ [x],
367 instances = x:is })
368 return (Bind x (Hole t) sc)
370setinj :: Name -> RunTactic
371setinj n ctxt env (Bind x (Hole t) sc)
372 = do action (\ps -> let is = injective ps in
373 ps { injective = n : is })
374 return (Bind x (Hole t) sc)
376defer :: Name -> RunTactic
377defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
378 do action (\ps -> let hs = holes ps in
379 ps { holes = hs \\ [x] })
380 return (Bind n (GHole (mkTy (reverse env) t))
381 (mkApp (P Ref n ty) (map getP (reverse env))))
382 where
383 mkTy [] t = t
384 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
386 getP (n, b) = P Bound n (binderTy b)
388-- as defer, but build the type and application explicitly
389deferType :: Name -> Raw -> [Name] -> RunTactic
390deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
391 do (fty, _) <- lift $ check ctxt env fty_in
392 action (\ps -> let hs = holes ps
393 ds = deferred ps in
394 ps { holes = hs \\ [x],
395 deferred = n : ds })
396 return (Bind n (GHole fty)
397 (mkApp (P Ref n ty) (map getP args)))
398 where
399 getP n = case lookup n env of
400 Just b -> P Bound n (binderTy b)
401 Nothing -> error ("deferType can't find " ++ show n)
403regret :: RunTactic
404regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
405 do action (\ps -> let hs = holes ps in
406 ps { holes = hs \\ [x] })
407 return sc
408regret ctxt env (Bind x (Hole t) _)
409 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
411exact :: Raw -> RunTactic
412exact guess ctxt env (Bind x (Hole ty) sc) =
413 do (val, valty) <- lift $ check ctxt env guess
414 lift $ converts ctxt env valty ty
415 return $ Bind x (Guess ty val) sc
416exact _ _ _ _ = fail "Can't fill here."
418-- As exact, but attempts to solve other goals by unification
420fill :: Raw -> RunTactic
421fill guess ctxt env (Bind x (Hole ty) sc) =
422 do (val, valty) <- lift $ check ctxt env guess
423-- let valtyn = normalise ctxt env valty
424-- let tyn = normalise ctxt env ty
425 ns <- unify' ctxt env valty ty
426 ps <- get
427 let (uh, uns) = unified ps
428-- put (ps { unified = (uh, uns ++ ns) })
429-- addLog (show (uh, uns ++ ns))
430 return $ Bind x (Guess ty val) sc
431fill _ _ _ _ = fail "Can't fill here."
433-- As fill, but attempts to solve other goals by matching
435match_fill :: Raw -> RunTactic
436match_fill guess ctxt env (Bind x (Hole ty) sc) =
437 do (val, valty) <- lift $ check ctxt env guess
438-- let valtyn = normalise ctxt env valty
439-- let tyn = normalise ctxt env ty
440 ns <- match_unify' ctxt env valty ty
441 ps <- get
442 let (uh, uns) = unified ps
443-- put (ps { unified = (uh, uns ++ ns) })
444-- addLog (show (uh, uns ++ ns))
445 return $ Bind x (Guess ty val) sc
446match_fill _ _ _ _ = fail "Can't fill here."
448prep_fill :: Name -> [Name] -> RunTactic
449prep_fill f as ctxt env (Bind x (Hole ty) sc) =
450 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
451 return $ Bind x (Guess ty val) sc
452prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
454complete_fill :: RunTactic
455complete_fill ctxt env (Bind x (Guess ty val) sc) =
456 do let guess = forget val
457 (val', valty) <- lift $ check ctxt env guess
458 ns <- unify' ctxt env valty ty
459 ps <- get
460 let (uh, uns) = unified ps
461-- put (ps { unified = (uh, uns ++ ns) })
462 return $ Bind x (Guess ty val) sc
463complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
465-- When solving something in the 'dont unify' set, we should check
466-- that the guess we are solving it with unifies with the thing unification
467-- found for it, if anything.
469solve :: RunTactic
470solve ctxt env (Bind x (Guess ty val) sc)
471 | True = do ps <- get
472 let (uh, uns) = unified ps
473 case lookup x (notunified ps) of
474 Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $
475 -- return []
476 unify' ctxt env tm val
477 _ -> return []
478 action (\ps -> ps { holes = holes ps \\ [x],
479 solved = Just (x, val),
480-- problems = solveInProblems
481-- x val (problems ps),
482 -- dontunify = dontunify ps \\ [x],
483 -- unified = (uh, uns ++ [(x, val)]),
484 instances = instances ps \\ [x] })
485 let tm' = instantiate val (pToV x sc) in
486 return tm'
487 | otherwise = lift $ tfail $ IncompleteTerm val
488solve _ _ h@(Bind x t sc)
489 = do ps <- get
490 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
492introTy :: Raw -> Maybe Name -> RunTactic
493introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
494 do let n = case mn of
495 Just name -> name
496 Nothing -> x
497 let t' = case t of
498 x@(Bind y (Pi s) _) -> x
499 _ -> hnf ctxt env t
500 (tyv, tyt) <- lift $ check ctxt env ty
501-- ns <- lift $ unify ctxt env tyv t'
502 case t' of
503 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
504 do ns <- unify' ctxt env s tyv
505 ps <- get
506 let (uh, uns) = unified ps
507-- put (ps { unified = (uh, uns ++ ns) })
508 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
509 _ -> lift $ tfail $ CantIntroduce t'
510introTy ty n ctxt env _ = fail "Can't introduce here."
512intro :: Maybe Name -> RunTactic
513intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
514 do let n = case mn of
515 Just name -> name
516 Nothing -> x
517 let t' = case t of
518 x@(Bind y (Pi s) _) -> x
519 _ -> hnf ctxt env t
520 case t' of
521 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
522 let t' = instantiate (P Bound n s) (pToV y t) in
523 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
524 _ -> lift $ tfail $ CantIntroduce t'
525intro n ctxt env _ = fail "Can't introduce here."
527forall :: Name -> Raw -> RunTactic
528forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
529 do (tyv, tyt) <- lift $ check ctxt env ty
530 unify' ctxt env tyt (TType (UVar 0))
531 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
532forall n ty ctxt env _ = fail "Can't pi bind here"
534patvar :: Name -> RunTactic
535patvar n ctxt env (Bind x (Hole t) sc) =
536 do action (\ps -> ps { holes = holes ps \\ [x] })
537 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
538patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
540letbind :: Name -> Raw -> Raw -> RunTactic
541letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
542 do (tyv, tyt) <- lift $ check ctxt env ty
543 (valv, valt) <- lift $ check ctxt env val
544 lift $ isType ctxt env tyt
545 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
546letbind n ty val ctxt env _ = fail "Can't let bind here"
548expandLet :: Name -> Term -> RunTactic
549expandLet n v ctxt env tm =
550 return $ subst n v tm
552rewrite :: Raw -> RunTactic
553rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
554 do (tmv, tmt) <- lift $ check ctxt env tm
555 let tmt' = normalise ctxt env tmt
556 case unApply tmt' of
557 (P _ (UN "=") _, [lt,rt,l,r]) ->
558 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
559 let newt = mkP l r l t
560 let sc = forget $ (Bind x (Hole newt)
561 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
562 [lt, l, r, p, tmv, xp]))
563 (scv, sct) <- lift $ check ctxt env sc
564 return scv
565 _ -> fail "Not an equality type"
566 where
567 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
568 -- an x, and put \x : lt in front
569 mkP lt l r ty | l == ty = lt
570 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
571 a' = if (r /= a) then mkP lt l r a else a in
572 App f' a'
573 mkP lt l r (Bind n b sc)
574 = let b' = mkPB b
575 sc' = if (r /= sc) then mkP lt l r sc else sc in
576 Bind n b' sc'
577 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
578 v' = if (r /= v) then mkP lt l r v else v in
579 Let t' v'
580 mkPB b = let ty = binderTy b
581 ty' = if (r /= ty) then mkP lt l r ty else ty in
582 b { binderTy = ty' }
583 mkP lt l r x = x
585 rname = MN 0 "replaced"
586rewrite _ _ _ _ = fail "Can't rewrite here"
588equiv :: Raw -> RunTactic
589equiv tm ctxt env (Bind x (Hole t) sc) =
590 do (tmv, tmt) <- lift $ check ctxt env tm
591 lift $ converts ctxt env tmv t
592 return $ Bind x (Hole tmv) sc
593equiv tm ctxt env _ = fail "Can't equiv here"
595patbind :: Name -> RunTactic
596patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
597 do let t' = case t of
598 x@(Bind y (PVTy s) t) -> x
599 _ -> hnf ctxt env t
600 case t' of
601 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
602 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
603 _ -> fail "Nothing to pattern bind"
604patbind n ctxt env _ = fail "Can't pattern bind here"
606compute :: RunTactic
607compute ctxt env (Bind x (Hole ty) sc) =
608 do return $ Bind x (Hole (normalise ctxt env ty)) sc
609compute ctxt env t = return t
611hnf_compute :: RunTactic
612hnf_compute ctxt env (Bind x (Hole ty) sc) =
613 do let ty' = hnf ctxt env ty in
614-- trace ("HNF " ++ show (ty, ty')) $
615 return $ Bind x (Hole ty') sc
616hnf_compute ctxt env t = return t
618-- reduce let bindings only
619simplify :: RunTactic
620simplify ctxt env (Bind x (Hole ty) sc) =
621 do return $ Bind x (Hole (specialise ctxt env [] ty)) sc
622simplify ctxt env t = return t
624check_in :: Raw -> RunTactic
625check_in t ctxt env tm =
626 do (val, valty) <- lift $ check ctxt env t
627 addLog (showEnv env val ++ " : " ++ showEnv env valty)
628 return tm
630eval_in :: Raw -> RunTactic
631eval_in t ctxt env tm =
632 do (val, valty) <- lift $ check ctxt env t
633 let val' = normalise ctxt env val
634 let valty' = normalise ctxt env valty
635 addLog (showEnv env val ++ " : " ++
636 showEnv env valty ++
637-- " in " ++ show env ++
638 " ==>\n " ++
639 showEnv env val' ++ " : " ++
640 showEnv env valty')
641 return tm
643start_unify :: Name -> RunTactic
644start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
645 return tm
647tmap f (a, b, c) = (f a, b, c)
649solve_unified :: RunTactic
650solve_unified ctxt env tm =
651 do ps <- get
652 let (_, ns) = unified ps
653 let unify = dropGiven (dontunify ps) ns (holes ps)
654 action (\ps -> ps { holes = holes ps \\ map fst unify })
655 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
656 return (updateSolved unify tm)
657 where
659dropGiven du [] hs = []
660dropGiven du ((n, P Bound t ty) : us) hs
661 | n `elem` du && not (t `elem` du)
662 && n `elem` hs && t `elem` hs
663 = (t, P Bound n ty) : dropGiven du us hs
664dropGiven du (u@(n, _) : us) hs
665 | n `elem` du = dropGiven du us hs
666-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
667dropGiven du (u : us) hs = u : dropGiven du us hs
669keepGiven du [] hs = []
670keepGiven du ((n, P Bound t ty) : us) hs
671 | n `elem` du && not (t `elem` du)
672 && n `elem` hs && t `elem` hs
673 = keepGiven du us hs
674keepGiven du (u@(n, _) : us) hs
675 | n `elem` du = u : keepGiven du us hs
676keepGiven du (u : us) hs = keepGiven du us hs
678updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
679 updateSolved' xs x
680updateSolved' xs (Bind n (Hole ty) t)
681 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
682updateSolved' xs (Bind n b t)
683 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
684updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
685updateSolved' xs (P _ n _)
686 | Just v <- lookup n xs = v
687updateSolved' xs t = t
689updateEnv ns [] = []
690updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
692updateError ns (CantUnify b l r e xs sc)
693 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
694updateError ns e = e
696solveInProblems x val [] = []
697solveInProblems x val ((l, r, env, err) : ps)
698 = ((instantiate val (pToV x l), instantiate val (pToV x r),
699 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
701updateProblems ctxt ns ps inj holes = up ns ps where
702 up ns [] = (ns, [])
703 up ns ((x, y, env, err) : ps) =
704 let x' = updateSolved ns x
705 y' = updateSolved ns y
706 err' = updateError ns err
707 env' = updateEnv ns env in
708 case unify ctxt env' x' y' inj holes of
709 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
710 up (ns ++ v) ps
711 _ -> let (ns', ps') = up ns ps in
712 (ns', (x',y',env',err') : ps')
714processTactic :: Tactic -> ProofState -> TC (ProofState, String)
715processTactic QED ps = case holes ps of
716 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
717 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
718 return (ps { done = True, pterm = tm' },
719 "Proof complete: " ++ showEnv [] tm')
720 _ -> fail "Still holes to fill."
721processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
722processTactic Undo ps = case previous ps of
723 Nothing -> fail "Nothing to undo."
724 Just pold -> return (pold, "")
725processTactic EndUnify ps
726 = let (h, ns_in) = unified ps
727 ns = dropGiven (dontunify ps) ns_in (holes ps)
728 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
729 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
730 (injective ps) (holes ps)
731 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
732 updateSolved ns'' (pterm ps) in
733 return (ps { pterm = tm',
734 unified = (h, []),
735 problems = probs',
736 holes = holes ps \\ map fst ns'' }, "")
737processTactic (Reorder n) ps
738 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
739 return (ps' { previous = Just ps, plog = "" }, plog ps')
740processTactic (ComputeLet n) ps
741 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")
742processTactic t ps
743 = case holes ps of
744 [] -> fail "Nothing to fill in."
745 (h:_) -> do ps' <- execStateT (process t h) ps
746 let (ns', probs')
747 = case solved ps' of
748 Just s -> updateProblems (context ps')
749 [s] (problems ps')
750 (injective ps')
751 (holes ps')
752 _ -> ([], problems ps')
753 -- rechecking problems may find more solutions, so
754 -- apply them here
755 let pterm'' = updateSolved ns' (pterm ps')
756 return (ps' { pterm = pterm'',
757 solved = Nothing,
758 problems = probs',
759 previous = Just ps, plog = "",
760 holes = holes ps' \\ (map fst ns')}, plog ps')
762process :: Tactic -> Name -> StateT TState TC ()
763process EndUnify _
764 = do ps <- get
765 let (h, _) = unified ps
766 tactic (Just h) solve_unified
767process t h = tactic (Just h) (mktac t)
768 where mktac Attack = attack
769 mktac (Claim n r) = claim n r
770 mktac (Exact r) = exact r
771 mktac (Fill r) = fill r
772 mktac (MatchFill r) = match_fill r
773 mktac (PrepFill n ns) = prep_fill n ns
774 mktac CompleteFill = complete_fill
775 mktac Regret = regret
776 mktac Solve = solve
777 mktac (StartUnify n) = start_unify n
778 mktac Compute = compute
779 mktac Simplify = Core.ProofState.simplify
780 mktac HNF_Compute = hnf_compute
781 mktac (Intro n) = intro n
782 mktac (IntroTy ty n) = introTy ty n
783 mktac (Forall n t) = forall n t
784 mktac (LetBind n t v) = letbind n t v
785 mktac (ExpandLet n b) = expandLet n b
786 mktac (Rewrite t) = rewrite t
787 mktac (Equiv t) = equiv t
788 mktac (PatVar n) = patvar n
789 mktac (PatBind n) = patbind n
790 mktac (CheckIn r) = check_in r
791 mktac (EvalIn r) = eval_in r
792 mktac (Focus n) = focus n
793 mktac (Defer n) = defer n
794 mktac (DeferType n t a) = deferType n t a
795 mktac (Instance n) = instanceArg n
796 mktac (SetInjective n) = setinj n
797 mktac (MoveLast n) = movelast n