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