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