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