git.iko.soy/Idris-dev
on 7b1336b help sign in
Idris-dev/src/Core/ProofState.hs
426 lines 17 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 previous :: Maybe ProofState, -- for undo
28 context :: Context,
29 plog :: String,
30 done :: Bool
31 }
33data Goal = GD { premises :: Env,
34 goalType :: Binder Term
35 }
37data Tactic = Attack
38 | Claim Name Raw
39 | Exact Raw
40 | Fill Raw
41 | PrepFill Name [Name]
42 | CompleteFill
43 | Regret
44 | Solve
45 | StartUnify Name
46 | EndUnify
47 | Compute
48 | EvalIn Raw
49 | CheckIn Raw
50 | Intro Name
51 | Forall Name Raw
52 | LetBind Name Raw Raw
53 | Rewrite Raw
54 | PatVar Name
55 | PatBind Name
56 | Focus Name
57 | Defer Name
58 | MoveLast Name
59 | ProofState
60 | Undo
61 | QED
62 deriving Show
64-- Some utilites on proof and tactic states
66instance Show ProofState where
67 show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
68 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
69 = let OK g = goal (Just h) tm
70 wkenv = premises g in
71 "Other goals: " ++ show hs ++ "\n" ++
72 showPs wkenv (reverse wkenv) ++ "\n" ++
73 "-------------------------------- (" ++ show nm ++
74 ") -------\n " ++
75 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
76 where showPs env [] = ""
77 showPs env ((n, Let t v):bs)
78 = " " ++ show n ++ " : " ++
79 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
80 showEnv env ({- normalise ctxt env -} v) ++
81 "\n" ++ showPs env bs
82 showPs env ((n, b):bs)
83 = " " ++ show n ++ " : " ++
84 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
85 "\n" ++ showPs env bs
86 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
87 " =?= " ++ showEnv ps v
88 showG ps b = showEnv ps (binderTy b)
90same Nothing n = True
91same (Just x) n = x == n
93hole (Hole _) = True
94hole (Guess _ _) = True
95hole _ = False
97holeName i = MN i "hole"
99getName :: Monad m => String -> StateT TState m Name
100getName tag = do ps <- get
101 let n = nextname ps
102 put (ps { nextname = n+1 })
103 return $ MN n tag
105action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
106action a = do ps <- get
107 put (a ps)
109addLog :: Monad m => String -> StateT TState m ()
110addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
112newProof :: Name -> Context -> Type -> ProofState
113newProof n ctxt ty = let h = holeName 0
114 ty' = vToP ty in
115 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
116 Nothing ctxt "" False
118type TState = ProofState -- [TacticAction])
119type RunTactic = Context -> Env -> Term -> StateT TState TC Term
120type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
122envAtFocus :: ProofState -> TC Env
123envAtFocus ps
124 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
125 return (premises g)
126 | otherwise = fail "No holes"
128goalAtFocus :: ProofState -> TC (Binder Type)
129goalAtFocus ps
130 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
131 return (goalType g)
133goal :: Hole -> Term -> TC Goal
134goal h tm = g [] tm where
135 g env (Bind n b sc) | hole b && same h n = return $ GD env b
136 | otherwise
137 = gb env b `mplus` g ((n, b):env) sc
138 g env (App f a) = g env f `mplus` g env a
139 g env t = fail "Can't find hole"
141 gb env (Let t v) = g env t `mplus` g env v
142 gb env (Guess t v) = g env t `mplus` g env v
143 gb env t = g env (binderTy t)
145tactic :: Hole -> RunTactic -> StateT TState TC ()
146tactic h f = do ps <- get
147 tm' <- atH (context ps) [] (pterm ps)
148 ps <- get -- might have changed while processing
149 put (ps { pterm = tm' })
150 where
151 atH c env binder@(Bind n b sc)
152 | hole b && same h n = f c env binder
153 | otherwise
154 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
155 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
156 atH c env t = return t
158 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
159 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
160 atHb c env t = do ty' <- atH c env (binderTy t)
161 return $ t { binderTy = ty' }
163attack :: RunTactic
164attack ctxt env (Bind x (Hole t) sc)
165 = do h <- getName "hole"
166 action (\ps -> ps { holes = h : holes ps })
167 return $ Bind x (Guess t (newtm h)) sc
168 where
169 newtm h = Bind h (Hole t) (P Bound h t)
170attack ctxt env _ = fail "Not an attackable hole"
172claim :: Name -> Raw -> RunTactic
173claim n ty ctxt env t =
174 do (tyv, tyt) <- lift $ check ctxt env ty
175 lift $ isSet ctxt env tyt
176 action (\ps -> let (g:gs) = holes ps in
177 ps { holes = g : n : gs } )
178 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
180focus :: Name -> RunTactic
181focus n ctxt env t = do action (\ps -> let hs = holes ps in
182 if n `elem` hs
183 then ps { holes = n : (hs \\ [n]) }
184 else ps)
185 return t
187movelast :: Name -> RunTactic
188movelast n ctxt env t = do action (\ps -> let hs = holes ps in
189 if n `elem` hs
190 then ps { holes = (hs \\ [n]) ++ [n] }
191 else ps)
192 return t
194defer :: Name -> RunTactic
195defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
196 do action (\ps -> let hs = holes ps in
197 ps { holes = hs \\ [x] })
198 return (Bind n (GHole (mkTy (reverse env) t))
199 (mkApp (P Ref n ty) (map getP (reverse env))))
200 where
201 mkTy [] t = t
202 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
204 getP (n, b) = P Bound n (binderTy b)
206-- Hmmm. YAGNI?
207regret :: RunTactic
208regret = undefined
210exact :: Raw -> RunTactic
211exact guess ctxt env (Bind x (Hole ty) sc) =
212 do (val, valty) <- lift $ check ctxt env guess
213 lift $ converts ctxt env valty ty
214 return $ Bind x (Guess ty val) sc
215exact _ _ _ _ = fail "Can't fill here."
217-- As exact, but attempts to solve other goals by unification
219fill :: Raw -> RunTactic
220fill guess ctxt env (Bind x (Hole ty) sc) =
221 do (val, valty) <- lift $ check ctxt env guess
222 ns <- lift $ unify ctxt env valty ty
223 ps <- get
224 let (uh, uns) = unified ps
225 put (ps { unified = (uh, uns ++ ns) })
226-- addLog (show (uh, uns ++ ns))
227 return $ Bind x (Guess ty val) sc
228fill _ _ _ _ = fail "Can't fill here."
230prep_fill :: Name -> [Name] -> RunTactic
231prep_fill f as ctxt env (Bind x (Hole ty) sc) =
232 do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
233 return $ Bind x (Guess ty val) sc
234prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
236complete_fill :: RunTactic
237complete_fill ctxt env (Bind x (Guess ty val) sc) =
238 do let guess = forget val
239 (val', valty) <- lift $ check ctxt env guess
240 ns <- lift $ unify ctxt env valty ty
241 ps <- get
242 let (uh, uns) = unified ps
243 put (ps { unified = (uh, uns ++ ns) })
244 return $ Bind x (Guess ty val) sc
245complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
247solve :: RunTactic
248solve ctxt env (Bind x (Guess ty val) sc)
249 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
250 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
251 | otherwise = fail "I see a hole in your solution."
252solve _ _ h = fail $ "Not a guess " ++ show h
254intro :: Name -> RunTactic
255intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
256 do let t' = normalise ctxt env t
257 case t' of
258 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
259 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
260 _ -> fail "Nothing to introduce"
261intro n ctxt env _ = fail "Can't introduce here."
263forall :: Name -> Raw -> RunTactic
264forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
265 do (tyv, tyt) <- lift $ check ctxt env ty
266 lift $ isSet ctxt env tyt
267 lift $ isSet ctxt env t
268 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
269forall n ty ctxt env _ = fail "Can't pi bind here"
271patvar :: Name -> RunTactic
272patvar n ctxt env (Bind x (Hole t) sc) =
273 do action (\ps -> ps { holes = holes ps \\ [x] })
274 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
276letbind :: Name -> Raw -> Raw -> RunTactic
277letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
278 do (tyv, tyt) <- lift $ check ctxt env ty
279 (valv, valt) <- lift $ check ctxt env val
280 lift $ isSet ctxt env tyt
281 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
282letbind n ty val ctxt env _ = fail "Can't let bind here"
284rewrite :: Raw -> RunTactic
285rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
286 do (tmv, tmt) <- lift $ check ctxt env tm
287 case unApply tmt of
288 (P _ (UN ["="]) _, [lt,rt,l,r]) ->
289 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
290 let newt = mkP l r l t
291 let sc = forget $ (Bind x (Hole newt)
292 (mkApp (P Ref (UN ["replace"]) (Set 0))
293 [lt, l, r, p, tmv, xp]))
294 (scv, sct) <- lift $ check ctxt env sc
295 return scv
296 _ -> fail "Not an equality type"
297 where
298 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
299 -- and x, and put \x : lt in front
300 mkP lt l r ty | l == ty = lt
301 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
302 a' = if (r /= a) then mkP lt l r a else a in
303 App f' a'
304 mkP lt l r x = x
306 rname = MN 0 "replaced"
307rewrite _ _ _ _ = fail "Can't rewrite here"
309patbind :: Name -> RunTactic
310patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
311 do let t' = normalise ctxt env t
312 case t' of
313 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
314 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
315 _ -> fail "Nothing to pattern bind"
316patbind n ctxt env _ = fail "Can't pattern bind here"
318compute :: RunTactic
319compute ctxt env (Bind x (Hole ty) sc) =
320 do return $ Bind x (Hole (normalise ctxt env ty)) sc
322check_in :: Raw -> RunTactic
323check_in t ctxt env tm =
324 do (val, valty) <- lift $ check ctxt env t
325 addLog (showEnv env val ++ " : " ++ showEnv env valty)
326 return tm
328eval_in :: Raw -> RunTactic
329eval_in t ctxt env tm =
330 do (val, valty) <- lift $ check ctxt env t
331 let val' = normalise ctxt env val
332 let valty' = normalise ctxt env valty
333 addLog (showEnv env val ++ " : " ++
334 showEnv env valty ++
335-- " in " ++ show env ++
336 " ==>\n " ++
337 showEnv env val' ++ " : " ++
338 showEnv env valty')
339 return tm
341start_unify :: Name -> RunTactic
342start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
343 return tm
345solve_unified :: RunTactic
346solve_unified ctxt env tm =
347 do ps <- get
348 let (_, ns) = unified ps
349 action (\ps -> ps { holes = holes ps \\ map fst ns })
350-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
351 return (updateSolved ns tm)
352 where
353 updateSolved xs (Bind n (Hole ty) t)
354 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
355 updateSolved xs (Bind n b t)
356 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
357 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
358 updateSolved xs (P _ n _)
359 | Just v <- lookup n xs = v
360 updateSolved xs t = t
362-- shuffleHoles :: Term -> Term
363-- shuffleHoles tm = shuffle [] tm
364-- where
365-- shuffle ns (Bind n b sc)
366-- |
368processTactic :: Tactic -> ProofState -> TC (ProofState, String)
369processTactic QED ps = case holes ps of
370 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
371 (tm', ty') <- recheck (context ps) [] tm
372 return (ps { done = True, pterm = tm' },
373 "Proof complete: " ++ showEnv [] tm')
374 _ -> fail "Still holes to fill."
375processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
376processTactic Undo ps = case previous ps of
377 Nothing -> fail "Nothing to undo."
378 Just pold -> return (pold, "")
379processTactic EndUnify ps = let (h, ns) = unified ps
380 tm' = updateSolved ns (pterm ps) in
381 return (ps { pterm = tm',
382 unified = (h, []),
383 holes = holes ps \\ map fst ns }, "")
384 where
385 updateSolved xs (Bind n (Hole ty) t)
386 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
387 updateSolved xs (Bind n b t)
388 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
389 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
390 updateSolved xs (P _ n _)
391 | Just v <- lookup n xs = v
392 updateSolved xs t = t
393processTactic t ps
394 = case holes ps of
395 [] -> fail "Nothing to fill in."
396 (h:_) -> do let n = nextname ps
397 ps' <- execStateT (process t h) ps
398 return (ps' { previous = Just ps, plog = "" }, plog ps')
400process :: Tactic -> Name -> StateT TState TC ()
401process EndUnify _
402 = do ps <- get
403 let (h, _) = unified ps
404 tactic (Just h) solve_unified
405process t h = tactic (Just h) (mktac t)
406 where mktac Attack = attack
407 mktac (Claim n r) = claim n r
408 mktac (Exact r) = exact r
409 mktac (Fill r) = fill r
410 mktac (PrepFill n ns) = prep_fill n ns
411 mktac CompleteFill = complete_fill
412 mktac Regret = regret
413 mktac Solve = solve
414 mktac (StartUnify n) = start_unify n
415 mktac Compute = compute
416 mktac (Intro n) = intro n
417 mktac (Forall n t) = forall n t
418 mktac (LetBind n t v) = letbind n t v
419 mktac (Rewrite t) = rewrite t
420 mktac (PatVar n) = patvar n
421 mktac (PatBind n) = patbind n
422 mktac (CheckIn r) = check_in r
423 mktac (EvalIn r) = eval_in r
424 mktac (Focus n) = focus n
425 mktac (MoveLast n) = movelast n
426 mktac (Defer n) = defer n