git.iko.soy/Idris-dev
on 0bc69fb help sign in
Idris-dev/src/Core/ProofState.hs
479 lines 19 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) where
10import Core.Typecheck
11import Core.Evaluate
12import Core.TT
13import Core.Unify
15import Control.Monad.State
16import Control.Applicative
17import Data.List
18import Debug.Trace
20data ProofState = PS { thname :: Name,
21 holes :: [Name], -- holes still to be solved
22 nextname :: Int, -- name supply
23 pterm :: Term, -- current proof term
24 ptype :: Type, -- original goal
25 unified :: (Name, [(Name, Term)]),
26 deferred :: [Name], -- names we'll need to define
27 instances :: [Name], -- instance arguments (for type classes)
28 previous :: Maybe ProofState, -- for undo
29 context :: Context,
30 plog :: String,
31 done :: Bool
32 }
34data Goal = GD { premises :: Env,
35 goalType :: Binder Term
36 }
38data Tactic = Attack
39 | Claim Name Raw
40 | Reorder Name
41 | Exact Raw
42 | Fill Raw
43 | PrepFill Name [Name]
44 | CompleteFill
45 | Regret
46 | Solve
47 | StartUnify Name
48 | EndUnify
49 | Compute
50 | EvalIn Raw
51 | CheckIn Raw
52 | Intro (Maybe Name)
53 | IntroTy Raw (Maybe Name)
54 | Forall Name Raw
55 | LetBind Name Raw Raw
56 | Rewrite Raw
57 | PatVar Name
58 | PatBind Name
59 | Focus Name
60 | Defer Name
61 | Instance Name
62 | MoveLast Name
63 | ProofState
64 | Undo
65 | QED
66 deriving Show
68-- Some utilites on proof and tactic states
70instance Show ProofState where
71 show (PS nm [] _ tm _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
72 show (PS nm (h:hs) _ tm _ _ i _ _ ctxt _ _)
73 = let OK g = goal (Just h) tm
74 wkenv = premises g in
75 "Other goals: " ++ show hs ++ "\n" ++
76 showPs wkenv (reverse wkenv) ++ "\n" ++
77 "-------------------------------- (" ++ show nm ++
78 ") -------\n " ++
79 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
80 where showPs env [] = ""
81 showPs env ((n, Let t v):bs)
82 = " " ++ show n ++ " : " ++
83 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
84 showEnv env ({- normalise ctxt env -} v) ++
85 "\n" ++ showPs env bs
86 showPs env ((n, b):bs)
87 = " " ++ show n ++ " : " ++
88 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
89 "\n" ++ showPs env bs
90 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
91 " =?= " ++ showEnv ps v
92 showG ps b = showEnv ps (binderTy b)
94same Nothing n = True
95same (Just x) n = x == n
97hole (Hole _) = True
98hole (Guess _ _) = True
99hole _ = False
101holeName i = MN i "hole"
103getName :: Monad m => String -> StateT TState m Name
104getName tag = do ps <- get
105 let n = nextname ps
106 put (ps { nextname = n+1 })
107 return $ MN n tag
109action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
110action a = do ps <- get
111 put (a ps)
113addLog :: Monad m => String -> StateT TState m ()
114addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
116newProof :: Name -> Context -> Type -> ProofState
117newProof n ctxt ty = let h = holeName 0
118 ty' = vToP ty in
119 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, [])
120 [] []
121 Nothing ctxt "" False
123type TState = ProofState -- [TacticAction])
124type RunTactic = Context -> Env -> Term -> StateT TState TC Term
125type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
127envAtFocus :: ProofState -> TC Env
128envAtFocus ps
129 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
130 return (premises g)
131 | otherwise = fail "No holes"
133goalAtFocus :: ProofState -> TC (Binder Type)
134goalAtFocus ps
135 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
136 return (goalType g)
138goal :: Hole -> Term -> TC Goal
139goal h tm = g [] tm where
140 g env (Bind n b sc) | hole b && same h n = return $ GD env b
141 | otherwise
142 = gb env b `mplus` g ((n, b):env) sc
143 g env (App f a) = g env f `mplus` g env a
144 g env t = fail "Can't find hole"
146 gb env (Let t v) = g env t `mplus` g env v
147 gb env (Guess t v) = g env t `mplus` g env v
148 gb env t = g env (binderTy t)
150tactic :: Hole -> RunTactic -> StateT TState TC ()
151tactic h f = do ps <- get
152 tm' <- atH (context ps) [] (pterm ps)
153 ps <- get -- might have changed while processing
154 put (ps { pterm = tm' })
155 where
156 atH c env binder@(Bind n b sc)
157 | hole b && same h n = f c env binder
158 | otherwise
159 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
160 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
161 atH c env t = return t
163 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
164 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
165 atHb c env t = do ty' <- atH c env (binderTy t)
166 return $ t { binderTy = ty' }
168attack :: RunTactic
169attack ctxt env (Bind x (Hole t) sc)
170 = do h <- getName "hole"
171 action (\ps -> ps { holes = h : holes ps })
172 return $ Bind x (Guess t (newtm h)) sc
173 where
174 newtm h = Bind h (Hole t) (P Bound h t)
175attack ctxt env _ = fail "Not an attackable hole"
177claim :: Name -> Raw -> RunTactic
178claim n ty ctxt env t =
179 do (tyv, tyt) <- lift $ check ctxt env ty
180 lift $ isSet ctxt env tyt
181 action (\ps -> let (g:gs) = holes ps in
182 ps { holes = g : n : gs } )
183 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
185reorder_claims :: RunTactic
186reorder_claims ctxt env t
187 = -- trace (showSep "\n" (map show (scvs t))) $
188 let (bs, sc) = scvs t []
189 newbs = reverse (sortB (reverse bs)) in
190 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
191 return (bindAll newbs sc)
192 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
193 scvs sc acc = (reverse acc, sc)
195 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
196 sortB [] = []
197 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
198 | otherwise = sortB (insertB x xs)
200 insertB x [] = [x]
201 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
202 | otherwise = y : insertB x ys
204 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
205 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
206 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
208focus :: Name -> RunTactic
209focus n ctxt env t = do action (\ps -> let hs = holes ps in
210 if n `elem` hs
211 then ps { holes = n : (hs \\ [n]) }
212 else ps)
213 return t
215movelast :: Name -> RunTactic
216movelast n ctxt env t = do action (\ps -> let hs = holes ps in
217 if n `elem` hs
218 then ps { holes = (hs \\ [n]) ++ [n] }
219 else ps)
220 return t
222instanceArg :: Name -> RunTactic
223instanceArg n ctxt env (Bind x (Hole t) sc)
224 = do action (\ps -> let hs = holes ps
225 is = instances ps in
226 ps { holes = (hs \\ [x]) ++ [x],
227 instances = x:is })
228 return (Bind x (Hole t) sc)
230defer :: Name -> RunTactic
231defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
232 do action (\ps -> let hs = holes ps in
233 ps { holes = hs \\ [x] })
234 return (Bind n (GHole (mkTy (reverse env) t))
235 (mkApp (P Ref n ty) (map getP (reverse env))))
236 where
237 mkTy [] t = t
238 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
240 getP (n, b) = P Bound n (binderTy b)
242-- Hmmm. YAGNI?
243regret :: RunTactic
244regret = undefined
246exact :: Raw -> RunTactic
247exact guess ctxt env (Bind x (Hole ty) sc) =
248 do (val, valty) <- lift $ check ctxt env guess
249 lift $ converts ctxt env valty ty
250 return $ Bind x (Guess ty val) sc
251exact _ _ _ _ = fail "Can't fill here."
253-- As exact, but attempts to solve other goals by unification
255fill :: Raw -> RunTactic
256fill guess ctxt env (Bind x (Hole ty) sc) =
257 do (val, valty) <- lift $ check ctxt env guess
258 s <- get
259 ns <- lift $ unify ctxt env valty ty
260 ps <- get
261 let (uh, uns) = unified ps
262 put (ps { unified = (uh, uns ++ ns) })
263-- addLog (show (uh, uns ++ ns))
264 return $ Bind x (Guess ty val) sc
265fill _ _ _ _ = fail "Can't fill here."
267prep_fill :: Name -> [Name] -> RunTactic
268prep_fill f as ctxt env (Bind x (Hole ty) sc) =
269 do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
270 return $ Bind x (Guess ty val) sc
271prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
273complete_fill :: RunTactic
274complete_fill ctxt env (Bind x (Guess ty val) sc) =
275 do let guess = forget val
276 (val', valty) <- lift $ check ctxt env guess
277 ns <- lift $ unify ctxt env valty ty
278 ps <- get
279 let (uh, uns) = unified ps
280 put (ps { unified = (uh, uns ++ ns) })
281 return $ Bind x (Guess ty val) sc
282complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
284solve :: RunTactic
285solve ctxt env (Bind x (Guess ty val) sc)
286 | pureTerm val = do ps <- get
287 let (uh, uns) = unified ps
288 action (\ps -> ps { holes = holes ps \\ [x],
289 -- unified = (uh, uns ++ [(x, val)]),
290 instances = instances ps \\ [x] })
291 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
292 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val
293solve _ _ h = fail $ "Not a guess " ++ show h
295introTy :: Raw -> Maybe Name -> RunTactic
296introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
297 do let n = case mn of
298 Just name -> name
299 Nothing -> x
300 let t' = normalise ctxt env t
301 (tyv, tyt) <- lift $ check ctxt env ty
302-- ns <- lift $ unify ctxt env tyv t'
303 case t' of
304 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
305 do ns <- lift $ unify ctxt env s tyv
306 ps <- get
307 let (uh, uns) = unified ps
308 put (ps { unified = (uh, uns ++ ns) })
309 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
310 _ -> fail "Nothing to introduce"
311introTy ty n ctxt env _ = fail "Can't introduce here."
313intro :: Maybe Name -> RunTactic
314intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
315 do let n = case mn of
316 Just name -> name
317 Nothing -> x
318 let t' = normalise ctxt env t
319 case t' of
320 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
321 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
322 _ -> fail "Nothing to introduce"
323intro n ctxt env _ = fail "Can't introduce here."
325forall :: Name -> Raw -> RunTactic
326forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
327 do (tyv, tyt) <- lift $ check ctxt env ty
328 lift $ isSet ctxt env tyt
329 lift $ isSet ctxt env t
330 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
331forall n ty ctxt env _ = fail "Can't pi bind here"
333patvar :: Name -> RunTactic
334patvar n ctxt env (Bind x (Hole t) sc) =
335 do action (\ps -> ps { holes = holes ps \\ [x] })
336 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
337patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
339letbind :: Name -> Raw -> Raw -> RunTactic
340letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
341 do (tyv, tyt) <- lift $ check ctxt env ty
342 (valv, valt) <- lift $ check ctxt env val
343 lift $ isSet ctxt env tyt
344 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
345letbind n ty val ctxt env _ = fail "Can't let bind here"
347rewrite :: Raw -> RunTactic
348rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
349 do (tmv, tmt) <- lift $ check ctxt env tm
350 case unApply tmt of
351 (P _ (UN "=") _, [lt,rt,l,r]) ->
352 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
353 let newt = mkP l r l t
354 let sc = forget $ (Bind x (Hole newt)
355 (mkApp (P Ref (UN "replace") (Set (UVal 0)))
356 [lt, l, r, p, tmv, xp]))
357 (scv, sct) <- lift $ check ctxt env sc
358 return scv
359 _ -> fail "Not an equality type"
360 where
361 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
362 -- and x, and put \x : lt in front
363 mkP lt l r ty | l == ty = lt
364 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
365 a' = if (r /= a) then mkP lt l r a else a in
366 App f' a'
367 mkP lt l r x = x
369 rname = MN 0 "replaced"
370rewrite _ _ _ _ = fail "Can't rewrite here"
372patbind :: Name -> RunTactic
373patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
374 do let t' = normalise ctxt env t
375 case t' of
376 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
377 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
378 _ -> fail "Nothing to pattern bind"
379patbind n ctxt env _ = fail "Can't pattern bind here"
381compute :: RunTactic
382compute ctxt env (Bind x (Hole ty) sc) =
383 do return $ Bind x (Hole (normalise ctxt env ty)) sc
385check_in :: Raw -> RunTactic
386check_in t ctxt env tm =
387 do (val, valty) <- lift $ check ctxt env t
388 addLog (showEnv env val ++ " : " ++ showEnv env valty)
389 return tm
391eval_in :: Raw -> RunTactic
392eval_in t ctxt env tm =
393 do (val, valty) <- lift $ check ctxt env t
394 let val' = normalise ctxt env val
395 let valty' = normalise ctxt env valty
396 addLog (showEnv env val ++ " : " ++
397 showEnv env valty ++
398-- " in " ++ show env ++
399 " ==>\n " ++
400 showEnv env val' ++ " : " ++
401 showEnv env valty')
402 return tm
404start_unify :: Name -> RunTactic
405start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
406 return tm
408solve_unified :: RunTactic
409solve_unified ctxt env tm =
410 do ps <- get
411 let (_, ns) = unified ps
412 action (\ps -> ps { holes = holes ps \\ map fst ns })
413 action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
414 return (updateSolved ns tm)
416updateSolved xs (Bind n (Hole ty) t)
417 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
418updateSolved xs (Bind n b t)
419 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
420updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
421updateSolved xs (P _ n _)
422 | Just v <- lookup n xs = v
423updateSolved xs t = t
425processTactic :: Tactic -> ProofState -> TC (ProofState, String)
426processTactic QED ps = case holes ps of
427 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
428 (tm', ty', _) <- recheck (context ps) [] tm
429 return (ps { done = True, pterm = tm' },
430 "Proof complete: " ++ showEnv [] tm')
431 _ -> fail "Still holes to fill."
432processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
433processTactic Undo ps = case previous ps of
434 Nothing -> fail "Nothing to undo."
435 Just pold -> return (pold, "")
436processTactic EndUnify ps = let (h, ns) = unified ps
437 tm' = updateSolved ns (pterm ps) in
438 return (ps { pterm = tm',
439 unified = (h, []),
440 holes = holes ps \\ map fst ns }, "")
441processTactic (Reorder n) ps
442 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
443 return (ps' { previous = Just ps, plog = "" }, plog ps')
444processTactic t ps
445 = case holes ps of
446 [] -> fail "Nothing to fill in."
447 (h:_) -> do ps' <- execStateT (process t h) ps
448 return (ps' { previous = Just ps, plog = "" }, plog ps')
450process :: Tactic -> Name -> StateT TState TC ()
451process EndUnify _
452 = do ps <- get
453 let (h, _) = unified ps
454 tactic (Just h) solve_unified
455process t h = tactic (Just h) (mktac t)
456 where mktac Attack = attack
457 mktac (Claim n r) = claim n r
458 mktac (Exact r) = exact r
459 mktac (Fill r) = fill r
460 mktac (PrepFill n ns) = prep_fill n ns
461 mktac CompleteFill = complete_fill
462 mktac Regret = regret
463 mktac Solve = solve
464 mktac (StartUnify n) = start_unify n
465 mktac Compute = compute
466 mktac (Intro n) = intro n
467 mktac (IntroTy ty n) = introTy ty n
468 mktac (Forall n t) = forall n t
469 mktac (LetBind n t v) = letbind n t v
470 mktac (Rewrite t) = rewrite t
471 mktac (PatVar n) = patvar n
472 mktac (PatBind n) = patbind n
473 mktac (CheckIn r) = check_in r
474 mktac (EvalIn r) = eval_in r
475 mktac (Focus n) = focus n
476 mktac (Defer n) = defer n
477 mktac (Instance n) = instanceArg n
478 mktac (MoveLast n) = movelast n