git.iko.soy/Idris-dev
on cbc60eb help sign in
Idris-dev/src/ProofState.hs
273 lines 10 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ProofState where
5import Typecheck
6import Evaluate
7import Core
8import Unify
10import Control.Monad.State
11import Control.Applicative
12import Data.List
13import Debug.Trace
15data ProofState = PS { thname :: Name,
16 holes :: [Name], -- holes still to be solved
17 nextname :: Int, -- name supply
18 pterm :: Term, -- current proof term
19 ptype :: Type, -- original goal
20 context :: Context,
21 done :: Bool
22 }
24data Goal = GD { premises :: Env,
25 goalType :: Binder Term
26 }
28data Command = Theorem Name Raw
29 | Eval Raw
30 | Quit
31 | Print Name
32 | Tac Tactic
34data Tactic = Attack
35 | Claim Name Raw
36 | Fill Raw
37 | UnifyFill Raw
38 | Regret
39 | Solve
40 | Compute
41 | EvalIn Raw
42 | CheckIn Raw
43 | Intro Name
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
157regret :: RunTactic
158regret = undefined
160fill :: Raw -> RunTactic
161fill guess ctxt env (Bind x (Hole ty) sc) =
162 do (val, valty) <- lift $ check ctxt env guess
163 lift $ converts ctxt env valty ty
164 return $ Bind x (Guess ty val) sc
165fill _ _ _ _ = fail "Can't fill here."
167-- As fill, but attempts to solve other goals by unification
169unify_fill :: Raw -> RunTactic
170unify_fill guess ctxt env (Bind x (Hole ty) sc) =
171 do (val, valty) <- lift $ check ctxt env guess
172 ns <- lift $ unify ctxt env valty ty
173 solve_all ns
174 return $ Bind x (Guess ty val) sc
175 where
176 solve_all [] = return ()
177 solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
178 solve_all ns
179unify_fill _ _ _ _ = fail "Can't fill here."
181solve :: RunTactic
182solve ctxt env (Bind x (Guess ty val) sc)
183 | pureTerm val = do action (Solved x)
184 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
185 | otherwise = fail "I see a hole in your solution."
186solve _ _ _ = fail "Not a guess."
188intro :: Name -> RunTactic
189intro n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
190 do let t' = normalise ctxt env t
191 case t' of
192 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
193 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
194 _ -> fail "Nothing to introduce"
195intro ctxt env _ _ = fail "Can't introduce here."
197compute :: RunTactic
198compute ctxt env (Bind x (Hole ty) sc) =
199 do return $ Bind x (Hole (normalise ctxt env ty)) sc
201check_in :: Raw -> RunTactic
202check_in t ctxt env tm =
203 do (val, valty) <- lift $ check ctxt env t
204 action (Log (showEnv env val ++ " : " ++ showEnv env valty))
205 return tm
207eval_in :: Raw -> RunTactic
208eval_in t ctxt env tm =
209 do (val, valty) <- lift $ check ctxt env t
210 let val' = normalise ctxt env val
211 let valty' = normalise ctxt env valty
212 action (Log (showEnv env val ++ " : " ++
213 showEnv env valty ++
214-- " in " ++ show env ++
215 " ==>\n " ++
216 showEnv env val' ++ " : " ++
217 showEnv env valty'))
218 return tm
221processTactic :: Tactic -> ProofState -> TC (ProofState, String)
222processTactic QED ps = case holes ps of
223 [] -> let tm = finalise (pterm ps) in
224 return (ps { done = True, pterm = tm },
225 "Proof complete: " ++ showEnv [] tm)
226 _ -> Error "Still holes to fill."
227processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
228processTactic t ps
229 = case holes ps of
230 [] -> Error "Nothing to fill in."
231 (h:_) -> do let n = nextname ps
232 (ps', (n', actions)) <- runStateT (process t h ps) (n, [])
233 return (ps' { nextname = n',
234 pterm = updateSolved (getSolved actions) (pterm ps'),
235 holes = goals (holes ps') actions },
236 logs actions)
237 where logs [] = ""
238 logs (Log x : xs) = x ++ "\n" ++ logs xs
239 logs (_ : xs) = logs xs
241 goals g [] = g
242 goals g (AddGoal n : xs) = goals (n : g) xs
243 goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
244 goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs
245 goals g (Solved n : xs) = goals (g \\ [n]) xs
246 goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs
247 goals g (_ : xs) = goals g xs
249 getSolved [] = []
250 getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs
251 getSolved (_ : xs) = getSolved xs
253 updateSolved xs (Bind n b t)
254 | Just v <- lookup n xs = Bind n (Let (binderTy b) v) (updateSolved xs t)
255 | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
256 updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
257 updateSolved xs t = t
261process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
262process t h ps = tactic (Just h) ps (context ps) (mktac t)
263 where mktac Attack = attack
264 mktac (Claim n r) = claim n r
265 mktac (Fill r) = fill r
266 mktac (UnifyFill r) = unify_fill r
267 mktac Regret = regret
268 mktac Solve = solve
269 mktac Compute = compute
270 mktac (Intro n) = intro n
271 mktac (CheckIn r) = check_in r
272 mktac (EvalIn r) = eval_in r
273 mktac (Focus n) = focus n