git.iko.soy/Idris-dev
on bbaa193 help sign in
Idris-dev/src/Core/Elaborate.hs
349 lines 11 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3{- A high level language of tactic composition, for building
4 elaborators from a high level language into the core theory.
6 This is our interface to proof construction, rather than
7 ProofState, because this gives us a language to build derived
8 tactics out of the primitives.
9-}
11module Core.Elaborate(module Core.Elaborate,
12 module Core.ProofState) where
14import Core.ProofState
15import Core.TT
16import Core.Evaluate
17import Core.Typecheck
19import Control.Monad.State
20import Data.Char
21import Data.List
22import Debug.Trace
24-- I don't really want this here, but it's useful for the test shell
25data Command = Theorem Name Raw
26 | Eval Raw
27 | Quit
28 | Print Name
29 | Tac (Elab ())
31data ElabState = ES ProofState String (Maybe ElabState)
32 deriving Show
33type Elab a = StateT ElabState TC a
35proof :: ElabState -> ProofState
36proof (ES p _ _) = p
38saveState :: Elab ()
39saveState = do e@(ES p s _) <- get
40 put (ES p s (Just e))
42loadState :: Elab ()
43loadState = do (ES p s e) <- get
44 case e of
45 Just st -> put st
46 _ -> fail "Nothing to undo"
48erun :: FC -> Elab a -> Elab a
49erun f elab = do s <- get
50 case runStateT elab s of
51 OK (a, s') -> do put s'
52 return a
53 Error (At f e) -> lift $ Error (At f e)
54 Error e -> lift $ Error (At f e)
56runElab :: Elab a -> ProofState -> TC (a, ElabState)
57runElab e ps = runStateT e (ES ps "" Nothing)
59execElab :: Elab a -> ProofState -> TC ElabState
60execElab e ps = execStateT e (ES ps "" Nothing)
62initElaborator :: Name -> Context -> Type -> ProofState
63initElaborator = newProof
65elaborate :: Context -> Name -> Type -> Elab a -> TC (a, String)
66elaborate ctxt n ty elab = do let ps = initElaborator n ctxt ty
67 (a, ES ps' str _) <- runElab elab ps
68 return (a, str)
70processTactic' t = do ES p logs prev <- get
71 (p', log) <- lift $ processTactic t p
72 put (ES p' (logs ++ log) prev)
73 return ()
75-- Some handy gadgets for pulling out bits of state
77-- get the global context
78get_context :: Elab Context
79get_context = do ES p _ _ <- get
80 return (context p)
82-- get the proof term
83get_term :: Elab Term
84get_term = do ES p _ _ <- get
85 return (pterm p)
87-- get the local context at the currently in focus hole
88get_env :: Elab Env
89get_env = do ES p _ _ <- get
90 lift $ envAtFocus p
92get_holes :: Elab [Name]
93get_holes = do ES p _ _ <- get
94 return (holes p)
96-- get the current goal type
97goal :: Elab Type
98goal = do ES p _ _ <- get
99 b <- lift $ goalAtFocus p
100 return (binderTy b)
102-- typecheck locally
103get_type :: Raw -> Elab Type
104get_type tm = do ctxt <- get_context
105 env <- get_env
106 (val, ty) <- lift $ check ctxt env tm
107 return (finalise ty)
109-- get holes we've deferred for later definition
110get_deferred :: Elab [Name]
111get_deferred = do ES p _ _ <- get
112 return (deferred p)
114-- get instance argument names
115get_instances :: Elab [Name]
116get_instances = do ES p _ _ <- get
117 return (instances p)
119-- given a desired hole name, return a unique hole name
120unique_hole :: Name -> Elab Name
121unique_hole n = do ES p _ _ <- get
122 let bs = bound_in (pterm p) ++ bound_in (ptype p)
123 n' <- uniqueNameCtxt (context p) n (holes p ++ bs)
124 return n'
125 where
126 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
127 where
128 bi (Let t v) = bound_in t ++ bound_in v
129 bi (Guess t v) = bound_in t ++ bound_in v
130 bi b = bound_in (binderTy b)
131 bound_in (App f a) = bound_in f ++ bound_in a
132 bound_in _ = []
134uniqueNameCtxt :: Context -> Name -> [Name] -> Elab Name
135uniqueNameCtxt ctxt n hs
136 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
137 | Just _ <- lookupCtxt n ctxt = uniqueNameCtxt ctxt (nextName n) hs
138 | otherwise = return n
140elog :: String -> Elab ()
141elog str = do ES p logs prev <- get
142 put (ES p (logs ++ str ++ "\n") prev)
144-- The primitives, from ProofState
146attack :: Elab ()
147attack = processTactic' Attack
149claim :: Name -> Raw -> Elab ()
150claim n t = processTactic' (Claim n t)
152exact :: Raw -> Elab ()
153exact t = processTactic' (Exact t)
155fill :: Raw -> Elab ()
156fill t = processTactic' (Fill t)
158prep_fill :: Name -> [Name] -> Elab ()
159prep_fill n ns = processTactic' (PrepFill n ns)
161complete_fill :: Elab ()
162complete_fill = processTactic' CompleteFill
164solve :: Elab ()
165solve = processTactic' Solve
167start_unify :: Name -> Elab ()
168start_unify n = processTactic' (StartUnify n)
170end_unify :: Elab ()
171end_unify = processTactic' EndUnify
173regret :: Elab ()
174regret = processTactic' Regret
176compute :: Elab ()
177compute = processTactic' Compute
179eval_in :: Raw -> Elab ()
180eval_in t = processTactic' (EvalIn t)
182check_in :: Raw -> Elab ()
183check_in t = processTactic' (CheckIn t)
185intro :: Maybe Name -> Elab ()
186intro n = processTactic' (Intro n)
188forall :: Name -> Raw -> Elab ()
189forall n t = processTactic' (Forall n t)
191letbind :: Name -> Raw -> Raw -> Elab ()
192letbind n t v = processTactic' (LetBind n t v)
194rewrite :: Raw -> Elab ()
195rewrite tm = processTactic' (Rewrite tm)
197patvar :: Name -> Elab ()
198patvar n = do n' <- case n of
199 UN _ -> return n
200 MN _ _ -> unique_hole n
201 processTactic' (PatVar n')
203patbind :: Name -> Elab ()
204patbind n = processTactic' (PatBind n)
206focus :: Name -> Elab ()
207focus n = processTactic' (Focus n)
209movelast :: Name -> Elab ()
210movelast n = processTactic' (MoveLast n)
212defer :: Name -> Elab ()
213defer n = do n' <- unique_hole n
214 processTactic' (Defer n')
216instanceArg :: Name -> Elab ()
217instanceArg n = processTactic' (Instance n)
219proofstate :: Elab ()
220proofstate = processTactic' ProofState
222qed :: Elab Term
223qed = do processTactic' QED
224 ES p _ _ <- get
225 return (pterm p)
227undo :: Elab ()
228undo = processTactic' Undo
230prepare_apply :: Raw -> [Bool] -> Elab [Name]
231prepare_apply fn imps =
232 do ty <- get_type fn
233 ctxt <- get_context
234 env <- get_env
235 -- let claims = getArgs ty imps
236 claims <- doClaims (normalise ctxt env ty) imps []
237 ES p s prev <- get
238 -- reverse the claims we made so that args go left to right
239 let n = length (filter not imps)
240 let (h : hs) = holes p
241 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }) s prev)
242 return claims
243 where
244 doClaims (Bind n' (Pi t) sc) (i : is) claims =
245 do n <- unique_hole (mkMN n')
246 when (null claims) (start_unify n)
247 let sc' = instantiate (P Bound n t) sc
248 claim n (forget t)
249 when i (movelast n)
250 doClaims sc' is (n : claims)
251 doClaims t [] claims = return (reverse claims)
252 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
254 mkMN n@(MN _ _) = n
255 mkMN n@(UN x) = MN 0 x
257apply :: Raw -> [Bool] -> Elab [Name]
258apply fn imps =
259 do args <- prepare_apply fn imps
260 fill (raw_apply fn (map Var args))
261 -- *Don't* solve the arguments we're specifying by hand.
262 -- (remove from unified list before calling end_unify)
263 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
264 -- so do nothing
265 let dontunify = [] -- map fst (filter (not.snd) (zip args imps))
266 ES p s prev <- get
267 let (n, hs) = unified p
268 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
269 put (ES (p { unified = unify }) s prev)
270 end_unify
271 return args
273apply_elab :: Name -> [Maybe (Int, Elab ())] -> Elab ()
274apply_elab n args =
275 do ty <- get_type (Var n)
276 ctxt <- get_context
277 env <- get_env
278 claims <- doClaims (normalise ctxt env ty) args []
279 prep_fill n (map fst claims)
280 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
281 elabClaims [] False claims
282 complete_fill
283 end_unify
284 where
285 priOrder Nothing Nothing = EQ
286 priOrder Nothing _ = LT
287 priOrder _ Nothing = GT
288 priOrder (Just (x, _)) (Just (y, _)) = compare x y
290 doClaims (Bind n' (Pi t) sc) (i : is) claims =
291 do n <- unique_hole (mkMN n')
292 when (null claims) (start_unify n)
293 let sc' = instantiate (P Bound n t) sc
294 claim n (forget t)
295 doClaims sc' is ((n, i) : claims)
296 doClaims t [] claims = return (reverse claims)
297 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
299 elabClaims failed r []
300 | null failed = return ()
301 | otherwise = if r then elabClaims [] False failed
302 else return ()
303 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
304 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
305 | r = try (do ES p _ _ <- get
306 focus n; elaboration; elabClaims failed r xs)
307 (elabClaims (e : failed) r xs)
308 | otherwise = do ES p _ _ <- get
309 focus n; elaboration; elabClaims failed r xs
311 mkMN n@(MN _ _) = n
312 mkMN n@(UN x) = MN 0 x
314simple_app :: Elab () -> Elab () -> Elab ()
315simple_app fun arg =
316 do a <- unique_hole (MN 0 "a")
317 b <- unique_hole (MN 0 "b")
318 f <- unique_hole (MN 0 "f")
319 s <- unique_hole (MN 0 "s")
320 claim a (RSet 0)
321 claim b (RSet 0)
322 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
323 start_unify s
324 claim s (Var a)
325 prep_fill f [s]
326 -- try elaborating in both orders, since we might learn something useful
327 -- either way
328 try (do focus s; arg
329 focus f; fun)
330 (do focus f; fun
331 focus s; arg)
332 complete_fill
333 end_unify
335-- Abstract over an argument of unknown type, giving a name for the hole
336-- which we'll fill with the argument type too.
337arg :: Name -> Name -> Elab ()
338arg n tyhole = do ty <- unique_hole tyhole
339 claim ty (RSet 0)
340 forall n (Var ty)
342-- Try a tactic, if it fails, try another
343try :: Elab a -> Elab a -> Elab a
344try t1 t2 = do s <- get
345 case runStateT t1 s of
346 OK (v, s') -> do put s'
347 return v
348 _ -> do put s; t2