git.iko.soy/Idris-dev
on cc0dc09 help sign in
Idris-dev/src/ProofState.hs
281 lines 11 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,
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 | Focus Name
45 | ProofState
46 | QED
47-- Next: add 'EvalHere' and 'CheckHere' tactics
49data TacticAction = AddGoal Name -- add a new goal, solve immediately
50 | NextGoal Name -- add a new goal, solve it after current one
51 | FocusGoal Name -- focus on this goal next
52 | Solved Name
53 | AlsoSolved Name Term -- goals solved by unification
54 | Log String
56-- Some utilites on proof and tactic states
58instance Show ProofState where
59 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
60 show (PS nm (h:hs) _ tm _ ctxt _)
61 = let OK g = goal (Just h) tm ctxt
62 wkenv = premises g in
63 showPs wkenv (reverse wkenv) ++ "\n" ++
64 "-------------------------------- (" ++ show nm ++
65 ") -------\n" ++
66 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
67 where showPs env [] = ""
68 showPs env ((n, Let t v):bs)
69 = " " ++ show n ++ " : " ++
70 showEnv env (normalise ctxt env t) ++ " = " ++
71 showEnv env (normalise ctxt env v) ++
72 "\n" ++ showPs env bs
73 showPs env ((n, b):bs)
74 = " " ++ show n ++ " : " ++
75 showEnv env (normalise ctxt env (binderTy b)) ++
76 "\n" ++ showPs env bs
77 showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++
78 " =?= " ++ showEnv ps v
79 showG ps b = showEnv ps (binderTy b)
81same Nothing n = True
82same (Just x) n = x == n
84hole (Hole _) = True
85hole (Guess _ _) = True
86hole _ = False
88holeName i = MN i "hole"
90getName :: Monad m => String -> StateT TState m Name
91getName tag = do (n, ts) <- get
92 put (n+1, ts)
93 return $ MN n tag
95action :: Monad m => TacticAction -> StateT TState m ()
96action a = do (n, ts) <- get
97 put (n, a:ts)
99newProof :: Name -> Context -> Type -> ProofState
100newProof n ctxt ty = let h = holeName 0
101 ty' = vToP ty in
102 PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty ctxt False
104type TState = (Int, [TacticAction])
105type RunTactic = Context -> Env -> Term -> StateT TState TC Term
106type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
108goal :: Hole -> Term -> Context -> TC Goal
109goal h tm ctxt = g [] tm where
110 g env (Bind n b sc) | hole b && same h n = return $ GD env b
111 | otherwise
112 = gb env b `mplus` g ((n, b):env) sc
113 g env (App f a) = g env f `mplus` g env a
114 g env t = Error "Can't find hole"
116 gb env (Let t v) = g env t `mplus` g env v
117 gb env (Guess t v) = g env t `mplus` g env v
118 gb env t = g env (binderTy t)
120tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
121tactic h ps ctxt f = do let tm = pterm ps
122 tm' <- atH [] tm
123 return (ps { pterm = tm' })
124 where
125 atH env binder@(Bind n b sc)
126 | hole b && same h n = f ctxt env binder
127 | otherwise
128 = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b) : env) sc
129 atH env (App f a) = pure App <*> atH env f <*> atH env a
130 atH env t = return t
132 atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
133 atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
134 atHb env t = do ty' <- atH env (binderTy t)
135 return $ t { binderTy = ty' }
137attack :: RunTactic
138attack ctxt env (Bind x (Hole t) sc)
139 = do h <- getName "hole"
140 action (AddGoal h)
141 return $ Bind x (Guess t (newtm h)) sc
142 where
143 newtm h = Bind h (Hole t) (P Bound h t)
144attack ctxt env _ = fail "Not an attackable hole"
146claim :: Name -> Raw -> RunTactic
147claim n ty ctxt env t =
148 do (tyv, tyt) <- lift $ check ctxt env ty
149 lift $ isSet ctxt env tyt
150 action (NextGoal n)
151 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
153focus :: Name -> RunTactic
154focus n ctxt env t = do action (FocusGoal n)
155 return t
157-- Hmmm. YAGNI?
158regret :: RunTactic
159regret = undefined
161fill :: Raw -> RunTactic
162fill guess ctxt env (Bind x (Hole ty) sc) =
163 do (val, valty) <- lift $ check ctxt env guess
164 lift $ converts ctxt env valty ty
165 return $ Bind x (Guess ty val) sc
166fill _ _ _ _ = fail "Can't fill here."
168-- As fill, but attempts to solve other goals by unification
170unify_fill :: Raw -> RunTactic
171unify_fill guess ctxt env (Bind x (Hole ty) sc) =
172 do (val, valty) <- lift $ check ctxt env guess
173 ns <- lift $ unify ctxt env valty ty
174 solve_all ns
175 return $ Bind x (Guess ty val) sc
176 where
177 solve_all [] = return ()
178 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
179 solve_all ns
180unify_fill _ _ _ _ = fail "Can't fill here."
182solve :: RunTactic
183solve ctxt env (Bind x (Guess ty val) sc)
184 | pureTerm val = do action (Solved x)
185 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
186 | otherwise = fail "I see a hole in your solution."
187solve _ _ _ = fail "Not a guess."
189intro :: Name -> RunTactic
190intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
191 do let t' = normalise ctxt env t
192 case t' of
193 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
194 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
195 _ -> fail "Nothing to introduce"
196intro ctxt env _ _ = fail "Can't introduce here."
198forall :: Name -> Raw -> RunTactic
199forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
200 do (tyv, tyt) <- lift $ check ctxt env ty
201 lift $ isSet ctxt env tyt
202 lift $ isSet ctxt env t
203 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
206compute :: RunTactic
207compute ctxt env (Bind x (Hole ty) sc) =
208 do return $ Bind x (Hole (normalise ctxt env ty)) sc
210check_in :: Raw -> RunTactic
211check_in t ctxt env tm =
212 do (val, valty) <- lift $ check ctxt env t
213 action (Log (showEnv env val ++ " : " ++ showEnv env valty))
214 return tm
216eval_in :: Raw -> RunTactic
217eval_in t ctxt env tm =
218 do (val, valty) <- lift $ check ctxt env t
219 let val' = normalise ctxt env val
220 let valty' = normalise ctxt env valty
221 action (Log (showEnv env val ++ " : " ++
222 showEnv env valty ++
223-- " in " ++ show env ++
224 " ==>\n " ++
225 showEnv env val' ++ " : " ++
226 showEnv env valty'))
227 return tm
230processTactic :: Tactic -> ProofState -> TC (ProofState, String)
231processTactic QED ps = case holes ps of
232 [] -> let tm = finalise (pterm ps) in
233 return (ps { done = True, pterm = tm },
234 "Proof complete: " ++ showEnv [] tm)
235 _ -> Error "Still holes to fill."
236processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
237processTactic t ps
238 = case holes ps of
239 [] -> Error "Nothing to fill in."
240 (h:_) -> do let n = nextname ps
241 (ps', (n', actions)) <- runStateT (process t h ps) (n, [])
242 return (ps' { nextname = n',
243 pterm = updateSolved (getSolved actions) (pterm ps'),
244 holes = goals (holes ps') actions },
245 logs actions)
246 where logs [] = ""
247 logs (Log x : xs) = x ++ "\n" ++ logs xs
248 logs (_ : xs) = logs xs
250 goals g [] = g
251 goals g (AddGoal n : xs) = goals (n : g) xs
252 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
253 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs
254 goals g (Solved n : xs) = goals (g \\ [n]) xs
255 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs
256 goals g (_ : xs) = goals g xs
258 getSolved [] = []
259 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs
260 getSolved (_ : xs) = getSolved xs
262 updateSolved xs (Bind n b t)
263 | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)
264 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
265 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
266 updateSolved xs t = t
268process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
269process t h ps = tactic (Just h) ps (context ps) (mktac t)
270 where mktac Attack = attack
271 mktac (Claim n r) = claim n r
272 mktac (Fill r) = fill r
273 mktac (UnifyFill r) = unify_fill r
274 mktac Regret = regret
275 mktac Solve = solve
276 mktac Compute = compute
277 mktac (Intro n) = intro n
278 mktac (Forall n t) = forall n t
279 mktac (CheckIn r) = check_in r
280 mktac (EvalIn r) = eval_in r
281 mktac (Focus n) = focus n