git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Core/Elaborate.hs
435 lines 15 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
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 aux = ES (ProofState, aux) String (Maybe (ElabState aux))
32 deriving Show
33type Elab' aux a = StateT (ElabState aux) TC a
34type Elab a = Elab' () a
36proof :: ElabState aux -> ProofState
37proof (ES (p, _) _ _) = p
39saveState :: Elab' aux ()
40saveState = do e@(ES p s _) <- get
41 put (ES p s (Just e))
43loadState :: Elab' aux ()
44loadState = do (ES p s e) <- get
45 case e of
46 Just st -> put st
47 _ -> fail "Nothing to undo"
49erun :: FC -> Elab' aux a -> Elab' aux a
50erun f elab = do s <- get
51 case runStateT elab s of
52 OK (a, s') -> do put s'
53 return a
54 Error (At f e) -> lift $ Error (At f e)
55 Error e -> lift $ Error (At f e)
57runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
58runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
60execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
61execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
63initElaborator :: Name -> Context -> Type -> ProofState
64initElaborator = newProof
66elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
67elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty
68 (a, ES ps' str _) <- runElab d elab ps
69 return (a, str)
71updateAux :: (aux -> aux) -> Elab' aux ()
72updateAux f = do ES (ps, a) l p <- get
73 put (ES (ps, f a) l p)
75getAux :: Elab' aux aux
76getAux = do ES (ps, a) _ _ <- get
77 return a
79processTactic' t = do ES (p, a) logs prev <- get
80 (p', log) <- lift $ processTactic t p
81 put (ES (p', a) (logs ++ log) prev)
82 return ()
84-- Some handy gadgets for pulling out bits of state
86-- get the global context
87get_context :: Elab' aux Context
88get_context = do ES p _ _ <- get
89 return (context (fst p))
91-- get the proof term
92get_term :: Elab' aux Term
93get_term = do ES p _ _ <- get
94 return (pterm (fst p))
96-- get the local context at the currently in focus hole
97get_env :: Elab' aux Env
98get_env = do ES p _ _ <- get
99 lift $ envAtFocus (fst p)
101get_holes :: Elab' aux [Name]
102get_holes = do ES p _ _ <- get
103 return (holes (fst p))
105-- get the current goal type
106goal :: Elab' aux Type
107goal = do ES p _ _ <- get
108 b <- lift $ goalAtFocus (fst p)
109 return (binderTy b)
111-- typecheck locally
112get_type :: Raw -> Elab' aux Type
113get_type tm = do ctxt <- get_context
114 env <- get_env
115 (val, ty) <- lift $ check ctxt env tm
116 return (finalise ty)
118-- get holes we've deferred for later definition
119get_deferred :: Elab' aux [Name]
120get_deferred = do ES p _ _ <- get
121 return (deferred (fst p))
123get_inj :: Elab' aux [(Term, Term, Term)]
124get_inj = do ES p _ _ <- get
125 return (injective (fst p))
127checkInjective :: (Term, Term, Term) -> Elab' aux ()
128checkInjective (tm, l, r) = if isInjective tm then return ()
129 else lift $ tfail (NotInjective tm l r)
131-- get instance argument names
132get_instances :: Elab' aux [Name]
133get_instances = do ES p _ _ <- get
134 return (instances (fst p))
136-- given a desired hole name, return a unique hole name
137unique_hole :: Name -> Elab' aux Name
138unique_hole n = do ES p _ _ <- get
139 let bs = bound_in (pterm (fst p)) ++ bound_in (ptype (fst p))
140 n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs)
141 return n'
142 where
143 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
144 where
145 bi (Let t v) = bound_in t ++ bound_in v
146 bi (Guess t v) = bound_in t ++ bound_in v
147 bi b = bound_in (binderTy b)
148 bound_in (App f a) = bound_in f ++ bound_in a
149 bound_in _ = []
151uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
152uniqueNameCtxt ctxt n hs
153 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
154 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs
155 | otherwise = return n
157elog :: String -> Elab' aux ()
158elog str = do ES p logs prev <- get
159 put (ES p (logs ++ str ++ "\n") prev)
161-- The primitives, from ProofState
163attack :: Elab' aux ()
164attack = processTactic' Attack
166claim :: Name -> Raw -> Elab' aux ()
167claim n t = processTactic' (Claim n t)
169exact :: Raw -> Elab' aux ()
170exact t = processTactic' (Exact t)
172fill :: Raw -> Elab' aux ()
173fill t = processTactic' (Fill t)
175prep_fill :: Name -> [Name] -> Elab' aux ()
176prep_fill n ns = processTactic' (PrepFill n ns)
178complete_fill :: Elab' aux ()
179complete_fill = processTactic' CompleteFill
181solve :: Elab' aux ()
182solve = processTactic' Solve
184start_unify :: Name -> Elab' aux ()
185start_unify n = processTactic' (StartUnify n)
187end_unify :: Elab' aux ()
188end_unify = processTactic' EndUnify
190regret :: Elab' aux ()
191regret = processTactic' Regret
193compute :: Elab' aux ()
194compute = processTactic' Compute
196eval_in :: Raw -> Elab' aux ()
197eval_in t = processTactic' (EvalIn t)
199check_in :: Raw -> Elab' aux ()
200check_in t = processTactic' (CheckIn t)
202intro :: Maybe Name -> Elab' aux ()
203intro n = processTactic' (Intro n)
205introTy :: Raw -> Maybe Name -> Elab' aux ()
206introTy ty n = processTactic' (IntroTy ty n)
208forall :: Name -> Raw -> Elab' aux ()
209forall n t = processTactic' (Forall n t)
211letbind :: Name -> Raw -> Raw -> Elab' aux ()
212letbind n t v = processTactic' (LetBind n t v)
214rewrite :: Raw -> Elab' aux ()
215rewrite tm = processTactic' (Rewrite tm)
217patvar :: Name -> Elab' aux ()
218patvar n = do env <- get_env
219 if (n `elem` map fst env) then do apply (Var n) []; solve
220 else do n' <- case n of
221 UN _ -> return n
222 MN _ _ -> unique_hole n
223 NS _ _ -> return n
224 processTactic' (PatVar n')
226patbind :: Name -> Elab' aux ()
227patbind n = processTactic' (PatBind n)
229focus :: Name -> Elab' aux ()
230focus n = processTactic' (Focus n)
232movelast :: Name -> Elab' aux ()
233movelast n = processTactic' (MoveLast n)
235defer :: Name -> Elab' aux ()
236defer n = do n' <- unique_hole n
237 processTactic' (Defer n')
239instanceArg :: Name -> Elab' aux ()
240instanceArg n = processTactic' (Instance n)
242proofstate :: Elab' aux ()
243proofstate = processTactic' ProofState
245reorder_claims :: Name -> Elab' aux ()
246reorder_claims n = processTactic' (Reorder n)
248qed :: Elab' aux Term
249qed = do processTactic' QED
250 ES p _ _ <- get
251 return (pterm (fst p))
253undo :: Elab' aux ()
254undo = processTactic' Undo
256prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]
257prepare_apply fn imps =
258 do ty <- get_type fn
259 ctxt <- get_context
260 env <- get_env
261 -- let claims = getArgs ty imps
262 claims <- mkClaims (normalise ctxt env ty) imps []
263 ES (p, a) s prev <- get
264 -- reverse the claims we made so that args go left to right
265 let n = length (filter not imps)
266 let (h : hs) = holes p
267 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
268-- case claims of
269-- [] -> return ()
270-- (h : _) -> reorder_claims h
271 return claims
272 where
273 mkClaims (Bind n' (Pi t) sc) (i : is) claims =
274 do n <- unique_hole (mkMN n')
275-- when (null claims) (start_unify n)
276 let sc' = instantiate (P Bound n t) sc
277 claim n (forget t)
278 when i (movelast n)
279 mkClaims sc' is (n : claims)
280 mkClaims t [] claims = return (reverse claims)
281 mkClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show fn
283 doClaim ((i, _), n, t) = do claim n t
284 when i (movelast n)
286 mkMN n@(MN _ _) = n
287 mkMN n@(UN x) = MN 0 x
288 mkMN (NS n xs) = NS (mkMN n) xs
290apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]
291apply fn imps =
292 do args <- prepare_apply fn (map fst imps)
293 fill (raw_apply fn (map Var args))
294 -- *Don't* solve the arguments we're specifying by hand.
295 -- (remove from unified list before calling end_unify)
296 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
297 -- so do nothing
298 ptm <- get_term
299 let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))
300 ES (p, a) s prev <- get
301 let (n, hs) = unified p
302 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
303 put (ES (p { unified = unify }, a) s prev)
304 end_unify
305 return (map (updateUnify hs) args)
306 where updateUnify hs n = case lookup n hs of
307 Just (P _ t _) -> t
308 _ -> n
310apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
311apply2 fn elabs =
312 do args <- prepare_apply fn (map isJust elabs)
313 fill (raw_apply fn (map Var args))
314 elabArgs args elabs
315 ES (p, a) s prev <- get
316 let (n, hs) = unified p
317 end_unify
318 solve
319 where elabArgs [] [] = return ()
320 elabArgs (n:ns) (Just e:es) = do focus n; e
321 elabArgs ns es
322 elabArgs (n:ns) (_:es) = elabArgs ns es
324 isJust (Just _) = False
325 isJust _ = True
327apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
328apply_elab n args =
329 do ty <- get_type (Var n)
330 ctxt <- get_context
331 env <- get_env
332 claims <- doClaims (normalise ctxt env ty) args []
333 prep_fill n (map fst claims)
334 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
335 elabClaims [] False claims
336 complete_fill
337 end_unify
338 where
339 priOrder Nothing Nothing = EQ
340 priOrder Nothing _ = LT
341 priOrder _ Nothing = GT
342 priOrder (Just (x, _)) (Just (y, _)) = compare x y
344 doClaims (Bind n' (Pi t) sc) (i : is) claims =
345 do n <- unique_hole (mkMN n')
346 when (null claims) (start_unify n)
347 let sc' = instantiate (P Bound n t) sc
348 claim n (forget t)
349 doClaims sc' is ((n, i) : claims)
350 doClaims t [] claims = return (reverse claims)
351 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
353 elabClaims failed r []
354 | null failed = return ()
355 | otherwise = if r then elabClaims [] False failed
356 else return ()
357 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
358 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
359 | r = try (do ES p _ _ <- get
360 focus n; elaboration; elabClaims failed r xs)
361 (elabClaims (e : failed) r xs)
362 | otherwise = do ES p _ _ <- get
363 focus n; elaboration; elabClaims failed r xs
365 mkMN n@(MN _ _) = n
366 mkMN n@(UN x) = MN 0 x
367 mkMN (NS n ns) = NS (mkMN n) ns
369simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
370simple_app fun arg =
371 do a <- unique_hole (MN 0 "a")
372 b <- unique_hole (MN 0 "b")
373 f <- unique_hole (MN 0 "f")
374 s <- unique_hole (MN 0 "s")
375 claim a RSet
376 claim b RSet
377 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
378 start_unify s
379 claim s (Var a)
380 prep_fill f [s]
381 -- try elaborating in both orders, since we might learn something useful
382 -- either way
383 try (do focus s; arg
384 focus f; fun)
385 (do focus f; fun
386 focus s; arg)
387 complete_fill
388 end_unify
390-- Abstract over an argument of unknown type, giving a name for the hole
391-- which we'll fill with the argument type too.
392arg :: Name -> Name -> Elab' aux ()
393arg n tyhole = do ty <- unique_hole tyhole
394 claim ty RSet
395 forall n (Var ty)
397-- Try a tactic, if it fails, try another
398try :: Elab' aux a -> Elab' aux a -> Elab' aux a
399try t1 t2 = do s <- get
400 case runStateT t1 s of
401 OK (v, s') -> do put s'
402 return v
403 Error e1 -> do put s
404 case runStateT t2 s of
405 OK (v, s') -> do put s'; return v
406 Error e2 -> if score e1 > score e2
407 then lift (tfail e1)
408 else lift (tfail e2)
410-- Try a selection of tactics. Exactly one must work, all others must fail
411tryAll :: [(Elab' aux a, String)] -> Elab' aux a
412tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)
413 where
414 cantResolve :: Elab' aux a
415 cantResolve = fail $ "Couldn't resolve alternative: "
416 ++ showSep ", " (map snd xs)
418 tryAll' :: [Elab' aux a] -> -- successes
419 (Elab' aux a, Int) -> -- smallest failure
420 [Elab' aux a] -> -- still to try
421 Elab' aux a
422 tryAll' [res] _ [] = res
423 tryAll' (_:_) _ [] = cantResolve
424 tryAll' [] (f, _) [] = f
425 tryAll' cs f (x:xs) = do s <- get
426 case runStateT x s of
427 OK (v, s') -> tryAll' ((do put s'
428 return v):cs) f xs
429 Error err -> do put s
430 tryAll' cs (better err f) xs
432 better err (f, i) = let s = score err in
433 if (s >= i) then (lift (tfail err), s)
434 else (f, i)