git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Core/Elaborate.hs
514 lines 18 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 proof term
100update_term :: (Term -> Term) -> Elab' aux ()
101update_term f = do ES (p,a) logs prev <- get
102 let p' = p { pterm = f (pterm p) }
103 put (ES (p', a) logs prev)
105-- get the local context at the currently in focus hole
106get_env :: Elab' aux Env
107get_env = do ES p _ _ <- get
108 lift $ envAtFocus (fst p)
110get_holes :: Elab' aux [Name]
111get_holes = do ES p _ _ <- get
112 return (holes (fst p))
114-- get the current goal type
115goal :: Elab' aux Type
116goal = do ES p _ _ <- get
117 b <- lift $ goalAtFocus (fst p)
118 return (binderTy b)
120-- Get the guess at the current hole, if there is one
121get_guess :: Elab' aux Type
122get_guess = do ES p _ _ <- get
123 b <- lift $ goalAtFocus (fst p)
124 case b of
125 Guess t v -> return v
126 _ -> fail "Not a guess"
128-- typecheck locally
129get_type :: Raw -> Elab' aux Type
130get_type tm = do ctxt <- get_context
131 env <- get_env
132 (val, ty) <- lift $ check ctxt env tm
133 return (finalise ty)
135-- get holes we've deferred for later definition
136get_deferred :: Elab' aux [Name]
137get_deferred = do ES p _ _ <- get
138 return (deferred (fst p))
140get_inj :: Elab' aux [(Term, Term, Term)]
141get_inj = do ES p _ _ <- get
142 return (injective (fst p))
144checkInjective :: (Term, Term, Term) -> Elab' aux ()
145checkInjective (tm, l, r) = if isInjective tm then return ()
146 else lift $ tfail (NotInjective tm l r)
148-- get instance argument names
149get_instances :: Elab' aux [Name]
150get_instances = do ES p _ _ <- get
151 return (instances (fst p))
153-- given a desired hole name, return a unique hole name
154unique_hole = unique_hole' False
156unique_hole' :: Bool -> Name -> Elab' aux Name
157unique_hole' reusable n
158 = do ES p _ _ <- get
159 let bs = bound_in (pterm (fst p)) ++
160 bound_in (ptype (fst p))
161 n' <- uniqueNameCtxt (context (fst p)) n (holes (fst p)
162 ++ bs ++ dontunify (fst p) ++ usedns (fst p))
163 ES (p, a) s u <- get
164 -- Hmm: Do we need this level of uniqueness?
165 let p' = p -- if reusable then p else p { usedns = n' : usedns p }
166 put (ES (p', a) s u)
167 return n'
168 where
169 bound_in (Bind n b sc) = n : bi b ++ bound_in sc
170 where
171 bi (Let t v) = bound_in t ++ bound_in v
172 bi (Guess t v) = bound_in t ++ bound_in v
173 bi b = bound_in (binderTy b)
174 bound_in (App f a) = bound_in f ++ bound_in a
175 bound_in _ = []
177uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name
178uniqueNameCtxt ctxt n hs
179 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
180 | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs
181 | otherwise = return n
183elog :: String -> Elab' aux ()
184elog str = do ES p logs prev <- get
185 put (ES p (logs ++ str ++ "\n") prev)
187getLog :: Elab' aux String
188getLog = do ES p logs _ <- get
189 return logs
191-- The primitives, from ProofState
193attack :: Elab' aux ()
194attack = processTactic' Attack
196claim :: Name -> Raw -> Elab' aux ()
197claim n t = processTactic' (Claim n t)
199exact :: Raw -> Elab' aux ()
200exact t = processTactic' (Exact t)
202fill :: Raw -> Elab' aux ()
203fill t = processTactic' (Fill t)
205prep_fill :: Name -> [Name] -> Elab' aux ()
206prep_fill n ns = processTactic' (PrepFill n ns)
208complete_fill :: Elab' aux ()
209complete_fill = processTactic' CompleteFill
211solve :: Elab' aux ()
212solve = processTactic' Solve
214start_unify :: Name -> Elab' aux ()
215start_unify n = processTactic' (StartUnify n)
217end_unify :: Elab' aux ()
218end_unify = processTactic' EndUnify
220regret :: Elab' aux ()
221regret = processTactic' Regret
223compute :: Elab' aux ()
224compute = processTactic' Compute
226eval_in :: Raw -> Elab' aux ()
227eval_in t = processTactic' (EvalIn t)
229check_in :: Raw -> Elab' aux ()
230check_in t = processTactic' (CheckIn t)
232intro :: Maybe Name -> Elab' aux ()
233intro n = processTactic' (Intro n)
235introTy :: Raw -> Maybe Name -> Elab' aux ()
236introTy ty n = processTactic' (IntroTy ty n)
238forall :: Name -> Raw -> Elab' aux ()
239forall n t = processTactic' (Forall n t)
241letbind :: Name -> Raw -> Raw -> Elab' aux ()
242letbind n t v = processTactic' (LetBind n t v)
244rewrite :: Raw -> Elab' aux ()
245rewrite tm = processTactic' (Rewrite tm)
247patvar :: Name -> Elab' aux ()
248patvar n = do env <- get_env
249 if (n `elem` map fst env) then do apply (Var n) []; solve
250 else do n' <- case n of
251 UN _ -> return n
252 MN _ _ -> unique_hole n
253 NS _ _ -> return n
254 processTactic' (PatVar n')
256patbind :: Name -> Elab' aux ()
257patbind n = processTactic' (PatBind n)
259focus :: Name -> Elab' aux ()
260focus n = processTactic' (Focus n)
262movelast :: Name -> Elab' aux ()
263movelast n = processTactic' (MoveLast n)
265defer :: Name -> Elab' aux ()
266defer n = do n' <- unique_hole n
267 processTactic' (Defer n')
269deferType :: Name -> Raw -> [Name] -> Elab' aux ()
270deferType n ty ns = do n' <- unique_hole n
271 processTactic' (DeferType n' ty ns)
273instanceArg :: Name -> Elab' aux ()
274instanceArg n = processTactic' (Instance n)
276proofstate :: Elab' aux ()
277proofstate = processTactic' ProofState
279reorder_claims :: Name -> Elab' aux ()
280reorder_claims n = processTactic' (Reorder n)
282qed :: Elab' aux Term
283qed = do processTactic' QED
284 ES p _ _ <- get
285 return (pterm (fst p))
287undo :: Elab' aux ()
288undo = processTactic' Undo
290prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]
291prepare_apply fn imps =
292 do ty <- get_type fn
293 ctxt <- get_context
294 env <- get_env
295 -- let claims = getArgs ty imps
296 -- claims <- mkClaims (normalise ctxt env ty) imps []
297 claims <- mkClaims (finalise ty) imps [] (map fst env)
298 ES (p, a) s prev <- get
299 -- reverse the claims we made so that args go left to right
300 let n = length (filter not imps)
301 let (h : hs) = holes p
302 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
303-- case claims of
304-- [] -> return ()
305-- (h : _) -> reorder_claims h
306 return claims
307 where
308 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =
309 do let t = rebind hs t_in
310 n <- unique_hole (mkMN n')
311-- when (null claims) (start_unify n)
312 let sc' = instantiate (P Bound n t) sc
313-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show hs) $
314 claim n (forget t)
315 when i (movelast n)
316 mkClaims sc' is (n : claims) hs
317 mkClaims t [] claims _ = return (reverse claims)
318 mkClaims _ _ _ _
319 | Var n <- fn
320 = do ctxt <- get_context
321 case lookupTy Nothing n ctxt of
322 [] -> lift $ tfail $ NoSuchVariable n
323 _ -> fail $ "Too many arguments for " ++ show fn
324 | otherwise = fail $ "Too many arguments for " ++ show fn
326 doClaim ((i, _), n, t) = do claim n t
327 when i (movelast n)
329 mkMN n@(MN _ _) = n
330 mkMN n@(UN x) = MN 1000 x
331 mkMN (NS n xs) = NS (mkMN n) xs
333 rebind hs (Bind n t sc)
334 | n `elem` hs = let n' = uniqueName n hs in
335 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)
336 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)
337 rebind hs (App f a) = App (rebind hs f) (rebind hs a)
338 rebind hs t = t
340apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]
341apply fn imps =
342 do args <- prepare_apply fn (map fst imps)
343 fill (raw_apply fn (map Var args))
344 -- *Don't* solve the arguments we're specifying by hand.
345 -- (remove from unified list before calling end_unify)
346 -- HMMM: Actually, if we get it wrong, the typechecker will complain!
347 -- so do nothing
348 ptm <- get_term
349 hs <- get_holes
350 ES (p, a) s prev <- get
351 let dont = nub $ head hs : dontunify p ++
352 if null imps then [] -- do all we can
353 else
354 map fst (filter (not.snd) (zip args (map fst imps)))
355 let (n, hs) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $
356 unified p
357 let unify = dropGiven dont hs
358 put (ES (p { dontunify = dont, unified = (n, unify) }, a) s prev)
359 ptm <- get_term
360 end_unify
361 ptm <- get_term
362 return (map (updateUnify unify) args)
363 where updateUnify hs n = case lookup n hs of
364 Just (P _ t _) -> t
365 _ -> n
367apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
368apply2 fn elabs =
369 do args <- prepare_apply fn (map isJust elabs)
370 fill (raw_apply fn (map Var args))
371 elabArgs args elabs
372 ES (p, a) s prev <- get
373 let (n, hs) = unified p
374 end_unify
375 solve
376 where elabArgs [] [] = return ()
377 elabArgs (n:ns) (Just e:es) = do focus n; e
378 elabArgs ns es
379 elabArgs (n:ns) (_:es) = elabArgs ns es
381 isJust (Just _) = False
382 isJust _ = True
384apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
385apply_elab n args =
386 do ty <- get_type (Var n)
387 ctxt <- get_context
388 env <- get_env
389 claims <- doClaims (normalise ctxt env ty) args []
390 prep_fill n (map fst claims)
391 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
392 elabClaims [] False claims
393 complete_fill
394 end_unify
395 where
396 priOrder Nothing Nothing = EQ
397 priOrder Nothing _ = LT
398 priOrder _ Nothing = GT
399 priOrder (Just (x, _)) (Just (y, _)) = compare x y
401 doClaims (Bind n' (Pi t) sc) (i : is) claims =
402 do n <- unique_hole (mkMN n')
403 when (null claims) (start_unify n)
404 let sc' = instantiate (P Bound n t) sc
405 claim n (forget t)
406 case i of
407 Nothing -> return ()
408 Just _ -> -- don't solve by unification as there is an explicit value
409 do ES (p, a) s prev <- get
410 put (ES (p { dontunify = n : dontunify p }, a) s prev)
411 doClaims sc' is ((n, i) : claims)
412 doClaims t [] claims = return (reverse claims)
413 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
415 elabClaims failed r []
416 | null failed = return ()
417 | otherwise = if r then elabClaims [] False failed
418 else return ()
419 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
420 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
421 | r = try (do ES p _ _ <- get
422 focus n; elaboration; elabClaims failed r xs)
423 (elabClaims (e : failed) r xs)
424 | otherwise = do ES p _ _ <- get
425 focus n; elaboration; elabClaims failed r xs
427 mkMN n@(MN _ _) = n
428 mkMN n@(UN x) = MN 1000 x
429 mkMN (NS n ns) = NS (mkMN n) ns
431simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()
432simple_app fun arg =
433 do a <- unique_hole (MN 0 "a")
434 b <- unique_hole (MN 0 "b")
435 f <- unique_hole (MN 0 "f")
436 s <- unique_hole (MN 0 "s")
437 claim a RSet
438 claim b RSet
439 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))
440 start_unify s
441 claim s (Var a)
442 prep_fill f [s]
443 -- try elaborating in both orders, since we might learn something useful
444 -- either way
445 try (do focus s; arg
446 focus f; fun)
447 (do focus f; fun
448 focus s; arg)
449 complete_fill
450 hs <- get_holes
451 -- We don't need a and b in the hole queue any more since they were just for
452 -- checking f, so discard them if they are still there. If they haven't been solved,
453 -- regret will fail
454 when (a `elem` hs) $ do focus a; regret
455 when (b `elem` hs) $ do focus b; regret
456 end_unify
458-- Abstract over an argument of unknown type, giving a name for the hole
459-- which we'll fill with the argument type too.
460arg :: Name -> Name -> Elab' aux ()
461arg n tyhole = do ty <- unique_hole tyhole
462 claim ty RSet
463 forall n (Var ty)
465-- Try a tactic, if it fails, try another
466try :: Elab' aux a -> Elab' aux a -> Elab' aux a
467try t1 t2 = do s <- get
468 case runStateT t1 s of
469 OK (v, s') -> do put s'
470 return v
471 Error e1 -> if recoverableErr e1 then
472 do case runStateT t2 s of
473 OK (v, s') -> do put s'; return v
474 Error e2 -> if score e1 >= score e2
475 then lift (tfail e1)
476 else lift (tfail e2)
477 else lift (tfail e1)
478 where recoverableErr (CantUnify r _ _ _ _ _) = r
479 recoverableErr _ = True
481tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
482tryWhen True a b = try a b
483tryWhen False a b = a
486-- Try a selection of tactics. Exactly one must work, all others must fail
487tryAll :: [(Elab' aux a, String)] -> Elab' aux a
488tryAll xs = tryAll' [] (cantResolve, 0) (map fst xs)
489 where
490 cantResolve :: Elab' aux a
491 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
493 tryAll' :: [Elab' aux a] -> -- successes
494 (Elab' aux a, Int) -> -- smallest failure
495 [Elab' aux a] -> -- still to try
496 Elab' aux a
497 tryAll' [res] _ [] = res
498 tryAll' (_:_) _ [] = cantResolve
499 tryAll' [] (f, _) [] = f
500 tryAll' cs f (x:xs) = do s <- get
501 case runStateT x s of
502 OK (v, s') -> tryAll' ((do put s'
503 return v):cs) f xs
504 Error err -> do put s
505 if (score err) < 100
506 then
507 tryAll' cs (better err f) xs
508 else
509 tryAll' [] (better err f) xs -- give up
511 better err (f, i) = let s = score err in
512 if (s >= i) then (lift (tfail err), s)
513 else (f, i)