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