git.iko.soy/Idris-dev
on 01dc619 help sign in
Idris-dev/src/Core/Elaborate.hs
456 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
24import Util.Pretty
26-- I don't really want this here, but it's useful for the test shell
27data Command = Theorem Name Raw
28 | Eval Raw
29 | Quit
30 | Print Name
31 | Tac (Elab ())
33data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
34 deriving Show
36type Elab' aux a = StateT (ElabState aux) TC a
37type Elab a = Elab' () a
39proof :: ElabState aux -> ProofState
40proof (ES (p, _) _ _) = p
42saveState :: Elab' aux ()
43saveState = do e@(ES p s _) <- get
44 put (ES p s (Just e))
46loadState :: Elab' aux ()
47loadState = do (ES p s e) <- get
48 case e of
49 Just st -> put st
50 _ -> fail "Nothing to undo"
52erun :: FC -> Elab' aux a -> Elab' aux a
53erun f elab = do s <- get
54 case runStateT elab s of
55 OK (a, s') -> do put s'
56 return a
57 Error (At f e) -> lift $ Error (At f e)
58 Error e -> lift $ Error (At f e)
60runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
61runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
63execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
64execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
66initElaborator :: Name -> Context -> Type -> ProofState
67initElaborator = newProof
69elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
70elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty
71 (a, ES ps' str _) <- runElab d elab ps
72 return (a, str)
74updateAux :: (aux -> aux) -> Elab' aux ()
75updateAux f = do ES (ps, a) l p <- get
76 put (ES (ps, f a) l p)
78getAux :: Elab' aux aux
79getAux = do ES (ps, a) _ _ <- get
80 return a
82processTactic' t = do ES (p, a) logs prev <- get
83 (p', log) <- lift $ processTactic t p
84 put (ES (p', a) (logs ++ log) prev)
85 return ()
87-- Some handy gadgets for pulling out bits of state
89-- get the global context
90get_context :: Elab' aux Context
91get_context = do ES p _ _ <- get
92 return (context (fst p))
94-- get the proof term
95get_term :: Elab' aux Term
96get_term = do ES p _ _ <- get
97 return (pterm (fst p))
99-- get the local context at the currently in focus hole
100get_env :: Elab' aux Env
101get_env = do ES p _ _ <- get
102 lift $ envAtFocus (fst p)
104get_holes :: Elab' aux [Name]
105get_holes = do ES p _ _ <- get
106 return (holes (fst p))
108-- get the current goal type
109goal :: Elab' aux Type
110goal = do ES p _ _ <- get
111 b <- lift $ goalAtFocus (fst p)
112 return (binderTy b)
114-- Get the guess at the current hole, if there is one
115get_guess :: Elab' aux Type
116get_guess = do ES p _ _ <- get
117 b <- lift $ goalAtFocus (fst p)
118 case b of
119 Guess t v -> return v
120 _ -> fail "Not a guess"
122-- typecheck locally
123get_type :: Raw -> Elab' aux Type
124get_type tm = do ctxt <- get_context
125 env <- get_env
126 (val, ty) <- lift $ check ctxt env tm
127 return (finalise ty)
129-- get holes we've deferred for later definition
130get_deferred :: Elab' aux [Name]
131get_deferred = do ES p _ _ <- get
132 return (deferred (fst p))
134get_inj :: Elab' aux [(Term, Term, Term)]
135get_inj = do ES p _ _ <- get
136 return (injective (fst p))
138checkInjective :: (Term, Term, Term) -> Elab' aux ()
139checkInjective (tm, l, r) = if isInjective tm then return ()
140 else lift $ tfail (NotInjective tm l r)
142-- get instance argument names
143get_instances :: Elab' aux [Name]
144get_instances = do ES p _ _ <- get
145 return (instances (fst p))
147-- given a desired hole name, return a unique hole name
148unique_hole :: Name -> Elab' aux Name
149unique_hole n = do ES p _ _ <- get
150 let bs = bound_in (pterm (fst p)) ++ bound_in (ptype (fst p))
151 n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p) ++ bs)
152 return n'
153 where
154 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
155 where
156 bi (Let t v) = bound_in t ++ bound_in v
157 bi (Guess t v) = bound_in t ++ bound_in v
158 bi b = bound_in (binderTy b)
159 bound_in (App f a) = bound_in f ++ bound_in a
160 bound_in _ = []
162uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
163uniqueNameCtxt ctxt n hs
164 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
165 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs
166 | otherwise = return n
168elog :: String -> Elab' aux ()
169elog str = do ES p logs prev <- get
170 put (ES p (logs ++ str ++ "\n") prev)
172-- The primitives, from ProofState
174attack :: Elab' aux ()
175attack = processTactic' Attack
177claim :: Name -> Raw -> Elab' aux ()
178claim n t = processTactic' (Claim n t)
180exact :: Raw -> Elab' aux ()
181exact t = processTactic' (Exact t)
183fill :: Raw -> Elab' aux ()
184fill t = processTactic' (Fill t)
186prep_fill :: Name -> [Name] -> Elab' aux ()
187prep_fill n ns = processTactic' (PrepFill n ns)
189complete_fill :: Elab' aux ()
190complete_fill = processTactic' CompleteFill
192solve :: Elab' aux ()
193solve = processTactic' Solve
195start_unify :: Name -> Elab' aux ()
196start_unify n = processTactic' (StartUnify n)
198end_unify :: Elab' aux ()
199end_unify = processTactic' EndUnify
201regret :: Elab' aux ()
202regret = processTactic' Regret
204compute :: Elab' aux ()
205compute = processTactic' Compute
207eval_in :: Raw -> Elab' aux ()
208eval_in t = processTactic' (EvalIn t)
210check_in :: Raw -> Elab' aux ()
211check_in t = processTactic' (CheckIn t)
213intro :: Maybe Name -> Elab' aux ()
214intro n = processTactic' (Intro n)
216introTy :: Raw -> Maybe Name -> Elab' aux ()
217introTy ty n = processTactic' (IntroTy ty n)
219forall :: Name -> Raw -> Elab' aux ()
220forall n t = processTactic' (Forall n t)
222letbind :: Name -> Raw -> Raw -> Elab' aux ()
223letbind n t v = processTactic' (LetBind n t v)
225rewrite :: Raw -> Elab' aux ()
226rewrite tm = processTactic' (Rewrite tm)
228patvar :: Name -> Elab' aux ()
229patvar n = do env <- get_env
230 if (n `elem` map fst env) then do apply (Var n) []; solve
231 else do n' <- case n of
232 UN _ -> return n
233 MN _ _ -> unique_hole n
234 NS _ _ -> return n
235 processTactic' (PatVar n')
237patbind :: Name -> Elab' aux ()
238patbind n = processTactic' (PatBind n)
240focus :: Name -> Elab' aux ()
241focus n = processTactic' (Focus n)
243movelast :: Name -> Elab' aux ()
244movelast n = processTactic' (MoveLast n)
246defer :: Name -> Elab' aux ()
247defer n = do n' <- unique_hole n
248 processTactic' (Defer n')
250instanceArg :: Name -> Elab' aux ()
251instanceArg n = processTactic' (Instance n)
253proofstate :: Elab' aux ()
254proofstate = processTactic' ProofState
256reorder_claims :: Name -> Elab' aux ()
257reorder_claims n = processTactic' (Reorder n)
259qed :: Elab' aux Term
260qed = do processTactic' QED
261 ES p _ _ <- get
262 return (pterm (fst p))
264undo :: Elab' aux ()
265undo = processTactic' Undo
267prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]
268prepare_apply fn imps =
269 do ty <- get_type fn
270 ctxt <- get_context
271 env <- get_env
272 -- let claims = getArgs ty imps
273 claims <- mkClaims (normalise ctxt env ty) imps []
274 ES (p, a) s prev <- get
275 -- reverse the claims we made so that args go left to right
276 let n = length (filter not imps)
277 let (h : hs) = holes p
278 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
279-- case claims of
280-- [] -> return ()
281-- (h : _) -> reorder_claims h
282 return claims
283 where
284 mkClaims (Bind n' (Pi t) sc) (i : is) claims =
285 do n <- unique_hole (mkMN n')
286-- when (null claims) (start_unify n)
287 let sc' = instantiate (P Bound n t) sc
288 claim n (forget t)
289 when i (movelast n)
290 mkClaims sc' is (n : claims)
291 mkClaims t [] claims = return (reverse claims)
292 mkClaims _ _ _
293 | Var n <- fn
294 = do ctxt <- get_context
295 case lookupTy Nothing n ctxt of
296 [] -> lift $ tfail $ NoSuchVariable n
297 _ -> fail $ "Too many arguments for " ++ show fn
298 | otherwise = fail $ "Too many arguments for " ++ show fn
300 doClaim ((i, _), n, t) = do claim n t
301 when i (movelast n)
303 mkMN n@(MN _ _) = n
304 mkMN n@(UN x) = MN 0 x
305 mkMN (NS n xs) = NS (mkMN n) xs
307apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]
308apply fn imps =
309 do args <- prepare_apply fn (map fst imps)
310 fill (raw_apply fn (map Var args))
311 -- *Don't* solve the arguments we're specifying by hand.
312 -- (remove from unified list before calling end_unify)
313 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
314 -- so do nothing
315 ptm <- get_term
316 let dontunify = [] -- map fst (filter (not.snd) (zip args (map fst imps)))
317 ES (p, a) s prev <- get
318 let (n, hs) = unified p
319 let unify = (n, filter (\ (n, t) -> not (n `elem` dontunify)) hs)
320 put (ES (p { unified = unify }, a) s prev)
321 end_unify
322 return (map (updateUnify hs) args)
323 where updateUnify hs n = case lookup n hs of
324 Just (P _ t _) -> t
325 _ -> n
327apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
328apply2 fn elabs =
329 do args <- prepare_apply fn (map isJust elabs)
330 fill (raw_apply fn (map Var args))
331 elabArgs args elabs
332 ES (p, a) s prev <- get
333 let (n, hs) = unified p
334 end_unify
335 solve
336 where elabArgs [] [] = return ()
337 elabArgs (n:ns) (Just e:es) = do focus n; e
338 elabArgs ns es
339 elabArgs (n:ns) (_:es) = elabArgs ns es
341 isJust (Just _) = False
342 isJust _ = True
344apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
345apply_elab n args =
346 do ty <- get_type (Var n)
347 ctxt <- get_context
348 env <- get_env
349 claims <- doClaims (normalise ctxt env ty) args []
350 prep_fill n (map fst claims)
351 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
352 elabClaims [] False claims
353 complete_fill
354 end_unify
355 where
356 priOrder Nothing Nothing = EQ
357 priOrder Nothing _ = LT
358 priOrder _ Nothing = GT
359 priOrder (Just (x, _)) (Just (y, _)) = compare x y
361 doClaims (Bind n' (Pi t) sc) (i : is) claims =
362 do n <- unique_hole (mkMN n')
363 when (null claims) (start_unify n)
364 let sc' = instantiate (P Bound n t) sc
365 claim n (forget t)
366 doClaims sc' is ((n, i) : claims)
367 doClaims t [] claims = return (reverse claims)
368 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
370 elabClaims failed r []
371 | null failed = return ()
372 | otherwise = if r then elabClaims [] False failed
373 else return ()
374 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
375 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
376 | r = try (do ES p _ _ <- get
377 focus n; elaboration; elabClaims failed r xs)
378 (elabClaims (e : failed) r xs)
379 | otherwise = do ES p _ _ <- get
380 focus n; elaboration; elabClaims failed r xs
382 mkMN n@(MN _ _) = n
383 mkMN n@(UN x) = MN 0 x
384 mkMN (NS n ns) = NS (mkMN n) ns
386simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
387simple_app fun arg =
388 do a <- unique_hole (MN 0 "a")
389 b <- unique_hole (MN 0 "b")
390 f <- unique_hole (MN 0 "f")
391 s <- unique_hole (MN 0 "s")
392 claim a RSet
393 claim b RSet
394 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
395 start_unify s
396 claim s (Var a)
397 prep_fill f [s]
398 -- try elaborating in both orders, since we might learn something useful
399 -- either way
400 try (do focus s; arg
401 focus f; fun)
402 (do focus f; fun
403 focus s; arg)
404 complete_fill
405 end_unify
407-- Abstract over an argument of unknown type, giving a name for the hole
408-- which we'll fill with the argument type too.
409arg :: Name -> Name -> Elab' aux ()
410arg n tyhole = do ty <- unique_hole tyhole
411 claim ty RSet
412 forall n (Var ty)
414-- Try a tactic, if it fails, try another
415try :: Elab' aux a -> Elab' aux a -> Elab' aux a
416try t1 t2 = do s <- get
417 case runStateT t1 s of
418 OK (v, s') -> do put s'
419 return v
420 Error e1 -> do put s
421 case runStateT t2 s of
422 OK (v, s') -> do put s'; return v
423 Error e2 -> if score e1 > score e2
424 then lift (tfail e1)
425 else lift (tfail e2)
427-- Try a selection of tactics. Exactly one must work, all others must fail
428tryAll :: [(Elab' aux a, String)] -> Elab' aux a
429tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)
430 where
431 cantResolve :: Elab' aux a
432 cantResolve = fail $ "Couldn't resolve alternative: "
433 ++ showSep ", " (map snd xs)
435 tryAll' :: [Elab' aux a] -> -- successes
436 (Elab' aux a, Int) -> -- smallest failure
437 [Elab' aux a] -> -- still to try
438 Elab' aux a
439 tryAll' [res] _ [] = res
440 tryAll' (_:_) _ [] = cantResolve
441 tryAll' [] (f, _) [] = f
442 tryAll' cs f (x:xs) = do s <- get
443 case runStateT x s of
444 OK (v, s') -> tryAll' ((do put s'
445 return v):cs) f xs
446 Error err -> do put s
447 if (score err) < 100
448 then
449 tryAll' cs (better err f) xs
450 else
451 tryAll' [] (better err f) xs -- give up
453 better err (f, i) = let s = score err in
454 if (s >= i) then (lift (tfail err), s)
455 else (f, i)