git.iko.soy/Idris-dev
on fc79985 help sign in
Idris-dev/src/Core/ProofState.hs
733 lines 31 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 done :: Bool
41 }
43data Goal = GD { premises :: Env,
44 goalType :: Binder Term
45 }
47data Tactic = Attack
48 | Claim Name Raw
49 | Reorder Name
50 | Exact Raw
51 | Fill Raw
52 | MatchFill Raw
53 | PrepFill Name [Name]
54 | CompleteFill
55 | Regret
56 | Solve
57 | StartUnify Name
58 | EndUnify
59 | Compute
60 | HNF_Compute
61 | EvalIn Raw
62 | CheckIn Raw
63 | Intro (Maybe Name)
64 | IntroTy Raw (Maybe Name)
65 | Forall Name Raw
66 | LetBind Name Raw Raw
67 | Rewrite Raw
68 | PatVar Name
69 | PatBind Name
70 | Focus Name
71 | Defer Name
72 | DeferType Name Raw [Name]
73 | Instance Name
74 | SetInjective Name
75 | MoveLast Name
76 | ProofState
77 | Undo
78 | QED
79 deriving Show
81-- Some utilites on proof and tactic states
83instance Show ProofState where
84 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
85 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _)
86 = let OK g = goal (Just h) tm
87 wkenv = premises g in
88 "Other goals: " ++ show hs ++ "\n" ++
89 showPs wkenv (reverse wkenv) ++ "\n" ++
90 "-------------------------------- (" ++ show nm ++
91 ") -------\n " ++
92 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
93 where showPs env [] = ""
94 showPs env ((n, Let t v):bs)
95 = " " ++ show n ++ " : " ++
96 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
97 showEnv env ({- normalise ctxt env -} v) ++
98 "\n" ++ showPs env bs
99 showPs env ((n, b):bs)
100 = " " ++ show n ++ " : " ++
101 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
102 "\n" ++ showPs env bs
103 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
104 " =?= " ++ showEnv ps v
105 showG ps b = showEnv ps (binderTy b)
107instance Pretty ProofState where
108 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _) =
109 if size nm > breakingSize then
110 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
111 else
112 pretty nm <> colon <+> text " no more goals."
113 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _) =
114 let OK g = goal (Just h) tm in
115 let wkEnv = premises g in
116 text "Other goals" <+> colon <+> pretty hs $$
117 prettyPs wkEnv (reverse wkEnv) $$
118 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
119 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
120 where
121 prettyGoal ps (Guess t v) =
122 if size v > breakingSize then
123 prettyEnv ps t <+> text "=?=" $$
124 nest nestingSize (prettyEnv ps v)
125 else
126 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
127 prettyGoal ps b = prettyEnv ps $ binderTy b
129 prettyPs env [] = empty
130 prettyPs env ((n, Let t v):bs) =
131 nest nestingSize (pretty n <+> colon <+>
132 if size v > breakingSize then
133 prettyEnv env t <+> text "=" $$
134 nest nestingSize (prettyEnv env v) $$
135 nest nestingSize (prettyPs env bs)
136 else
137 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
138 nest nestingSize (prettyPs env bs))
139 prettyPs env ((n, b):bs) =
140 if size (binderTy b) > breakingSize then
141 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
142 else
143 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
144 nest nestingSize (prettyPs env bs))
146same Nothing n = True
147same (Just x) n = x == n
149hole (Hole _) = True
150hole (Guess _ _) = True
151hole _ = False
153holeName i = MN i "hole"
155qshow :: Fails -> String
156qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
158match_unify' :: Context -> Env -> TT Name -> TT Name ->
159 StateT TState TC [(Name, TT Name)]
160match_unify' ctxt env topx topy =
161 do ps <- get
162 let dont = dontunify ps
163 u <- lift $ match_unify ctxt env topx topy dont (holes ps)
164 let (h, ns) = unified ps
165 put (ps { unified = (h, u ++ ns) })
166 return u
168unify' :: Context -> Env -> TT Name -> TT Name ->
169 StateT TState TC [(Name, TT Name)]
170unify' ctxt env topx topy =
171 do ps <- get
172 let dont = dontunify ps
173 (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $
174 lift $ unify ctxt env topx topy dont (holes ps)
175-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
176-- " in " ++ show env ++
177-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"
178-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"
179-- -- ++ show (pterm ps)
180-- ++ "\n----------") $
181 case fails of
182-- [] -> return u
183 err ->
184 do ps <- get
185 let (h, ns) = unified ps
186 let (ns', probs') = updateProblems (context ps) (u ++ ns)
187 (err ++ problems ps)
188 (injective ps)
189 (holes ps)
190 put (ps { problems = probs',
191 unified = (h, ns') })
192 return u
194getName :: Monad m => String -> StateT TState m Name
195getName tag = do ps <- get
196 let n = nextname ps
197 put (ps { nextname = n+1 })
198 return $ MN n tag
200action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
201action a = do ps <- get
202 put (a ps)
204addLog :: Monad m => String -> StateT TState m ()
205addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
207newProof :: Name -> Context -> Type -> ProofState
208newProof n ctxt ty = let h = holeName 0
209 ty' = vToP ty in
210 PS n [h] [] 1 (Bind h (Hole ty')
211 (P Bound h ty')) ty [] (h, []) []
212 Nothing [] []
213 [] []
214 Nothing ctxt "" False
216type TState = ProofState -- [TacticAction])
217type RunTactic = Context -> Env -> Term -> StateT TState TC Term
218type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
220envAtFocus :: ProofState -> TC Env
221envAtFocus ps
222 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
223 return (premises g)
224 | otherwise = fail "No holes"
226goalAtFocus :: ProofState -> TC (Binder Type)
227goalAtFocus ps
228 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
229 return (goalType g)
230 | otherwise = error $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
232goal :: Hole -> Term -> TC Goal
233goal h tm = g [] tm where
234 g env (Bind n b sc) | hole b && same h n = return $ GD env b
235 | otherwise
236 = gb env b `mplus` g ((n, b):env) sc
237 g env (App f a) = g env f `mplus` g env a
238 g env t = fail "Can't find hole"
240 gb env (Let t v) = g env t `mplus` g env v
241 gb env (Guess t v) = g env t `mplus` g env v
242 gb env t = g env (binderTy t)
244tactic :: Hole -> RunTactic -> StateT TState TC ()
245tactic h f = do ps <- get
246 tm' <- atH (context ps) [] (pterm ps)
247 ps <- get -- might have changed while processing
248 put (ps { pterm = tm' })
249 where
250 atH c env binder@(Bind n b sc)
251 | hole b && same h n = f c env binder
252 | otherwise
253 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
254 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
255 atH c env t = return t
257 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
258 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
259 atHb c env t = do ty' <- atH c env (binderTy t)
260 return $ t { binderTy = ty' }
262attack :: RunTactic
263attack ctxt env (Bind x (Hole t) sc)
264 = do h <- getName "hole"
265 action (\ps -> ps { holes = h : holes ps })
266 return $ Bind x (Guess t (newtm h)) sc
267 where
268 newtm h = Bind h (Hole t) (P Bound h t)
269attack ctxt env _ = fail "Not an attackable hole"
271claim :: Name -> Raw -> RunTactic
272claim n ty ctxt env t =
273 do (tyv, tyt) <- lift $ check ctxt env ty
274 lift $ isType ctxt env tyt
275 action (\ps -> let (g:gs) = holes ps in
276 ps { holes = g : n : gs } )
277 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
279reorder_claims :: RunTactic
280reorder_claims ctxt env t
281 = -- trace (showSep "\n" (map show (scvs t))) $
282 let (bs, sc) = scvs t []
283 newbs = reverse (sortB (reverse bs)) in
284 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
285 return (bindAll newbs sc)
286 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
287 scvs sc acc = (reverse acc, sc)
289 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
290 sortB [] = []
291 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
292 | otherwise = sortB (insertB x xs)
294 insertB x [] = [x]
295 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
296 | otherwise = y : insertB x ys
298 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
299 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
300 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
302focus :: Name -> RunTactic
303focus n ctxt env t = do action (\ps -> let hs = holes ps in
304 if n `elem` hs
305 then ps { holes = n : (hs \\ [n]) }
306 else ps)
307 ps <- get
308 return t
310movelast :: Name -> RunTactic
311movelast n ctxt env t = do action (\ps -> let hs = holes ps in
312 if n `elem` hs
313 then ps { holes = (hs \\ [n]) ++ [n] }
314 else ps)
315 return t
317instanceArg :: Name -> RunTactic
318instanceArg n ctxt env (Bind x (Hole t) sc)
319 = do action (\ps -> let hs = holes ps
320 is = instances ps in
321 ps { holes = (hs \\ [x]) ++ [x],
322 instances = x:is })
323 return (Bind x (Hole t) sc)
325setinj :: Name -> RunTactic
326setinj n ctxt env (Bind x (Hole t) sc)
327 = do action (\ps -> let is = injective ps in
328 ps { injective = n : is })
329 return (Bind x (Hole t) sc)
331defer :: Name -> RunTactic
332defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
333 do action (\ps -> let hs = holes ps in
334 ps { holes = hs \\ [x] })
335 return (Bind n (GHole (mkTy (reverse env) t))
336 (mkApp (P Ref n ty) (map getP (reverse env))))
337 where
338 mkTy [] t = t
339 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
341 getP (n, b) = P Bound n (binderTy b)
343-- as defer, but build the type and application explicitly
344deferType :: Name -> Raw -> [Name] -> RunTactic
345deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
346 do (fty, _) <- lift $ check ctxt env fty_in
347 action (\ps -> let hs = holes ps
348 ds = deferred ps in
349 ps { holes = hs \\ [x],
350 deferred = n : ds })
351 return (Bind n (GHole fty)
352 (mkApp (P Ref n ty) (map getP args)))
353 where
354 getP n = case lookup n env of
355 Just b -> P Bound n (binderTy b)
356 Nothing -> error ("deferType can't find " ++ show n)
358regret :: RunTactic
359regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
360 do action (\ps -> let hs = holes ps in
361 ps { holes = hs \\ [x] })
362 return sc
363regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
365exact :: Raw -> RunTactic
366exact guess ctxt env (Bind x (Hole ty) sc) =
367 do (val, valty) <- lift $ check ctxt env guess
368 lift $ converts ctxt env valty ty
369 return $ Bind x (Guess ty val) sc
370exact _ _ _ _ = fail "Can't fill here."
372-- As exact, but attempts to solve other goals by unification
374fill :: Raw -> RunTactic
375fill guess ctxt env (Bind x (Hole ty) sc) =
376 do (val, valty) <- lift $ check ctxt env guess
377-- let valtyn = normalise ctxt env valty
378-- let tyn = normalise ctxt env ty
379 ns <- unify' ctxt env valty ty
380 ps <- get
381 let (uh, uns) = unified ps
382-- put (ps { unified = (uh, uns ++ ns) })
383-- addLog (show (uh, uns ++ ns))
384 return $ Bind x (Guess ty val) sc
385fill _ _ _ _ = fail "Can't fill here."
387-- As fill, but attempts to solve other goals by matching
389match_fill :: Raw -> RunTactic
390match_fill guess ctxt env (Bind x (Hole ty) sc) =
391 do (val, valty) <- lift $ check ctxt env guess
392-- let valtyn = normalise ctxt env valty
393-- let tyn = normalise ctxt env ty
394 ns <- match_unify' ctxt env valty ty
395 ps <- get
396 let (uh, uns) = unified ps
397-- put (ps { unified = (uh, uns ++ ns) })
398-- addLog (show (uh, uns ++ ns))
399 return $ Bind x (Guess ty val) sc
400match_fill _ _ _ _ = fail "Can't fill here."
402prep_fill :: Name -> [Name] -> RunTactic
403prep_fill f as ctxt env (Bind x (Hole ty) sc) =
404 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
405 return $ Bind x (Guess ty val) sc
406prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
408complete_fill :: RunTactic
409complete_fill ctxt env (Bind x (Guess ty val) sc) =
410 do let guess = forget val
411 (val', valty) <- lift $ check ctxt env guess
412 ns <- unify' ctxt env valty ty
413 ps <- get
414 let (uh, uns) = unified ps
415-- put (ps { unified = (uh, uns ++ ns) })
416 return $ Bind x (Guess ty val) sc
417complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
419-- When solving something in the 'dont unify' set, we should check
420-- that the guess we are solving it with unifies with the thing unification
421-- found for it, if anything.
423solve :: RunTactic
424solve ctxt env (Bind x (Guess ty val) sc)
425 | True = do ps <- get
426 let (uh, uns) = unified ps
427 case lookup x (notunified ps) of
428 Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $
429 -- return []
430 unify' ctxt env tm val
431 _ -> return []
432 action (\ps -> ps { holes = holes ps \\ [x],
433 solved = Just (x, val),
434-- problems = solveInProblems
435-- x val (problems ps),
436 -- dontunify = dontunify ps \\ [x],
437 -- unified = (uh, uns ++ [(x, val)]),
438 instances = instances ps \\ [x] })
439 return $ {- Bind x (Let ty val) sc -}
440 instantiate val (pToV x sc)
441 | otherwise = lift $ tfail $ IncompleteTerm val
442solve _ _ h@(Bind x t sc)
443 = do ps <- get
444 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
446introTy :: Raw -> Maybe Name -> RunTactic
447introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
448 do let n = case mn of
449 Just name -> name
450 Nothing -> x
451 let t' = case t of
452 x@(Bind y (Pi s) _) -> x
453 _ -> hnf ctxt env t
454 (tyv, tyt) <- lift $ check ctxt env ty
455-- ns <- lift $ unify ctxt env tyv t'
456 case t' of
457 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
458 do ns <- unify' ctxt env s tyv
459 ps <- get
460 let (uh, uns) = unified ps
461-- put (ps { unified = (uh, uns ++ ns) })
462 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
463 _ -> lift $ tfail $ CantIntroduce t'
464introTy ty n ctxt env _ = fail "Can't introduce here."
466intro :: Maybe Name -> RunTactic
467intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
468 do let n = case mn of
469 Just name -> name
470 Nothing -> x
471 let t' = case t of
472 x@(Bind y (Pi s) _) -> x
473 _ -> hnf ctxt env t
474 case t' of
475 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
476 let t' = instantiate (P Bound n s) (pToV y t) in
477 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
478 _ -> lift $ tfail $ CantIntroduce t'
479intro n ctxt env _ = fail "Can't introduce here."
481forall :: Name -> Raw -> RunTactic
482forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
483 do (tyv, tyt) <- lift $ check ctxt env ty
484 unify' ctxt env tyt (TType (UVar 0))
485 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
486forall n ty ctxt env _ = fail "Can't pi bind here"
488patvar :: Name -> RunTactic
489patvar n ctxt env (Bind x (Hole t) sc) =
490 do action (\ps -> ps { holes = holes ps \\ [x] })
491 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
492patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
494letbind :: Name -> Raw -> Raw -> RunTactic
495letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
496 do (tyv, tyt) <- lift $ check ctxt env ty
497 (valv, valt) <- lift $ check ctxt env val
498 lift $ isType ctxt env tyt
499 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
500letbind n ty val ctxt env _ = fail "Can't let bind here"
502rewrite :: Raw -> RunTactic
503rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
504 do (tmv, tmt) <- lift $ check ctxt env tm
505 let tmt' = normalise ctxt env tmt
506 case unApply tmt' of
507 (P _ (UN "=") _, [lt,rt,l,r]) ->
508 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
509 let newt = mkP l r l t
510 let sc = forget $ (Bind x (Hole newt)
511 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
512 [lt, l, r, p, tmv, xp]))
513 (scv, sct) <- lift $ check ctxt env sc
514 return scv
515 _ -> fail "Not an equality type"
516 where
517 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
518 -- an x, and put \x : lt in front
519 mkP lt l r ty | l == ty = lt
520 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
521 a' = if (r /= a) then mkP lt l r a else a in
522 App f' a'
523 mkP lt l r (Bind n b sc)
524 = let b' = mkPB b
525 sc' = if (r /= sc) then mkP lt l r sc else sc in
526 Bind n b' sc'
527 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
528 v' = if (r /= v) then mkP lt l r v else v in
529 Let t' v'
530 mkPB b = let ty = binderTy b
531 ty' = if (r /= ty) then mkP lt l r ty else ty in
532 b { binderTy = ty' }
533 mkP lt l r x = x
535 rname = MN 0 "replaced"
536rewrite _ _ _ _ = fail "Can't rewrite here"
538patbind :: Name -> RunTactic
539patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
540 do let t' = case t of
541 x@(Bind y (PVTy s) t) -> x
542 _ -> hnf ctxt env t
543 case t' of
544 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
545 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
546 _ -> fail "Nothing to pattern bind"
547patbind n ctxt env _ = fail "Can't pattern bind here"
549compute :: RunTactic
550compute ctxt env (Bind x (Hole ty) sc) =
551 do return $ Bind x (Hole (normalise ctxt env ty)) sc
552compute ctxt env t = return t
554hnf_compute :: RunTactic
555hnf_compute ctxt env (Bind x (Hole ty) sc) =
556 do let ty' = hnf ctxt env ty in
557-- trace ("HNF " ++ show (ty, ty')) $
558 return $ Bind x (Hole ty') sc
559hnf_compute ctxt env t = return t
561check_in :: Raw -> RunTactic
562check_in t ctxt env tm =
563 do (val, valty) <- lift $ check ctxt env t
564 addLog (showEnv env val ++ " : " ++ showEnv env valty)
565 return tm
567eval_in :: Raw -> RunTactic
568eval_in t ctxt env tm =
569 do (val, valty) <- lift $ check ctxt env t
570 let val' = normalise ctxt env val
571 let valty' = normalise ctxt env valty
572 addLog (showEnv env val ++ " : " ++
573 showEnv env valty ++
574-- " in " ++ show env ++
575 " ==>\n " ++
576 showEnv env val' ++ " : " ++
577 showEnv env valty')
578 return tm
580start_unify :: Name -> RunTactic
581start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
582 return tm
584tmap f (a, b, c) = (f a, b, c)
586solve_unified :: RunTactic
587solve_unified ctxt env tm =
588 do ps <- get
589 let (_, ns) = unified ps
590 let unify = dropGiven (dontunify ps) ns (holes ps)
591 action (\ps -> ps { holes = holes ps \\ map fst unify })
592 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
593 return (updateSolved unify tm)
594 where
596dropGiven du [] hs = []
597dropGiven du ((n, P Bound t ty) : us) hs
598 | n `elem` du && not (t `elem` du)
599 && n `elem` hs && t `elem` hs
600 = (t, P Bound n ty) : dropGiven du us hs
601dropGiven du (u@(n, _) : us) hs
602 | n `elem` du = dropGiven du us hs
603-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
604dropGiven du (u : us) hs = u : dropGiven du us hs
606keepGiven du [] hs = []
607keepGiven du ((n, P Bound t ty) : us) hs
608 | n `elem` du && not (t `elem` du)
609 && n `elem` hs && t `elem` hs
610 = keepGiven du us hs
611keepGiven du (u@(n, _) : us) hs
612 | n `elem` du = u : keepGiven du us hs
613keepGiven du (u : us) hs = keepGiven du us hs
615updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
616 updateSolved' xs x
617updateSolved' xs (Bind n (Hole ty) t)
618 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
619updateSolved' xs (Bind n b t)
620 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
621updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
622updateSolved' xs (P _ n _)
623 | Just v <- lookup n xs = v
624updateSolved' xs t = t
626updateEnv ns [] = []
627updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
629updateError ns (CantUnify b l r e xs sc)
630 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
631updateError ns e = e
633solveInProblems x val [] = []
634solveInProblems x val ((l, r, env, err) : ps)
635 = ((instantiate val (pToV x l), instantiate val (pToV x r),
636 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
638updateProblems ctxt ns ps inj holes = up ns ps where
639 up ns [] = (ns, [])
640 up ns ((x, y, env, err) : ps) =
641 let x' = updateSolved ns x
642 y' = updateSolved ns y
643 err' = updateError ns err
644 env' = updateEnv ns env in
645 case unify ctxt env' x' y' inj holes of
646 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
647 up (ns ++ v) ps
648 _ -> let (ns', ps') = up ns ps in
649 (ns', (x',y',env',err') : ps')
651processTactic :: Tactic -> ProofState -> TC (ProofState, String)
652processTactic QED ps = case holes ps of
653 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
654 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
655 return (ps { done = True, pterm = tm' },
656 "Proof complete: " ++ showEnv [] tm')
657 _ -> fail "Still holes to fill."
658processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
659processTactic Undo ps = case previous ps of
660 Nothing -> fail "Nothing to undo."
661 Just pold -> return (pold, "")
662processTactic EndUnify ps
663 = let (h, ns_in) = unified ps
664 ns = dropGiven (dontunify ps) ns_in (holes ps)
665 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
666 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
667 (injective ps) (holes ps)
668 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
669 updateSolved ns'' (pterm ps) in
670 return (ps { pterm = tm',
671 unified = (h, []),
672 problems = probs',
673 holes = holes ps \\ map fst ns'' }, "")
674processTactic (Reorder n) ps
675 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
676 return (ps' { previous = Just ps, plog = "" }, plog ps')
677processTactic t ps
678 = case holes ps of
679 [] -> fail "Nothing to fill in."
680 (h:_) -> do ps' <- execStateT (process t h) ps
681 let pterm' = case solved ps' of
682 Just s -> updateSolved [s] (pterm ps')
683 _ -> pterm ps'
684 let (ns', probs')
685 = case solved ps' of
686 Just s -> updateProblems (context ps')
687 [s] (problems ps')
688 (injective ps')
689 (holes ps')
690 _ -> ([], problems ps')
691 -- rechecking problems may find more solutions, so
692 -- apply them here
693 let pterm'' = updateSolved ns' pterm'
694 return (ps' { pterm = pterm'',
695 solved = Nothing,
696 problems = probs',
697 previous = Just ps, plog = "",
698 holes = holes ps' \\ (map fst ns')}, plog ps')
700process :: Tactic -> Name -> StateT TState TC ()
701process EndUnify _
702 = do ps <- get
703 let (h, _) = unified ps
704 tactic (Just h) solve_unified
705process t h = tactic (Just h) (mktac t)
706 where mktac Attack = attack
707 mktac (Claim n r) = claim n r
708 mktac (Exact r) = exact r
709 mktac (Fill r) = fill r
710 mktac (MatchFill r) = match_fill r
711 mktac (PrepFill n ns) = prep_fill n ns
712 mktac CompleteFill = complete_fill
713 mktac Regret = regret
714 mktac Solve = solve
715 mktac (StartUnify n) = start_unify n
716 mktac Compute = compute
717 mktac HNF_Compute = hnf_compute
718 mktac (Intro n) = intro n
719 mktac (IntroTy ty n) = introTy ty n
720 mktac (Forall n t) = forall n t
721 mktac (LetBind n t v) = letbind n t v
722 mktac (Rewrite t) = rewrite t
723 mktac (PatVar n) = patvar n
724 mktac (PatBind n) = patbind n
725 mktac (CheckIn r) = check_in r
726 mktac (EvalIn r) = eval_in r
727 mktac (Focus n) = focus n
728 mktac (Defer n) = defer n
729 mktac (DeferType n t a) = deferType n t a
730 mktac (Instance n) = instanceArg n
731 mktac (SetInjective n) = setinj n
732 mktac (MoveLast n) = movelast n