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