git.iko.soy/Idris-dev
on ce2d69d help sign in
Idris-dev/src/Core/ProofState.hs
869 lines 36 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
7module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic,
9 dropGiven, keepGiven) where
11import Core.Typecheck
12import Core.Evaluate
13import Core.TT
14import Core.Unify
16import Control.Monad.State
17import Control.Applicative hiding (empty)
18import Data.List
19import Debug.Trace
21import Util.Pretty
23data ProofState = PS { thname :: Name,
24 holes :: [Name], -- holes still to be solved
25 usedns :: [Name], -- used names, don't use again
26 nextname :: Int, -- name supply
27 pterm :: Term, -- current proof term
28 ptype :: Type, -- original goal
29 dontunify :: [Name], -- explicitly given by programmer, leave it
30 unified :: (Name, [(Name, Term)]),
31 notunified :: [(Name, Term)],
32 solved :: Maybe (Name, Term),
33 problems :: Fails,
34 injective :: [Name],
35 deferred :: [Name], -- names we'll need to define
36 instances :: [Name], -- instance arguments (for type classes)
37 previous :: Maybe ProofState, -- for undo
38 context :: Context,
39 plog :: String,
40 unifylog :: Bool,
41 done :: Bool
42 }
44data Goal = GD { premises :: Env,
45 goalType :: Binder Term
46 }
48data Tactic = Attack
49 | Claim Name Raw
50 | Reorder Name
51 | Exact Raw
52 | Fill Raw
53 | MatchFill Raw
54 | PrepFill Name [Name]
55 | CompleteFill
56 | Regret
57 | Solve
58 | StartUnify Name
59 | EndUnify
60 | Compute
61 | ComputeLet Name
62 | Simplify
63 | HNF_Compute
64 | EvalIn Raw
65 | CheckIn Raw
66 | Intro (Maybe Name)
67 | IntroTy Raw (Maybe Name)
68 | Forall Name Raw
69 | LetBind Name Raw Raw
70 | ExpandLet Name Term
71 | Rewrite Raw
72 | Induction Name
73 | Equiv Raw
74 | PatVar Name
75 | PatBind Name
76 | Focus Name
77 | Defer Name
78 | DeferType Name Raw [Name]
79 | Instance Name
80 | SetInjective Name
81 | MoveLast Name
82 | MatchProblems
83 | UnifyProblems
84 | ProofState
85 | Undo
86 | QED
87 deriving Show
89-- Some utilites on proof and tactic states
91instance Show ProofState where
92 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _)
93 = show nm ++ ": no more goals"
94 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _)
95 = let OK g = goal (Just h) tm
96 wkenv = premises g in
97 "Other goals: " ++ show hs ++ "\n" ++
98 showPs wkenv (reverse wkenv) ++ "\n" ++
99 "-------------------------------- (" ++ show nm ++
100 ") -------\n " ++
101 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
102 where showPs env [] = ""
103 showPs env ((n, Let t v):bs)
104 = " " ++ show n ++ " : " ++
105 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
106 showEnv env ({- normalise ctxt env -} v) ++
107 "\n" ++ showPs env bs
108 showPs env ((n, b):bs)
109 = " " ++ show n ++ " : " ++
110 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
111 "\n" ++ showPs env bs
112 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
113 " =?= " ++ showEnv ps v
114 showG ps b = showEnv ps (binderTy b)
116instance Pretty ProofState where
117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
118 if size nm > breakingSize then
119 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
120 else
121 pretty nm <> colon <+> text " no more goals."
122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
123 let OK g = goal (Just h) tm in
124 let wkEnv = premises g in
125 text "Other goals" <+> colon <+> pretty hs $$
126 prettyPs wkEnv (reverse wkEnv) $$
127 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
129 where
130 prettyGoal ps (Guess t v) =
131 if size v > breakingSize then
132 prettyEnv ps t <+> text "=?=" $$
133 nest nestingSize (prettyEnv ps v)
134 else
135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
136 prettyGoal ps b = prettyEnv ps $ binderTy b
138 prettyPs env [] = empty
139 prettyPs env ((n, Let t v):bs) =
140 nest nestingSize (pretty n <+> colon <+>
141 if size v > breakingSize then
142 prettyEnv env t <+> text "=" $$
143 nest nestingSize (prettyEnv env v) $$
144 nest nestingSize (prettyPs env bs)
145 else
146 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
147 nest nestingSize (prettyPs env bs))
148 prettyPs env ((n, b):bs) =
149 if size (binderTy b) > breakingSize then
150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
151 else
152 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
153 nest nestingSize (prettyPs env bs))
155same Nothing n = True
156same (Just x) n = x == n
158hole (Hole _) = True
159hole (Guess _ _) = True
160hole _ = False
162holeName i = MN i "hole"
164qshow :: Fails -> String
165qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
167match_unify' :: Context -> Env -> TT Name -> TT Name ->
168 StateT TState TC [(Name, TT Name)]
169match_unify' ctxt env topx topy =
170 do ps <- get
171 let dont = dontunify ps
172 u <- lift $ match_unify ctxt env topx topy dont (holes ps)
173 let (h, ns) = unified ps
174 put (ps { unified = (h, u ++ ns) })
175 return u
177unify' :: Context -> Env -> TT Name -> TT Name ->
178 StateT TState TC [(Name, TT Name)]
179unify' ctxt env topx topy =
180 do ps <- get
181 let dont = dontunify ps
182 (u, fails) <- traceWhen (unifylog ps)
183 ("Trying " ++ show (topx, topy) ++
184 " in " ++ show env ++
185 "\nHoles: " ++ show (holes ps) ++ "\n") $
186 lift $ unify ctxt env topx topy dont (holes ps)
187 traceWhen (unifylog ps)
188 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
189 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
190 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
191-- ++ show (pterm ps)
192 ++ "\n----------") $
193 case fails of
194-- [] -> return u
195 err ->
196 do ps <- get
197 let (h, ns) = unified ps
198 let (ns', probs') = updateProblems (context ps) (u ++ ns)
199 (err ++ problems ps)
200 (injective ps)
201 (holes ps)
202 put (ps { problems = probs',
203 unified = (h, ns') })
204 return u
206getName :: Monad m => String -> StateT TState m Name
207getName tag = do ps <- get
208 let n = nextname ps
209 put (ps { nextname = n+1 })
210 return $ MN n tag
212action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
213action a = do ps <- get
214 put (a ps)
216addLog :: Monad m => String -> StateT TState m ()
217addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
219newProof :: Name -> Context -> Type -> ProofState
220newProof n ctxt ty = let h = holeName 0
221 ty' = vToP ty in
222 PS n [h] [] 1 (Bind h (Hole ty')
223 (P Bound h ty')) ty [] (h, []) []
224 Nothing [] []
225 [] []
226 Nothing ctxt "" False False
228type TState = ProofState -- [TacticAction])
229type RunTactic = Context -> Env -> Term -> StateT TState TC Term
230type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
232envAtFocus :: ProofState -> TC Env
233envAtFocus ps
234 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
235 return (premises g)
236 | otherwise = fail "No holes"
238goalAtFocus :: ProofState -> TC (Binder Type)
239goalAtFocus ps
240 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
241 return (goalType g)
242 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (pterm ps)
244goal :: Hole -> Term -> TC Goal
245goal h tm = g [] tm where
246 g env (Bind n b@(Guess _ _) sc)
247 | same h n = return $ GD env b
248 | otherwise
249 = gb env b `mplus` g ((n, b):env) sc
250 g env (Bind n b sc) | hole b && same h n = return $ GD env b
251 | otherwise
252 = g ((n, b):env) sc `mplus` gb env b
253 g env (App f a) = g env f `mplus` g env a
254 g env t = fail "Can't find hole"
256 gb env (Let t v) = g env v `mplus` g env t
257 gb env (Guess t v) = g env v `mplus` g env t
258 gb env t = g env (binderTy t)
260tactic :: Hole -> RunTactic -> StateT TState TC ()
261tactic h f = do ps <- get
262 (tm', _) <- atH (context ps) [] (pterm ps)
263 ps <- get -- might have changed while processing
264 put (ps { pterm = tm' })
265 where
266 updated o = do o' <- o
267 return (o', True)
269 ulift2 c env op a b
270 = do (b', u) <- atH c env b
271 if u then return (op a b', True)
272 else do (a', u) <- atH c env a
273 return (op a' b', u)
275 -- Search the things most likely to contain the binding first!
277 atH :: Context -> Env -> Term -> StateT TState TC (Term, Bool)
278 atH c env binder@(Bind n b@(Guess t v) sc)
279 | same h n = updated (f c env binder)
280 | otherwise
281 = do -- binder first
282 (b', u) <- ulift2 c env Guess t v
283 if u then return (Bind n b' sc, True)
284 else do (sc', u) <- atH c ((n, b) : env) sc
285 return (Bind n b' sc', u)
286 atH c env binder@(Bind n b sc)
287 | hole b && same h n = updated (f c env binder)
288 | otherwise -- scope first
289 = do (sc', u) <- atH c ((n, b) : env) sc
290 if u then return (Bind n b sc', True)
291 else do (b', u) <- atHb c env b
292 return (Bind n b' sc', u)
293 atH c env (App f a) = ulift2 c env App f a
294 atH c env t = return (t, False)
296 atHb c env (Let t v) = ulift2 c env Let t v
297 atHb c env (Guess t v) = ulift2 c env Guess t v
298 atHb c env t = do (ty', u) <- atH c env (binderTy t)
299 return (t { binderTy = ty' }, u)
301computeLet :: Context -> Name -> Term -> Term
302computeLet ctxt n tm = cl [] tm where
303 cl env (Bind n' (Let t v) sc)
304 | n' == n = let v' = normalise ctxt env v in
305 Bind n' (Let t v') sc
306 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
307 cl env (App f a) = App (cl env f) (cl env a)
308 cl env t = t
310attack :: RunTactic
311attack ctxt env (Bind x (Hole t) sc)
312 = do h <- getName "hole"
313 action (\ps -> ps { holes = h : holes ps })
314 return $ Bind x (Guess t (newtm h)) sc
315 where
316 newtm h = Bind h (Hole t) (P Bound h t)
317attack ctxt env _ = fail "Not an attackable hole"
319claim :: Name -> Raw -> RunTactic
320claim n ty ctxt env t =
321 do (tyv, tyt) <- lift $ check ctxt env ty
322 lift $ isType ctxt env tyt
323 action (\ps -> let (g:gs) = holes ps in
324 ps { holes = g : n : gs } )
325 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
327reorder_claims :: RunTactic
328reorder_claims ctxt env t
329 = -- trace (showSep "\n" (map show (scvs t))) $
330 let (bs, sc) = scvs t []
331 newbs = reverse (sortB (reverse bs)) in
332 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
333 return (bindAll newbs sc)
334 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
335 scvs sc acc = (reverse acc, sc)
337 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
338 sortB [] = []
339 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
340 | otherwise = sortB (insertB x xs)
342 insertB x [] = [x]
343 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
344 | otherwise = y : insertB x ys
346 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
347 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
348 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
350focus :: Name -> RunTactic
351focus n ctxt env t = do action (\ps -> let hs = holes ps in
352 if n `elem` hs
353 then ps { holes = n : (hs \\ [n]) }
354 else ps)
355 ps <- get
356 return t
358movelast :: Name -> RunTactic
359movelast n ctxt env t = do action (\ps -> let hs = holes ps in
360 if n `elem` hs
361 then ps { holes = (hs \\ [n]) ++ [n] }
362 else ps)
363 return t
365instanceArg :: Name -> RunTactic
366instanceArg n ctxt env (Bind x (Hole t) sc)
367 = do action (\ps -> let hs = holes ps
368 is = instances ps in
369 ps { holes = (hs \\ [x]) ++ [x],
370 instances = x:is })
371 return (Bind x (Hole t) sc)
373setinj :: Name -> RunTactic
374setinj n ctxt env (Bind x (Hole t) sc)
375 = do action (\ps -> let is = injective ps in
376 ps { injective = n : is })
377 return (Bind x (Hole t) sc)
379defer :: Name -> RunTactic
380defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
381 do action (\ps -> let hs = holes ps in
382 ps { holes = hs \\ [x] })
383 return (Bind n (GHole (length env) (mkTy (reverse env) t))
384 (mkApp (P Ref n ty) (map getP (reverse env))))
385 where
386 mkTy [] t = t
387 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
389 getP (n, b) = P Bound n (binderTy b)
391-- as defer, but build the type and application explicitly
392deferType :: Name -> Raw -> [Name] -> RunTactic
393deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
394 do (fty, _) <- lift $ check ctxt env fty_in
395 action (\ps -> let hs = holes ps
396 ds = deferred ps in
397 ps { holes = hs \\ [x],
398 deferred = n : ds })
399 return (Bind n (GHole 0 fty)
400 (mkApp (P Ref n ty) (map getP args)))
401 where
402 getP n = case lookup n env of
403 Just b -> P Bound n (binderTy b)
404 Nothing -> error ("deferType can't find " ++ show n)
406regret :: RunTactic
407regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
408 do action (\ps -> let hs = holes ps in
409 ps { holes = hs \\ [x] })
410 return sc
411regret ctxt env (Bind x (Hole t) _)
412 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
414exact :: Raw -> RunTactic
415exact guess ctxt env (Bind x (Hole ty) sc) =
416 do (val, valty) <- lift $ check ctxt env guess
417 lift $ converts ctxt env valty ty
418 return $ Bind x (Guess ty val) sc
419exact _ _ _ _ = fail "Can't fill here."
421-- As exact, but attempts to solve other goals by unification
423fill :: Raw -> RunTactic
424fill guess ctxt env (Bind x (Hole ty) sc) =
425 do (val, valty) <- lift $ check ctxt env guess
426-- let valtyn = normalise ctxt env valty
427-- let tyn = normalise ctxt env ty
428 ns <- unify' ctxt env valty ty
429 ps <- get
430 let (uh, uns) = unified ps
431-- put (ps { unified = (uh, uns ++ ns) })
432-- addLog (show (uh, uns ++ ns))
433 return $ Bind x (Guess ty val) sc
434fill _ _ _ _ = fail "Can't fill here."
436-- As fill, but attempts to solve other goals by matching
438match_fill :: Raw -> RunTactic
439match_fill guess ctxt env (Bind x (Hole ty) sc) =
440 do (val, valty) <- lift $ check ctxt env guess
441-- let valtyn = normalise ctxt env valty
442-- let tyn = normalise ctxt env ty
443 ns <- match_unify' ctxt env valty ty
444 ps <- get
445 let (uh, uns) = unified ps
446-- put (ps { unified = (uh, uns ++ ns) })
447-- addLog (show (uh, uns ++ ns))
448 return $ Bind x (Guess ty val) sc
449match_fill _ _ _ _ = fail "Can't fill here."
451prep_fill :: Name -> [Name] -> RunTactic
452prep_fill f as ctxt env (Bind x (Hole ty) sc) =
453 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
454 return $ Bind x (Guess ty val) sc
455prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
457complete_fill :: RunTactic
458complete_fill ctxt env (Bind x (Guess ty val) sc) =
459 do let guess = forget val
460 (val', valty) <- lift $ check ctxt env guess
461 ns <- unify' ctxt env valty ty
462 ps <- get
463 let (uh, uns) = unified ps
464-- put (ps { unified = (uh, uns ++ ns) })
465 return $ Bind x (Guess ty val) sc
466complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
468-- When solving something in the 'dont unify' set, we should check
469-- that the guess we are solving it with unifies with the thing unification
470-- found for it, if anything.
472solve :: RunTactic
473solve ctxt env (Bind x (Guess ty val) sc)
474 | True = do ps <- get
475 let (uh, uns) = unified ps
476 case lookup x (notunified ps) of
477 Just tm -> do -- trace ("AVOIDED " ++ show (x, tm, val)) $
478 -- return []
479 unify' ctxt env tm val
480 _ -> return []
481 action (\ps -> ps { holes = holes ps \\ [x],
482 solved = Just (x, val),
483-- problems = solveInProblems
484-- x val (problems ps),
485 -- dontunify = dontunify ps \\ [x],
486 -- unified = (uh, uns ++ [(x, val)]),
487 instances = instances ps \\ [x] })
488 let tm' = instantiate val (pToV x sc) in
489 return tm'
490 | otherwise = lift $ tfail $ IncompleteTerm val
491solve _ _ h@(Bind x t sc)
492 = do ps <- get
493 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
495introTy :: Raw -> Maybe Name -> RunTactic
496introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
497 do let n = case mn of
498 Just name -> name
499 Nothing -> x
500 let t' = case t of
501 x@(Bind y (Pi s) _) -> x
502 _ -> hnf ctxt env t
503 (tyv, tyt) <- lift $ check ctxt env ty
504-- ns <- lift $ unify ctxt env tyv t'
505 case t' of
506 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
507 do ns <- unify' ctxt env s tyv
508 ps <- get
509 let (uh, uns) = unified ps
510-- put (ps { unified = (uh, uns ++ ns) })
511 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
512 _ -> lift $ tfail $ CantIntroduce t'
513introTy ty n ctxt env _ = fail "Can't introduce here."
515intro :: Maybe Name -> RunTactic
516intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
517 do let n = case mn of
518 Just name -> name
519 Nothing -> x
520 let t' = case t of
521 x@(Bind y (Pi s) _) -> x
522 _ -> hnf ctxt env t
523 case t' of
524 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $
525 let t' = instantiate (P Bound n s) (pToV y t) in
526 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
527 _ -> lift $ tfail $ CantIntroduce t'
528intro n ctxt env _ = fail "Can't introduce here."
530forall :: Name -> Raw -> RunTactic
531forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
532 do (tyv, tyt) <- lift $ check ctxt env ty
533 unify' ctxt env tyt (TType (UVar 0))
534 unify' ctxt env t (TType (UVar 0))
535 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
536forall n ty ctxt env _ = fail "Can't pi bind here"
538patvar :: Name -> RunTactic
539patvar n ctxt env (Bind x (Hole t) sc) =
540 do action (\ps -> ps { holes = holes ps \\ [x] })
541 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
542patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
544letbind :: Name -> Raw -> Raw -> RunTactic
545letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
546 do (tyv, tyt) <- lift $ check ctxt env ty
547 (valv, valt) <- lift $ check ctxt env val
548 lift $ isType ctxt env tyt
549 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
550letbind n ty val ctxt env _ = fail "Can't let bind here"
552expandLet :: Name -> Term -> RunTactic
553expandLet n v ctxt env tm =
554 return $ subst n v tm
556rewrite :: Raw -> RunTactic
557rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
558 do (tmv, tmt) <- lift $ check ctxt env tm
559 let tmt' = normalise ctxt env tmt
560 case unApply tmt' of
561 (P _ (UN "=") _, [lt,rt,l,r]) ->
562 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
563 let newt = mkP l r l t
564 let sc = forget $ (Bind x (Hole newt)
565 (mkApp (P Ref (UN "replace") (TType (UVal 0)))
566 [lt, l, r, p, tmv, xp]))
567 (scv, sct) <- lift $ check ctxt env sc
568 return scv
569 _ -> fail "Not an equality type"
570 where rname = MN 0 "replaced"
571rewrite _ _ _ _ = fail "Can't rewrite here"
573-- To make the P for rewrite, replace syntactic occurrences of l in ty with
574-- an x, and put \x : lt in front
575mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
576mkP lt l r ty | l == ty = lt
577mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
578 a' = if (r /= a) then mkP lt l r a else a in
579 App f' a'
580mkP lt l r (Bind n b sc)
581 = let b' = mkPB b
582 sc' = if (r /= sc) then mkP lt l r sc else sc in
583 Bind n b' sc'
584 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
585 v' = if (r /= v) then mkP lt l r v else v in
586 Let t' v'
587 mkPB b = let ty = binderTy b
588 ty' = if (r /= ty) then mkP lt l r ty else ty in
589 b { binderTy = ty' }
590mkP lt l r x = x
592induction :: Name -> RunTactic
593induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
594 (tmv, tmt) <- lift $ check ctxt env (Var nm)
595 let tmt' = normalise ctxt env tmt
596 case unApply tmt' of
597 (P _ tnm _, pms@[]) -> do
598 case lookupTy (SN (ElimN tnm)) ctxt of
599 [elimTy] -> do
600 let args = getArgTys elimTy
601 let pmargs = take (length pms) args -- TODO: Fill these correctly when having multiple parameters working
602 let args' = drop (length pms) args
603 let propTy = head args'
604 let consargs = init $ tail args -- TODO: This is incorrect when type has indicies, get indicies and use the correct count
605 let scr = last $ tail args
606 let prop = Bind nm (Lam tmt') t -- TODO: Make this work for types with indicies
607 let res = substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0))) ([prop] ++ map makeConsArg consargs ++ [tmv]))
608 action (\ps -> ps {holes = holes ps \\ [x]})
609 mapM_ addConsHole (reverse consargs)
610 let res' = forget $ res
611 (scv, sct) <- lift $ check ctxt env res'
612 let scv' = specialise ctxt env [] scv
613 return scv'
614 [] -> fail $ "Induction needs an eliminator for " ++ show nm
615 xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show nm
616 (P _ nm _, _) -> fail "Induction not yet supported for types with arguments"
617 _ -> fail "Unkown type for induction"
618 where scname = MN 0 "scarg"
619 makeConsArg (nm, ty) = P Bound nm ty
620 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
621 bindConsArgs [] v = v
622 addConsHole (nm, ty) =
623 action (\ps -> ps { holes = nm : holes ps })
624induction tm ctxt env _ = do fail "Can't do induction here"
627equiv :: Raw -> RunTactic
628equiv tm ctxt env (Bind x (Hole t) sc) =
629 do (tmv, tmt) <- lift $ check ctxt env tm
630 lift $ converts ctxt env tmv t
631 return $ Bind x (Hole tmv) sc
632equiv tm ctxt env _ = fail "Can't equiv here"
634patbind :: Name -> RunTactic
635patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
636 do let t' = case t of
637 x@(Bind y (PVTy s) t) -> x
638 _ -> hnf ctxt env t
639 case t' of
640 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
641 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
642 _ -> fail "Nothing to pattern bind"
643patbind n ctxt env _ = fail "Can't pattern bind here"
645compute :: RunTactic
646compute ctxt env (Bind x (Hole ty) sc) =
647 do return $ Bind x (Hole (normalise ctxt env ty)) sc
648compute ctxt env t = return t
650hnf_compute :: RunTactic
651hnf_compute ctxt env (Bind x (Hole ty) sc) =
652 do let ty' = hnf ctxt env ty in
653-- trace ("HNF " ++ show (ty, ty')) $
654 return $ Bind x (Hole ty') sc
655hnf_compute ctxt env t = return t
657-- reduce let bindings only
658simplify :: RunTactic
659simplify ctxt env (Bind x (Hole ty) sc) =
660 do return $ Bind x (Hole (specialise ctxt env [] ty)) sc
661simplify ctxt env t = return t
663check_in :: Raw -> RunTactic
664check_in t ctxt env tm =
665 do (val, valty) <- lift $ check ctxt env t
666 addLog (showEnv env val ++ " : " ++ showEnv env valty)
667 return tm
669eval_in :: Raw -> RunTactic
670eval_in t ctxt env tm =
671 do (val, valty) <- lift $ check ctxt env t
672 let val' = normalise ctxt env val
673 let valty' = normalise ctxt env valty
674 addLog (showEnv env val ++ " : " ++
675 showEnv env valty ++
676-- " in " ++ show env ++
677 " ==>\n " ++
678 showEnv env val' ++ " : " ++
679 showEnv env valty')
680 return tm
682start_unify :: Name -> RunTactic
683start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
684 return tm
686tmap f (a, b, c) = (f a, b, c)
688solve_unified :: RunTactic
689solve_unified ctxt env tm =
690 do ps <- get
691 let (_, ns) = unified ps
692 let unify = dropGiven (dontunify ps) ns (holes ps)
693 action (\ps -> ps { holes = holes ps \\ map fst unify })
694 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
695 return (updateSolved unify tm)
696 where
698dropGiven du [] hs = []
699dropGiven du ((n, P Bound t ty) : us) hs
700 | n `elem` du && not (t `elem` du)
701 && n `elem` hs && t `elem` hs
702 = (t, P Bound n ty) : dropGiven du us hs
703dropGiven du (u@(n, _) : us) hs
704 | n `elem` du = dropGiven du us hs
705-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
706dropGiven du (u : us) hs = u : dropGiven du us hs
708keepGiven du [] hs = []
709keepGiven du ((n, P Bound t ty) : us) hs
710 | n `elem` du && not (t `elem` du)
711 && n `elem` hs && t `elem` hs
712 = keepGiven du us hs
713keepGiven du (u@(n, _) : us) hs
714 | n `elem` du = u : keepGiven du us hs
715keepGiven du (u : us) hs = keepGiven du us hs
717updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
718 updateSolved' xs x
719updateSolved' xs (Bind n (Hole ty) t)
720 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
721updateSolved' xs (Bind n b t)
722 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
723updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
724updateSolved' xs (P _ n _)
725 | Just v <- lookup n xs = v
726updateSolved' xs t = t
728updateEnv ns [] = []
729updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
731updateError ns (CantUnify b l r e xs sc)
732 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
733updateError ns e = e
735solveInProblems x val [] = []
736solveInProblems x val ((l, r, env, err) : ps)
737 = ((instantiate val (pToV x l), instantiate val (pToV x r),
738 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
740updateProblems ctxt ns ps inj holes = up ns ps where
741 up ns [] = (ns, [])
742 up ns ((x, y, env, err) : ps) =
743 let x' = updateSolved ns x
744 y' = updateSolved ns y
745 err' = updateError ns err
746 env' = updateEnv ns env in
747 case unify ctxt env' x' y' inj holes of
748 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
749 up (ns ++ v) ps
750 _ -> let (ns', ps') = up ns ps in
751 (ns', (x',y',env',err') : ps')
753-- attempt to solve remaining problems with match_unify
754matchProblems ctxt ps inj holes = up [] ps where
755 up ns [] = (ns, [])
756 up ns ((x, y, env, err) : ps) =
757 let x' = updateSolved ns x
758 y' = updateSolved ns y
759 err' = updateError ns err
760 env' = updateEnv ns env in
761 case match_unify ctxt env' x' y' inj holes of
762 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
763 up (ns ++ v) ps
764 _ -> let (ns', ps') = up ns ps in
765 (ns', (x',y',env',err') : ps')
767processTactic :: Tactic -> ProofState -> TC (ProofState, String)
768processTactic QED ps = case holes ps of
769 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
770 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
771 return (ps { done = True, pterm = tm' },
772 "Proof complete: " ++ showEnv [] tm')
773 _ -> fail "Still holes to fill."
774processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
775processTactic Undo ps = case previous ps of
776 Nothing -> fail "Nothing to undo."
777 Just pold -> return (pold, "")
778processTactic EndUnify ps
779 = let (h, ns_in) = unified ps
780 ns = dropGiven (dontunify ps) ns_in (holes ps)
781 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
782 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
783 (injective ps) (holes ps)
784 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
785 updateSolved ns'' (pterm ps) in
786 return (ps { pterm = tm',
787 unified = (h, []),
788 problems = probs',
789 holes = holes ps \\ map fst ns'' }, "")
790processTactic (Reorder n) ps
791 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
792 return (ps' { previous = Just ps, plog = "" }, plog ps')
793processTactic (ComputeLet n) ps
794 = return (ps { pterm = computeLet (context ps) n (pterm ps) }, "")
795processTactic UnifyProblems ps
796 = let (ns', probs') = updateProblems (context ps) []
797 (problems ps)
798 (injective ps)
799 (holes ps)
800 pterm' = updateSolved ns' (pterm ps) in
801 return (ps { pterm = pterm', solved = Nothing, problems = probs',
802 previous = Just ps, plog = "",
803 holes = holes ps \\ (map fst ns') }, plog ps)
804processTactic MatchProblems ps
805 = let (ns', probs') = matchProblems (context ps)
806 (problems ps)
807 (injective ps)
808 (holes ps)
809 pterm' = updateSolved ns' (pterm ps) in
810 return (ps { pterm = pterm', solved = Nothing, problems = probs',
811 previous = Just ps, plog = "",
812 holes = holes ps \\ (map fst ns') }, plog ps)
813processTactic t ps
814 = case holes ps of
815 [] -> fail "Nothing to fill in."
816 (h:_) -> do ps' <- execStateT (process t h) ps
817 let (ns', probs')
818 = case solved ps' of
819 Just s -> updateProblems (context ps')
820 [s] (problems ps')
821 (injective ps')
822 (holes ps')
823 _ -> ([], problems ps')
824 -- rechecking problems may find more solutions, so
825 -- apply them here
826 let pterm'' = updateSolved ns' (pterm ps')
827 return (ps' { pterm = pterm'',
828 solved = Nothing,
829 problems = probs',
830 previous = Just ps, plog = "",
831 holes = holes ps' \\ (map fst ns')}, plog ps')
833process :: Tactic -> Name -> StateT TState TC ()
834process EndUnify _
835 = do ps <- get
836 let (h, _) = unified ps
837 tactic (Just h) solve_unified
838process t h = tactic (Just h) (mktac t)
839 where mktac Attack = attack
840 mktac (Claim n r) = claim n r
841 mktac (Exact r) = exact r
842 mktac (Fill r) = fill r
843 mktac (MatchFill r) = match_fill r
844 mktac (PrepFill n ns) = prep_fill n ns
845 mktac CompleteFill = complete_fill
846 mktac Regret = regret
847 mktac Solve = solve
848 mktac (StartUnify n) = start_unify n
849 mktac Compute = compute
850 mktac Simplify = Core.ProofState.simplify
851 mktac HNF_Compute = hnf_compute
852 mktac (Intro n) = intro n
853 mktac (IntroTy ty n) = introTy ty n
854 mktac (Forall n t) = forall n t
855 mktac (LetBind n t v) = letbind n t v
856 mktac (ExpandLet n b) = expandLet n b
857 mktac (Rewrite t) = rewrite t
858 mktac (Induction t) = induction t
859 mktac (Equiv t) = equiv t
860 mktac (PatVar n) = patvar n
861 mktac (PatBind n) = patbind n
862 mktac (CheckIn r) = check_in r
863 mktac (EvalIn r) = eval_in r
864 mktac (Focus n) = focus n
865 mktac (Defer n) = defer n
866 mktac (DeferType n t a) = deferType n t a
867 mktac (Instance n) = instanceArg n
868 mktac (SetInjective n) = setinj n
869 mktac (MoveLast n) = movelast n