git.iko.soy/Idris-dev
on bf368ab help sign in
Idris-dev/src/Core/ProofState.hs
398 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(..), 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 Type
128goalAtFocus ps
129 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
130 return (binderTy (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)
143tactic :: Hole -> RunTactic -> StateT TState TC ()
144tactic h f = do ps <- get
145 tm' <- atH (context ps) [] (pterm ps)
146 ps <- get -- might have changed while processing
147 put (ps { pterm = tm' })
148 where
149 atH c env binder@(Bind n b sc)
150 | hole b && same h n = f c env binder
151 | otherwise
152 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
153 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
154 atH c env t = return t
156 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
157 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
158 atHb c env t = do ty' <- atH c env (binderTy t)
159 return $ t { binderTy = ty' }
161attack :: RunTactic
162attack ctxt env (Bind x (Hole t) sc)
163 = do h <- getName "hole"
164 action (\ps -> ps { holes = h : holes ps })
165 return $ Bind x (Guess t (newtm h)) sc
166 where
167 newtm h = Bind h (Hole t) (P Bound h t)
168attack ctxt env _ = fail "Not an attackable hole"
170claim :: Name -> Raw -> RunTactic
171claim n ty ctxt env t =
172 do (tyv, tyt) <- lift $ check ctxt env ty
173 lift $ isSet ctxt env tyt
174 action (\ps -> let (g:gs) = holes ps in
175 ps { holes = g : n : gs } )
176 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
178focus :: Name -> RunTactic
179focus n ctxt env t = do action (\ps -> let hs = holes ps in
180 if n `elem` hs
181 then ps { holes = n : (hs \\ [n]) }
182 else ps)
183 return t
185movelast :: Name -> RunTactic
186movelast n ctxt env t = do action (\ps -> let hs = holes ps in
187 if n `elem` hs
188 then ps { holes = (hs \\ [n]) ++ [n] }
189 else ps)
190 return t
192defer :: Name -> RunTactic
193defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
194 do action (\ps -> let hs = holes ps in
195 ps { holes = hs \\ [x] })
196 return (Bind n (GHole (mkTy (reverse env) t))
197 (mkApp (P nt n ty) (map getP (reverse env))))
198 where
199 mkTy [] t = t
200 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
202 getP (n, b) = P Bound n (binderTy b)
204-- Hmmm. YAGNI?
205regret :: RunTactic
206regret = undefined
208exact :: Raw -> RunTactic
209exact guess ctxt env (Bind x (Hole ty) sc) =
210 do (val, valty) <- lift $ check ctxt env guess
211 lift $ converts ctxt env valty ty
212 return $ Bind x (Guess ty val) sc
213exact _ _ _ _ = fail "Can't fill here."
215-- As exact, but attempts to solve other goals by unification
217fill :: Raw -> RunTactic
218fill guess ctxt env (Bind x (Hole ty) sc) =
219 do (val, valty) <- lift $ check ctxt env guess
220 ns <- lift $ unify ctxt env valty ty
221 ps <- get
222 let (uh, uns) = unified ps
223 put (ps { unified = (uh, uns ++ ns) })
224-- addLog (show (uh, uns ++ ns))
225 return $ Bind x (Guess ty val) sc
226fill _ _ _ _ = fail "Can't fill here."
228prep_fill :: Name -> [Name] -> RunTactic
229prep_fill f as ctxt env (Bind x (Hole ty) sc) =
230 do let val = mkApp (P Ref f undefined) (map (\n -> P Ref n undefined) as)
231 return $ Bind x (Guess ty val) sc
232prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
234complete_fill :: RunTactic
235complete_fill ctxt env (Bind x (Guess ty val) sc) =
236 do let guess = forget val
237 (val', valty) <- lift $ check ctxt env guess
238 ns <- lift $ unify ctxt env valty ty
239 ps <- get
240 let (uh, uns) = unified ps
241 put (ps { unified = (uh, uns ++ ns) })
242 return $ Bind x (Guess ty val) sc
243complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
245solve :: RunTactic
246solve ctxt env (Bind x (Guess ty val) sc)
247 | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
248 return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)
249 | otherwise = fail "I see a hole in your solution."
250solve _ _ h = fail $ "Not a guess " ++ show h
252intro :: Name -> RunTactic
253intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
254 do let t' = normalise ctxt env t
255 case t' of
256 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
257 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
258 _ -> fail "Nothing to introduce"
259intro n ctxt env _ = fail "Can't introduce here."
261forall :: Name -> Raw -> RunTactic
262forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
263 do (tyv, tyt) <- lift $ check ctxt env ty
264 lift $ isSet ctxt env tyt
265 lift $ isSet ctxt env t
266 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
267forall n ty ctxt env _ = fail "Can't pi bind here"
269patvar :: Name -> RunTactic
270patvar n ctxt env (Bind x (Hole t) sc) =
271 do action (\ps -> ps { holes = holes ps \\ [x] })
272 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
274letbind :: Name -> Raw -> Raw -> RunTactic
275letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
276 do (tyv, tyt) <- lift $ check ctxt env ty
277 (valv, valt) <- lift $ check ctxt env val
278 lift $ isSet ctxt env tyt
279 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
280letbind n ty val ctxt env _ = fail "Can't let bind here"
282patbind :: Name -> RunTactic
283patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
284 do let t' = normalise ctxt env t
285 case t' of
286 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
287 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
288 _ -> fail "Nothing to pattern bind"
289patbind n ctxt env _ = fail "Can't pattern bind here"
291compute :: RunTactic
292compute ctxt env (Bind x (Hole ty) sc) =
293 do return $ Bind x (Hole (normalise ctxt env ty)) sc
295check_in :: Raw -> RunTactic
296check_in t ctxt env tm =
297 do (val, valty) <- lift $ check ctxt env t
298 addLog (showEnv env val ++ " : " ++ showEnv env valty)
299 return tm
301eval_in :: Raw -> RunTactic
302eval_in t ctxt env tm =
303 do (val, valty) <- lift $ check ctxt env t
304 let val' = normalise ctxt env val
305 let valty' = normalise ctxt env valty
306 addLog (showEnv env val ++ " : " ++
307 showEnv env valty ++
308-- " in " ++ show env ++
309 " ==>\n " ++
310 showEnv env val' ++ " : " ++
311 showEnv env valty')
312 return tm
314start_unify :: Name -> RunTactic
315start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
316 return tm
318solve_unified :: RunTactic
319solve_unified ctxt env tm =
320 do ps <- get
321 let (_, ns) = unified ps
322 action (\ps -> ps { holes = holes ps \\ map fst ns })
323-- action (\ps -> ps { pterm = updateSolved ns (pterm ps) })
324 return (updateSolved ns tm)
325 where
326 updateSolved xs (Bind n (Hole ty) t)
327 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
328 updateSolved xs (Bind n b t)
329 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
330 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
331 updateSolved xs (P _ n _)
332 | Just v <- lookup n xs = v
333 updateSolved xs t = t
335-- shuffleHoles :: Term -> Term
336-- shuffleHoles tm = shuffle [] tm
337-- where
338-- shuffle ns (Bind n b sc)
339-- |
341processTactic :: Tactic -> ProofState -> TC (ProofState, String)
342processTactic QED ps = case holes ps of
343 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
344 (tm', ty') <- recheck (context ps) [] tm
345 return (ps { done = True, pterm = tm' },
346 "Proof complete: " ++ showEnv [] tm')
347 _ -> fail "Still holes to fill."
348processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
349processTactic Undo ps = case previous ps of
350 Nothing -> fail "Nothing to undo."
351 Just pold -> return (pold, "")
352processTactic EndUnify ps = let (h, ns) = unified ps
353 tm' = updateSolved ns (pterm ps) in
354 return (ps { pterm = tm',
355 unified = (h, []),
356 holes = holes ps \\ map fst ns }, "")
357 where
358 updateSolved xs (Bind n (Hole ty) t)
359 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
360 updateSolved xs (Bind n b t)
361 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
362 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
363 updateSolved xs (P _ n _)
364 | Just v <- lookup n xs = v
365 updateSolved xs t = t
366processTactic t ps
367 = case holes ps of
368 [] -> fail "Nothing to fill in."
369 (h:_) -> do let n = nextname ps
370 ps' <- execStateT (process t h) ps
371 return (ps' { previous = Just ps, plog = "" }, plog ps')
373process :: Tactic -> Name -> StateT TState TC ()
374process EndUnify _
375 = do ps <- get
376 let (h, _) = unified ps
377 tactic (Just h) solve_unified
378process t h = tactic (Just h) (mktac t)
379 where mktac Attack = attack
380 mktac (Claim n r) = claim n r
381 mktac (Exact r) = exact r
382 mktac (Fill r) = fill r
383 mktac (PrepFill n ns) = prep_fill n ns
384 mktac CompleteFill = complete_fill
385 mktac Regret = regret
386 mktac Solve = solve
387 mktac (StartUnify n) = start_unify n
388 mktac Compute = compute
389 mktac (Intro n) = intro n
390 mktac (Forall n t) = forall n t
391 mktac (LetBind n t v) = letbind n t v
392 mktac (PatVar n) = patvar n
393 mktac (PatBind n) = patbind n
394 mktac (CheckIn r) = check_in r
395 mktac (EvalIn r) = eval_in r
396 mktac (Focus n) = focus n
397 mktac (MoveLast n) = movelast n
398 mktac (Defer n) = defer n