git.iko.soy/Idris-dev
on ee3dbaa help sign in
Idris-dev/src/ProofState.hs
317 lines 12 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
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 ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), processTactic) where
10import Typecheck
11import Evaluate
12import Core
13import 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 defer :: [(Name, Type)], -- names we'll need to define
26 previous :: Maybe ProofState, -- for undo
27 context :: Context,
28 done :: Bool
29 }
31data Goal = GD { premises :: Env,
32 goalType :: Binder Term
33 }
35data Tactic = Attack
36 | Claim Name Raw
37 | Exact Raw
38 | Fill Raw
39 | Regret
40 | Solve
41 | Compute
42 | EvalIn Raw
43 | CheckIn Raw
44 | Intro Name
45 | Forall Name Raw
46 | PatVar Name Raw
47 | Focus Name
48 | MoveLast Name
49 | ProofState
50 | Undo
51 | QED
53data TacticAction = AddGoal Name -- add a new goal, solve immediately
54 | NextGoal Name -- add a new goal, solve it after current one
55 | FocusGoal Name -- focus on this goal next
56 | MoveGoal Name -- move this goal to the end of the hole queue
57 | Solved Name
58 | AlsoSolved Name Term -- goals solved by unification
59 | Log String
61-- Some utilites on proof and tactic states
63instance Show ProofState where
64 show (PS nm [] _ tm _ _ _ _ _) = show nm ++ ": no more goals"
65 show (PS nm (h:hs) _ tm _ i _ ctxt _)
66 = let OK g = goal (Just h) tm
67 wkenv = premises g in
68 showPs wkenv (reverse wkenv) ++ "\n" ++
69 "-------------------------------- (" ++ show nm ++
70 ") -------\n" ++
71 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
72 where showPs env [] = ""
73 showPs env ((n, Let t v):bs)
74 = " " ++ show n ++ " : " ++
75 showEnv env (normalise ctxt env t) ++ " = " ++
76 showEnv env (normalise ctxt env v) ++
77 "\n" ++ showPs env bs
78 showPs env ((n, b):bs)
79 = " " ++ show n ++ " : " ++
80 showEnv env (normalise ctxt env (binderTy b)) ++
81 "\n" ++ showPs env bs
82 showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++
83 " =?= " ++ showEnv ps v
84 showG ps b = showEnv ps (binderTy b)
86same Nothing n = True
87same (Just x) n = x == n
89hole (Hole _) = True
90hole (Guess _ _) = True
91hole _ = False
93holeName i = MN i "hole"
95getName :: Monad m => String -> StateT TState m Name
96getName tag = do (n, ts) <- get
97 put (n+1, ts)
98 return $ MN n tag
100action :: Monad m => TacticAction -> StateT TState m ()
101action a = do (n, ts) <- get
102 put (n, a:ts)
104newProof :: Name -> Context -> Type -> ProofState
105newProof n ctxt ty = let h = holeName 0
106 ty' = vToP ty in
107 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty []
108 Nothing ctxt False
110type TState = (Int, [TacticAction])
111type RunTactic = Context -> Env -> Term -> StateT TState TC Term
112type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
114envAtFocus :: ProofState -> TC Env
115envAtFocus ps
116 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
117 return (premises g)
118 | otherwise = fail "No holes"
120goalAtFocus :: ProofState -> TC Type
121goalAtFocus ps
122 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
123 return (binderTy (goalType g))
125goal :: Hole -> Term -> TC Goal
126goal h tm = g [] tm where
127 g env (Bind n b sc) | hole b && same h n = return $ GD env b
128 | otherwise
129 = gb env b `mplus` g ((n, b):env) sc
130 g env (App f a) = g env f `mplus` g env a
131 g env t = Error "Can't find hole"
133 gb env (Let t v) = g env t `mplus` g env v
134 gb env (Guess t v) = g env t `mplus` g env v
135 gb env t = g env (binderTy t)
137tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
138tactic h ps ctxt f = do let tm = pterm ps
139 tm' <- atH [] tm
140 return (ps { pterm = tm' })
141 where
142 atH env binder@(Bind n b sc)
143 | hole b && same h n = f ctxt env binder
144 | otherwise
145 = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b) : env) sc
146 atH env (App f a) = pure App <*> atH env f <*> atH env a
147 atH env t = return t
149 atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
150 atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
151 atHb env t = do ty' <- atH env (binderTy t)
152 return $ t { binderTy = ty' }
154attack :: RunTactic
155attack ctxt env (Bind x (Hole t) sc)
156 = do h <- getName "hole"
157 action (AddGoal h)
158 return $ Bind x (Guess t (newtm h)) sc
159 where
160 newtm h = Bind h (Hole t) (P Bound h t)
161attack ctxt env _ = fail "Not an attackable hole"
163claim :: Name -> Raw -> RunTactic
164claim n ty ctxt env t =
165 do (tyv, tyt) <- lift $ check ctxt env ty
166 lift $ isSet ctxt env tyt
167 action (NextGoal n)
168 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
170focus :: Name -> RunTactic
171focus n ctxt env t = do action (FocusGoal n)
172 return t
174movelast :: Name -> RunTactic
175movelast n ctxt env t = do action (MoveGoal n)
176 return t
178-- Hmmm. YAGNI?
179regret :: RunTactic
180regret = undefined
182exact :: Raw -> RunTactic
183exact guess ctxt env (Bind x (Hole ty) sc) =
184 do (val, valty) <- lift $ check ctxt env guess
185 lift $ converts ctxt env valty ty
186 return $ Bind x (Guess ty val) sc
187exact _ _ _ _ = fail "Can't fill here."
189-- As fill, but attempts to solve other goals by unification
191fill :: Raw -> RunTactic
192fill guess ctxt env (Bind x (Hole ty) sc) =
193 do (val, valty) <- lift $ check ctxt env guess
194 ns <- lift $ unify ctxt env valty ty
195 solve_all ns
196 return $ Bind x (Guess ty val) sc
197 where
198 solve_all [] = return ()
199 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
200 solve_all ns
201fill _ _ _ _ = fail "Can't fill here."
203solve :: RunTactic
204solve ctxt env (Bind x (Guess ty val) sc)
205 | pureTerm val = do action (Solved x)
206 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
207 | otherwise = fail "I see a hole in your solution."
208solve _ _ _ = fail "Not a guess."
210intro :: Name -> RunTactic
211intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
212 do let t' = normalise ctxt env t
213 case t' of
214 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
215 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
216 _ -> fail "Nothing to introduce"
217intro ctxt env _ _ = fail "Can't introduce here."
219forall :: Name -> Raw -> RunTactic
220forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
221 do (tyv, tyt) <- lift $ check ctxt env ty
222 lift $ isSet ctxt env tyt
223 lift $ isSet ctxt env t
224 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
226patvar :: Name -> Raw -> RunTactic
227patvar n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
228 do (tyv, tyt) <- lift $ check ctxt env ty
229 lift $ isSet ctxt env tyt
230 return $ Bind n (PVar tyv) (Bind x (Hole t) (P Bound x t))
232compute :: RunTactic
233compute ctxt env (Bind x (Hole ty) sc) =
234 do return $ Bind x (Hole (normalise ctxt env ty)) sc
236check_in :: Raw -> RunTactic
237check_in t ctxt env tm =
238 do (val, valty) <- lift $ check ctxt env t
239 action (Log (showEnv env val ++ " : " ++ showEnv env valty))
240 return tm
242eval_in :: Raw -> RunTactic
243eval_in t ctxt env tm =
244 do (val, valty) <- lift $ check ctxt env t
245 let val' = normalise ctxt env val
246 let valty' = normalise ctxt env valty
247 action (Log (showEnv env val ++ " : " ++
248 showEnv env valty ++
249-- " in " ++ show env ++
250 " ==>\n " ++
251 showEnv env val' ++ " : " ++
252 showEnv env valty'))
253 return tm
255processTactic :: Tactic -> ProofState -> TC (ProofState, String)
256processTactic QED ps = case holes ps of
257 [] -> do let tm = pterm ps
258 (tm', ty') <- recheck (context ps) [] tm
259 return (ps { done = True, pterm = tm' },
260 "Proof complete: " ++ showEnv [] tm')
261 _ -> Error "Still holes to fill."
262processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
263processTactic Undo ps = case previous ps of
264 Nothing -> Error "Nothing to undo."
265 Just pold -> return (pold, "")
266processTactic t ps
267 = case holes ps of
268 [] -> Error "Nothing to fill in."
269 (h:_) -> do let n = nextname ps
270 (ps', (n', actions)) <- runStateT (process t h ps) (n, [])
271 return (ps' { nextname = n',
272 pterm = updateSolved (getSolved actions) (pterm ps'),
273 holes = goals (holes ps') actions,
274 previous = Just ps },
275 logs actions)
276 where logs [] = ""
277 logs (Log x : xs) = x ++ "\n" ++ logs xs
278 logs (_ : xs) = logs xs
280 goals g [] = g
281 goals g (AddGoal n : xs) = goals (n : g) xs
282 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
283 goals g (FocusGoal n : xs)
284 | n `elem` g = goals (n : (g \\ [n])) xs
285 goals g (MoveGoal n : xs)
286 | n `elem` g = goals ((g \\ [n]) ++ [n]) xs
287 goals g (Solved n : xs) = goals (g \\ [n]) xs
288 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs
289 goals g (_ : xs) = goals g xs
291 getSolved [] = []
292 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs
293 getSolved (_ : xs) = getSolved xs
295 updateSolved xs (Bind n b@(Hole _) t)
296 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
297 updateSolved xs (Bind n b t)
298 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
299 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
300 updateSolved xs t = t
302process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
303process t h ps = tactic (Just h) ps (context ps) (mktac t)
304 where mktac Attack = attack
305 mktac (Claim n r) = claim n r
306 mktac (Exact r) = exact r
307 mktac (Fill r) = fill r
308 mktac Regret = regret
309 mktac Solve = solve
310 mktac Compute = compute
311 mktac (Intro n) = intro n
312 mktac (Forall n t) = forall n t
313 mktac (PatVar n t) = patvar n t
314 mktac (CheckIn r) = check_in r
315 mktac (EvalIn r) = eval_in r
316 mktac (Focus n) = focus n
317 mktac (MoveLast n) = movelast n