git.iko.soy/Idris-dev
on 2c4ff83 help sign in
Idris-dev/src/Core/ProofState.hs
388 lines 15 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(..), 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 | PatVar Name
53 | PatBind Name
54 | Focus Name
55 | Defer Name
56 | MoveLast Name
57 | ProofState
58 | Undo
59 | QED
60 deriving Show
62-- Some utilites on proof and tactic states
64instance Show ProofState where
65 show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
66 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
67 = let OK g = goal (Just h) tm
68 wkenv = premises g in
69 "Other goals: " ++ show hs ++ "\n" ++
70 showPs wkenv (reverse wkenv) ++ "\n" ++
71 "-------------------------------- (" ++ show nm ++
72 ") -------\n " ++
73 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
74 where showPs env [] = ""
75 showPs env ((n, Let t v):bs)
76 = " " ++ show n ++ " : " ++
77 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
78 showEnv env ({- normalise ctxt env -} v) ++
79 "\n" ++ showPs env bs
80 showPs env ((n, b):bs)
81 = " " ++ show n ++ " : " ++
82 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
83 "\n" ++ showPs env bs
84 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
85 " =?= " ++ showEnv ps v
86 showG ps b = showEnv ps (binderTy b)
88same Nothing n = True
89same (Just x) n = x == n
91hole (Hole _) = True
92hole (Guess _ _) = True
93hole _ = False
95holeName i = MN i "hole"
97getName :: Monad m => String -> StateT TState m Name
98getName tag = do ps <- get
99 let n = nextname ps
100 put (ps { nextname = n+1 })
101 return $ MN n tag
103action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
104action a = do ps <- get
105 put (a ps)
107addLog :: Monad m => String -> StateT TState m ()
108addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
110newProof :: Name -> Context -> Type -> ProofState
111newProof n ctxt ty = let h = holeName 0
112 ty' = vToP ty in
113 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
114 Nothing ctxt "" False
116type TState = ProofState -- [TacticAction])
117type RunTactic = Context -> Env -> Term -> StateT TState TC Term
118type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
120envAtFocus :: ProofState -> TC Env
121envAtFocus ps
122 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
123 return (premises g)
124 | otherwise = fail "No holes"
126goalAtFocus :: ProofState -> TC Type
127goalAtFocus ps
128 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
129 return (binderTy (goalType g))
131goal :: Hole -> Term -> TC Goal
132goal h tm = g [] tm where
133 g env (Bind n b sc) | hole b && same h n = return $ GD env b
134 | otherwise
135 = gb env b `mplus` g ((n, b):env) sc
136 g env (App f a) = g env f `mplus` g env a
137 g env t = fail "Can't find hole"
139 gb env (Let t v) = g env t `mplus` g env v
140 gb env (Guess t v) = g env t `mplus` g env v
141 gb env t = g env (binderTy t)
142tactic :: Hole -> RunTactic -> StateT TState TC ()
143tactic h f = do ps <- get
144 tm' <- atH (context ps) [] (pterm ps)
145 ps <- get -- might have changed while processing
146 put (ps { pterm = tm' })
147 where
148 atH c env binder@(Bind n b sc)
149 | hole b && same h n = f c env binder
150 | otherwise
151 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
152 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
153 atH c env t = return t
155 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
156 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
157 atHb c env t = do ty' <- atH c env (binderTy t)
158 return $ t { binderTy = ty' }
160attack :: RunTactic
161attack ctxt env (Bind x (Hole t) sc)
162 = do h <- getName "hole"
163 action (\ps -> ps { holes = h : holes ps })
164 return $ Bind x (Guess t (newtm h)) sc
165 where
166 newtm h = Bind h (Hole t) (P Bound h t)
167attack ctxt env _ = fail "Not an attackable hole"
169claim :: Name -> Raw -> RunTactic
170claim n ty ctxt env t =
171 do (tyv, tyt) <- lift $ check ctxt env ty
172 lift $ isSet ctxt env tyt
173 action (\ps -> let (g:gs) = holes ps in
174 ps { holes = g : n : gs } )
175 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
177focus :: Name -> RunTactic
178focus n ctxt env t = do action (\ps -> let hs = holes ps in
179 if n `elem` hs
180 then ps { holes = n : (hs \\ [n]) }
181 else ps)
182 return t
184movelast :: Name -> RunTactic
185movelast n ctxt env t = do action (\ps -> let hs = holes ps in
186 if n `elem` hs
187 then ps { holes = (hs \\ [n]) ++ [n] }
188 else ps)
189 return t
191defer :: Name -> RunTactic
192defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
193 do action (\ps -> let hs = holes ps in
194 ps { holes = hs \\ [x] })
195 return (Bind n (GHole (mkTy (reverse env) t))
196 (mkApp (P nt n ty) (map getP (reverse env))))
197 where
198 mkTy [] t = t
199 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
201 getP (n, b) = P Bound n (binderTy b)
203-- Hmmm. YAGNI?
204regret :: RunTactic
205regret = undefined
207exact :: Raw -> RunTactic
208exact guess ctxt env (Bind x (Hole ty) sc) =
209 do (val, valty) <- lift $ check ctxt env guess
210 lift $ converts ctxt env valty ty
211 return $ Bind x (Guess ty val) sc
212exact _ _ _ _ = fail "Can't fill here."
214-- As exact, but attempts to solve other goals by unification
216fill :: Raw -> RunTactic
217fill guess ctxt env (Bind x (Hole ty) sc) =
218 do (val, valty) <- lift $ check ctxt env guess
219 ns <- lift $ unify ctxt env valty ty
220 ps <- get
221 let (uh, uns) = unified ps
222 put (ps { unified = (uh, uns ++ ns) })
223-- addLog (show (uh, uns ++ ns))
224 return $ Bind x (Guess ty val) sc
225fill _ _ _ _ = fail "Can't fill here."
227prep_fill :: Name -> [Name] -> RunTactic
228prep_fill f as ctxt env (Bind x (Hole ty) sc) =
229 do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
230 return $ Bind x (Guess ty val) sc
231prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
233complete_fill :: RunTactic
234complete_fill ctxt env (Bind x (Guess ty val) sc) =
235 do let guess = forget val
236 (val', valty) <- lift $ check ctxt env guess
237 ns <- lift $ unify ctxt env valty ty
238 ps <- get
239 let (uh, uns) = unified ps
240 put (ps { unified = (uh, uns ++ ns) })
241 return $ Bind x (Guess ty val) sc
242complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
244solve :: RunTactic
245solve ctxt env (Bind x (Guess ty val) sc)
246 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
247 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
248 | otherwise = fail "I see a hole in your solution."
249solve _ _ h = fail $ "Not a guess " ++ show h
251intro :: Name -> RunTactic
252intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
253 do let t' = normalise ctxt env t
254 case t' of
255 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
256 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
257 _ -> fail "Nothing to introduce"
258intro n ctxt env _ = fail "Can't introduce here."
260forall :: Name -> Raw -> RunTactic
261forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
262 do (tyv, tyt) <- lift $ check ctxt env ty
263 lift $ isSet ctxt env tyt
264 lift $ isSet ctxt env t
265 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
266forall n ty ctxt env _ = fail "Can't pi bind here"
268patvar :: Name -> RunTactic
269patvar n ctxt env (Bind x (Hole t) sc) =
270 do action (\ps -> ps { holes = holes ps \\ [x] })
271 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
273patbind :: Name -> RunTactic
274patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
275 do let t' = normalise ctxt env t
276 case t' of
277 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
278 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
279 _ -> fail "Nothing to pattern bind"
280patbind n ctxt env _ = fail "Can't pattern bind here"
282compute :: RunTactic
283compute ctxt env (Bind x (Hole ty) sc) =
284 do return $ Bind x (Hole (normalise ctxt env ty)) sc
286check_in :: Raw -> RunTactic
287check_in t ctxt env tm =
288 do (val, valty) <- lift $ check ctxt env t
289 addLog (showEnv env val ++ " : " ++ showEnv env valty)
290 return tm
292eval_in :: Raw -> RunTactic
293eval_in t ctxt env tm =
294 do (val, valty) <- lift $ check ctxt env t
295 let val' = normalise ctxt env val
296 let valty' = normalise ctxt env valty
297 addLog (showEnv env val ++ " : " ++
298 showEnv env valty ++
299-- " in " ++ show env ++
300 " ==>\n " ++
301 showEnv env val' ++ " : " ++
302 showEnv env valty')
303 return tm
305start_unify :: Name -> RunTactic
306start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
307 return tm
309solve_unified :: RunTactic
310solve_unified ctxt env tm =
311 do ps <- get
312 let (_, ns) = unified ps
313 action (\ps -> ps { holes = holes ps \\ map fst ns })
314-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
315 return (updateSolved ns tm)
316 where
317 updateSolved xs (Bind n (Hole ty) t)
318 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
319 updateSolved xs (Bind n b t)
320 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
321 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
322 updateSolved xs (P _ n _)
323 | Just v <- lookup n xs = v
324 updateSolved xs t = t
326-- shuffleHoles :: Term -> Term
327-- shuffleHoles tm = shuffle [] tm
328-- where
329-- shuffle ns (Bind n b sc)
330-- |
332processTactic :: Tactic -> ProofState -> TC (ProofState, String)
333processTactic QED ps = case holes ps of
334 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
335 (tm', ty') <- recheck (context ps) [] tm
336 return (ps { done = True, pterm = tm' },
337 "Proof complete: " ++ showEnv [] tm')
338 _ -> fail "Still holes to fill."
339processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
340processTactic Undo ps = case previous ps of
341 Nothing -> fail "Nothing to undo."
342 Just pold -> return (pold, "")
343processTactic EndUnify ps = let (h, ns) = unified ps
344 tm' = updateSolved ns (pterm ps) in
345 return (ps { pterm = tm',
346 unified = (h, []),
347 holes = holes ps \\ map fst ns }, "")
348 where
349 updateSolved xs (Bind n (Hole ty) t)
350 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
351 updateSolved xs (Bind n b t)
352 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
353 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
354 updateSolved xs (P _ n _)
355 | Just v <- lookup n xs = v
356 updateSolved xs t = t
357processTactic t ps
358 = case holes ps of
359 [] -> fail "Nothing to fill in."
360 (h:_) -> do let n = nextname ps
361 ps' <- execStateT (process t h) ps
362 return (ps' { previous = Just ps, plog = "" }, plog ps')
364process :: Tactic -> Name -> StateT TState TC ()
365process EndUnify _
366 = do ps <- get
367 let (h, _) = unified ps
368 tactic (Just h) solve_unified
369process t h = tactic (Just h) (mktac t)
370 where mktac Attack = attack
371 mktac (Claim n r) = claim n r
372 mktac (Exact r) = exact r
373 mktac (Fill r) = fill r
374 mktac (PrepFill n ns) = prep_fill n ns
375 mktac CompleteFill = complete_fill
376 mktac Regret = regret
377 mktac Solve = solve
378 mktac (StartUnify n) = start_unify n
379 mktac Compute = compute
380 mktac (Intro n) = intro n
381 mktac (Forall n t) = forall n t
382 mktac (PatVar n) = patvar n
383 mktac (PatBind n) = patbind n
384 mktac (CheckIn r) = check_in r
385 mktac (EvalIn r) = eval_in r
386 mktac (Focus n) = focus n
387 mktac (MoveLast n) = movelast n
388 mktac (Defer n) = defer n