git.iko.soy/Idris-dev
on cd8fe96 help sign in
Idris-dev/src/Core/Elaborate.hs
664 lines 23 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"
62errAt :: String -> Name -> Elab' aux a -> Elab' aux a
63errAt thing n elab = do s <- get
64 case runStateT elab s of
65 OK (a, s') -> do put s'
66 return a
67 Error (At f e) ->
68 lift $ Error (At f (Elaborating thing n e))
69 Error e -> lift $ Error (Elaborating thing n e)
71erun :: FC -> Elab' aux a -> Elab' aux a
72erun f elab = do s <- get
73 case runStateT elab s of
74 OK (a, s') -> do put s'
75 return a
76 Error (ProofSearchFail (At f e))
77 -> lift $ Error (ProofSearchFail (At f e))
78 Error (At f e) -> lift $ Error (At f e)
79 Error e -> lift $ Error (At f e)
81runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
82runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
84execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
85execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
87initElaborator :: Name -> Context -> Type -> ProofState
88initElaborator = newProof
90elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
91elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty
92 (a, ES ps' str _) <- runElab d elab ps
93 return (a, str)
95updateAux :: (aux -> aux) -> Elab' aux ()
96updateAux f = do ES (ps, a) l p <- get
97 put (ES (ps, f a) l p)
99getAux :: Elab' aux aux
100getAux = do ES (ps, a) _ _ <- get
101 return a
103unifyLog :: Bool -> Elab' aux ()
104unifyLog log = do ES (ps, a) l p <- get
105 put (ES (ps { unifylog = log }, a) l p)
107processTactic' t = do ES (p, a) logs prev <- get
108 (p', log) <- lift $ processTactic t p
109 put (ES (p', a) (logs ++ log) prev)
110 return ()
112-- Some handy gadgets for pulling out bits of state
114-- get the global context
115get_context :: Elab' aux Context
116get_context = do ES p _ _ <- get
117 return (context (fst p))
119-- update the context
120-- (should only be used for adding temporary definitions or all sorts of
121-- stuff could go wrong)
122set_context :: Context -> Elab' aux ()
123set_context ctxt = do ES (p, a) logs prev <- get
124 put (ES (p { context = ctxt }, a) logs prev)
126-- get the proof term
127get_term :: Elab' aux Term
128get_term = do ES p _ _ <- get
129 return (pterm (fst p))
131-- get the proof term
132update_term :: (Term -> Term) -> Elab' aux ()
133update_term f = do ES (p,a) logs prev <- get
134 let p' = p { pterm = f (pterm p) }
135 put (ES (p', a) logs prev)
137-- get the local context at the currently in focus hole
138get_env :: Elab' aux Env
139get_env = do ES p _ _ <- get
140 lift $ envAtFocus (fst p)
142get_holes :: Elab' aux [Name]
143get_holes = do ES p _ _ <- get
144 return (holes (fst p))
146get_probs :: Elab' aux Fails
147get_probs = do ES p _ _ <- get
148 return (problems (fst p))
150-- get the current goal type
151goal :: Elab' aux Type
152goal = do ES p _ _ <- get
153 b <- lift $ goalAtFocus (fst p)
154 return (binderTy b)
156-- Get the guess at the current hole, if there is one
157get_guess :: Elab' aux Type
158get_guess = do ES p _ _ <- get
159 b <- lift $ goalAtFocus (fst p)
160 case b of
161 Guess t v -> return v
162 _ -> fail "Not a guess"
164-- typecheck locally
165get_type :: Raw -> Elab' aux Type
166get_type tm = do ctxt <- get_context
167 env <- get_env
168 (val, ty) <- lift $ check ctxt env tm
169 return (finalise ty)
171get_type_val :: Raw -> Elab' aux (Term, Type)
172get_type_val tm = do ctxt <- get_context
173 env <- get_env
174 (val, ty) <- lift $ check ctxt env tm
175 return (finalise val, finalise ty)
177-- get holes we've deferred for later definition
178get_deferred :: Elab' aux [Name]
179get_deferred = do ES p _ _ <- get
180 return (deferred (fst p))
182checkInjective :: (Term, Term, Term) -> Elab' aux ()
183checkInjective (tm, l, r) = do ctxt <- get_context
184 if isInj ctxt tm then return ()
185 else lift $ tfail (NotInjective tm l r)
186 where isInj ctxt (P _ n _)
187 | isConName n ctxt = True
188 isInj ctxt (App f a) = isInj ctxt f
189 isInj ctxt (Constant _) = True
190 isInj ctxt (TType _) = True
191 isInj ctxt (Bind _ (Pi _) sc) = True
192 isInj ctxt _ = False
194-- get instance argument names
195get_instances :: Elab' aux [Name]
196get_instances = do ES p _ _ <- get
197 return (instances (fst p))
199-- given a desired hole name, return a unique hole name
200unique_hole = unique_hole' False
202unique_hole' :: Bool -> Name -> Elab' aux Name
203unique_hole' reusable n
204 = do ES p _ _ <- get
205 let bs = bound_in (pterm (fst p)) ++
206 bound_in (ptype (fst p))
207 n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p)
208 ++ bs ++ dontunify (fst p) ++ usedns (fst p))
209 ES (p, a) s u <- get
210 -- Hmm: Do we need this level of uniqueness?
211 let p' = p -- if reusable then p else p { usedns = n' : usedns p }
212 put (ES (p', a) s u)
213 return n'
214 where
215 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
216 where
217 bi (Let t v) = bound_in t ++ bound_in v
218 bi (Guess t v) = bound_in t ++ bound_in v
219 bi b = bound_in (binderTy b)
220 bound_in (App f a) = bound_in f ++ bound_in a
221 bound_in _ = []
223uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
224uniqueNameCtxt ctxt n hs
225 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
226 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs
227 | otherwise = return n
229elog :: String -> Elab' aux ()
230elog str = do ES p logs prev <- get
231 put (ES p (logs ++ str ++ "\n") prev)
233getLog :: Elab' aux String
234getLog = do ES p logs _ <- get
235 return logs
237-- The primitives, from ProofState
239attack :: Elab' aux ()
240attack = processTactic' Attack
242claim :: Name -> Raw -> Elab' aux ()
243claim n t = processTactic' (Claim n t)
245exact :: Raw -> Elab' aux ()
246exact t = processTactic' (Exact t)
248fill :: Raw -> Elab' aux ()
249fill t = processTactic' (Fill t)
251match_fill :: Raw -> Elab' aux ()
252match_fill t = processTactic' (MatchFill t)
254prep_fill :: Name -> [Name] -> Elab' aux ()
255prep_fill n ns = processTactic' (PrepFill n ns)
257complete_fill :: Elab' aux ()
258complete_fill = processTactic' CompleteFill
260solve :: Elab' aux ()
261solve = processTactic' Solve
263start_unify :: Name -> Elab' aux ()
264start_unify n = processTactic' (StartUnify n)
266end_unify :: Elab' aux ()
267end_unify = processTactic' EndUnify
269regret :: Elab' aux ()
270regret = processTactic' Regret
272compute :: Elab' aux ()
273compute = processTactic' Compute
275computeLet :: Name -> Elab' aux ()
276computeLet n = processTactic' (ComputeLet n)
278simplify :: Elab' aux ()
279simplify = processTactic' Simplify
281hnf_compute :: Elab' aux ()
282hnf_compute = processTactic' HNF_Compute
284eval_in :: Raw -> Elab' aux ()
285eval_in t = processTactic' (EvalIn t)
287check_in :: Raw -> Elab' aux ()
288check_in t = processTactic' (CheckIn t)
290intro :: Maybe Name -> Elab' aux ()
291intro n = processTactic' (Intro n)
293introTy :: Raw -> Maybe Name -> Elab' aux ()
294introTy ty n = processTactic' (IntroTy ty n)
296forall :: Name -> Raw -> Elab' aux ()
297forall n t = processTactic' (Forall n t)
299letbind :: Name -> Raw -> Raw -> Elab' aux ()
300letbind n t v = processTactic' (LetBind n t v)
302expandLet :: Name -> Term -> Elab' aux ()
303expandLet n v = processTactic' (ExpandLet n v)
305rewrite :: Raw -> Elab' aux ()
306rewrite tm = processTactic' (Rewrite tm)
308induction :: Name -> Elab' aux ()
309induction nm = processTactic' (Induction nm)
311equiv :: Raw -> Elab' aux ()
312equiv tm = processTactic' (Equiv tm)
314patvar :: Name -> Elab' aux ()
315patvar n = do env <- get_env
316 if (n `elem` map fst env) then do apply (Var n) []; solve
317 else do n' <- case n of
318 UN _ -> return n
319 MN _ _ -> unique_hole n
320 NS _ _ -> return n
321 processTactic' (PatVar n')
323patbind :: Name -> Elab' aux ()
324patbind n = processTactic' (PatBind n)
326focus :: Name -> Elab' aux ()
327focus n = processTactic' (Focus n)
329movelast :: Name -> Elab' aux ()
330movelast n = processTactic' (MoveLast n)
332matchProblems :: Elab' aux ()
333matchProblems = processTactic' MatchProblems
335unifyProblems :: Elab' aux ()
336unifyProblems = processTactic' UnifyProblems
338defer :: Name -> Elab' aux ()
339defer n = do n' <- unique_hole n
340 processTactic' (Defer n')
342deferType :: Name -> Raw -> [Name] -> Elab' aux ()
343deferType n ty ns = processTactic' (DeferType n ty ns)
345instanceArg :: Name -> Elab' aux ()
346instanceArg n = processTactic' (Instance n)
348setinj :: Name -> Elab' aux ()
349setinj n = processTactic' (SetInjective n)
351proofstate :: Elab' aux ()
352proofstate = processTactic' ProofState
354reorder_claims :: Name -> Elab' aux ()
355reorder_claims n = processTactic' (Reorder n)
357qed :: Elab' aux Term
358qed = do processTactic' QED
359 ES p _ _ <- get
360 return (pterm (fst p))
362undo :: Elab' aux ()
363undo = processTactic' Undo
365prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]
366prepare_apply fn imps =
367 do ty <- get_type fn
368 ctxt <- get_context
369 env <- get_env
370 -- let claims = getArgs ty imps
371 -- claims <- mkClaims (normalise ctxt env ty) imps []
372 claims <- mkClaims (finalise ty) imps [] (map fst env)
373 ES (p, a) s prev <- get
374 -- reverse the claims we made so that args go left to right
375 let n = length (filter not imps)
376 let (h : hs) = holes p
377 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
378-- case claims of
379-- [] -> return ()
380-- (h : _) -> reorder_claims h
381 return claims
382 where
383 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =
384 do let t = rebind hs t_in
385 n <- unique_hole (mkMN n')
386-- when (null claims) (start_unify n)
387 let sc' = instantiate (P Bound n t) sc
388-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show hs) $
389 claim n (forget t)
390 when i (movelast n)
391 mkClaims sc' is (n : claims) hs
392 mkClaims t [] claims _ = return (reverse claims)
393 mkClaims _ _ _ _
394 | Var n <- fn
395 = do ctxt <- get_context
396 case lookupTy n ctxt of
397 [] -> lift $ tfail $ NoSuchVariable n
398 _ -> lift $ tfail $ TooManyArguments n
399 | otherwise = fail $ "Too many arguments for " ++ show fn
401 doClaim ((i, _), n, t) = do claim n t
402 when i (movelast n)
404 mkMN n@(MN _ _) = n
405 mkMN n@(UN x) = MN 1000 x
406 mkMN n@(SN s) = MN 1000 (show s)
407 mkMN (NS n xs) = NS (mkMN n) xs
409 rebind hs (Bind n t sc)
410 | n `elem` hs = let n' = uniqueName n hs in
411 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)
412 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)
413 rebind hs (App f a) = App (rebind hs f) (rebind hs a)
414 rebind hs t = t
416apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]
417apply = apply' fill
418match_apply = apply' match_fill
420apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]
421apply' fillt fn imps =
422 do args <- prepare_apply fn (map fst imps)
423 env <- get_env
424 g <- goal
425 fillt (raw_apply fn (map Var args))
426 -- _Don't_ solve the arguments we're specifying by hand.
427 -- (remove from unified list before calling end_unify)
428 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
429 -- so do nothing
430 ptm <- get_term
431 hs <- get_holes
432 ES (p, a) s prev <- get
433 let dont = nub $ head hs : dontunify p ++
434 if null imps then [] -- do all we can
435 else
436 map fst (filter (not.snd) (zip args (map fst imps)))
437 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $
438 unified p
439 let unify = -- trace ("Not done " ++ show hs) $
440 dropGiven dont hunis hs
441 let notunify = -- trace ("Not done " ++ show hs) $
442 keepGiven dont hunis hs
443 put (ES (p { dontunify = dont, unified = (n, unify),
444 notunified = notunify ++ notunified p }, a) s prev)
445 ptm <- get_term
446 g <- goal
447-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $
448 end_unify
449 ptm <- get_term
450 return (map (updateUnify unify) args)
451 where updateUnify hs n = case lookup n hs of
452 Just (P _ t _) -> t
453 _ -> n
455apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
456apply2 fn elabs =
457 do args <- prepare_apply fn (map isJust elabs)
458 fill (raw_apply fn (map Var args))
459 elabArgs args elabs
460 ES (p, a) s prev <- get
461 let (n, hs) = unified p
462 end_unify
463 solve
464 where elabArgs [] [] = return ()
465 elabArgs (n:ns) (Just e:es) = do focus n; e
466 elabArgs ns es
467 elabArgs (n:ns) (_:es) = elabArgs ns es
469 isJust (Just _) = False
470 isJust _ = True
472apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
473apply_elab n args =
474 do ty <- get_type (Var n)
475 ctxt <- get_context
476 env <- get_env
477 claims <- doClaims (hnf ctxt env ty) args []
478 prep_fill n (map fst claims)
479 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
480 elabClaims [] False claims
481 complete_fill
482 end_unify
483 where
484 priOrder Nothing Nothing = EQ
485 priOrder Nothing _ = LT
486 priOrder _ Nothing = GT
487 priOrder (Just (x, _)) (Just (y, _)) = compare x y
489 doClaims (Bind n' (Pi t) sc) (i : is) claims =
490 do n <- unique_hole (mkMN n')
491 when (null claims) (start_unify n)
492 let sc' = instantiate (P Bound n t) sc
493 claim n (forget t)
494 case i of
495 Nothing -> return ()
496 Just _ -> -- don't solve by unification as there is an explicit value
497 do ES (p, a) s prev <- get
498 put (ES (p { dontunify = n : dontunify p }, a) s prev)
499 doClaims sc' is ((n, i) : claims)
500 doClaims t [] claims = return (reverse claims)
501 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
503 elabClaims failed r []
504 | null failed = return ()
505 | otherwise = if r then elabClaims [] False failed
506 else return ()
507 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
508 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
509 | r = try (do ES p _ _ <- get
510 focus n; elaboration; elabClaims failed r xs)
511 (elabClaims (e : failed) r xs)
512 | otherwise = do ES p _ _ <- get
513 focus n; elaboration; elabClaims failed r xs
515 mkMN n@(MN _ _) = n
516 mkMN n@(UN x) = MN 1000 x
517 mkMN (NS n ns) = NS (mkMN n) ns
519-- If the goal is not a Pi-type, invent some names and make it a pi type
520checkPiGoal :: Name -> Elab' aux ()
521checkPiGoal n
522 = do g <- goal
523 case g of
524 Bind _ (Pi _) _ -> return ()
525 _ -> do a <- unique_hole (MN 0 "pargTy")
526 b <- unique_hole (MN 0 "pretTy")
527 f <- unique_hole (MN 0 "pf")
528 claim a RType
529 claim b RType
530 claim f (RBind n (Pi (Var a)) (Var b))
531 movelast a
532 movelast b
533 fill (Var f)
534 solve
535 focus f
537simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
538simple_app fun arg appstr =
539 do a <- unique_hole (MN 0 "argTy")
540 b <- unique_hole (MN 0 "retTy")
541 f <- unique_hole (MN 0 "f")
542 s <- unique_hole (MN 0 "s")
543 claim a RType
544 claim b RType
545 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
546 tm <- get_term
547 start_unify s
548 claim s (Var a)
549 prep_fill f [s]
550 focus f; fun
551 focus s; arg
552 tm <- get_term
553 ps <- get_probs
554 complete_fill
555 hs <- get_holes
556 env <- get_env
557 -- We don't need a and b in the hole queue any more since they were
558 -- just for checking f, so discard them if they are still there.
559 -- If they haven't been solved, regret will fail
560 when (a `elem` hs) $ do focus a; regretWith (CantInferType appstr)
561 when (b `elem` hs) $ do focus b; regretWith (CantInferType appstr)
562 end_unify
563 where regretWith err = try regret
564 (lift $ tfail err)
566-- Abstract over an argument of unknown type, giving a name for the hole
567-- which we'll fill with the argument type too.
568arg :: Name -> Name -> Elab' aux ()
569arg n tyhole = do ty <- unique_hole tyhole
570 claim ty RType
571 forall n (Var ty)
573-- try a tactic, if it adds any unification problem, return an error
574no_errors :: Elab' aux () -> Elab' aux ()
575no_errors tac
576 = do ps <- get_probs
577 tac
578 ps' <- get_probs
579 if (length ps' > length ps) then
580 case reverse ps' of
581 ((x,y,env,err) : _) ->
582 let env' = map (\(x, b) -> (x, binderTy b)) env in
583 lift $ tfail $ CantUnify False x y err env' 0
584 else return ()
586-- Try a tactic, if it fails, try another
587try :: Elab' aux a -> Elab' aux a -> Elab' aux a
588try t1 t2 = try' t1 t2 False
590try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
591try' t1 t2 proofSearch
592 = do s <- get
593 ps <- get_probs
594 case prunStateT 999999 False ps t1 s of
595 OK ((v, _), s') -> do put s'
596 return v
597 Error e1 -> if recoverableErr e1 then
598 do case runStateT t2 s of
599 OK (v, s') -> do put s'; return v
600 Error e2 -> if score e1 >= score e2
601 then lift (tfail e1)
602 else lift (tfail e2)
603 else lift (tfail e1)
604 where recoverableErr err@(CantUnify r _ _ _ _ _)
605 = -- traceWhen r (show err) $
606 r || proofSearch
607 recoverableErr (ProofSearchFail _) = False
608 recoverableErr _ = True
610tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
611tryWhen True a b = try a b
612tryWhen False a b = a
615-- Try a selection of tactics. Exactly one must work, all others must fail
616tryAll :: [(Elab' aux a, String)] -> Elab' aux a
617tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)
618 where
619 cantResolve :: Elab' aux a
620 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
622 tryAll' :: [Elab' aux a] -> -- successes
623 Int -> -- most problems
624 (Elab' aux a, Int) -> -- smallest failure
625 [Elab' aux a] -> -- still to try
626 Elab' aux a
627 tryAll' [res] pmax _ [] = res
628 tryAll' (_:_) pmax _ [] = cantResolve
629 tryAll' [] pmax (f, _) [] = f
630 tryAll' cs pmax f (x:xs)
631 = do s <- get
632 ps <- get_probs
633 case prunStateT pmax True ps x s of
634 OK ((v, newps), s') ->
635 do let cs' = if (newps < pmax)
636 then [do put s'; return v]
637 else (do put s'; return v) : cs
638 tryAll' cs' newps f xs
639 Error err -> do put s
640 if (score err) < 100
641 then tryAll' cs pmax (better err f) xs
642 else tryAll' [] pmax (better err f) xs -- give up
645 better err (f, i) = let s = score err in
646 if (s >= i) then (lift (tfail err), s)
647 else (f, i)
649prunStateT pmax zok ps x s
650 = case runStateT x s of
651 OK (v, s'@(ES (p, _) _ _)) ->
652 let newps = length (problems p) - length ps
653 newpmax = if newps < 0 then 0 else newps in
654 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
655 then case reverse (problems p) of
656 ((_,_,_,e):_) -> Error e
657 else OK ((v, newpmax), s')
658 Error e -> Error e
660qshow :: Fails -> String
661qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)
663dumpprobs [] = ""
664dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es