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