git.iko.soy/Idris-dev
on e613365 help sign in
Idris-dev/src/Core/ProofState.hs
375 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 defer :: [(Name, Type)], -- 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 | MoveLast Name
56 | ProofState
57 | Undo
58 | QED
59 deriving Show
61-- Some utilites on proof and tactic states
63instance Show ProofState where
64 show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
65 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
66 = let OK g = goal (Just h) tm
67 wkenv = premises g in
68 "Other goals: " ++ show hs ++ "\n" ++
69 showPs wkenv (reverse wkenv) ++ "\n" ++
70 "-------------------------------- (" ++ show nm ++
71 ") -------\n " ++
72 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
73 where showPs env [] = ""
74 showPs env ((n, Let t v):bs)
75 = " " ++ show n ++ " : " ++
76 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
77 showEnv env ({- normalise ctxt env -} v) ++
78 "\n" ++ showPs env bs
79 showPs env ((n, b):bs)
80 = " " ++ show n ++ " : " ++
81 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
82 "\n" ++ showPs env bs
83 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
84 " =?= " ++ showEnv ps v
85 showG ps b = showEnv ps (binderTy b)
87same Nothing n = True
88same (Just x) n = x == n
90hole (Hole _) = True
91hole (Guess _ _) = True
92hole _ = False
94holeName i = MN i "hole"
96getName :: Monad m => String -> StateT TState m Name
97getName tag = do ps <- get
98 let n = nextname ps
99 put (ps { nextname = n+1 })
100 return $ MN n tag
102action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
103action a = do ps <- get
104 put (a ps)
106addLog :: Monad m => String -> StateT TState m ()
107addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
109newProof :: Name -> Context -> Type -> ProofState
110newProof n ctxt ty = let h = holeName 0
111 ty' = vToP ty in
112 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
113 Nothing ctxt "" False
115type TState = ProofState -- [TacticAction])
116type RunTactic = Context -> Env -> Term -> StateT TState TC Term
117type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
119envAtFocus :: ProofState -> TC Env
120envAtFocus ps
121 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
122 return (premises g)
123 | otherwise = fail "No holes"
125goalAtFocus :: ProofState -> TC Type
126goalAtFocus ps
127 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
128 return (binderTy (goalType g))
130goal :: Hole -> Term -> TC Goal
131goal h tm = g [] tm where
132 g env (Bind n b sc) | hole b && same h n = return $ GD env b
133 | otherwise
134 = gb env b `mplus` g ((n, b):env) sc
135 g env (App f a) = g env f `mplus` g env a
136 g env t = Error "Can't find hole"
138 gb env (Let t v) = g env t `mplus` g env v
139 gb env (Guess t v) = g env t `mplus` g env v
140 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
191-- Hmmm. YAGNI?
192regret :: RunTactic
193regret = undefined
195exact :: Raw -> RunTactic
196exact guess ctxt env (Bind x (Hole ty) sc) =
197 do (val, valty) <- lift $ check ctxt env guess
198 lift $ converts ctxt env valty ty
199 return $ Bind x (Guess ty val) sc
200exact _ _ _ _ = fail "Can't fill here."
202-- As exact, but attempts to solve other goals by unification
204fill :: Raw -> RunTactic
205fill guess ctxt env (Bind x (Hole ty) sc) =
206 do (val, valty) <- lift $ check ctxt env guess
207 ns <- lift $ unify ctxt env valty ty
208 ps <- get
209 let (uh, uns) = unified ps
210 put (ps { unified = (uh, uns ++ ns) })
211-- addLog (show (uh, uns ++ ns))
212 return $ Bind x (Guess ty val) sc
213fill _ _ _ _ = fail "Can't fill here."
215prep_fill :: Name -> [Name] -> RunTactic
216prep_fill f as ctxt env (Bind x (Hole ty) sc) =
217 do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
218 return $ Bind x (Guess ty val) sc
219prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
221complete_fill :: RunTactic
222complete_fill ctxt env (Bind x (Guess ty val) sc) =
223 do let guess = forget val
224 (val', valty) <- lift $ check ctxt env guess
225 ns <- lift $ unify ctxt env valty ty
226 ps <- get
227 let (uh, uns) = unified ps
228 put (ps { unified = (uh, uns ++ ns) })
229 return $ Bind x (Guess ty val) sc
230complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
232solve :: RunTactic
233solve ctxt env (Bind x (Guess ty val) sc)
234 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
235 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
236 | otherwise = fail "I see a hole in your solution."
237solve _ _ h = fail $ "Not a guess " ++ show h
239intro :: Name -> RunTactic
240intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
241 do let t' = normalise ctxt env t
242 case t' of
243 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
244 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
245 _ -> fail "Nothing to introduce"
246intro n ctxt env _ = fail "Can't introduce here."
248forall :: Name -> Raw -> RunTactic
249forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
250 do (tyv, tyt) <- lift $ check ctxt env ty
251 lift $ isSet ctxt env tyt
252 lift $ isSet ctxt env t
253 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
254forall n ty ctxt env _ = fail "Can't pi bind here"
256patvar :: Name -> RunTactic
257patvar n ctxt env (Bind x (Hole t) sc) =
258 do action (\ps -> ps { holes = holes ps \\ [x] })
259 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
261patbind :: Name -> RunTactic
262patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
263 do let t' = normalise ctxt env t
264 case t' of
265 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
266 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
267 _ -> fail "Nothing to pattern bind"
268patbind n ctxt env _ = fail "Can't pattern bind here"
270compute :: RunTactic
271compute ctxt env (Bind x (Hole ty) sc) =
272 do return $ Bind x (Hole (normalise ctxt env ty)) sc
274check_in :: Raw -> RunTactic
275check_in t ctxt env tm =
276 do (val, valty) <- lift $ check ctxt env t
277 addLog (showEnv env val ++ " : " ++ showEnv env valty)
278 return tm
280eval_in :: Raw -> RunTactic
281eval_in t ctxt env tm =
282 do (val, valty) <- lift $ check ctxt env t
283 let val' = normalise ctxt env val
284 let valty' = normalise ctxt env valty
285 addLog (showEnv env val ++ " : " ++
286 showEnv env valty ++
287-- " in " ++ show env ++
288 " ==>\n " ++
289 showEnv env val' ++ " : " ++
290 showEnv env valty')
291 return tm
293start_unify :: Name -> RunTactic
294start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
295 return tm
297solve_unified :: RunTactic
298solve_unified ctxt env tm =
299 do ps <- get
300 let (_, ns) = unified ps
301 action (\ps -> ps { holes = holes ps \\ map fst ns })
302-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
303 return (updateSolved ns tm)
304 where
305 updateSolved xs (Bind n (Hole ty) t)
306 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
307 updateSolved xs (Bind n b t)
308 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
309 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
310 updateSolved xs (P _ n _)
311 | Just v <- lookup n xs = v
312 updateSolved xs t = t
314-- shuffleHoles :: Term -> Term
315-- shuffleHoles tm = shuffle [] tm
316-- where
317-- shuffle ns (Bind n b sc)
318-- |
320processTactic :: Tactic -> ProofState -> TC (ProofState, String)
321processTactic QED ps = case holes ps of
322 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
323 (tm', ty') <- recheck (context ps) [] tm
324 return (ps { done = True, pterm = tm' },
325 "Proof complete: " ++ showEnv [] tm')
326 _ -> Error "Still holes to fill."
327processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
328processTactic Undo ps = case previous ps of
329 Nothing -> Error "Nothing to undo."
330 Just pold -> return (pold, "")
331processTactic EndUnify ps = let (h, ns) = unified ps
332 tm' = updateSolved ns (pterm ps) in
333 return (ps { pterm = tm',
334 unified = (h, []),
335 holes = holes ps \\ map fst ns }, "")
336 where
337 updateSolved xs (Bind n (Hole ty) t)
338 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
339 updateSolved xs (Bind n b t)
340 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
341 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
342 updateSolved xs (P _ n _)
343 | Just v <- lookup n xs = v
344 updateSolved xs t = t
345processTactic t ps
346 = case holes ps of
347 [] -> Error "Nothing to fill in."
348 (h:_) -> do let n = nextname ps
349 ps' <- execStateT (process t h) ps
350 return (ps' { previous = Just ps, plog = "" }, plog ps')
352process :: Tactic -> Name -> StateT TState TC ()
353process EndUnify _
354 = do ps <- get
355 let (h, _) = unified ps
356 tactic (Just h) solve_unified
357process t h = tactic (Just h) (mktac t)
358 where mktac Attack = attack
359 mktac (Claim n r) = claim n r
360 mktac (Exact r) = exact r
361 mktac (Fill r) = fill r
362 mktac (PrepFill n ns) = prep_fill n ns
363 mktac CompleteFill = complete_fill
364 mktac Regret = regret
365 mktac Solve = solve
366 mktac (StartUnify n) = start_unify n
367 mktac Compute = compute
368 mktac (Intro n) = intro n
369 mktac (Forall n t) = forall n t
370 mktac (PatVar n) = patvar n
371 mktac (PatBind n) = patbind n
372 mktac (CheckIn r) = check_in r
373 mktac (EvalIn r) = eval_in r
374 mktac (Focus n) = focus n
375 mktac (MoveLast n) = movelast n