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