git.iko.soy/Idris-dev
on be2b9bc help sign in
Idris-dev/src/Core/ProofState.hs
342 lines 13 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 | Regret
42 | Solve
43 | StartUnify Name
44 | EndUnify
45 | Compute
46 | EvalIn Raw
47 | CheckIn Raw
48 | Intro Name
49 | Forall Name Raw
50 | PatVar Name
51 | Focus Name
52 | MoveLast Name
53 | ProofState
54 | Undo
55 | QED
56 deriving Show
58-- Some utilites on proof and tactic states
60instance Show ProofState where
61 show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
62 show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
63 = let OK g = goal (Just h) tm
64 wkenv = premises g in
65 "Other goals: " ++ show hs ++ "\n" ++
66 showPs wkenv (reverse wkenv) ++ "\n" ++
67 "-------------------------------- (" ++ show nm ++
68 ") -------\n " ++
69 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
70 where showPs env [] = ""
71 showPs env ((n, Let t v):bs)
72 = " " ++ show n ++ " : " ++
73 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
74 showEnv env ({- normalise ctxt env -} v) ++
75 "\n" ++ showPs env bs
76 showPs env ((n, b):bs)
77 = " " ++ show n ++ " : " ++
78 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
79 "\n" ++ showPs env bs
80 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
81 " =?= " ++ showEnv ps v
82 showG ps b = showEnv ps (binderTy b)
84same Nothing n = True
85same (Just x) n = x == n
87hole (Hole _) = True
88hole (Guess _ _) = True
89hole _ = False
91holeName i = MN i "hole"
93getName :: Monad m => String -> StateT TState m Name
94getName tag = do ps <- get
95 let n = nextname ps
96 put (ps { nextname = n+1 })
97 return $ MN n tag
99action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
100action a = do ps <- get
101 put (a ps)
103addLog :: Monad m => String -> StateT TState m ()
104addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
106newProof :: Name -> Context -> Type -> ProofState
107newProof n ctxt ty = let h = holeName 0
108 ty' = vToP ty in
109 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
110 Nothing ctxt "" False
112type TState = ProofState -- [TacticAction])
113type RunTactic = Context -> Env -> Term -> StateT TState TC Term
114type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
116envAtFocus :: ProofState -> TC Env
117envAtFocus ps
118 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
119 return (premises g)
120 | otherwise = fail "No holes"
122goalAtFocus :: ProofState -> TC Type
123goalAtFocus ps
124 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
125 return (binderTy (goalType g))
127goal :: Hole -> Term -> TC Goal
128goal h tm = g [] tm where
129 g env (Bind n b sc) | hole b && same h n = return $ GD env b
130 | otherwise
131 = gb env b `mplus` g ((n, b):env) sc
132 g env (App f a) = g env f `mplus` g env a
133 g env t = Error "Can't find hole"
135 gb env (Let t v) = g env t `mplus` g env v
136 gb env (Guess t v) = g env t `mplus` g env v
137 gb env t = g env (binderTy t)
139tactic :: Hole -> RunTactic -> StateT TState TC ()
140tactic h f = do ps <- get
141 tm' <- atH (context ps) [] (pterm ps)
142 ps <- get -- might have changed while processing
143 put (ps { pterm = tm' })
144 where
145 atH c env binder@(Bind n b sc)
146 | hole b && same h n = f c env binder
147 | otherwise
148 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
149 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
150 atH c env t = return t
152 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
153 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
154 atHb c env t = do ty' <- atH c env (binderTy t)
155 return $ t { binderTy = ty' }
157attack :: RunTactic
158attack ctxt env (Bind x (Hole t) sc)
159 = do h <- getName "hole"
160 action (\ps -> ps { holes = h : holes ps })
161 return $ Bind x (Guess t (newtm h)) sc
162 where
163 newtm h = Bind h (Hole t) (P Bound h t)
164attack ctxt env _ = fail "Not an attackable hole"
166claim :: Name -> Raw -> RunTactic
167claim n ty ctxt env t =
168 do (tyv, tyt) <- lift $ check ctxt env ty
169 lift $ isSet ctxt env tyt
170 action (\ps -> let (g:gs) = holes ps in
171 ps { holes = g : n : gs } )
172 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
174focus :: Name -> RunTactic
175focus n ctxt env t = do action (\ps -> let hs = holes ps in
176 if n `elem` hs
177 then ps { holes = n : (hs \\ [n]) }
178 else ps)
179 return t
181movelast :: Name -> RunTactic
182movelast n ctxt env t = do action (\ps -> let hs = holes ps in
183 if n `elem` hs
184 then ps { holes = (hs \\ [n]) ++ [n] }
185 else ps)
186 return t
188-- Hmmm. YAGNI?
189regret :: RunTactic
190regret = undefined
192exact :: Raw -> RunTactic
193exact guess ctxt env (Bind x (Hole ty) sc) =
194 do (val, valty) <- lift $ check ctxt env guess
195 lift $ converts ctxt env valty ty
196 return $ Bind x (Guess ty val) sc
197exact _ _ _ _ = fail "Can't fill here."
199-- As exact, but attempts to solve other goals by unification
201fill :: Raw -> RunTactic
202fill guess ctxt env (Bind x (Hole ty) sc) =
203 do (val, valty) <- lift $ check ctxt env guess
204 ns <- lift $ unify ctxt env valty ty
205 ps <- get
206 let (uh, uns) = unified ps
207 put (ps { unified = (uh, uns ++ ns) })
208-- addLog (show (uh, uns ++ ns))
209 return $ Bind x (Guess ty val) sc
210fill _ _ _ _ = fail "Can't fill here."
212solve :: RunTactic
213solve ctxt env (Bind x (Guess ty val) sc)
214 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
215 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
216 | otherwise = fail "I see a hole in your solution."
217solve _ _ h = fail $ "Not a guess " ++ show h
219intro :: Name -> RunTactic
220intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
221 do let t' = normalise ctxt env t
222 case t' of
223 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
224 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
225 _ -> fail "Nothing to introduce"
226intro ctxt env _ _ = fail "Can't introduce here."
228forall :: Name -> Raw -> RunTactic
229forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
230 do (tyv, tyt) <- lift $ check ctxt env ty
231 lift $ isSet ctxt env tyt
232 lift $ isSet ctxt env t
233 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
235patvar :: Name -> RunTactic
236patvar n ctxt env (Bind x (Hole t) sc) =
237 do action (\ps -> ps { holes = holes ps \\ [x] })
238 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
240compute :: RunTactic
241compute ctxt env (Bind x (Hole ty) sc) =
242 do return $ Bind x (Hole (normalise ctxt env ty)) sc
244check_in :: Raw -> RunTactic
245check_in t ctxt env tm =
246 do (val, valty) <- lift $ check ctxt env t
247 addLog (showEnv env val ++ " : " ++ showEnv env valty)
248 return tm
250eval_in :: Raw -> RunTactic
251eval_in t ctxt env tm =
252 do (val, valty) <- lift $ check ctxt env t
253 let val' = normalise ctxt env val
254 let valty' = normalise ctxt env valty
255 addLog (showEnv env val ++ " : " ++
256 showEnv env valty ++
257-- " in " ++ show env ++
258 " ==>\n " ++
259 showEnv env val' ++ " : " ++
260 showEnv env valty')
261 return tm
263start_unify :: Name -> RunTactic
264start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
265 return tm
267solve_unified :: RunTactic
268solve_unified ctxt env tm =
269 do ps <- get
270 let (_, ns) = unified ps
271 action (\ps -> ps { holes = holes ps \\ map fst ns })
272-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
273 return (updateSolved ns tm)
274 where
275 updateSolved xs (Bind n (Hole ty) t)
276 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
277 updateSolved xs (Bind n b t)
278 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
279 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
280 updateSolved xs (P _ n _)
281 | Just v <- lookup n xs = v
282 updateSolved xs t = t
284-- shuffleHoles :: Term -> Term
285-- shuffleHoles tm = shuffle [] tm
286-- where
287-- shuffle ns (Bind n b sc)
288-- |
290processTactic :: Tactic -> ProofState -> TC (ProofState, String)
291processTactic QED ps = case holes ps of
292 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
293 (tm', ty') <- recheck (context ps) [] tm
294 return (ps { done = True, pterm = tm' },
295 "Proof complete: " ++ showEnv [] tm')
296 _ -> Error "Still holes to fill."
297processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
298processTactic Undo ps = case previous ps of
299 Nothing -> Error "Nothing to undo."
300 Just pold -> return (pold, "")
301processTactic EndUnify ps = let (h, ns) = unified ps
302 tm' = updateSolved ns (pterm ps) in
303 return (ps { pterm = tm',
304 unified = (h, []),
305 holes = holes ps \\ map fst ns }, "")
306 where
307 updateSolved xs (Bind n (Hole ty) t)
308 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
309 updateSolved xs (Bind n b t)
310 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
311 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
312 updateSolved xs (P _ n _)
313 | Just v <- lookup n xs = v
314 updateSolved xs t = t
315processTactic t ps
316 = case holes ps of
317 [] -> Error "Nothing to fill in."
318 (h:_) -> do let n = nextname ps
319 ps' <- execStateT (process t h) ps
320 return (ps' { previous = Just ps, plog = "" }, plog ps')
322process :: Tactic -> Name -> StateT TState TC ()
323process EndUnify _
324 = do ps <- get
325 let (h, _) = unified ps
326 tactic (Just h) solve_unified
327process t h = tactic (Just h) (mktac t)
328 where mktac Attack = attack
329 mktac (Claim n r) = claim n r
330 mktac (Exact r) = exact r
331 mktac (Fill r) = fill r
332 mktac Regret = regret
333 mktac Solve = solve
334 mktac (StartUnify n) = start_unify n
335 mktac Compute = compute
336 mktac (Intro n) = intro n
337 mktac (Forall n t) = forall n t
338 mktac (PatVar n) = patvar n
339 mktac (CheckIn r) = check_in r
340 mktac (EvalIn r) = eval_in r
341 mktac (Focus n) = focus n
342 mktac (MoveLast n) = movelast n