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