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