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