git.iko.soy/Idris-dev
on 25aef32 help sign in
Idris-dev/src/Core/Elaborate.hs
606 lines 21 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
18import Core.Unify
20import Control.Monad.State
21import Data.Char
22import Data.List
23import Debug.Trace
25import Util.Pretty
27-- I don't really want this here, but it's useful for the test shell
28data Command = Theorem Name Raw
29 | Eval Raw
30 | Quit
31 | Print Name
32 | Tac (Elab ())
34data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
35 deriving Show
37type Elab' aux a = StateT (ElabState aux) TC a
38type Elab a = Elab' () a
40proof :: ElabState aux -> ProofState
41proof (ES (p, _) _ _) = p
43-- Insert a 'proofSearchFail' error if necessary to shortcut any further
44-- fruitless searching
45proofFail :: Elab' aux a -> Elab' aux a
46proofFail e = do s <- get
47 case runStateT e s of
48 OK (a, s') -> do put s'
49 return a
50 Error err -> lift $ Error (ProofSearchFail err)
52saveState :: Elab' aux ()
53saveState = do e@(ES p s _) <- get
54 put (ES p s (Just e))
56loadState :: Elab' aux ()
57loadState = do (ES p s e) <- get
58 case e of
59 Just st -> put st
60 _ -> fail "Nothing to undo"
62erun :: FC -> Elab' aux a -> Elab' aux a
63erun f elab = do s <- get
64 case runStateT elab s of
65 OK (a, s') -> do put s'
66 return a
67 Error (ProofSearchFail (At f e))
68 -> lift $ Error (ProofSearchFail (At f e))
69 Error (At f e) -> lift $ Error (At f e)
70 Error e -> lift $ Error (At f e)
72runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
73runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
75execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
76execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
78initElaborator :: Name -> Context -> Type -> ProofState
79initElaborator = newProof
81elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
82elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty
83 (a, ES ps' str _) <- runElab d elab ps
84 return (a, str)
86updateAux :: (aux -> aux) -> Elab' aux ()
87updateAux f = do ES (ps, a) l p <- get
88 put (ES (ps, f a) l p)
90getAux :: Elab' aux aux
91getAux = do ES (ps, a) _ _ <- get
92 return a
94processTactic' t = do ES (p, a) logs prev <- get
95 (p', log) <- lift $ processTactic t p
96 put (ES (p', a) (logs ++ log) prev)
97 return ()
99-- Some handy gadgets for pulling out bits of state
101-- get the global context
102get_context :: Elab' aux Context
103get_context = do ES p _ _ <- get
104 return (context (fst p))
106-- update the context
107-- (should only be used for adding temporary definitions or all sorts of
108-- stuff could go wrong)
109set_context :: Context -> Elab' aux ()
110set_context ctxt = do ES (p, a) logs prev <- get
111 put (ES (p { context = ctxt }, a) logs prev)
113-- get the proof term
114get_term :: Elab' aux Term
115get_term = do ES p _ _ <- get
116 return (pterm (fst p))
118-- get the proof term
119update_term :: (Term -> Term) -> Elab' aux ()
120update_term f = do ES (p,a) logs prev <- get
121 let p' = p { pterm = f (pterm p) }
122 put (ES (p', a) logs prev)
124-- get the local context at the currently in focus hole
125get_env :: Elab' aux Env
126get_env = do ES p _ _ <- get
127 lift $ envAtFocus (fst p)
129get_holes :: Elab' aux [Name]
130get_holes = do ES p _ _ <- get
131 return (holes (fst p))
133get_probs :: Elab' aux Fails
134get_probs = do ES p _ _ <- get
135 return (problems (fst p))
137-- get the current goal type
138goal :: Elab' aux Type
139goal = do ES p _ _ <- get
140 b <- lift $ goalAtFocus (fst p)
141 return (binderTy b)
143-- Get the guess at the current hole, if there is one
144get_guess :: Elab' aux Type
145get_guess = do ES p _ _ <- get
146 b <- lift $ goalAtFocus (fst p)
147 case b of
148 Guess t v -> return v
149 _ -> fail "Not a guess"
151-- typecheck locally
152get_type :: Raw -> Elab' aux Type
153get_type tm = do ctxt <- get_context
154 env <- get_env
155 (val, ty) <- lift $ check ctxt env tm
156 return (finalise ty)
158get_type_val :: Raw -> Elab' aux (Term, Type)
159get_type_val tm = do ctxt <- get_context
160 env <- get_env
161 (val, ty) <- lift $ check ctxt env tm
162 return (finalise val, finalise ty)
164-- get holes we've deferred for later definition
165get_deferred :: Elab' aux [Name]
166get_deferred = do ES p _ _ <- get
167 return (deferred (fst p))
169checkInjective :: (Term, Term, Term) -> Elab' aux ()
170checkInjective (tm, l, r) = do ctxt <- get_context
171 if isInj ctxt tm then return ()
172 else lift $ tfail (NotInjective tm l r)
173 where isInj ctxt (P _ n _)
174 | isConName Nothing n ctxt = True
175 isInj ctxt (App f a) = isInj ctxt f
176 isInj ctxt (Constant _) = True
177 isInj ctxt (TType _) = True
178 isInj ctxt (Bind _ (Pi _) sc) = True
179 isInj ctxt _ = False
181-- get instance argument names
182get_instances :: Elab' aux [Name]
183get_instances = do ES p _ _ <- get
184 return (instances (fst p))
186-- given a desired hole name, return a unique hole name
187unique_hole = unique_hole' False
189unique_hole' :: Bool -> Name -> Elab' aux Name
190unique_hole' reusable n
191 = do ES p _ _ <- get
192 let bs = bound_in (pterm (fst p)) ++
193 bound_in (ptype (fst p))
194 n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p)
195 ++ bs ++ dontunify (fst p) ++ usedns (fst p))
196 ES (p, a) s u <- get
197 -- Hmm: Do we need this level of uniqueness?
198 let p' = p -- if reusable then p else p { usedns = n' : usedns p }
199 put (ES (p', a) s u)
200 return n'
201 where
202 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
203 where
204 bi (Let t v) = bound_in t ++ bound_in v
205 bi (Guess t v) = bound_in t ++ bound_in v
206 bi b = bound_in (binderTy b)
207 bound_in (App f a) = bound_in f ++ bound_in a
208 bound_in _ = []
210uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
211uniqueNameCtxt ctxt n hs
212 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
213 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs
214 | otherwise = return n
216elog :: String -> Elab' aux ()
217elog str = do ES p logs prev <- get
218 put (ES p (logs ++ str ++ "\n") prev)
220getLog :: Elab' aux String
221getLog = do ES p logs _ <- get
222 return logs
224-- The primitives, from ProofState
226attack :: Elab' aux ()
227attack = processTactic' Attack
229claim :: Name -> Raw -> Elab' aux ()
230claim n t = processTactic' (Claim n t)
232exact :: Raw -> Elab' aux ()
233exact t = processTactic' (Exact t)
235fill :: Raw -> Elab' aux ()
236fill t = processTactic' (Fill t)
238prep_fill :: Name -> [Name] -> Elab' aux ()
239prep_fill n ns = processTactic' (PrepFill n ns)
241complete_fill :: Elab' aux ()
242complete_fill = processTactic' CompleteFill
244solve :: Elab' aux ()
245solve = processTactic' Solve
247start_unify :: Name -> Elab' aux ()
248start_unify n = processTactic' (StartUnify n)
250end_unify :: Elab' aux ()
251end_unify = processTactic' EndUnify
253regret :: Elab' aux ()
254regret = processTactic' Regret
256compute :: Elab' aux ()
257compute = processTactic' Compute
259hnf_compute :: Elab' aux ()
260hnf_compute = processTactic' HNF_Compute
262eval_in :: Raw -> Elab' aux ()
263eval_in t = processTactic' (EvalIn t)
265check_in :: Raw -> Elab' aux ()
266check_in t = processTactic' (CheckIn t)
268intro :: Maybe Name -> Elab' aux ()
269intro n = processTactic' (Intro n)
271introTy :: Raw -> Maybe Name -> Elab' aux ()
272introTy ty n = processTactic' (IntroTy ty n)
274forall :: Name -> Raw -> Elab' aux ()
275forall n t = processTactic' (Forall n t)
277letbind :: Name -> Raw -> Raw -> Elab' aux ()
278letbind n t v = processTactic' (LetBind n t v)
280rewrite :: Raw -> Elab' aux ()
281rewrite tm = processTactic' (Rewrite tm)
283patvar :: Name -> Elab' aux ()
284patvar n = do env <- get_env
285 if (n `elem` map fst env) then do apply (Var n) []; solve
286 else do n' <- case n of
287 UN _ -> return n
288 MN _ _ -> unique_hole n
289 NS _ _ -> return n
290 processTactic' (PatVar n')
292patbind :: Name -> Elab' aux ()
293patbind n = processTactic' (PatBind n)
295focus :: Name -> Elab' aux ()
296focus n = processTactic' (Focus n)
298movelast :: Name -> Elab' aux ()
299movelast n = processTactic' (MoveLast n)
301defer :: Name -> Elab' aux ()
302defer n = do n' <- unique_hole n
303 processTactic' (Defer n')
305deferType :: Name -> Raw -> [Name] -> Elab' aux ()
306deferType n ty ns = processTactic' (DeferType n ty ns)
308instanceArg :: Name -> Elab' aux ()
309instanceArg n = processTactic' (Instance n)
311setinj :: Name -> Elab' aux ()
312setinj n = processTactic' (SetInjective n)
314proofstate :: Elab' aux ()
315proofstate = processTactic' ProofState
317reorder_claims :: Name -> Elab' aux ()
318reorder_claims n = processTactic' (Reorder n)
320qed :: Elab' aux Term
321qed = do processTactic' QED
322 ES p _ _ <- get
323 return (pterm (fst p))
325undo :: Elab' aux ()
326undo = processTactic' Undo
328prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]
329prepare_apply fn imps =
330 do ty <- get_type fn
331 ctxt <- get_context
332 env <- get_env
333 -- let claims = getArgs ty imps
334 -- claims <- mkClaims (normalise ctxt env ty) imps []
335 claims <- mkClaims (finalise ty) imps [] (map fst env)
336 ES (p, a) s prev <- get
337 -- reverse the claims we made so that args go left to right
338 let n = length (filter not imps)
339 let (h : hs) = holes p
340 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
341-- case claims of
342-- [] -> return ()
343-- (h : _) -> reorder_claims h
344 return claims
345 where
346 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =
347 do let t = rebind hs t_in
348 n <- unique_hole (mkMN n')
349-- when (null claims) (start_unify n)
350 let sc' = instantiate (P Bound n t) sc
351-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show hs) $
352 claim n (forget t)
353 when i (movelast n)
354 mkClaims sc' is (n : claims) hs
355 mkClaims t [] claims _ = return (reverse claims)
356 mkClaims _ _ _ _
357 | Var n <- fn
358 = do ctxt <- get_context
359 case lookupTy Nothing n ctxt of
360 [] -> lift $ tfail $ NoSuchVariable n
361 _ -> fail $ "Too many arguments for " ++ show fn
362 | otherwise = fail $ "Too many arguments for " ++ show fn
364 doClaim ((i, _), n, t) = do claim n t
365 when i (movelast n)
367 mkMN n@(MN _ _) = n
368 mkMN n@(UN x) = MN 1000 x
369 mkMN (NS n xs) = NS (mkMN n) xs
371 rebind hs (Bind n t sc)
372 | n `elem` hs = let n' = uniqueName n hs in
373 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)
374 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)
375 rebind hs (App f a) = App (rebind hs f) (rebind hs a)
376 rebind hs t = t
378apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]
379apply fn imps =
380 do args <- prepare_apply fn (map fst imps)
381 fill (raw_apply fn (map Var args))
382 -- _Don't_ solve the arguments we're specifying by hand.
383 -- (remove from unified list before calling end_unify)
384 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
385 -- so do nothing
386 ptm <- get_term
387 hs <- get_holes
388 ES (p, a) s prev <- get
389 let dont = nub $ head hs : dontunify p ++
390 if null imps then [] -- do all we can
391 else
392 map fst (filter (not.snd) (zip args (map fst imps)))
393 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $
394 unified p
395 let unify = -- trace ("Not done " ++ show hs) $
396 dropGiven dont hunis hs
397 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)
398 ptm <- get_term
399 g <- goal
400-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $
401 end_unify
402 ptm <- get_term
403 return (map (updateUnify unify) args)
404 where updateUnify hs n = case lookup n hs of
405 Just (P _ t _) -> t
406 _ -> n
408apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
409apply2 fn elabs =
410 do args <- prepare_apply fn (map isJust elabs)
411 fill (raw_apply fn (map Var args))
412 elabArgs args elabs
413 ES (p, a) s prev <- get
414 let (n, hs) = unified p
415 end_unify
416 solve
417 where elabArgs [] [] = return ()
418 elabArgs (n:ns) (Just e:es) = do focus n; e
419 elabArgs ns es
420 elabArgs (n:ns) (_:es) = elabArgs ns es
422 isJust (Just _) = False
423 isJust _ = True
425apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
426apply_elab n args =
427 do ty <- get_type (Var n)
428 ctxt <- get_context
429 env <- get_env
430 claims <- doClaims (hnf ctxt env ty) args []
431 prep_fill n (map fst claims)
432 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
433 elabClaims [] False claims
434 complete_fill
435 end_unify
436 where
437 priOrder Nothing Nothing = EQ
438 priOrder Nothing _ = LT
439 priOrder _ Nothing = GT
440 priOrder (Just (x, _)) (Just (y, _)) = compare x y
442 doClaims (Bind n' (Pi t) sc) (i : is) claims =
443 do n <- unique_hole (mkMN n')
444 when (null claims) (start_unify n)
445 let sc' = instantiate (P Bound n t) sc
446 claim n (forget t)
447 case i of
448 Nothing -> return ()
449 Just _ -> -- don't solve by unification as there is an explicit value
450 do ES (p, a) s prev <- get
451 put (ES (p { dontunify = n : dontunify p }, a) s prev)
452 doClaims sc' is ((n, i) : claims)
453 doClaims t [] claims = return (reverse claims)
454 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
456 elabClaims failed r []
457 | null failed = return ()
458 | otherwise = if r then elabClaims [] False failed
459 else return ()
460 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
461 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
462 | r = try (do ES p _ _ <- get
463 focus n; elaboration; elabClaims failed r xs)
464 (elabClaims (e : failed) r xs)
465 | otherwise = do ES p _ _ <- get
466 focus n; elaboration; elabClaims failed r xs
468 mkMN n@(MN _ _) = n
469 mkMN n@(UN x) = MN 1000 x
470 mkMN (NS n ns) = NS (mkMN n) ns
472-- If the goal is not a Pi-type, invent some names and make it a pi type
473checkPiGoal :: Elab' aux ()
474checkPiGoal = do g <- goal
475 case g of
476 Bind _ (Pi _) _ -> return ()
477 _ -> do a <- unique_hole (MN 0 "argTy")
478 b <- unique_hole (MN 0 "retTy")
479 f <- unique_hole (MN 0 "f")
480 claim a RType
481 claim b RType
482 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
483 movelast a
484 movelast b
485 fill (Var f)
486 solve
487 focus f
489simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
490simple_app fun arg =
491 do a <- unique_hole (MN 0 "argTy")
492 b <- unique_hole (MN 0 "retTy")
493 f <- unique_hole (MN 0 "f")
494 s <- unique_hole (MN 0 "s")
495 claim a RType
496 claim b RType
497 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
498 tm <- get_term
499 start_unify s
500 claim s (Var a)
501 prep_fill f [s]
502 -- try elaborating in both orders, since we might learn something useful
503 -- either way
504-- try (do focus s; arg
505-- focus f; fun)
506-- (do focus f; fun
507-- focus s; arg)
508 focus f; fun
509 focus s; arg
510 tm <- get_term
511 ps <- get_probs
512 complete_fill
513 hs <- get_holes
514 -- We don't need a and b in the hole queue any more since they were just for
515 -- checking f, so discard them if they are still there. If they haven't been solved,
516 -- regret will fail
517 when (a `elem` hs) $ do focus a; regret
518 when (b `elem` hs) $ do focus b; regret
519 end_unify
521-- Abstract over an argument of unknown type, giving a name for the hole
522-- which we'll fill with the argument type too.
523arg :: Name -> Name -> Elab' aux ()
524arg n tyhole = do ty <- unique_hole tyhole
525 claim ty RType
526 forall n (Var ty)
528-- Try a tactic, if it fails, try another
529try :: Elab' aux a -> Elab' aux a -> Elab' aux a
530try t1 t2 = try' t1 t2 False
532try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
533try' t1 t2 proofSearch
534 = do s <- get
535 ps <- get_probs
536 case prunStateT 999999 False ps t1 s of
537 OK ((v, _), s') -> do put s'
538 return v
539 Error e1 -> if recoverableErr e1 then
540 do case runStateT t2 s of
541 OK (v, s') -> do put s'; return v
542 Error e2 -> if score e1 >= score e2
543 then lift (tfail e1)
544 else lift (tfail e2)
545 else lift (tfail e1)
546 where recoverableErr err@(CantUnify r _ _ _ _ _)
547 = -- traceWhen r (show err) $
548 r || proofSearch
549 recoverableErr (ProofSearchFail _) = False
550 recoverableErr _ = True
552tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
553tryWhen True a b = try a b
554tryWhen False a b = a
557-- Try a selection of tactics. Exactly one must work, all others must fail
558tryAll :: [(Elab' aux a, String)] -> Elab' aux a
559tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)
560 where
561 cantResolve :: Elab' aux a
562 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
564 tryAll' :: [Elab' aux a] -> -- successes
565 Int -> -- most problems
566 (Elab' aux a, Int) -> -- smallest failure
567 [Elab' aux a] -> -- still to try
568 Elab' aux a
569 tryAll' [res] pmax _ [] = res
570 tryAll' (_:_) pmax _ [] = cantResolve
571 tryAll' [] pmax (f, _) [] = f
572 tryAll' cs pmax f (x:xs)
573 = do s <- get
574 ps <- get_probs
575 case prunStateT pmax True ps x s of
576 OK ((v, newps), s') ->
577 do let cs' = if (newps < pmax)
578 then [do put s'; return v]
579 else (do put s'; return v) : cs
580 tryAll' cs' newps f xs
581 Error err -> do put s
582 if (score err) < 100
583 then tryAll' cs pmax (better err f) xs
584 else tryAll' [] pmax (better err f) xs -- give up
587 better err (f, i) = let s = score err in
588 if (s >= i) then (lift (tfail err), s)
589 else (f, i)
591prunStateT pmax zok ps x s
592 = case runStateT x s of
593 OK (v, s'@(ES (p, _) _ _)) ->
594 let newps = length (problems p) - length ps
595 newpmax = if newps < 0 then 0 else newps in
596 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
597 then case reverse (problems p) of
598 ((_,_,_,e):_) -> Error e
599 else OK ((v, newpmax), s')
600 Error e -> Error e
602qshow :: Fails -> String
603qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
605dumpprobs [] = ""
606dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es